1 theory TySch |
1 theory TySch |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
2 imports "Parser" "../Attic/Prove" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 text {* type schemes *} |
7 ML {* val _ = cheat_fv_rsp := false *} |
8 datatype ty = |
8 ML {* val _ = cheat_const_rsp := false *} |
|
9 ML {* val _ = cheat_equivp := false *} |
|
10 ML {* val _ = cheat_fv_eqvt := false *} |
|
11 ML {* val _ = cheat_alpha_eqvt := false *} |
|
12 ML {* val _ = recursive := false *} |
|
13 |
|
14 nominal_datatype t = |
9 Var "name" |
15 Var "name" |
10 | Fun "ty" "ty" |
16 | Fun "t" "t" |
|
17 and tyS = |
|
18 All xs::"name set" ty::"t" bind xs in ty |
11 |
19 |
12 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.ty") 1 *} |
20 thm t_tyS_fv |
13 print_theorems |
21 thm t_tyS_inject |
|
22 thm t_tyS_bn |
|
23 thm t_tyS_perm |
|
24 thm t_tyS_induct |
|
25 thm t_tyS_distinct |
14 |
26 |
15 datatype tyS = |
27 lemma supports: |
16 All "name set" "ty" |
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 |
17 |
34 |
18 lemma support_image: "supp (atom ` (s :: (('a :: at) set))) = supp s" |
35 lemma fs: |
19 apply (simp add: supp_def) |
36 "finite (supp (x\<Colon>t)) \<and> finite (supp (z\<Colon>tyS))" |
20 apply (simp add: eqvts eqvts_raw) |
37 apply(induct rule: t_tyS_induct) |
21 (* apply (metis COMBC_def Collect_def Collect_mem_eq atom_name_def_raw finite finite_imageI obtain_at_base rangeI)*) |
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) |
22 sorry |
44 sorry |
23 |
45 |
24 lemma atom_image_swap_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at) set); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn" |
46 instance t and tyS :: fs |
25 apply (simp add: fresh_def) |
47 apply default |
26 apply (simp add: support_image) |
48 apply (simp_all add: fs) |
27 apply (fold fresh_def) |
49 sorry |
28 apply (simp add: swap_fresh_fresh) |
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_inject) |
|
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_inject) |
|
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_inject) |
|
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) |
29 done |
87 done |
30 |
88 |
31 lemma "\<lbrakk>a \<sharp> atom ` fun; a \<sharp> t; b \<sharp> atom ` fun; b \<sharp> t\<rbrakk> \<Longrightarrow> All ((a \<rightleftharpoons> b) \<bullet> fun) t = All fun t" |
|
32 apply (simp add: atom_image_swap_fresh) |
|
33 done |
|
34 |
|
35 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *} |
|
36 print_theorems |
|
37 |
|
38 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty") |
|
39 [[[[]], [[], []]]] *} |
|
40 print_theorems |
|
41 |
|
42 (* |
|
43 Doesnot work yet since we do not refer to fv_ty |
|
44 local_setup {* define_raw_fv (Datatype.the_info @{theory} "TySch.tyS") [[[[], []]]] *} |
|
45 print_theorems |
|
46 *) |
|
47 |
|
48 primrec |
|
49 fv_tyS |
|
50 where |
|
51 "fv_tyS (All xs T) = (fv_ty T - atom ` xs)" |
|
52 |
|
53 inductive |
|
54 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100) |
|
55 where |
|
56 a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2)) |
|
57 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2" |
|
58 |
|
59 lemma |
89 lemma |
60 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))" |
90 shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" |
61 apply(rule a1) |
91 apply(simp add: t_tyS_inject) |
|
92 apply(rule_tac x="0::perm" in exI) |
62 apply(simp add: alpha_gen) |
93 apply(simp add: alpha_gen) |
63 apply(rule_tac x="0::perm" in exI) |
94 apply(auto) |
64 apply(simp add: fresh_star_def) |
95 apply(simp add: fresh_star_def fresh_zero_perm) |
65 done |
96 done |
66 |
97 |
67 lemma |
98 lemma |
68 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))" |
99 shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))" |
69 apply(rule a1) |
100 apply(simp add: t_tyS_inject) |
70 apply(simp add: alpha_gen) |
|
71 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
101 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
72 apply(simp add: fresh_star_def) |
102 apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts) |
|
103 apply auto |
73 done |
104 done |
74 |
105 |
75 lemma |
106 lemma |
76 shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))" |
107 shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))" |
77 apply(rule a1) |
108 apply(simp add: t_tyS_inject) |
78 apply(simp add: alpha_gen) |
|
79 apply(rule_tac x="0::perm" in exI) |
109 apply(rule_tac x="0::perm" in exI) |
80 apply(simp add: fresh_star_def) |
110 apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject) |
81 done |
111 oops |
82 |
112 |
83 lemma |
113 lemma |
84 assumes a: "a \<noteq> b" |
114 assumes a: "a \<noteq> b" |
85 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))" |
115 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))" |
86 using a |
116 using a |
|
117 apply(simp add: t_tyS_inject) |
87 apply(clarify) |
118 apply(clarify) |
88 apply(erule alpha_tyS.cases) |
119 apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject) |
89 apply(simp add: alpha_gen) |
120 apply auto |
90 apply(erule conjE)+ |
|
91 apply(erule exE) |
|
92 apply(erule conjE)+ |
|
93 apply(clarify) |
|
94 apply(simp) |
|
95 apply(simp add: fresh_star_def) |
|
96 apply(auto) |
|
97 done |
121 done |
98 |
122 |
99 |
123 |
100 end |
124 end |