# HG changeset patch
# User paulson
# Date 914860768 -3600
# Node ID 8a1059aa01f084a93b721eb7f5db660d30a928f6
# Parent  4f093e55beebf494d7008e3a1f5193b07121321d
new inductive, datatype and primrec packages, etc.

diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/AC.thy
--- a/src/ZF/AC.thy	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/AC.thy	Mon Dec 28 16:59:28 1998 +0100
@@ -9,6 +9,12 @@
 *)
 
 AC = func +
+
+constdefs
+  (*Needs to be visible for Zorn.thy*)
+  increasing :: i=>i
+    "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
+
 rules
   AC    "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
 end
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Bool.ML
--- a/src/ZF/Bool.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Bool.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -24,6 +24,8 @@
 by (rtac consI1 1);
 qed "bool_0I";
 
+Addsimps [bool_1I, bool_0I];
+
 Goalw bool_defs "1~=0";
 by (rtac succ_not_0 1);
 qed "one_not_0";
@@ -54,10 +56,16 @@
 fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
 
 
-Goal "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
+Goal "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
 by (bool_tac 1);
 qed "cond_type";
 
+(*For Simp_tac and Blast_tac*)
+Goal "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A";
+by (bool_tac 1);
+qed "cond_simple_type";
+Addsimps [cond_simple_type];
+
 val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
 by (rewtac rew);
 by (rtac cond_1 1);
@@ -89,10 +97,14 @@
     "[| a:bool;  b:bool |] ==> a or b : bool"
  (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
 
+Addsimps [not_type, and_type, or_type];
+
 qed_goalw "xor_type" Bool.thy [xor_def]
     "[| a:bool;  b:bool |] ==> a xor b : bool"
  (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
 
+Addsimps [xor_type];
+
 val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
                        or_type, xor_type];
 
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Datatype.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -7,63 +7,41 @@
 *)
 
 
-(*For most datatypes involving univ*)
-val datatype_intrs = 
-    [SigmaI, InlI, InrI,
-     Pair_in_univ, Inl_in_univ, Inr_in_univ, 
-     zero_in_univ, A_into_univ, nat_into_univ, UnCI];
-
-(*Needed for mutual recursion*)
-val datatype_elims = [make_elim InlD, make_elim InrD];
+(*Typechecking rules for most datatypes involving univ*)
+structure Data_Arg =
+  struct
+  val intrs = 
+      [SigmaI, InlI, InrI,
+       Pair_in_univ, Inl_in_univ, Inr_in_univ, 
+       zero_in_univ, A_into_univ, nat_into_univ, UnCI];
 
-(*For most codatatypes involving quniv*)
-val codatatype_intrs = 
-    [QSigmaI, QInlI, QInrI,
-     QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
-     zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
-
-val codatatype_elims = [make_elim QInlD, make_elim QInrD];
-
-signature INDUCTIVE_THMS =
-  sig
-  val monos      : thm list             (*monotonicity of each M operator*)
-  val type_intrs : thm list             (*type-checking intro rules*)
-  val type_elims : thm list             (*type-checking elim rules*)
+  (*Needed for mutual recursion*)
+  val elims = [make_elim InlD, make_elim InrD];
   end;
 
-functor Data_section_Fun
- (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
-    : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
-struct
 
-structure Con = Constructor_Fun 
-        (structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
-
-structure Inductive = Ind_section_Fun
-   (open Arg; 
-    val con_defs = Con.con_defs
-    val type_intrs = Arg.type_intrs @ datatype_intrs
-    val type_elims = Arg.type_elims @ datatype_elims);
-
-open Inductive Con
-end;
+structure Data_Package = 
+    Add_datatype_def_Fun
+      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+       and Su=Standard_Sum
+       and Ind_Package = Ind_Package
+       and Datatype_Arg = Data_Arg);
 
 
-functor CoData_section_Fun
- (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
-    : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
-struct
-
-structure Con = Constructor_Fun 
-        (structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
+(*Typechecking rules for most codatatypes involving quniv*)
+structure CoData_Arg =
+  struct
+  val intrs = 
+      [QSigmaI, QInlI, QInrI,
+       QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
+       zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
 
-structure CoInductive = CoInd_section_Fun
-   (open Arg; 
-    val con_defs = Con.con_defs
-    val type_intrs = Arg.type_intrs @ codatatype_intrs
-    val type_elims = Arg.type_elims @ codatatype_elims);
+  val elims = [make_elim QInlD, make_elim QInrD];
+  end;
 
-open CoInductive Con
-end;
+structure CoData_Package = 
+    Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
+                          and Su=Quine_Sum
+			  and Ind_Package = CoInd_Package
+			  and Datatype_Arg = CoData_Arg);
 
-
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Datatype.thy	Mon Dec 28 16:59:28 1998 +0100
@@ -8,7 +8,9 @@
 	"Datatype" must be capital to avoid conflicts with ML's "datatype"
 *)
 
-Datatype = "constructor" + Inductive + Univ + QUniv +
+Datatype = Inductive + Univ + QUniv +
+
+setup setup_datatypes
 
 end
 
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Finite.thy	Mon Dec 28 16:59:28 1998 +0100
@@ -16,7 +16,7 @@
   intrs
     emptyI  "0 : Fin(A)"
     consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
-  type_intrs "[empty_subsetI, cons_subsetI, PowI]"
+  type_intrs empty_subsetI, cons_subsetI, PowI
   type_elims "[make_elim PowD]"
 
 inductive
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Inductive.ML
--- a/src/ZF/Inductive.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Inductive.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -56,35 +56,10 @@
   end;
 
 
-functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
-  : sig include INTR_ELIM INDRULE end =
-let
-  structure Intr_elim = 
-      Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
-                    Pr=Standard_Prod and Su=Standard_Sum);
-
-  structure Indrule = 
-      Indrule_Fun (structure Inductive=Inductive and 
-                   Pr=Standard_Prod and CP=Standard_CP and
-                   Su=Standard_Sum and 
-                   Intr_elim=Intr_elim)
-in 
-   struct 
-   val thy      = Intr_elim.thy
-   val defs     = Intr_elim.defs
-   val bnd_mono = Intr_elim.bnd_mono
-   val dom_subset = Intr_elim.dom_subset
-   val intrs    = Intr_elim.intrs
-   val elim     = Intr_elim.elim
-   val mk_cases = Intr_elim.mk_cases
-   open Indrule 
-   end
-end;
-
-
-structure Ind = Add_inductive_def_Fun
-    (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
-     and Su=Standard_Sum);
+structure Ind_Package = 
+    Add_inductive_def_Fun
+      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+       and Su=Standard_Sum);
 
 
 structure Gfp =
@@ -128,34 +103,7 @@
   end;
 
 
-signature COINDRULE =
-  sig
-  val coinduct : thm
-  end;
-
-
-functor CoInd_section_Fun
- (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
-    : sig include INTR_ELIM COINDRULE end =
-let
-  structure Intr_elim = 
-      Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
-                    Pr=Quine_Prod and CP=Standard_CP and
-                    Su=Quine_Sum);
-in
-   struct
-   val thy      = Intr_elim.thy
-   val defs     = Intr_elim.defs
-   val bnd_mono = Intr_elim.bnd_mono
-   val dom_subset = Intr_elim.dom_subset
-   val intrs    = Intr_elim.intrs
-   val elim     = Intr_elim.elim
-   val mk_cases = Intr_elim.mk_cases
-   val coinduct = Intr_elim.raw_induct
-   end
-end;
-
-structure CoInd = 
+structure CoInd_Package = 
     Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
                           and Su=Quine_Sum);
 
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Inductive.thy
--- a/src/ZF/Inductive.thy	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Inductive.thy	Mon Dec 28 16:59:28 1998 +0100
@@ -1,5 +1,5 @@
 (*Dummy theory to document dependencies *)
 
-Inductive = Fixedpt + Sum + QPair + "indrule" +
+Inductive = Fixedpt + Sum + QPair + 
 
 end
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/InfDatatype.ML
--- a/src/ZF/InfDatatype.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/InfDatatype.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -97,4 +97,4 @@
     [InfCard_nat, InfCard_nat_Un_cardinal,
      Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, 
      zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc,
-     Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ datatype_intrs;
+     Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ Data_Arg.intrs;
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/IsaMakefile	Mon Dec 28 16:59:28 1998 +0100
@@ -38,12 +38,12 @@
   Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \
   Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy \
   Update.ML Update.thy Univ.ML Univ.thy WF.ML WF.thy \
-  ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \
-  cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \
+  ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML \
   domrange.thy equalities.ML equalities.thy func.ML func.thy \
-  ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \
-  intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
-  subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy \
+  ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
+  subset.thy thy_syntax.ML upair.ML upair.thy \
+  Tools/cartprod.ML Tools/datatype_package.ML Tools/inductive_package.ML \
+  Tools/primrec_package.ML Tools/typechk.ML \
   Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \
   Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy 
 	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
@@ -96,7 +96,7 @@
   Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
   Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
   Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
-  Resid/SubUnion.ML Resid/SubUnion.thy Resid/Substitution.ML \
+  Resid/Substitution.ML \
   Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
 	@$(ISATOOL) usedir $(OUT)/ZF Resid
 
@@ -111,6 +111,7 @@
   ex/Enum.thy ex/LList.ML ex/LList.thy \
   ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
   ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
+  ex/Primrec_defs.ML ex/Primrec_defs.thy \
   ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
   ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
   ex/Term.ML ex/Term.thy ex/misc.ML
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/List.ML
--- a/src/ZF/List.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/List.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -6,13 +6,8 @@
 Datatype definition of Lists
 *)
 
-open List;
-
 (*** Aspects of the datatype definition ***)
 
-Addsimps list.case_eqns;
-
-
 (*An elimination rule, for type-checking*)
 val ConsE = list.mk_cases list.con_defs "Cons(a,l) : list(A)";
 
@@ -61,39 +56,12 @@
 \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))  \
 \    |] ==> list_case(c,h,l) : C(l)";
 by (rtac (major RS list.induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps list.case_eqns @ prems)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
 qed "list_case_type";
 
 
-(** For recursion **)
-
-Goalw list.con_defs "rank(a) < rank(Cons(a,l))";
-by (simp_tac rank_ss 1);
-qed "rank_Cons1";
-
-Goalw list.con_defs "rank(l) < rank(Cons(a,l))";
-by (simp_tac rank_ss 1);
-qed "rank_Cons2";
-
-
 (*** List functions ***)
 
-(** hd and tl **)
-
-Goalw [hd_def] "hd(Cons(a,l)) = a";
-by (resolve_tac list.case_eqns 1);
-qed "hd_Cons";
-
-Goalw [tl_def] "tl(Nil) = Nil";
-by (resolve_tac list.case_eqns 1);
-qed "tl_Nil";
-
-Goalw [tl_def] "tl(Cons(a,l)) = l";
-by (resolve_tac list.case_eqns 1);
-qed "tl_Cons";
-
-Addsimps [hd_Cons, tl_Nil, tl_Cons];
-
 Goal "l: list(A) ==> tl(l) : list(A)";
 by (etac list.elim 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs)));
@@ -126,52 +94,21 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type])));
 qed "drop_type";
 
-(** list_rec -- by Vset recursion **)
-
-Goal "list_rec(Nil,c,h) = c";
-by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (simpset() addsimps list.case_eqns) 1);
-qed "list_rec_Nil";
 
-Goal "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
-by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps rank_Cons2::list.case_eqns) 1);
-qed "list_rec_Cons";
+(** Type checking -- proved by induction, as usual **)
 
-Addsimps [list_rec_Nil, list_rec_Cons];
-
-
-(*Type checking -- proved by induction, as usual*)
 val prems = Goal
     "[| l: list(A);    \
 \       c: C(Nil);       \
 \       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
-\    |] ==> list_rec(l,c,h) : C(l)";
+\    |] ==> list_rec(c,h,l) : C(l)";
 by (list_ind_tac "l" prems 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
 qed "list_rec_type";
 
-(** Versions for use with definitions **)
-
-val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
-by (rewtac rew);
-by (rtac list_rec_Nil 1);
-qed "def_list_rec_Nil";
-
-val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
-by (rewtac rew);
-by (rtac list_rec_Cons 1);
-qed "def_list_rec_Cons";
-
-fun list_recs def = map standard
-        ([def] RL [def_list_rec_Nil, def_list_rec_Cons]);
-
 (** map **)
 
-val [map_Nil,map_Cons] = list_recs map_def;
-Addsimps [map_Nil, map_Cons];
-
-val prems = Goalw [map_def] 
+val prems = Goalw [get_def thy "map_list"] 
     "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
 by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
 qed "map_type";
@@ -183,30 +120,21 @@
 
 (** length **)
 
-val [length_Nil,length_Cons] = list_recs length_def;
-Addsimps [length_Nil,length_Cons];
-
-Goalw [length_def] 
+Goalw [get_def thy "length_list"] 
     "l: list(A) ==> length(l) : nat";
 by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
 qed "length_type";
 
 (** app **)
 
-val [app_Nil,app_Cons] = list_recs app_def;
-Addsimps [app_Nil, app_Cons];
-
-Goalw [app_def] 
+Goalw [get_def thy "op @_list"] 
     "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
 by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
 qed "app_type";
 
 (** rev **)
 
-val [rev_Nil,rev_Cons] = list_recs rev_def;
-Addsimps [rev_Nil,rev_Cons] ;
-
-Goalw [rev_def] 
+Goalw [get_def thy "rev_list"] 
     "xs: list(A) ==> rev(xs) : list(A)";
 by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
 qed "rev_type";
@@ -214,10 +142,7 @@
 
 (** flat **)
 
-val [flat_Nil,flat_Cons] = list_recs flat_def;
-Addsimps [flat_Nil,flat_Cons];
-
-Goalw [flat_def] 
+Goalw [get_def thy "flat_list"] 
     "ls: list(list(A)) ==> flat(ls) : list(A)";
 by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
 qed "flat_type";
@@ -225,10 +150,7 @@
 
 (** set_of_list **)
 
-val [set_of_list_Nil,set_of_list_Cons] = list_recs set_of_list_def;
-Addsimps [set_of_list_Nil,set_of_list_Cons];
-
-Goalw [set_of_list_def] 
+Goalw [get_def thy "set_of_list_list"] 
     "l: list(A) ==> set_of_list(l) : Pow(A)";
 by (etac list_rec_type 1);
 by (ALLGOALS (Blast_tac));
@@ -243,10 +165,7 @@
 
 (** list_add **)
 
-val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
-Addsimps [list_add_Nil,list_add_Cons];
-
-Goalw [list_add_def] 
+Goalw [get_def thy "list_add_list"] 
     "xs: list(nat) ==> list_add(xs) : nat";
 by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
 qed "list_add_type";
@@ -256,6 +175,8 @@
     [list_rec_type, map_type, map_type2, app_type, length_type, 
      rev_type, flat_type, list_add_type];
 
+Addsimps list_typechecks;
+
 simpset_ref() := simpset() setSolver (type_auto_tac list_typechecks);
 
 
@@ -282,8 +203,8 @@
 qed "map_flat";
 
 Goal "l: list(A) ==> \
-\    list_rec(map(h,l), c, d) = \
-\    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
+\    list_rec(c, d, map(h,l)) = \
+\    list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)";
 by (list_ind_tac "l" [] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "list_rec_map";
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/List.thy
--- a/src/ZF/List.thy	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/List.thy	Mon Dec 28 16:59:28 1998 +0100
@@ -29,42 +29,54 @@
   "[]"          == "Nil"
 
 
-constdefs
+consts
+  length :: i=>i
   hd      :: i=>i
-  "hd(l)       == list_case(0, %x xs. x, l)"
+  tl      :: i=>i
+  map        :: [i=>i, i] => i
+  set_of_list :: i=>i
+  "@"        :: [i,i]=>i                        (infixr 60)
+  rev :: i=>i
+  flat       :: i=>i
+  list_add   :: i=>i
+
+primrec
+  "length([]) = 0"
+  "length(Cons(a,l)) = succ(length(l))"
   
-  tl      :: i=>i
-  "tl(l)       == list_case(Nil, %x xs. xs, l)"
+primrec
+  "hd(Cons(a,l)) = a"
+
+primrec
+  "tl([]) = []"
+  "tl(Cons(a,l)) = l"
+
+primrec
+  "map(f,[]) = []"
+  "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
+ 
+primrec
+  "set_of_list([]) = 0"
+  "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
+   
+primrec
+  "[] @ ys = ys"
+  "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
   
+primrec
+  "rev([]) = []"
+  "rev(Cons(a,l)) = rev(l) @ [a]"
+
+primrec
+  "flat([]) = []"
+  "flat(Cons(l,ls)) = l @ flat(ls)"
+   
+primrec
+  "list_add([]) = 0"
+  "list_add(Cons(a,l)) = a #+ list_add(l)"
+       
+constdefs
   drop       :: [i,i]=>i
   "drop(i,l)   == rec(i, l, %j r. tl(r))"
 
-  list_rec   :: [i, i, [i,i,i]=>i] => i
-  "list_rec(l,c,h) == Vrec(l, %l g. list_case(c, %x xs. h(x, xs, g`xs), l))"
-
-  map        :: [i=>i, i] => i
-  "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
-
-  length :: i=>i
-  "length(l)   == list_rec(l,  0,  %x xs r. succ(r))"
-
-  set_of_list :: i=>i
-  "set_of_list(l)   == list_rec(l,  0,  %x xs r. cons(x,r))"
-
-consts  (*Cannot use constdefs because @ is not an identifier*)
-  "@"        :: [i,i]=>i                        (infixr 60)
-defs
-  app_def       "xs@ys       == list_rec(xs, ys, %x xs r. Cons(x,r))"
-
-
-constdefs
-  rev :: i=>i
-  "rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"
-
-  flat       :: i=>i
-  "flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"
-
-  list_add   :: i=>i
-  "list_add(l) == list_rec(l, 0,  %x xs r. x#+r)"
-
 end
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Perm.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -71,7 +71,7 @@
 
 Goal "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)";
 by (asm_simp_tac (simpset() addsimps [inj_def]) 1);
-by (deepen_tac (claset() addEs [subst_context RS box_equals]) 0 1);
+by (blast_tac (claset() addIs [subst_context RS box_equals]) 1);
 bind_thm ("f_imp_injective", ballI RSN (2,result()));
 
 val prems = Goal
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/ROOT.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -30,12 +30,22 @@
 print_depth 1;
 
 (*Add user sections for inductive/datatype definitions*)
-use     "$ISABELLE_HOME/src/Pure/section_utils.ML";
-use     "thy_syntax.ML";
+use     "$ISABELLE_HOME/src/Pure/section_utils";
+use     "thy_syntax";
 
 use_thy "Let";
 use_thy "func";
-use     "typechk.ML";
+use     "Tools/typechk";
+use_thy "mono";
+use     "ind_syntax";
+use     "Tools/cartprod";
+use_thy "Fixedpt";
+use     "Tools/inductive_package";
+use_thy "Inductive";
+use_thy "QUniv";
+use "Tools/datatype_package";
+use "Tools/primrec_package";
+use_thy "Datatype";
 use_thy "InfDatatype";
 use_thy "List";
 
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Univ.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -513,6 +513,20 @@
 by (rtac Vrec 1);
 qed "def_Vrec";
 
+(*NOT SUITABLE FOR REWRITING: recursive!*)
+Goalw [Vrecursor_def]
+     "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)";
+by (stac transrec 1);
+by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
+                              VsetI RS beta, le_refl]) 1);
+qed "Vrecursor";
+
+(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
+Goal "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x),  a)";
+by (Asm_simp_tac 1);
+by (rtac Vrecursor 1);
+qed "def_Vrecursor";
+
 
 (*** univ(A) ***)
 
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Univ.thy	Mon Dec 28 16:59:28 1998 +0100
@@ -19,6 +19,7 @@
     Vfrom       :: [i,i]=>i
     Vset        :: i=>i
     Vrec        :: [i, [i,i]=>i] =>i
+    Vrecursor   :: [[i,i]=>i, i] =>i
     univ        :: i=>i
 
 translations
@@ -33,6 +34,10 @@
         "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
                              H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
 
+    Vrecursor_def
+        "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
+                                    H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
+
     univ_def    "univ(A) == Vfrom(A,nat)"
 
 end
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Zorn.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -9,8 +9,6 @@
     Classical Theorems of Set Theory. 
 *)
 
-open Zorn;
-
 (*** Section 1.  Mathematical Preamble ***)
 
 Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Zorn.thy	Mon Dec 28 16:59:28 1998 +0100
@@ -15,13 +15,11 @@
 
 consts
   Subset_rel      :: i=>i
-  increasing      :: i=>i
   chain, maxchain :: i=>i
   super           :: [i,i]=>i
 
 defs
   Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
-  increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
 
   chain_def      "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
   super_def      "super(A,c)    == {d: chain(A). c<=d & c~=d}"
@@ -44,8 +42,8 @@
 
     Pow_UnionI  "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
 
-  monos         "[Pow_mono]"
-  con_defs      "[increasing_def]"
+  monos         Pow_mono
+  con_defs      increasing_def
   type_intrs    "[CollectD1 RS apply_funtype, Union_in_Pow]"
   
 end
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,270 +0,0 @@
-(*  Title:      ZF/add_ind_def.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Fixedpoint definition module -- for Inductive/Coinductive Definitions
-
-Features:
-* least or greatest fixedpoints
-* user-specified product and sum constructions
-* mutually recursive definitions
-* definitions involving arbitrary monotone operators
-* automatically proves introduction and elimination rules
-
-The recursive sets must *already* be declared as constants in parent theory!
-
-  Introduction rules have the form
-  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
-  where M is some monotone operator (usually the identity)
-  P(x) is any (non-conjunctive) side condition on the free variables
-  ti, t are any terms
-  Sj, Sk are two of the sets being defined in mutual recursion
-
-Sums are used only for mutual recursion;
-Products are used only to derive "streamlined" induction rules for relations
-*)
-
-signature FP =          (** Description of a fixed point operator **)
-  sig
-  val oper      : term                  (*fixed point operator*)
-  val bnd_mono  : term                  (*monotonicity predicate*)
-  val bnd_monoI : thm                   (*intro rule for bnd_mono*)
-  val subs      : thm                   (*subset theorem for fp*)
-  val Tarski    : thm                   (*Tarski's fixed point theorem*)
-  val induct    : thm                   (*induction/coinduction rule*)
-  end;
-
-signature SU =                  (** Description of a disjoint sum **)
-  sig
-  val sum       : term                  (*disjoint sum operator*)
-  val inl       : term                  (*left injection*)
-  val inr       : term                  (*right injection*)
-  val elim      : term                  (*case operator*)
-  val case_inl  : thm                   (*inl equality rule for case*)
-  val case_inr  : thm                   (*inr equality rule for case*)
-  val inl_iff   : thm                   (*injectivity of inl, using <->*)
-  val inr_iff   : thm                   (*injectivity of inr, using <->*)
-  val distinct  : thm                   (*distinctness of inl, inr using <->*)
-  val distinct' : thm                   (*distinctness of inr, inl using <->*)
-  val free_SEs  : thm list              (*elim rules for SU, and pair_iff!*)
-  end;
-
-signature ADD_INDUCTIVE_DEF =
-  sig 
-  val add_fp_def_i : term list * term * term list -> theory -> theory
-  val add_constructs_def :
-        string list * ((string*typ*mixfix) * 
-                       string * term list * term list) list list ->
-        theory -> theory
-  end;
-
-
-
-(*Declares functions to add fixedpoint/constructor defs to a theory*)
-functor Add_inductive_def_Fun 
-    (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU)
-    : ADD_INDUCTIVE_DEF =
-struct
-open Logic Ind_Syntax;
-
-(*internal version*)
-fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
-  let
-    val dummy = (*has essential ancestors?*)
-	Theory.requires thy "Inductive" "(co)inductive definitions" 
-
-    val sign = sign_of thy;
-
-    (*recT and rec_params should agree for all mutually recursive components*)
-    val rec_hds = map head_of rec_tms;
-
-    val dummy = assert_all is_Const rec_hds
-            (fn t => "Recursive set not previously declared as constant: " ^ 
-                     Sign.string_of_term sign t);
-
-    (*Now we know they are all Consts, so get their names, type and params*)
-    val rec_names = map (#1 o dest_Const) rec_hds
-    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
-
-    val rec_base_names = map Sign.base_name rec_names;
-    val dummy = assert_all Syntax.is_identifier rec_base_names
-      (fn a => "Base name of recursive set not an identifier: " ^ a);
-
-    local (*Checking the introduction rules*)
-      val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
-      fun intr_ok set =
-          case head_of set of Const(a,recT) => a mem rec_names | _ => false;
-    in
-      val dummy =  assert_all intr_ok intr_sets
-         (fn t => "Conclusion of rule does not name a recursive set: " ^ 
-                  Sign.string_of_term sign t);
-    end;
-
-    val dummy = assert_all is_Free rec_params
-        (fn t => "Param in recursion term not a free variable: " ^
-                 Sign.string_of_term sign t);
-
-    (*** Construct the lfp definition ***)
-    val mk_variant = variant (foldr add_term_names (intr_tms,[]));
-
-    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
-
-    fun dest_tprop (Const("Trueprop",_) $ P) = P
-      | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
-                              Sign.string_of_term sign Q);
-
-    (*Makes a disjunct from an introduction rule*)
-    fun lfp_part intr = (*quantify over rule's free vars except parameters*)
-      let val prems = map dest_tprop (strip_imp_prems intr)
-          val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
-          val exfrees = term_frees intr \\ rec_params
-          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
-      in foldr FOLogic.mk_exists
-	       (exfrees, fold_bal (app FOLogic.conj) (zeq::prems)) 
-      end;
-
-    (*The Part(A,h) terms -- compose injections to make h*)
-    fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
-      | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
-
-    (*Access to balanced disjoint sums via injections*)
-    val parts = 
-        map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
-                                  (length rec_tms));
-
-    (*replace each set by the corresponding Part(A,h)*)
-    val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
-
-    val lfp_abs = absfree(X', iT, 
-                     mk_Collect(z', dom_sum, 
-				fold_bal (app FOLogic.disj) part_intrs));
-
-    val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
-
-    val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
-                               "Illegal occurrence of recursion operator")
-             rec_hds;
-
-    (*** Make the new theory ***)
-
-    (*A key definition:
-      If no mutual recursion then it equals the one recursive set.
-      If mutual recursion then it differs from all the recursive sets. *)
-    val big_rec_base_name = space_implode "_" rec_base_names;
-    val big_rec_name = Sign.intern_const sign big_rec_base_name;
-
-    (*Big_rec... is the union of the mutually recursive sets*)
-    val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
-
-    (*The individual sets must already be declared*)
-    val axpairs = map Logic.mk_defpair 
-          ((big_rec_tm, lfp_rhs) ::
-           (case parts of 
-               [_] => []                        (*no mutual recursion*)
-             | _ => rec_tms ~~          (*define the sets as Parts*)
-                    map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
-
-    (*tracing: print the fixedpoint definition*)
-    val _ = if !Ind_Syntax.trace then
-		seq (writeln o Sign.string_of_term sign o #2) axpairs
-            else ()
-
-  in  thy |> PureThy.add_defs_i (map Attribute.none axpairs)  end
-
-
-(*Expects the recursive sets to have been defined already.
-  con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
-fun add_constructs_def (rec_base_names, con_ty_lists) thy = 
-  let
-    val dummy = (*has essential ancestors?*)
-      Theory.requires thy "Datatype" "(co)datatype definitions";
-
-    val sign = sign_of thy;
-    val full_name = Sign.full_name sign;
-
-    val dummy = writeln"  Defining the constructor functions...";
-    val case_name = "f";                (*name for case variables*)
-
-
-    (** Define the constructors **)
-
-    (*The empty tuple is 0*)
-    fun mk_tuple [] = Const("0",iT)
-      | mk_tuple args = foldr1 (app Pr.pair) args;
-
-    fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
-
-    val npart = length rec_base_names;       (*total # of mutually recursive parts*)
-
-    (*Make constructor definition; kpart is # of this mutually recursive part*)
-    fun mk_con_defs (kpart, con_ty_list) = 
-      let val ncon = length con_ty_list    (*number of constructors*)
-          fun mk_def (((id,T,syn), name, args, prems), kcon) =
-                (*kcon is index of constructor*)
-              mk_defpair (list_comb (Const (full_name name, T), args),
-                          mk_inject npart kpart
-                          (mk_inject ncon kcon (mk_tuple args)))
-      in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
-
-    (** Define the case operator **)
-
-    (*Combine split terms using case; yields the case operator for one part*)
-    fun call_case case_list = 
-      let fun call_f (free,[]) = Abs("null", iT, free)
-            | call_f (free,args) =
-                  CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
-                              Ind_Syntax.iT 
-                              free 
-      in  fold_bal (app Su.elim) (map call_f case_list)  end;
-
-    (** Generating function variables for the case definition
-        Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
-
-    (*Treatment of a single constructor*)
-    fun add_case (((_, T, _), name, args, prems), (opno, cases)) =
-      if Syntax.is_identifier name then
-        (opno, (Free (case_name ^ "_" ^ name, T), args) :: cases)
-      else
-        (opno + 1, (Free (case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases);
-
-    (*Treatment of a list of constructors, for one part*)
-    fun add_case_list (con_ty_list, (opno, case_lists)) =
-      let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))
-      in (opno', case_list :: case_lists) end;
-
-    (*Treatment of all parts*)
-    val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
-
-    val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
-
-    val big_rec_base_name = space_implode "_" rec_base_names;
-    val big_case_base_name = big_rec_base_name ^ "_case";
-    val big_case_name = full_name big_case_base_name;
-
-    (*The list of all the function variables*)
-    val big_case_args = flat (map (map #1) case_lists);
-
-    val big_case_tm =
-      list_comb (Const (big_case_name, big_case_typ), big_case_args); 
-
-    val big_case_def = mk_defpair
-      (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));
-
-
-    (* Build the new theory *)
-
-    val const_decs =
-      (big_case_base_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
-
-    val axpairs =
-      big_case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists));
-
-  in
-    thy
-    |> Theory.add_consts_i const_decs
-    |> PureThy.add_defs_i (map Attribute.none axpairs)
-  end;
-
-
-end;
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/add_ind_def.thy
--- a/src/ZF/add_ind_def.thy	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-add_ind_def = Fixedpt + "ind_syntax" + "cartprod"
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/cartprod.ML
--- a/src/ZF/cartprod.ML	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-(*  Title:      ZF/cartprod.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1996  University of Cambridge
-
-Syntactic operations for Cartesian Products
-*)
-
-signature PR =                  (** Description of a Cartesian product **)
-  sig
-  val sigma     : term                  (*Cartesian product operator*)
-  val pair      : term                  (*pairing operator*)
-  val split_name : string               (*name of polymorphic split*)
-  val pair_iff  : thm                   (*injectivity of pairing, using <->*)
-  val split_eq  : thm                   (*equality rule for split*)
-  val fsplitI   : thm                   (*intro rule for fsplit*)
-  val fsplitD   : thm                   (*destruct rule for fsplit*)
-  val fsplitE   : thm                   (*elim rule; apparently never used*)
-  end;
-
-signature CARTPROD =            (** Derived syntactic functions for produts **)
-  sig
-  val ap_split : typ -> typ -> term -> term
-  val factors : typ -> typ list
-  val mk_prod : typ * typ -> typ
-  val mk_tuple : term -> typ -> term list -> term
-  val pseudo_type : term -> typ
-  val remove_split : thm -> thm
-  val split_const : typ -> term
-  val split_rule_var : term * typ * thm -> thm
-  end;
-
-
-functor CartProd_Fun (Pr: PR) : CARTPROD =
-struct
-
-(* Some of these functions expect "pseudo-types" containing products,
-   as in HOL; the true ZF types would just be "i" *)
-
-fun mk_prod (T1,T2) = Type("*", [T1,T2]);
-
-(*Bogus product type underlying a (possibly nested) Sigma.  
-  Lets us share HOL code*)
-fun pseudo_type (t $ A $ Abs(_,_,B)) = 
-        if t = Pr.sigma  then  mk_prod(pseudo_type A, pseudo_type B)
-                         else  Ind_Syntax.iT
-  | pseudo_type _           =  Ind_Syntax.iT;
-
-(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
-fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
-  | factors T                    = [T];
-
-(*Make a well-typed instance of "split"*)
-fun split_const T = Const(Pr.split_name, 
-                          [[Ind_Syntax.iT, Ind_Syntax.iT]--->T, 
-                           Ind_Syntax.iT] ---> T);
-
-(*In ap_split S T u, term u expects separate arguments for the factors of S,
-  with result type T.  The call creates a new term expecting one argument
-  of type S.*)
-fun ap_split (Type("*", [T1,T2])) T3 u   = 
-       split_const T3 $ 
-       Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
-           ap_split T2 T3
-           ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
-            Bound 0))
-  | ap_split T T3 u = u;
-
-(*Makes a nested tuple from a list, following the product type structure*)
-fun mk_tuple pair (Type("*", [T1,T2])) tms = 
-        pair $ (mk_tuple pair T1 tms)
-             $ (mk_tuple pair T2 (drop (length (factors T1), tms)))
-  | mk_tuple pair T (t::_) = t;
-
-(*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [Pr.split_eq];
-
-(*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
-fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
-      let val T' = factors T1 ---> T2
-          val newt = ap_split T1 T2 (Var(v,T'))
-          val cterm = Thm.cterm_of (#sign(rep_thm rl))
-      in
-          remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
-                                           cterm newt)]) rl)
-      end
-  | split_rule_var (t,T,rl) = rl;
-
-end;
-
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/cartprod.thy
--- a/src/ZF/cartprod.thy	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-cartprod = "ind_syntax"
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/constructor.ML
--- a/src/ZF/constructor.ML	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-(*  Title:      ZF/constructor.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Constructor function module -- for (Co)Datatype Definitions
-*)
-
-signature CONSTRUCTOR_ARG =
-  sig
-  val thy          : theory             (*parent containing constructor defs*)
-  val big_rec_name : string             (*name of mutually recursive set*)
-  val con_ty_lists : ((string*typ*mixfix) * 
-                      string * term list * term list) list list
-                                        (*description of constructors*)
-  end;
-
-signature CONSTRUCTOR_RESULT =
-  sig
-  val con_defs   : thm list             (*definitions made in thy*)
-  val case_eqns  : thm list             (*equations for case operator*)
-  val free_iffs  : thm list             (*freeness rewrite rules*)
-  val free_SEs   : thm list             (*freeness destruct rules*)
-  val mk_free    : string -> thm        (*makes freeness theorems*)
-  end;
-
-
-(*Proves theorems relating to constructors*)
-functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
-                      Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
-let
-
-(*1st element is the case definition; others are the constructors*)
-val big_case_name = Const.big_rec_name ^ "_case";
-
-val con_defs = get_def Const.thy big_case_name :: 
-               map (get_def Const.thy o #2) (flat Const.con_ty_lists);
-
-(** Prove the case theorem **)
-
-(*Get the case term from its definition*)
-val Const("==",_) $ big_case_tm $ _ =
-    hd con_defs |> rep_thm |> #prop |> Logic.unvarify;
-
-val (_, big_case_args) = strip_comb big_case_tm;
-
-(*Each equation has the form 
-  rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
-fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = 
-  FOLogic.mk_Trueprop
-    (FOLogic.mk_eq
-     (big_case_tm $
-       (list_comb (Const (Sign.intern_const (sign_of Const.thy) name,T), 
-		   args)),
-      list_comb (case_free, args)));
-
-val case_trans = hd con_defs RS Ind_Syntax.def_trans
-and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
-
-(*Proves a single case equation.  Could use simp_tac, but it's slower!*)
-fun case_tacsf con_def _ = 
-  [rewtac con_def,
-   rtac case_trans 1,
-   REPEAT (resolve_tac [refl, split_trans, 
-                        Su.case_inl RS trans, 
-                        Su.case_inr RS trans] 1)];
-
-fun prove_case_equation (arg,con_def) =
-    prove_goalw_cterm [] 
-        (cterm_of (sign_of Const.thy) (mk_case_equation arg))
-        (case_tacsf con_def);
-
-val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
-
-in
-  struct
-  val con_defs = con_defs
-
-  val free_iffs = con_iffs @ 
-    [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
-
-  val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
-
-  (*Typical theorems have the form ~con1=con2, con1=con2==>False,
-    con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
-  fun mk_free s =
-      prove_goalw Const.thy con_defs s
-        (fn prems => [cut_facts_tac prems 1, 
-                      fast_tac (ZF_cs addSEs free_SEs) 1]);
-
-  val case_eqns = map prove_case_equation 
-              (flat Const.con_ty_lists ~~ big_case_args ~~ tl con_defs);
-  end
-end;
-
-
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/constructor.thy
--- a/src/ZF/constructor.thy	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-constructor = "intr_elim"
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/ind_syntax.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -15,6 +15,10 @@
 (*Print tracing messages during processing of "inductive" theory sections*)
 val trace = ref false;
 
+fun traceIt msg ct = 
+    if !trace then (writeln (msg ^ string_of_cterm ct); ct)
+    else ct;
+
 (** Abstract syntax definitions for ZF **)
 
 val iT = Type("i",[]);
@@ -29,6 +33,10 @@
 
 val Part_const = Const("Part", [iT,iT-->iT]--->iT);
 
+val apply_const = Const("op `", [iT,iT]--->iT);
+
+val Vrecursor_const = Const("Vrecursor", [[iT,iT]--->iT, iT]--->iT);
+
 val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
 
@@ -60,6 +68,11 @@
 
 (** For datatype definitions **)
 
+(*Constructor name, type, mixfix info;
+  internal name from mixfix, datatype sets, full premises*)
+type constructor_spec = 
+    ((string * typ * mixfix) * string * term list * term list);
+
 fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
   | dest_mem _ = error "Constructor specifications must have the form x:A";
 
@@ -103,8 +116,8 @@
 
 (*Previously these both did    replicate (length rec_tms);  however now
   [q]univ itself constitutes the sum domain for mutual recursion!*)
-fun data_domain rec_tms = univ $ union_params (hd rec_tms);
-fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms);
+fun data_domain false rec_tms = univ $ union_params (hd rec_tms)
+  | data_domain true  rec_tms = quniv $ union_params (hd rec_tms);
 
 (*Could go to FOL, but it's hardly general*)
 val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
@@ -128,5 +141,3 @@
 
 end;
 
-
-val trace_induct = Ind_Syntax.trace;
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/ind_syntax.thy
--- a/src/ZF/ind_syntax.thy	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-ind_syntax = "mono"
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,276 +0,0 @@
-(*  Title:      ZF/indrule.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Induction rule module -- for Inductive/Coinductive Definitions
-
-Proves a strong induction rule and a mutual induction rule
-*)
-
-signature INDRULE =
-  sig
-  val induct        : thm                       (*main induction rule*)
-  val mutual_induct : thm                       (*mutual induction rule*)
-  end;
-
-
-functor Indrule_Fun
-    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
-     and Pr: PR and CP: CARTPROD and Su : SU and 
-     Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE  =
-let
-
-val sign = sign_of Inductive.thy;
-
-val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms);
-
-val big_rec_name =
-  Sign.intern_const sign (space_implode "_" (map Sign.base_name Intr_elim.rec_names));
-
-val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
-
-val _ = writeln "  Proving the induction rule...";
-
-(*** Prove the main induction rule ***)
-
-val pred_name = "P";            (*name for predicate variables*)
-
-val big_rec_def::part_rec_defs = Intr_elim.defs;
-
-(*Used to make induction rules;
-   ind_alist = [(rec_tm1,pred1),...]  -- associates predicates with rec ops
-   prem is a premise of an intr rule*)
-fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ 
-                 (Const("op :",_)$t$X), iprems) =
-     (case gen_assoc (op aconv) (ind_alist, X) of
-          Some pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
-        | None => (*possibly membership in M(rec_tm), for M monotone*)
-            let fun mk_sb (rec_tm,pred) = 
-                        (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
-            in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
-  | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
-
-(*Make a premise of the induction rule.*)
-fun induct_prem ind_alist intr =
-  let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
-      val iprems = foldr (add_induct_prem ind_alist)
-                         (Logic.strip_imp_prems intr,[])
-      val (t,X) = Ind_Syntax.rule_concl intr
-      val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
-      val concl = FOLogic.mk_Trueprop (pred $ t)
-  in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
-  handle Bind => error"Recursion term not found in conclusion";
-
-(*Minimizes backtracking by delivering the correct premise to each goal.
-  Intro rules with extra Vars in premises still cause some backtracking *)
-fun ind_tac [] 0 = all_tac
-  | ind_tac(prem::prems) i = 
-        DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN
-        ind_tac prems (i-1);
-
-val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
-
-val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
-                    Inductive.intr_tms;
-
-val _ = if !Ind_Syntax.trace then 
-            (writeln "ind_prems = ";
-	     seq (writeln o Sign.string_of_term sign) ind_prems;
-	     writeln "raw_induct = "; print_thm Intr_elim.raw_induct)
-        else ();
-
-
-(*We use a MINIMAL simpset because others (such as FOL_ss) contain too many
-  simplifications.  If the premises get simplified, then the proofs could 
-  fail.  *)
-val min_ss = empty_ss
-      setmksimps (map mk_eq o ZF_atomize o gen_all)
-      setSolver  (fn prems => resolve_tac (triv_rls@prems) 
-                              ORELSE' assume_tac
-                              ORELSE' etac FalseE);
-
-val quant_induct = 
-    prove_goalw_cterm part_rec_defs 
-      (cterm_of sign 
-       (Logic.list_implies (ind_prems, 
-                FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))
-      (fn prems =>
-       [rtac (impI RS allI) 1,
-        DETERM (etac Intr_elim.raw_induct 1),
-        (*Push Part inside Collect*)
-        full_simp_tac (min_ss addsimps [Part_Collect]) 1,
-        (*This CollectE and disjE separates out the introduction rules*)
-	REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
-	(*Now break down the individual cases.  No disjE here in case
-          some premise involves disjunction.*)
-        REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE] 
-                           ORELSE' hyp_subst_tac)),
-        ind_tac (rev prems) (length prems) ]);
-
-val _ = if !Ind_Syntax.trace then 
-            (writeln "quant_induct = "; print_thm quant_induct)
-        else ();
-
-
-(*** Prove the simultaneous induction rule ***)
-
-(*Make distinct predicates for each inductive set*)
-
-(*The components of the element type, several if it is a product*)
-val elem_type = CP.pseudo_type Inductive.dom_sum;
-val elem_factors = CP.factors elem_type;
-val elem_frees = mk_frees "za" elem_factors;
-val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees;
-
-(*Given a recursive set and its domain, return the "fsplit" predicate
-  and a conclusion for the simultaneous induction rule.
-  NOTE.  This will not work for mutually recursive predicates.  Previously
-  a summand 'domt' was also an argument, but this required the domain of
-  mutual recursion to invariably be a disjoint sum.*)
-fun mk_predpair rec_tm = 
-  let val rec_name = (#1 o dest_Const o head_of) rec_tm
-      val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
-                       elem_factors ---> FOLogic.oT)
-      val qconcl = 
-        foldr FOLogic.mk_all
-          (elem_frees, 
-           FOLogic.imp $ 
-           (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
-                 $ (list_comb (pfree, elem_frees)))
-  in  (CP.ap_split elem_type FOLogic.oT pfree, 
-       qconcl)  
-  end;
-
-val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
-
-(*Used to form simultaneous induction lemma*)
-fun mk_rec_imp (rec_tm,pred) = 
-    FOLogic.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $ 
-                     (pred $ Bound 0);
-
-(*To instantiate the main induction rule*)
-val induct_concl = 
-    FOLogic.mk_Trueprop
-      (Ind_Syntax.mk_all_imp
-       (big_rec_tm,
-        Abs("z", Ind_Syntax.iT, 
-            fold_bal (app FOLogic.conj) 
-            (ListPair.map mk_rec_imp (Inductive.rec_tms,preds)))))
-and mutual_induct_concl =
- FOLogic.mk_Trueprop(fold_bal (app FOLogic.conj) qconcls);
-
-val _ = if !Ind_Syntax.trace then 
-            (writeln ("induct_concl = " ^
-		      Sign.string_of_term sign induct_concl);
-             writeln ("mutual_induct_concl = " ^
-		      Sign.string_of_term sign mutual_induct_concl))
-        else ();
-
-
-val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
-                        resolve_tac [allI, impI, conjI, Part_eqI],
-                        dresolve_tac [spec, mp, Pr.fsplitD]];
-
-val need_mutual = length Intr_elim.rec_names > 1;
-
-val lemma = (*makes the link between the two induction rules*)
-  if need_mutual then
-     (writeln "  Proving the mutual induction rule...";
-      prove_goalw_cterm part_rec_defs 
-	    (cterm_of sign (Logic.mk_implies (induct_concl,
-					      mutual_induct_concl)))
-	    (fn prems =>
-	     [cut_facts_tac prems 1, 
-	      REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
-		      lemma_tac 1)]))
-  else (writeln "  [ No mutual induction rule needed ]";
-        TrueI);
-
-val _ = if !Ind_Syntax.trace then 
-            (writeln "lemma = "; print_thm lemma)
-        else ();
-
-
-(*Mutual induction follows by freeness of Inl/Inr.*)
-
-(*Simplification largely reduces the mutual induction rule to the 
-  standard rule*)
-val mut_ss = 
-    min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
-
-val all_defs = Inductive.con_defs @ part_rec_defs;
-
-(*Removes Collects caused by M-operators in the intro rules.  It is very
-  hard to simplify
-    list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))}) 
-  where t==Part(tf,Inl) and f==Part(tf,Inr) to  list({v: tf. P_t(v)}).
-  Instead the following rules extract the relevant conjunct.
-*)
-val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos
-              RLN (2,[rev_subsetD]);
-
-(*Minimizes backtracking by delivering the correct premise to each goal*)
-fun mutual_ind_tac [] 0 = all_tac
-  | mutual_ind_tac(prem::prems) i = 
-      DETERM
-       (SELECT_GOAL 
-          (
-           (*Simplify the assumptions and goal by unfolding Part and
-             using freeness of the Sum constructors; proves all but one
-             conjunct by contradiction*)
-           rewrite_goals_tac all_defs  THEN
-           simp_tac (mut_ss addsimps [Part_iff]) 1  THEN
-           IF_UNSOLVED (*simp_tac may have finished it off!*)
-             ((*simplify assumptions*)
-              (*some risk of excessive simplification here -- might have
-                to identify the bare minimum set of rewrites*)
-              full_simp_tac 
-                 (mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1
-              THEN
-              (*unpackage and use "prem" in the corresponding place*)
-              REPEAT (rtac impI 1)  THEN
-              rtac (rewrite_rule all_defs prem) 1  THEN
-              (*prem must not be REPEATed below: could loop!*)
-              DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' 
-                                      eresolve_tac (conjE::mp::cmonos))))
-          ) i)
-       THEN mutual_ind_tac prems (i-1);
-
-val mutual_induct_fsplit = 
-  if need_mutual then
-    prove_goalw_cterm []
-          (cterm_of sign
-           (Logic.list_implies 
-              (map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms,
-               mutual_induct_concl)))
-          (fn prems =>
-           [rtac (quant_induct RS lemma) 1,
-            mutual_ind_tac (rev prems) (length prems)])
-  else TrueI;
-
-(** Uncurrying the predicate in the ordinary induction rule **)
-
-(*instantiate the variable to a tuple, if it is non-trivial, in order to
-  allow the predicate to be "opened up".
-  The name "x.1" comes from the "RS spec" !*)
-val inst = 
-    case elem_frees of [_] => I
-       | _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)), 
-                                 cterm_of sign elem_tuple)]);
-
-(*strip quantifier and the implication*)
-val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
-
-val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0
-
-in
-  struct
-  (*strip quantifier*)
-  val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0) 
-               |> standard;
-
-  (*Just "True" unless there's true mutual recursion.  This saves storage.*)
-  val mutual_induct = CP.remove_split mutual_induct_fsplit
-  end
-end;
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/indrule.thy
--- a/src/ZF/indrule.thy	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-indrule = "ind_syntax" + "cartprod" + "intr_elim"
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,165 +0,0 @@
-(*  Title:      ZF/intr_elim.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Introduction/elimination rule module -- for Inductive/Coinductive Definitions
-*)
-
-signature INDUCTIVE_ARG =       (** Description of a (co)inductive def **)
-  sig
-  val thy        : theory               (*new theory with inductive defs*)
-  val monos      : thm list             (*monotonicity of each M operator*)
-  val con_defs   : thm list             (*definitions of the constructors*)
-  val type_intrs : thm list             (*type-checking intro rules*)
-  val type_elims : thm list             (*type-checking elim rules*)
-  end;
-
-
-signature INDUCTIVE_I =         (** Terms read from the theory section **)
-  sig
-  val rec_tms    : term list            (*the recursive sets*)
-  val dom_sum    : term                 (*their common domain*)
-  val intr_tms   : term list            (*terms for the introduction rules*)
-  end;
-
-signature INTR_ELIM =
-  sig
-  val thy        : theory               (*copy of input theory*)
-  val defs       : thm list             (*definitions made in thy*)
-  val bnd_mono   : thm                  (*monotonicity for the lfp definition*)
-  val dom_subset : thm                  (*inclusion of recursive set in dom*)
-  val intrs      : thm list             (*introduction rules*)
-  val elim       : thm                  (*case analysis theorem*)
-  val mk_cases   : thm list -> string -> thm    (*generates case theorems*)
-  end;
-
-signature INTR_ELIM_AUX =       (** Used to make induction rules **)
-  sig
-  val raw_induct : thm                  (*raw induction rule from Fp.induct*)
-  val rec_names  : string list          (*names of recursive sets*)
-  end;
-
-(*prove intr/elim rules for a fixedpoint definition*)
-functor Intr_elim_Fun
-    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
-     and Fp: FP and Pr : PR and Su : SU) 
-    : sig include INTR_ELIM INTR_ELIM_AUX end =
-let
-
-val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
-val big_rec_base_name = space_implode "_" (map Sign.base_name rec_names);
-
-val _ = deny (big_rec_base_name mem (Sign.stamp_names_of (sign_of Inductive.thy)))
-             ("Definition " ^ big_rec_base_name ^ 
-              " would clash with the theory of the same name!");
-
-(*fetch fp definitions from the theory*)
-val big_rec_def::part_rec_defs = 
-  map (get_def Inductive.thy)
-      (case rec_names of [_] => rec_names | _ => big_rec_base_name::rec_names);
-
-
-val sign = sign_of Inductive.thy;
-
-(********)
-val _ = writeln "  Proving monotonicity...";
-
-val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
-    big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
-
-val bnd_mono = 
-    prove_goalw_cterm [] 
-      (cterm_of sign (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
-      (fn _ =>
-       [rtac (Collect_subset RS bnd_monoI) 1,
-        REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);
-
-val dom_subset = standard (big_rec_def RS Fp.subs);
-
-val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
-
-(********)
-val _ = writeln "  Proving the introduction rules...";
-
-(*Mutual recursion?  Helps to derive subset rules for the individual sets.*)
-val Part_trans =
-    case rec_names of
-         [_] => asm_rl
-       | _   => standard (Part_subset RS subset_trans);
-
-(*To type-check recursive occurrences of the inductive sets, possibly
-  enclosed in some monotonic operator M.*)
-val rec_typechecks = 
-   [dom_subset] RL (asm_rl :: ([Part_trans] RL Inductive.monos)) RL [subsetD];
-
-(*Type-checking is hardest aspect of proof;
-  disjIn selects the correct disjunct after unfolding*)
-fun intro_tacsf disjIn prems = 
-  [(*insert prems and underlying sets*)
-   cut_facts_tac prems 1,
-   DETERM (stac unfold 1),
-   REPEAT (resolve_tac [Part_eqI,CollectI] 1),
-   (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
-   rtac disjIn 2,
-   (*Not ares_tac, since refl must be tried before any equality assumptions;
-     backtracking may occur if the premises have extra variables!*)
-   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2),
-   (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
-   rewrite_goals_tac Inductive.con_defs,
-   REPEAT (rtac refl 2),
-   (*Typechecking; this can fail*)
-   REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
-                      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::
-                                            Inductive.type_elims)
-                      ORELSE' hyp_subst_tac)),
-   DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::Inductive.type_intrs) 1)];
-
-(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
-val mk_disj_rls = 
-    let fun f rl = rl RS disjI1
-        and g rl = rl RS disjI2
-    in  accesses_bal(f, g, asm_rl)  end;
-
-val intrs = ListPair.map (uncurry (prove_goalw_cterm part_rec_defs))
-            (map (cterm_of sign) Inductive.intr_tms,
-             map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
-
-(********)
-val _ = writeln "  Proving the elimination rule...";
-
-(*Breaks down logical connectives in the monotonic function*)
-val basic_elim_tac =
-    REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
-              ORELSE' bound_hyp_subst_tac))
-    THEN prune_params_tac
-        (*Mutual recursion: collapse references to Part(D,h)*)
-    THEN fold_tac part_rec_defs;
-
-in
-  struct
-  val thy = Inductive.thy
-  and defs = big_rec_def :: part_rec_defs
-  and bnd_mono   = bnd_mono
-  and dom_subset = dom_subset
-  and intrs      = intrs;
-
-  val elim = rule_by_tactic basic_elim_tac 
-                  (unfold RS Ind_Syntax.equals_CollectD);
-
-  (*Applies freeness of the given constructors, which *must* be unfolded by
-      the given defs.  Cannot simply use the local con_defs because  
-      con_defs=[] for inference systems. 
-    String s should have the form t:Si where Si is an inductive set*)
-  fun mk_cases defs s = 
-      rule_by_tactic (rewrite_goals_tac defs THEN 
-                      basic_elim_tac THEN
-                      fold_tac defs)
-         (assume_read Inductive.thy s  RS  elim)
-      |> standard;
-
-  val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
-  and rec_names = rec_names
-  end
-end;
-
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/intr_elim.thy
--- a/src/ZF/intr_elim.thy	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-intr_elim = "add_ind_def"
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/mono.ML
--- a/src/ZF/mono.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/mono.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -6,8 +6,6 @@
 Monotonicity of various operations (for lattice properties see subset.ML)
 *)
 
-open mono;
-
 (** Replacement, in its various formulations **)
 
 (*Not easy to express monotonicity in P, since any "bigger" predicate
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/thy_syntax.ML
--- a/src/ZF/thy_syntax.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/thy_syntax.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -9,134 +9,144 @@
 
 local
 
-(*Inductive definitions theory section.   co is either "" or "Co"*)
-fun inductive_decl co =
-  let open ThyParse 
-    fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
-        if Syntax.is_identifier s then "op " ^ s  else "_"
-    fun mk_params ((((((rec_tms, sdom_sum), ipairs), 
+
+open ThyParse;
+
+(*ML identifiers for introduction rules.*)
+fun mk_intr_name suffix s =  
+    if Syntax.is_identifier s then
+	"op " ^ s ^ suffix  (*the "op" cancels any infix status*)
+    else "_";               (*bad name, don't try to bind*)
+
+
+(*For lists of theorems.  Either a string (an ML list expression) or else
+  a list of identifiers.*)
+fun optlist s = 
+    optional (s $$-- 
+	      (string >> strip_quotes
+	       || list1 (name>>strip_quotes) >> mk_list)) 
+    "[]";
+
+
+(*(Co)Inductive definitions theory section."*)
+fun inductive_decl coind =
+  let  
+    fun mk_params ((((((recs, sdom_sum), ipairs), 
                       monos), con_defs), type_intrs), type_elims) =
       let val big_rec_name = space_implode "_" 
-                           (map (scan_to_id o trim) rec_tms)
-          and srec_tms = mk_list rec_tms
+                           (map (scan_to_id o strip_quotes) recs)
+          and srec_tms = mk_list recs
           and sintrs   = mk_big_list (map snd ipairs)
-          val stri_name = big_rec_name ^ "_Intrnl"
+          and inames   = mk_list (map (mk_intr_name "" o fst) ipairs)
       in
-         (";\n\n\
-          \structure " ^ stri_name ^ " =\n\
-          \  struct\n\
-          \  val _ = writeln \"" ^ co ^ 
-                     "Inductive definition " ^ big_rec_name ^ "\"\n\
-          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) "
-                           ^ srec_tms ^ "\n\
-          \  and dom_sum\t= readtm (sign_of thy) Ind_Syntax.iT " ^ sdom_sum ^ "\n\
-          \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
-                           ^ sintrs ^ "\n\
-          \  end;\n\n\
-          \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
-             stri_name ^ ".rec_tms, " ^
-             stri_name ^ ".dom_sum, " ^
-             stri_name ^ ".intr_tms)"
-         ,
-          "structure " ^ big_rec_name ^ " =\n\
-          \ let\n\
-          \  val _ = writeln \"Proofs for " ^ co ^ 
-                     "Inductive definition " ^ big_rec_name ^ "\"\n\
-          \  structure Result = " ^ co ^ "Ind_section_Fun\n\
-          \\t  (open " ^ stri_name ^ "\n\
-          \\t   val thy\t\t= thy\n\
-          \\t   val monos\t\t= " ^ monos ^ "\n\
-          \\t   val con_defs\t\t= " ^ con_defs ^ "\n\
-          \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
-          \\t   val type_elims\t= " ^ type_elims ^ ")\n\
-          \ in\n\
-          \  struct\n\
-          \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
-          \  open Result\n\
-          \  end\n\
-          \ end;\n\n\
-          \structure " ^ stri_name ^ " = struct end;\n\n"
-         )
+	 ";\n\n\
+	 \local\n\
+	 \val (thy, {defs, intrs, elim, mk_cases, \
+		    \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
+	 \  " ^
+	 (if coind then "Co" else "") ^ 
+	 "Ind_Package.add_inductive (" ^  srec_tms ^ ", " ^ sdom_sum ^ ", " ^
+	  sintrs ^ ", " ^ monos ^ ", " ^ con_defs ^ ", " ^ 
+	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
+	 \in\n\
+	 \structure " ^ big_rec_name ^ " =\n\
+	 \struct\n\
+	 \  val defs = defs\n\
+	 \  val bnd_mono = bnd_mono\n\
+	 \  val dom_subset = dom_subset\n\
+	 \  val intrs = intrs\n\
+	 \  val elim = elim\n\
+	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
+	 \  val mutual_induct = mutual_induct\n\
+	 \  val mk_cases = mk_cases\n\
+	 \  val " ^ inames ^ " = intrs\n\
+	 \end;\n\
+	 \val thy = thy;\nend;\n\
+	 \val thy = thy\n"
       end
     val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
     val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
-    fun optstring s = optional (s $$-- string >> trim) "[]"
-  in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
-             -- optstring "type_intrs" -- optstring "type_elims"
+  in domains -- ipairs -- optlist "monos" -- optlist "con_defs"
+             -- optlist "type_intrs" -- optlist "type_elims"
      >> mk_params
   end;
 
 
-(*Datatype definitions theory section.   co is either "" or "Co"*)
-fun datatype_decl co =
-  let open ThyParse 
-      (*generate strings*)
-      fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
-      val mk_data = mk_list o map mk_const o snd
-      val mk_scons = mk_big_list o map mk_data
-      fun mk_intr_name s =  (*the "op" cancels any infix status*)
-          if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_"
-      fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) =
-        let val rec_names = map (scan_to_id o trim o fst) rec_pairs
-            val big_rec_name = space_implode "_" rec_names
-            and srec_tms = mk_list (map fst rec_pairs)
-            and scons    = mk_scons rec_pairs
-            and sdom_sum = 
-                if dom = "" then  (*default domain: univ or quniv*)
-                    "Ind_Syntax." ^ co ^ "data_domain rec_tms"
-                else "readtm (sign_of thy) Ind_Syntax.iT " ^ dom
-            val stri_name = big_rec_name ^ "_Intrnl"
-            val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
-        in
-           (";\n\n\
-            \structure " ^ stri_name ^ " =\n\
-            \  struct\n\
-            \  val _ = writeln \"" ^ co ^ 
-                       "Datatype definition " ^ big_rec_name ^ "\"\n\
-            \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) " ^ srec_tms ^ "\n\
-            \  val dom_sum\t= " ^ sdom_sum ^ "\n\
-            \  and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n" 
-                   ^ scons ^ "\n\
-            \  val intr_tms\t= Ind_Syntax.mk_all_intr_tms (sign_of thy) (rec_tms, con_ty_lists)\n\
-            \  end;\n\n\
-            \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ 
-                 mk_list (map quote rec_names) ^ ", " ^ 
-                 stri_name ^ ".con_ty_lists) \n\
-            \              |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
-               stri_name ^ ".rec_tms, " ^
-               stri_name ^ ".dom_sum, " ^
-               stri_name ^ ".intr_tms)"
-           ,
-            "structure " ^ big_rec_name ^ " =\n\
-            \ let\n\
-            \  val _ = writeln \"Proofs for " ^ co ^ 
-                       "Datatype definition " ^ big_rec_name ^ "\"\n\
-            \  structure Result = " ^ co ^ "Data_section_Fun\n\
-            \\t  (open " ^ stri_name ^ "\n\
-            \\t   val thy\t\t= thy\n\
-            \\t   val big_rec_name\t= Sign.intern_const (sign_of thy) \"" ^ big_rec_name ^ "\"\n\
-            \\t   val monos\t\t= " ^ monos ^ "\n\
-            \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
-            \\t   val type_elims\t= " ^ type_elims ^ ");\n\
-            \ in\n\
-            \  struct\n\
-            \  val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
-            \  open Result\n\
-            \  end\n\
-            \ end;\n\n\
-            \structure " ^ stri_name ^ " = struct end;\n\n"
-           )
-        end
-      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
-      val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
-      val construct = name -- string_list -- opt_mixfix;
-  in optional ("<=" $$-- string) "" --
+(*Datatype definitions theory section.   co is true for codatatypes*)
+fun datatype_decl coind =
+  let
+    (*generate strings*)
+    fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
+    val mk_data = mk_list o map mk_const o snd
+    val mk_scons = mk_big_list o map mk_data
+    fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
+      let val rec_names = map (scan_to_id o strip_quotes o fst) rec_pairs
+	  val big_rec_name = space_implode "_" rec_names
+	  and srec_tms = mk_list (map fst rec_pairs)
+	  and scons    = mk_scons rec_pairs
+	  val con_names = flat (map (map (strip_quotes o #1 o #1) o snd)
+				rec_pairs)
+          val inames = mk_list (map (mk_intr_name "_I") con_names)
+      in
+	 ";\n\n\
+	 \local\n\
+	 \val (thy,\n\
+         \     {defs, intrs, elim, mk_cases, \
+		    \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
+         \     {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\
+	 \  " ^
+	 (if coind then "Co" else "") ^ 
+	 "Data_Package.add_datatype (" ^  sdom ^ ", " ^ srec_tms ^ ", " ^
+	  scons ^ ", " ^ monos ^ ", " ^ 
+	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
+	 \in\n\
+	 \structure " ^ big_rec_name ^ " =\n\
+	 \struct\n\
+	 \  val defs = defs\n\
+	 \  val bnd_mono = bnd_mono\n\
+	 \  val dom_subset = dom_subset\n\
+	 \  val intrs = intrs\n\
+	 \  val elim = elim\n\
+	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
+	 \  val mutual_induct = mutual_induct\n\
+	 \  val mk_cases = mk_cases\n\
+	 \  val con_defs = con_defs\n\
+	 \  val case_eqns = case_eqns\n\
+	 \  val recursor_eqns = recursor_eqns\n\
+	 \  val free_iffs = free_iffs\n\
+	 \  val free_SEs = free_SEs\n\
+	 \  val mk_free = mk_free\n\
+	 \  val " ^ inames ^ " = intrs;\n\
+	 \end;\n\
+	 \val thy = thy;\nend;\n\
+	 \val thy = thy\n"
+      end
+    val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
+    val construct = name -- string_list -- opt_mixfix;
+  in optional ("<=" $$-- string) "\"\"" --
      enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
-     optstring "monos" -- optstring "type_intrs" -- optstring "type_elims"
+     optlist "monos" -- optlist "type_intrs" -- optlist "type_elims"
      >> mk_params
 end;
 
 
+(** primrec **)
+
+fun mk_primrec_decl eqns =
+  let val names = map fst eqns
+  in
+    ";\nval (thy, " ^ mk_list names ^
+    ") = PrimrecPackage.add_primrec " ^
+      mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
+    \val thy = thy\n"
+  end;
+
+(* either names and axioms or just axioms *)
+val primrec_decl = 
+    ((repeat1 ((ident -- string) || (string >> pair "_")))) >> mk_primrec_decl;
+
+
+
 
 (** augment thy syntax **)
 
@@ -146,9 +156,10 @@
  ["inductive", "coinductive", "datatype", "codatatype", "and", "|",
   "<=", "domains", "intrs", "monos", "con_defs", "type_intrs",
   "type_elims"]
- [("inductive", inductive_decl ""),
-  ("coinductive", inductive_decl "Co"),
-  ("datatype", datatype_decl ""),
-  ("codatatype", datatype_decl "Co")];
+ [section "inductive"   "" (inductive_decl false),
+  section "coinductive" "" (inductive_decl true),
+  section "datatype"    "" (datatype_decl false),
+  section "codatatype"  "" (datatype_decl true),
+  section "primrec"     "" primrec_decl];
 
 end;
diff -r 4f093e55beeb -r 8a1059aa01f0 src/ZF/typechk.ML
--- a/src/ZF/typechk.ML	Mon Dec 28 16:58:11 1998 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      ZF/typechk
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Tactics for type checking -- from CTT
-*)
-
-fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
-      not (is_Var (head_of a))
-  | is_rigid_elem _ = false;
-
-(*Try solving a:A by assumption provided a is rigid!*) 
-val test_assume_tac = SUBGOAL(fn (prem,i) =>
-    if is_rigid_elem (Logic.strip_assums_concl prem)
-    then  assume_tac i  else  eq_assume_tac i);
-
-(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
-  match_tac is too strict; would refuse to instantiate ?A*)
-fun typechk_step_tac tyrls =
-    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
-
-fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
-
-val ZF_typechecks =
-    [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
-
-(*Instantiates variables in typing conditions.
-  drawback: does not simplify conjunctions*)
-fun type_auto_tac tyrls hyps = SELECT_GOAL
-    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
-           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
-