73 height :: "lam \<Rightarrow> int" |
73 height :: "lam \<Rightarrow> int" |
74 where |
74 where |
75 "height (Var x) = 1" |
75 "height (Var x) = 1" |
76 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
76 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
77 | "height (Lam [x].t) = height t + 1" |
77 | "height (Lam [x].t) = height t + 1" |
78 defer |
78 unfolding eqvt_def height_graph_def |
|
79 apply (rule, perm_simp, rule) |
79 apply(rule_tac y="x" in lam.exhaust) |
80 apply(rule_tac y="x" in lam.exhaust) |
80 apply(auto simp add: lam.distinct lam.eq_iff) |
81 apply(auto simp add: lam.distinct lam.eq_iff) |
81 apply (erule Abs1_eq_fdest) |
82 apply (erule Abs1_eq_fdest) |
82 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
83 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
83 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") |
|
84 unfolding eqvt_def |
|
85 apply(rule allI) |
|
86 apply(simp add: permute_fun_def) |
|
87 apply(rule ext) |
|
88 apply(rule ext) |
|
89 apply(simp add: permute_bool_def) |
|
90 apply(rule iffI) |
|
91 apply(drule_tac x="p" in meta_spec) |
|
92 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
93 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
94 apply(simp) |
|
95 apply(drule_tac x="-p" in meta_spec) |
|
96 apply(drule_tac x="x" in meta_spec) |
|
97 apply(drule_tac x="xa" in meta_spec) |
|
98 apply(simp) |
|
99 apply(erule height_graph.induct) |
|
100 apply(perm_simp) |
|
101 apply(rule height_graph.intros) |
|
102 apply(perm_simp) |
|
103 apply(rule height_graph.intros) |
|
104 apply(assumption) |
|
105 apply(assumption) |
|
106 apply(perm_simp) |
|
107 apply(rule height_graph.intros) |
|
108 apply(assumption) |
|
109 done |
84 done |
110 |
85 |
111 termination |
86 termination |
112 by (relation "measure size") (simp_all add: lam.size) |
87 by (relation "measure size") (simp_all add: lam.size) |
113 |
88 |
120 frees_lst :: "lam \<Rightarrow> atom list" |
95 frees_lst :: "lam \<Rightarrow> atom list" |
121 where |
96 where |
122 "frees_lst (Var x) = [atom x]" |
97 "frees_lst (Var x) = [atom x]" |
123 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
98 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
124 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
99 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
125 defer |
100 unfolding eqvt_def frees_lst_graph_def |
|
101 apply (rule, perm_simp, rule) |
126 apply(rule_tac y="x" in lam.exhaust) |
102 apply(rule_tac y="x" in lam.exhaust) |
127 apply(simp_all)[3] |
103 apply(simp_all)[3] |
128 apply(auto)[1] |
104 apply(auto)[1] |
129 apply(simp_all) |
105 apply(simp_all) |
130 apply (erule Abs1_eq_fdest) |
106 apply (erule Abs1_eq_fdest) |
131 apply(simp add: supp_removeAll fresh_def) |
107 apply(simp add: supp_removeAll fresh_def) |
132 apply(drule supp_eqvt_at) |
108 apply(drule supp_eqvt_at) |
133 apply(simp add: finite_supp) |
109 apply(simp add: finite_supp) |
134 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
110 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
135 apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") |
|
136 unfolding eqvt_def |
|
137 apply(rule allI) |
|
138 apply(simp add: permute_fun_def) |
|
139 apply(rule ext) |
|
140 apply(rule ext) |
|
141 apply(simp add: permute_bool_def) |
|
142 apply(rule iffI) |
|
143 apply(drule_tac x="p" in meta_spec) |
|
144 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
145 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
146 apply(simp) |
|
147 apply(drule_tac x="-p" in meta_spec) |
|
148 apply(drule_tac x="x" in meta_spec) |
|
149 apply(drule_tac x="xa" in meta_spec) |
|
150 apply(simp) |
|
151 apply(erule frees_lst_graph.induct) |
|
152 apply(perm_simp) |
|
153 apply(rule frees_lst_graph.intros) |
|
154 apply(perm_simp) |
|
155 apply(rule frees_lst_graph.intros) |
|
156 apply(assumption) |
|
157 apply(assumption) |
|
158 apply(perm_simp) |
|
159 apply(rule frees_lst_graph.intros) |
|
160 apply(assumption) |
|
161 done |
111 done |
162 |
112 |
163 termination |
113 termination |
164 apply(relation "measure size") |
114 apply(relation "measure size") |
165 apply(simp_all add: lam.size) |
115 apply(simp_all add: lam.size) |
178 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
128 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
179 where |
129 where |
180 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
130 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
181 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
131 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
182 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
132 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
183 defer |
133 unfolding eqvt_def subst_graph_def |
|
134 apply (rule, perm_simp, rule) |
184 apply(auto simp add: lam.distinct lam.eq_iff) |
135 apply(auto simp add: lam.distinct lam.eq_iff) |
185 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
136 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
186 apply(blast)+ |
137 apply(blast)+ |
187 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
138 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
188 apply (erule Abs1_eq_fdest) |
139 apply (erule Abs1_eq_fdest) |
191 apply(simp_all add: finite_supp fresh_Pair) |
142 apply(simp_all add: finite_supp fresh_Pair) |
192 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
143 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
193 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
144 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
194 apply(simp add: eqvt_at_def) |
145 apply(simp add: eqvt_at_def) |
195 apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ |
146 apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ |
196 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
|
197 unfolding eqvt_def |
|
198 apply(rule allI) |
|
199 apply(simp add: permute_fun_def) |
|
200 apply(rule ext) |
|
201 apply(rule ext) |
|
202 apply(simp add: permute_bool_def) |
|
203 apply(rule iffI) |
|
204 apply(drule_tac x="p" in meta_spec) |
|
205 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
206 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
207 apply(simp) |
|
208 apply(drule_tac x="-p" in meta_spec) |
|
209 apply(drule_tac x="x" in meta_spec) |
|
210 apply(drule_tac x="xa" in meta_spec) |
|
211 apply(simp) |
|
212 apply(erule subst_graph.induct) |
|
213 apply(perm_simp) |
|
214 apply(rule subst_graph.intros) |
|
215 apply(perm_simp) |
|
216 apply(rule subst_graph.intros) |
|
217 apply(assumption) |
|
218 apply(assumption) |
|
219 apply(perm_simp) |
|
220 apply(rule subst_graph.intros) |
|
221 apply(simp add: fresh_Pair) |
|
222 apply(assumption) |
|
223 done |
147 done |
224 |
148 |
225 termination |
149 termination |
226 by (relation "measure (\<lambda>(t,_,_). size t)") |
150 by (relation "measure (\<lambda>(t,_,_). size t)") |
227 (simp_all add: lam.size) |
151 (simp_all add: lam.size) |
372 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
296 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
373 where |
297 where |
374 "trans (Var x) xs = lookup xs 0 x" |
298 "trans (Var x) xs = lookup xs 0 x" |
375 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
299 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
376 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
300 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
377 defer |
301 unfolding eqvt_def trans_graph_def |
|
302 apply (rule, perm_simp, rule) |
378 apply(case_tac x) |
303 apply(case_tac x) |
379 apply(simp) |
304 apply(simp) |
380 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
305 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
381 apply(simp_all add: fresh_star_def)[3] |
306 apply(simp_all add: fresh_star_def)[3] |
382 apply(blast) |
307 apply(blast) |