7 ML {* val _ = cheat_fv_rsp := false *} |
7 ML {* val _ = cheat_fv_rsp := false *} |
8 ML {* val _ = cheat_const_rsp := false *} |
8 ML {* val _ = cheat_const_rsp := false *} |
9 ML {* val _ = cheat_equivp := false *} |
9 ML {* val _ = cheat_equivp := false *} |
10 ML {* val _ = cheat_fv_eqvt := false *} |
10 ML {* val _ = cheat_fv_eqvt := false *} |
11 ML {* val _ = cheat_alpha_eqvt := false *} |
11 ML {* val _ = cheat_alpha_eqvt := false *} |
12 ML {* val _ = recursive := false *} |
|
13 |
12 |
14 nominal_datatype t = |
13 nominal_datatype t = |
15 Var "name" |
14 Var "name" |
16 | Fun "t" "t" |
15 | Fun "t" "t" |
17 and tyS = |
16 and tyS = |
21 thm t_tyS_eq_iff |
20 thm t_tyS_eq_iff |
22 thm t_tyS_bn |
21 thm t_tyS_bn |
23 thm t_tyS_perm |
22 thm t_tyS_perm |
24 thm t_tyS_induct |
23 thm t_tyS_induct |
25 thm t_tyS_distinct |
24 thm t_tyS_distinct |
26 |
|
27 lemma supports: |
|
28 "(supp (atom i)) supports (Var i)" |
|
29 "(supp A \<union> supp M) supports (Fun A M)" |
|
30 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh t_tyS_perm) |
|
31 apply clarify |
|
32 apply(simp_all add: fresh_atom) |
|
33 done |
|
34 |
|
35 lemma fs: |
|
36 "finite (supp (x\<Colon>t)) \<and> finite (supp (z\<Colon>tyS))" |
|
37 apply(induct rule: t_tyS_induct) |
|
38 apply(rule supports_finite) |
|
39 apply(rule supports) |
|
40 apply(simp add: supp_atom) |
|
41 apply(rule supports_finite) |
|
42 apply(rule supports) |
|
43 apply(simp add: supp_atom) |
|
44 sorry |
|
45 |
|
46 instance t and tyS :: fs |
|
47 apply default |
|
48 apply (simp_all add: fs) |
|
49 sorry |
|
50 |
|
51 (* Should be moved to a proper place *) |
|
52 lemma infinite_Un: |
|
53 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
54 by simp |
|
55 |
|
56 lemma supp_fv_t_tyS: |
|
57 shows "supp T = fv_t T" |
|
58 and "supp S = fv_tyS S" |
|
59 apply(induct T and S rule: t_tyS_inducts) |
|
60 apply(simp_all add: t_tyS_fv) |
|
61 (* VarTS case *) |
|
62 apply(simp only: supp_def) |
|
63 apply(simp only: t_tyS_perm) |
|
64 apply(simp only: t_tyS_eq_iff) |
|
65 apply(simp only: supp_def[symmetric]) |
|
66 apply(simp only: supp_at_base) |
|
67 (* FunTS case *) |
|
68 apply(simp only: supp_def) |
|
69 apply(simp only: t_tyS_perm) |
|
70 apply(simp only: t_tyS_eq_iff) |
|
71 apply(simp only: de_Morgan_conj) |
|
72 apply(simp only: Collect_disj_eq) |
|
73 apply(simp only: infinite_Un) |
|
74 apply(simp only: Collect_disj_eq) |
|
75 (* All case *) |
|
76 apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst) |
|
77 apply(simp (no_asm) only: supp_def) |
|
78 apply(simp only: t_tyS_perm) |
|
79 apply(simp only: permute_ABS) |
|
80 apply(simp only: t_tyS_eq_iff) |
|
81 apply(simp only: Abs_eq_iff) |
|
82 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) |
|
83 apply(simp only: alpha_gen) |
|
84 apply(simp only: supp_eqvt[symmetric]) |
|
85 apply(simp only: eqvts) |
|
86 apply(simp only: supp_Abs) |
|
87 done |
|
88 |
25 |
89 lemma |
26 lemma |
90 shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" |
27 shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" |
91 apply(simp add: t_tyS_eq_iff) |
28 apply(simp add: t_tyS_eq_iff) |
92 apply(rule_tac x="0::perm" in exI) |
29 apply(rule_tac x="0::perm" in exI) |