author | wenzelm |
Fri, 17 Nov 2006 02:20:03 +0100 | |
changeset 21404 | eb85850d3eb7 |
parent 21243 | afffe1f72143 |
child 21407 | af60523da908 |
permissions | -rw-r--r-- |
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Datatype.thy |
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
20819 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
11954 | 4 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
20819 | 5 |
|
6 |
Could <*> be generalized to a general summation (Sigma)? |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
7 |
*) |
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
8 |
|
20819 | 9 |
header{*Analogues of the Cartesian Product and Disjoint Sum for Datatypes*} |
11954 | 10 |
|
15131 | 11 |
theory Datatype |
21243 | 12 |
imports Nat Sum_Type |
15131 | 13 |
begin |
11954 | 14 |
|
20819 | 15 |
typedef (Node) |
16 |
('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
|
17 |
--{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} |
|
18 |
by auto |
|
19 |
||
20 |
text{*Datatypes will be represented by sets of type @{text node}*} |
|
21 |
||
22 |
types 'a item = "('a, unit) node set" |
|
23 |
('a, 'b) dtree = "('a, 'b) node set" |
|
24 |
||
25 |
consts |
|
26 |
apfst :: "['a=>'c, 'a*'b] => 'c*'b" |
|
27 |
Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))" |
|
28 |
||
29 |
Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node" |
|
30 |
ndepth :: "('a, 'b) node => nat" |
|
31 |
||
32 |
Atom :: "('a + nat) => ('a, 'b) dtree" |
|
33 |
Leaf :: "'a => ('a, 'b) dtree" |
|
34 |
Numb :: "nat => ('a, 'b) dtree" |
|
35 |
Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree" |
|
36 |
In0 :: "('a, 'b) dtree => ('a, 'b) dtree" |
|
37 |
In1 :: "('a, 'b) dtree => ('a, 'b) dtree" |
|
38 |
Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree" |
|
39 |
||
40 |
ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree" |
|
41 |
||
42 |
uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set" |
|
43 |
usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set" |
|
44 |
||
45 |
Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" |
|
46 |
Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" |
|
47 |
||
48 |
dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
|
49 |
=> (('a, 'b) dtree * ('a, 'b) dtree)set" |
|
50 |
dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
|
51 |
=> (('a, 'b) dtree * ('a, 'b) dtree)set" |
|
52 |
||
53 |
||
54 |
defs |
|
55 |
||
56 |
Push_Node_def: "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))" |
|
57 |
||
58 |
(*crude "lists" of nats -- needed for the constructions*) |
|
59 |
apfst_def: "apfst == (%f (x,y). (f(x),y))" |
|
60 |
Push_def: "Push == (%b h. nat_case b h)" |
|
61 |
||
62 |
(** operations on S-expressions -- sets of nodes **) |
|
63 |
||
64 |
(*S-expression constructors*) |
|
65 |
Atom_def: "Atom == (%x. {Abs_Node((%k. Inr 0, x))})" |
|
66 |
Scons_def: "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)" |
|
67 |
||
68 |
(*Leaf nodes, with arbitrary or nat labels*) |
|
69 |
Leaf_def: "Leaf == Atom o Inl" |
|
70 |
Numb_def: "Numb == Atom o Inr" |
|
71 |
||
72 |
(*Injections of the "disjoint sum"*) |
|
73 |
In0_def: "In0(M) == Scons (Numb 0) M" |
|
74 |
In1_def: "In1(M) == Scons (Numb 1) M" |
|
75 |
||
76 |
(*Function spaces*) |
|
77 |
Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}" |
|
78 |
||
79 |
(*the set of nodes with depth less than k*) |
|
80 |
ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" |
|
81 |
ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}" |
|
82 |
||
83 |
(*products and sums for the "universe"*) |
|
84 |
uprod_def: "uprod A B == UN x:A. UN y:B. { Scons x y }" |
|
85 |
usum_def: "usum A B == In0`A Un In1`B" |
|
86 |
||
87 |
(*the corresponding eliminators*) |
|
88 |
Split_def: "Split c M == THE u. EX x y. M = Scons x y & u = c x y" |
|
89 |
||
90 |
Case_def: "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) |
|
91 |
| (EX y . M = In1(y) & u = d(y))" |
|
92 |
||
93 |
||
94 |
(** equality for the "universe" **) |
|
95 |
||
96 |
dprod_def: "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}" |
|
97 |
||
98 |
dsum_def: "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un |
|
99 |
(UN (y,y'):s. {(In1(y),In1(y'))})" |
|
100 |
||
101 |
||
102 |
||
103 |
(** apfst -- can be used in similar type definitions **) |
|
104 |
||
105 |
lemma apfst_conv [simp]: "apfst f (a,b) = (f(a),b)" |
|
106 |
by (simp add: apfst_def) |
|
107 |
||
108 |
||
109 |
lemma apfst_convE: |
|
110 |
"[| q = apfst f p; !!x y. [| p = (x,y); q = (f(x),y) |] ==> R |
|
111 |
|] ==> R" |
|
112 |
by (force simp add: apfst_def) |
|
113 |
||
114 |
(** Push -- an injection, analogous to Cons on lists **) |
|
115 |
||
116 |
lemma Push_inject1: "Push i f = Push j g ==> i=j" |
|
117 |
apply (simp add: Push_def expand_fun_eq) |
|
118 |
apply (drule_tac x=0 in spec, simp) |
|
119 |
done |
|
120 |
||
121 |
lemma Push_inject2: "Push i f = Push j g ==> f=g" |
|
122 |
apply (auto simp add: Push_def expand_fun_eq) |
|
123 |
apply (drule_tac x="Suc x" in spec, simp) |
|
124 |
done |
|
125 |
||
126 |
lemma Push_inject: |
|
127 |
"[| Push i f =Push j g; [| i=j; f=g |] ==> P |] ==> P" |
|
128 |
by (blast dest: Push_inject1 Push_inject2) |
|
129 |
||
130 |
lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P" |
|
131 |
by (auto simp add: Push_def expand_fun_eq split: nat.split_asm) |
|
132 |
||
133 |
lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard] |
|
134 |
||
135 |
||
136 |
(*** Introduction rules for Node ***) |
|
137 |
||
138 |
lemma Node_K0_I: "(%k. Inr 0, a) : Node" |
|
139 |
by (simp add: Node_def) |
|
140 |
||
141 |
lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node" |
|
142 |
apply (simp add: Node_def Push_def) |
|
143 |
apply (fast intro!: apfst_conv nat_case_Suc [THEN trans]) |
|
144 |
done |
|
145 |
||
146 |
||
147 |
subsection{*Freeness: Distinctness of Constructors*} |
|
148 |
||
149 |
(** Scons vs Atom **) |
|
150 |
||
151 |
lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)" |
|
152 |
apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def) |
|
153 |
apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] |
|
154 |
dest!: Abs_Node_inj |
|
155 |
elim!: apfst_convE sym [THEN Push_neq_K0]) |
|
156 |
done |
|
157 |
||
158 |
lemmas Atom_not_Scons = Scons_not_Atom [THEN not_sym, standard] |
|
159 |
declare Atom_not_Scons [iff] |
|
160 |
||
161 |
(*** Injectiveness ***) |
|
162 |
||
163 |
(** Atomic nodes **) |
|
164 |
||
165 |
lemma inj_Atom: "inj(Atom)" |
|
166 |
apply (simp add: Atom_def) |
|
167 |
apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj) |
|
168 |
done |
|
169 |
lemmas Atom_inject = inj_Atom [THEN injD, standard] |
|
170 |
||
171 |
lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)" |
|
172 |
by (blast dest!: Atom_inject) |
|
173 |
||
174 |
lemma inj_Leaf: "inj(Leaf)" |
|
175 |
apply (simp add: Leaf_def o_def) |
|
176 |
apply (rule inj_onI) |
|
177 |
apply (erule Atom_inject [THEN Inl_inject]) |
|
178 |
done |
|
179 |
||
180 |
lemmas Leaf_inject = inj_Leaf [THEN injD, standard] |
|
181 |
declare Leaf_inject [dest!] |
|
182 |
||
183 |
lemma inj_Numb: "inj(Numb)" |
|
184 |
apply (simp add: Numb_def o_def) |
|
185 |
apply (rule inj_onI) |
|
186 |
apply (erule Atom_inject [THEN Inr_inject]) |
|
187 |
done |
|
188 |
||
189 |
lemmas Numb_inject = inj_Numb [THEN injD, standard] |
|
190 |
declare Numb_inject [dest!] |
|
191 |
||
192 |
||
193 |
(** Injectiveness of Push_Node **) |
|
194 |
||
195 |
lemma Push_Node_inject: |
|
196 |
"[| Push_Node i m =Push_Node j n; [| i=j; m=n |] ==> P |
|
197 |
|] ==> P" |
|
198 |
apply (simp add: Push_Node_def) |
|
199 |
apply (erule Abs_Node_inj [THEN apfst_convE]) |
|
200 |
apply (rule Rep_Node [THEN Node_Push_I])+ |
|
201 |
apply (erule sym [THEN apfst_convE]) |
|
202 |
apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject) |
|
203 |
done |
|
204 |
||
205 |
||
206 |
(** Injectiveness of Scons **) |
|
207 |
||
208 |
lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'" |
|
209 |
apply (simp add: Scons_def One_nat_def) |
|
210 |
apply (blast dest!: Push_Node_inject) |
|
211 |
done |
|
212 |
||
213 |
lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'" |
|
214 |
apply (simp add: Scons_def One_nat_def) |
|
215 |
apply (blast dest!: Push_Node_inject) |
|
216 |
done |
|
217 |
||
218 |
lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'" |
|
219 |
apply (erule equalityE) |
|
220 |
apply (iprover intro: equalityI Scons_inject_lemma1) |
|
221 |
done |
|
222 |
||
223 |
lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'" |
|
224 |
apply (erule equalityE) |
|
225 |
apply (iprover intro: equalityI Scons_inject_lemma2) |
|
226 |
done |
|
227 |
||
228 |
lemma Scons_inject: |
|
229 |
"[| Scons M N = Scons M' N'; [| M=M'; N=N' |] ==> P |] ==> P" |
|
230 |
by (iprover dest: Scons_inject1 Scons_inject2) |
|
231 |
||
232 |
lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')" |
|
233 |
by (blast elim!: Scons_inject) |
|
234 |
||
235 |
(*** Distinctness involving Leaf and Numb ***) |
|
236 |
||
237 |
(** Scons vs Leaf **) |
|
238 |
||
239 |
lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)" |
|
240 |
by (simp add: Leaf_def o_def Scons_not_Atom) |
|
241 |
||
242 |
lemmas Leaf_not_Scons = Scons_not_Leaf [THEN not_sym, standard] |
|
243 |
declare Leaf_not_Scons [iff] |
|
244 |
||
245 |
(** Scons vs Numb **) |
|
246 |
||
247 |
lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)" |
|
248 |
by (simp add: Numb_def o_def Scons_not_Atom) |
|
249 |
||
250 |
lemmas Numb_not_Scons = Scons_not_Numb [THEN not_sym, standard] |
|
251 |
declare Numb_not_Scons [iff] |
|
252 |
||
253 |
||
254 |
(** Leaf vs Numb **) |
|
255 |
||
256 |
lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)" |
|
257 |
by (simp add: Leaf_def Numb_def) |
|
258 |
||
259 |
lemmas Numb_not_Leaf = Leaf_not_Numb [THEN not_sym, standard] |
|
260 |
declare Numb_not_Leaf [iff] |
|
261 |
||
262 |
||
263 |
(*** ndepth -- the depth of a node ***) |
|
264 |
||
265 |
lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0" |
|
266 |
by (simp add: ndepth_def Node_K0_I [THEN Abs_Node_inverse] Least_equality) |
|
267 |
||
268 |
lemma ndepth_Push_Node_aux: |
|
269 |
"nat_case (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k" |
|
270 |
apply (induct_tac "k", auto) |
|
271 |
apply (erule Least_le) |
|
272 |
done |
|
273 |
||
274 |
lemma ndepth_Push_Node: |
|
275 |
"ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))" |
|
276 |
apply (insert Rep_Node [of n, unfolded Node_def]) |
|
277 |
apply (auto simp add: ndepth_def Push_Node_def |
|
278 |
Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse]) |
|
279 |
apply (rule Least_equality) |
|
280 |
apply (auto simp add: Push_def ndepth_Push_Node_aux) |
|
281 |
apply (erule LeastI) |
|
282 |
done |
|
283 |
||
284 |
||
285 |
(*** ntrunc applied to the various node sets ***) |
|
286 |
||
287 |
lemma ntrunc_0 [simp]: "ntrunc 0 M = {}" |
|
288 |
by (simp add: ntrunc_def) |
|
289 |
||
290 |
lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)" |
|
291 |
by (auto simp add: Atom_def ntrunc_def ndepth_K0) |
|
292 |
||
293 |
lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)" |
|
294 |
by (simp add: Leaf_def o_def ntrunc_Atom) |
|
295 |
||
296 |
lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)" |
|
297 |
by (simp add: Numb_def o_def ntrunc_Atom) |
|
298 |
||
299 |
lemma ntrunc_Scons [simp]: |
|
300 |
"ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)" |
|
301 |
by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node) |
|
302 |
||
303 |
||
304 |
||
305 |
(** Injection nodes **) |
|
306 |
||
307 |
lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}" |
|
308 |
apply (simp add: In0_def) |
|
309 |
apply (simp add: Scons_def) |
|
310 |
done |
|
311 |
||
312 |
lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)" |
|
313 |
by (simp add: In0_def) |
|
314 |
||
315 |
lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}" |
|
316 |
apply (simp add: In1_def) |
|
317 |
apply (simp add: Scons_def) |
|
318 |
done |
|
319 |
||
320 |
lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)" |
|
321 |
by (simp add: In1_def) |
|
322 |
||
323 |
||
324 |
subsection{*Set Constructions*} |
|
325 |
||
326 |
||
327 |
(*** Cartesian Product ***) |
|
328 |
||
329 |
lemma uprodI [intro!]: "[| M:A; N:B |] ==> Scons M N : uprod A B" |
|
330 |
by (simp add: uprod_def) |
|
331 |
||
332 |
(*The general elimination rule*) |
|
333 |
lemma uprodE [elim!]: |
|
334 |
"[| c : uprod A B; |
|
335 |
!!x y. [| x:A; y:B; c = Scons x y |] ==> P |
|
336 |
|] ==> P" |
|
337 |
by (auto simp add: uprod_def) |
|
338 |
||
339 |
||
340 |
(*Elimination of a pair -- introduces no eigenvariables*) |
|
341 |
lemma uprodE2: "[| Scons M N : uprod A B; [| M:A; N:B |] ==> P |] ==> P" |
|
342 |
by (auto simp add: uprod_def) |
|
343 |
||
344 |
||
345 |
(*** Disjoint Sum ***) |
|
346 |
||
347 |
lemma usum_In0I [intro]: "M:A ==> In0(M) : usum A B" |
|
348 |
by (simp add: usum_def) |
|
349 |
||
350 |
lemma usum_In1I [intro]: "N:B ==> In1(N) : usum A B" |
|
351 |
by (simp add: usum_def) |
|
352 |
||
353 |
lemma usumE [elim!]: |
|
354 |
"[| u : usum A B; |
|
355 |
!!x. [| x:A; u=In0(x) |] ==> P; |
|
356 |
!!y. [| y:B; u=In1(y) |] ==> P |
|
357 |
|] ==> P" |
|
358 |
by (auto simp add: usum_def) |
|
359 |
||
360 |
||
361 |
(** Injection **) |
|
362 |
||
363 |
lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)" |
|
364 |
by (auto simp add: In0_def In1_def One_nat_def) |
|
365 |
||
366 |
lemmas In1_not_In0 = In0_not_In1 [THEN not_sym, standard] |
|
367 |
declare In1_not_In0 [iff] |
|
368 |
||
369 |
lemma In0_inject: "In0(M) = In0(N) ==> M=N" |
|
370 |
by (simp add: In0_def) |
|
371 |
||
372 |
lemma In1_inject: "In1(M) = In1(N) ==> M=N" |
|
373 |
by (simp add: In1_def) |
|
374 |
||
375 |
lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)" |
|
376 |
by (blast dest!: In0_inject) |
|
377 |
||
378 |
lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)" |
|
379 |
by (blast dest!: In1_inject) |
|
380 |
||
381 |
lemma inj_In0: "inj In0" |
|
382 |
by (blast intro!: inj_onI) |
|
383 |
||
384 |
lemma inj_In1: "inj In1" |
|
385 |
by (blast intro!: inj_onI) |
|
386 |
||
387 |
||
388 |
(*** Function spaces ***) |
|
389 |
||
390 |
lemma Lim_inject: "Lim f = Lim g ==> f = g" |
|
391 |
apply (simp add: Lim_def) |
|
392 |
apply (rule ext) |
|
393 |
apply (blast elim!: Push_Node_inject) |
|
394 |
done |
|
395 |
||
396 |
||
397 |
(*** proving equality of sets and functions using ntrunc ***) |
|
398 |
||
399 |
lemma ntrunc_subsetI: "ntrunc k M <= M" |
|
400 |
by (auto simp add: ntrunc_def) |
|
401 |
||
402 |
lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N" |
|
403 |
by (auto simp add: ntrunc_def) |
|
404 |
||
405 |
(*A generalized form of the take-lemma*) |
|
406 |
lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N" |
|
407 |
apply (rule equalityI) |
|
408 |
apply (rule_tac [!] ntrunc_subsetD) |
|
409 |
apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto) |
|
410 |
done |
|
411 |
||
412 |
lemma ntrunc_o_equality: |
|
413 |
"[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2" |
|
414 |
apply (rule ntrunc_equality [THEN ext]) |
|
415 |
apply (simp add: expand_fun_eq) |
|
416 |
done |
|
417 |
||
418 |
||
419 |
(*** Monotonicity ***) |
|
420 |
||
421 |
lemma uprod_mono: "[| A<=A'; B<=B' |] ==> uprod A B <= uprod A' B'" |
|
422 |
by (simp add: uprod_def, blast) |
|
423 |
||
424 |
lemma usum_mono: "[| A<=A'; B<=B' |] ==> usum A B <= usum A' B'" |
|
425 |
by (simp add: usum_def, blast) |
|
426 |
||
427 |
lemma Scons_mono: "[| M<=M'; N<=N' |] ==> Scons M N <= Scons M' N'" |
|
428 |
by (simp add: Scons_def, blast) |
|
429 |
||
430 |
lemma In0_mono: "M<=N ==> In0(M) <= In0(N)" |
|
431 |
by (simp add: In0_def subset_refl Scons_mono) |
|
432 |
||
433 |
lemma In1_mono: "M<=N ==> In1(M) <= In1(N)" |
|
434 |
by (simp add: In1_def subset_refl Scons_mono) |
|
435 |
||
436 |
||
437 |
(*** Split and Case ***) |
|
438 |
||
439 |
lemma Split [simp]: "Split c (Scons M N) = c M N" |
|
440 |
by (simp add: Split_def) |
|
441 |
||
442 |
lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)" |
|
443 |
by (simp add: Case_def) |
|
444 |
||
445 |
lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)" |
|
446 |
by (simp add: Case_def) |
|
447 |
||
448 |
||
449 |
||
450 |
(**** UN x. B(x) rules ****) |
|
451 |
||
452 |
lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))" |
|
453 |
by (simp add: ntrunc_def, blast) |
|
454 |
||
455 |
lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)" |
|
456 |
by (simp add: Scons_def, blast) |
|
457 |
||
458 |
lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))" |
|
459 |
by (simp add: Scons_def, blast) |
|
460 |
||
461 |
lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))" |
|
462 |
by (simp add: In0_def Scons_UN1_y) |
|
463 |
||
464 |
lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))" |
|
465 |
by (simp add: In1_def Scons_UN1_y) |
|
466 |
||
467 |
||
468 |
(*** Equality for Cartesian Product ***) |
|
469 |
||
470 |
lemma dprodI [intro!]: |
|
471 |
"[| (M,M'):r; (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s" |
|
472 |
by (auto simp add: dprod_def) |
|
473 |
||
474 |
(*The general elimination rule*) |
|
475 |
lemma dprodE [elim!]: |
|
476 |
"[| c : dprod r s; |
|
477 |
!!x y x' y'. [| (x,x') : r; (y,y') : s; |
|
478 |
c = (Scons x y, Scons x' y') |] ==> P |
|
479 |
|] ==> P" |
|
480 |
by (auto simp add: dprod_def) |
|
481 |
||
482 |
||
483 |
(*** Equality for Disjoint Sum ***) |
|
484 |
||
485 |
lemma dsum_In0I [intro]: "(M,M'):r ==> (In0(M), In0(M')) : dsum r s" |
|
486 |
by (auto simp add: dsum_def) |
|
487 |
||
488 |
lemma dsum_In1I [intro]: "(N,N'):s ==> (In1(N), In1(N')) : dsum r s" |
|
489 |
by (auto simp add: dsum_def) |
|
490 |
||
491 |
lemma dsumE [elim!]: |
|
492 |
"[| w : dsum r s; |
|
493 |
!!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P; |
|
494 |
!!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P |
|
495 |
|] ==> P" |
|
496 |
by (auto simp add: dsum_def) |
|
497 |
||
498 |
||
499 |
(*** Monotonicity ***) |
|
500 |
||
501 |
lemma dprod_mono: "[| r<=r'; s<=s' |] ==> dprod r s <= dprod r' s'" |
|
502 |
by blast |
|
503 |
||
504 |
lemma dsum_mono: "[| r<=r'; s<=s' |] ==> dsum r s <= dsum r' s'" |
|
505 |
by blast |
|
506 |
||
507 |
||
508 |
(*** Bounding theorems ***) |
|
509 |
||
510 |
lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)" |
|
511 |
by blast |
|
512 |
||
513 |
lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard] |
|
514 |
||
515 |
(*Dependent version*) |
|
516 |
lemma dprod_subset_Sigma2: |
|
517 |
"(dprod (Sigma A B) (Sigma C D)) <= |
|
518 |
Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))" |
|
519 |
by auto |
|
520 |
||
521 |
lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)" |
|
522 |
by blast |
|
523 |
||
524 |
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard] |
|
525 |
||
526 |
||
527 |
(*** Domain ***) |
|
528 |
||
529 |
lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)" |
|
530 |
by auto |
|
531 |
||
532 |
lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)" |
|
533 |
by auto |
|
534 |
||
535 |
||
536 |
subsection {* Finishing the datatype package setup *} |
|
537 |
||
538 |
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} |
|
20847 | 539 |
setup "DatatypeCodegen.setup_hooks" |
20819 | 540 |
hide (open) const Push Node Atom Leaf Numb Lim Split Case |
541 |
hide (open) type node item |
|
542 |
||
543 |
||
544 |
section {* Datatypes *} |
|
545 |
||
11954 | 546 |
subsection {* Representing primitive types *} |
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
547 |
|
5759 | 548 |
rep_datatype bool |
11954 | 549 |
distinct True_not_False False_not_True |
550 |
induction bool_induct |
|
551 |
||
552 |
declare case_split [cases type: bool] |
|
553 |
-- "prefer plain propositional version" |
|
554 |
||
555 |
rep_datatype unit |
|
556 |
induction unit_induct |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
557 |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
558 |
rep_datatype prod |
11954 | 559 |
inject Pair_eq |
560 |
induction prod_induct |
|
561 |
||
12918 | 562 |
rep_datatype sum |
563 |
distinct Inl_not_Inr Inr_not_Inl |
|
564 |
inject Inl_eq Inr_eq |
|
565 |
induction sum_induct |
|
566 |
||
567 |
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" |
|
568 |
apply (rule_tac s = s in sumE) |
|
569 |
apply (erule ssubst) |
|
20798 | 570 |
apply (rule sum.cases(1)) |
12918 | 571 |
apply (erule ssubst) |
20798 | 572 |
apply (rule sum.cases(2)) |
12918 | 573 |
done |
574 |
||
575 |
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t" |
|
576 |
-- {* Prevents simplification of @{text f} and @{text g}: much faster. *} |
|
20798 | 577 |
by simp |
12918 | 578 |
|
579 |
lemma sum_case_inject: |
|
580 |
"sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P" |
|
581 |
proof - |
|
582 |
assume a: "sum_case f1 f2 = sum_case g1 g2" |
|
583 |
assume r: "f1 = g1 ==> f2 = g2 ==> P" |
|
584 |
show P |
|
585 |
apply (rule r) |
|
586 |
apply (rule ext) |
|
14208 | 587 |
apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp) |
12918 | 588 |
apply (rule ext) |
14208 | 589 |
apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp) |
12918 | 590 |
done |
591 |
qed |
|
592 |
||
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
593 |
constdefs |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
594 |
Suml :: "('a => 'c) => 'a + 'b => 'c" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
595 |
"Suml == (%f. sum_case f arbitrary)" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
596 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
597 |
Sumr :: "('b => 'c) => 'a + 'b => 'c" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
598 |
"Sumr == sum_case arbitrary" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
599 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
600 |
lemma Suml_inject: "Suml f = Suml g ==> f = g" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
601 |
by (unfold Suml_def) (erule sum_case_inject) |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
602 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
603 |
lemma Sumr_inject: "Sumr f = Sumr g ==> f = g" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
604 |
by (unfold Sumr_def) (erule sum_case_inject) |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
605 |
|
20798 | 606 |
hide (open) const Suml Sumr |
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
607 |
|
12918 | 608 |
|
609 |
subsection {* Further cases/induct rules for tuples *} |
|
11954 | 610 |
|
20798 | 611 |
lemma prod_cases3 [cases type]: |
612 |
obtains (fields) a b c where "y = (a, b, c)" |
|
613 |
by (cases y, case_tac b) blast |
|
11954 | 614 |
|
615 |
lemma prod_induct3 [case_names fields, induct type]: |
|
616 |
"(!!a b c. P (a, b, c)) ==> P x" |
|
617 |
by (cases x) blast |
|
618 |
||
20798 | 619 |
lemma prod_cases4 [cases type]: |
620 |
obtains (fields) a b c d where "y = (a, b, c, d)" |
|
621 |
by (cases y, case_tac c) blast |
|
11954 | 622 |
|
623 |
lemma prod_induct4 [case_names fields, induct type]: |
|
624 |
"(!!a b c d. P (a, b, c, d)) ==> P x" |
|
625 |
by (cases x) blast |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
626 |
|
20798 | 627 |
lemma prod_cases5 [cases type]: |
628 |
obtains (fields) a b c d e where "y = (a, b, c, d, e)" |
|
629 |
by (cases y, case_tac d) blast |
|
11954 | 630 |
|
631 |
lemma prod_induct5 [case_names fields, induct type]: |
|
632 |
"(!!a b c d e. P (a, b, c, d, e)) ==> P x" |
|
633 |
by (cases x) blast |
|
634 |
||
20798 | 635 |
lemma prod_cases6 [cases type]: |
636 |
obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" |
|
637 |
by (cases y, case_tac e) blast |
|
11954 | 638 |
|
639 |
lemma prod_induct6 [case_names fields, induct type]: |
|
640 |
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" |
|
641 |
by (cases x) blast |
|
642 |
||
20798 | 643 |
lemma prod_cases7 [cases type]: |
644 |
obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" |
|
645 |
by (cases y, case_tac f) blast |
|
11954 | 646 |
|
647 |
lemma prod_induct7 [case_names fields, induct type]: |
|
648 |
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" |
|
649 |
by (cases x) blast |
|
5759 | 650 |
|
12918 | 651 |
|
652 |
subsection {* The option type *} |
|
653 |
||
654 |
datatype 'a option = None | Some 'a |
|
655 |
||
20798 | 656 |
lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" |
18576 | 657 |
by (induct x) auto |
658 |
||
20798 | 659 |
lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" |
18447 | 660 |
by (induct x) auto |
661 |
||
18576 | 662 |
text{*Although it may appear that both of these equalities are helpful |
663 |
only when applied to assumptions, in practice it seems better to give |
|
664 |
them the uniform iff attribute. *} |
|
12918 | 665 |
|
666 |
lemma option_caseE: |
|
20798 | 667 |
assumes c: "(case x of None => P | Some y => Q y)" |
668 |
obtains |
|
669 |
(None) "x = None" and P |
|
670 |
| (Some) y where "x = Some y" and "Q y" |
|
671 |
using c by (cases x) simp_all |
|
12918 | 672 |
|
673 |
||
674 |
subsubsection {* Operations *} |
|
675 |
||
676 |
consts |
|
677 |
the :: "'a option => 'a" |
|
678 |
primrec |
|
679 |
"the (Some x) = x" |
|
680 |
||
681 |
consts |
|
682 |
o2s :: "'a option => 'a set" |
|
683 |
primrec |
|
684 |
"o2s None = {}" |
|
685 |
"o2s (Some x) = {x}" |
|
686 |
||
687 |
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x" |
|
688 |
by simp |
|
689 |
||
17876 | 690 |
ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *} |
12918 | 691 |
|
692 |
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)" |
|
693 |
by (cases xo) auto |
|
694 |
||
695 |
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)" |
|
696 |
by (cases xo) auto |
|
697 |
||
698 |
||
699 |
constdefs |
|
700 |
option_map :: "('a => 'b) => ('a option => 'b option)" |
|
701 |
"option_map == %f y. case y of None => None | Some x => Some (f x)" |
|
702 |
||
703 |
lemma option_map_None [simp]: "option_map f None = None" |
|
704 |
by (simp add: option_map_def) |
|
705 |
||
706 |
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)" |
|
707 |
by (simp add: option_map_def) |
|
708 |
||
20798 | 709 |
lemma option_map_is_None [iff]: |
710 |
"(option_map f opt = None) = (opt = None)" |
|
711 |
by (simp add: option_map_def split add: option.split) |
|
14187 | 712 |
|
12918 | 713 |
lemma option_map_eq_Some [iff]: |
714 |
"(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" |
|
20798 | 715 |
by (simp add: option_map_def split add: option.split) |
14187 | 716 |
|
717 |
lemma option_map_comp: |
|
20798 | 718 |
"option_map f (option_map g opt) = option_map (f o g) opt" |
719 |
by (simp add: option_map_def split add: option.split) |
|
12918 | 720 |
|
721 |
lemma option_map_o_sum_case [simp]: |
|
722 |
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" |
|
20798 | 723 |
by (rule ext) (simp split: sum.split) |
12918 | 724 |
|
19787 | 725 |
|
21111 | 726 |
subsubsection {* Code generator setup *} |
19817 | 727 |
|
21111 | 728 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21243
diff
changeset
|
729 |
is_none :: "'a option \<Rightarrow> bool" where |
21111 | 730 |
is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" |
19787 | 731 |
|
21111 | 732 |
lemma is_none_code [code]: |
733 |
shows "is_none None \<longleftrightarrow> True" |
|
734 |
and "is_none (Some x) \<longleftrightarrow> False" |
|
735 |
unfolding is_none_none [symmetric] by simp_all |
|
736 |
||
737 |
hide (open) const is_none |
|
19787 | 738 |
|
17458
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset
|
739 |
lemmas [code] = imp_conv_disj |
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset
|
740 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
741 |
lemma [code func]: |
19138 | 742 |
"(\<not> True) = False" by (rule HOL.simp_thms) |
743 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
744 |
lemma [code func]: |
19138 | 745 |
"(\<not> False) = True" by (rule HOL.simp_thms) |
746 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
747 |
lemma [code func]: |
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
748 |
shows "(False \<and> x) = False" |
20798 | 749 |
and "(True \<and> x) = x" |
750 |
and "(x \<and> False) = False" |
|
751 |
and "(x \<and> True) = x" by simp_all |
|
19138 | 752 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
753 |
lemma [code func]: |
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
754 |
shows "(False \<or> x) = x" |
20798 | 755 |
and "(True \<or> x) = True" |
756 |
and "(x \<or> False) = x" |
|
757 |
and "(x \<or> True) = True" by simp_all |
|
19138 | 758 |
|
759 |
declare |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
760 |
if_True [code func] |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
761 |
if_False [code func] |
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
762 |
fst_conv [code] |
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
763 |
snd_conv [code] |
19138 | 764 |
|
20105 | 765 |
lemma split_is_prod_case [code inline]: |
20798 | 766 |
"split = prod_case" |
767 |
by (simp add: expand_fun_eq split_def prod.cases) |
|
20105 | 768 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
769 |
code_type bool |
21111 | 770 |
(SML "bool") |
771 |
(Haskell "Bool") |
|
19138 | 772 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
773 |
code_const True and False and Not and "op &" and "op |" and If |
21111 | 774 |
(SML "true" and "false" and "not" |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
775 |
and infixl 1 "andalso" and infixl 0 "orelse" |
21126 | 776 |
and "!(if (_)/ then (_)/ else (_))") |
21111 | 777 |
(Haskell "True" and "False" and "not" |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
778 |
and infixl 3 "&&" and infixl 2 "||" |
21126 | 779 |
and "!(if (_)/ then (_)/ else (_))") |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
780 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
781 |
code_type * |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
782 |
(SML infix 2 "*") |
21126 | 783 |
(Haskell "!((_),/ (_))") |
19138 | 784 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
785 |
code_const Pair |
21126 | 786 |
(SML "!((_),/ (_))") |
787 |
(Haskell "!((_),/ (_))") |
|
18702 | 788 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
789 |
code_type unit |
21111 | 790 |
(SML "unit") |
791 |
(Haskell "()") |
|
19150 | 792 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
793 |
code_const Unity |
21111 | 794 |
(SML "()") |
795 |
(Haskell "()") |
|
19150 | 796 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
797 |
code_type option |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
798 |
(SML "_ option") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
799 |
(Haskell "Maybe _") |
19150 | 800 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
801 |
code_const None and Some |
21111 | 802 |
(SML "NONE" and "SOME") |
803 |
(Haskell "Nothing" and "Just") |
|
19150 | 804 |
|
20588 | 805 |
code_instance option :: eq |
806 |
(Haskell -) |
|
807 |
||
21046
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20847
diff
changeset
|
808 |
code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool" |
20588 | 809 |
(Haskell infixl 4 "==") |
810 |
||
21079 | 811 |
code_reserved SML |
812 |
bool true false not unit option NONE SOME |
|
813 |
||
814 |
code_reserved Haskell |
|
815 |
Bool True False not Maybe Nothing Just |
|
816 |
||
20819 | 817 |
ML |
818 |
{* |
|
819 |
val apfst_conv = thm "apfst_conv"; |
|
820 |
val apfst_convE = thm "apfst_convE"; |
|
821 |
val Push_inject1 = thm "Push_inject1"; |
|
822 |
val Push_inject2 = thm "Push_inject2"; |
|
823 |
val Push_inject = thm "Push_inject"; |
|
824 |
val Push_neq_K0 = thm "Push_neq_K0"; |
|
825 |
val Abs_Node_inj = thm "Abs_Node_inj"; |
|
826 |
val Node_K0_I = thm "Node_K0_I"; |
|
827 |
val Node_Push_I = thm "Node_Push_I"; |
|
828 |
val Scons_not_Atom = thm "Scons_not_Atom"; |
|
829 |
val Atom_not_Scons = thm "Atom_not_Scons"; |
|
830 |
val inj_Atom = thm "inj_Atom"; |
|
831 |
val Atom_inject = thm "Atom_inject"; |
|
832 |
val Atom_Atom_eq = thm "Atom_Atom_eq"; |
|
833 |
val inj_Leaf = thm "inj_Leaf"; |
|
834 |
val Leaf_inject = thm "Leaf_inject"; |
|
835 |
val inj_Numb = thm "inj_Numb"; |
|
836 |
val Numb_inject = thm "Numb_inject"; |
|
837 |
val Push_Node_inject = thm "Push_Node_inject"; |
|
838 |
val Scons_inject1 = thm "Scons_inject1"; |
|
839 |
val Scons_inject2 = thm "Scons_inject2"; |
|
840 |
val Scons_inject = thm "Scons_inject"; |
|
841 |
val Scons_Scons_eq = thm "Scons_Scons_eq"; |
|
842 |
val Scons_not_Leaf = thm "Scons_not_Leaf"; |
|
843 |
val Leaf_not_Scons = thm "Leaf_not_Scons"; |
|
844 |
val Scons_not_Numb = thm "Scons_not_Numb"; |
|
845 |
val Numb_not_Scons = thm "Numb_not_Scons"; |
|
846 |
val Leaf_not_Numb = thm "Leaf_not_Numb"; |
|
847 |
val Numb_not_Leaf = thm "Numb_not_Leaf"; |
|
848 |
val ndepth_K0 = thm "ndepth_K0"; |
|
849 |
val ndepth_Push_Node_aux = thm "ndepth_Push_Node_aux"; |
|
850 |
val ndepth_Push_Node = thm "ndepth_Push_Node"; |
|
851 |
val ntrunc_0 = thm "ntrunc_0"; |
|
852 |
val ntrunc_Atom = thm "ntrunc_Atom"; |
|
853 |
val ntrunc_Leaf = thm "ntrunc_Leaf"; |
|
854 |
val ntrunc_Numb = thm "ntrunc_Numb"; |
|
855 |
val ntrunc_Scons = thm "ntrunc_Scons"; |
|
856 |
val ntrunc_one_In0 = thm "ntrunc_one_In0"; |
|
857 |
val ntrunc_In0 = thm "ntrunc_In0"; |
|
858 |
val ntrunc_one_In1 = thm "ntrunc_one_In1"; |
|
859 |
val ntrunc_In1 = thm "ntrunc_In1"; |
|
860 |
val uprodI = thm "uprodI"; |
|
861 |
val uprodE = thm "uprodE"; |
|
862 |
val uprodE2 = thm "uprodE2"; |
|
863 |
val usum_In0I = thm "usum_In0I"; |
|
864 |
val usum_In1I = thm "usum_In1I"; |
|
865 |
val usumE = thm "usumE"; |
|
866 |
val In0_not_In1 = thm "In0_not_In1"; |
|
867 |
val In1_not_In0 = thm "In1_not_In0"; |
|
868 |
val In0_inject = thm "In0_inject"; |
|
869 |
val In1_inject = thm "In1_inject"; |
|
870 |
val In0_eq = thm "In0_eq"; |
|
871 |
val In1_eq = thm "In1_eq"; |
|
872 |
val inj_In0 = thm "inj_In0"; |
|
873 |
val inj_In1 = thm "inj_In1"; |
|
874 |
val Lim_inject = thm "Lim_inject"; |
|
875 |
val ntrunc_subsetI = thm "ntrunc_subsetI"; |
|
876 |
val ntrunc_subsetD = thm "ntrunc_subsetD"; |
|
877 |
val ntrunc_equality = thm "ntrunc_equality"; |
|
878 |
val ntrunc_o_equality = thm "ntrunc_o_equality"; |
|
879 |
val uprod_mono = thm "uprod_mono"; |
|
880 |
val usum_mono = thm "usum_mono"; |
|
881 |
val Scons_mono = thm "Scons_mono"; |
|
882 |
val In0_mono = thm "In0_mono"; |
|
883 |
val In1_mono = thm "In1_mono"; |
|
884 |
val Split = thm "Split"; |
|
885 |
val Case_In0 = thm "Case_In0"; |
|
886 |
val Case_In1 = thm "Case_In1"; |
|
887 |
val ntrunc_UN1 = thm "ntrunc_UN1"; |
|
888 |
val Scons_UN1_x = thm "Scons_UN1_x"; |
|
889 |
val Scons_UN1_y = thm "Scons_UN1_y"; |
|
890 |
val In0_UN1 = thm "In0_UN1"; |
|
891 |
val In1_UN1 = thm "In1_UN1"; |
|
892 |
val dprodI = thm "dprodI"; |
|
893 |
val dprodE = thm "dprodE"; |
|
894 |
val dsum_In0I = thm "dsum_In0I"; |
|
895 |
val dsum_In1I = thm "dsum_In1I"; |
|
896 |
val dsumE = thm "dsumE"; |
|
897 |
val dprod_mono = thm "dprod_mono"; |
|
898 |
val dsum_mono = thm "dsum_mono"; |
|
899 |
val dprod_Sigma = thm "dprod_Sigma"; |
|
900 |
val dprod_subset_Sigma = thm "dprod_subset_Sigma"; |
|
901 |
val dprod_subset_Sigma2 = thm "dprod_subset_Sigma2"; |
|
902 |
val dsum_Sigma = thm "dsum_Sigma"; |
|
903 |
val dsum_subset_Sigma = thm "dsum_subset_Sigma"; |
|
904 |
val Domain_dprod = thm "Domain_dprod"; |
|
905 |
val Domain_dsum = thm "Domain_dsum"; |
|
906 |
*} |
|
907 |
||
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
908 |
end |