equal
deleted
inserted
replaced
47 apply (rule arg_cong) |
47 apply (rule arg_cong) |
48 back |
48 back |
49 apply simp |
49 apply simp |
50 apply (thin_tac "eqvt ka") |
50 apply (thin_tac "eqvt ka") |
51 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
51 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
52 apply (subgoal_tac "eqvt_at CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
53 apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
52 apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
54 prefer 2 |
53 prefer 2 |
55 apply (simp add: Abs1_eq_iff') |
54 apply (simp add: Abs1_eq_iff') |
56 apply (case_tac "c = a") |
55 apply (case_tac "c = a") |
57 apply simp_all[2] |
56 apply simp_all[2] |
128 apply rule |
127 apply rule |
129 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
128 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
130 apply (simp add: fresh_def supp_at_base) |
129 apply (simp add: fresh_def supp_at_base) |
131 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
130 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
132 --"-" |
131 --"-" |
133 prefer 2 |
|
134 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
132 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
135 apply (subgoal_tac "eqvt_at CPS1_CPS2_sumC (Inr (Ma, ca~))") |
|
136 apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
133 apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
137 prefer 2 |
134 prefer 2 |
138 apply (simp add: Abs1_eq_iff') |
135 apply (simp add: Abs1_eq_iff') |
139 apply (case_tac "c = a") |
136 apply (case_tac "c = a") |
140 apply simp_all[2] |
137 apply simp_all[2] |
210 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
207 apply (simp add: fresh_Inr fresh_Pair lt.fresh) |
211 apply rule |
208 apply rule |
212 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
209 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
213 apply (simp add: fresh_def supp_at_base) |
210 apply (simp add: fresh_def supp_at_base) |
214 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
211 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
215 --"Only left subgoals are eqvt for the other side" |
212 done |
216 oops |
213 |
217 |
214 termination |
218 (*termination |
215 by lexicographic_order |
219 sorry |
|
220 |
216 |
221 definition psi:: "lt => lt" |
217 definition psi:: "lt => lt" |
222 where "psi V == V*(\<lambda>x. x)" |
218 where "psi V == V*(\<lambda>x. x)" |
223 |
219 |
224 section {* Simple consequence of CPS *} |
220 section {* Simple consequence of CPS *} |
235 apply (subst CPS1.simps(3)) |
231 apply (subst CPS1.simps(3)) |
236 apply (simp add: eqvt_def eqvt_bound eqvt_lambda) |
232 apply (simp add: eqvt_def eqvt_bound eqvt_lambda) |
237 apply assumption |
233 apply assumption |
238 apply rule |
234 apply rule |
239 done |
235 done |
240 *) |
|
241 |
236 |
242 end |
237 end |
243 |
238 |
244 |
239 |
245 |
240 |