Up to index of Isabelle/HOL/PI

(* 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