12 (M $ N)* = Lam k (M* $ Lam m (N* $ Lam n (m~ $ n~ $ k~)))" |
12 (M $ N)* = Lam k (M* $ Lam m (N* $ Lam n (m~ $ n~ $ k~)))" |
13 unfolding eqvt_def CPS_graph_def |
13 unfolding eqvt_def CPS_graph_def |
14 apply (rule, perm_simp, rule, rule) |
14 apply (rule, perm_simp, rule, rule) |
15 apply (simp_all add: fresh_Pair_elim) |
15 apply (simp_all add: fresh_Pair_elim) |
16 apply (rule_tac y="x" in lt.exhaust) |
16 apply (rule_tac y="x" in lt.exhaust) |
17 apply (auto) |
17 apply (auto)[3] |
18 apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
18 apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
19 apply (simp_all add: fresh_at_base)[3] |
19 apply (simp_all add: fresh_at_base)[3] |
20 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh) |
20 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh) |
21 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh) |
21 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh) |
22 apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh) |
22 apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh) |
26 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base) |
26 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base) |
27 --"-" |
27 --"-" |
28 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans) |
28 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans) |
29 apply (case_tac "k = ka") |
29 apply (case_tac "k = ka") |
30 apply simp |
30 apply simp |
31 apply(simp (no_asm) add: Abs1_eq_iff del:eqvts) |
31 thm Abs1_eq_iff |
32 apply (simp del: eqvts add: lt.fresh fresh_at_base) |
32 apply(subst Abs1_eq_iff) |
|
33 apply(auto)[2] |
|
34 apply(rule disjI2) |
|
35 apply(rule conjI) |
|
36 apply(simp) |
|
37 apply(rule conjI) |
33 apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff) |
38 apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff) |
34 apply (subst flip_at_base_simps(2)) |
39 apply (subst flip_at_base_simps(2)) |
35 apply simp |
40 apply(simp) |
36 apply (intro conjI refl) |
41 apply (intro conjI refl) |
37 apply (rule flip_fresh_fresh[symmetric]) |
42 apply (rule flip_fresh_fresh[symmetric]) |
38 apply (simp_all add: lt.fresh) |
43 apply (simp_all add: lt.fresh) |
39 apply (metis fresh_eqvt_at lt.fsupp) |
44 apply (metis fresh_eqvt_at lt.fsupp) |
40 apply (case_tac "ka = x") |
45 apply (case_tac "ka = x") |
123 apply (simp add: fresh_Pair_elim fresh_at_base) |
128 apply (simp add: fresh_Pair_elim fresh_at_base) |
124 apply (auto simp add: Abs1_eq_iff eqvts)[1] |
129 apply (auto simp add: Abs1_eq_iff eqvts)[1] |
125 apply (rename_tac M N u K) |
130 apply (rename_tac M N u K) |
126 apply (subgoal_tac "Lam n (M+ $ n~ $ K) = Lam u (M+ $ u~ $ K)") |
131 apply (subgoal_tac "Lam n (M+ $ n~ $ K) = Lam u (M+ $ u~ $ K)") |
127 apply (simp only:) |
132 apply (simp only:) |
128 apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1] |
133 apply (auto simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)[1] |
129 apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))") |
134 apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))") |
130 apply (simp only:) |
135 apply (simp only:) |
131 apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base) |
136 apply (simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base) |
132 apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka") |
137 apply(simp_all add: flip_def[symmetric]) |
133 apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka") |
|
134 apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka") |
|
135 apply (case_tac "m = ma") |
138 apply (case_tac "m = ma") |
136 apply simp_all |
139 apply simp_all |
137 apply rule |
140 apply (case_tac "m = na") |
138 apply (auto simp add: flip_fresh_fresh[symmetric]) |
141 apply(simp_all add: flip_fresh_fresh) |
139 apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+ |
|
140 done |
142 done |
141 |
143 |
142 termination (eqvt) |
144 termination (eqvt) |
143 by (relation "measure (\<lambda>(t, _). size t)") (simp_all) |
145 by (relation "measure (\<lambda>(t, _). size t)") (simp_all) |
144 |
146 |
225 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1") |
227 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1") |
226 assume e: "isValue lt1" |
228 assume e: "isValue lt1" |
227 have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+" |
229 have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+" |
228 using * d e by simp |
230 using * d e by simp |
229 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)" |
231 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)" |
230 by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base) |
232 by (rule evbeta')(simp_all add: * d e) |
231 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2") |
233 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2") |
232 assume f: "isValue lt2" |
234 assume f: "isValue lt2" |
233 have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp |
235 have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp |
234 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K" |
236 also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K" |
235 by (rule evbeta', simp_all add: d e f) |
237 by (rule evbeta', simp_all add: d e f) |