4 |
4 |
5 text {* example 1, equivalent to example 2 from Terms *} |
5 text {* example 1, equivalent to example 2 from Terms *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 (* maybe should be added to Infinite.thy *) |
|
10 lemma infinite_Un: |
|
11 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
12 by simp |
|
13 |
|
14 ML {* val _ = cheat_alpha_eqvt := false *} |
|
15 ML {* val _ = cheat_fv_eqvt := false *} |
|
16 ML {* val _ = recursive := false *} |
9 ML {* val _ = recursive := false *} |
17 |
10 |
18 nominal_datatype lm = |
11 nominal_datatype lm = |
19 Vr "name" |
12 Vr "name" |
20 | Ap "lm" "lm" |
13 | Ap "lm" "lm" |
245 thm lam'_bp'.induct |
238 thm lam'_bp'.induct |
246 thm lam'_bp'.inducts |
239 thm lam'_bp'.inducts |
247 thm lam'_bp'.distinct |
240 thm lam'_bp'.distinct |
248 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} |
241 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} |
249 |
242 |
|
243 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
|
244 apply (simp add: supp_Abs supp_Pair) |
|
245 apply blast |
|
246 done |
|
247 |
250 lemma supp_fv': |
248 lemma supp_fv': |
251 shows "supp t = fv_lam' t" |
249 shows "supp t = fv_lam' t" |
252 and "supp bp = fv_bp' bp" |
250 and "supp bp = fv_bp' bp" |
253 apply(induct t and bp rule: lam'_bp'.inducts) |
251 apply(induct t and bp rule: lam'_bp'.inducts) |
254 apply(simp_all) |
252 apply(simp_all) |
478 apply(simp only: de_Morgan_conj) |
476 apply(simp only: de_Morgan_conj) |
479 apply(simp only: Collect_disj_eq) |
477 apply(simp only: Collect_disj_eq) |
480 apply(simp only: infinite_Un) |
478 apply(simp only: infinite_Un) |
481 apply(simp only: Collect_disj_eq) |
479 apply(simp only: Collect_disj_eq) |
482 (* All case *) |
480 (* All case *) |
483 apply(rule_tac t="supp (All fun t)" and s="supp (Abs (atom ` fun) t)" in subst) |
481 apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst) |
484 apply(simp (no_asm) only: supp_def) |
482 apply(simp (no_asm) only: supp_def) |
485 apply(simp only: t_tyS.perm) |
483 apply(simp only: t_tyS.perm) |
486 apply(simp only: permute_ABS) |
484 apply(simp only: permute_ABS) |
487 apply(simp only: t_tyS.eq_iff) |
485 apply(simp only: t_tyS.eq_iff) |
488 apply(simp only: Abs_eq_iff) |
486 apply(simp only: Abs_eq_iff) |
489 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) |
487 apply(simp only: eqvts) |
490 apply(simp only: alpha_gen) |
488 apply(simp only: alpha_gen) |
491 apply(simp only: supp_eqvt[symmetric]) |
489 apply(simp only: supp_eqvt[symmetric]) |
492 apply(simp only: eqvts) |
490 apply(simp only: eqvts eqvts_raw) |
493 apply(rule trans) |
491 apply(rule trans) |
494 apply(rule finite_supp_Abs) |
492 apply(rule finite_supp_Abs) |
495 apply(simp add: finite_fv_t_tyS) |
493 apply(simp add: finite_fv_t_tyS) |
496 apply(simp) |
494 apply(simp) |
497 done |
495 done |
567 thm trm5_lts.eq_iff |
565 thm trm5_lts.eq_iff |
568 thm trm5_lts.bn |
566 thm trm5_lts.bn |
569 thm trm5_lts.perm |
567 thm trm5_lts.perm |
570 thm trm5_lts.induct |
568 thm trm5_lts.induct |
571 thm trm5_lts.distinct |
569 thm trm5_lts.distinct |
|
570 |
|
571 lemma |
|
572 shows "fv_trm5 t = supp t" |
|
573 and "fv_lts l = supp l \<and> fv_bv5 l = {a. infinite {b. \<not>alpha_bv5 ((a \<rightleftharpoons> b) \<bullet> l) l}}" |
|
574 apply(induct t and l rule: trm5_lts.inducts) |
|
575 apply(simp_all only: trm5_lts.fv) |
|
576 apply(simp_all only: supp_Abs[symmetric]) |
|
577 (*apply(simp_all only: supp_abs_sum)*) |
|
578 apply(simp_all (no_asm) only: supp_def) |
|
579 apply(simp_all only: trm5_lts.perm) |
|
580 apply(simp_all only: permute_ABS) |
|
581 apply(simp_all only: trm5_lts.eq_iff Abs_eq_iff) |
|
582 (*apply(simp_all only: alpha_gen2)*) |
|
583 apply(simp_all only: alpha_gen) |
|
584 apply(simp_all only: eqvts[symmetric] supp_Pair) |
|
585 apply(simp_all only: eqvts Pair_eq) |
|
586 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
|
587 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
|
588 apply(simp_all only: de_Morgan_conj[symmetric]) |
|
589 apply simp_all |
|
590 done |
572 |
591 |
573 (* example from my PHD *) |
592 (* example from my PHD *) |
574 |
593 |
575 atom_decl coname |
594 atom_decl coname |
576 |
595 |