1 theory TypeSchemes |
1 theory TypeSchemes |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 section {*** Type Schemes ***} |
5 section {*** Type Schemes ***} |
|
6 |
|
7 nominal_datatype |
|
8 A = Aa bool | Ab B |
|
9 and |
|
10 B = Ba bool | Bb A |
|
11 |
|
12 lemma |
|
13 "(p \<bullet> (Sum_Type.Projl (f (Inl x)))) = Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> x)))" |
|
14 apply(perm_simp) |
|
15 apply(subst permute_fun_def) |
|
16 sorry |
|
17 |
|
18 |
|
19 nominal_primrec |
|
20 even :: "nat \<Rightarrow> A" |
|
21 and odd :: "nat \<Rightarrow> B" |
|
22 where |
|
23 "even 0 = Aa True" |
|
24 | "even (Suc n) = Ab (odd n)" |
|
25 | "odd 0 = Ba False" |
|
26 | "odd (Suc n) = Bb (even n)" |
|
27 thm even_odd_graph.intros even_odd_sumC_def |
|
28 thm sum.cases Product_Type.split |
|
29 thm even_odd_graph_def |
|
30 term Inr |
|
31 term Sum_Type.Projr |
|
32 term even_odd_sumC |
|
33 thm even_odd_sumC_def |
|
34 unfolding even_odd_sumC_def |
|
35 sorry |
|
36 |
|
37 ML {* the *} |
|
38 |
|
39 thm even.psimps odd.psimps |
|
40 |
|
41 |
6 |
42 |
7 atom_decl name |
43 atom_decl name |
8 |
44 |
9 (* defined as a single nominal datatype *) |
45 (* defined as a single nominal datatype *) |
10 |
46 |
38 shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)" |
74 shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)" |
39 apply(induct Ts T rule: lookup.induct) |
75 apply(induct Ts T rule: lookup.induct) |
40 apply(simp_all) |
76 apply(simp_all) |
41 done |
77 done |
42 |
78 |
|
79 lemma test: |
|
80 assumes a: "f x = Inl y" |
|
81 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))" |
|
82 using a |
|
83 apply(frule_tac p="p" in permute_boolI) |
|
84 apply(simp (no_asm_use) only: eqvts) |
|
85 apply(subst (asm) permute_fun_app_eq) |
|
86 back |
|
87 apply(simp) |
|
88 done |
|
89 |
|
90 lemma |
|
91 "(p \<bullet> (Sum_Type.Projl x)) = Sum_Type.Projl (p \<bullet> x)" |
|
92 apply(case_tac x) |
|
93 apply(simp) |
|
94 apply(simp) |
|
95 |
|
96 |
43 nominal_primrec |
97 nominal_primrec |
44 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
98 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
45 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
99 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
46 where |
100 where |
47 "subst \<theta> (Var X) = lookup \<theta> X" |
101 "subst \<theta> (Var X) = lookup \<theta> X" |
48 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
102 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
49 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
103 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
104 |
50 term subst_substs_sumC |
105 term subst_substs_sumC |
|
106 thm subst_substs_sumC_def |
51 term Inl |
107 term Inl |
52 thm subst_substs_graph.induct |
108 thm subst_substs_graph.induct |
53 thm subst_substs_graph.intros |
109 thm subst_substs_graph.intros |
54 thm Projl.simps |
110 thm Projl.simps |
55 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") |
111 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") |
71 thm subst_substs_graph.intros |
127 thm subst_substs_graph.intros |
72 thm Projl.simps |
128 thm Projl.simps |
73 apply(erule subst_substs_graph.induct) |
129 apply(erule subst_substs_graph.induct) |
74 apply(perm_simp) |
130 apply(perm_simp) |
75 apply(rule subst_substs_graph.intros) |
131 apply(rule subst_substs_graph.intros) |
|
132 thm subst_substs_graph.cases |
|
133 apply(erule subst_substs_graph.cases) |
|
134 apply(simp (no_asm_use) only: eqvts) |
|
135 apply(subst test) |
|
136 back |
|
137 apply(assumption) |
|
138 apply(rotate_tac 1) |
|
139 apply(erule subst_substs_graph.cases) |
|
140 apply(subst test) |
|
141 back |
|
142 apply(assumption) |
|
143 apply(perm_simp) |
|
144 apply(rule subst_substs_graph.intros) |
|
145 apply(assumption) |
|
146 apply(assumption) |
|
147 apply(subst test) |
|
148 back |
|
149 apply(assumption) |
|
150 apply(perm_simp) |
|
151 apply(rule subst_substs_graph.intros) |
|
152 apply(assumption) |
|
153 apply(assumption) |
|
154 apply(simp) |
|
155 --"A" |
|
156 apply(simp (no_asm_use) only: eqvts) |
|
157 apply(subst test) |
|
158 back |
|
159 apply(assumption) |
|
160 apply(rotate_tac 1) |
|
161 apply(erule subst_substs_graph.cases) |
|
162 apply(subst test) |
|
163 back |
|
164 apply(assumption) |
|
165 apply(perm_simp) |
|
166 apply(rule subst_substs_graph.intros) |
|
167 apply(assumption) |
|
168 apply(assumption) |
|
169 apply(subst test) |
|
170 back |
|
171 apply(assumption) |
|
172 apply(perm_simp) |
|
173 apply(rule subst_substs_graph.intros) |
|
174 apply(assumption) |
|
175 apply(assumption) |
|
176 apply(simp) |
|
177 --"A" |
|
178 apply(simp) |
|
179 apply(erule subst_substs_graph.cases) |
|
180 apply(simp (no_asm_use) only: eqvts) |
|
181 apply(subst test) |
|
182 back |
|
183 back |
|
184 apply(assumption) |
|
185 apply(rule subst_substs_graph.intros) |
|
186 defer |
|
187 apply(perm_simp) |
|
188 apply(assumption) |
|
189 apply(simp (no_asm_use) only: eqvts) |
|
190 apply(subst test) |
|
191 back |
|
192 back |
|
193 apply(assumption) |
|
194 apply(rule subst_substs_graph.intros) |
|
195 defer |
|
196 apply(perm_simp) |
|
197 apply(assumption) |
|
198 apply(simp) |
|
199 apply(simp_all add: ty_tys.distinct) |
|
200 defer |
|
201 apply(simp add: ty_tys.eq_iff) |
|
202 apply(simp add: ty_tys.eq_iff) |
|
203 apply(erule conjE)+ |
|
204 apply(simp add: ty_tys.eq_iff) |
|
205 apply(subst (asm) Abs_eq_iff2) |
|
206 apply(erule exE) |
|
207 apply(simp add: alphas) |
|
208 apply(clarify) |
|
209 thm subst_def |
|
210 |
|
211 |
|
212 apply(assumption) |
|
213 apply(subst test) |
|
214 back |
|
215 apply(assumption) |
|
216 apply(perm_simp) |
|
217 apply(rule subst_substs_graph.intros) |
|
218 apply(assumption) |
|
219 apply(assumption) |
|
220 apply(subst test) |
|
221 back |
|
222 apply(assumption) |
|
223 apply(perm_simp) |
|
224 apply(rule subst_substs_graph.intros) |
|
225 apply(assumption) |
|
226 apply(assumption) |
|
227 apply(simp) |
|
228 |
|
229 |
|
230 apply(rotate_tac 1) |
|
231 apply(erule subst_substs_graph.cases) |
|
232 apply(subst test) |
|
233 back |
|
234 apply(assumption) |
|
235 |
|
236 |
|
237 apply(auto)[4] |
|
238 thm subst_substs_graph.cases |
|
239 thm subst_substs_graph.intros |
|
240 thm subst_substs_graph.intros(2)[THEN permute_boolI] |
|
241 term subst_substs_graph |
76 apply(simp only: eqvts) |
242 apply(simp only: eqvts) |
77 thm Projl.simps |
243 thm Projl.simps |
78 term Inl |
244 term Inl |
79 term Inr |
245 term Inr |
80 apply(perm_simp) |
246 apply(perm_simp) |
81 thm subst_substs_graph.intros |
247 thm subst_substs_graph.intros |
|
248 apply(simp add: permute_fun_def) |
82 thm Projl.simps |
249 thm Projl.simps |
83 oops |
250 oops |
84 |
251 |
85 |
252 |
86 section {* defined as two separate nominal datatypes *} |
253 section {* defined as two separate nominal datatypes *} |