equal
deleted
inserted
replaced
41 apply(rule_tac y="x" in lam.exhaust) |
41 apply(rule_tac y="x" in lam.exhaust) |
42 apply(auto)[3] |
42 apply(auto)[3] |
43 apply(all_trivials) |
43 apply(all_trivials) |
44 done |
44 done |
45 |
45 |
46 termination by lexicographic_order |
46 termination (eqvt) by lexicographic_order |
|
47 |
|
48 ML {* |
|
49 Item_Net.content; |
|
50 Nominal_Function_Common.get_function |
|
51 *} |
|
52 |
|
53 ML {* |
|
54 Item_Net.content (Nominal_Function_Common.get_function @{context}) |
|
55 *} |
|
56 |
47 |
57 |
48 lemma [eqvt]: |
58 lemma [eqvt]: |
49 shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)" |
59 shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)" |
50 apply(induct t rule: lam.induct) |
60 apply(induct t rule: lam.induct) |
51 apply(simp_all add: permute_bool_def) |
61 apply(simp_all add: permute_bool_def) |
63 apply(rule_tac y="x" in lam.exhaust) |
73 apply(rule_tac y="x" in lam.exhaust) |
64 apply(auto)[3] |
74 apply(auto)[3] |
65 apply(simp_all) |
75 apply(simp_all) |
66 done |
76 done |
67 |
77 |
68 termination by lexicographic_order |
78 termination (eqvt) by lexicographic_order |
69 |
79 |
70 lemma [eqvt]: |
80 lemma [eqvt]: |
71 shows "(p \<bullet> (rator t)) = rator (p \<bullet> t)" |
81 shows "(p \<bullet> (rator t)) = rator (p \<bullet> t)" |
72 apply(induct t rule: lam.induct) |
82 apply(induct t rule: lam.induct) |
73 apply(simp_all) |
83 apply(simp_all) |
85 apply(rule_tac y="x" in lam.exhaust) |
95 apply(rule_tac y="x" in lam.exhaust) |
86 apply(auto)[3] |
96 apply(auto)[3] |
87 apply(simp_all) |
97 apply(simp_all) |
88 done |
98 done |
89 |
99 |
90 termination by lexicographic_order |
100 termination (eqvt) by lexicographic_order |
91 |
101 |
92 lemma [eqvt]: |
102 lemma [eqvt]: |
93 shows "(p \<bullet> (rand t)) = rand (p \<bullet> t)" |
103 shows "(p \<bullet> (rand t)) = rand (p \<bullet> t)" |
94 apply(induct t rule: lam.induct) |
104 apply(induct t rule: lam.induct) |
95 apply(simp_all) |
105 apply(simp_all) |
116 apply(simp add: eqvt_at_def conj_eqvt) |
126 apply(simp add: eqvt_at_def conj_eqvt) |
117 apply(perm_simp) |
127 apply(perm_simp) |
118 apply(rule refl) |
128 apply(rule refl) |
119 done |
129 done |
120 |
130 |
121 termination by lexicographic_order |
131 termination (eqvt) by lexicographic_order |
122 |
132 |
123 nominal_datatype path = Left | Right | In |
133 nominal_datatype path = Left | Right | In |
124 |
134 |
125 section {* Paths to a free variables *} |
135 section {* Paths to a free variables *} |
126 |
136 |
153 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq) |
163 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq) |
154 apply(perm_simp) |
164 apply(perm_simp) |
155 apply(rule refl) |
165 apply(rule refl) |
156 done |
166 done |
157 |
167 |
158 termination by lexicographic_order |
168 termination (eqvt) by lexicographic_order |
159 |
169 |
160 lemma var_pos1: |
170 lemma var_pos1: |
161 assumes "atom y \<notin> supp t" |
171 assumes "atom y \<notin> supp t" |
162 shows "var_pos y t = {}" |
172 shows "var_pos y t = {}" |
163 using assms |
173 using assms |
193 apply(simp add: fresh_star_def fresh_Pair) |
203 apply(simp add: fresh_star_def fresh_Pair) |
194 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
204 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
195 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
205 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
196 done |
206 done |
197 |
207 |
198 termination by lexicographic_order |
208 termination (eqvt) by lexicographic_order |
199 |
209 |
200 |
210 |
201 section {* free name function *} |
211 section {* free name function *} |
202 |
212 |
203 text {* first returns an atom list *} |
213 text {* first returns an atom list *} |
219 apply(simp add: fresh_star_def fresh_Unit) |
229 apply(simp add: fresh_star_def fresh_Unit) |
220 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
230 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
221 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
231 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
222 done |
232 done |
223 |
233 |
224 termination by lexicographic_order |
234 termination (eqvt) by lexicographic_order |
225 |
235 |
226 text {* a small test lemma *} |
236 text {* a small test lemma *} |
227 lemma shows "supp t = set (frees_lst t)" |
237 lemma shows "supp t = set (frees_lst t)" |
228 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
238 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
229 |
239 |
247 apply(simp add: fresh_star_def fresh_Unit) |
257 apply(simp add: fresh_star_def fresh_Unit) |
248 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
258 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
249 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
259 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
250 done |
260 done |
251 |
261 |
252 termination |
262 termination (eqvt) |
253 by lexicographic_order |
263 by lexicographic_order |
254 |
264 |
255 lemma "frees_set t = supp t" |
265 lemma "frees_set t = supp t" |
256 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) |
266 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) |
257 |
267 |
270 apply(auto) |
280 apply(auto) |
271 apply (erule_tac c="()" in Abs_lst1_fcb2) |
281 apply (erule_tac c="()" in Abs_lst1_fcb2) |
272 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
282 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
273 done |
283 done |
274 |
284 |
275 termination |
285 termination (eqvt) |
276 by lexicographic_order |
286 by lexicographic_order |
277 |
287 |
278 thm height.simps |
288 thm height.simps |
279 |
289 |
280 |
290 |
298 apply(simp add: fresh_star_def fresh_Pair) |
308 apply(simp add: fresh_star_def fresh_Pair) |
299 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
309 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
300 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
310 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
301 done |
311 done |
302 |
312 |
303 termination |
313 termination (eqvt) |
304 by lexicographic_order |
314 by lexicographic_order |
305 |
315 |
306 lemma subst_eqvt[eqvt]: |
316 lemma subst_eqvt[eqvt]: |
307 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
317 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
308 by (induct t x s rule: subst.induct) (simp_all) |
318 by (induct t x s rule: subst.induct) (simp_all) |
484 apply (simp add: fresh_star_def) |
494 apply (simp add: fresh_star_def) |
485 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
495 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
486 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
496 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
487 done |
497 done |
488 |
498 |
489 termination |
499 termination (eqvt) |
490 by lexicographic_order |
500 by lexicographic_order |
491 |
501 |
492 |
502 |
493 text {* count the occurences of lambdas in a term *} |
503 text {* count the occurences of lambdas in a term *} |
494 |
504 |
511 apply(simp add: fresh_star_def pure_fresh) |
521 apply(simp add: fresh_star_def pure_fresh) |
512 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
522 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
513 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
523 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
514 done |
524 done |
515 |
525 |
516 termination |
526 termination (eqvt) |
517 by lexicographic_order |
527 by lexicographic_order |
518 |
528 |
519 |
529 |
520 text {* count the bound-variable occurences in a lambda-term *} |
530 text {* count the bound-variable occurences in a lambda-term *} |
521 |
531 |
541 apply(simp add: fresh_star_def) |
551 apply(simp add: fresh_star_def) |
542 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
552 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
543 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
553 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
544 done |
554 done |
545 |
555 |
546 termination |
556 termination (eqvt) |
547 by lexicographic_order |
557 by lexicographic_order |
548 |
558 |
549 section {* De Bruijn Terms *} |
559 section {* De Bruijn Terms *} |
550 |
560 |
551 nominal_datatype db = |
561 nominal_datatype db = |
592 apply (simp add: pure_fresh) |
602 apply (simp add: pure_fresh) |
593 apply(simp add: fresh_star_def fresh_at_list) |
603 apply(simp add: fresh_star_def fresh_at_list) |
594 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+ |
604 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+ |
595 done |
605 done |
596 |
606 |
597 termination |
607 termination (eqvt) |
598 by lexicographic_order |
608 by lexicographic_order |
599 |
609 |
600 lemma transdb_eqvt[eqvt]: |
610 lemma transdb_eqvt[eqvt]: |
601 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
611 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
602 apply (nominal_induct t avoiding: l rule: lam.strong_induct) |
612 apply (nominal_induct t avoiding: l rule: lam.strong_induct) |
663 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
673 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
664 done |
674 done |
665 |
675 |
666 |
676 |
667 (* a small test |
677 (* a small test |
668 termination sorry |
678 termination (eqvt) sorry |
669 |
679 |
670 lemma |
680 lemma |
671 assumes "x \<noteq> y" |
681 assumes "x \<noteq> y" |
672 shows "eval (App (Lam [x].App (Var x) (Var x)) (Var y)) = App (Var y) (Var y)" |
682 shows "eval (App (Lam [x].App (Var x) (Var x)) (Var y)) = App (Var y) (Var y)" |
673 using assms |
683 using assms |
717 apply (erule Abs_lst1_fcb) |
727 apply (erule Abs_lst1_fcb) |
718 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
728 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
719 apply (simp add: eqvt_def permute_fun_app_eq) |
729 apply (simp add: eqvt_def permute_fun_app_eq) |
720 done |
730 done |
721 |
731 |
722 termination |
732 termination (eqvt) |
723 by lexicographic_order |
733 by lexicographic_order |
724 |
734 |
725 |
735 |
726 (* |
736 (* |
727 abbreviation |
737 abbreviation |