1(*  Title:      HOL/Library/Old_Datatype.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
4*)
5
6section \<open>Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums\<close>
7
8theory Old_Datatype
9imports Main
10begin
11
12
13subsection \<open>The datatype universe\<close>
14
15definition "Node = {p. \<exists>f x k. p = (f :: nat => 'b + nat, x ::'a + nat) \<and> f k = Inr 0}"
16
17typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
18  morphisms Rep_Node Abs_Node
19  unfolding Node_def by auto
20
21text\<open>Datatypes will be represented by sets of type \<open>node\<close>\<close>
22
23type_synonym 'a item        = "('a, unit) node set"
24type_synonym ('a, 'b) dtree = "('a, 'b) node set"
25
26definition Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
27  (*crude "lists" of nats -- needed for the constructions*)
28  where "Push == (%b h. case_nat b h)"
29
30definition Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
31  where "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
32
33
34(** operations on S-expressions -- sets of nodes **)
35
36(*S-expression constructors*)
37definition Atom :: "('a + nat) => ('a, 'b) dtree"
38  where "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
39definition Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
40  where "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
41
42(*Leaf nodes, with arbitrary or nat labels*)
43definition Leaf :: "'a => ('a, 'b) dtree"
44  where "Leaf == Atom \<circ> Inl"
45definition Numb :: "nat => ('a, 'b) dtree"
46  where "Numb == Atom \<circ> Inr"
47
48(*Injections of the "disjoint sum"*)
49definition In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
50  where "In0(M) == Scons (Numb 0) M"
51definition In1 :: "('a, 'b) dtree => ('a, 'b) dtree"
52  where "In1(M) == Scons (Numb 1) M"
53
54(*Function spaces*)
55definition Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
56  where "Lim f == \<Union>{z. \<exists>x. z = Push_Node (Inl x) ` (f x)}"
57
58(*the set of nodes with depth less than k*)
59definition ndepth :: "('a, 'b) node => nat"
60  where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
61definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
62  where "ntrunc k N == {n. n\<in>N \<and> ndepth(n)<k}"
63
64(*products and sums for the "universe"*)
65definition uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
66  where "uprod A B == UN x:A. UN y:B. { Scons x y }"
67definition usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
68  where "usum A B == In0`A Un In1`B"
69
70(*the corresponding eliminators*)
71definition Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
72  where "Split c M == THE u. \<exists>x y. M = Scons x y \<and> u = c x y"
73
74definition Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
75  where "Case c d M == THE u. (\<exists>x . M = In0(x) \<and> u = c(x)) \<or> (\<exists>y . M = In1(y) \<and> u = d(y))"
76
77
78(** equality for the "universe" **)
79
80definition dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
81      => (('a, 'b) dtree * ('a, 'b) dtree)set"
82  where "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
83
84definition dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
85      => (('a, 'b) dtree * ('a, 'b) dtree)set"
86  where "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un (UN (y,y'):s. {(In1(y),In1(y'))})"
87
88
89lemma apfst_convE: 
90    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R  
91     |] ==> R"
92by (force simp add: apfst_def)
93
94(** Push -- an injection, analogous to Cons on lists **)
95
96lemma Push_inject1: "Push i f = Push j g  ==> i=j"
97apply (simp add: Push_def fun_eq_iff) 
98apply (drule_tac x=0 in spec, simp) 
99done
100
101lemma Push_inject2: "Push i f = Push j g  ==> f=g"
102apply (auto simp add: Push_def fun_eq_iff) 
103apply (drule_tac x="Suc x" in spec, simp) 
104done
105
106lemma Push_inject:
107    "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P |] ==> P"
108by (blast dest: Push_inject1 Push_inject2) 
109
110lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
111by (auto simp add: Push_def fun_eq_iff split: nat.split_asm)
112
113lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1]
114
115
116(*** Introduction rules for Node ***)
117
118lemma Node_K0_I: "(\<lambda>k. Inr 0, a) \<in> Node"
119by (simp add: Node_def)
120
121lemma Node_Push_I: "p \<in> Node \<Longrightarrow> apfst (Push i) p \<in> Node"
122apply (simp add: Node_def Push_def) 
123apply (fast intro!: apfst_conv nat.case(2)[THEN trans])
124done
125
126
127subsection\<open>Freeness: Distinctness of Constructors\<close>
128
129(** Scons vs Atom **)
130
131lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)"
132unfolding Atom_def Scons_def Push_Node_def One_nat_def
133by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
134         dest!: Abs_Node_inj 
135         elim!: apfst_convE sym [THEN Push_neq_K0])  
136
137lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym]
138
139
140(*** Injectiveness ***)
141
142(** Atomic nodes **)
143
144lemma inj_Atom: "inj(Atom)"
145apply (simp add: Atom_def)
146apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
147done
148lemmas Atom_inject = inj_Atom [THEN injD]
149
150lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
151by (blast dest!: Atom_inject)
152
153lemma inj_Leaf: "inj(Leaf)"
154apply (simp add: Leaf_def o_def)
155apply (rule inj_onI)
156apply (erule Atom_inject [THEN Inl_inject])
157done
158
159lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD]
160
161lemma inj_Numb: "inj(Numb)"
162apply (simp add: Numb_def o_def)
163apply (rule inj_onI)
164apply (erule Atom_inject [THEN Inr_inject])
165done
166
167lemmas Numb_inject [dest!] = inj_Numb [THEN injD]
168
169
170(** Injectiveness of Push_Node **)
171
172lemma Push_Node_inject:
173    "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P  
174     |] ==> P"
175apply (simp add: Push_Node_def)
176apply (erule Abs_Node_inj [THEN apfst_convE])
177apply (rule Rep_Node [THEN Node_Push_I])+
178apply (erule sym [THEN apfst_convE]) 
179apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject)
180done
181
182
183(** Injectiveness of Scons **)
184
185lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'"
186unfolding Scons_def One_nat_def
187by (blast dest!: Push_Node_inject)
188
189lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'"
190unfolding Scons_def One_nat_def
191by (blast dest!: Push_Node_inject)
192
193lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
194apply (erule equalityE)
195apply (iprover intro: equalityI Scons_inject_lemma1)
196done
197
198lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'"
199apply (erule equalityE)
200apply (iprover intro: equalityI Scons_inject_lemma2)
201done
202
203lemma Scons_inject:
204    "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P |] ==> P"
205by (iprover dest: Scons_inject1 Scons_inject2)
206
207lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' \<and> N=N')"
208by (blast elim!: Scons_inject)
209
210(*** Distinctness involving Leaf and Numb ***)
211
212(** Scons vs Leaf **)
213
214lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
215unfolding Leaf_def o_def by (rule Scons_not_Atom)
216
217lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym]
218
219(** Scons vs Numb **)
220
221lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
222unfolding Numb_def o_def by (rule Scons_not_Atom)
223
224lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym]
225
226
227(** Leaf vs Numb **)
228
229lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
230by (simp add: Leaf_def Numb_def)
231
232lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym]
233
234
235(*** ndepth -- the depth of a node ***)
236
237lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0"
238by (simp add: ndepth_def  Node_K0_I [THEN Abs_Node_inverse] Least_equality)
239
240lemma ndepth_Push_Node_aux:
241     "case_nat (Inr (Suc i)) f k = Inr 0 \<longrightarrow> Suc(LEAST x. f x = Inr 0) \<le> k"
242apply (induct_tac "k", auto)
243apply (erule Least_le)
244done
245
246lemma ndepth_Push_Node: 
247    "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))"
248apply (insert Rep_Node [of n, unfolded Node_def])
249apply (auto simp add: ndepth_def Push_Node_def
250                 Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse])
251apply (rule Least_equality)
252apply (auto simp add: Push_def ndepth_Push_Node_aux)
253apply (erule LeastI)
254done
255
256
257(*** ntrunc applied to the various node sets ***)
258
259lemma ntrunc_0 [simp]: "ntrunc 0 M = {}"
260by (simp add: ntrunc_def)
261
262lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)"
263by (auto simp add: Atom_def ntrunc_def ndepth_K0)
264
265lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)"
266unfolding Leaf_def o_def by (rule ntrunc_Atom)
267
268lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)"
269unfolding Numb_def o_def by (rule ntrunc_Atom)
270
271lemma ntrunc_Scons [simp]: 
272    "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"
273unfolding Scons_def ntrunc_def One_nat_def
274by (auto simp add: ndepth_Push_Node)
275
276
277
278(** Injection nodes **)
279
280lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}"
281apply (simp add: In0_def)
282apply (simp add: Scons_def)
283done
284
285lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"
286by (simp add: In0_def)
287
288lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}"
289apply (simp add: In1_def)
290apply (simp add: Scons_def)
291done
292
293lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"
294by (simp add: In1_def)
295
296
297subsection\<open>Set Constructions\<close>
298
299
300(*** Cartesian Product ***)
301
302lemma uprodI [intro!]: "\<lbrakk>M\<in>A; N\<in>B\<rbrakk> \<Longrightarrow> Scons M N \<in> uprod A B"
303by (simp add: uprod_def)
304
305(*The general elimination rule*)
306lemma uprodE [elim!]:
307    "\<lbrakk>c \<in> uprod A B;   
308        \<And>x y. \<lbrakk>x \<in> A; y \<in> B; c = Scons x y\<rbrakk> \<Longrightarrow> P  
309     \<rbrakk> \<Longrightarrow> P"
310by (auto simp add: uprod_def) 
311
312
313(*Elimination of a pair -- introduces no eigenvariables*)
314lemma uprodE2: "\<lbrakk>Scons M N \<in> uprod A B; \<lbrakk>M \<in> A; N \<in> B\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
315by (auto simp add: uprod_def)
316
317
318(*** Disjoint Sum ***)
319
320lemma usum_In0I [intro]: "M \<in> A \<Longrightarrow> In0(M) \<in> usum A B"
321by (simp add: usum_def)
322
323lemma usum_In1I [intro]: "N \<in> B \<Longrightarrow> In1(N) \<in> usum A B"
324by (simp add: usum_def)
325
326lemma usumE [elim!]: 
327    "\<lbrakk>u \<in> usum A B;   
328        \<And>x. \<lbrakk>x \<in> A; u=In0(x)\<rbrakk> \<Longrightarrow> P;  
329        \<And>y. \<lbrakk>y \<in> B; u=In1(y)\<rbrakk> \<Longrightarrow> P  
330     \<rbrakk> \<Longrightarrow> P"
331by (auto simp add: usum_def)
332
333
334(** Injection **)
335
336lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
337unfolding In0_def In1_def One_nat_def by auto
338
339lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym]
340
341lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
342by (simp add: In0_def)
343
344lemma In1_inject: "In1(M) = In1(N) ==>  M=N"
345by (simp add: In1_def)
346
347lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)"
348by (blast dest!: In0_inject)
349
350lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)"
351by (blast dest!: In1_inject)
352
353lemma inj_In0: "inj In0"
354by (blast intro!: inj_onI)
355
356lemma inj_In1: "inj In1"
357by (blast intro!: inj_onI)
358
359
360(*** Function spaces ***)
361
362lemma Lim_inject: "Lim f = Lim g ==> f = g"
363apply (simp add: Lim_def)
364apply (rule ext)
365apply (blast elim!: Push_Node_inject)
366done
367
368
369(*** proving equality of sets and functions using ntrunc ***)
370
371lemma ntrunc_subsetI: "ntrunc k M <= M"
372by (auto simp add: ntrunc_def)
373
374lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N"
375by (auto simp add: ntrunc_def)
376
377(*A generalized form of the take-lemma*)
378lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N"
379apply (rule equalityI)
380apply (rule_tac [!] ntrunc_subsetD)
381apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto) 
382done
383
384lemma ntrunc_o_equality: 
385    "[| !!k. (ntrunc(k) \<circ> h1) = (ntrunc(k) \<circ> h2) |] ==> h1=h2"
386apply (rule ntrunc_equality [THEN ext])
387apply (simp add: fun_eq_iff) 
388done
389
390
391(*** Monotonicity ***)
392
393lemma uprod_mono: "[| A<=A';  B<=B' |] ==> uprod A B <= uprod A' B'"
394by (simp add: uprod_def, blast)
395
396lemma usum_mono: "[| A<=A';  B<=B' |] ==> usum A B <= usum A' B'"
397by (simp add: usum_def, blast)
398
399lemma Scons_mono: "[| M<=M';  N<=N' |] ==> Scons M N <= Scons M' N'"
400by (simp add: Scons_def, blast)
401
402lemma In0_mono: "M<=N ==> In0(M) <= In0(N)"
403by (simp add: In0_def Scons_mono)
404
405lemma In1_mono: "M<=N ==> In1(M) <= In1(N)"
406by (simp add: In1_def Scons_mono)
407
408
409(*** Split and Case ***)
410
411lemma Split [simp]: "Split c (Scons M N) = c M N"
412by (simp add: Split_def)
413
414lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)"
415by (simp add: Case_def)
416
417lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)"
418by (simp add: Case_def)
419
420
421
422(**** UN x. B(x) rules ****)
423
424lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))"
425by (simp add: ntrunc_def, blast)
426
427lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)"
428by (simp add: Scons_def, blast)
429
430lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))"
431by (simp add: Scons_def, blast)
432
433lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))"
434by (simp add: In0_def Scons_UN1_y)
435
436lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))"
437by (simp add: In1_def Scons_UN1_y)
438
439
440(*** Equality for Cartesian Product ***)
441
442lemma dprodI [intro!]: 
443    "\<lbrakk>(M,M') \<in> r; (N,N') \<in> s\<rbrakk> \<Longrightarrow> (Scons M N, Scons M' N') \<in> dprod r s"
444by (auto simp add: dprod_def)
445
446(*The general elimination rule*)
447lemma dprodE [elim!]: 
448    "\<lbrakk>c \<in> dprod r s;   
449        \<And>x y x' y'. \<lbrakk>(x,x') \<in> r; (y,y') \<in> s;  
450                        c = (Scons x y, Scons x' y')\<rbrakk> \<Longrightarrow> P  
451     \<rbrakk> \<Longrightarrow> P"
452by (auto simp add: dprod_def)
453
454
455(*** Equality for Disjoint Sum ***)
456
457lemma dsum_In0I [intro]: "(M,M') \<in> r \<Longrightarrow> (In0(M), In0(M')) \<in> dsum r s"
458by (auto simp add: dsum_def)
459
460lemma dsum_In1I [intro]: "(N,N') \<in> s \<Longrightarrow> (In1(N), In1(N')) \<in> dsum r s"
461by (auto simp add: dsum_def)
462
463lemma dsumE [elim!]: 
464    "\<lbrakk>w \<in> dsum r s;   
465        \<And>x x'. \<lbrakk> (x,x') \<in> r;  w = (In0(x), In0(x')) \<rbrakk> \<Longrightarrow> P;  
466        \<And>y y'. \<lbrakk> (y,y') \<in> s;  w = (In1(y), In1(y')) \<rbrakk> \<Longrightarrow> P  
467     \<rbrakk> \<Longrightarrow> P"
468by (auto simp add: dsum_def)
469
470
471(*** Monotonicity ***)
472
473lemma dprod_mono: "[| r<=r';  s<=s' |] ==> dprod r s <= dprod r' s'"
474by blast
475
476lemma dsum_mono: "[| r<=r';  s<=s' |] ==> dsum r s <= dsum r' s'"
477by blast
478
479
480(*** Bounding theorems ***)
481
482lemma dprod_Sigma: "(dprod (A \<times> B) (C \<times> D)) <= (uprod A C) \<times> (uprod B D)"
483by blast
484
485lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
486
487(*Dependent version*)
488lemma dprod_subset_Sigma2:
489    "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
490by auto
491
492lemma dsum_Sigma: "(dsum (A \<times> B) (C \<times> D)) <= (usum A C) \<times> (usum B D)"
493by blast
494
495lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
496
497
498(*** Domain theorems ***)
499
500lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
501  by auto
502
503lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
504  by auto
505
506
507text \<open>hides popular names\<close>
508hide_type (open) node item
509hide_const (open) Push Node Atom Leaf Numb Lim Split Case
510
511ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
512
513end
514