38 where |
38 where |
39 "is_app (Var x) = False" |
39 "is_app (Var x) = False" |
40 | "is_app (App t1 t2) = True" |
40 | "is_app (App t1 t2) = True" |
41 | "is_app (Lam [x]. t) = False" |
41 | "is_app (Lam [x]. t) = False" |
42 apply(simp add: eqvt_def is_app_graph_def) |
42 apply(simp add: eqvt_def is_app_graph_def) |
43 apply (rule, perm_simp, rule) |
|
44 apply(rule TrueI) |
43 apply(rule TrueI) |
45 apply(rule_tac y="x" in lam.exhaust) |
44 apply(rule_tac y="x" in lam.exhaust) |
46 apply(auto)[3] |
45 apply(auto)[3] |
47 apply(all_trivials) |
46 apply(all_trivials) |
48 done |
47 done |
59 where |
58 where |
60 "rator (Var x) = None" |
59 "rator (Var x) = None" |
61 | "rator (App t1 t2) = Some t1" |
60 | "rator (App t1 t2) = Some t1" |
62 | "rator (Lam [x]. t) = None" |
61 | "rator (Lam [x]. t) = None" |
63 apply(simp add: eqvt_def rator_graph_def) |
62 apply(simp add: eqvt_def rator_graph_def) |
64 apply (rule, perm_simp, rule) |
|
65 apply(rule TrueI) |
63 apply(rule TrueI) |
66 apply(rule_tac y="x" in lam.exhaust) |
64 apply(rule_tac y="x" in lam.exhaust) |
67 apply(auto)[3] |
65 apply(auto)[3] |
68 apply(simp_all) |
66 apply(simp_all) |
69 done |
67 done |
75 where |
73 where |
76 "rand (Var x) = None" |
74 "rand (Var x) = None" |
77 | "rand (App t1 t2) = Some t2" |
75 | "rand (App t1 t2) = Some t2" |
78 | "rand (Lam [x]. t) = None" |
76 | "rand (Lam [x]. t) = None" |
79 apply(simp add: eqvt_def rand_graph_def) |
77 apply(simp add: eqvt_def rand_graph_def) |
80 apply (rule, perm_simp, rule) |
|
81 apply(rule TrueI) |
78 apply(rule TrueI) |
82 apply(rule_tac y="x" in lam.exhaust) |
79 apply(rule_tac y="x" in lam.exhaust) |
83 apply(auto)[3] |
80 apply(auto)[3] |
84 apply(simp_all) |
81 apply(simp_all) |
85 done |
82 done |
92 "is_eta_nf (Var x) = True" |
89 "is_eta_nf (Var x) = True" |
93 | "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)" |
90 | "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)" |
94 | "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> |
91 | "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> |
95 ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))" |
92 ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))" |
96 apply(simp add: eqvt_def is_eta_nf_graph_def) |
93 apply(simp add: eqvt_def is_eta_nf_graph_def) |
97 apply (rule, perm_simp, rule) |
|
98 apply(rule TrueI) |
94 apply(rule TrueI) |
99 apply(rule_tac y="x" in lam.exhaust) |
95 apply(rule_tac y="x" in lam.exhaust) |
100 apply(auto)[3] |
96 apply(auto)[3] |
101 apply(simp_all) |
97 apply(simp_all) |
102 apply(erule_tac c="()" in Abs_lst1_fcb2') |
98 apply(erule_tac c="()" in Abs_lst1_fcb2') |
103 apply(simp_all add: pure_fresh fresh_star_def)[3] |
99 apply(simp_all add: pure_fresh fresh_star_def)[3] |
104 apply(simp add: eqvt_at_def conj_eqvt) |
100 apply(simp add: eqvt_at_def conj_eqvt) |
105 apply(perm_simp) |
|
106 apply(rule refl) |
|
107 apply(simp add: eqvt_at_def conj_eqvt) |
101 apply(simp add: eqvt_at_def conj_eqvt) |
108 apply(perm_simp) |
|
109 apply(rule refl) |
|
110 done |
102 done |
111 |
103 |
112 termination (eqvt) by lexicographic_order |
104 termination (eqvt) by lexicographic_order |
113 |
105 |
114 nominal_datatype path = Left | Right | In |
106 nominal_datatype path = Left | Right | In |
126 where |
118 where |
127 "var_pos y (Var x) = (if y = x then {[]} else {})" |
119 "var_pos y (Var x) = (if y = x then {[]} else {})" |
128 | "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))" |
120 | "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))" |
129 | "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))" |
121 | "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))" |
130 apply(simp add: eqvt_def var_pos_graph_def) |
122 apply(simp add: eqvt_def var_pos_graph_def) |
131 apply (rule, perm_simp, rule) |
|
132 apply(rule TrueI) |
123 apply(rule TrueI) |
133 apply(case_tac x) |
124 apply(case_tac x) |
134 apply(rule_tac y="b" and c="a" in lam.strong_exhaust) |
125 apply(rule_tac y="b" and c="a" in lam.strong_exhaust) |
135 apply(auto simp add: fresh_star_def)[3] |
126 apply(auto simp add: fresh_star_def)[3] |
136 apply(simp_all) |
127 apply(simp_all) |
137 apply(erule conjE)+ |
128 apply(erule conjE)+ |
138 apply(erule_tac Abs_lst1_fcb2) |
129 apply(erule_tac Abs_lst1_fcb2) |
139 apply(simp add: pure_fresh) |
130 apply(simp add: pure_fresh) |
140 apply(simp add: fresh_star_def) |
131 apply(simp add: fresh_star_def) |
141 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq) |
132 apply(simp only: eqvt_at_def) |
142 apply(perm_simp) |
133 apply(perm_simp) |
143 apply(rule refl) |
134 apply(simp) |
144 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq) |
135 apply(simp add: perm_supp_eq) |
|
136 apply(simp only: eqvt_at_def) |
145 apply(perm_simp) |
137 apply(perm_simp) |
146 apply(rule refl) |
138 apply(simp) |
|
139 apply(simp add: perm_supp_eq) |
147 done |
140 done |
148 |
141 |
149 termination (eqvt) by lexicographic_order |
142 termination (eqvt) by lexicographic_order |
150 |
143 |
151 lemma var_pos1: |
144 lemma var_pos1: |
170 where |
163 where |
171 "(Var x)[y ::== s] = (if x = y then s else (Var x))" |
164 "(Var x)[y ::== s] = (if x = y then s else (Var x))" |
172 | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])" |
165 | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])" |
173 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])" |
166 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])" |
174 apply(simp add: eqvt_def subst'_graph_def) |
167 apply(simp add: eqvt_def subst'_graph_def) |
175 apply(perm_simp, simp) |
|
176 apply(rule TrueI) |
168 apply(rule TrueI) |
177 apply(case_tac x) |
169 apply(case_tac x) |
178 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
170 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
179 apply(auto simp add: fresh_star_def)[3] |
171 apply(auto simp add: fresh_star_def)[3] |
180 apply(simp_all) |
172 apply(simp_all) |
181 apply(erule conjE)+ |
173 apply(erule conjE)+ |
182 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
174 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
183 apply(simp_all add: Abs_fresh_iff) |
175 apply(simp_all add: Abs_fresh_iff) |
184 apply(simp add: fresh_star_def fresh_Pair) |
176 apply(simp add: fresh_star_def fresh_Pair) |
185 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
177 apply(simp only: eqvt_at_def) |
186 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
178 apply(perm_simp) |
|
179 apply(simp) |
|
180 apply(simp add: fresh_star_Pair perm_supp_eq) |
|
181 apply(simp only: eqvt_at_def) |
|
182 apply(perm_simp) |
|
183 apply(simp) |
|
184 apply(simp add: fresh_star_Pair perm_supp_eq) |
187 done |
185 done |
188 |
186 |
189 termination (eqvt) by lexicographic_order |
187 termination (eqvt) by lexicographic_order |
190 |
188 |
191 |
189 |
199 "frees_lst (Var x) = [atom x]" |
197 "frees_lst (Var x) = [atom x]" |
200 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
198 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
201 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
199 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
202 unfolding eqvt_def |
200 unfolding eqvt_def |
203 unfolding frees_lst_graph_def |
201 unfolding frees_lst_graph_def |
204 apply (rule, perm_simp, rule) |
202 apply(simp) |
205 apply(rule TrueI) |
203 apply(rule TrueI) |
206 apply(rule_tac y="x" in lam.exhaust) |
204 apply(rule_tac y="x" in lam.exhaust) |
207 apply(auto) |
205 apply(auto) |
208 apply (erule_tac c="()" in Abs_lst1_fcb2) |
206 apply (erule_tac c="()" in Abs_lst1_fcb2) |
209 apply(simp add: supp_removeAll fresh_def) |
207 apply(simp add: supp_removeAll fresh_def) |
225 where |
223 where |
226 "frees_set (Var x) = {atom x}" |
224 "frees_set (Var x) = {atom x}" |
227 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
225 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
228 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}" |
226 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}" |
229 apply(simp add: eqvt_def frees_set_graph_def) |
227 apply(simp add: eqvt_def frees_set_graph_def) |
230 apply(rule, perm_simp, rule) |
|
231 apply(erule frees_set_graph.induct) |
228 apply(erule frees_set_graph.induct) |
232 apply(auto)[9] |
229 apply(auto)[9] |
233 apply(rule_tac y="x" in lam.exhaust) |
230 apply(rule_tac y="x" in lam.exhaust) |
234 apply(auto)[3] |
231 apply(auto)[3] |
235 apply(simp) |
232 apply(simp) |
236 apply(erule_tac c="()" in Abs_lst1_fcb2) |
233 apply(erule_tac c="()" in Abs_lst1_fcb2) |
237 apply(simp add: fresh_minus_atom_set) |
234 apply(simp add: fresh_minus_atom_set) |
238 apply(simp add: fresh_star_def fresh_Unit) |
235 apply(simp add: fresh_star_def fresh_Unit) |
239 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
236 apply(simp add: Diff_eqvt eqvt_at_def) |
240 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
237 apply(simp add: Diff_eqvt eqvt_at_def) |
241 done |
238 done |
242 |
239 |
243 termination (eqvt) |
240 termination (eqvt) |
244 by lexicographic_order |
241 by lexicographic_order |
245 |
242 |
253 where |
250 where |
254 "height (Var x) = 1" |
251 "height (Var x) = 1" |
255 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
252 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
256 | "height (Lam [x].t) = height t + 1" |
253 | "height (Lam [x].t) = height t + 1" |
257 apply(simp add: eqvt_def height_graph_def) |
254 apply(simp add: eqvt_def height_graph_def) |
258 apply (rule, perm_simp, rule) |
|
259 apply(rule TrueI) |
255 apply(rule TrueI) |
260 apply(rule_tac y="x" in lam.exhaust) |
256 apply(rule_tac y="x" in lam.exhaust) |
261 apply(auto) |
257 apply(auto) |
262 apply (erule_tac c="()" in Abs_lst1_fcb2) |
258 apply (erule_tac c="()" in Abs_lst1_fcb2) |
263 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
259 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
276 where |
272 where |
277 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
273 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
278 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
274 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
279 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
275 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
280 unfolding eqvt_def subst_graph_def |
276 unfolding eqvt_def subst_graph_def |
281 apply (rule, perm_simp, rule) |
277 apply(simp) |
282 apply(rule TrueI) |
278 apply(rule TrueI) |
283 apply(auto) |
279 apply(auto) |
284 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
280 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
285 apply(blast)+ |
281 apply(blast)+ |
286 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
282 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
287 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
283 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
288 apply(simp_all add: Abs_fresh_iff) |
284 apply(simp_all add: Abs_fresh_iff) |
289 apply(simp add: fresh_star_def fresh_Pair) |
285 apply(simp add: fresh_star_def fresh_Pair) |
290 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
286 apply(simp only: eqvt_at_def) |
291 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
287 apply(perm_simp) |
|
288 apply(simp) |
|
289 apply(simp add: fresh_star_Pair perm_supp_eq) |
|
290 apply(simp only: eqvt_at_def) |
|
291 apply(perm_simp) |
|
292 apply(simp) |
|
293 apply(simp add: fresh_star_Pair perm_supp_eq) |
292 done |
294 done |
293 |
295 |
294 termination (eqvt) |
296 termination (eqvt) |
295 by lexicographic_order |
297 by lexicographic_order |
296 |
298 |
455 where |
457 where |
456 "trans (Var x) xs = lookup xs 0 x" |
458 "trans (Var x) xs = lookup xs 0 x" |
457 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
459 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
458 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
460 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
459 apply (simp add: eqvt_def trans_graph_def) |
461 apply (simp add: eqvt_def trans_graph_def) |
460 apply (rule, perm_simp, rule) |
|
461 apply (erule trans_graph.induct) |
462 apply (erule trans_graph.induct) |
462 apply (auto simp add: ln.fresh)[3] |
463 apply (auto simp add: ln.fresh)[3] |
463 apply (simp add: supp_lookup_fresh) |
464 apply (simp add: supp_lookup_fresh) |
464 apply (simp add: fresh_star_def ln.fresh) |
465 apply (simp add: fresh_star_def ln.fresh) |
465 apply (simp add: ln.fresh fresh_star_def) |
466 apply (simp add: ln.fresh fresh_star_def) |
469 apply(simp_all) |
470 apply(simp_all) |
470 apply(erule conjE)+ |
471 apply(erule conjE)+ |
471 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
472 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
472 apply (simp add: fresh_star_def) |
473 apply (simp add: fresh_star_def) |
473 apply (simp add: fresh_star_def) |
474 apply (simp add: fresh_star_def) |
474 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
475 apply(simp only: eqvt_at_def) |
475 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
476 apply(perm_simp) |
|
477 apply(simp add: fresh_star_Pair perm_supp_eq) |
|
478 apply(simp only: eqvt_at_def) |
|
479 apply(perm_simp) |
|
480 apply(simp add: fresh_star_Pair perm_supp_eq) |
476 done |
481 done |
477 |
482 |
478 termination (eqvt) |
483 termination (eqvt) |
479 by lexicographic_order |
484 by lexicographic_order |
480 |
485 |
486 where |
491 where |
487 "cntlams (Var x) = 0" |
492 "cntlams (Var x) = 0" |
488 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)" |
493 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)" |
489 | "cntlams (Lam [x]. t) = Suc (cntlams t)" |
494 | "cntlams (Lam [x]. t) = Suc (cntlams t)" |
490 apply(simp add: eqvt_def cntlams_graph_def) |
495 apply(simp add: eqvt_def cntlams_graph_def) |
491 apply(rule, perm_simp, rule) |
|
492 apply(rule TrueI) |
496 apply(rule TrueI) |
493 apply(rule_tac y="x" in lam.exhaust) |
497 apply(rule_tac y="x" in lam.exhaust) |
494 apply(auto)[3] |
498 apply(auto)[3] |
495 apply(all_trivials) |
499 apply(all_trivials) |
496 apply(simp) |
500 apply(simp) |
513 where |
517 where |
514 "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)" |
518 "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)" |
515 | "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)" |
519 | "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)" |
516 | "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)" |
520 | "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)" |
517 apply(simp add: eqvt_def cntbvs_graph_def) |
521 apply(simp add: eqvt_def cntbvs_graph_def) |
518 apply(rule, perm_simp, rule) |
|
519 apply(rule TrueI) |
522 apply(rule TrueI) |
520 apply(case_tac x) |
523 apply(case_tac x) |
521 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
524 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
522 apply(auto simp add: fresh_star_def)[3] |
525 apply(auto simp add: fresh_star_def)[3] |
523 apply(all_trivials) |
526 apply(all_trivials) |
526 apply(simp) |
529 apply(simp) |
527 apply(erule conjE) |
530 apply(erule conjE) |
528 apply(erule Abs_lst1_fcb2') |
531 apply(erule Abs_lst1_fcb2') |
529 apply(simp add: pure_fresh fresh_star_def) |
532 apply(simp add: pure_fresh fresh_star_def) |
530 apply(simp add: fresh_star_def) |
533 apply(simp add: fresh_star_def) |
531 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
534 apply(simp only: eqvt_at_def) |
532 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
535 apply(perm_simp) |
|
536 apply(simp add: fresh_star_Pair perm_supp_eq) |
|
537 apply(simp only: eqvt_at_def) |
|
538 apply(perm_simp) |
|
539 apply(simp add: fresh_star_Pair perm_supp_eq) |
533 done |
540 done |
534 |
541 |
535 termination (eqvt) |
542 termination (eqvt) |
536 by lexicographic_order |
543 by lexicographic_order |
537 |
544 |
568 "transdb (Var x) l = vindex l x 0" |
575 "transdb (Var x) l = vindex l x 0" |
569 | "transdb (App t1 t2) xs = |
576 | "transdb (App t1 t2) xs = |
570 Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))" |
577 Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))" |
571 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" |
578 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" |
572 unfolding eqvt_def transdb_graph_def |
579 unfolding eqvt_def transdb_graph_def |
573 apply (rule, perm_simp, rule) |
580 apply(simp) |
574 apply(rule TrueI) |
581 apply(rule TrueI) |
575 apply (case_tac x) |
582 apply (case_tac x) |
576 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
583 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
577 apply (auto simp add: fresh_star_def fresh_at_list)[3] |
584 apply (auto simp add: fresh_star_def fresh_at_list)[3] |
578 apply(simp_all) |
585 apply(simp_all) |
579 apply(elim conjE) |
586 apply(elim conjE) |
580 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
587 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
581 apply (simp add: pure_fresh) |
588 apply (simp add: pure_fresh) |
582 apply(simp add: fresh_star_def fresh_at_list) |
589 apply(simp add: fresh_star_def fresh_at_list) |
583 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+ |
590 apply(simp only: eqvt_at_def) |
|
591 apply(perm_simp) |
|
592 apply(simp) |
|
593 apply(simp add: fresh_star_Pair perm_supp_eq) |
|
594 apply(simp only: eqvt_at_def) |
|
595 apply(perm_simp) |
|
596 apply(simp) |
|
597 apply(simp add: fresh_star_Pair perm_supp_eq) |
584 done |
598 done |
585 |
599 |
586 termination (eqvt) |
600 termination (eqvt) |
587 by lexicographic_order |
601 by lexicographic_order |
588 |
602 |
622 | "eval (App t1 t2) = apply_subst (eval t1) (eval t2)" |
636 | "eval (App t1 t2) = apply_subst (eval t1) (eval t2)" |
623 | "apply_subst (Var x) t2 = App (Var x) t2" |
637 | "apply_subst (Var x) t2 = App (Var x) t2" |
624 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2" |
638 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2" |
625 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])" |
639 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])" |
626 apply(simp add: eval_apply_subst_graph_def eqvt_def) |
640 apply(simp add: eval_apply_subst_graph_def eqvt_def) |
627 apply(rule, perm_simp, rule) |
|
628 apply(rule TrueI) |
641 apply(rule TrueI) |
629 apply (case_tac x) |
642 apply (case_tac x) |
630 apply (case_tac a rule: lam.exhaust) |
643 apply (case_tac a rule: lam.exhaust) |
631 apply simp_all[3] |
644 apply simp_all[3] |
632 apply blast |
645 apply blast |
646 apply(erule_tac c="t2a" in Abs_lst1_fcb2') |
659 apply(erule_tac c="t2a" in Abs_lst1_fcb2') |
647 apply (erule fresh_eqvt_at) |
660 apply (erule fresh_eqvt_at) |
648 apply (simp add: finite_supp) |
661 apply (simp add: finite_supp) |
649 apply (simp add: fresh_Inl var_fresh_subst) |
662 apply (simp add: fresh_Inl var_fresh_subst) |
650 apply(simp add: fresh_star_def) |
663 apply(simp add: fresh_star_def) |
651 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt) |
664 apply(simp only: eqvt_at_def) |
652 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt) |
665 apply(perm_simp) |
|
666 apply(simp add: fresh_star_Pair perm_supp_eq) |
|
667 apply(simp only: eqvt_at_def) |
|
668 apply(perm_simp) |
|
669 apply(simp add: fresh_star_Pair perm_supp_eq) |
653 done |
670 done |
654 |
671 |
655 |
672 |
656 (* a small test |
673 (* a small test |
657 termination (eqvt) sorry |
674 termination (eqvt) sorry |
669 nominal_primrec q where |
686 nominal_primrec q where |
670 "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))" |
687 "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))" |
671 | "q (Var x) N = Var x" |
688 | "q (Var x) N = Var x" |
672 | "q (App l r) N = App l r" |
689 | "q (App l r) N = App l r" |
673 unfolding eqvt_def q_graph_def |
690 unfolding eqvt_def q_graph_def |
674 apply (rule, perm_simp, rule) |
691 apply (simp) |
675 apply (rule TrueI) |
692 apply (rule TrueI) |
676 apply (case_tac x) |
693 apply (case_tac x) |
677 apply (rule_tac y="a" in lam.exhaust) |
694 apply (rule_tac y="a" in lam.exhaust) |
678 apply simp_all |
695 apply simp_all |
679 apply blast |
696 apply blast |
697 "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)" |
714 "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)" |
698 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)" |
715 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)" |
699 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)" |
716 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)" |
700 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
717 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
701 apply (simp add: eqvt_def map_term_graph_def) |
718 apply (simp add: eqvt_def map_term_graph_def) |
702 apply (rule, perm_simp, rule) |
|
703 apply(rule TrueI) |
719 apply(rule TrueI) |
704 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
720 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
705 apply auto |
721 apply auto |
706 apply (erule Abs_lst1_fcb) |
722 apply (erule Abs_lst1_fcb) |
707 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
723 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
817 | "aux (Lam [x].t) (Var y) xs = False" |
833 | "aux (Lam [x].t) (Var y) xs = False" |
818 | "aux (Lam [x].t) (App t1 t2) xs = False" |
834 | "aux (Lam [x].t) (App t1 t2) xs = False" |
819 | "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> |
835 | "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> |
820 aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)" |
836 aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)" |
821 apply (simp add: eqvt_def aux_graph_def) |
837 apply (simp add: eqvt_def aux_graph_def) |
822 apply (rule, perm_simp, rule) |
|
823 apply(erule aux_graph.induct) |
838 apply(erule aux_graph.induct) |
824 apply(simp_all add: fresh_star_def pure_fresh)[9] |
839 apply(simp_all add: fresh_star_def pure_fresh)[9] |
825 apply(case_tac x) |
840 apply(case_tac x) |
826 apply(simp) |
841 apply(simp) |
827 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
842 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
865 | "aux2 (App t1 t2) (Lam [x].t) = False" |
880 | "aux2 (App t1 t2) (Lam [x].t) = False" |
866 | "aux2 (Lam [x].t) (Var y) = False" |
881 | "aux2 (Lam [x].t) (Var y) = False" |
867 | "aux2 (Lam [x].t) (App t1 t2) = False" |
882 | "aux2 (Lam [x].t) (App t1 t2) = False" |
868 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s" |
883 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s" |
869 apply(simp add: eqvt_def aux2_graph_def) |
884 apply(simp add: eqvt_def aux2_graph_def) |
870 apply(rule, perm_simp, rule, rule) |
885 apply(simp) |
871 apply(case_tac x) |
886 apply(case_tac x) |
872 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
887 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
873 apply(rule_tac y="b" in lam.exhaust) |
888 apply(rule_tac y="b" in lam.exhaust) |
874 apply(auto)[3] |
889 apply(auto)[3] |
875 apply(rule_tac y="b" in lam.exhaust) |
890 apply(rule_tac y="b" in lam.exhaust) |