moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
authorblanchet
Thu Sep 18 16:47:40 2014 +0200 (2014-09-18)
changeset 58372bfd497f2f4c2
parent 58371 7f30ec82fe40
child 58373 4bdd00a76e54
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
* * *
made example compile again
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Tutorial/ToyList/ToyList.thy
src/Doc/Tutorial/ToyList/ToyList1.txt
src/Doc/Tutorial/ToyList/ToyList_Test.thy
src/HOL/Bali/Basis.thy
src/HOL/Datatype_Examples/Compat.thy
src/HOL/Induct/Sexp.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Old_Datatype.thy
src/HOL/Main.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Old_Datatype.thy
src/HOL/Proofs/Extraction/Higman.thy
src/HOL/Proofs/Extraction/Util.thy
src/HOL/Proofs/Extraction/Warshall.thy
src/HOL/Proofs/Lambda/Commutation.thy
src/HOL/Proofs/Lambda/Lambda.thy
src/HOL/Proofs/Lambda/ListOrder.thy
src/HOL/Proofs/ex/XML_Data.thy
src/HOL/ROOT
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 18 16:47:40 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 18 16:47:40 2014 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  theory HOL_Specific
     1.5 -imports Base Main "~~/src/HOL/Library/Old_Recdef" "~~/src/Tools/Adhoc_Overloading"
     1.6 +imports Base "~~/src/HOL/Library/Old_Datatype" "~~/src/HOL/Library/Old_Recdef"
     1.7 +  "~~/src/Tools/Adhoc_Overloading"
     1.8  begin
     1.9  
    1.10  chapter {* Higher-Order Logic *}
     2.1 --- a/src/Doc/Tutorial/ToyList/ToyList.thy	Thu Sep 18 16:47:40 2014 +0200
     2.2 +++ b/src/Doc/Tutorial/ToyList/ToyList.thy	Thu Sep 18 16:47:40 2014 +0200
     2.3 @@ -1,14 +1,14 @@
     2.4  theory ToyList
     2.5 -imports Old_Datatype
     2.6 +imports BNF_Least_Fixpoint
     2.7  begin
     2.8  
     2.9  text{*\noindent
    2.10  HOL already has a predefined theory of lists called @{text List} ---
    2.11  @{text ToyList} is merely a small fragment of it chosen as an example. In
    2.12  contrast to what is recommended in \S\ref{sec:Basic:Theories},
    2.13 -@{text ToyList} is not based on @{text Main} but on @{text Datatype}, a
    2.14 -theory that contains pretty much everything but lists, thus avoiding
    2.15 -ambiguities caused by defining lists twice.
    2.16 +@{text ToyList} is not based on @{text Main} but on
    2.17 +@{text BNF_Least_Fixpoint}, a theory that contains pretty much everything
    2.18 +but lists, thus avoiding ambiguities caused by defining lists twice.
    2.19  *}
    2.20  
    2.21  datatype 'a list = Nil                          ("[]")
     3.1 --- a/src/Doc/Tutorial/ToyList/ToyList1.txt	Thu Sep 18 16:47:40 2014 +0200
     3.2 +++ b/src/Doc/Tutorial/ToyList/ToyList1.txt	Thu Sep 18 16:47:40 2014 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  theory ToyList
     3.5 -imports Old_Datatype
     3.6 +imports BNF_Least_Fixpoint
     3.7  begin
     3.8  
     3.9  datatype 'a list = Nil                          ("[]")
     4.1 --- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Thu Sep 18 16:47:40 2014 +0200
     4.2 +++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Thu Sep 18 16:47:40 2014 +0200
     4.3 @@ -1,5 +1,5 @@
     4.4  theory ToyList_Test
     4.5 -imports Old_Datatype
     4.6 +imports BNF_Least_Fixpoint
     4.7  begin
     4.8  
     4.9  ML {*
     5.1 --- a/src/HOL/Bali/Basis.thy	Thu Sep 18 16:47:40 2014 +0200
     5.2 +++ b/src/HOL/Bali/Basis.thy	Thu Sep 18 16:47:40 2014 +0200
     5.3 @@ -145,9 +145,7 @@
     5.4  
     5.5  section "sums"
     5.6  
     5.7 -hide_const In0 In1
     5.8 -
     5.9 -notation case_sum  (infixr "'(+')"80)
    5.10 +notation case_sum  (infixr "'(+')" 80)
    5.11  
    5.12  primrec the_Inl :: "'a + 'b \<Rightarrow> 'a"
    5.13    where "the_Inl (Inl a) = a"
     6.1 --- a/src/HOL/Datatype_Examples/Compat.thy	Thu Sep 18 16:47:40 2014 +0200
     6.2 +++ b/src/HOL/Datatype_Examples/Compat.thy	Thu Sep 18 16:47:40 2014 +0200
     6.3 @@ -8,7 +8,7 @@
     6.4  header {* Tests for Compatibility with the Old Datatype Package *}
     6.5  
     6.6  theory Compat
     6.7 -imports Main
     6.8 +imports "~~/src/HOL/Library/Old_Datatype"
     6.9  begin
    6.10  
    6.11  subsection {* Viewing and Registering New-Style Datatypes as Old-Style Ones *}
     7.1 --- a/src/HOL/Induct/Sexp.thy	Thu Sep 18 16:47:40 2014 +0200
     7.2 +++ b/src/HOL/Induct/Sexp.thy	Thu Sep 18 16:47:40 2014 +0200
     7.3 @@ -7,7 +7,7 @@
     7.4  *)
     7.5  
     7.6  theory Sexp
     7.7 -imports Main
     7.8 +imports "~~/src/HOL/Library/Old_Datatype"
     7.9  begin
    7.10  
    7.11  type_synonym 'a item = "'a Old_Datatype.item"
     8.1 --- a/src/HOL/Library/Countable.thy	Thu Sep 18 16:47:40 2014 +0200
     8.2 +++ b/src/HOL/Library/Countable.thy	Thu Sep 18 16:47:40 2014 +0200
     8.3 @@ -7,7 +7,7 @@
     8.4  header {* Encoding (almost) everything into natural numbers *}
     8.5  
     8.6  theory Countable
     8.7 -imports Main Rat Nat_Bijection
     8.8 +imports Old_Datatype Rat Nat_Bijection
     8.9  begin
    8.10  
    8.11  subsection {* The class of countable types *}
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Library/Old_Datatype.thy	Thu Sep 18 16:47:40 2014 +0200
     9.3 @@ -0,0 +1,527 @@
     9.4 +(*  Title:      HOL/Library/Old_Datatype.thy
     9.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.6 +    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     9.7 +*)
     9.8 +
     9.9 +header {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
    9.10 +
    9.11 +theory Old_Datatype
    9.12 +imports "../Main"
    9.13 +keywords "old_datatype" :: thy_decl
    9.14 +begin
    9.15 +
    9.16 +subsection {* The datatype universe *}
    9.17 +
    9.18 +definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
    9.19 +
    9.20 +typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
    9.21 +  morphisms Rep_Node Abs_Node
    9.22 +  unfolding Node_def by auto
    9.23 +
    9.24 +text{*Datatypes will be represented by sets of type @{text node}*}
    9.25 +
    9.26 +type_synonym 'a item        = "('a, unit) node set"
    9.27 +type_synonym ('a, 'b) dtree = "('a, 'b) node set"
    9.28 +
    9.29 +consts
    9.30 +  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
    9.31 +
    9.32 +  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
    9.33 +  ndepth    :: "('a, 'b) node => nat"
    9.34 +
    9.35 +  Atom      :: "('a + nat) => ('a, 'b) dtree"
    9.36 +  Leaf      :: "'a => ('a, 'b) dtree"
    9.37 +  Numb      :: "nat => ('a, 'b) dtree"
    9.38 +  Scons     :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
    9.39 +  In0       :: "('a, 'b) dtree => ('a, 'b) dtree"
    9.40 +  In1       :: "('a, 'b) dtree => ('a, 'b) dtree"
    9.41 +  Lim       :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
    9.42 +
    9.43 +  ntrunc    :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
    9.44 +
    9.45 +  uprod     :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    9.46 +  usum      :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    9.47 +
    9.48 +  Split     :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
    9.49 +  Case      :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
    9.50 +
    9.51 +  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
    9.52 +                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    9.53 +  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
    9.54 +                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    9.55 +
    9.56 +
    9.57 +defs
    9.58 +
    9.59 +  Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    9.60 +
    9.61 +  (*crude "lists" of nats -- needed for the constructions*)
    9.62 +  Push_def:   "Push == (%b h. case_nat b h)"
    9.63 +
    9.64 +  (** operations on S-expressions -- sets of nodes **)
    9.65 +
    9.66 +  (*S-expression constructors*)
    9.67 +  Atom_def:   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
    9.68 +  Scons_def:  "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
    9.69 +
    9.70 +  (*Leaf nodes, with arbitrary or nat labels*)
    9.71 +  Leaf_def:   "Leaf == Atom o Inl"
    9.72 +  Numb_def:   "Numb == Atom o Inr"
    9.73 +
    9.74 +  (*Injections of the "disjoint sum"*)
    9.75 +  In0_def:    "In0(M) == Scons (Numb 0) M"
    9.76 +  In1_def:    "In1(M) == Scons (Numb 1) M"
    9.77 +
    9.78 +  (*Function spaces*)
    9.79 +  Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
    9.80 +
    9.81 +  (*the set of nodes with depth less than k*)
    9.82 +  ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
    9.83 +  ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}"
    9.84 +
    9.85 +  (*products and sums for the "universe"*)
    9.86 +  uprod_def:  "uprod A B == UN x:A. UN y:B. { Scons x y }"
    9.87 +  usum_def:   "usum A B == In0`A Un In1`B"
    9.88 +
    9.89 +  (*the corresponding eliminators*)
    9.90 +  Split_def:  "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
    9.91 +
    9.92 +  Case_def:   "Case c d M == THE u.  (EX x . M = In0(x) & u = c(x))
    9.93 +                                  | (EX y . M = In1(y) & u = d(y))"
    9.94 +
    9.95 +
    9.96 +  (** equality for the "universe" **)
    9.97 +
    9.98 +  dprod_def:  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
    9.99 +
   9.100 +  dsum_def:   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
   9.101 +                          (UN (y,y'):s. {(In1(y),In1(y'))})"
   9.102 +
   9.103 +
   9.104 +
   9.105 +lemma apfst_convE: 
   9.106 +    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R  
   9.107 +     |] ==> R"
   9.108 +by (force simp add: apfst_def)
   9.109 +
   9.110 +(** Push -- an injection, analogous to Cons on lists **)
   9.111 +
   9.112 +lemma Push_inject1: "Push i f = Push j g  ==> i=j"
   9.113 +apply (simp add: Push_def fun_eq_iff) 
   9.114 +apply (drule_tac x=0 in spec, simp) 
   9.115 +done
   9.116 +
   9.117 +lemma Push_inject2: "Push i f = Push j g  ==> f=g"
   9.118 +apply (auto simp add: Push_def fun_eq_iff) 
   9.119 +apply (drule_tac x="Suc x" in spec, simp) 
   9.120 +done
   9.121 +
   9.122 +lemma Push_inject:
   9.123 +    "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P |] ==> P"
   9.124 +by (blast dest: Push_inject1 Push_inject2) 
   9.125 +
   9.126 +lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
   9.127 +by (auto simp add: Push_def fun_eq_iff split: nat.split_asm)
   9.128 +
   9.129 +lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1]
   9.130 +
   9.131 +
   9.132 +(*** Introduction rules for Node ***)
   9.133 +
   9.134 +lemma Node_K0_I: "(%k. Inr 0, a) : Node"
   9.135 +by (simp add: Node_def)
   9.136 +
   9.137 +lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
   9.138 +apply (simp add: Node_def Push_def) 
   9.139 +apply (fast intro!: apfst_conv nat.case(2)[THEN trans])
   9.140 +done
   9.141 +
   9.142 +
   9.143 +subsection{*Freeness: Distinctness of Constructors*}
   9.144 +
   9.145 +(** Scons vs Atom **)
   9.146 +
   9.147 +lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)"
   9.148 +unfolding Atom_def Scons_def Push_Node_def One_nat_def
   9.149 +by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
   9.150 +         dest!: Abs_Node_inj 
   9.151 +         elim!: apfst_convE sym [THEN Push_neq_K0])  
   9.152 +
   9.153 +lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym]
   9.154 +
   9.155 +
   9.156 +(*** Injectiveness ***)
   9.157 +
   9.158 +(** Atomic nodes **)
   9.159 +
   9.160 +lemma inj_Atom: "inj(Atom)"
   9.161 +apply (simp add: Atom_def)
   9.162 +apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
   9.163 +done
   9.164 +lemmas Atom_inject = inj_Atom [THEN injD]
   9.165 +
   9.166 +lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
   9.167 +by (blast dest!: Atom_inject)
   9.168 +
   9.169 +lemma inj_Leaf: "inj(Leaf)"
   9.170 +apply (simp add: Leaf_def o_def)
   9.171 +apply (rule inj_onI)
   9.172 +apply (erule Atom_inject [THEN Inl_inject])
   9.173 +done
   9.174 +
   9.175 +lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD]
   9.176 +
   9.177 +lemma inj_Numb: "inj(Numb)"
   9.178 +apply (simp add: Numb_def o_def)
   9.179 +apply (rule inj_onI)
   9.180 +apply (erule Atom_inject [THEN Inr_inject])
   9.181 +done
   9.182 +
   9.183 +lemmas Numb_inject [dest!] = inj_Numb [THEN injD]
   9.184 +
   9.185 +
   9.186 +(** Injectiveness of Push_Node **)
   9.187 +
   9.188 +lemma Push_Node_inject:
   9.189 +    "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P  
   9.190 +     |] ==> P"
   9.191 +apply (simp add: Push_Node_def)
   9.192 +apply (erule Abs_Node_inj [THEN apfst_convE])
   9.193 +apply (rule Rep_Node [THEN Node_Push_I])+
   9.194 +apply (erule sym [THEN apfst_convE]) 
   9.195 +apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject)
   9.196 +done
   9.197 +
   9.198 +
   9.199 +(** Injectiveness of Scons **)
   9.200 +
   9.201 +lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'"
   9.202 +unfolding Scons_def One_nat_def
   9.203 +by (blast dest!: Push_Node_inject)
   9.204 +
   9.205 +lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'"
   9.206 +unfolding Scons_def One_nat_def
   9.207 +by (blast dest!: Push_Node_inject)
   9.208 +
   9.209 +lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
   9.210 +apply (erule equalityE)
   9.211 +apply (iprover intro: equalityI Scons_inject_lemma1)
   9.212 +done
   9.213 +
   9.214 +lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'"
   9.215 +apply (erule equalityE)
   9.216 +apply (iprover intro: equalityI Scons_inject_lemma2)
   9.217 +done
   9.218 +
   9.219 +lemma Scons_inject:
   9.220 +    "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P |] ==> P"
   9.221 +by (iprover dest: Scons_inject1 Scons_inject2)
   9.222 +
   9.223 +lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')"
   9.224 +by (blast elim!: Scons_inject)
   9.225 +
   9.226 +(*** Distinctness involving Leaf and Numb ***)
   9.227 +
   9.228 +(** Scons vs Leaf **)
   9.229 +
   9.230 +lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
   9.231 +unfolding Leaf_def o_def by (rule Scons_not_Atom)
   9.232 +
   9.233 +lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym]
   9.234 +
   9.235 +(** Scons vs Numb **)
   9.236 +
   9.237 +lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
   9.238 +unfolding Numb_def o_def by (rule Scons_not_Atom)
   9.239 +
   9.240 +lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym]
   9.241 +
   9.242 +
   9.243 +(** Leaf vs Numb **)
   9.244 +
   9.245 +lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
   9.246 +by (simp add: Leaf_def Numb_def)
   9.247 +
   9.248 +lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym]
   9.249 +
   9.250 +
   9.251 +(*** ndepth -- the depth of a node ***)
   9.252 +
   9.253 +lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0"
   9.254 +by (simp add: ndepth_def  Node_K0_I [THEN Abs_Node_inverse] Least_equality)
   9.255 +
   9.256 +lemma ndepth_Push_Node_aux:
   9.257 +     "case_nat (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k"
   9.258 +apply (induct_tac "k", auto)
   9.259 +apply (erule Least_le)
   9.260 +done
   9.261 +
   9.262 +lemma ndepth_Push_Node: 
   9.263 +    "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))"
   9.264 +apply (insert Rep_Node [of n, unfolded Node_def])
   9.265 +apply (auto simp add: ndepth_def Push_Node_def
   9.266 +                 Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse])
   9.267 +apply (rule Least_equality)
   9.268 +apply (auto simp add: Push_def ndepth_Push_Node_aux)
   9.269 +apply (erule LeastI)
   9.270 +done
   9.271 +
   9.272 +
   9.273 +(*** ntrunc applied to the various node sets ***)
   9.274 +
   9.275 +lemma ntrunc_0 [simp]: "ntrunc 0 M = {}"
   9.276 +by (simp add: ntrunc_def)
   9.277 +
   9.278 +lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)"
   9.279 +by (auto simp add: Atom_def ntrunc_def ndepth_K0)
   9.280 +
   9.281 +lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)"
   9.282 +unfolding Leaf_def o_def by (rule ntrunc_Atom)
   9.283 +
   9.284 +lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)"
   9.285 +unfolding Numb_def o_def by (rule ntrunc_Atom)
   9.286 +
   9.287 +lemma ntrunc_Scons [simp]: 
   9.288 +    "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"
   9.289 +unfolding Scons_def ntrunc_def One_nat_def
   9.290 +by (auto simp add: ndepth_Push_Node)
   9.291 +
   9.292 +
   9.293 +
   9.294 +(** Injection nodes **)
   9.295 +
   9.296 +lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}"
   9.297 +apply (simp add: In0_def)
   9.298 +apply (simp add: Scons_def)
   9.299 +done
   9.300 +
   9.301 +lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"
   9.302 +by (simp add: In0_def)
   9.303 +
   9.304 +lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}"
   9.305 +apply (simp add: In1_def)
   9.306 +apply (simp add: Scons_def)
   9.307 +done
   9.308 +
   9.309 +lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"
   9.310 +by (simp add: In1_def)
   9.311 +
   9.312 +
   9.313 +subsection{*Set Constructions*}
   9.314 +
   9.315 +
   9.316 +(*** Cartesian Product ***)
   9.317 +
   9.318 +lemma uprodI [intro!]: "[| M:A;  N:B |] ==> Scons M N : uprod A B"
   9.319 +by (simp add: uprod_def)
   9.320 +
   9.321 +(*The general elimination rule*)
   9.322 +lemma uprodE [elim!]:
   9.323 +    "[| c : uprod A B;   
   9.324 +        !!x y. [| x:A;  y:B;  c = Scons x y |] ==> P  
   9.325 +     |] ==> P"
   9.326 +by (auto simp add: uprod_def) 
   9.327 +
   9.328 +
   9.329 +(*Elimination of a pair -- introduces no eigenvariables*)
   9.330 +lemma uprodE2: "[| Scons M N : uprod A B;  [| M:A;  N:B |] ==> P |] ==> P"
   9.331 +by (auto simp add: uprod_def)
   9.332 +
   9.333 +
   9.334 +(*** Disjoint Sum ***)
   9.335 +
   9.336 +lemma usum_In0I [intro]: "M:A ==> In0(M) : usum A B"
   9.337 +by (simp add: usum_def)
   9.338 +
   9.339 +lemma usum_In1I [intro]: "N:B ==> In1(N) : usum A B"
   9.340 +by (simp add: usum_def)
   9.341 +
   9.342 +lemma usumE [elim!]: 
   9.343 +    "[| u : usum A B;   
   9.344 +        !!x. [| x:A;  u=In0(x) |] ==> P;  
   9.345 +        !!y. [| y:B;  u=In1(y) |] ==> P  
   9.346 +     |] ==> P"
   9.347 +by (auto simp add: usum_def)
   9.348 +
   9.349 +
   9.350 +(** Injection **)
   9.351 +
   9.352 +lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
   9.353 +unfolding In0_def In1_def One_nat_def by auto
   9.354 +
   9.355 +lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym]
   9.356 +
   9.357 +lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
   9.358 +by (simp add: In0_def)
   9.359 +
   9.360 +lemma In1_inject: "In1(M) = In1(N) ==>  M=N"
   9.361 +by (simp add: In1_def)
   9.362 +
   9.363 +lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)"
   9.364 +by (blast dest!: In0_inject)
   9.365 +
   9.366 +lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)"
   9.367 +by (blast dest!: In1_inject)
   9.368 +
   9.369 +lemma inj_In0: "inj In0"
   9.370 +by (blast intro!: inj_onI)
   9.371 +
   9.372 +lemma inj_In1: "inj In1"
   9.373 +by (blast intro!: inj_onI)
   9.374 +
   9.375 +
   9.376 +(*** Function spaces ***)
   9.377 +
   9.378 +lemma Lim_inject: "Lim f = Lim g ==> f = g"
   9.379 +apply (simp add: Lim_def)
   9.380 +apply (rule ext)
   9.381 +apply (blast elim!: Push_Node_inject)
   9.382 +done
   9.383 +
   9.384 +
   9.385 +(*** proving equality of sets and functions using ntrunc ***)
   9.386 +
   9.387 +lemma ntrunc_subsetI: "ntrunc k M <= M"
   9.388 +by (auto simp add: ntrunc_def)
   9.389 +
   9.390 +lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N"
   9.391 +by (auto simp add: ntrunc_def)
   9.392 +
   9.393 +(*A generalized form of the take-lemma*)
   9.394 +lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N"
   9.395 +apply (rule equalityI)
   9.396 +apply (rule_tac [!] ntrunc_subsetD)
   9.397 +apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto) 
   9.398 +done
   9.399 +
   9.400 +lemma ntrunc_o_equality: 
   9.401 +    "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2"
   9.402 +apply (rule ntrunc_equality [THEN ext])
   9.403 +apply (simp add: fun_eq_iff) 
   9.404 +done
   9.405 +
   9.406 +
   9.407 +(*** Monotonicity ***)
   9.408 +
   9.409 +lemma uprod_mono: "[| A<=A';  B<=B' |] ==> uprod A B <= uprod A' B'"
   9.410 +by (simp add: uprod_def, blast)
   9.411 +
   9.412 +lemma usum_mono: "[| A<=A';  B<=B' |] ==> usum A B <= usum A' B'"
   9.413 +by (simp add: usum_def, blast)
   9.414 +
   9.415 +lemma Scons_mono: "[| M<=M';  N<=N' |] ==> Scons M N <= Scons M' N'"
   9.416 +by (simp add: Scons_def, blast)
   9.417 +
   9.418 +lemma In0_mono: "M<=N ==> In0(M) <= In0(N)"
   9.419 +by (simp add: In0_def Scons_mono)
   9.420 +
   9.421 +lemma In1_mono: "M<=N ==> In1(M) <= In1(N)"
   9.422 +by (simp add: In1_def Scons_mono)
   9.423 +
   9.424 +
   9.425 +(*** Split and Case ***)
   9.426 +
   9.427 +lemma Split [simp]: "Split c (Scons M N) = c M N"
   9.428 +by (simp add: Split_def)
   9.429 +
   9.430 +lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)"
   9.431 +by (simp add: Case_def)
   9.432 +
   9.433 +lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)"
   9.434 +by (simp add: Case_def)
   9.435 +
   9.436 +
   9.437 +
   9.438 +(**** UN x. B(x) rules ****)
   9.439 +
   9.440 +lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))"
   9.441 +by (simp add: ntrunc_def, blast)
   9.442 +
   9.443 +lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)"
   9.444 +by (simp add: Scons_def, blast)
   9.445 +
   9.446 +lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))"
   9.447 +by (simp add: Scons_def, blast)
   9.448 +
   9.449 +lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))"
   9.450 +by (simp add: In0_def Scons_UN1_y)
   9.451 +
   9.452 +lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))"
   9.453 +by (simp add: In1_def Scons_UN1_y)
   9.454 +
   9.455 +
   9.456 +(*** Equality for Cartesian Product ***)
   9.457 +
   9.458 +lemma dprodI [intro!]: 
   9.459 +    "[| (M,M'):r;  (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s"
   9.460 +by (auto simp add: dprod_def)
   9.461 +
   9.462 +(*The general elimination rule*)
   9.463 +lemma dprodE [elim!]: 
   9.464 +    "[| c : dprod r s;   
   9.465 +        !!x y x' y'. [| (x,x') : r;  (y,y') : s;  
   9.466 +                        c = (Scons x y, Scons x' y') |] ==> P  
   9.467 +     |] ==> P"
   9.468 +by (auto simp add: dprod_def)
   9.469 +
   9.470 +
   9.471 +(*** Equality for Disjoint Sum ***)
   9.472 +
   9.473 +lemma dsum_In0I [intro]: "(M,M'):r ==> (In0(M), In0(M')) : dsum r s"
   9.474 +by (auto simp add: dsum_def)
   9.475 +
   9.476 +lemma dsum_In1I [intro]: "(N,N'):s ==> (In1(N), In1(N')) : dsum r s"
   9.477 +by (auto simp add: dsum_def)
   9.478 +
   9.479 +lemma dsumE [elim!]: 
   9.480 +    "[| w : dsum r s;   
   9.481 +        !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P;  
   9.482 +        !!y y'. [| (y,y') : s;  w = (In1(y), In1(y')) |] ==> P  
   9.483 +     |] ==> P"
   9.484 +by (auto simp add: dsum_def)
   9.485 +
   9.486 +
   9.487 +(*** Monotonicity ***)
   9.488 +
   9.489 +lemma dprod_mono: "[| r<=r';  s<=s' |] ==> dprod r s <= dprod r' s'"
   9.490 +by blast
   9.491 +
   9.492 +lemma dsum_mono: "[| r<=r';  s<=s' |] ==> dsum r s <= dsum r' s'"
   9.493 +by blast
   9.494 +
   9.495 +
   9.496 +(*** Bounding theorems ***)
   9.497 +
   9.498 +lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
   9.499 +by blast
   9.500 +
   9.501 +lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
   9.502 +
   9.503 +(*Dependent version*)
   9.504 +lemma dprod_subset_Sigma2:
   9.505 +    "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
   9.506 +by auto
   9.507 +
   9.508 +lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
   9.509 +by blast
   9.510 +
   9.511 +lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
   9.512 +
   9.513 +
   9.514 +(*** Domain theorems ***)
   9.515 +
   9.516 +lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
   9.517 +  by auto
   9.518 +
   9.519 +lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
   9.520 +  by auto
   9.521 +
   9.522 +
   9.523 +text {* hides popular names *}
   9.524 +hide_type (open) node item
   9.525 +hide_const (open) Push Node Atom Leaf Numb Lim Split Case
   9.526 +
   9.527 +ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
   9.528 +ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
   9.529 +
   9.530 +end
    10.1 --- a/src/HOL/Main.thy	Thu Sep 18 16:47:40 2014 +0200
    10.2 +++ b/src/HOL/Main.thy	Thu Sep 18 16:47:40 2014 +0200
    10.3 @@ -2,7 +2,7 @@
    10.4  
    10.5  theory Main
    10.6  imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
    10.7 -  Basic_BNF_Least_Fixpoints BNF_Greatest_Fixpoint Old_Datatype
    10.8 +  Basic_BNF_Least_Fixpoints BNF_Greatest_Fixpoint
    10.9  begin
   10.10  
   10.11  text {*
    11.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Sep 18 16:47:40 2014 +0200
    11.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 18 16:47:40 2014 +0200
    11.3 @@ -1,5 +1,5 @@
    11.4  theory Nominal 
    11.5 -imports Main "~~/src/HOL/Library/Infinite_Set"
    11.6 +imports "~~/src/HOL/Library/Infinite_Set" "~~/src/HOL/Library/Old_Datatype"
    11.7  keywords
    11.8    "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
    11.9    "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
    12.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Sep 18 16:47:40 2014 +0200
    12.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Sep 18 16:47:40 2014 +0200
    12.3 @@ -752,7 +752,7 @@
    12.4                    Old_Datatype_Aux.DtRec k => if k < length new_type_names then
    12.5                        Const (nth rep_names k, Old_Datatype_Aux.typ_of_dtyp descr'' dt -->
    12.6                          Old_Datatype_Aux.typ_of_dtyp descr dt) $ x
    12.7 -                    else error "nested recursion not (yet) supported"
    12.8 +                    else error "nested recursion not supported"
    12.9                  | _ => x) :: r_args)
   12.10            end
   12.11  
    13.1 --- a/src/HOL/Old_Datatype.thy	Thu Sep 18 16:47:40 2014 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,529 +0,0 @@
    13.4 -(*  Title:      HOL/Old_Datatype.thy
    13.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.6 -    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    13.7 -*)
    13.8 -
    13.9 -header {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
   13.10 -
   13.11 -theory Old_Datatype
   13.12 -imports Power
   13.13 -keywords "old_datatype" :: thy_decl
   13.14 -begin
   13.15 -
   13.16 -subsection {* The datatype universe *}
   13.17 -
   13.18 -definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
   13.19 -
   13.20 -typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
   13.21 -  morphisms Rep_Node Abs_Node
   13.22 -  unfolding Node_def by auto
   13.23 -
   13.24 -text{*Datatypes will be represented by sets of type @{text node}*}
   13.25 -
   13.26 -type_synonym 'a item        = "('a, unit) node set"
   13.27 -type_synonym ('a, 'b) dtree = "('a, 'b) node set"
   13.28 -
   13.29 -consts
   13.30 -  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
   13.31 -
   13.32 -  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
   13.33 -  ndepth    :: "('a, 'b) node => nat"
   13.34 -
   13.35 -  Atom      :: "('a + nat) => ('a, 'b) dtree"
   13.36 -  Leaf      :: "'a => ('a, 'b) dtree"
   13.37 -  Numb      :: "nat => ('a, 'b) dtree"
   13.38 -  Scons     :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
   13.39 -  In0       :: "('a, 'b) dtree => ('a, 'b) dtree"
   13.40 -  In1       :: "('a, 'b) dtree => ('a, 'b) dtree"
   13.41 -  Lim       :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
   13.42 -
   13.43 -  ntrunc    :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
   13.44 -
   13.45 -  uprod     :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
   13.46 -  usum      :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
   13.47 -
   13.48 -  Split     :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
   13.49 -  Case      :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
   13.50 -
   13.51 -  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
   13.52 -                => (('a, 'b) dtree * ('a, 'b) dtree)set"
   13.53 -  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
   13.54 -                => (('a, 'b) dtree * ('a, 'b) dtree)set"
   13.55 -
   13.56 -
   13.57 -defs
   13.58 -
   13.59 -  Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
   13.60 -
   13.61 -  (*crude "lists" of nats -- needed for the constructions*)
   13.62 -  Push_def:   "Push == (%b h. case_nat b h)"
   13.63 -
   13.64 -  (** operations on S-expressions -- sets of nodes **)
   13.65 -
   13.66 -  (*S-expression constructors*)
   13.67 -  Atom_def:   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
   13.68 -  Scons_def:  "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
   13.69 -
   13.70 -  (*Leaf nodes, with arbitrary or nat labels*)
   13.71 -  Leaf_def:   "Leaf == Atom o Inl"
   13.72 -  Numb_def:   "Numb == Atom o Inr"
   13.73 -
   13.74 -  (*Injections of the "disjoint sum"*)
   13.75 -  In0_def:    "In0(M) == Scons (Numb 0) M"
   13.76 -  In1_def:    "In1(M) == Scons (Numb 1) M"
   13.77 -
   13.78 -  (*Function spaces*)
   13.79 -  Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
   13.80 -
   13.81 -  (*the set of nodes with depth less than k*)
   13.82 -  ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
   13.83 -  ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}"
   13.84 -
   13.85 -  (*products and sums for the "universe"*)
   13.86 -  uprod_def:  "uprod A B == UN x:A. UN y:B. { Scons x y }"
   13.87 -  usum_def:   "usum A B == In0`A Un In1`B"
   13.88 -
   13.89 -  (*the corresponding eliminators*)
   13.90 -  Split_def:  "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
   13.91 -
   13.92 -  Case_def:   "Case c d M == THE u.  (EX x . M = In0(x) & u = c(x))
   13.93 -                                  | (EX y . M = In1(y) & u = d(y))"
   13.94 -
   13.95 -
   13.96 -  (** equality for the "universe" **)
   13.97 -
   13.98 -  dprod_def:  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
   13.99 -
  13.100 -  dsum_def:   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
  13.101 -                          (UN (y,y'):s. {(In1(y),In1(y'))})"
  13.102 -
  13.103 -
  13.104 -
  13.105 -lemma apfst_convE: 
  13.106 -    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R  
  13.107 -     |] ==> R"
  13.108 -by (force simp add: apfst_def)
  13.109 -
  13.110 -(** Push -- an injection, analogous to Cons on lists **)
  13.111 -
  13.112 -lemma Push_inject1: "Push i f = Push j g  ==> i=j"
  13.113 -apply (simp add: Push_def fun_eq_iff) 
  13.114 -apply (drule_tac x=0 in spec, simp) 
  13.115 -done
  13.116 -
  13.117 -lemma Push_inject2: "Push i f = Push j g  ==> f=g"
  13.118 -apply (auto simp add: Push_def fun_eq_iff) 
  13.119 -apply (drule_tac x="Suc x" in spec, simp) 
  13.120 -done
  13.121 -
  13.122 -lemma Push_inject:
  13.123 -    "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P |] ==> P"
  13.124 -by (blast dest: Push_inject1 Push_inject2) 
  13.125 -
  13.126 -lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
  13.127 -by (auto simp add: Push_def fun_eq_iff split: nat.split_asm)
  13.128 -
  13.129 -lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1]
  13.130 -
  13.131 -
  13.132 -(*** Introduction rules for Node ***)
  13.133 -
  13.134 -lemma Node_K0_I: "(%k. Inr 0, a) : Node"
  13.135 -by (simp add: Node_def)
  13.136 -
  13.137 -lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
  13.138 -apply (simp add: Node_def Push_def) 
  13.139 -apply (fast intro!: apfst_conv nat.case(2)[THEN trans])
  13.140 -done
  13.141 -
  13.142 -
  13.143 -subsection{*Freeness: Distinctness of Constructors*}
  13.144 -
  13.145 -(** Scons vs Atom **)
  13.146 -
  13.147 -lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)"
  13.148 -unfolding Atom_def Scons_def Push_Node_def One_nat_def
  13.149 -by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
  13.150 -         dest!: Abs_Node_inj 
  13.151 -         elim!: apfst_convE sym [THEN Push_neq_K0])  
  13.152 -
  13.153 -lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym]
  13.154 -
  13.155 -
  13.156 -(*** Injectiveness ***)
  13.157 -
  13.158 -(** Atomic nodes **)
  13.159 -
  13.160 -lemma inj_Atom: "inj(Atom)"
  13.161 -apply (simp add: Atom_def)
  13.162 -apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
  13.163 -done
  13.164 -lemmas Atom_inject = inj_Atom [THEN injD]
  13.165 -
  13.166 -lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
  13.167 -by (blast dest!: Atom_inject)
  13.168 -
  13.169 -lemma inj_Leaf: "inj(Leaf)"
  13.170 -apply (simp add: Leaf_def o_def)
  13.171 -apply (rule inj_onI)
  13.172 -apply (erule Atom_inject [THEN Inl_inject])
  13.173 -done
  13.174 -
  13.175 -lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD]
  13.176 -
  13.177 -lemma inj_Numb: "inj(Numb)"
  13.178 -apply (simp add: Numb_def o_def)
  13.179 -apply (rule inj_onI)
  13.180 -apply (erule Atom_inject [THEN Inr_inject])
  13.181 -done
  13.182 -
  13.183 -lemmas Numb_inject [dest!] = inj_Numb [THEN injD]
  13.184 -
  13.185 -
  13.186 -(** Injectiveness of Push_Node **)
  13.187 -
  13.188 -lemma Push_Node_inject:
  13.189 -    "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P  
  13.190 -     |] ==> P"
  13.191 -apply (simp add: Push_Node_def)
  13.192 -apply (erule Abs_Node_inj [THEN apfst_convE])
  13.193 -apply (rule Rep_Node [THEN Node_Push_I])+
  13.194 -apply (erule sym [THEN apfst_convE]) 
  13.195 -apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject)
  13.196 -done
  13.197 -
  13.198 -
  13.199 -(** Injectiveness of Scons **)
  13.200 -
  13.201 -lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'"
  13.202 -unfolding Scons_def One_nat_def
  13.203 -by (blast dest!: Push_Node_inject)
  13.204 -
  13.205 -lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'"
  13.206 -unfolding Scons_def One_nat_def
  13.207 -by (blast dest!: Push_Node_inject)
  13.208 -
  13.209 -lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
  13.210 -apply (erule equalityE)
  13.211 -apply (iprover intro: equalityI Scons_inject_lemma1)
  13.212 -done
  13.213 -
  13.214 -lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'"
  13.215 -apply (erule equalityE)
  13.216 -apply (iprover intro: equalityI Scons_inject_lemma2)
  13.217 -done
  13.218 -
  13.219 -lemma Scons_inject:
  13.220 -    "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P |] ==> P"
  13.221 -by (iprover dest: Scons_inject1 Scons_inject2)
  13.222 -
  13.223 -lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')"
  13.224 -by (blast elim!: Scons_inject)
  13.225 -
  13.226 -(*** Distinctness involving Leaf and Numb ***)
  13.227 -
  13.228 -(** Scons vs Leaf **)
  13.229 -
  13.230 -lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
  13.231 -unfolding Leaf_def o_def by (rule Scons_not_Atom)
  13.232 -
  13.233 -lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym]
  13.234 -
  13.235 -(** Scons vs Numb **)
  13.236 -
  13.237 -lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
  13.238 -unfolding Numb_def o_def by (rule Scons_not_Atom)
  13.239 -
  13.240 -lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym]
  13.241 -
  13.242 -
  13.243 -(** Leaf vs Numb **)
  13.244 -
  13.245 -lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
  13.246 -by (simp add: Leaf_def Numb_def)
  13.247 -
  13.248 -lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym]
  13.249 -
  13.250 -
  13.251 -(*** ndepth -- the depth of a node ***)
  13.252 -
  13.253 -lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0"
  13.254 -by (simp add: ndepth_def  Node_K0_I [THEN Abs_Node_inverse] Least_equality)
  13.255 -
  13.256 -lemma ndepth_Push_Node_aux:
  13.257 -     "case_nat (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k"
  13.258 -apply (induct_tac "k", auto)
  13.259 -apply (erule Least_le)
  13.260 -done
  13.261 -
  13.262 -lemma ndepth_Push_Node: 
  13.263 -    "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))"
  13.264 -apply (insert Rep_Node [of n, unfolded Node_def])
  13.265 -apply (auto simp add: ndepth_def Push_Node_def
  13.266 -                 Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse])
  13.267 -apply (rule Least_equality)
  13.268 -apply (auto simp add: Push_def ndepth_Push_Node_aux)
  13.269 -apply (erule LeastI)
  13.270 -done
  13.271 -
  13.272 -
  13.273 -(*** ntrunc applied to the various node sets ***)
  13.274 -
  13.275 -lemma ntrunc_0 [simp]: "ntrunc 0 M = {}"
  13.276 -by (simp add: ntrunc_def)
  13.277 -
  13.278 -lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)"
  13.279 -by (auto simp add: Atom_def ntrunc_def ndepth_K0)
  13.280 -
  13.281 -lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)"
  13.282 -unfolding Leaf_def o_def by (rule ntrunc_Atom)
  13.283 -
  13.284 -lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)"
  13.285 -unfolding Numb_def o_def by (rule ntrunc_Atom)
  13.286 -
  13.287 -lemma ntrunc_Scons [simp]: 
  13.288 -    "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"
  13.289 -unfolding Scons_def ntrunc_def One_nat_def
  13.290 -by (auto simp add: ndepth_Push_Node)
  13.291 -
  13.292 -
  13.293 -
  13.294 -(** Injection nodes **)
  13.295 -
  13.296 -lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}"
  13.297 -apply (simp add: In0_def)
  13.298 -apply (simp add: Scons_def)
  13.299 -done
  13.300 -
  13.301 -lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"
  13.302 -by (simp add: In0_def)
  13.303 -
  13.304 -lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}"
  13.305 -apply (simp add: In1_def)
  13.306 -apply (simp add: Scons_def)
  13.307 -done
  13.308 -
  13.309 -lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"
  13.310 -by (simp add: In1_def)
  13.311 -
  13.312 -
  13.313 -subsection{*Set Constructions*}
  13.314 -
  13.315 -
  13.316 -(*** Cartesian Product ***)
  13.317 -
  13.318 -lemma uprodI [intro!]: "[| M:A;  N:B |] ==> Scons M N : uprod A B"
  13.319 -by (simp add: uprod_def)
  13.320 -
  13.321 -(*The general elimination rule*)
  13.322 -lemma uprodE [elim!]:
  13.323 -    "[| c : uprod A B;   
  13.324 -        !!x y. [| x:A;  y:B;  c = Scons x y |] ==> P  
  13.325 -     |] ==> P"
  13.326 -by (auto simp add: uprod_def) 
  13.327 -
  13.328 -
  13.329 -(*Elimination of a pair -- introduces no eigenvariables*)
  13.330 -lemma uprodE2: "[| Scons M N : uprod A B;  [| M:A;  N:B |] ==> P |] ==> P"
  13.331 -by (auto simp add: uprod_def)
  13.332 -
  13.333 -
  13.334 -(*** Disjoint Sum ***)
  13.335 -
  13.336 -lemma usum_In0I [intro]: "M:A ==> In0(M) : usum A B"
  13.337 -by (simp add: usum_def)
  13.338 -
  13.339 -lemma usum_In1I [intro]: "N:B ==> In1(N) : usum A B"
  13.340 -by (simp add: usum_def)
  13.341 -
  13.342 -lemma usumE [elim!]: 
  13.343 -    "[| u : usum A B;   
  13.344 -        !!x. [| x:A;  u=In0(x) |] ==> P;  
  13.345 -        !!y. [| y:B;  u=In1(y) |] ==> P  
  13.346 -     |] ==> P"
  13.347 -by (auto simp add: usum_def)
  13.348 -
  13.349 -
  13.350 -(** Injection **)
  13.351 -
  13.352 -lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
  13.353 -unfolding In0_def In1_def One_nat_def by auto
  13.354 -
  13.355 -lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym]
  13.356 -
  13.357 -lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
  13.358 -by (simp add: In0_def)
  13.359 -
  13.360 -lemma In1_inject: "In1(M) = In1(N) ==>  M=N"
  13.361 -by (simp add: In1_def)
  13.362 -
  13.363 -lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)"
  13.364 -by (blast dest!: In0_inject)
  13.365 -
  13.366 -lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)"
  13.367 -by (blast dest!: In1_inject)
  13.368 -
  13.369 -lemma inj_In0: "inj In0"
  13.370 -by (blast intro!: inj_onI)
  13.371 -
  13.372 -lemma inj_In1: "inj In1"
  13.373 -by (blast intro!: inj_onI)
  13.374 -
  13.375 -
  13.376 -(*** Function spaces ***)
  13.377 -
  13.378 -lemma Lim_inject: "Lim f = Lim g ==> f = g"
  13.379 -apply (simp add: Lim_def)
  13.380 -apply (rule ext)
  13.381 -apply (blast elim!: Push_Node_inject)
  13.382 -done
  13.383 -
  13.384 -
  13.385 -(*** proving equality of sets and functions using ntrunc ***)
  13.386 -
  13.387 -lemma ntrunc_subsetI: "ntrunc k M <= M"
  13.388 -by (auto simp add: ntrunc_def)
  13.389 -
  13.390 -lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N"
  13.391 -by (auto simp add: ntrunc_def)
  13.392 -
  13.393 -(*A generalized form of the take-lemma*)
  13.394 -lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N"
  13.395 -apply (rule equalityI)
  13.396 -apply (rule_tac [!] ntrunc_subsetD)
  13.397 -apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto) 
  13.398 -done
  13.399 -
  13.400 -lemma ntrunc_o_equality: 
  13.401 -    "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2"
  13.402 -apply (rule ntrunc_equality [THEN ext])
  13.403 -apply (simp add: fun_eq_iff) 
  13.404 -done
  13.405 -
  13.406 -
  13.407 -(*** Monotonicity ***)
  13.408 -
  13.409 -lemma uprod_mono: "[| A<=A';  B<=B' |] ==> uprod A B <= uprod A' B'"
  13.410 -by (simp add: uprod_def, blast)
  13.411 -
  13.412 -lemma usum_mono: "[| A<=A';  B<=B' |] ==> usum A B <= usum A' B'"
  13.413 -by (simp add: usum_def, blast)
  13.414 -
  13.415 -lemma Scons_mono: "[| M<=M';  N<=N' |] ==> Scons M N <= Scons M' N'"
  13.416 -by (simp add: Scons_def, blast)
  13.417 -
  13.418 -lemma In0_mono: "M<=N ==> In0(M) <= In0(N)"
  13.419 -by (simp add: In0_def Scons_mono)
  13.420 -
  13.421 -lemma In1_mono: "M<=N ==> In1(M) <= In1(N)"
  13.422 -by (simp add: In1_def Scons_mono)
  13.423 -
  13.424 -
  13.425 -(*** Split and Case ***)
  13.426 -
  13.427 -lemma Split [simp]: "Split c (Scons M N) = c M N"
  13.428 -by (simp add: Split_def)
  13.429 -
  13.430 -lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)"
  13.431 -by (simp add: Case_def)
  13.432 -
  13.433 -lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)"
  13.434 -by (simp add: Case_def)
  13.435 -
  13.436 -
  13.437 -
  13.438 -(**** UN x. B(x) rules ****)
  13.439 -
  13.440 -lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))"
  13.441 -by (simp add: ntrunc_def, blast)
  13.442 -
  13.443 -lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)"
  13.444 -by (simp add: Scons_def, blast)
  13.445 -
  13.446 -lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))"
  13.447 -by (simp add: Scons_def, blast)
  13.448 -
  13.449 -lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))"
  13.450 -by (simp add: In0_def Scons_UN1_y)
  13.451 -
  13.452 -lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))"
  13.453 -by (simp add: In1_def Scons_UN1_y)
  13.454 -
  13.455 -
  13.456 -(*** Equality for Cartesian Product ***)
  13.457 -
  13.458 -lemma dprodI [intro!]: 
  13.459 -    "[| (M,M'):r;  (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s"
  13.460 -by (auto simp add: dprod_def)
  13.461 -
  13.462 -(*The general elimination rule*)
  13.463 -lemma dprodE [elim!]: 
  13.464 -    "[| c : dprod r s;   
  13.465 -        !!x y x' y'. [| (x,x') : r;  (y,y') : s;  
  13.466 -                        c = (Scons x y, Scons x' y') |] ==> P  
  13.467 -     |] ==> P"
  13.468 -by (auto simp add: dprod_def)
  13.469 -
  13.470 -
  13.471 -(*** Equality for Disjoint Sum ***)
  13.472 -
  13.473 -lemma dsum_In0I [intro]: "(M,M'):r ==> (In0(M), In0(M')) : dsum r s"
  13.474 -by (auto simp add: dsum_def)
  13.475 -
  13.476 -lemma dsum_In1I [intro]: "(N,N'):s ==> (In1(N), In1(N')) : dsum r s"
  13.477 -by (auto simp add: dsum_def)
  13.478 -
  13.479 -lemma dsumE [elim!]: 
  13.480 -    "[| w : dsum r s;   
  13.481 -        !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P;  
  13.482 -        !!y y'. [| (y,y') : s;  w = (In1(y), In1(y')) |] ==> P  
  13.483 -     |] ==> P"
  13.484 -by (auto simp add: dsum_def)
  13.485 -
  13.486 -
  13.487 -(*** Monotonicity ***)
  13.488 -
  13.489 -lemma dprod_mono: "[| r<=r';  s<=s' |] ==> dprod r s <= dprod r' s'"
  13.490 -by blast
  13.491 -
  13.492 -lemma dsum_mono: "[| r<=r';  s<=s' |] ==> dsum r s <= dsum r' s'"
  13.493 -by blast
  13.494 -
  13.495 -
  13.496 -(*** Bounding theorems ***)
  13.497 -
  13.498 -lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
  13.499 -by blast
  13.500 -
  13.501 -lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
  13.502 -
  13.503 -(*Dependent version*)
  13.504 -lemma dprod_subset_Sigma2:
  13.505 -    "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
  13.506 -by auto
  13.507 -
  13.508 -lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
  13.509 -by blast
  13.510 -
  13.511 -lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
  13.512 -
  13.513 -
  13.514 -(*** Domain theorems ***)
  13.515 -
  13.516 -lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
  13.517 -  by auto
  13.518 -
  13.519 -lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
  13.520 -  by auto
  13.521 -
  13.522 -
  13.523 -text {* hides popular names *}
  13.524 -hide_type (open) node item
  13.525 -hide_const (open) Push Node Atom Leaf Numb Lim Split Case
  13.526 -
  13.527 -ML_file "Tools/Old_Datatype/old_datatype.ML"
  13.528 -
  13.529 -ML_file "Tools/inductive_realizer.ML"
  13.530 -setup InductiveRealizer.setup
  13.531 -
  13.532 -end
    14.1 --- a/src/HOL/Proofs/Extraction/Higman.thy	Thu Sep 18 16:47:40 2014 +0200
    14.2 +++ b/src/HOL/Proofs/Extraction/Higman.thy	Thu Sep 18 16:47:40 2014 +0200
    14.3 @@ -6,7 +6,7 @@
    14.4  header {* Higman's lemma *}
    14.5  
    14.6  theory Higman
    14.7 -imports Main
    14.8 +imports Old_Datatype
    14.9  begin
   14.10  
   14.11  text {*
    15.1 --- a/src/HOL/Proofs/Extraction/Util.thy	Thu Sep 18 16:47:40 2014 +0200
    15.2 +++ b/src/HOL/Proofs/Extraction/Util.thy	Thu Sep 18 16:47:40 2014 +0200
    15.3 @@ -5,7 +5,7 @@
    15.4  header {* Auxiliary lemmas used in program extraction examples *}
    15.5  
    15.6  theory Util
    15.7 -imports Main
    15.8 +imports Old_Datatype
    15.9  begin
   15.10  
   15.11  text {*
    16.1 --- a/src/HOL/Proofs/Extraction/Warshall.thy	Thu Sep 18 16:47:40 2014 +0200
    16.2 +++ b/src/HOL/Proofs/Extraction/Warshall.thy	Thu Sep 18 16:47:40 2014 +0200
    16.3 @@ -5,7 +5,7 @@
    16.4  header {* Warshall's algorithm *}
    16.5  
    16.6  theory Warshall
    16.7 -imports Main
    16.8 +imports Old_Datatype
    16.9  begin
   16.10  
   16.11  text {*
    17.1 --- a/src/HOL/Proofs/Lambda/Commutation.thy	Thu Sep 18 16:47:40 2014 +0200
    17.2 +++ b/src/HOL/Proofs/Lambda/Commutation.thy	Thu Sep 18 16:47:40 2014 +0200
    17.3 @@ -5,7 +5,9 @@
    17.4  
    17.5  header {* Abstract commutation and confluence notions *}
    17.6  
    17.7 -theory Commutation imports Main begin
    17.8 +theory Commutation
    17.9 +imports Old_Datatype
   17.10 +begin
   17.11  
   17.12  declare [[syntax_ambiguity_warning = false]]
   17.13  
    18.1 --- a/src/HOL/Proofs/Lambda/Lambda.thy	Thu Sep 18 16:47:40 2014 +0200
    18.2 +++ b/src/HOL/Proofs/Lambda/Lambda.thy	Thu Sep 18 16:47:40 2014 +0200
    18.3 @@ -5,7 +5,9 @@
    18.4  
    18.5  header {* Basic definitions of Lambda-calculus *}
    18.6  
    18.7 -theory Lambda imports Main begin
    18.8 +theory Lambda
    18.9 +imports Old_Datatype
   18.10 +begin
   18.11  
   18.12  declare [[syntax_ambiguity_warning = false]]
   18.13  
    19.1 --- a/src/HOL/Proofs/Lambda/ListOrder.thy	Thu Sep 18 16:47:40 2014 +0200
    19.2 +++ b/src/HOL/Proofs/Lambda/ListOrder.thy	Thu Sep 18 16:47:40 2014 +0200
    19.3 @@ -5,7 +5,9 @@
    19.4  
    19.5  header {* Lifting an order to lists of elements *}
    19.6  
    19.7 -theory ListOrder imports Main begin
    19.8 +theory ListOrder
    19.9 +imports Old_Datatype
   19.10 +begin
   19.11  
   19.12  declare [[syntax_ambiguity_warning = false]]
   19.13  
    20.1 --- a/src/HOL/Proofs/ex/XML_Data.thy	Thu Sep 18 16:47:40 2014 +0200
    20.2 +++ b/src/HOL/Proofs/ex/XML_Data.thy	Thu Sep 18 16:47:40 2014 +0200
    20.3 @@ -63,4 +63,3 @@
    20.4  *}
    20.5  
    20.6  end
    20.7 -
    21.1 --- a/src/HOL/ROOT	Thu Sep 18 16:47:40 2014 +0200
    21.2 +++ b/src/HOL/ROOT	Thu Sep 18 16:47:40 2014 +0200
    21.3 @@ -21,7 +21,7 @@
    21.4    *}
    21.5    options [timeout = 5400, document = false]
    21.6    theories Proofs (*sequential change of global flag!*)
    21.7 -  theories Main
    21.8 +  theories "~~/src/HOL/Library/Old_Datatype"
    21.9    files
   21.10      "Tools/Quickcheck/Narrowing_Engine.hs"
   21.11      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
   21.12 @@ -51,6 +51,7 @@
   21.13      RBT_Set
   21.14      (*legacy tools*)
   21.15      Refute
   21.16 +    Old_Datatype
   21.17      Old_Recdef
   21.18      Old_SMT
   21.19    theories [condition = ISABELLE_FULL_TEST]
   21.20 @@ -91,11 +92,13 @@
   21.21  
   21.22      PropLog proves the completeness of a formalization of propositional logic
   21.23      (see
   21.24 -    HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
   21.25 +    http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
   21.26  
   21.27      Exp demonstrates the use of iterated inductive definitions to reason about
   21.28      mutually recursive relations.
   21.29    *}
   21.30 +  theories [document = false]
   21.31 +    "~~/src/HOL/Library/Old_Datatype"
   21.32    theories [quick_and_dirty]
   21.33      Common_Patterns
   21.34    theories
   21.35 @@ -741,6 +744,7 @@
   21.36    *}
   21.37    options [document = false]
   21.38    theories
   21.39 +    "~~/src/HOL/Library/Old_Datatype"
   21.40      Compat
   21.41      Lambda_Term
   21.42      Process
    22.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Sep 18 16:47:40 2014 +0200
    22.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Sep 18 16:47:40 2014 +0200
    22.3 @@ -8,7 +8,6 @@
    22.4  signature INDUCTIVE_REALIZER =
    22.5  sig
    22.6    val add_ind_realizers: string -> string list -> theory -> theory
    22.7 -  val setup: theory -> theory
    22.8  end;
    22.9  
   22.10  structure InductiveRealizer : INDUCTIVE_REALIZER =
   22.11 @@ -513,11 +512,10 @@
   22.12        | SOME (SOME sets') => subtract (op =) sets' sets)
   22.13    end I);
   22.14  
   22.15 -val setup =
   22.16 -  Attrib.setup @{binding ind_realizer}
   22.17 -    ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
   22.18 -      Scan.option (Scan.lift (Args.colon) |--
   22.19 -        Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib)
   22.20 -    "add realizers for inductive set";
   22.21 +val _ = Theory.setup (Attrib.setup @{binding ind_realizer}
   22.22 +  ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
   22.23 +    Scan.option (Scan.lift (Args.colon) |--
   22.24 +      Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib)
   22.25 +  "add realizers for inductive set");
   22.26  
   22.27  end;