equal
deleted
inserted
replaced
17 val test:((Proof.context -> Method.method) context_parser) = |
17 val test:((Proof.context -> Method.method) context_parser) = |
18 Scan.succeed (fn ctxt => |
18 Scan.succeed (fn ctxt => |
19 let |
19 let |
20 val _ = Inductive.the_inductive ctxt "local.frees_lst_graph" |
20 val _ = Inductive.the_inductive ctxt "local.frees_lst_graph" |
21 in |
21 in |
22 Method.SIMPLE_METHOD' (K all_tac) |
22 Method.SIMPLE_METHOD' (K (all_tac)) |
23 end) |
23 end) |
24 *} |
24 *} |
25 |
25 |
26 method_setup test = {* test *} {* test *} |
26 method_setup test = {* test *} {* test *} |
27 |
27 |
82 termination |
82 termination |
83 by lexicographic_order |
83 by lexicographic_order |
84 |
84 |
85 lemma "frees_set t = supp t" |
85 lemma "frees_set t = supp t" |
86 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) |
86 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) |
87 |
|
88 lemma fresh_fun_eqvt_app3: |
|
89 assumes a: "eqvt f" |
|
90 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
|
91 shows "a \<sharp> f x y z" |
|
92 using fresh_fun_eqvt_app[OF a b(1)] a b |
|
93 by (metis fresh_fun_app) |
|
94 |
|
95 |
87 |
96 section {* height function *} |
88 section {* height function *} |
97 |
89 |
98 nominal_primrec |
90 nominal_primrec |
99 height :: "lam \<Rightarrow> int" |
91 height :: "lam \<Rightarrow> int" |
315 apply(auto)[1] |
307 apply(auto)[1] |
316 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
308 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
317 apply (auto simp add: fresh_star_def)[3] |
309 apply (auto simp add: fresh_star_def)[3] |
318 apply(simp_all) |
310 apply(simp_all) |
319 apply(erule conjE)+ |
311 apply(erule conjE)+ |
320 apply (erule_tac Abs_lst1_fcb2') |
312 thm Abs_lst1_fcb2' |
|
313 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
321 apply (simp add: fresh_star_def) |
314 apply (simp add: fresh_star_def) |
322 apply (simp add: fresh_star_def) |
315 apply (simp add: fresh_star_def) |
323 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
316 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
324 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
317 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
325 done |
318 done |
662 apply(simp add: fresh_star_Pair) |
655 apply(simp add: fresh_star_Pair) |
663 apply(simp add: fresh_star_def fresh_at_base lam.fresh) |
656 apply(simp add: fresh_star_def fresh_at_base lam.fresh) |
664 apply(auto)[1] |
657 apply(auto)[1] |
665 apply(simp_all)[44] |
658 apply(simp_all)[44] |
666 apply(simp del: Product_Type.prod.inject) |
659 apply(simp del: Product_Type.prod.inject) |
667 sorry |
660 oops |
668 |
|
669 termination by lexicographic_order |
|
670 |
661 |
671 lemma abs_same_binder: |
662 lemma abs_same_binder: |
672 fixes t ta s sa :: "_ :: fs" |
663 fixes t ta s sa :: "_ :: fs" |
673 assumes "sort_of (atom x) = sort_of (atom y)" |
664 assumes "sort_of (atom x) = sort_of (atom y)" |
674 shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa |
665 shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa |