40 apply (simp add: eqvt_def) |
40 apply (simp add: eqvt_def) |
41 apply (simp add: fresh_def) |
41 apply (simp add: fresh_def) |
42 apply (rule contra_subsetD[OF supp_fun_app]) |
42 apply (rule contra_subsetD[OF supp_fun_app]) |
43 back |
43 back |
44 apply (simp add: supp_fun_eqvt lt.supp supp_at_base) |
44 apply (simp add: supp_fun_eqvt lt.supp supp_at_base) |
45 --"-" |
45 oops |
46 apply (rule arg_cong) |
|
47 back |
|
48 apply simp |
|
49 apply (thin_tac "eqvt ka") |
|
50 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
|
51 apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
52 prefer 2 |
|
53 apply (simp add: Abs1_eq_iff') |
|
54 apply (case_tac "c = a") |
|
55 apply simp_all[2] |
|
56 apply rule |
|
57 apply (simp add: eqvt_at_def) |
|
58 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
59 apply (erule fresh_eqvt_at) |
|
60 apply (simp add: supp_Inr finite_supp) |
|
61 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
62 apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
63 prefer 2 |
|
64 apply (simp add: Abs1_eq_iff') |
|
65 apply (case_tac "ca = a") |
|
66 apply simp_all[2] |
|
67 apply rule |
|
68 apply (simp add: eqvt_at_def) |
|
69 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
70 apply (erule fresh_eqvt_at) |
|
71 apply (simp add: supp_Inr finite_supp) |
|
72 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
73 apply (simp only: ) |
|
74 apply (erule Abs_lst1_fcb) |
|
75 apply (simp add: Abs_fresh_iff) |
|
76 apply (drule sym) |
|
77 apply (simp only:) |
|
78 apply (simp add: Abs_fresh_iff lt.fresh) |
|
79 apply clarify |
|
80 apply (erule fresh_eqvt_at) |
|
81 apply (simp add: supp_Inr finite_supp) |
|
82 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
83 apply (drule sym) |
|
84 apply (drule sym) |
|
85 apply (drule sym) |
|
86 apply (simp only:) |
|
87 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
88 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
89 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
90 apply (simp add: fresh_Pair_elim) |
|
91 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
92 back |
|
93 back |
|
94 back |
|
95 apply assumption |
|
96 apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
97 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
98 apply simp_all[3] |
|
99 apply rule |
|
100 apply (case_tac "c = xa") |
|
101 apply simp_all[2] |
|
102 apply (rotate_tac 1) |
|
103 apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm) |
|
104 apply (simp add: swap_fresh_fresh) |
|
105 apply (simp add: eqvt_at_def swap_fresh_fresh) |
|
106 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
|
107 apply (simp add: eqvt_at_def) |
|
108 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
|
109 apply simp |
|
110 apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh) |
|
111 apply (case_tac "c = xa") |
|
112 apply simp |
|
113 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
114 apply (simp add: atom_eqvt eqvt_at_def) |
|
115 apply (simp add: flip_fresh_fresh) |
|
116 apply (subst fresh_permute_iff) |
|
117 apply (erule fresh_eqvt_at) |
|
118 apply (simp add: supp_Inr finite_supp) |
|
119 apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
120 apply simp |
|
121 apply clarify |
|
122 apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
123 apply (simp add: eqvt_at_def) |
|
124 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
125 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
126 apply (erule fresh_eqvt_at) |
|
127 apply (simp add: finite_supp supp_Inr) |
|
128 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
129 apply rule |
|
130 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
131 apply (simp add: fresh_def supp_at_base) |
|
132 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
133 --"-" |
|
134 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
|
135 apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))") |
|
136 prefer 2 |
|
137 apply (simp add: Abs1_eq_iff') |
|
138 apply (case_tac "c = a") |
|
139 apply simp_all[2] |
|
140 apply rule |
|
141 apply (simp add: eqvt_at_def) |
|
142 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
143 apply (erule fresh_eqvt_at) |
|
144 apply (simp add: supp_Inr finite_supp) |
|
145 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
146 apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
|
147 prefer 2 |
|
148 apply (simp add: Abs1_eq_iff') |
|
149 apply (case_tac "ca = a") |
|
150 apply simp_all[2] |
|
151 apply rule |
|
152 apply (simp add: eqvt_at_def) |
|
153 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
|
154 apply (erule fresh_eqvt_at) |
|
155 apply (simp add: supp_Inr finite_supp) |
|
156 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
157 apply (simp only: ) |
|
158 apply (erule Abs_lst1_fcb) |
|
159 apply (simp add: Abs_fresh_iff) |
|
160 apply (drule sym) |
|
161 apply (simp only:) |
|
162 apply (simp add: Abs_fresh_iff lt.fresh) |
|
163 apply clarify |
|
164 apply (erule fresh_eqvt_at) |
|
165 apply (simp add: supp_Inr finite_supp) (* TODO put sum of fs into fs typeclass *) |
|
166 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
|
167 apply (drule sym) |
|
168 apply (drule sym) |
|
169 apply (drule sym) |
|
170 apply (simp only:) |
|
171 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") |
|
172 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
|
173 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
|
174 apply (simp add: fresh_Pair_elim) |
|
175 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
|
176 back |
|
177 back |
|
178 back |
|
179 apply assumption |
|
180 apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh) |
|
181 apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca") |
|
182 apply simp_all[3] |
|
183 apply rule |
|
184 apply (case_tac "c = xa") |
|
185 apply simp_all[2] |
|
186 apply (rotate_tac 1) |
|
187 apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm) |
|
188 apply (simp add: swap_fresh_fresh) |
|
189 apply (simp add: eqvt_at_def swap_fresh_fresh) |
|
190 apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))") |
|
191 apply (simp add: eqvt_at_def) |
|
192 apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec) |
|
193 apply simp |
|
194 apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh) |
|
195 apply (case_tac "c = xa") |
|
196 apply simp |
|
197 apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
198 apply (simp add: atom_eqvt eqvt_at_def) |
|
199 apply (simp add: flip_fresh_fresh) |
|
200 apply (subst fresh_permute_iff) |
|
201 apply (erule fresh_eqvt_at) |
|
202 apply (simp add: supp_Inr finite_supp) |
|
203 apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair) |
|
204 apply simp |
|
205 apply clarify |
|
206 apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))") |
|
207 apply (simp add: eqvt_at_def) |
|
208 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))") |
|
209 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
210 apply (erule fresh_eqvt_at) |
|
211 apply (simp add: finite_supp supp_Inr) |
|
212 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
|
213 apply rule |
|
214 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
|
215 apply (simp add: fresh_def supp_at_base) |
|
216 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
|
217 done |
|
218 |
|
219 termination (eqvt) |
|
220 by lexicographic_order |
|
221 |
|
222 definition psi:: "lt => lt" |
|
223 where [simp]: "psi V == V*(\<lambda>x. x)" |
|
224 |
|
225 section {* Simple consequence of CPS *} |
|
226 |
|
227 lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)" |
|
228 by (simp add: eqvt_def eqvt_bound eqvt_lambda) |
|
229 |
|
230 lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)" |
|
231 apply (cases V rule: lt.exhaust) |
|
232 apply simp_all |
|
233 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
234 apply simp |
|
235 done |
|
236 |
|
237 lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)" |
|
238 apply (cases V rule: lt.exhaust) |
|
239 apply simp_all |
|
240 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
|
241 apply simp |
|
242 done |
|
243 |
|
244 lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Lam n (k (Var n))))" |
|
245 by (cases M rule: lt.exhaust) auto |
|
246 |
|
247 |
46 |
248 |
47 |
249 end |
48 end |
250 |
49 |
251 |
50 |