1 header {* CPS conversion *} |
1 header {* CPS conversion *} |
2 theory CPS1_Plotkin |
2 theory CPS1_Plotkin |
3 imports Lt |
3 imports Lt |
4 begin |
4 begin |
|
5 |
|
6 lemma Abs_lst_fcb2: |
|
7 fixes as bs :: "atom list" |
|
8 and x y :: "'b :: fs" |
|
9 and c::"'c::fs" |
|
10 assumes eq: "[as]lst. x = [bs]lst. y" |
|
11 and fcb1: "(set as) \<sharp>* c \<Longrightarrow> (set as) \<sharp>* f as x c" |
|
12 and fresh1: "set as \<sharp>* c" |
|
13 and fresh2: "set bs \<sharp>* c" |
|
14 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
|
15 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
|
16 shows "f as x c = f bs y c" |
|
17 proof - |
|
18 have "supp (as, x, c) supports (f as x c)" |
|
19 unfolding supports_def fresh_def[symmetric] |
|
20 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
|
21 then have fin1: "finite (supp (f as x c))" |
|
22 by (auto intro: supports_finite simp add: finite_supp) |
|
23 have "supp (bs, y, c) supports (f bs y c)" |
|
24 unfolding supports_def fresh_def[symmetric] |
|
25 by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) |
|
26 then have fin2: "finite (supp (f bs y c))" |
|
27 by (auto intro: supports_finite simp add: finite_supp) |
|
28 obtain q::"perm" where |
|
29 fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and |
|
30 fr2: "supp q \<sharp>* Abs_lst as x" and |
|
31 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
|
32 using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] |
|
33 fin1 fin2 |
|
34 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
|
35 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
|
36 also have "\<dots> = Abs_lst as x" |
|
37 by (simp only: fr2 perm_supp_eq) |
|
38 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp |
|
39 then obtain r::perm where |
|
40 qq1: "q \<bullet> x = r \<bullet> y" and |
|
41 qq2: "q \<bullet> as = r \<bullet> bs" and |
|
42 qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs" |
|
43 apply(drule_tac sym) |
|
44 apply(simp only: Abs_eq_iff2 alphas) |
|
45 apply(erule exE) |
|
46 apply(erule conjE)+ |
|
47 apply(drule_tac x="p" in meta_spec) |
|
48 apply(simp add: set_eqvt) |
|
49 apply(blast) |
|
50 done |
|
51 have "(set as) \<sharp>* f as x c" |
|
52 apply(rule fcb1) |
|
53 apply(rule fresh1) |
|
54 done |
|
55 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
|
56 by (simp add: permute_bool_def) |
|
57 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
|
58 apply(simp add: fresh_star_eqvt set_eqvt) |
|
59 apply(subst (asm) perm1) |
|
60 using inc fresh1 fr1 |
|
61 apply(auto simp add: fresh_star_def fresh_Pair) |
|
62 done |
|
63 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
64 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
|
65 apply(simp add: fresh_star_eqvt set_eqvt) |
|
66 apply(subst (asm) perm2[symmetric]) |
|
67 using qq3 fresh2 fr1 |
|
68 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
|
69 done |
|
70 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
|
71 have "f as x c = q \<bullet> (f as x c)" |
|
72 apply(rule perm_supp_eq[symmetric]) |
|
73 using inc fcb1[OF fresh1] fr1 by (auto simp add: fresh_star_def) |
|
74 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
|
75 apply(rule perm1) |
|
76 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
|
77 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
78 also have "\<dots> = r \<bullet> (f bs y c)" |
|
79 apply(rule perm2[symmetric]) |
|
80 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
|
81 also have "... = f bs y c" |
|
82 apply(rule perm_supp_eq) |
|
83 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
|
84 finally show ?thesis by simp |
|
85 qed |
|
86 |
|
87 lemma Abs_lst1_fcb2: |
|
88 fixes a b :: "atom" |
|
89 and x y :: "'b :: fs" |
|
90 and c::"'c :: fs" |
|
91 assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" |
|
92 and fcb1: "a \<sharp> c \<Longrightarrow> a \<sharp> f a x c" |
|
93 and fresh: "{a, b} \<sharp>* c" |
|
94 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
|
95 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
|
96 shows "f a x c = f b y c" |
|
97 using e |
|
98 apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"]) |
|
99 apply(simp_all) |
|
100 using fcb1 fresh perm1 perm2 |
|
101 apply(simp_all add: fresh_star_def) |
|
102 done |
5 |
103 |
6 nominal_primrec |
104 nominal_primrec |
7 CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250) |
105 CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250) |
8 where |
106 where |
9 "atom k \<sharp> x \<Longrightarrow> (x~)* = (Abs k ((k~) $ (x~)))" |
107 "atom k \<sharp> x \<Longrightarrow> (x~)* = (Abs k ((k~) $ (x~)))" |
41 apply simp_all[2] |
139 apply simp_all[2] |
42 apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp) |
140 apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp) |
43 apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp) |
141 apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp) |
44 --"-" |
142 --"-" |
45 apply (simp add: Abs1_eq(3)) |
143 apply (simp add: Abs1_eq(3)) |
46 apply (erule Abs_lst1_fcb) |
144 apply (erule Abs_lst1_fcb2) |
47 apply (simp add: fresh_def supp_Abs) |
145 apply (simp_all add: Abs_fresh_iff fresh_Nil fresh_star_def eqvt_at_def)[4] |
48 apply (drule_tac a="atom xa" in fresh_eqvt_at) |
|
49 apply (simp add: finite_supp) |
|
50 apply assumption |
|
51 apply (simp add: fresh_def supp_Abs) |
|
52 apply (simp add: eqvts eqvt_at_def) |
|
53 apply simp |
|
54 --"-" |
146 --"-" |
55 apply (rename_tac k' M N m' n') |
147 apply (rename_tac k' M N m' n') |
56 apply (subgoal_tac "atom k \<sharp> CPS_sumC M \<and> atom k' \<sharp> CPS_sumC M \<and> atom k \<sharp> CPS_sumC N \<and> atom k' \<sharp> CPS_sumC N \<and> |
148 apply (subgoal_tac "atom k \<sharp> CPS_sumC M \<and> atom k' \<sharp> CPS_sumC M \<and> atom k \<sharp> CPS_sumC N \<and> atom k' \<sharp> CPS_sumC N \<and> |
57 atom m \<sharp> CPS_sumC N \<and> atom m' \<sharp> CPS_sumC N") |
149 atom m \<sharp> CPS_sumC N \<and> atom m' \<sharp> CPS_sumC N") |
58 prefer 2 |
150 prefer 2 |