10 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))" |
10 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))" |
11 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow> |
11 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow> |
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 using [[simproc del: alpha_lst]] |
15 apply (simp_all add: fresh_Pair_elim) |
16 apply (simp_all add: fresh_Pair_elim) |
16 apply (rule_tac y="x" in lt.exhaust) |
17 apply (rule_tac y="x" in lt.exhaust) |
17 apply (auto)[3] |
18 apply (auto)[3] |
18 apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
19 apply (rule_tac x="name" and ?'a="name" in obtain_fresh) |
|
20 using [[simproc del: alpha_lst]] |
19 apply (simp_all add: fresh_at_base)[3] |
21 apply (simp_all add: fresh_at_base)[3] |
20 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh) |
22 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) |
23 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) |
24 apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh) |
23 apply (simp add: fresh_Pair_elim fresh_at_base) |
25 apply (simp add: fresh_Pair_elim fresh_at_base) |
79 | "(Lam x M)+ = Lam x (M*)" |
81 | "(Lam x M)+ = Lam x (M*)" |
80 | "(M $$ N)+ = M $$ N" |
82 | "(M $$ N)+ = M $$ N" |
81 unfolding convert_graph_def eqvt_def |
83 unfolding convert_graph_def eqvt_def |
82 apply (rule, perm_simp, rule, rule) |
84 apply (rule, perm_simp, rule, rule) |
83 apply (erule lt.exhaust) |
85 apply (erule lt.exhaust) |
|
86 using [[simproc del: alpha_lst]] |
84 apply (simp_all) |
87 apply (simp_all) |
85 apply blast |
88 apply blast |
86 apply (simp add: Abs1_eq_iff CPS.eqvt) |
89 apply (simp add: Abs1_eq_iff CPS.eqvt) |
87 by blast |
90 by blast |
88 |
91 |
111 Kapply (M $$ N) K = N; (Lam n (M+ $$ Var n $$ K))" |
114 Kapply (M $$ N) K = N; (Lam n (M+ $$ Var n $$ K))" |
112 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
115 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> |
113 Kapply (M $$ N) K = M; (Lam m (N* $$ (Lam n (Var m $$ Var n $$ K))))" |
116 Kapply (M $$ N) K = M; (Lam m (N* $$ (Lam n (Var m $$ Var n $$ K))))" |
114 unfolding Kapply_graph_def eqvt_def |
117 unfolding Kapply_graph_def eqvt_def |
115 apply (rule, perm_simp, rule, rule) |
118 apply (rule, perm_simp, rule, rule) |
|
119 using [[simproc del: alpha_lst]] |
116 apply (simp_all) |
120 apply (simp_all) |
117 apply (case_tac x) |
121 apply (case_tac x) |
118 apply (rule_tac y="a" in lt.exhaust) |
122 apply (rule_tac y="a" in lt.exhaust) |
119 apply (auto) |
123 apply (auto) |
120 apply (case_tac "isValue lt1") |
124 apply (case_tac "isValue lt1") |