5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
6 and |
6 and |
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
8 where |
8 where |
9 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |
9 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |
10 | "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Abs c (k (c~)))))))" |
10 | "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))" |
11 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(c~))))" |
11 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))" |
12 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t" |
12 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t" |
13 | "(x~)^l = l $ (x~)" |
13 | "(x~)^l = l $ (x~)" |
14 | "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))" |
14 | "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))" |
15 | "atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))" |
15 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))" |
16 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
16 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
17 apply (rule, perm_simp, rule) |
17 apply (rule, perm_simp, rule) |
18 apply auto |
18 apply auto |
19 apply (case_tac x) |
19 apply (case_tac x) |
20 apply (case_tac a) |
20 apply (case_tac a) |
29 apply blast |
29 apply blast |
30 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
30 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) |
31 apply (simp add: fresh_at_base Abs1_eq_iff) |
31 apply (simp add: fresh_at_base Abs1_eq_iff) |
32 apply blast |
32 apply blast |
33 --"-" |
33 --"-" |
34 apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))") |
34 apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))") |
35 apply (simp only:) |
35 apply (simp only:) |
36 apply (simp add: Abs1_eq_iff) |
36 apply (simp add: Abs1_eq_iff) |
37 apply (case_tac "c=ca") |
37 apply (case_tac "c=ca") |
38 apply simp_all[2] |
38 apply simp_all[2] |
39 apply rule |
39 apply rule |
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 "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
52 apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))") |
53 prefer 2 |
53 prefer 2 |
54 apply (simp add: Abs1_eq_iff') |
54 apply (simp add: Abs1_eq_iff') |
55 apply (case_tac "c = a") |
55 apply (case_tac "c = a") |
56 apply simp_all[2] |
56 apply simp_all[2] |
57 apply rule |
57 apply rule |
58 apply (simp add: eqvt_at_def) |
58 apply (simp add: eqvt_at_def) |
59 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
59 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
60 apply (erule fresh_eqvt_at) |
60 apply (erule fresh_eqvt_at) |
61 apply (simp add: supp_Inr finite_supp) |
61 apply (simp add: supp_Inr finite_supp) |
62 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
62 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
63 apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
63 apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
64 prefer 2 |
64 prefer 2 |
65 apply (simp add: Abs1_eq_iff') |
65 apply (simp add: Abs1_eq_iff') |
66 apply (case_tac "ca = a") |
66 apply (case_tac "ca = a") |
67 apply simp_all[2] |
67 apply simp_all[2] |
68 apply rule |
68 apply rule |
83 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
83 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
84 apply (drule sym) |
84 apply (drule sym) |
85 apply (drule sym) |
85 apply (drule sym) |
86 apply (drule sym) |
86 apply (drule sym) |
87 apply (simp only:) |
87 apply (simp only:) |
88 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))") |
88 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") |
89 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
89 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
90 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
90 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
91 apply (simp add: fresh_Pair_elim) |
91 apply (simp add: fresh_Pair_elim) |
92 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
92 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
93 back |
93 back |
94 back |
94 back |
131 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
131 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
132 apply (simp add: fresh_def supp_at_base) |
132 apply (simp add: fresh_def supp_at_base) |
133 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
133 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
134 --"-" |
134 --"-" |
135 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
135 apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh) |
136 apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))") |
136 apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))") |
137 prefer 2 |
137 prefer 2 |
138 apply (simp add: Abs1_eq_iff') |
138 apply (simp add: Abs1_eq_iff') |
139 apply (case_tac "c = a") |
139 apply (case_tac "c = a") |
140 apply simp_all[2] |
140 apply simp_all[2] |
141 apply rule |
141 apply rule |
142 apply (simp add: eqvt_at_def) |
142 apply (simp add: eqvt_at_def) |
143 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
143 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
144 apply (erule fresh_eqvt_at) |
144 apply (erule fresh_eqvt_at) |
145 apply (simp add: supp_Inr finite_supp) |
145 apply (simp add: supp_Inr finite_supp) |
146 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
146 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
147 apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
147 apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))") |
148 prefer 2 |
148 prefer 2 |
149 apply (simp add: Abs1_eq_iff') |
149 apply (simp add: Abs1_eq_iff') |
150 apply (case_tac "ca = a") |
150 apply (case_tac "ca = a") |
151 apply simp_all[2] |
151 apply simp_all[2] |
152 apply rule |
152 apply rule |
167 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
167 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
168 apply (drule sym) |
168 apply (drule sym) |
169 apply (drule sym) |
169 apply (drule sym) |
170 apply (drule sym) |
170 apply (drule sym) |
171 apply (simp only:) |
171 apply (simp only:) |
172 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))") |
172 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") |
173 apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
173 apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))") |
174 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
174 apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)") |
175 apply (simp add: fresh_Pair_elim) |
175 apply (simp add: fresh_Pair_elim) |
176 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
176 apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]]) |
177 back |
177 back |
178 back |
178 back |