20 thm t_tyS.perm |
20 thm t_tyS.perm |
21 thm t_tyS.inducts |
21 thm t_tyS.inducts |
22 thm t_tyS.distinct |
22 thm t_tyS.distinct |
23 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
23 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
24 |
24 |
25 lemma finite_fv_t_tyS: |
25 lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp] |
26 shows "finite (fv_t t)" "finite (fv_tyS ts)" |
|
27 by (induct rule: t_tyS.inducts) (simp_all) |
|
28 |
|
29 lemma supp_fv_t_tyS: |
|
30 shows "fv_t t = supp t" "fv_tyS ts = supp ts" |
|
31 apply(induct rule: t_tyS.inducts) |
|
32 apply(simp_all only: t_tyS.fv) |
|
33 prefer 3 |
|
34 apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst) |
|
35 prefer 2 |
|
36 apply(subst finite_supp_Abs) |
|
37 apply(drule sym) |
|
38 apply(simp add: finite_fv_t_tyS(1)) |
|
39 apply(simp) |
|
40 apply(simp_all (no_asm) only: supp_def) |
|
41 apply(simp_all only: t_tyS.perm) |
|
42 apply(simp_all only: permute_ABS) |
|
43 apply(simp_all only: t_tyS.eq_iff Abs_eq_iff) |
|
44 apply(simp_all only: alpha_gen) |
|
45 apply(simp_all only: eqvts[symmetric]) |
|
46 apply(simp_all only: eqvts eqvts_raw) |
|
47 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
|
48 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
|
49 apply(simp_all only: de_Morgan_conj[symmetric]) |
|
50 done |
|
51 |
|
52 instance t and tyS :: fs |
|
53 apply default |
|
54 apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS) |
|
55 done |
|
56 |
|
57 lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS] |
|
58 |
26 |
59 lemma induct: |
27 lemma induct: |
60 assumes a1: "\<And>name b. P b (Var name)" |
28 assumes a1: "\<And>name b. P b (Var name)" |
61 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
29 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
62 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
30 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |