Theory ProcExp

Up to index of Isabelle/HOL/PI

theory ProcExp = ProcExt
files [ProcExp.ML]:
(* Title:    ProcExp.thy
   Author:   Christine Roeckl

ProcExp establishes that it is possible for all well-formed
processes to abstract over a name in its body. This result is called
beta-expansion, and is the reverse wrt. beta-reduction.
*)

ProcExp = ProcExt +

types
  'a trlist = "(('a::inf_class) * ('a => 'a)) list"


(* derive a transformation list *)
consts
  mk_trl :: ('a::inf_class) list => 'a => ('a trlist)

primrec
  mtr1 "mk_trl [] a = []"
  mtr2 "mk_trl (x#xs) a = (if x = a then (mk_trl xs a) \
                                  \ else (x, (%y. x))#(mk_trl xs a))"


(* well-formed abstractions over transformation lists *)
consts
  WFTRL :: (('a::inf_class) => 'a trlist) set

syntax
  "@WFTRL" :: (('a::inf_class) => 'a trlist) => bool
              ("wftrl (_)" [100] 90)

translations
  "wftrl fxs" == "fxs : WFTRL"

inductive WFTRL
  intrs
    etrl  "wftrl (%x. [])"
    ctrl  "[| wfnaa ffa ; wftrl fxs |] \
           \ ==> wftrl (%x. (a, ffa x)#fxs x)"


(* transform a name according to a transformation list xs *)
consts
  trn :: ('a::inf_class) => 'a trlist => ('a => 'a)

primrec
  trn1 "trn a [] = (%x. x)"
  trn2 "trn a (x#xs) = (if a = fst x then snd x else (trn a xs))"


(* transform a process according to a transformation list xs using
   a list of fresh names ys *)
consts
  tr :: ('a::inf_class) procs => 'a trlist => 'a list => ('a => 'a procs)

primrec
  tr0 "tr (.0) xs ys = (%x. .0)"
  tr1 "tr (.t.P) xs ys = (%x. .t.(tr P xs ys) x)"
  tr2 "tr (a<b>.P) xs ys = (%x. (trn a xs) x<(trn b xs) x>. \
          \ (tr P xs ys) x)"
  tr3 "tr (In a fP) xs ys = (%x. (trn a xs) x[y]. \
          \ (tr (fP (hd ys)) ((hd ys, (%x. y))#xs) (tl ys)) x)"
  tr4 "tr (Res fP) xs ys = (%x. .#y. \
          \ (tr (fP (hd ys)) ((hd ys, (%x. y))#xs) (tl ys)) x)"
  tr5 "tr (P .+ Q) xs ys = (%x. (tr P xs ys) x .+ (tr Q xs ys) x)"
  tr6 "tr (P .| Q) xs ys = (%x. (tr P xs ys) x .| (tr Q xs ys) x)"
  tr7 "tr (.[a.=b]P) xs ys = (%x. .[(trn a xs) x.=(trn b xs) x] \
          \ (tr P xs ys) x)"
  tr8 "tr (.[a.~=b]P) xs ys = (%x. .[(trn a xs) x.~=(trn b xs) x] \
          \ (tr P xs ys) x)"
  tr9 "tr (.!P) xs ys = (%x. .!(tr P xs ys) x)"

end


theorem dob3':

  dob (In a fP) c = Suc (doba fP c)

theorem dob4':

  dob (Res fP) c = Suc (doba fP c)

theorem a_not_in_trl:

  a ~: set (map fst (mk_trl xs a))

theorem mk_trl_contain:

  set xs <= insert a (set (map fst (mk_trl xs a)))

theorem lemma:

  set (map fst (mk_trl xs a)) <= set xs

theorem mk_trl_map_fst:

  insert a (set (map fst (mk_trl xs a))) = insert a (set xs)

theorem mk_trl_wfna:

  ALL x:set (mk_trl xs a). wfna snd x

theorem lemma:

  b ~: insert a (set xs) --> (ALL x:set (mk_trl xs a). a ~= snd x b)

theorem mk_trl_ineq:

  b ~: insert a (set xs) ==> ALL x:set (mk_trl xs a). a ~= snd x b

theorem mk_trl_const:

  ALL x:set (mk_trl xs a). snd x = (%y. fst x)

theorem lemma:

  (ALL x:set xs. wfna snd x) --> wfna trn a xs

theorem wfna_trn:

  ALL x:set xs. wfna snd x ==> wfna trn a xs

theorem const_trl_wfna_trl:

  ALL x:set xs. snd x = (%y. fst x) ==> ALL x:set xs. wfna snd x

theorem lemma:

  (ALL x:set xs. snd x = (%y. fst x)) & b : insert a (set (map fst xs)) -->
  trn b xs a = b

theorem const_trn:

  [| ALL x:set xs. snd x = (%y. fst x); b : insert a (set (map fst xs)) |]
  ==> trn b xs a = b

theorem lemma:

  (ALL x:set xs. wfna snd x) --> wftrl (%x. xs)

theorem wfna_wftrl:

  ALL x:set xs. wfna snd x ==> wftrl (%x. xs)

theorem wftrl_wfna:

  wftrl fxs ==> ALL x:set (fxs a). wfna snd x

theorem wftrl_cons1:

  wftrl fxs ==> wftrl (%x. (a, %y. b) # fxs c)

theorem wftrl_cons2:

  wftrl fxs ==> wftrl (%x. (a, %y. x) # fxs c)

theorem wftrl_cons3:

  wftrl fxs ==> wftrl (%x. (a, %y. b) # fxs x)

theorem wftrl_cons4:

  wftrl fxs ==> wftrl (%x. (a, %y. x) # fxs x)

theorem wftrl_wfna_trn1:

  wftrl fxs ==> wfna trn a (fxs b)

theorem wftrl_wfna_trn2:

  wftrl fxs ==> wfna (%x. trn a (fxs x) b)

theorem lemma:

  (ALL x:set xs. a ~= snd x b) & a ~= b --> a ~= trn c xs b

theorem trn_fresh:

  [| ALL x:set xs. a ~= snd x b; a ~= b |] ==> a ~= trn c xs b

theorem lemma:

  wfpa fP
  ==> ALL xs ys.
         (ALL x:set xs. a ~= snd x b) & a ~= b --> a ~: fn (tr (fP c) xs ys b)

theorem tr_not_fn_abs:

  [| wfpa fP; ALL x:set xs. a ~= snd x b; a ~= b |]
  ==> a ~: fn (tr (fP c) xs ys b)

theorem lemma:

  wfp P ==> (ALL x:set xs. a ~= snd x b) & a ~= b --> a ~: fn (tr P xs ys b)

theorem tr_not_fn:

  [| wfp P; ALL x:set xs. a ~= snd x b; a ~= b |] ==> a ~: fn (tr P xs ys b)

theorem tr_fresh_abs:

  [| wfpa fP; ALL x:set xs. a ~= snd x b; a ~= b |]
  ==> fresh a (tr (fP c) xs ys b)

theorem tr_fresh:

  [| wfp P; ALL x:set xs. a ~= snd x b; a ~= b |] ==> fresh a (tr P xs ys b)

theorem inst_hyp1:

  [| ALL b fxs ys d.
        wftrl fxs -->
        wfpa tr (ffP b c) (fxs d) ys & wfpa (%x. tr (ffP b c) (fxs x) ys d);
     wftrl fxs |]
  ==> wfpa tr (ffP e c) ((e, %y. b) # fxs d) ys

theorem inst_hyp2:

  [| ALL b fxs ys d.
        wftrl fxs -->
        wfpa tr (ffP b c) (fxs d) ys & wfpa (%x. tr (ffP b c) (fxs x) ys d);
     wftrl fxs |]
  ==> wfpa (%x. tr (ffP e c) ((e, %y. x) # fxs d) ys b)

theorem inst_hyp3:

  [| ALL b fxs ys d.
        wftrl fxs -->
        wfpa tr (ffP b c) (fxs d) ys & wfpa (%x. tr (ffP b c) (fxs x) ys d);
     wftrl fxs |]
  ==> wfpa (%x. tr (ffP e c) ((e, %y. d) # fxs x) ys b)

theorem lemma:

  wfpa fP
  ==> ALL fxs ys d.
         wftrl fxs -->
         wfpa tr (fP c) (fxs d) ys & wfpa (%x. tr (fP c) (fxs x) ys d)

theorem tr_wfpa_abs1:

  [| wfpa fP; wftrl fxs |] ==> wfpa tr (fP c) (fxs b) ys

theorem tr_wfpa_abs2:

  [| wfpa fP; wftrl fxs |] ==> wfpa (%x. tr (fP c) (fxs x) ys b)

theorem lemma:

  wfp P ==> (ALL x:set xs. wfna snd x) --> wfpa tr P xs ys

theorem tr_wfpa:

  [| wfp P; ALL x:set xs. wfna snd x |] ==> wfpa tr P xs ys

theorem inst_hyp:

  [| ALL b xs ys.
        (ALL x:set xs. snd x = (%y. fst x)) &
        doba (ffP b) c <= length ys &
        fna (ffP b) <= insert a (set (map fst xs)) &
        a ~: set (map fst xs) &
        d : set (map fst xs) &
        nodups ys & set ys Int insert a (set (map fst xs)) = {} -->
        tr (ffP b d) xs ys a = ffP b d;
     ALL b. wfpa ffP b; ALL b. wfpa (%x. ffP x b);
     ALL x:set xs. snd x = (%y. fst x); Suc (doba (ffP c) c) <= length ys;
     fnaa ffP <= insert a (set (map fst xs)); a ~: set (map fst xs);
     d : set (map fst xs); nodups ys;
     set ys Int insert a (set (map fst xs)) = {} |]
  ==> (%y. tr (ffP (hd ys) d) ((hd ys, %x. y) # xs) (tl ys) a) = (%y. ffP y d)

theorem lemma:

  wfpa fP
  ==> ALL xs ys.
         (ALL x:set xs. snd x = (%y. fst x)) &
         doba fP c <= length ys &
         fna fP <= insert a (set (map fst xs)) &
         a ~: set (map fst xs) &
         d : set (map fst xs) &
         nodups ys & set ys Int insert a (set (map fst xs)) = {} -->
         tr (fP d) xs ys a = fP d

theorem tr_eq_abs:

  [| wfpa fP; ALL x:set xs. snd x = (%y. fst x); doba fP c <= length ys;
     fna fP <= insert a (set (map fst xs)); a ~: set (map fst xs);
     d : set (map fst xs); nodups ys;
     set ys Int insert a (set (map fst xs)) = {} |]
  ==> tr (fP d) xs ys a = fP d

theorem inst_hyp:

  [| wfpa fP; ALL x:set xs. snd x = (%y. fst x); Suc (doba fP c) <= length ys;
     fna fP <= insert a (set (map fst xs)); a ~: set (map fst xs); nodups ys;
     set ys Int insert a (set (map fst xs)) = {} |]
  ==> (%y. tr (fP (hd ys)) ((hd ys, %x. y) # xs) (tl ys) a) = fP

theorem lemma:

  wfp P
  ==> ALL xs ys.
         (ALL x:set xs. snd x = (%y. fst x)) &
         dob P c <= length ys &
         fn P <= insert a (set (map fst xs)) &
         a ~: set (map fst xs) &
         nodups ys & set ys Int insert a (set (map fst xs)) = {} -->
         tr P xs ys a = P

theorem tr_eq:

  [| wfp P; ALL x:set xs. snd x = (%y. fst x); dob P c <= length ys;
     fn P <= insert a (set (map fst xs)); a ~: set (map fst xs); nodups ys;
     set ys Int insert a (set (map fst xs)) = {} |]
  ==> tr P xs ys a = P

theorem finite_insert_fn:

  finite (insert a (fn P))

theorem beta_exp:

  wfp P ==> EX fP. wfpa fP & fresha a fP & P = fP a

theorem beta_expa:

  wfpa fP
  ==> EX ffP.
         (ALL b. wfpa ffP b) &
         (ALL b. wfpa (%x. ffP x b)) & freshaa a ffP & fP = ffP a