removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
authorwenzelm
Sun Oct 01 22:19:23 2006 +0200 (2006-10-01)
changeset 2082058693343905f
parent 20819 cb6ae81dd0be
child 20821 bae9a1002d84
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
src/HOL/Datatype_Universe.thy
src/HOL/Induct/SList.thy
src/HOL/Induct/Sexp.thy
src/HOL/IsaMakefile
src/HOL/Library/Coinductive_List.thy
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Datatype_Universe.thy	Sun Oct 01 22:19:21 2006 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,634 +0,0 @@
     1.4 -(*  Title:      HOL/Datatype_Universe.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1993  University of Cambridge
     1.8 -
     1.9 -Could <*> be generalized to a general summation (Sigma)?
    1.10 -*)
    1.11 -
    1.12 -header{*Analogues of the Cartesian Product and Disjoint Sum for Datatypes*}
    1.13 -
    1.14 -theory Datatype_Universe
    1.15 -imports NatArith Sum_Type
    1.16 -begin
    1.17 -
    1.18 -
    1.19 -typedef (Node)
    1.20 -  ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
    1.21 -    --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
    1.22 -  by auto
    1.23 -
    1.24 -text{*Datatypes will be represented by sets of type @{text node}*}
    1.25 -
    1.26 -types 'a item        = "('a, unit) node set"
    1.27 -      ('a, 'b) dtree = "('a, 'b) node set"
    1.28 -
    1.29 -consts
    1.30 -  apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
    1.31 -  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
    1.32 -
    1.33 -  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
    1.34 -  ndepth    :: "('a, 'b) node => nat"
    1.35 -
    1.36 -  Atom      :: "('a + nat) => ('a, 'b) dtree"
    1.37 -  Leaf      :: "'a => ('a, 'b) dtree"
    1.38 -  Numb      :: "nat => ('a, 'b) dtree"
    1.39 -  Scons     :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
    1.40 -  In0       :: "('a, 'b) dtree => ('a, 'b) dtree"
    1.41 -  In1       :: "('a, 'b) dtree => ('a, 'b) dtree"
    1.42 -  Lim       :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
    1.43 -
    1.44 -  ntrunc    :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
    1.45 -
    1.46 -  uprod     :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    1.47 -  usum      :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    1.48 -
    1.49 -  Split     :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
    1.50 -  Case      :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
    1.51 -
    1.52 -  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
    1.53 -                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    1.54 -  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
    1.55 -                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    1.56 -
    1.57 -
    1.58 -defs
    1.59 -
    1.60 -  Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    1.61 -
    1.62 -  (*crude "lists" of nats -- needed for the constructions*)
    1.63 -  apfst_def:  "apfst == (%f (x,y). (f(x),y))"
    1.64 -  Push_def:   "Push == (%b h. nat_case b h)"
    1.65 -
    1.66 -  (** operations on S-expressions -- sets of nodes **)
    1.67 -
    1.68 -  (*S-expression constructors*)
    1.69 -  Atom_def:   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
    1.70 -  Scons_def:  "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
    1.71 -
    1.72 -  (*Leaf nodes, with arbitrary or nat labels*)
    1.73 -  Leaf_def:   "Leaf == Atom o Inl"
    1.74 -  Numb_def:   "Numb == Atom o Inr"
    1.75 -
    1.76 -  (*Injections of the "disjoint sum"*)
    1.77 -  In0_def:    "In0(M) == Scons (Numb 0) M"
    1.78 -  In1_def:    "In1(M) == Scons (Numb 1) M"
    1.79 -
    1.80 -  (*Function spaces*)
    1.81 -  Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
    1.82 -
    1.83 -  (*the set of nodes with depth less than k*)
    1.84 -  ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
    1.85 -  ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}"
    1.86 -
    1.87 -  (*products and sums for the "universe"*)
    1.88 -  uprod_def:  "uprod A B == UN x:A. UN y:B. { Scons x y }"
    1.89 -  usum_def:   "usum A B == In0`A Un In1`B"
    1.90 -
    1.91 -  (*the corresponding eliminators*)
    1.92 -  Split_def:  "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
    1.93 -
    1.94 -  Case_def:   "Case c d M == THE u.  (EX x . M = In0(x) & u = c(x))
    1.95 -                                  | (EX y . M = In1(y) & u = d(y))"
    1.96 -
    1.97 -
    1.98 -  (** equality for the "universe" **)
    1.99 -
   1.100 -  dprod_def:  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
   1.101 -
   1.102 -  dsum_def:   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
   1.103 -                          (UN (y,y'):s. {(In1(y),In1(y'))})"
   1.104 -
   1.105 -
   1.106 -
   1.107 -(** apfst -- can be used in similar type definitions **)
   1.108 -
   1.109 -lemma apfst_conv [simp]: "apfst f (a,b) = (f(a),b)"
   1.110 -by (simp add: apfst_def)
   1.111 -
   1.112 -
   1.113 -lemma apfst_convE: 
   1.114 -    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R  
   1.115 -     |] ==> R"
   1.116 -by (force simp add: apfst_def)
   1.117 -
   1.118 -(** Push -- an injection, analogous to Cons on lists **)
   1.119 -
   1.120 -lemma Push_inject1: "Push i f = Push j g  ==> i=j"
   1.121 -apply (simp add: Push_def expand_fun_eq) 
   1.122 -apply (drule_tac x=0 in spec, simp) 
   1.123 -done
   1.124 -
   1.125 -lemma Push_inject2: "Push i f = Push j g  ==> f=g"
   1.126 -apply (auto simp add: Push_def expand_fun_eq) 
   1.127 -apply (drule_tac x="Suc x" in spec, simp) 
   1.128 -done
   1.129 -
   1.130 -lemma Push_inject:
   1.131 -    "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P |] ==> P"
   1.132 -by (blast dest: Push_inject1 Push_inject2) 
   1.133 -
   1.134 -lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
   1.135 -by (auto simp add: Push_def expand_fun_eq split: nat.split_asm)
   1.136 -
   1.137 -lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard]
   1.138 -
   1.139 -
   1.140 -(*** Introduction rules for Node ***)
   1.141 -
   1.142 -lemma Node_K0_I: "(%k. Inr 0, a) : Node"
   1.143 -by (simp add: Node_def)
   1.144 -
   1.145 -lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
   1.146 -apply (simp add: Node_def Push_def) 
   1.147 -apply (fast intro!: apfst_conv nat_case_Suc [THEN trans])
   1.148 -done
   1.149 -
   1.150 -
   1.151 -subsection{*Freeness: Distinctness of Constructors*}
   1.152 -
   1.153 -(** Scons vs Atom **)
   1.154 -
   1.155 -lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)"
   1.156 -apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def)
   1.157 -apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
   1.158 -         dest!: Abs_Node_inj 
   1.159 -         elim!: apfst_convE sym [THEN Push_neq_K0])  
   1.160 -done
   1.161 -
   1.162 -lemmas Atom_not_Scons = Scons_not_Atom [THEN not_sym, standard]
   1.163 -declare Atom_not_Scons [iff]
   1.164 -
   1.165 -(*** Injectiveness ***)
   1.166 -
   1.167 -(** Atomic nodes **)
   1.168 -
   1.169 -lemma inj_Atom: "inj(Atom)"
   1.170 -apply (simp add: Atom_def)
   1.171 -apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
   1.172 -done
   1.173 -lemmas Atom_inject = inj_Atom [THEN injD, standard]
   1.174 -
   1.175 -lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
   1.176 -by (blast dest!: Atom_inject)
   1.177 -
   1.178 -lemma inj_Leaf: "inj(Leaf)"
   1.179 -apply (simp add: Leaf_def o_def)
   1.180 -apply (rule inj_onI)
   1.181 -apply (erule Atom_inject [THEN Inl_inject])
   1.182 -done
   1.183 -
   1.184 -lemmas Leaf_inject = inj_Leaf [THEN injD, standard]
   1.185 -declare Leaf_inject [dest!]
   1.186 -
   1.187 -lemma inj_Numb: "inj(Numb)"
   1.188 -apply (simp add: Numb_def o_def)
   1.189 -apply (rule inj_onI)
   1.190 -apply (erule Atom_inject [THEN Inr_inject])
   1.191 -done
   1.192 -
   1.193 -lemmas Numb_inject = inj_Numb [THEN injD, standard]
   1.194 -declare Numb_inject [dest!]
   1.195 -
   1.196 -
   1.197 -(** Injectiveness of Push_Node **)
   1.198 -
   1.199 -lemma Push_Node_inject:
   1.200 -    "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P  
   1.201 -     |] ==> P"
   1.202 -apply (simp add: Push_Node_def)
   1.203 -apply (erule Abs_Node_inj [THEN apfst_convE])
   1.204 -apply (rule Rep_Node [THEN Node_Push_I])+
   1.205 -apply (erule sym [THEN apfst_convE]) 
   1.206 -apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject)
   1.207 -done
   1.208 -
   1.209 -
   1.210 -(** Injectiveness of Scons **)
   1.211 -
   1.212 -lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'"
   1.213 -apply (simp add: Scons_def One_nat_def)
   1.214 -apply (blast dest!: Push_Node_inject)
   1.215 -done
   1.216 -
   1.217 -lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'"
   1.218 -apply (simp add: Scons_def One_nat_def)
   1.219 -apply (blast dest!: Push_Node_inject)
   1.220 -done
   1.221 -
   1.222 -lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
   1.223 -apply (erule equalityE)
   1.224 -apply (iprover intro: equalityI Scons_inject_lemma1)
   1.225 -done
   1.226 -
   1.227 -lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'"
   1.228 -apply (erule equalityE)
   1.229 -apply (iprover intro: equalityI Scons_inject_lemma2)
   1.230 -done
   1.231 -
   1.232 -lemma Scons_inject:
   1.233 -    "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P |] ==> P"
   1.234 -by (iprover dest: Scons_inject1 Scons_inject2)
   1.235 -
   1.236 -lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')"
   1.237 -by (blast elim!: Scons_inject)
   1.238 -
   1.239 -(*** Distinctness involving Leaf and Numb ***)
   1.240 -
   1.241 -(** Scons vs Leaf **)
   1.242 -
   1.243 -lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
   1.244 -by (simp add: Leaf_def o_def Scons_not_Atom)
   1.245 -
   1.246 -lemmas Leaf_not_Scons = Scons_not_Leaf [THEN not_sym, standard]
   1.247 -declare Leaf_not_Scons [iff]
   1.248 -
   1.249 -(** Scons vs Numb **)
   1.250 -
   1.251 -lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
   1.252 -by (simp add: Numb_def o_def Scons_not_Atom)
   1.253 -
   1.254 -lemmas Numb_not_Scons = Scons_not_Numb [THEN not_sym, standard]
   1.255 -declare Numb_not_Scons [iff]
   1.256 -
   1.257 -
   1.258 -(** Leaf vs Numb **)
   1.259 -
   1.260 -lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
   1.261 -by (simp add: Leaf_def Numb_def)
   1.262 -
   1.263 -lemmas Numb_not_Leaf = Leaf_not_Numb [THEN not_sym, standard]
   1.264 -declare Numb_not_Leaf [iff]
   1.265 -
   1.266 -
   1.267 -(*** ndepth -- the depth of a node ***)
   1.268 -
   1.269 -lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0"
   1.270 -by (simp add: ndepth_def  Node_K0_I [THEN Abs_Node_inverse] Least_equality)
   1.271 -
   1.272 -lemma ndepth_Push_Node_aux:
   1.273 -     "nat_case (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k"
   1.274 -apply (induct_tac "k", auto)
   1.275 -apply (erule Least_le)
   1.276 -done
   1.277 -
   1.278 -lemma ndepth_Push_Node: 
   1.279 -    "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))"
   1.280 -apply (insert Rep_Node [of n, unfolded Node_def])
   1.281 -apply (auto simp add: ndepth_def Push_Node_def
   1.282 -                 Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse])
   1.283 -apply (rule Least_equality)
   1.284 -apply (auto simp add: Push_def ndepth_Push_Node_aux)
   1.285 -apply (erule LeastI)
   1.286 -done
   1.287 -
   1.288 -
   1.289 -(*** ntrunc applied to the various node sets ***)
   1.290 -
   1.291 -lemma ntrunc_0 [simp]: "ntrunc 0 M = {}"
   1.292 -by (simp add: ntrunc_def)
   1.293 -
   1.294 -lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)"
   1.295 -by (auto simp add: Atom_def ntrunc_def ndepth_K0)
   1.296 -
   1.297 -lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)"
   1.298 -by (simp add: Leaf_def o_def ntrunc_Atom)
   1.299 -
   1.300 -lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)"
   1.301 -by (simp add: Numb_def o_def ntrunc_Atom)
   1.302 -
   1.303 -lemma ntrunc_Scons [simp]: 
   1.304 -    "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"
   1.305 -by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node) 
   1.306 -
   1.307 -
   1.308 -
   1.309 -(** Injection nodes **)
   1.310 -
   1.311 -lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}"
   1.312 -apply (simp add: In0_def)
   1.313 -apply (simp add: Scons_def)
   1.314 -done
   1.315 -
   1.316 -lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"
   1.317 -by (simp add: In0_def)
   1.318 -
   1.319 -lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}"
   1.320 -apply (simp add: In1_def)
   1.321 -apply (simp add: Scons_def)
   1.322 -done
   1.323 -
   1.324 -lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"
   1.325 -by (simp add: In1_def)
   1.326 -
   1.327 -
   1.328 -subsection{*Set Constructions*}
   1.329 -
   1.330 -
   1.331 -(*** Cartesian Product ***)
   1.332 -
   1.333 -lemma uprodI [intro!]: "[| M:A;  N:B |] ==> Scons M N : uprod A B"
   1.334 -by (simp add: uprod_def)
   1.335 -
   1.336 -(*The general elimination rule*)
   1.337 -lemma uprodE [elim!]:
   1.338 -    "[| c : uprod A B;   
   1.339 -        !!x y. [| x:A;  y:B;  c = Scons x y |] ==> P  
   1.340 -     |] ==> P"
   1.341 -by (auto simp add: uprod_def) 
   1.342 -
   1.343 -
   1.344 -(*Elimination of a pair -- introduces no eigenvariables*)
   1.345 -lemma uprodE2: "[| Scons M N : uprod A B;  [| M:A;  N:B |] ==> P |] ==> P"
   1.346 -by (auto simp add: uprod_def)
   1.347 -
   1.348 -
   1.349 -(*** Disjoint Sum ***)
   1.350 -
   1.351 -lemma usum_In0I [intro]: "M:A ==> In0(M) : usum A B"
   1.352 -by (simp add: usum_def)
   1.353 -
   1.354 -lemma usum_In1I [intro]: "N:B ==> In1(N) : usum A B"
   1.355 -by (simp add: usum_def)
   1.356 -
   1.357 -lemma usumE [elim!]: 
   1.358 -    "[| u : usum A B;   
   1.359 -        !!x. [| x:A;  u=In0(x) |] ==> P;  
   1.360 -        !!y. [| y:B;  u=In1(y) |] ==> P  
   1.361 -     |] ==> P"
   1.362 -by (auto simp add: usum_def)
   1.363 -
   1.364 -
   1.365 -(** Injection **)
   1.366 -
   1.367 -lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
   1.368 -by (auto simp add: In0_def In1_def One_nat_def)
   1.369 -
   1.370 -lemmas In1_not_In0 = In0_not_In1 [THEN not_sym, standard]
   1.371 -declare In1_not_In0 [iff]
   1.372 -
   1.373 -lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
   1.374 -by (simp add: In0_def)
   1.375 -
   1.376 -lemma In1_inject: "In1(M) = In1(N) ==>  M=N"
   1.377 -by (simp add: In1_def)
   1.378 -
   1.379 -lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)"
   1.380 -by (blast dest!: In0_inject)
   1.381 -
   1.382 -lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)"
   1.383 -by (blast dest!: In1_inject)
   1.384 -
   1.385 -lemma inj_In0: "inj In0"
   1.386 -by (blast intro!: inj_onI)
   1.387 -
   1.388 -lemma inj_In1: "inj In1"
   1.389 -by (blast intro!: inj_onI)
   1.390 -
   1.391 -
   1.392 -(*** Function spaces ***)
   1.393 -
   1.394 -lemma Lim_inject: "Lim f = Lim g ==> f = g"
   1.395 -apply (simp add: Lim_def)
   1.396 -apply (rule ext)
   1.397 -apply (blast elim!: Push_Node_inject)
   1.398 -done
   1.399 -
   1.400 -
   1.401 -(*** proving equality of sets and functions using ntrunc ***)
   1.402 -
   1.403 -lemma ntrunc_subsetI: "ntrunc k M <= M"
   1.404 -by (auto simp add: ntrunc_def)
   1.405 -
   1.406 -lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N"
   1.407 -by (auto simp add: ntrunc_def)
   1.408 -
   1.409 -(*A generalized form of the take-lemma*)
   1.410 -lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N"
   1.411 -apply (rule equalityI)
   1.412 -apply (rule_tac [!] ntrunc_subsetD)
   1.413 -apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto) 
   1.414 -done
   1.415 -
   1.416 -lemma ntrunc_o_equality: 
   1.417 -    "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2"
   1.418 -apply (rule ntrunc_equality [THEN ext])
   1.419 -apply (simp add: expand_fun_eq) 
   1.420 -done
   1.421 -
   1.422 -
   1.423 -(*** Monotonicity ***)
   1.424 -
   1.425 -lemma uprod_mono: "[| A<=A';  B<=B' |] ==> uprod A B <= uprod A' B'"
   1.426 -by (simp add: uprod_def, blast)
   1.427 -
   1.428 -lemma usum_mono: "[| A<=A';  B<=B' |] ==> usum A B <= usum A' B'"
   1.429 -by (simp add: usum_def, blast)
   1.430 -
   1.431 -lemma Scons_mono: "[| M<=M';  N<=N' |] ==> Scons M N <= Scons M' N'"
   1.432 -by (simp add: Scons_def, blast)
   1.433 -
   1.434 -lemma In0_mono: "M<=N ==> In0(M) <= In0(N)"
   1.435 -by (simp add: In0_def subset_refl Scons_mono)
   1.436 -
   1.437 -lemma In1_mono: "M<=N ==> In1(M) <= In1(N)"
   1.438 -by (simp add: In1_def subset_refl Scons_mono)
   1.439 -
   1.440 -
   1.441 -(*** Split and Case ***)
   1.442 -
   1.443 -lemma Split [simp]: "Split c (Scons M N) = c M N"
   1.444 -by (simp add: Split_def)
   1.445 -
   1.446 -lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)"
   1.447 -by (simp add: Case_def)
   1.448 -
   1.449 -lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)"
   1.450 -by (simp add: Case_def)
   1.451 -
   1.452 -
   1.453 -
   1.454 -(**** UN x. B(x) rules ****)
   1.455 -
   1.456 -lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))"
   1.457 -by (simp add: ntrunc_def, blast)
   1.458 -
   1.459 -lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)"
   1.460 -by (simp add: Scons_def, blast)
   1.461 -
   1.462 -lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))"
   1.463 -by (simp add: Scons_def, blast)
   1.464 -
   1.465 -lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))"
   1.466 -by (simp add: In0_def Scons_UN1_y)
   1.467 -
   1.468 -lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))"
   1.469 -by (simp add: In1_def Scons_UN1_y)
   1.470 -
   1.471 -
   1.472 -(*** Equality for Cartesian Product ***)
   1.473 -
   1.474 -lemma dprodI [intro!]: 
   1.475 -    "[| (M,M'):r;  (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s"
   1.476 -by (auto simp add: dprod_def)
   1.477 -
   1.478 -(*The general elimination rule*)
   1.479 -lemma dprodE [elim!]: 
   1.480 -    "[| c : dprod r s;   
   1.481 -        !!x y x' y'. [| (x,x') : r;  (y,y') : s;  
   1.482 -                        c = (Scons x y, Scons x' y') |] ==> P  
   1.483 -     |] ==> P"
   1.484 -by (auto simp add: dprod_def)
   1.485 -
   1.486 -
   1.487 -(*** Equality for Disjoint Sum ***)
   1.488 -
   1.489 -lemma dsum_In0I [intro]: "(M,M'):r ==> (In0(M), In0(M')) : dsum r s"
   1.490 -by (auto simp add: dsum_def)
   1.491 -
   1.492 -lemma dsum_In1I [intro]: "(N,N'):s ==> (In1(N), In1(N')) : dsum r s"
   1.493 -by (auto simp add: dsum_def)
   1.494 -
   1.495 -lemma dsumE [elim!]: 
   1.496 -    "[| w : dsum r s;   
   1.497 -        !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P;  
   1.498 -        !!y y'. [| (y,y') : s;  w = (In1(y), In1(y')) |] ==> P  
   1.499 -     |] ==> P"
   1.500 -by (auto simp add: dsum_def)
   1.501 -
   1.502 -
   1.503 -(*** Monotonicity ***)
   1.504 -
   1.505 -lemma dprod_mono: "[| r<=r';  s<=s' |] ==> dprod r s <= dprod r' s'"
   1.506 -by blast
   1.507 -
   1.508 -lemma dsum_mono: "[| r<=r';  s<=s' |] ==> dsum r s <= dsum r' s'"
   1.509 -by blast
   1.510 -
   1.511 -
   1.512 -(*** Bounding theorems ***)
   1.513 -
   1.514 -lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
   1.515 -by blast
   1.516 -
   1.517 -lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard]
   1.518 -
   1.519 -(*Dependent version*)
   1.520 -lemma dprod_subset_Sigma2:
   1.521 -     "(dprod (Sigma A B) (Sigma C D)) <= 
   1.522 -      Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
   1.523 -by auto
   1.524 -
   1.525 -lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
   1.526 -by blast
   1.527 -
   1.528 -lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
   1.529 -
   1.530 -
   1.531 -(*** Domain ***)
   1.532 -
   1.533 -lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
   1.534 -by auto
   1.535 -
   1.536 -lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
   1.537 -by auto
   1.538 -
   1.539 -
   1.540 -subsection {* Finishing the datatype package setup *}
   1.541 -
   1.542 -text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
   1.543 -hide (open) const Push Node Atom Leaf Numb Lim Split Case
   1.544 -hide (open) type node item
   1.545 -
   1.546 -ML
   1.547 -{*
   1.548 -val apfst_conv = thm "apfst_conv";
   1.549 -val apfst_convE = thm "apfst_convE";
   1.550 -val Push_inject1 = thm "Push_inject1";
   1.551 -val Push_inject2 = thm "Push_inject2";
   1.552 -val Push_inject = thm "Push_inject";
   1.553 -val Push_neq_K0 = thm "Push_neq_K0";
   1.554 -val Abs_Node_inj = thm "Abs_Node_inj";
   1.555 -val Node_K0_I = thm "Node_K0_I";
   1.556 -val Node_Push_I = thm "Node_Push_I";
   1.557 -val Scons_not_Atom = thm "Scons_not_Atom";
   1.558 -val Atom_not_Scons = thm "Atom_not_Scons";
   1.559 -val inj_Atom = thm "inj_Atom";
   1.560 -val Atom_inject = thm "Atom_inject";
   1.561 -val Atom_Atom_eq = thm "Atom_Atom_eq";
   1.562 -val inj_Leaf = thm "inj_Leaf";
   1.563 -val Leaf_inject = thm "Leaf_inject";
   1.564 -val inj_Numb = thm "inj_Numb";
   1.565 -val Numb_inject = thm "Numb_inject";
   1.566 -val Push_Node_inject = thm "Push_Node_inject";
   1.567 -val Scons_inject1 = thm "Scons_inject1";
   1.568 -val Scons_inject2 = thm "Scons_inject2";
   1.569 -val Scons_inject = thm "Scons_inject";
   1.570 -val Scons_Scons_eq = thm "Scons_Scons_eq";
   1.571 -val Scons_not_Leaf = thm "Scons_not_Leaf";
   1.572 -val Leaf_not_Scons = thm "Leaf_not_Scons";
   1.573 -val Scons_not_Numb = thm "Scons_not_Numb";
   1.574 -val Numb_not_Scons = thm "Numb_not_Scons";
   1.575 -val Leaf_not_Numb = thm "Leaf_not_Numb";
   1.576 -val Numb_not_Leaf = thm "Numb_not_Leaf";
   1.577 -val ndepth_K0 = thm "ndepth_K0";
   1.578 -val ndepth_Push_Node_aux = thm "ndepth_Push_Node_aux";
   1.579 -val ndepth_Push_Node = thm "ndepth_Push_Node";
   1.580 -val ntrunc_0 = thm "ntrunc_0";
   1.581 -val ntrunc_Atom = thm "ntrunc_Atom";
   1.582 -val ntrunc_Leaf = thm "ntrunc_Leaf";
   1.583 -val ntrunc_Numb = thm "ntrunc_Numb";
   1.584 -val ntrunc_Scons = thm "ntrunc_Scons";
   1.585 -val ntrunc_one_In0 = thm "ntrunc_one_In0";
   1.586 -val ntrunc_In0 = thm "ntrunc_In0";
   1.587 -val ntrunc_one_In1 = thm "ntrunc_one_In1";
   1.588 -val ntrunc_In1 = thm "ntrunc_In1";
   1.589 -val uprodI = thm "uprodI";
   1.590 -val uprodE = thm "uprodE";
   1.591 -val uprodE2 = thm "uprodE2";
   1.592 -val usum_In0I = thm "usum_In0I";
   1.593 -val usum_In1I = thm "usum_In1I";
   1.594 -val usumE = thm "usumE";
   1.595 -val In0_not_In1 = thm "In0_not_In1";
   1.596 -val In1_not_In0 = thm "In1_not_In0";
   1.597 -val In0_inject = thm "In0_inject";
   1.598 -val In1_inject = thm "In1_inject";
   1.599 -val In0_eq = thm "In0_eq";
   1.600 -val In1_eq = thm "In1_eq";
   1.601 -val inj_In0 = thm "inj_In0";
   1.602 -val inj_In1 = thm "inj_In1";
   1.603 -val Lim_inject = thm "Lim_inject";
   1.604 -val ntrunc_subsetI = thm "ntrunc_subsetI";
   1.605 -val ntrunc_subsetD = thm "ntrunc_subsetD";
   1.606 -val ntrunc_equality = thm "ntrunc_equality";
   1.607 -val ntrunc_o_equality = thm "ntrunc_o_equality";
   1.608 -val uprod_mono = thm "uprod_mono";
   1.609 -val usum_mono = thm "usum_mono";
   1.610 -val Scons_mono = thm "Scons_mono";
   1.611 -val In0_mono = thm "In0_mono";
   1.612 -val In1_mono = thm "In1_mono";
   1.613 -val Split = thm "Split";
   1.614 -val Case_In0 = thm "Case_In0";
   1.615 -val Case_In1 = thm "Case_In1";
   1.616 -val ntrunc_UN1 = thm "ntrunc_UN1";
   1.617 -val Scons_UN1_x = thm "Scons_UN1_x";
   1.618 -val Scons_UN1_y = thm "Scons_UN1_y";
   1.619 -val In0_UN1 = thm "In0_UN1";
   1.620 -val In1_UN1 = thm "In1_UN1";
   1.621 -val dprodI = thm "dprodI";
   1.622 -val dprodE = thm "dprodE";
   1.623 -val dsum_In0I = thm "dsum_In0I";
   1.624 -val dsum_In1I = thm "dsum_In1I";
   1.625 -val dsumE = thm "dsumE";
   1.626 -val dprod_mono = thm "dprod_mono";
   1.627 -val dsum_mono = thm "dsum_mono";
   1.628 -val dprod_Sigma = thm "dprod_Sigma";
   1.629 -val dprod_subset_Sigma = thm "dprod_subset_Sigma";
   1.630 -val dprod_subset_Sigma2 = thm "dprod_subset_Sigma2";
   1.631 -val dsum_Sigma = thm "dsum_Sigma";
   1.632 -val dsum_subset_Sigma = thm "dsum_subset_Sigma";
   1.633 -val Domain_dprod = thm "Domain_dprod";
   1.634 -val Domain_dsum = thm "Domain_dsum";
   1.635 -*}
   1.636 -
   1.637 -end
     2.1 --- a/src/HOL/Induct/SList.thy	Sun Oct 01 22:19:21 2006 +0200
     2.2 +++ b/src/HOL/Induct/SList.thy	Sun Oct 01 22:19:23 2006 +0200
     2.3 @@ -56,8 +56,8 @@
     2.4    by (blast intro: list.NIL_I)
     2.5  
     2.6  abbreviation
     2.7 -  "Case == Datatype_Universe.Case"
     2.8 -  "Split == Datatype_Universe.Split"
     2.9 +  "Case == Datatype.Case"
    2.10 +  "Split == Datatype.Split"
    2.11  
    2.12  definition
    2.13    List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
     3.1 --- a/src/HOL/Induct/Sexp.thy	Sun Oct 01 22:19:21 2006 +0200
     3.2 +++ b/src/HOL/Induct/Sexp.thy	Sun Oct 01 22:19:23 2006 +0200
     3.3 @@ -10,10 +10,10 @@
     3.4  theory Sexp imports Main begin
     3.5  
     3.6  types
     3.7 -  'a item = "'a Datatype_Universe.item"
     3.8 +  'a item = "'a Datatype.item"
     3.9  abbreviation
    3.10 -  "Leaf == Datatype_Universe.Leaf"
    3.11 -  "Numb == Datatype_Universe.Numb"
    3.12 +  "Leaf == Datatype.Leaf"
    3.13 +  "Numb == Datatype.Numb"
    3.14  
    3.15  consts
    3.16    sexp      :: "'a item set"
     4.1 --- a/src/HOL/IsaMakefile	Sun Oct 01 22:19:21 2006 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Sun Oct 01 22:19:23 2006 +0200
     4.3 @@ -85,7 +85,7 @@
     4.4    $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
     4.5    Tools/res_atpset.ML \
     4.6    Binomial.thy Datatype.ML Datatype.thy			\
     4.7 -  Datatype_Universe.thy Divides.thy						\
     4.8 +  Divides.thy						\
     4.9    Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
    4.10    FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy	\
    4.11    Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy				\
     5.1 --- a/src/HOL/Library/Coinductive_List.thy	Sun Oct 01 22:19:21 2006 +0200
     5.2 +++ b/src/HOL/Library/Coinductive_List.thy	Sun Oct 01 22:19:23 2006 +0200
     5.3 @@ -12,8 +12,8 @@
     5.4  subsection {* List constructors over the datatype universe *}
     5.5  
     5.6  definition
     5.7 -  "NIL = Datatype_Universe.In0 (Datatype_Universe.Numb 0)"
     5.8 -  "CONS M N = Datatype_Universe.In1 (Datatype_Universe.Scons M N)"
     5.9 +  "NIL = Datatype.In0 (Datatype.Numb 0)"
    5.10 +  "CONS M N = Datatype.In1 (Datatype.Scons M N)"
    5.11  
    5.12  lemma CONS_not_NIL [iff]: "CONS M N \<noteq> NIL"
    5.13    and NIL_not_CONS [iff]: "NIL \<noteq> CONS M N"
    5.14 @@ -28,7 +28,7 @@
    5.15    by (simp add: CONS_def In1_UN1 Scons_UN1_y)
    5.16  
    5.17  definition
    5.18 -  "List_case c h = Datatype_Universe.Case (\<lambda>_. c) (Datatype_Universe.Split h)"
    5.19 +  "List_case c h = Datatype.Case (\<lambda>_. c) (Datatype.Split h)"
    5.20  
    5.21  lemma List_case_NIL [simp]: "List_case c h NIL = c"
    5.22    and List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
    5.23 @@ -38,7 +38,7 @@
    5.24  subsection {* Corecursive lists *}
    5.25  
    5.26  consts
    5.27 -  LList  :: "'a Datatype_Universe.item set \<Rightarrow> 'a Datatype_Universe.item set"
    5.28 +  LList  :: "'a Datatype.item set \<Rightarrow> 'a Datatype.item set"
    5.29  
    5.30  coinductive "LList A"
    5.31    intros
    5.32 @@ -50,8 +50,8 @@
    5.33    unfolding LList.defs by (blast intro!: gfp_mono)
    5.34  
    5.35  consts
    5.36 -  LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype_Universe.item \<times> 'a) option) \<Rightarrow>
    5.37 -    'a \<Rightarrow> 'b Datatype_Universe.item"
    5.38 +  LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
    5.39 +    'a \<Rightarrow> 'b Datatype.item"
    5.40  primrec
    5.41    "LList_corec_aux 0 f x = {}"
    5.42    "LList_corec_aux (Suc k) f x =
    5.43 @@ -117,7 +117,7 @@
    5.44  subsection {* Abstract type definition *}
    5.45  
    5.46  typedef 'a llist =
    5.47 -  "LList (range Datatype_Universe.Leaf) :: 'a Datatype_Universe.item set"
    5.48 +  "LList (range Datatype.Leaf) :: 'a Datatype.item set"
    5.49  proof
    5.50    show "NIL \<in> ?llist" ..
    5.51  qed
    5.52 @@ -125,20 +125,20 @@
    5.53  lemma NIL_type: "NIL \<in> llist"
    5.54    unfolding llist_def by (rule LList.NIL)
    5.55  
    5.56 -lemma CONS_type: "a \<in> range Datatype_Universe.Leaf \<Longrightarrow>
    5.57 +lemma CONS_type: "a \<in> range Datatype.Leaf \<Longrightarrow>
    5.58      M \<in> llist \<Longrightarrow> CONS a M \<in> llist"
    5.59    unfolding llist_def by (rule LList.CONS)
    5.60  
    5.61 -lemma llistI: "x \<in> LList (range Datatype_Universe.Leaf) \<Longrightarrow> x \<in> llist"
    5.62 +lemma llistI: "x \<in> LList (range Datatype.Leaf) \<Longrightarrow> x \<in> llist"
    5.63    by (simp add: llist_def)
    5.64  
    5.65 -lemma llistD: "x \<in> llist \<Longrightarrow> x \<in> LList (range Datatype_Universe.Leaf)"
    5.66 +lemma llistD: "x \<in> llist \<Longrightarrow> x \<in> LList (range Datatype.Leaf)"
    5.67    by (simp add: llist_def)
    5.68  
    5.69  lemma Rep_llist_UNIV: "Rep_llist x \<in> LList UNIV"
    5.70  proof -
    5.71    have "Rep_llist x \<in> llist" by (rule Rep_llist)
    5.72 -  then have "Rep_llist x \<in> LList (range Datatype_Universe.Leaf)"
    5.73 +  then have "Rep_llist x \<in> LList (range Datatype.Leaf)"
    5.74      by (simp add: llist_def)
    5.75    also have "\<dots> \<subseteq> LList UNIV" by (rule LList_mono) simp
    5.76    finally show ?thesis .
    5.77 @@ -146,7 +146,7 @@
    5.78  
    5.79  definition
    5.80    "LNil = Abs_llist NIL"
    5.81 -  "LCons x xs = Abs_llist (CONS (Datatype_Universe.Leaf x) (Rep_llist xs))"
    5.82 +  "LCons x xs = Abs_llist (CONS (Datatype.Leaf x) (Rep_llist xs))"
    5.83  
    5.84  lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
    5.85    apply (simp add: LNil_def LCons_def)
    5.86 @@ -167,7 +167,7 @@
    5.87    by (simp add: LNil_def add: Abs_llist_inverse NIL_type)
    5.88  
    5.89  lemma Rep_llist_LCons: "Rep_llist (LCons x l) =
    5.90 -    CONS (Datatype_Universe.Leaf x) (Rep_llist l)"
    5.91 +    CONS (Datatype.Leaf x) (Rep_llist l)"
    5.92    by (simp add: LCons_def Abs_llist_inverse CONS_type Rep_llist)
    5.93  
    5.94  lemma llist_cases [cases type: llist]:
    5.95 @@ -176,7 +176,7 @@
    5.96    | (LCons) x l' where "l = LCons x l'"
    5.97  proof (cases l)
    5.98    case (Abs_llist L)
    5.99 -  from `L \<in> llist` have "L \<in> LList (range Datatype_Universe.Leaf)" by (rule llistD)
   5.100 +  from `L \<in> llist` have "L \<in> LList (range Datatype.Leaf)" by (rule llistD)
   5.101    then show ?thesis
   5.102    proof cases
   5.103      case NIL
   5.104 @@ -195,7 +195,7 @@
   5.105  
   5.106  definition
   5.107    "llist_case c d l =
   5.108 -    List_case c (\<lambda>x y. d (inv Datatype_Universe.Leaf x) (Abs_llist y)) (Rep_llist l)"
   5.109 +    List_case c (\<lambda>x y. d (inv Datatype.Leaf x) (Abs_llist y)) (Rep_llist l)"
   5.110  
   5.111  syntax  (* FIXME? *)
   5.112    LNil :: logic
   5.113 @@ -217,17 +217,17 @@
   5.114      Abs_llist (LList_corec a
   5.115        (\<lambda>z.
   5.116          case f z of None \<Rightarrow> None
   5.117 -        | Some (v, w) \<Rightarrow> Some (Datatype_Universe.Leaf v, w)))"
   5.118 +        | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)))"
   5.119  
   5.120  lemma LList_corec_type2:
   5.121    "LList_corec a
   5.122      (\<lambda>z. case f z of None \<Rightarrow> None
   5.123 -      | Some (v, w) \<Rightarrow> Some (Datatype_Universe.Leaf v, w)) \<in> llist"
   5.124 +      | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)) \<in> llist"
   5.125    (is "?corec a \<in> _")
   5.126  proof (unfold llist_def)
   5.127    let "LList_corec a ?g" = "?corec a"
   5.128    have "?corec a \<in> {?corec x | x. True}" by blast
   5.129 -  then show "?corec a \<in> LList (range Datatype_Universe.Leaf)"
   5.130 +  then show "?corec a \<in> LList (range Datatype.Leaf)"
   5.131    proof coinduct
   5.132      case (LList L)
   5.133      then obtain x where L: "L = ?corec x" by blast
   5.134 @@ -241,7 +241,7 @@
   5.135      next
   5.136        case (Some p)
   5.137        then have "?corec x =
   5.138 -          CONS (Datatype_Universe.Leaf (fst p)) (?corec (snd p))"
   5.139 +          CONS (Datatype.Leaf (fst p)) (?corec (snd p))"
   5.140          by (simp add: split_def LList_corec)
   5.141        with L have ?CONS by auto
   5.142        then show ?thesis ..
   5.143 @@ -263,12 +263,12 @@
   5.144    let "?rep_corec a" =
   5.145      "LList_corec a
   5.146        (\<lambda>z. case f z of None \<Rightarrow> None
   5.147 -        | Some (v, w) \<Rightarrow> Some (Datatype_Universe.Leaf v, w))"
   5.148 +        | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w))"
   5.149  
   5.150    have "?corec a = Abs_llist (?rep_corec a)"
   5.151      by (simp only: llist_corec_def)
   5.152    also from Some have "?rep_corec a =
   5.153 -      CONS (Datatype_Universe.Leaf (fst p)) (?rep_corec (snd p))"
   5.154 +      CONS (Datatype.Leaf (fst p)) (?rep_corec (snd p))"
   5.155      by (simp add: split_def LList_corec)
   5.156    also have "?rep_corec (snd p) = Rep_llist (?corec (snd p))"
   5.157      by (simp only: llist_corec_def Abs_llist_inverse LList_corec_type2)
   5.158 @@ -281,8 +281,8 @@
   5.159  subsection {* Equality as greatest fixed-point; the bisimulation principle. *}
   5.160  
   5.161  consts
   5.162 -  EqLList :: "('a Datatype_Universe.item \<times> 'a Datatype_Universe.item) set \<Rightarrow>
   5.163 -    ('a Datatype_Universe.item \<times> 'a Datatype_Universe.item) set"
   5.164 +  EqLList :: "('a Datatype.item \<times> 'a Datatype.item) set \<Rightarrow>
   5.165 +    ('a Datatype.item \<times> 'a Datatype.item) set"
   5.166  
   5.167  coinductive "EqLList r"
   5.168    intros
   5.169 @@ -291,7 +291,7 @@
   5.170        (CONS a M, CONS b N) \<in> EqLList r"
   5.171  
   5.172  lemma EqLList_unfold:
   5.173 -    "EqLList r = dsum (diag {Datatype_Universe.Numb 0}) (dprod r (EqLList r))"
   5.174 +    "EqLList r = dsum (diag {Datatype.Numb 0}) (dprod r (EqLList r))"
   5.175    by (fast intro!: EqLList.intros [unfolded NIL_def CONS_def]
   5.176             elim: EqLList.cases [unfolded NIL_def CONS_def])
   5.177  
   5.178 @@ -612,7 +612,7 @@
   5.179    have "(?lhs M, ?rhs M) \<in> {(?lhs N, ?rhs N) | N. N \<in> LList A}"
   5.180      using M by blast
   5.181    then show ?thesis
   5.182 -  proof (coinduct taking: "range (\<lambda>N :: 'a Datatype_Universe.item. N)"
   5.183 +  proof (coinduct taking: "range (\<lambda>N :: 'a Datatype.item. N)"
   5.184        rule: LList_equalityI)
   5.185      case (EqLList q)
   5.186      then obtain N where q: "q = (?lhs N, ?rhs N)" and N: "N \<in> LList A" by blast
   5.187 @@ -635,7 +635,7 @@
   5.188  proof -
   5.189    have "(?lmap M, M) \<in> {(?lmap N, N) | N. N \<in> LList A}" using M by blast
   5.190    then show ?thesis
   5.191 -  proof (coinduct taking: "range (\<lambda>N :: 'a Datatype_Universe.item. N)"
   5.192 +  proof (coinduct taking: "range (\<lambda>N :: 'a Datatype.item. N)"
   5.193        rule: LList_equalityI)
   5.194      case (EqLList q)
   5.195      then obtain N where q: "q = (?lmap N, N)" and N: "N \<in> LList A" by blast
     6.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Oct 01 22:19:21 2006 +0200
     6.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Oct 01 22:19:23 2006 +0200
     6.3 @@ -927,7 +927,7 @@
     6.4  
     6.5  fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
     6.6    let
     6.7 -    val _ = Theory.requires thy "Datatype_Universe" "datatype definitions";
     6.8 +    val _ = Theory.requires thy "Datatype" "datatype definitions";
     6.9  
    6.10      (* this theory is used just for parsing *)
    6.11  
     7.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Oct 01 22:19:21 2006 +0200
     7.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Oct 01 22:19:23 2006 +0200
     7.3 @@ -43,13 +43,13 @@
     7.4        new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
     7.5    let
     7.6      val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
     7.7 -    val node_name = "Datatype_Universe.node";
     7.8 -    val In0_name = "Datatype_Universe.In0";
     7.9 -    val In1_name = "Datatype_Universe.In1";
    7.10 -    val Scons_name = "Datatype_Universe.Scons";
    7.11 -    val Leaf_name = "Datatype_Universe.Leaf";
    7.12 -    val Numb_name = "Datatype_Universe.Numb";
    7.13 -    val Lim_name = "Datatype_Universe.Lim";
    7.14 +    val node_name = "Datatype.node";
    7.15 +    val In0_name = "Datatype.In0";
    7.16 +    val In1_name = "Datatype.In1";
    7.17 +    val Scons_name = "Datatype.Scons";
    7.18 +    val Leaf_name = "Datatype.Leaf";
    7.19 +    val Numb_name = "Datatype.Numb";
    7.20 +    val Lim_name = "Datatype.Lim";
    7.21      val Suml_name = "Datatype.Suml";
    7.22      val Sumr_name = "Datatype.Sumr";
    7.23