3 begin |
3 begin |
4 |
4 |
5 (* Type Schemes *) |
5 (* Type Schemes *) |
6 atom_decl name |
6 atom_decl name |
7 |
7 |
8 (*ML {* val _ = alpha_type := AlphaRes *}*) |
8 ML {* val _ = alpha_type := AlphaRes *} |
9 nominal_datatype t = |
9 nominal_datatype t = |
10 Var "name" |
10 Var "name" |
11 | Fun "t" "t" |
11 | Fun "t" "t" |
12 and tyS = |
12 and tyS = |
13 All xs::"name fset" ty::"t" bind xs in ty |
13 All xs::"name fset" ty::"t" bind xs in ty |
|
14 |
|
15 lemma t_tyS_supp_fv: "fv_t t = supp t \<and> fv_tyS tyS = supp tyS" |
|
16 apply (induct rule: t_tyS.induct) |
|
17 apply (simp_all only: t_tyS.fv) |
|
18 apply (simp_all only: supp_abs(2)[symmetric]) |
|
19 apply(simp_all (no_asm) only: supp_def) |
|
20 apply(simp_all only: t_tyS.perm permute_abs) |
|
21 apply(simp only: t_tyS.eq_iff supp_at_base[simplified supp_def]) |
|
22 apply(simp only: t_tyS.eq_iff Collect_disj_eq[symmetric] infinite_Un[symmetric]) |
|
23 apply simp |
|
24 apply(simp only: Abs_eq_iff t_tyS.eq_iff) |
|
25 apply (simp add: alphas) |
|
26 apply (simp add: eqvts[symmetric]) |
|
27 apply (simp add: eqvts eqvts_raw) |
|
28 done |
|
29 |
|
30 lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS_supp_fv] |
|
31 |
14 |
32 |
15 lemma size_eqvt_raw: |
33 lemma size_eqvt_raw: |
16 "size (pi \<bullet> t :: t_raw) = size t" |
34 "size (pi \<bullet> t :: t_raw) = size t" |
17 "size (pi \<bullet> ts :: tyS_raw) = size ts" |
35 "size (pi \<bullet> ts :: tyS_raw) = size ts" |
18 apply (induct rule: t_raw_tyS_raw.inducts) |
36 apply (induct rule: t_raw_tyS_raw.inducts) |
67 thm t_tyS.perm |
85 thm t_tyS.perm |
68 thm t_tyS.inducts |
86 thm t_tyS.inducts |
69 thm t_tyS.distinct |
87 thm t_tyS.distinct |
70 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
88 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
71 |
89 |
72 lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp] |
|
73 |
|
74 lemma induct: |
90 lemma induct: |
75 assumes a1: "\<And>name b. P b (Var name)" |
91 assumes a1: "\<And>name b. P b (Var name)" |
76 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
92 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
77 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)" |
93 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)" |
78 shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts " |
94 shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts " |
118 lemma |
134 lemma |
119 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
135 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
120 apply(simp add: t_tyS.eq_iff) |
136 apply(simp add: t_tyS.eq_iff) |
121 apply(rule_tac x="0::perm" in exI) |
137 apply(rule_tac x="0::perm" in exI) |
122 apply(simp add: alphas) |
138 apply(simp add: alphas) |
123 apply(auto) |
|
124 apply(simp add: fresh_star_def fresh_zero_perm) |
139 apply(simp add: fresh_star_def fresh_zero_perm) |
125 done |
140 done |
126 |
141 |
127 lemma |
142 lemma |
128 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
143 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
129 apply(simp add: t_tyS.eq_iff) |
144 apply(simp add: t_tyS.eq_iff) |
130 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
145 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
131 apply(simp add: alpha_gen fresh_star_def eqvts) |
146 apply(simp add: alphas fresh_star_def eqvts) |
132 apply auto |
|
133 done |
147 done |
134 |
148 |
135 lemma |
149 lemma |
136 shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))" |
150 shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))" |
137 apply(simp add: t_tyS.eq_iff) |
151 apply(simp add: t_tyS.eq_iff) |
138 apply(rule_tac x="0::perm" in exI) |
152 apply(rule_tac x="0::perm" in exI) |
139 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
153 apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff) |
140 oops |
154 done |
141 |
155 |
142 lemma |
156 lemma |
143 assumes a: "a \<noteq> b" |
157 assumes a: "a \<noteq> b" |
144 shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))" |
158 shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))" |
145 using a |
159 using a |
146 apply(simp add: t_tyS.eq_iff) |
160 apply(simp add: t_tyS.eq_iff) |
147 apply(clarify) |
161 apply(clarify) |
148 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
162 apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff) |
149 apply auto |
163 apply auto |
150 done |
164 done |
151 |
165 |
152 (* PROBLEM: |
166 (* PROBLEM: |
153 Type schemes with separate datatypes |
167 Type schemes with separate datatypes |