equal
deleted
inserted
replaced
84 apply(rule_tac y="x" in lam.exhaust) |
84 apply(rule_tac y="x" in lam.exhaust) |
85 apply(auto)[3] |
85 apply(auto)[3] |
86 apply(all_trivials) |
86 apply(all_trivials) |
87 done |
87 done |
88 |
88 |
89 termination (eqvt) by lexicographic_order |
89 nominal_termination (eqvt) by lexicographic_order |
90 |
90 |
91 thm is_app_def |
91 thm is_app_def |
92 thm is_app.eqvt |
92 thm is_app.eqvt |
93 |
93 |
94 thm eqvts |
94 thm eqvts |
104 apply(rule_tac y="x" in lam.exhaust) |
104 apply(rule_tac y="x" in lam.exhaust) |
105 apply(auto)[3] |
105 apply(auto)[3] |
106 apply(simp_all) |
106 apply(simp_all) |
107 done |
107 done |
108 |
108 |
109 termination (eqvt) by lexicographic_order |
109 nominal_termination (eqvt) by lexicographic_order |
110 |
110 |
111 nominal_function |
111 nominal_function |
112 rand :: "lam \<Rightarrow> lam option" |
112 rand :: "lam \<Rightarrow> lam option" |
113 where |
113 where |
114 "rand (Var x) = None" |
114 "rand (Var x) = None" |
119 apply(rule_tac y="x" in lam.exhaust) |
119 apply(rule_tac y="x" in lam.exhaust) |
120 apply(auto)[3] |
120 apply(auto)[3] |
121 apply(simp_all) |
121 apply(simp_all) |
122 done |
122 done |
123 |
123 |
124 termination (eqvt) by lexicographic_order |
124 nominal_termination (eqvt) by lexicographic_order |
125 |
125 |
126 nominal_function |
126 nominal_function |
127 is_eta_nf :: "lam \<Rightarrow> bool" |
127 is_eta_nf :: "lam \<Rightarrow> bool" |
128 where |
128 where |
129 "is_eta_nf (Var x) = True" |
129 "is_eta_nf (Var x) = True" |
140 apply(simp_all add: pure_fresh fresh_star_def)[3] |
140 apply(simp_all add: pure_fresh fresh_star_def)[3] |
141 apply(simp add: eqvt_at_def conj_eqvt) |
141 apply(simp add: eqvt_at_def conj_eqvt) |
142 apply(simp add: eqvt_at_def conj_eqvt) |
142 apply(simp add: eqvt_at_def conj_eqvt) |
143 done |
143 done |
144 |
144 |
145 termination (eqvt) by lexicographic_order |
145 nominal_termination (eqvt) by lexicographic_order |
146 |
146 |
147 nominal_datatype path = Left | Right | In |
147 nominal_datatype path = Left | Right | In |
148 |
148 |
149 section {* Paths to a free variables *} |
149 section {* Paths to a free variables *} |
150 |
150 |
179 apply(perm_simp) |
179 apply(perm_simp) |
180 apply(simp) |
180 apply(simp) |
181 apply(simp add: perm_supp_eq) |
181 apply(simp add: perm_supp_eq) |
182 done |
182 done |
183 |
183 |
184 termination (eqvt) by lexicographic_order |
184 nominal_termination (eqvt) by lexicographic_order |
185 |
185 |
186 lemma var_pos1: |
186 lemma var_pos1: |
187 assumes "atom y \<notin> supp t" |
187 assumes "atom y \<notin> supp t" |
188 shows "var_pos y t = {}" |
188 shows "var_pos y t = {}" |
189 using assms |
189 using assms |
225 apply(perm_simp) |
225 apply(perm_simp) |
226 apply(simp) |
226 apply(simp) |
227 apply(simp add: fresh_star_Pair perm_supp_eq) |
227 apply(simp add: fresh_star_Pair perm_supp_eq) |
228 done |
228 done |
229 |
229 |
230 termination (eqvt) by lexicographic_order |
230 nominal_termination (eqvt) by lexicographic_order |
231 |
231 |
232 |
232 |
233 section {* free name function *} |
233 section {* free name function *} |
234 |
234 |
235 text {* first returns an atom list *} |
235 text {* first returns an atom list *} |
250 apply(simp add: fresh_star_def fresh_Unit) |
250 apply(simp add: fresh_star_def fresh_Unit) |
251 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
251 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
252 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
252 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
253 done |
253 done |
254 |
254 |
255 termination (eqvt) by lexicographic_order |
255 nominal_termination (eqvt) by lexicographic_order |
256 |
256 |
257 text {* a small test lemma *} |
257 text {* a small test lemma *} |
258 lemma shows "supp t = set (frees_lst t)" |
258 lemma shows "supp t = set (frees_lst t)" |
259 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
259 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
260 |
260 |
278 apply(simp add: fresh_star_def fresh_Unit) |
278 apply(simp add: fresh_star_def fresh_Unit) |
279 apply(simp add: Diff_eqvt eqvt_at_def) |
279 apply(simp add: Diff_eqvt eqvt_at_def) |
280 apply(simp add: Diff_eqvt eqvt_at_def) |
280 apply(simp add: Diff_eqvt eqvt_at_def) |
281 done |
281 done |
282 |
282 |
283 termination (eqvt) |
283 nominal_termination (eqvt) |
284 by lexicographic_order |
284 by lexicographic_order |
285 |
285 |
286 lemma "frees_set t = supp t" |
286 lemma "frees_set t = supp t" |
287 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) |
287 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) |
288 |
288 |
301 apply(auto) |
301 apply(auto) |
302 apply (erule_tac c="()" in Abs_lst1_fcb2) |
302 apply (erule_tac c="()" in Abs_lst1_fcb2) |
303 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
303 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
304 done |
304 done |
305 |
305 |
306 termination (eqvt) |
306 nominal_termination (eqvt) |
307 by lexicographic_order |
307 by lexicographic_order |
308 |
308 |
309 thm height.simps |
309 thm height.simps |
310 |
310 |
311 |
311 |
336 apply(perm_simp) |
336 apply(perm_simp) |
337 apply(simp) |
337 apply(simp) |
338 apply(simp add: fresh_star_Pair perm_supp_eq) |
338 apply(simp add: fresh_star_Pair perm_supp_eq) |
339 done |
339 done |
340 |
340 |
341 termination (eqvt) |
341 nominal_termination (eqvt) |
342 by lexicographic_order |
342 by lexicographic_order |
343 |
343 |
344 thm subst.eqvt |
344 thm subst.eqvt |
345 |
345 |
346 lemma forget: |
346 lemma forget: |
528 apply(simp only: eqvt_at_def) |
528 apply(simp only: eqvt_at_def) |
529 apply(perm_simp) |
529 apply(perm_simp) |
530 apply(simp add: fresh_star_Pair perm_supp_eq) |
530 apply(simp add: fresh_star_Pair perm_supp_eq) |
531 done |
531 done |
532 |
532 |
533 termination (eqvt) |
533 nominal_termination (eqvt) |
534 by lexicographic_order |
534 by lexicographic_order |
535 |
535 |
536 |
536 |
537 text {* count the occurences of lambdas in a term *} |
537 text {* count the occurences of lambdas in a term *} |
538 |
538 |
555 apply(simp add: fresh_star_def pure_fresh) |
555 apply(simp add: fresh_star_def pure_fresh) |
556 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
556 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
557 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
557 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
558 done |
558 done |
559 |
559 |
560 termination (eqvt) |
560 nominal_termination (eqvt) |
561 by lexicographic_order |
561 by lexicographic_order |
562 |
562 |
563 |
563 |
564 text {* count the bound-variable occurences in a lambda-term *} |
564 text {* count the bound-variable occurences in a lambda-term *} |
565 |
565 |
589 apply(simp only: eqvt_at_def) |
589 apply(simp only: eqvt_at_def) |
590 apply(perm_simp) |
590 apply(perm_simp) |
591 apply(simp add: fresh_star_Pair perm_supp_eq) |
591 apply(simp add: fresh_star_Pair perm_supp_eq) |
592 done |
592 done |
593 |
593 |
594 termination (eqvt) |
594 nominal_termination (eqvt) |
595 by lexicographic_order |
595 by lexicographic_order |
596 |
596 |
597 section {* De Bruijn Terms *} |
597 section {* De Bruijn Terms *} |
598 |
598 |
599 nominal_datatype db = |
599 nominal_datatype db = |
647 apply(perm_simp) |
647 apply(perm_simp) |
648 apply(simp) |
648 apply(simp) |
649 apply(simp add: fresh_star_Pair perm_supp_eq) |
649 apply(simp add: fresh_star_Pair perm_supp_eq) |
650 done |
650 done |
651 |
651 |
652 termination (eqvt) |
652 nominal_termination (eqvt) |
653 by lexicographic_order |
653 by lexicographic_order |
654 |
654 |
655 lemma transdb_eqvt[eqvt]: |
655 lemma transdb_eqvt[eqvt]: |
656 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
656 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
657 apply (nominal_induct t avoiding: l rule: lam.strong_induct) |
657 apply (nominal_induct t avoiding: l rule: lam.strong_induct) |
720 apply(simp add: fresh_star_Pair perm_supp_eq) |
720 apply(simp add: fresh_star_Pair perm_supp_eq) |
721 done |
721 done |
722 |
722 |
723 |
723 |
724 (* a small test |
724 (* a small test |
725 termination (eqvt) sorry |
725 nominal_termination (eqvt) sorry |
726 |
726 |
727 lemma |
727 lemma |
728 assumes "x \<noteq> y" |
728 assumes "x \<noteq> y" |
729 shows "eval (App (Lam [x].App (Var x) (Var x)) (Var y)) = App (Var y) (Var y)" |
729 shows "eval (App (Lam [x].App (Var x) (Var x)) (Var y)) = App (Var y) (Var y)" |
730 using assms |
730 using assms |
772 apply (erule Abs_lst1_fcb) |
772 apply (erule Abs_lst1_fcb) |
773 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
773 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
774 apply (simp add: eqvt_def permute_fun_app_eq) |
774 apply (simp add: eqvt_def permute_fun_app_eq) |
775 done |
775 done |
776 |
776 |
777 termination (eqvt) |
777 nominal_termination (eqvt) |
778 by lexicographic_order |
778 by lexicographic_order |
779 |
779 |
780 |
780 |
781 (* |
781 (* |
782 abbreviation |
782 abbreviation |