new inductive, datatype and primrec packages, etc.
authorpaulson
Mon Dec 28 16:59:28 1998 +0100 (1998-12-28)
changeset 60538a1059aa01f0
parent 6052 4f093e55beeb
child 6054 4a4f6ad607a1
new inductive, datatype and primrec packages, etc.
src/ZF/AC.thy
src/ZF/Bool.ML
src/ZF/Datatype.ML
src/ZF/Datatype.thy
src/ZF/Finite.thy
src/ZF/Inductive.ML
src/ZF/Inductive.thy
src/ZF/InfDatatype.ML
src/ZF/IsaMakefile
src/ZF/List.ML
src/ZF/List.thy
src/ZF/Perm.ML
src/ZF/ROOT.ML
src/ZF/Univ.ML
src/ZF/Univ.thy
src/ZF/Zorn.ML
src/ZF/Zorn.thy
src/ZF/add_ind_def.ML
src/ZF/add_ind_def.thy
src/ZF/cartprod.ML
src/ZF/cartprod.thy
src/ZF/constructor.ML
src/ZF/constructor.thy
src/ZF/ind_syntax.ML
src/ZF/ind_syntax.thy
src/ZF/indrule.ML
src/ZF/indrule.thy
src/ZF/intr_elim.ML
src/ZF/intr_elim.thy
src/ZF/mono.ML
src/ZF/thy_syntax.ML
src/ZF/typechk.ML
     1.1 --- a/src/ZF/AC.thy	Mon Dec 28 16:58:11 1998 +0100
     1.2 +++ b/src/ZF/AC.thy	Mon Dec 28 16:59:28 1998 +0100
     1.3 @@ -9,6 +9,12 @@
     1.4  *)
     1.5  
     1.6  AC = func +
     1.7 +
     1.8 +constdefs
     1.9 +  (*Needs to be visible for Zorn.thy*)
    1.10 +  increasing :: i=>i
    1.11 +    "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
    1.12 +
    1.13  rules
    1.14    AC    "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
    1.15  end
     2.1 --- a/src/ZF/Bool.ML	Mon Dec 28 16:58:11 1998 +0100
     2.2 +++ b/src/ZF/Bool.ML	Mon Dec 28 16:59:28 1998 +0100
     2.3 @@ -24,6 +24,8 @@
     2.4  by (rtac consI1 1);
     2.5  qed "bool_0I";
     2.6  
     2.7 +Addsimps [bool_1I, bool_0I];
     2.8 +
     2.9  Goalw bool_defs "1~=0";
    2.10  by (rtac succ_not_0 1);
    2.11  qed "one_not_0";
    2.12 @@ -54,10 +56,16 @@
    2.13  fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
    2.14  
    2.15  
    2.16 -Goal "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
    2.17 +Goal "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
    2.18  by (bool_tac 1);
    2.19  qed "cond_type";
    2.20  
    2.21 +(*For Simp_tac and Blast_tac*)
    2.22 +Goal "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A";
    2.23 +by (bool_tac 1);
    2.24 +qed "cond_simple_type";
    2.25 +Addsimps [cond_simple_type];
    2.26 +
    2.27  val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
    2.28  by (rewtac rew);
    2.29  by (rtac cond_1 1);
    2.30 @@ -89,10 +97,14 @@
    2.31      "[| a:bool;  b:bool |] ==> a or b : bool"
    2.32   (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
    2.33  
    2.34 +Addsimps [not_type, and_type, or_type];
    2.35 +
    2.36  qed_goalw "xor_type" Bool.thy [xor_def]
    2.37      "[| a:bool;  b:bool |] ==> a xor b : bool"
    2.38   (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
    2.39  
    2.40 +Addsimps [xor_type];
    2.41 +
    2.42  val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
    2.43                         or_type, xor_type];
    2.44  
     3.1 --- a/src/ZF/Datatype.ML	Mon Dec 28 16:58:11 1998 +0100
     3.2 +++ b/src/ZF/Datatype.ML	Mon Dec 28 16:59:28 1998 +0100
     3.3 @@ -7,63 +7,41 @@
     3.4  *)
     3.5  
     3.6  
     3.7 -(*For most datatypes involving univ*)
     3.8 -val datatype_intrs = 
     3.9 -    [SigmaI, InlI, InrI,
    3.10 -     Pair_in_univ, Inl_in_univ, Inr_in_univ, 
    3.11 -     zero_in_univ, A_into_univ, nat_into_univ, UnCI];
    3.12 -
    3.13 -(*Needed for mutual recursion*)
    3.14 -val datatype_elims = [make_elim InlD, make_elim InrD];
    3.15 +(*Typechecking rules for most datatypes involving univ*)
    3.16 +structure Data_Arg =
    3.17 +  struct
    3.18 +  val intrs = 
    3.19 +      [SigmaI, InlI, InrI,
    3.20 +       Pair_in_univ, Inl_in_univ, Inr_in_univ, 
    3.21 +       zero_in_univ, A_into_univ, nat_into_univ, UnCI];
    3.22  
    3.23 -(*For most codatatypes involving quniv*)
    3.24 -val codatatype_intrs = 
    3.25 -    [QSigmaI, QInlI, QInrI,
    3.26 -     QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    3.27 -     zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
    3.28 -
    3.29 -val codatatype_elims = [make_elim QInlD, make_elim QInrD];
    3.30 -
    3.31 -signature INDUCTIVE_THMS =
    3.32 -  sig
    3.33 -  val monos      : thm list             (*monotonicity of each M operator*)
    3.34 -  val type_intrs : thm list             (*type-checking intro rules*)
    3.35 -  val type_elims : thm list             (*type-checking elim rules*)
    3.36 +  (*Needed for mutual recursion*)
    3.37 +  val elims = [make_elim InlD, make_elim InrD];
    3.38    end;
    3.39  
    3.40 -functor Data_section_Fun
    3.41 - (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
    3.42 -    : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
    3.43 -struct
    3.44  
    3.45 -structure Con = Constructor_Fun 
    3.46 -        (structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
    3.47 -
    3.48 -structure Inductive = Ind_section_Fun
    3.49 -   (open Arg; 
    3.50 -    val con_defs = Con.con_defs
    3.51 -    val type_intrs = Arg.type_intrs @ datatype_intrs
    3.52 -    val type_elims = Arg.type_elims @ datatype_elims);
    3.53 -
    3.54 -open Inductive Con
    3.55 -end;
    3.56 +structure Data_Package = 
    3.57 +    Add_datatype_def_Fun
    3.58 +      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    3.59 +       and Su=Standard_Sum
    3.60 +       and Ind_Package = Ind_Package
    3.61 +       and Datatype_Arg = Data_Arg);
    3.62  
    3.63  
    3.64 -functor CoData_section_Fun
    3.65 - (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
    3.66 -    : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
    3.67 -struct
    3.68 -
    3.69 -structure Con = Constructor_Fun 
    3.70 -        (structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
    3.71 +(*Typechecking rules for most codatatypes involving quniv*)
    3.72 +structure CoData_Arg =
    3.73 +  struct
    3.74 +  val intrs = 
    3.75 +      [QSigmaI, QInlI, QInrI,
    3.76 +       QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    3.77 +       zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
    3.78  
    3.79 -structure CoInductive = CoInd_section_Fun
    3.80 -   (open Arg; 
    3.81 -    val con_defs = Con.con_defs
    3.82 -    val type_intrs = Arg.type_intrs @ codatatype_intrs
    3.83 -    val type_elims = Arg.type_elims @ codatatype_elims);
    3.84 +  val elims = [make_elim QInlD, make_elim QInrD];
    3.85 +  end;
    3.86  
    3.87 -open CoInductive Con
    3.88 -end;
    3.89 +structure CoData_Package = 
    3.90 +    Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
    3.91 +                          and Su=Quine_Sum
    3.92 +			  and Ind_Package = CoInd_Package
    3.93 +			  and Datatype_Arg = CoData_Arg);
    3.94  
    3.95 -
     4.1 --- a/src/ZF/Datatype.thy	Mon Dec 28 16:58:11 1998 +0100
     4.2 +++ b/src/ZF/Datatype.thy	Mon Dec 28 16:59:28 1998 +0100
     4.3 @@ -8,7 +8,9 @@
     4.4  	"Datatype" must be capital to avoid conflicts with ML's "datatype"
     4.5  *)
     4.6  
     4.7 -Datatype = "constructor" + Inductive + Univ + QUniv +
     4.8 +Datatype = Inductive + Univ + QUniv +
     4.9 +
    4.10 +setup setup_datatypes
    4.11  
    4.12  end
    4.13  
     5.1 --- a/src/ZF/Finite.thy	Mon Dec 28 16:58:11 1998 +0100
     5.2 +++ b/src/ZF/Finite.thy	Mon Dec 28 16:59:28 1998 +0100
     5.3 @@ -16,7 +16,7 @@
     5.4    intrs
     5.5      emptyI  "0 : Fin(A)"
     5.6      consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
     5.7 -  type_intrs "[empty_subsetI, cons_subsetI, PowI]"
     5.8 +  type_intrs empty_subsetI, cons_subsetI, PowI
     5.9    type_elims "[make_elim PowD]"
    5.10  
    5.11  inductive
     6.1 --- a/src/ZF/Inductive.ML	Mon Dec 28 16:58:11 1998 +0100
     6.2 +++ b/src/ZF/Inductive.ML	Mon Dec 28 16:59:28 1998 +0100
     6.3 @@ -56,35 +56,10 @@
     6.4    end;
     6.5  
     6.6  
     6.7 -functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
     6.8 -  : sig include INTR_ELIM INDRULE end =
     6.9 -let
    6.10 -  structure Intr_elim = 
    6.11 -      Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
    6.12 -                    Pr=Standard_Prod and Su=Standard_Sum);
    6.13 -
    6.14 -  structure Indrule = 
    6.15 -      Indrule_Fun (structure Inductive=Inductive and 
    6.16 -                   Pr=Standard_Prod and CP=Standard_CP and
    6.17 -                   Su=Standard_Sum and 
    6.18 -                   Intr_elim=Intr_elim)
    6.19 -in 
    6.20 -   struct 
    6.21 -   val thy      = Intr_elim.thy
    6.22 -   val defs     = Intr_elim.defs
    6.23 -   val bnd_mono = Intr_elim.bnd_mono
    6.24 -   val dom_subset = Intr_elim.dom_subset
    6.25 -   val intrs    = Intr_elim.intrs
    6.26 -   val elim     = Intr_elim.elim
    6.27 -   val mk_cases = Intr_elim.mk_cases
    6.28 -   open Indrule 
    6.29 -   end
    6.30 -end;
    6.31 -
    6.32 -
    6.33 -structure Ind = Add_inductive_def_Fun
    6.34 -    (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    6.35 -     and Su=Standard_Sum);
    6.36 +structure Ind_Package = 
    6.37 +    Add_inductive_def_Fun
    6.38 +      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    6.39 +       and Su=Standard_Sum);
    6.40  
    6.41  
    6.42  structure Gfp =
    6.43 @@ -128,34 +103,7 @@
    6.44    end;
    6.45  
    6.46  
    6.47 -signature COINDRULE =
    6.48 -  sig
    6.49 -  val coinduct : thm
    6.50 -  end;
    6.51 -
    6.52 -
    6.53 -functor CoInd_section_Fun
    6.54 - (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
    6.55 -    : sig include INTR_ELIM COINDRULE end =
    6.56 -let
    6.57 -  structure Intr_elim = 
    6.58 -      Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
    6.59 -                    Pr=Quine_Prod and CP=Standard_CP and
    6.60 -                    Su=Quine_Sum);
    6.61 -in
    6.62 -   struct
    6.63 -   val thy      = Intr_elim.thy
    6.64 -   val defs     = Intr_elim.defs
    6.65 -   val bnd_mono = Intr_elim.bnd_mono
    6.66 -   val dom_subset = Intr_elim.dom_subset
    6.67 -   val intrs    = Intr_elim.intrs
    6.68 -   val elim     = Intr_elim.elim
    6.69 -   val mk_cases = Intr_elim.mk_cases
    6.70 -   val coinduct = Intr_elim.raw_induct
    6.71 -   end
    6.72 -end;
    6.73 -
    6.74 -structure CoInd = 
    6.75 +structure CoInd_Package = 
    6.76      Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
    6.77                            and Su=Quine_Sum);
    6.78  
     7.1 --- a/src/ZF/Inductive.thy	Mon Dec 28 16:58:11 1998 +0100
     7.2 +++ b/src/ZF/Inductive.thy	Mon Dec 28 16:59:28 1998 +0100
     7.3 @@ -1,5 +1,5 @@
     7.4  (*Dummy theory to document dependencies *)
     7.5  
     7.6 -Inductive = Fixedpt + Sum + QPair + "indrule" +
     7.7 +Inductive = Fixedpt + Sum + QPair + 
     7.8  
     7.9  end
     8.1 --- a/src/ZF/InfDatatype.ML	Mon Dec 28 16:58:11 1998 +0100
     8.2 +++ b/src/ZF/InfDatatype.ML	Mon Dec 28 16:59:28 1998 +0100
     8.3 @@ -97,4 +97,4 @@
     8.4      [InfCard_nat, InfCard_nat_Un_cardinal,
     8.5       Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, 
     8.6       zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc,
     8.7 -     Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ datatype_intrs;
     8.8 +     Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ Data_Arg.intrs;
     9.1 --- a/src/ZF/IsaMakefile	Mon Dec 28 16:58:11 1998 +0100
     9.2 +++ b/src/ZF/IsaMakefile	Mon Dec 28 16:59:28 1998 +0100
     9.3 @@ -38,12 +38,12 @@
     9.4    Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \
     9.5    Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy \
     9.6    Update.ML Update.thy Univ.ML Univ.thy WF.ML WF.thy \
     9.7 -  ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \
     9.8 -  cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \
     9.9 +  ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML \
    9.10    domrange.thy equalities.ML equalities.thy func.ML func.thy \
    9.11 -  ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \
    9.12 -  intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
    9.13 -  subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy \
    9.14 +  ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
    9.15 +  subset.thy thy_syntax.ML upair.ML upair.thy \
    9.16 +  Tools/cartprod.ML Tools/datatype_package.ML Tools/inductive_package.ML \
    9.17 +  Tools/primrec_package.ML Tools/typechk.ML \
    9.18    Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \
    9.19    Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy 
    9.20  	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
    9.21 @@ -96,7 +96,7 @@
    9.22    Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
    9.23    Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
    9.24    Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
    9.25 -  Resid/SubUnion.ML Resid/SubUnion.thy Resid/Substitution.ML \
    9.26 +  Resid/Substitution.ML \
    9.27    Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
    9.28  	@$(ISATOOL) usedir $(OUT)/ZF Resid
    9.29  
    9.30 @@ -111,6 +111,7 @@
    9.31    ex/Enum.thy ex/LList.ML ex/LList.thy \
    9.32    ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
    9.33    ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
    9.34 +  ex/Primrec_defs.ML ex/Primrec_defs.thy \
    9.35    ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
    9.36    ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
    9.37    ex/Term.ML ex/Term.thy ex/misc.ML
    10.1 --- a/src/ZF/List.ML	Mon Dec 28 16:58:11 1998 +0100
    10.2 +++ b/src/ZF/List.ML	Mon Dec 28 16:59:28 1998 +0100
    10.3 @@ -6,13 +6,8 @@
    10.4  Datatype definition of Lists
    10.5  *)
    10.6  
    10.7 -open List;
    10.8 -
    10.9  (*** Aspects of the datatype definition ***)
   10.10  
   10.11 -Addsimps list.case_eqns;
   10.12 -
   10.13 -
   10.14  (*An elimination rule, for type-checking*)
   10.15  val ConsE = list.mk_cases list.con_defs "Cons(a,l) : list(A)";
   10.16  
   10.17 @@ -61,39 +56,12 @@
   10.18  \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))  \
   10.19  \    |] ==> list_case(c,h,l) : C(l)";
   10.20  by (rtac (major RS list.induct) 1);
   10.21 -by (ALLGOALS (asm_simp_tac (simpset() addsimps list.case_eqns @ prems)));
   10.22 +by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   10.23  qed "list_case_type";
   10.24  
   10.25  
   10.26 -(** For recursion **)
   10.27 -
   10.28 -Goalw list.con_defs "rank(a) < rank(Cons(a,l))";
   10.29 -by (simp_tac rank_ss 1);
   10.30 -qed "rank_Cons1";
   10.31 -
   10.32 -Goalw list.con_defs "rank(l) < rank(Cons(a,l))";
   10.33 -by (simp_tac rank_ss 1);
   10.34 -qed "rank_Cons2";
   10.35 -
   10.36 -
   10.37  (*** List functions ***)
   10.38  
   10.39 -(** hd and tl **)
   10.40 -
   10.41 -Goalw [hd_def] "hd(Cons(a,l)) = a";
   10.42 -by (resolve_tac list.case_eqns 1);
   10.43 -qed "hd_Cons";
   10.44 -
   10.45 -Goalw [tl_def] "tl(Nil) = Nil";
   10.46 -by (resolve_tac list.case_eqns 1);
   10.47 -qed "tl_Nil";
   10.48 -
   10.49 -Goalw [tl_def] "tl(Cons(a,l)) = l";
   10.50 -by (resolve_tac list.case_eqns 1);
   10.51 -qed "tl_Cons";
   10.52 -
   10.53 -Addsimps [hd_Cons, tl_Nil, tl_Cons];
   10.54 -
   10.55  Goal "l: list(A) ==> tl(l) : list(A)";
   10.56  by (etac list.elim 1);
   10.57  by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs)));
   10.58 @@ -126,52 +94,21 @@
   10.59  by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type])));
   10.60  qed "drop_type";
   10.61  
   10.62 -(** list_rec -- by Vset recursion **)
   10.63 -
   10.64 -Goal "list_rec(Nil,c,h) = c";
   10.65 -by (rtac (list_rec_def RS def_Vrec RS trans) 1);
   10.66 -by (simp_tac (simpset() addsimps list.case_eqns) 1);
   10.67 -qed "list_rec_Nil";
   10.68  
   10.69 -Goal "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
   10.70 -by (rtac (list_rec_def RS def_Vrec RS trans) 1);
   10.71 -by (simp_tac (rank_ss addsimps rank_Cons2::list.case_eqns) 1);
   10.72 -qed "list_rec_Cons";
   10.73 +(** Type checking -- proved by induction, as usual **)
   10.74  
   10.75 -Addsimps [list_rec_Nil, list_rec_Cons];
   10.76 -
   10.77 -
   10.78 -(*Type checking -- proved by induction, as usual*)
   10.79  val prems = Goal
   10.80      "[| l: list(A);    \
   10.81  \       c: C(Nil);       \
   10.82  \       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
   10.83 -\    |] ==> list_rec(l,c,h) : C(l)";
   10.84 +\    |] ==> list_rec(c,h,l) : C(l)";
   10.85  by (list_ind_tac "l" prems 1);
   10.86  by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   10.87  qed "list_rec_type";
   10.88  
   10.89 -(** Versions for use with definitions **)
   10.90 -
   10.91 -val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
   10.92 -by (rewtac rew);
   10.93 -by (rtac list_rec_Nil 1);
   10.94 -qed "def_list_rec_Nil";
   10.95 -
   10.96 -val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
   10.97 -by (rewtac rew);
   10.98 -by (rtac list_rec_Cons 1);
   10.99 -qed "def_list_rec_Cons";
  10.100 -
  10.101 -fun list_recs def = map standard
  10.102 -        ([def] RL [def_list_rec_Nil, def_list_rec_Cons]);
  10.103 -
  10.104  (** map **)
  10.105  
  10.106 -val [map_Nil,map_Cons] = list_recs map_def;
  10.107 -Addsimps [map_Nil, map_Cons];
  10.108 -
  10.109 -val prems = Goalw [map_def] 
  10.110 +val prems = Goalw [get_def thy "map_list"] 
  10.111      "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
  10.112  by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
  10.113  qed "map_type";
  10.114 @@ -183,30 +120,21 @@
  10.115  
  10.116  (** length **)
  10.117  
  10.118 -val [length_Nil,length_Cons] = list_recs length_def;
  10.119 -Addsimps [length_Nil,length_Cons];
  10.120 -
  10.121 -Goalw [length_def] 
  10.122 +Goalw [get_def thy "length_list"] 
  10.123      "l: list(A) ==> length(l) : nat";
  10.124  by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
  10.125  qed "length_type";
  10.126  
  10.127  (** app **)
  10.128  
  10.129 -val [app_Nil,app_Cons] = list_recs app_def;
  10.130 -Addsimps [app_Nil, app_Cons];
  10.131 -
  10.132 -Goalw [app_def] 
  10.133 +Goalw [get_def thy "op @_list"] 
  10.134      "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
  10.135  by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
  10.136  qed "app_type";
  10.137  
  10.138  (** rev **)
  10.139  
  10.140 -val [rev_Nil,rev_Cons] = list_recs rev_def;
  10.141 -Addsimps [rev_Nil,rev_Cons] ;
  10.142 -
  10.143 -Goalw [rev_def] 
  10.144 +Goalw [get_def thy "rev_list"] 
  10.145      "xs: list(A) ==> rev(xs) : list(A)";
  10.146  by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
  10.147  qed "rev_type";
  10.148 @@ -214,10 +142,7 @@
  10.149  
  10.150  (** flat **)
  10.151  
  10.152 -val [flat_Nil,flat_Cons] = list_recs flat_def;
  10.153 -Addsimps [flat_Nil,flat_Cons];
  10.154 -
  10.155 -Goalw [flat_def] 
  10.156 +Goalw [get_def thy "flat_list"] 
  10.157      "ls: list(list(A)) ==> flat(ls) : list(A)";
  10.158  by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
  10.159  qed "flat_type";
  10.160 @@ -225,10 +150,7 @@
  10.161  
  10.162  (** set_of_list **)
  10.163  
  10.164 -val [set_of_list_Nil,set_of_list_Cons] = list_recs set_of_list_def;
  10.165 -Addsimps [set_of_list_Nil,set_of_list_Cons];
  10.166 -
  10.167 -Goalw [set_of_list_def] 
  10.168 +Goalw [get_def thy "set_of_list_list"] 
  10.169      "l: list(A) ==> set_of_list(l) : Pow(A)";
  10.170  by (etac list_rec_type 1);
  10.171  by (ALLGOALS (Blast_tac));
  10.172 @@ -243,10 +165,7 @@
  10.173  
  10.174  (** list_add **)
  10.175  
  10.176 -val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
  10.177 -Addsimps [list_add_Nil,list_add_Cons];
  10.178 -
  10.179 -Goalw [list_add_def] 
  10.180 +Goalw [get_def thy "list_add_list"] 
  10.181      "xs: list(nat) ==> list_add(xs) : nat";
  10.182  by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
  10.183  qed "list_add_type";
  10.184 @@ -256,6 +175,8 @@
  10.185      [list_rec_type, map_type, map_type2, app_type, length_type, 
  10.186       rev_type, flat_type, list_add_type];
  10.187  
  10.188 +Addsimps list_typechecks;
  10.189 +
  10.190  simpset_ref() := simpset() setSolver (type_auto_tac list_typechecks);
  10.191  
  10.192  
  10.193 @@ -282,8 +203,8 @@
  10.194  qed "map_flat";
  10.195  
  10.196  Goal "l: list(A) ==> \
  10.197 -\    list_rec(map(h,l), c, d) = \
  10.198 -\    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
  10.199 +\    list_rec(c, d, map(h,l)) = \
  10.200 +\    list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)";
  10.201  by (list_ind_tac "l" [] 1);
  10.202  by (ALLGOALS Asm_simp_tac);
  10.203  qed "list_rec_map";
    11.1 --- a/src/ZF/List.thy	Mon Dec 28 16:58:11 1998 +0100
    11.2 +++ b/src/ZF/List.thy	Mon Dec 28 16:59:28 1998 +0100
    11.3 @@ -29,42 +29,54 @@
    11.4    "[]"          == "Nil"
    11.5  
    11.6  
    11.7 -constdefs
    11.8 +consts
    11.9 +  length :: i=>i
   11.10    hd      :: i=>i
   11.11 -  "hd(l)       == list_case(0, %x xs. x, l)"
   11.12 +  tl      :: i=>i
   11.13 +  map        :: [i=>i, i] => i
   11.14 +  set_of_list :: i=>i
   11.15 +  "@"        :: [i,i]=>i                        (infixr 60)
   11.16 +  rev :: i=>i
   11.17 +  flat       :: i=>i
   11.18 +  list_add   :: i=>i
   11.19 +
   11.20 +primrec
   11.21 +  "length([]) = 0"
   11.22 +  "length(Cons(a,l)) = succ(length(l))"
   11.23    
   11.24 -  tl      :: i=>i
   11.25 -  "tl(l)       == list_case(Nil, %x xs. xs, l)"
   11.26 +primrec
   11.27 +  "hd(Cons(a,l)) = a"
   11.28 +
   11.29 +primrec
   11.30 +  "tl([]) = []"
   11.31 +  "tl(Cons(a,l)) = l"
   11.32 +
   11.33 +primrec
   11.34 +  "map(f,[]) = []"
   11.35 +  "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
   11.36 + 
   11.37 +primrec
   11.38 +  "set_of_list([]) = 0"
   11.39 +  "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
   11.40 +   
   11.41 +primrec
   11.42 +  "[] @ ys = ys"
   11.43 +  "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
   11.44    
   11.45 +primrec
   11.46 +  "rev([]) = []"
   11.47 +  "rev(Cons(a,l)) = rev(l) @ [a]"
   11.48 +
   11.49 +primrec
   11.50 +  "flat([]) = []"
   11.51 +  "flat(Cons(l,ls)) = l @ flat(ls)"
   11.52 +   
   11.53 +primrec
   11.54 +  "list_add([]) = 0"
   11.55 +  "list_add(Cons(a,l)) = a #+ list_add(l)"
   11.56 +       
   11.57 +constdefs
   11.58    drop       :: [i,i]=>i
   11.59    "drop(i,l)   == rec(i, l, %j r. tl(r))"
   11.60  
   11.61 -  list_rec   :: [i, i, [i,i,i]=>i] => i
   11.62 -  "list_rec(l,c,h) == Vrec(l, %l g. list_case(c, %x xs. h(x, xs, g`xs), l))"
   11.63 -
   11.64 -  map        :: [i=>i, i] => i
   11.65 -  "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
   11.66 -
   11.67 -  length :: i=>i
   11.68 -  "length(l)   == list_rec(l,  0,  %x xs r. succ(r))"
   11.69 -
   11.70 -  set_of_list :: i=>i
   11.71 -  "set_of_list(l)   == list_rec(l,  0,  %x xs r. cons(x,r))"
   11.72 -
   11.73 -consts  (*Cannot use constdefs because @ is not an identifier*)
   11.74 -  "@"        :: [i,i]=>i                        (infixr 60)
   11.75 -defs
   11.76 -  app_def       "xs@ys       == list_rec(xs, ys, %x xs r. Cons(x,r))"
   11.77 -
   11.78 -
   11.79 -constdefs
   11.80 -  rev :: i=>i
   11.81 -  "rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"
   11.82 -
   11.83 -  flat       :: i=>i
   11.84 -  "flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"
   11.85 -
   11.86 -  list_add   :: i=>i
   11.87 -  "list_add(l) == list_rec(l, 0,  %x xs r. x#+r)"
   11.88 -
   11.89  end
    12.1 --- a/src/ZF/Perm.ML	Mon Dec 28 16:58:11 1998 +0100
    12.2 +++ b/src/ZF/Perm.ML	Mon Dec 28 16:59:28 1998 +0100
    12.3 @@ -71,7 +71,7 @@
    12.4  
    12.5  Goal "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)";
    12.6  by (asm_simp_tac (simpset() addsimps [inj_def]) 1);
    12.7 -by (deepen_tac (claset() addEs [subst_context RS box_equals]) 0 1);
    12.8 +by (blast_tac (claset() addIs [subst_context RS box_equals]) 1);
    12.9  bind_thm ("f_imp_injective", ballI RSN (2,result()));
   12.10  
   12.11  val prems = Goal
    13.1 --- a/src/ZF/ROOT.ML	Mon Dec 28 16:58:11 1998 +0100
    13.2 +++ b/src/ZF/ROOT.ML	Mon Dec 28 16:59:28 1998 +0100
    13.3 @@ -30,12 +30,22 @@
    13.4  print_depth 1;
    13.5  
    13.6  (*Add user sections for inductive/datatype definitions*)
    13.7 -use     "$ISABELLE_HOME/src/Pure/section_utils.ML";
    13.8 -use     "thy_syntax.ML";
    13.9 +use     "$ISABELLE_HOME/src/Pure/section_utils";
   13.10 +use     "thy_syntax";
   13.11  
   13.12  use_thy "Let";
   13.13  use_thy "func";
   13.14 -use     "typechk.ML";
   13.15 +use     "Tools/typechk";
   13.16 +use_thy "mono";
   13.17 +use     "ind_syntax";
   13.18 +use     "Tools/cartprod";
   13.19 +use_thy "Fixedpt";
   13.20 +use     "Tools/inductive_package";
   13.21 +use_thy "Inductive";
   13.22 +use_thy "QUniv";
   13.23 +use "Tools/datatype_package";
   13.24 +use "Tools/primrec_package";
   13.25 +use_thy "Datatype";
   13.26  use_thy "InfDatatype";
   13.27  use_thy "List";
   13.28  
    14.1 --- a/src/ZF/Univ.ML	Mon Dec 28 16:58:11 1998 +0100
    14.2 +++ b/src/ZF/Univ.ML	Mon Dec 28 16:59:28 1998 +0100
    14.3 @@ -513,6 +513,20 @@
    14.4  by (rtac Vrec 1);
    14.5  qed "def_Vrec";
    14.6  
    14.7 +(*NOT SUITABLE FOR REWRITING: recursive!*)
    14.8 +Goalw [Vrecursor_def]
    14.9 +     "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)";
   14.10 +by (stac transrec 1);
   14.11 +by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
   14.12 +                              VsetI RS beta, le_refl]) 1);
   14.13 +qed "Vrecursor";
   14.14 +
   14.15 +(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   14.16 +Goal "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x),  a)";
   14.17 +by (Asm_simp_tac 1);
   14.18 +by (rtac Vrecursor 1);
   14.19 +qed "def_Vrecursor";
   14.20 +
   14.21  
   14.22  (*** univ(A) ***)
   14.23  
    15.1 --- a/src/ZF/Univ.thy	Mon Dec 28 16:58:11 1998 +0100
    15.2 +++ b/src/ZF/Univ.thy	Mon Dec 28 16:59:28 1998 +0100
    15.3 @@ -19,6 +19,7 @@
    15.4      Vfrom       :: [i,i]=>i
    15.5      Vset        :: i=>i
    15.6      Vrec        :: [i, [i,i]=>i] =>i
    15.7 +    Vrecursor   :: [[i,i]=>i, i] =>i
    15.8      univ        :: i=>i
    15.9  
   15.10  translations
   15.11 @@ -33,6 +34,10 @@
   15.12          "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
   15.13                               H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
   15.14  
   15.15 +    Vrecursor_def
   15.16 +        "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
   15.17 +                                    H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
   15.18 +
   15.19      univ_def    "univ(A) == Vfrom(A,nat)"
   15.20  
   15.21  end
    16.1 --- a/src/ZF/Zorn.ML	Mon Dec 28 16:58:11 1998 +0100
    16.2 +++ b/src/ZF/Zorn.ML	Mon Dec 28 16:59:28 1998 +0100
    16.3 @@ -9,8 +9,6 @@
    16.4      Classical Theorems of Set Theory. 
    16.5  *)
    16.6  
    16.7 -open Zorn;
    16.8 -
    16.9  (*** Section 1.  Mathematical Preamble ***)
   16.10  
   16.11  Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
    17.1 --- a/src/ZF/Zorn.thy	Mon Dec 28 16:58:11 1998 +0100
    17.2 +++ b/src/ZF/Zorn.thy	Mon Dec 28 16:59:28 1998 +0100
    17.3 @@ -15,13 +15,11 @@
    17.4  
    17.5  consts
    17.6    Subset_rel      :: i=>i
    17.7 -  increasing      :: i=>i
    17.8    chain, maxchain :: i=>i
    17.9    super           :: [i,i]=>i
   17.10  
   17.11  defs
   17.12    Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
   17.13 -  increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
   17.14  
   17.15    chain_def      "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
   17.16    super_def      "super(A,c)    == {d: chain(A). c<=d & c~=d}"
   17.17 @@ -44,8 +42,8 @@
   17.18  
   17.19      Pow_UnionI  "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
   17.20  
   17.21 -  monos         "[Pow_mono]"
   17.22 -  con_defs      "[increasing_def]"
   17.23 +  monos         Pow_mono
   17.24 +  con_defs      increasing_def
   17.25    type_intrs    "[CollectD1 RS apply_funtype, Union_in_Pow]"
   17.26    
   17.27  end
    18.1 --- a/src/ZF/add_ind_def.ML	Mon Dec 28 16:58:11 1998 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,270 +0,0 @@
    18.4 -(*  Title:      ZF/add_ind_def.ML
    18.5 -    ID:         $Id$
    18.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.7 -    Copyright   1994  University of Cambridge
    18.8 -
    18.9 -Fixedpoint definition module -- for Inductive/Coinductive Definitions
   18.10 -
   18.11 -Features:
   18.12 -* least or greatest fixedpoints
   18.13 -* user-specified product and sum constructions
   18.14 -* mutually recursive definitions
   18.15 -* definitions involving arbitrary monotone operators
   18.16 -* automatically proves introduction and elimination rules
   18.17 -
   18.18 -The recursive sets must *already* be declared as constants in parent theory!
   18.19 -
   18.20 -  Introduction rules have the form
   18.21 -  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
   18.22 -  where M is some monotone operator (usually the identity)
   18.23 -  P(x) is any (non-conjunctive) side condition on the free variables
   18.24 -  ti, t are any terms
   18.25 -  Sj, Sk are two of the sets being defined in mutual recursion
   18.26 -
   18.27 -Sums are used only for mutual recursion;
   18.28 -Products are used only to derive "streamlined" induction rules for relations
   18.29 -*)
   18.30 -
   18.31 -signature FP =          (** Description of a fixed point operator **)
   18.32 -  sig
   18.33 -  val oper      : term                  (*fixed point operator*)
   18.34 -  val bnd_mono  : term                  (*monotonicity predicate*)
   18.35 -  val bnd_monoI : thm                   (*intro rule for bnd_mono*)
   18.36 -  val subs      : thm                   (*subset theorem for fp*)
   18.37 -  val Tarski    : thm                   (*Tarski's fixed point theorem*)
   18.38 -  val induct    : thm                   (*induction/coinduction rule*)
   18.39 -  end;
   18.40 -
   18.41 -signature SU =                  (** Description of a disjoint sum **)
   18.42 -  sig
   18.43 -  val sum       : term                  (*disjoint sum operator*)
   18.44 -  val inl       : term                  (*left injection*)
   18.45 -  val inr       : term                  (*right injection*)
   18.46 -  val elim      : term                  (*case operator*)
   18.47 -  val case_inl  : thm                   (*inl equality rule for case*)
   18.48 -  val case_inr  : thm                   (*inr equality rule for case*)
   18.49 -  val inl_iff   : thm                   (*injectivity of inl, using <->*)
   18.50 -  val inr_iff   : thm                   (*injectivity of inr, using <->*)
   18.51 -  val distinct  : thm                   (*distinctness of inl, inr using <->*)
   18.52 -  val distinct' : thm                   (*distinctness of inr, inl using <->*)
   18.53 -  val free_SEs  : thm list              (*elim rules for SU, and pair_iff!*)
   18.54 -  end;
   18.55 -
   18.56 -signature ADD_INDUCTIVE_DEF =
   18.57 -  sig 
   18.58 -  val add_fp_def_i : term list * term * term list -> theory -> theory
   18.59 -  val add_constructs_def :
   18.60 -        string list * ((string*typ*mixfix) * 
   18.61 -                       string * term list * term list) list list ->
   18.62 -        theory -> theory
   18.63 -  end;
   18.64 -
   18.65 -
   18.66 -
   18.67 -(*Declares functions to add fixedpoint/constructor defs to a theory*)
   18.68 -functor Add_inductive_def_Fun 
   18.69 -    (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU)
   18.70 -    : ADD_INDUCTIVE_DEF =
   18.71 -struct
   18.72 -open Logic Ind_Syntax;
   18.73 -
   18.74 -(*internal version*)
   18.75 -fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
   18.76 -  let
   18.77 -    val dummy = (*has essential ancestors?*)
   18.78 -	Theory.requires thy "Inductive" "(co)inductive definitions" 
   18.79 -
   18.80 -    val sign = sign_of thy;
   18.81 -
   18.82 -    (*recT and rec_params should agree for all mutually recursive components*)
   18.83 -    val rec_hds = map head_of rec_tms;
   18.84 -
   18.85 -    val dummy = assert_all is_Const rec_hds
   18.86 -            (fn t => "Recursive set not previously declared as constant: " ^ 
   18.87 -                     Sign.string_of_term sign t);
   18.88 -
   18.89 -    (*Now we know they are all Consts, so get their names, type and params*)
   18.90 -    val rec_names = map (#1 o dest_Const) rec_hds
   18.91 -    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
   18.92 -
   18.93 -    val rec_base_names = map Sign.base_name rec_names;
   18.94 -    val dummy = assert_all Syntax.is_identifier rec_base_names
   18.95 -      (fn a => "Base name of recursive set not an identifier: " ^ a);
   18.96 -
   18.97 -    local (*Checking the introduction rules*)
   18.98 -      val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
   18.99 -      fun intr_ok set =
  18.100 -          case head_of set of Const(a,recT) => a mem rec_names | _ => false;
  18.101 -    in
  18.102 -      val dummy =  assert_all intr_ok intr_sets
  18.103 -         (fn t => "Conclusion of rule does not name a recursive set: " ^ 
  18.104 -                  Sign.string_of_term sign t);
  18.105 -    end;
  18.106 -
  18.107 -    val dummy = assert_all is_Free rec_params
  18.108 -        (fn t => "Param in recursion term not a free variable: " ^
  18.109 -                 Sign.string_of_term sign t);
  18.110 -
  18.111 -    (*** Construct the lfp definition ***)
  18.112 -    val mk_variant = variant (foldr add_term_names (intr_tms,[]));
  18.113 -
  18.114 -    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
  18.115 -
  18.116 -    fun dest_tprop (Const("Trueprop",_) $ P) = P
  18.117 -      | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
  18.118 -                              Sign.string_of_term sign Q);
  18.119 -
  18.120 -    (*Makes a disjunct from an introduction rule*)
  18.121 -    fun lfp_part intr = (*quantify over rule's free vars except parameters*)
  18.122 -      let val prems = map dest_tprop (strip_imp_prems intr)
  18.123 -          val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
  18.124 -          val exfrees = term_frees intr \\ rec_params
  18.125 -          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
  18.126 -      in foldr FOLogic.mk_exists
  18.127 -	       (exfrees, fold_bal (app FOLogic.conj) (zeq::prems)) 
  18.128 -      end;
  18.129 -
  18.130 -    (*The Part(A,h) terms -- compose injections to make h*)
  18.131 -    fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
  18.132 -      | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
  18.133 -
  18.134 -    (*Access to balanced disjoint sums via injections*)
  18.135 -    val parts = 
  18.136 -        map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
  18.137 -                                  (length rec_tms));
  18.138 -
  18.139 -    (*replace each set by the corresponding Part(A,h)*)
  18.140 -    val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
  18.141 -
  18.142 -    val lfp_abs = absfree(X', iT, 
  18.143 -                     mk_Collect(z', dom_sum, 
  18.144 -				fold_bal (app FOLogic.disj) part_intrs));
  18.145 -
  18.146 -    val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
  18.147 -
  18.148 -    val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
  18.149 -                               "Illegal occurrence of recursion operator")
  18.150 -             rec_hds;
  18.151 -
  18.152 -    (*** Make the new theory ***)
  18.153 -
  18.154 -    (*A key definition:
  18.155 -      If no mutual recursion then it equals the one recursive set.
  18.156 -      If mutual recursion then it differs from all the recursive sets. *)
  18.157 -    val big_rec_base_name = space_implode "_" rec_base_names;
  18.158 -    val big_rec_name = Sign.intern_const sign big_rec_base_name;
  18.159 -
  18.160 -    (*Big_rec... is the union of the mutually recursive sets*)
  18.161 -    val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
  18.162 -
  18.163 -    (*The individual sets must already be declared*)
  18.164 -    val axpairs = map Logic.mk_defpair 
  18.165 -          ((big_rec_tm, lfp_rhs) ::
  18.166 -           (case parts of 
  18.167 -               [_] => []                        (*no mutual recursion*)
  18.168 -             | _ => rec_tms ~~          (*define the sets as Parts*)
  18.169 -                    map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
  18.170 -
  18.171 -    (*tracing: print the fixedpoint definition*)
  18.172 -    val _ = if !Ind_Syntax.trace then
  18.173 -		seq (writeln o Sign.string_of_term sign o #2) axpairs
  18.174 -            else ()
  18.175 -
  18.176 -  in  thy |> PureThy.add_defs_i (map Attribute.none axpairs)  end
  18.177 -
  18.178 -
  18.179 -(*Expects the recursive sets to have been defined already.
  18.180 -  con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
  18.181 -fun add_constructs_def (rec_base_names, con_ty_lists) thy = 
  18.182 -  let
  18.183 -    val dummy = (*has essential ancestors?*)
  18.184 -      Theory.requires thy "Datatype" "(co)datatype definitions";
  18.185 -
  18.186 -    val sign = sign_of thy;
  18.187 -    val full_name = Sign.full_name sign;
  18.188 -
  18.189 -    val dummy = writeln"  Defining the constructor functions...";
  18.190 -    val case_name = "f";                (*name for case variables*)
  18.191 -
  18.192 -
  18.193 -    (** Define the constructors **)
  18.194 -
  18.195 -    (*The empty tuple is 0*)
  18.196 -    fun mk_tuple [] = Const("0",iT)
  18.197 -      | mk_tuple args = foldr1 (app Pr.pair) args;
  18.198 -
  18.199 -    fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
  18.200 -
  18.201 -    val npart = length rec_base_names;       (*total # of mutually recursive parts*)
  18.202 -
  18.203 -    (*Make constructor definition; kpart is # of this mutually recursive part*)
  18.204 -    fun mk_con_defs (kpart, con_ty_list) = 
  18.205 -      let val ncon = length con_ty_list    (*number of constructors*)
  18.206 -          fun mk_def (((id,T,syn), name, args, prems), kcon) =
  18.207 -                (*kcon is index of constructor*)
  18.208 -              mk_defpair (list_comb (Const (full_name name, T), args),
  18.209 -                          mk_inject npart kpart
  18.210 -                          (mk_inject ncon kcon (mk_tuple args)))
  18.211 -      in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
  18.212 -
  18.213 -    (** Define the case operator **)
  18.214 -
  18.215 -    (*Combine split terms using case; yields the case operator for one part*)
  18.216 -    fun call_case case_list = 
  18.217 -      let fun call_f (free,[]) = Abs("null", iT, free)
  18.218 -            | call_f (free,args) =
  18.219 -                  CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
  18.220 -                              Ind_Syntax.iT 
  18.221 -                              free 
  18.222 -      in  fold_bal (app Su.elim) (map call_f case_list)  end;
  18.223 -
  18.224 -    (** Generating function variables for the case definition
  18.225 -        Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
  18.226 -
  18.227 -    (*Treatment of a single constructor*)
  18.228 -    fun add_case (((_, T, _), name, args, prems), (opno, cases)) =
  18.229 -      if Syntax.is_identifier name then
  18.230 -        (opno, (Free (case_name ^ "_" ^ name, T), args) :: cases)
  18.231 -      else
  18.232 -        (opno + 1, (Free (case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases);
  18.233 -
  18.234 -    (*Treatment of a list of constructors, for one part*)
  18.235 -    fun add_case_list (con_ty_list, (opno, case_lists)) =
  18.236 -      let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))
  18.237 -      in (opno', case_list :: case_lists) end;
  18.238 -
  18.239 -    (*Treatment of all parts*)
  18.240 -    val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
  18.241 -
  18.242 -    val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
  18.243 -
  18.244 -    val big_rec_base_name = space_implode "_" rec_base_names;
  18.245 -    val big_case_base_name = big_rec_base_name ^ "_case";
  18.246 -    val big_case_name = full_name big_case_base_name;
  18.247 -
  18.248 -    (*The list of all the function variables*)
  18.249 -    val big_case_args = flat (map (map #1) case_lists);
  18.250 -
  18.251 -    val big_case_tm =
  18.252 -      list_comb (Const (big_case_name, big_case_typ), big_case_args); 
  18.253 -
  18.254 -    val big_case_def = mk_defpair
  18.255 -      (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));
  18.256 -
  18.257 -
  18.258 -    (* Build the new theory *)
  18.259 -
  18.260 -    val const_decs =
  18.261 -      (big_case_base_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
  18.262 -
  18.263 -    val axpairs =
  18.264 -      big_case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists));
  18.265 -
  18.266 -  in
  18.267 -    thy
  18.268 -    |> Theory.add_consts_i const_decs
  18.269 -    |> PureThy.add_defs_i (map Attribute.none axpairs)
  18.270 -  end;
  18.271 -
  18.272 -
  18.273 -end;
    19.1 --- a/src/ZF/add_ind_def.thy	Mon Dec 28 16:58:11 1998 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,3 +0,0 @@
    19.4 -(*Dummy theory to document dependencies *)
    19.5 -
    19.6 -add_ind_def = Fixedpt + "ind_syntax" + "cartprod"
    20.1 --- a/src/ZF/cartprod.ML	Mon Dec 28 16:58:11 1998 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,90 +0,0 @@
    20.4 -(*  Title:      ZF/cartprod.ML
    20.5 -    ID:         $Id$
    20.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    20.7 -    Copyright   1996  University of Cambridge
    20.8 -
    20.9 -Syntactic operations for Cartesian Products
   20.10 -*)
   20.11 -
   20.12 -signature PR =                  (** Description of a Cartesian product **)
   20.13 -  sig
   20.14 -  val sigma     : term                  (*Cartesian product operator*)
   20.15 -  val pair      : term                  (*pairing operator*)
   20.16 -  val split_name : string               (*name of polymorphic split*)
   20.17 -  val pair_iff  : thm                   (*injectivity of pairing, using <->*)
   20.18 -  val split_eq  : thm                   (*equality rule for split*)
   20.19 -  val fsplitI   : thm                   (*intro rule for fsplit*)
   20.20 -  val fsplitD   : thm                   (*destruct rule for fsplit*)
   20.21 -  val fsplitE   : thm                   (*elim rule; apparently never used*)
   20.22 -  end;
   20.23 -
   20.24 -signature CARTPROD =            (** Derived syntactic functions for produts **)
   20.25 -  sig
   20.26 -  val ap_split : typ -> typ -> term -> term
   20.27 -  val factors : typ -> typ list
   20.28 -  val mk_prod : typ * typ -> typ
   20.29 -  val mk_tuple : term -> typ -> term list -> term
   20.30 -  val pseudo_type : term -> typ
   20.31 -  val remove_split : thm -> thm
   20.32 -  val split_const : typ -> term
   20.33 -  val split_rule_var : term * typ * thm -> thm
   20.34 -  end;
   20.35 -
   20.36 -
   20.37 -functor CartProd_Fun (Pr: PR) : CARTPROD =
   20.38 -struct
   20.39 -
   20.40 -(* Some of these functions expect "pseudo-types" containing products,
   20.41 -   as in HOL; the true ZF types would just be "i" *)
   20.42 -
   20.43 -fun mk_prod (T1,T2) = Type("*", [T1,T2]);
   20.44 -
   20.45 -(*Bogus product type underlying a (possibly nested) Sigma.  
   20.46 -  Lets us share HOL code*)
   20.47 -fun pseudo_type (t $ A $ Abs(_,_,B)) = 
   20.48 -        if t = Pr.sigma  then  mk_prod(pseudo_type A, pseudo_type B)
   20.49 -                         else  Ind_Syntax.iT
   20.50 -  | pseudo_type _           =  Ind_Syntax.iT;
   20.51 -
   20.52 -(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
   20.53 -fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
   20.54 -  | factors T                    = [T];
   20.55 -
   20.56 -(*Make a well-typed instance of "split"*)
   20.57 -fun split_const T = Const(Pr.split_name, 
   20.58 -                          [[Ind_Syntax.iT, Ind_Syntax.iT]--->T, 
   20.59 -                           Ind_Syntax.iT] ---> T);
   20.60 -
   20.61 -(*In ap_split S T u, term u expects separate arguments for the factors of S,
   20.62 -  with result type T.  The call creates a new term expecting one argument
   20.63 -  of type S.*)
   20.64 -fun ap_split (Type("*", [T1,T2])) T3 u   = 
   20.65 -       split_const T3 $ 
   20.66 -       Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
   20.67 -           ap_split T2 T3
   20.68 -           ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
   20.69 -            Bound 0))
   20.70 -  | ap_split T T3 u = u;
   20.71 -
   20.72 -(*Makes a nested tuple from a list, following the product type structure*)
   20.73 -fun mk_tuple pair (Type("*", [T1,T2])) tms = 
   20.74 -        pair $ (mk_tuple pair T1 tms)
   20.75 -             $ (mk_tuple pair T2 (drop (length (factors T1), tms)))
   20.76 -  | mk_tuple pair T (t::_) = t;
   20.77 -
   20.78 -(*Attempts to remove occurrences of split, and pair-valued parameters*)
   20.79 -val remove_split = rewrite_rule [Pr.split_eq];
   20.80 -
   20.81 -(*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
   20.82 -fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
   20.83 -      let val T' = factors T1 ---> T2
   20.84 -          val newt = ap_split T1 T2 (Var(v,T'))
   20.85 -          val cterm = Thm.cterm_of (#sign(rep_thm rl))
   20.86 -      in
   20.87 -          remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
   20.88 -                                           cterm newt)]) rl)
   20.89 -      end
   20.90 -  | split_rule_var (t,T,rl) = rl;
   20.91 -
   20.92 -end;
   20.93 -
    21.1 --- a/src/ZF/cartprod.thy	Mon Dec 28 16:58:11 1998 +0100
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,3 +0,0 @@
    21.4 -(*Dummy theory to document dependencies *)
    21.5 -
    21.6 -cartprod = "ind_syntax"
    22.1 --- a/src/ZF/constructor.ML	Mon Dec 28 16:58:11 1998 +0100
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,96 +0,0 @@
    22.4 -(*  Title:      ZF/constructor.ML
    22.5 -    ID:         $Id$
    22.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7 -    Copyright   1993  University of Cambridge
    22.8 -
    22.9 -Constructor function module -- for (Co)Datatype Definitions
   22.10 -*)
   22.11 -
   22.12 -signature CONSTRUCTOR_ARG =
   22.13 -  sig
   22.14 -  val thy          : theory             (*parent containing constructor defs*)
   22.15 -  val big_rec_name : string             (*name of mutually recursive set*)
   22.16 -  val con_ty_lists : ((string*typ*mixfix) * 
   22.17 -                      string * term list * term list) list list
   22.18 -                                        (*description of constructors*)
   22.19 -  end;
   22.20 -
   22.21 -signature CONSTRUCTOR_RESULT =
   22.22 -  sig
   22.23 -  val con_defs   : thm list             (*definitions made in thy*)
   22.24 -  val case_eqns  : thm list             (*equations for case operator*)
   22.25 -  val free_iffs  : thm list             (*freeness rewrite rules*)
   22.26 -  val free_SEs   : thm list             (*freeness destruct rules*)
   22.27 -  val mk_free    : string -> thm        (*makes freeness theorems*)
   22.28 -  end;
   22.29 -
   22.30 -
   22.31 -(*Proves theorems relating to constructors*)
   22.32 -functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
   22.33 -                      Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
   22.34 -let
   22.35 -
   22.36 -(*1st element is the case definition; others are the constructors*)
   22.37 -val big_case_name = Const.big_rec_name ^ "_case";
   22.38 -
   22.39 -val con_defs = get_def Const.thy big_case_name :: 
   22.40 -               map (get_def Const.thy o #2) (flat Const.con_ty_lists);
   22.41 -
   22.42 -(** Prove the case theorem **)
   22.43 -
   22.44 -(*Get the case term from its definition*)
   22.45 -val Const("==",_) $ big_case_tm $ _ =
   22.46 -    hd con_defs |> rep_thm |> #prop |> Logic.unvarify;
   22.47 -
   22.48 -val (_, big_case_args) = strip_comb big_case_tm;
   22.49 -
   22.50 -(*Each equation has the form 
   22.51 -  rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
   22.52 -fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = 
   22.53 -  FOLogic.mk_Trueprop
   22.54 -    (FOLogic.mk_eq
   22.55 -     (big_case_tm $
   22.56 -       (list_comb (Const (Sign.intern_const (sign_of Const.thy) name,T), 
   22.57 -		   args)),
   22.58 -      list_comb (case_free, args)));
   22.59 -
   22.60 -val case_trans = hd con_defs RS Ind_Syntax.def_trans
   22.61 -and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
   22.62 -
   22.63 -(*Proves a single case equation.  Could use simp_tac, but it's slower!*)
   22.64 -fun case_tacsf con_def _ = 
   22.65 -  [rewtac con_def,
   22.66 -   rtac case_trans 1,
   22.67 -   REPEAT (resolve_tac [refl, split_trans, 
   22.68 -                        Su.case_inl RS trans, 
   22.69 -                        Su.case_inr RS trans] 1)];
   22.70 -
   22.71 -fun prove_case_equation (arg,con_def) =
   22.72 -    prove_goalw_cterm [] 
   22.73 -        (cterm_of (sign_of Const.thy) (mk_case_equation arg))
   22.74 -        (case_tacsf con_def);
   22.75 -
   22.76 -val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
   22.77 -
   22.78 -in
   22.79 -  struct
   22.80 -  val con_defs = con_defs
   22.81 -
   22.82 -  val free_iffs = con_iffs @ 
   22.83 -    [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
   22.84 -
   22.85 -  val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
   22.86 -
   22.87 -  (*Typical theorems have the form ~con1=con2, con1=con2==>False,
   22.88 -    con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
   22.89 -  fun mk_free s =
   22.90 -      prove_goalw Const.thy con_defs s
   22.91 -        (fn prems => [cut_facts_tac prems 1, 
   22.92 -                      fast_tac (ZF_cs addSEs free_SEs) 1]);
   22.93 -
   22.94 -  val case_eqns = map prove_case_equation 
   22.95 -              (flat Const.con_ty_lists ~~ big_case_args ~~ tl con_defs);
   22.96 -  end
   22.97 -end;
   22.98 -
   22.99 -
    23.1 --- a/src/ZF/constructor.thy	Mon Dec 28 16:58:11 1998 +0100
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,3 +0,0 @@
    23.4 -(*Dummy theory to document dependencies *)
    23.5 -
    23.6 -constructor = "intr_elim"
    24.1 --- a/src/ZF/ind_syntax.ML	Mon Dec 28 16:58:11 1998 +0100
    24.2 +++ b/src/ZF/ind_syntax.ML	Mon Dec 28 16:59:28 1998 +0100
    24.3 @@ -15,6 +15,10 @@
    24.4  (*Print tracing messages during processing of "inductive" theory sections*)
    24.5  val trace = ref false;
    24.6  
    24.7 +fun traceIt msg ct = 
    24.8 +    if !trace then (writeln (msg ^ string_of_cterm ct); ct)
    24.9 +    else ct;
   24.10 +
   24.11  (** Abstract syntax definitions for ZF **)
   24.12  
   24.13  val iT = Type("i",[]);
   24.14 @@ -29,6 +33,10 @@
   24.15  
   24.16  val Part_const = Const("Part", [iT,iT-->iT]--->iT);
   24.17  
   24.18 +val apply_const = Const("op `", [iT,iT]--->iT);
   24.19 +
   24.20 +val Vrecursor_const = Const("Vrecursor", [[iT,iT]--->iT, iT]--->iT);
   24.21 +
   24.22  val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
   24.23  fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
   24.24  
   24.25 @@ -60,6 +68,11 @@
   24.26  
   24.27  (** For datatype definitions **)
   24.28  
   24.29 +(*Constructor name, type, mixfix info;
   24.30 +  internal name from mixfix, datatype sets, full premises*)
   24.31 +type constructor_spec = 
   24.32 +    ((string * typ * mixfix) * string * term list * term list);
   24.33 +
   24.34  fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
   24.35    | dest_mem _ = error "Constructor specifications must have the form x:A";
   24.36  
   24.37 @@ -103,8 +116,8 @@
   24.38  
   24.39  (*Previously these both did    replicate (length rec_tms);  however now
   24.40    [q]univ itself constitutes the sum domain for mutual recursion!*)
   24.41 -fun data_domain rec_tms = univ $ union_params (hd rec_tms);
   24.42 -fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms);
   24.43 +fun data_domain false rec_tms = univ $ union_params (hd rec_tms)
   24.44 +  | data_domain true  rec_tms = quniv $ union_params (hd rec_tms);
   24.45  
   24.46  (*Could go to FOL, but it's hardly general*)
   24.47  val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
   24.48 @@ -128,5 +141,3 @@
   24.49  
   24.50  end;
   24.51  
   24.52 -
   24.53 -val trace_induct = Ind_Syntax.trace;
    25.1 --- a/src/ZF/ind_syntax.thy	Mon Dec 28 16:58:11 1998 +0100
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,3 +0,0 @@
    25.4 -(*Dummy theory to document dependencies *)
    25.5 -
    25.6 -ind_syntax = "mono"
    26.1 --- a/src/ZF/indrule.ML	Mon Dec 28 16:58:11 1998 +0100
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,276 +0,0 @@
    26.4 -(*  Title:      ZF/indrule.ML
    26.5 -    ID:         $Id$
    26.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    26.7 -    Copyright   1994  University of Cambridge
    26.8 -
    26.9 -Induction rule module -- for Inductive/Coinductive Definitions
   26.10 -
   26.11 -Proves a strong induction rule and a mutual induction rule
   26.12 -*)
   26.13 -
   26.14 -signature INDRULE =
   26.15 -  sig
   26.16 -  val induct        : thm                       (*main induction rule*)
   26.17 -  val mutual_induct : thm                       (*mutual induction rule*)
   26.18 -  end;
   26.19 -
   26.20 -
   26.21 -functor Indrule_Fun
   26.22 -    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
   26.23 -     and Pr: PR and CP: CARTPROD and Su : SU and 
   26.24 -     Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE  =
   26.25 -let
   26.26 -
   26.27 -val sign = sign_of Inductive.thy;
   26.28 -
   26.29 -val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms);
   26.30 -
   26.31 -val big_rec_name =
   26.32 -  Sign.intern_const sign (space_implode "_" (map Sign.base_name Intr_elim.rec_names));
   26.33 -
   26.34 -val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
   26.35 -
   26.36 -val _ = writeln "  Proving the induction rule...";
   26.37 -
   26.38 -(*** Prove the main induction rule ***)
   26.39 -
   26.40 -val pred_name = "P";            (*name for predicate variables*)
   26.41 -
   26.42 -val big_rec_def::part_rec_defs = Intr_elim.defs;
   26.43 -
   26.44 -(*Used to make induction rules;
   26.45 -   ind_alist = [(rec_tm1,pred1),...]  -- associates predicates with rec ops
   26.46 -   prem is a premise of an intr rule*)
   26.47 -fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ 
   26.48 -                 (Const("op :",_)$t$X), iprems) =
   26.49 -     (case gen_assoc (op aconv) (ind_alist, X) of
   26.50 -          Some pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
   26.51 -        | None => (*possibly membership in M(rec_tm), for M monotone*)
   26.52 -            let fun mk_sb (rec_tm,pred) = 
   26.53 -                        (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
   26.54 -            in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
   26.55 -  | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
   26.56 -
   26.57 -(*Make a premise of the induction rule.*)
   26.58 -fun induct_prem ind_alist intr =
   26.59 -  let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
   26.60 -      val iprems = foldr (add_induct_prem ind_alist)
   26.61 -                         (Logic.strip_imp_prems intr,[])
   26.62 -      val (t,X) = Ind_Syntax.rule_concl intr
   26.63 -      val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
   26.64 -      val concl = FOLogic.mk_Trueprop (pred $ t)
   26.65 -  in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
   26.66 -  handle Bind => error"Recursion term not found in conclusion";
   26.67 -
   26.68 -(*Minimizes backtracking by delivering the correct premise to each goal.
   26.69 -  Intro rules with extra Vars in premises still cause some backtracking *)
   26.70 -fun ind_tac [] 0 = all_tac
   26.71 -  | ind_tac(prem::prems) i = 
   26.72 -        DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN
   26.73 -        ind_tac prems (i-1);
   26.74 -
   26.75 -val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
   26.76 -
   26.77 -val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
   26.78 -                    Inductive.intr_tms;
   26.79 -
   26.80 -val _ = if !Ind_Syntax.trace then 
   26.81 -            (writeln "ind_prems = ";
   26.82 -	     seq (writeln o Sign.string_of_term sign) ind_prems;
   26.83 -	     writeln "raw_induct = "; print_thm Intr_elim.raw_induct)
   26.84 -        else ();
   26.85 -
   26.86 -
   26.87 -(*We use a MINIMAL simpset because others (such as FOL_ss) contain too many
   26.88 -  simplifications.  If the premises get simplified, then the proofs could 
   26.89 -  fail.  *)
   26.90 -val min_ss = empty_ss
   26.91 -      setmksimps (map mk_eq o ZF_atomize o gen_all)
   26.92 -      setSolver  (fn prems => resolve_tac (triv_rls@prems) 
   26.93 -                              ORELSE' assume_tac
   26.94 -                              ORELSE' etac FalseE);
   26.95 -
   26.96 -val quant_induct = 
   26.97 -    prove_goalw_cterm part_rec_defs 
   26.98 -      (cterm_of sign 
   26.99 -       (Logic.list_implies (ind_prems, 
  26.100 -                FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))
  26.101 -      (fn prems =>
  26.102 -       [rtac (impI RS allI) 1,
  26.103 -        DETERM (etac Intr_elim.raw_induct 1),
  26.104 -        (*Push Part inside Collect*)
  26.105 -        full_simp_tac (min_ss addsimps [Part_Collect]) 1,
  26.106 -        (*This CollectE and disjE separates out the introduction rules*)
  26.107 -	REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
  26.108 -	(*Now break down the individual cases.  No disjE here in case
  26.109 -          some premise involves disjunction.*)
  26.110 -        REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE] 
  26.111 -                           ORELSE' hyp_subst_tac)),
  26.112 -        ind_tac (rev prems) (length prems) ]);
  26.113 -
  26.114 -val _ = if !Ind_Syntax.trace then 
  26.115 -            (writeln "quant_induct = "; print_thm quant_induct)
  26.116 -        else ();
  26.117 -
  26.118 -
  26.119 -(*** Prove the simultaneous induction rule ***)
  26.120 -
  26.121 -(*Make distinct predicates for each inductive set*)
  26.122 -
  26.123 -(*The components of the element type, several if it is a product*)
  26.124 -val elem_type = CP.pseudo_type Inductive.dom_sum;
  26.125 -val elem_factors = CP.factors elem_type;
  26.126 -val elem_frees = mk_frees "za" elem_factors;
  26.127 -val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees;
  26.128 -
  26.129 -(*Given a recursive set and its domain, return the "fsplit" predicate
  26.130 -  and a conclusion for the simultaneous induction rule.
  26.131 -  NOTE.  This will not work for mutually recursive predicates.  Previously
  26.132 -  a summand 'domt' was also an argument, but this required the domain of
  26.133 -  mutual recursion to invariably be a disjoint sum.*)
  26.134 -fun mk_predpair rec_tm = 
  26.135 -  let val rec_name = (#1 o dest_Const o head_of) rec_tm
  26.136 -      val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
  26.137 -                       elem_factors ---> FOLogic.oT)
  26.138 -      val qconcl = 
  26.139 -        foldr FOLogic.mk_all
  26.140 -          (elem_frees, 
  26.141 -           FOLogic.imp $ 
  26.142 -           (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
  26.143 -                 $ (list_comb (pfree, elem_frees)))
  26.144 -  in  (CP.ap_split elem_type FOLogic.oT pfree, 
  26.145 -       qconcl)  
  26.146 -  end;
  26.147 -
  26.148 -val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
  26.149 -
  26.150 -(*Used to form simultaneous induction lemma*)
  26.151 -fun mk_rec_imp (rec_tm,pred) = 
  26.152 -    FOLogic.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $ 
  26.153 -                     (pred $ Bound 0);
  26.154 -
  26.155 -(*To instantiate the main induction rule*)
  26.156 -val induct_concl = 
  26.157 -    FOLogic.mk_Trueprop
  26.158 -      (Ind_Syntax.mk_all_imp
  26.159 -       (big_rec_tm,
  26.160 -        Abs("z", Ind_Syntax.iT, 
  26.161 -            fold_bal (app FOLogic.conj) 
  26.162 -            (ListPair.map mk_rec_imp (Inductive.rec_tms,preds)))))
  26.163 -and mutual_induct_concl =
  26.164 - FOLogic.mk_Trueprop(fold_bal (app FOLogic.conj) qconcls);
  26.165 -
  26.166 -val _ = if !Ind_Syntax.trace then 
  26.167 -            (writeln ("induct_concl = " ^
  26.168 -		      Sign.string_of_term sign induct_concl);
  26.169 -             writeln ("mutual_induct_concl = " ^
  26.170 -		      Sign.string_of_term sign mutual_induct_concl))
  26.171 -        else ();
  26.172 -
  26.173 -
  26.174 -val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
  26.175 -                        resolve_tac [allI, impI, conjI, Part_eqI],
  26.176 -                        dresolve_tac [spec, mp, Pr.fsplitD]];
  26.177 -
  26.178 -val need_mutual = length Intr_elim.rec_names > 1;
  26.179 -
  26.180 -val lemma = (*makes the link between the two induction rules*)
  26.181 -  if need_mutual then
  26.182 -     (writeln "  Proving the mutual induction rule...";
  26.183 -      prove_goalw_cterm part_rec_defs 
  26.184 -	    (cterm_of sign (Logic.mk_implies (induct_concl,
  26.185 -					      mutual_induct_concl)))
  26.186 -	    (fn prems =>
  26.187 -	     [cut_facts_tac prems 1, 
  26.188 -	      REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
  26.189 -		      lemma_tac 1)]))
  26.190 -  else (writeln "  [ No mutual induction rule needed ]";
  26.191 -        TrueI);
  26.192 -
  26.193 -val _ = if !Ind_Syntax.trace then 
  26.194 -            (writeln "lemma = "; print_thm lemma)
  26.195 -        else ();
  26.196 -
  26.197 -
  26.198 -(*Mutual induction follows by freeness of Inl/Inr.*)
  26.199 -
  26.200 -(*Simplification largely reduces the mutual induction rule to the 
  26.201 -  standard rule*)
  26.202 -val mut_ss = 
  26.203 -    min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
  26.204 -
  26.205 -val all_defs = Inductive.con_defs @ part_rec_defs;
  26.206 -
  26.207 -(*Removes Collects caused by M-operators in the intro rules.  It is very
  26.208 -  hard to simplify
  26.209 -    list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))}) 
  26.210 -  where t==Part(tf,Inl) and f==Part(tf,Inr) to  list({v: tf. P_t(v)}).
  26.211 -  Instead the following rules extract the relevant conjunct.
  26.212 -*)
  26.213 -val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos
  26.214 -              RLN (2,[rev_subsetD]);
  26.215 -
  26.216 -(*Minimizes backtracking by delivering the correct premise to each goal*)
  26.217 -fun mutual_ind_tac [] 0 = all_tac
  26.218 -  | mutual_ind_tac(prem::prems) i = 
  26.219 -      DETERM
  26.220 -       (SELECT_GOAL 
  26.221 -          (
  26.222 -           (*Simplify the assumptions and goal by unfolding Part and
  26.223 -             using freeness of the Sum constructors; proves all but one
  26.224 -             conjunct by contradiction*)
  26.225 -           rewrite_goals_tac all_defs  THEN
  26.226 -           simp_tac (mut_ss addsimps [Part_iff]) 1  THEN
  26.227 -           IF_UNSOLVED (*simp_tac may have finished it off!*)
  26.228 -             ((*simplify assumptions*)
  26.229 -              (*some risk of excessive simplification here -- might have
  26.230 -                to identify the bare minimum set of rewrites*)
  26.231 -              full_simp_tac 
  26.232 -                 (mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1
  26.233 -              THEN
  26.234 -              (*unpackage and use "prem" in the corresponding place*)
  26.235 -              REPEAT (rtac impI 1)  THEN
  26.236 -              rtac (rewrite_rule all_defs prem) 1  THEN
  26.237 -              (*prem must not be REPEATed below: could loop!*)
  26.238 -              DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' 
  26.239 -                                      eresolve_tac (conjE::mp::cmonos))))
  26.240 -          ) i)
  26.241 -       THEN mutual_ind_tac prems (i-1);
  26.242 -
  26.243 -val mutual_induct_fsplit = 
  26.244 -  if need_mutual then
  26.245 -    prove_goalw_cterm []
  26.246 -          (cterm_of sign
  26.247 -           (Logic.list_implies 
  26.248 -              (map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms,
  26.249 -               mutual_induct_concl)))
  26.250 -          (fn prems =>
  26.251 -           [rtac (quant_induct RS lemma) 1,
  26.252 -            mutual_ind_tac (rev prems) (length prems)])
  26.253 -  else TrueI;
  26.254 -
  26.255 -(** Uncurrying the predicate in the ordinary induction rule **)
  26.256 -
  26.257 -(*instantiate the variable to a tuple, if it is non-trivial, in order to
  26.258 -  allow the predicate to be "opened up".
  26.259 -  The name "x.1" comes from the "RS spec" !*)
  26.260 -val inst = 
  26.261 -    case elem_frees of [_] => I
  26.262 -       | _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)), 
  26.263 -                                 cterm_of sign elem_tuple)]);
  26.264 -
  26.265 -(*strip quantifier and the implication*)
  26.266 -val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
  26.267 -
  26.268 -val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0
  26.269 -
  26.270 -in
  26.271 -  struct
  26.272 -  (*strip quantifier*)
  26.273 -  val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0) 
  26.274 -               |> standard;
  26.275 -
  26.276 -  (*Just "True" unless there's true mutual recursion.  This saves storage.*)
  26.277 -  val mutual_induct = CP.remove_split mutual_induct_fsplit
  26.278 -  end
  26.279 -end;
    27.1 --- a/src/ZF/indrule.thy	Mon Dec 28 16:58:11 1998 +0100
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,3 +0,0 @@
    27.4 -(*Dummy theory to document dependencies *)
    27.5 -
    27.6 -indrule = "ind_syntax" + "cartprod" + "intr_elim"
    28.1 --- a/src/ZF/intr_elim.ML	Mon Dec 28 16:58:11 1998 +0100
    28.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.3 @@ -1,165 +0,0 @@
    28.4 -(*  Title:      ZF/intr_elim.ML
    28.5 -    ID:         $Id$
    28.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    28.7 -    Copyright   1994  University of Cambridge
    28.8 -
    28.9 -Introduction/elimination rule module -- for Inductive/Coinductive Definitions
   28.10 -*)
   28.11 -
   28.12 -signature INDUCTIVE_ARG =       (** Description of a (co)inductive def **)
   28.13 -  sig
   28.14 -  val thy        : theory               (*new theory with inductive defs*)
   28.15 -  val monos      : thm list             (*monotonicity of each M operator*)
   28.16 -  val con_defs   : thm list             (*definitions of the constructors*)
   28.17 -  val type_intrs : thm list             (*type-checking intro rules*)
   28.18 -  val type_elims : thm list             (*type-checking elim rules*)
   28.19 -  end;
   28.20 -
   28.21 -
   28.22 -signature INDUCTIVE_I =         (** Terms read from the theory section **)
   28.23 -  sig
   28.24 -  val rec_tms    : term list            (*the recursive sets*)
   28.25 -  val dom_sum    : term                 (*their common domain*)
   28.26 -  val intr_tms   : term list            (*terms for the introduction rules*)
   28.27 -  end;
   28.28 -
   28.29 -signature INTR_ELIM =
   28.30 -  sig
   28.31 -  val thy        : theory               (*copy of input theory*)
   28.32 -  val defs       : thm list             (*definitions made in thy*)
   28.33 -  val bnd_mono   : thm                  (*monotonicity for the lfp definition*)
   28.34 -  val dom_subset : thm                  (*inclusion of recursive set in dom*)
   28.35 -  val intrs      : thm list             (*introduction rules*)
   28.36 -  val elim       : thm                  (*case analysis theorem*)
   28.37 -  val mk_cases   : thm list -> string -> thm    (*generates case theorems*)
   28.38 -  end;
   28.39 -
   28.40 -signature INTR_ELIM_AUX =       (** Used to make induction rules **)
   28.41 -  sig
   28.42 -  val raw_induct : thm                  (*raw induction rule from Fp.induct*)
   28.43 -  val rec_names  : string list          (*names of recursive sets*)
   28.44 -  end;
   28.45 -
   28.46 -(*prove intr/elim rules for a fixedpoint definition*)
   28.47 -functor Intr_elim_Fun
   28.48 -    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
   28.49 -     and Fp: FP and Pr : PR and Su : SU) 
   28.50 -    : sig include INTR_ELIM INTR_ELIM_AUX end =
   28.51 -let
   28.52 -
   28.53 -val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
   28.54 -val big_rec_base_name = space_implode "_" (map Sign.base_name rec_names);
   28.55 -
   28.56 -val _ = deny (big_rec_base_name mem (Sign.stamp_names_of (sign_of Inductive.thy)))
   28.57 -             ("Definition " ^ big_rec_base_name ^ 
   28.58 -              " would clash with the theory of the same name!");
   28.59 -
   28.60 -(*fetch fp definitions from the theory*)
   28.61 -val big_rec_def::part_rec_defs = 
   28.62 -  map (get_def Inductive.thy)
   28.63 -      (case rec_names of [_] => rec_names | _ => big_rec_base_name::rec_names);
   28.64 -
   28.65 -
   28.66 -val sign = sign_of Inductive.thy;
   28.67 -
   28.68 -(********)
   28.69 -val _ = writeln "  Proving monotonicity...";
   28.70 -
   28.71 -val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
   28.72 -    big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
   28.73 -
   28.74 -val bnd_mono = 
   28.75 -    prove_goalw_cterm [] 
   28.76 -      (cterm_of sign (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
   28.77 -      (fn _ =>
   28.78 -       [rtac (Collect_subset RS bnd_monoI) 1,
   28.79 -        REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);
   28.80 -
   28.81 -val dom_subset = standard (big_rec_def RS Fp.subs);
   28.82 -
   28.83 -val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
   28.84 -
   28.85 -(********)
   28.86 -val _ = writeln "  Proving the introduction rules...";
   28.87 -
   28.88 -(*Mutual recursion?  Helps to derive subset rules for the individual sets.*)
   28.89 -val Part_trans =
   28.90 -    case rec_names of
   28.91 -         [_] => asm_rl
   28.92 -       | _   => standard (Part_subset RS subset_trans);
   28.93 -
   28.94 -(*To type-check recursive occurrences of the inductive sets, possibly
   28.95 -  enclosed in some monotonic operator M.*)
   28.96 -val rec_typechecks = 
   28.97 -   [dom_subset] RL (asm_rl :: ([Part_trans] RL Inductive.monos)) RL [subsetD];
   28.98 -
   28.99 -(*Type-checking is hardest aspect of proof;
  28.100 -  disjIn selects the correct disjunct after unfolding*)
  28.101 -fun intro_tacsf disjIn prems = 
  28.102 -  [(*insert prems and underlying sets*)
  28.103 -   cut_facts_tac prems 1,
  28.104 -   DETERM (stac unfold 1),
  28.105 -   REPEAT (resolve_tac [Part_eqI,CollectI] 1),
  28.106 -   (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
  28.107 -   rtac disjIn 2,
  28.108 -   (*Not ares_tac, since refl must be tried before any equality assumptions;
  28.109 -     backtracking may occur if the premises have extra variables!*)
  28.110 -   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2),
  28.111 -   (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
  28.112 -   rewrite_goals_tac Inductive.con_defs,
  28.113 -   REPEAT (rtac refl 2),
  28.114 -   (*Typechecking; this can fail*)
  28.115 -   REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
  28.116 -                      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::
  28.117 -                                            Inductive.type_elims)
  28.118 -                      ORELSE' hyp_subst_tac)),
  28.119 -   DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::Inductive.type_intrs) 1)];
  28.120 -
  28.121 -(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
  28.122 -val mk_disj_rls = 
  28.123 -    let fun f rl = rl RS disjI1
  28.124 -        and g rl = rl RS disjI2
  28.125 -    in  accesses_bal(f, g, asm_rl)  end;
  28.126 -
  28.127 -val intrs = ListPair.map (uncurry (prove_goalw_cterm part_rec_defs))
  28.128 -            (map (cterm_of sign) Inductive.intr_tms,
  28.129 -             map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
  28.130 -
  28.131 -(********)
  28.132 -val _ = writeln "  Proving the elimination rule...";
  28.133 -
  28.134 -(*Breaks down logical connectives in the monotonic function*)
  28.135 -val basic_elim_tac =
  28.136 -    REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
  28.137 -              ORELSE' bound_hyp_subst_tac))
  28.138 -    THEN prune_params_tac
  28.139 -        (*Mutual recursion: collapse references to Part(D,h)*)
  28.140 -    THEN fold_tac part_rec_defs;
  28.141 -
  28.142 -in
  28.143 -  struct
  28.144 -  val thy = Inductive.thy
  28.145 -  and defs = big_rec_def :: part_rec_defs
  28.146 -  and bnd_mono   = bnd_mono
  28.147 -  and dom_subset = dom_subset
  28.148 -  and intrs      = intrs;
  28.149 -
  28.150 -  val elim = rule_by_tactic basic_elim_tac 
  28.151 -                  (unfold RS Ind_Syntax.equals_CollectD);
  28.152 -
  28.153 -  (*Applies freeness of the given constructors, which *must* be unfolded by
  28.154 -      the given defs.  Cannot simply use the local con_defs because  
  28.155 -      con_defs=[] for inference systems. 
  28.156 -    String s should have the form t:Si where Si is an inductive set*)
  28.157 -  fun mk_cases defs s = 
  28.158 -      rule_by_tactic (rewrite_goals_tac defs THEN 
  28.159 -                      basic_elim_tac THEN
  28.160 -                      fold_tac defs)
  28.161 -         (assume_read Inductive.thy s  RS  elim)
  28.162 -      |> standard;
  28.163 -
  28.164 -  val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
  28.165 -  and rec_names = rec_names
  28.166 -  end
  28.167 -end;
  28.168 -
    29.1 --- a/src/ZF/intr_elim.thy	Mon Dec 28 16:58:11 1998 +0100
    29.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.3 @@ -1,3 +0,0 @@
    29.4 -(*Dummy theory to document dependencies *)
    29.5 -
    29.6 -intr_elim = "add_ind_def"
    30.1 --- a/src/ZF/mono.ML	Mon Dec 28 16:58:11 1998 +0100
    30.2 +++ b/src/ZF/mono.ML	Mon Dec 28 16:59:28 1998 +0100
    30.3 @@ -6,8 +6,6 @@
    30.4  Monotonicity of various operations (for lattice properties see subset.ML)
    30.5  *)
    30.6  
    30.7 -open mono;
    30.8 -
    30.9  (** Replacement, in its various formulations **)
   30.10  
   30.11  (*Not easy to express monotonicity in P, since any "bigger" predicate
    31.1 --- a/src/ZF/thy_syntax.ML	Mon Dec 28 16:58:11 1998 +0100
    31.2 +++ b/src/ZF/thy_syntax.ML	Mon Dec 28 16:59:28 1998 +0100
    31.3 @@ -9,134 +9,144 @@
    31.4  
    31.5  local
    31.6  
    31.7 -(*Inductive definitions theory section.   co is either "" or "Co"*)
    31.8 -fun inductive_decl co =
    31.9 -  let open ThyParse 
   31.10 -    fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
   31.11 -        if Syntax.is_identifier s then "op " ^ s  else "_"
   31.12 -    fun mk_params ((((((rec_tms, sdom_sum), ipairs), 
   31.13 +
   31.14 +open ThyParse;
   31.15 +
   31.16 +(*ML identifiers for introduction rules.*)
   31.17 +fun mk_intr_name suffix s =  
   31.18 +    if Syntax.is_identifier s then
   31.19 +	"op " ^ s ^ suffix  (*the "op" cancels any infix status*)
   31.20 +    else "_";               (*bad name, don't try to bind*)
   31.21 +
   31.22 +
   31.23 +(*For lists of theorems.  Either a string (an ML list expression) or else
   31.24 +  a list of identifiers.*)
   31.25 +fun optlist s = 
   31.26 +    optional (s $$-- 
   31.27 +	      (string >> strip_quotes
   31.28 +	       || list1 (name>>strip_quotes) >> mk_list)) 
   31.29 +    "[]";
   31.30 +
   31.31 +
   31.32 +(*(Co)Inductive definitions theory section."*)
   31.33 +fun inductive_decl coind =
   31.34 +  let  
   31.35 +    fun mk_params ((((((recs, sdom_sum), ipairs), 
   31.36                        monos), con_defs), type_intrs), type_elims) =
   31.37        let val big_rec_name = space_implode "_" 
   31.38 -                           (map (scan_to_id o trim) rec_tms)
   31.39 -          and srec_tms = mk_list rec_tms
   31.40 +                           (map (scan_to_id o strip_quotes) recs)
   31.41 +          and srec_tms = mk_list recs
   31.42            and sintrs   = mk_big_list (map snd ipairs)
   31.43 -          val stri_name = big_rec_name ^ "_Intrnl"
   31.44 +          and inames   = mk_list (map (mk_intr_name "" o fst) ipairs)
   31.45        in
   31.46 -         (";\n\n\
   31.47 -          \structure " ^ stri_name ^ " =\n\
   31.48 -          \  struct\n\
   31.49 -          \  val _ = writeln \"" ^ co ^ 
   31.50 -                     "Inductive definition " ^ big_rec_name ^ "\"\n\
   31.51 -          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) "
   31.52 -                           ^ srec_tms ^ "\n\
   31.53 -          \  and dom_sum\t= readtm (sign_of thy) Ind_Syntax.iT " ^ sdom_sum ^ "\n\
   31.54 -          \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
   31.55 -                           ^ sintrs ^ "\n\
   31.56 -          \  end;\n\n\
   31.57 -          \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
   31.58 -             stri_name ^ ".rec_tms, " ^
   31.59 -             stri_name ^ ".dom_sum, " ^
   31.60 -             stri_name ^ ".intr_tms)"
   31.61 -         ,
   31.62 -          "structure " ^ big_rec_name ^ " =\n\
   31.63 -          \ let\n\
   31.64 -          \  val _ = writeln \"Proofs for " ^ co ^ 
   31.65 -                     "Inductive definition " ^ big_rec_name ^ "\"\n\
   31.66 -          \  structure Result = " ^ co ^ "Ind_section_Fun\n\
   31.67 -          \\t  (open " ^ stri_name ^ "\n\
   31.68 -          \\t   val thy\t\t= thy\n\
   31.69 -          \\t   val monos\t\t= " ^ monos ^ "\n\
   31.70 -          \\t   val con_defs\t\t= " ^ con_defs ^ "\n\
   31.71 -          \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
   31.72 -          \\t   val type_elims\t= " ^ type_elims ^ ")\n\
   31.73 -          \ in\n\
   31.74 -          \  struct\n\
   31.75 -          \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
   31.76 -          \  open Result\n\
   31.77 -          \  end\n\
   31.78 -          \ end;\n\n\
   31.79 -          \structure " ^ stri_name ^ " = struct end;\n\n"
   31.80 -         )
   31.81 +	 ";\n\n\
   31.82 +	 \local\n\
   31.83 +	 \val (thy, {defs, intrs, elim, mk_cases, \
   31.84 +		    \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
   31.85 +	 \  " ^
   31.86 +	 (if coind then "Co" else "") ^ 
   31.87 +	 "Ind_Package.add_inductive (" ^  srec_tms ^ ", " ^ sdom_sum ^ ", " ^
   31.88 +	  sintrs ^ ", " ^ monos ^ ", " ^ con_defs ^ ", " ^ 
   31.89 +	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
   31.90 +	 \in\n\
   31.91 +	 \structure " ^ big_rec_name ^ " =\n\
   31.92 +	 \struct\n\
   31.93 +	 \  val defs = defs\n\
   31.94 +	 \  val bnd_mono = bnd_mono\n\
   31.95 +	 \  val dom_subset = dom_subset\n\
   31.96 +	 \  val intrs = intrs\n\
   31.97 +	 \  val elim = elim\n\
   31.98 +	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
   31.99 +	 \  val mutual_induct = mutual_induct\n\
  31.100 +	 \  val mk_cases = mk_cases\n\
  31.101 +	 \  val " ^ inames ^ " = intrs\n\
  31.102 +	 \end;\n\
  31.103 +	 \val thy = thy;\nend;\n\
  31.104 +	 \val thy = thy\n"
  31.105        end
  31.106      val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
  31.107      val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
  31.108 -    fun optstring s = optional (s $$-- string >> trim) "[]"
  31.109 -  in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
  31.110 -             -- optstring "type_intrs" -- optstring "type_elims"
  31.111 +  in domains -- ipairs -- optlist "monos" -- optlist "con_defs"
  31.112 +             -- optlist "type_intrs" -- optlist "type_elims"
  31.113       >> mk_params
  31.114    end;
  31.115  
  31.116  
  31.117 -(*Datatype definitions theory section.   co is either "" or "Co"*)
  31.118 -fun datatype_decl co =
  31.119 -  let open ThyParse 
  31.120 -      (*generate strings*)
  31.121 -      fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
  31.122 -      val mk_data = mk_list o map mk_const o snd
  31.123 -      val mk_scons = mk_big_list o map mk_data
  31.124 -      fun mk_intr_name s =  (*the "op" cancels any infix status*)
  31.125 -          if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_"
  31.126 -      fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) =
  31.127 -        let val rec_names = map (scan_to_id o trim o fst) rec_pairs
  31.128 -            val big_rec_name = space_implode "_" rec_names
  31.129 -            and srec_tms = mk_list (map fst rec_pairs)
  31.130 -            and scons    = mk_scons rec_pairs
  31.131 -            and sdom_sum = 
  31.132 -                if dom = "" then  (*default domain: univ or quniv*)
  31.133 -                    "Ind_Syntax." ^ co ^ "data_domain rec_tms"
  31.134 -                else "readtm (sign_of thy) Ind_Syntax.iT " ^ dom
  31.135 -            val stri_name = big_rec_name ^ "_Intrnl"
  31.136 -            val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
  31.137 -        in
  31.138 -           (";\n\n\
  31.139 -            \structure " ^ stri_name ^ " =\n\
  31.140 -            \  struct\n\
  31.141 -            \  val _ = writeln \"" ^ co ^ 
  31.142 -                       "Datatype definition " ^ big_rec_name ^ "\"\n\
  31.143 -            \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) " ^ srec_tms ^ "\n\
  31.144 -            \  val dom_sum\t= " ^ sdom_sum ^ "\n\
  31.145 -            \  and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n" 
  31.146 -                   ^ scons ^ "\n\
  31.147 -            \  val intr_tms\t= Ind_Syntax.mk_all_intr_tms (sign_of thy) (rec_tms, con_ty_lists)\n\
  31.148 -            \  end;\n\n\
  31.149 -            \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ 
  31.150 -                 mk_list (map quote rec_names) ^ ", " ^ 
  31.151 -                 stri_name ^ ".con_ty_lists) \n\
  31.152 -            \              |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
  31.153 -               stri_name ^ ".rec_tms, " ^
  31.154 -               stri_name ^ ".dom_sum, " ^
  31.155 -               stri_name ^ ".intr_tms)"
  31.156 -           ,
  31.157 -            "structure " ^ big_rec_name ^ " =\n\
  31.158 -            \ let\n\
  31.159 -            \  val _ = writeln \"Proofs for " ^ co ^ 
  31.160 -                       "Datatype definition " ^ big_rec_name ^ "\"\n\
  31.161 -            \  structure Result = " ^ co ^ "Data_section_Fun\n\
  31.162 -            \\t  (open " ^ stri_name ^ "\n\
  31.163 -            \\t   val thy\t\t= thy\n\
  31.164 -            \\t   val big_rec_name\t= Sign.intern_const (sign_of thy) \"" ^ big_rec_name ^ "\"\n\
  31.165 -            \\t   val monos\t\t= " ^ monos ^ "\n\
  31.166 -            \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
  31.167 -            \\t   val type_elims\t= " ^ type_elims ^ ");\n\
  31.168 -            \ in\n\
  31.169 -            \  struct\n\
  31.170 -            \  val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
  31.171 -            \  open Result\n\
  31.172 -            \  end\n\
  31.173 -            \ end;\n\n\
  31.174 -            \structure " ^ stri_name ^ " = struct end;\n\n"
  31.175 -           )
  31.176 -        end
  31.177 -      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
  31.178 -      val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
  31.179 -      val construct = name -- string_list -- opt_mixfix;
  31.180 -  in optional ("<=" $$-- string) "" --
  31.181 +(*Datatype definitions theory section.   co is true for codatatypes*)
  31.182 +fun datatype_decl coind =
  31.183 +  let
  31.184 +    (*generate strings*)
  31.185 +    fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
  31.186 +    val mk_data = mk_list o map mk_const o snd
  31.187 +    val mk_scons = mk_big_list o map mk_data
  31.188 +    fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
  31.189 +      let val rec_names = map (scan_to_id o strip_quotes o fst) rec_pairs
  31.190 +	  val big_rec_name = space_implode "_" rec_names
  31.191 +	  and srec_tms = mk_list (map fst rec_pairs)
  31.192 +	  and scons    = mk_scons rec_pairs
  31.193 +	  val con_names = flat (map (map (strip_quotes o #1 o #1) o snd)
  31.194 +				rec_pairs)
  31.195 +          val inames = mk_list (map (mk_intr_name "_I") con_names)
  31.196 +      in
  31.197 +	 ";\n\n\
  31.198 +	 \local\n\
  31.199 +	 \val (thy,\n\
  31.200 +         \     {defs, intrs, elim, mk_cases, \
  31.201 +		    \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
  31.202 +         \     {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\
  31.203 +	 \  " ^
  31.204 +	 (if coind then "Co" else "") ^ 
  31.205 +	 "Data_Package.add_datatype (" ^  sdom ^ ", " ^ srec_tms ^ ", " ^
  31.206 +	  scons ^ ", " ^ monos ^ ", " ^ 
  31.207 +	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
  31.208 +	 \in\n\
  31.209 +	 \structure " ^ big_rec_name ^ " =\n\
  31.210 +	 \struct\n\
  31.211 +	 \  val defs = defs\n\
  31.212 +	 \  val bnd_mono = bnd_mono\n\
  31.213 +	 \  val dom_subset = dom_subset\n\
  31.214 +	 \  val intrs = intrs\n\
  31.215 +	 \  val elim = elim\n\
  31.216 +	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
  31.217 +	 \  val mutual_induct = mutual_induct\n\
  31.218 +	 \  val mk_cases = mk_cases\n\
  31.219 +	 \  val con_defs = con_defs\n\
  31.220 +	 \  val case_eqns = case_eqns\n\
  31.221 +	 \  val recursor_eqns = recursor_eqns\n\
  31.222 +	 \  val free_iffs = free_iffs\n\
  31.223 +	 \  val free_SEs = free_SEs\n\
  31.224 +	 \  val mk_free = mk_free\n\
  31.225 +	 \  val " ^ inames ^ " = intrs;\n\
  31.226 +	 \end;\n\
  31.227 +	 \val thy = thy;\nend;\n\
  31.228 +	 \val thy = thy\n"
  31.229 +      end
  31.230 +    val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
  31.231 +    val construct = name -- string_list -- opt_mixfix;
  31.232 +  in optional ("<=" $$-- string) "\"\"" --
  31.233       enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
  31.234 -     optstring "monos" -- optstring "type_intrs" -- optstring "type_elims"
  31.235 +     optlist "monos" -- optlist "type_intrs" -- optlist "type_elims"
  31.236       >> mk_params
  31.237  end;
  31.238  
  31.239  
  31.240 +(** primrec **)
  31.241 +
  31.242 +fun mk_primrec_decl eqns =
  31.243 +  let val names = map fst eqns
  31.244 +  in
  31.245 +    ";\nval (thy, " ^ mk_list names ^
  31.246 +    ") = PrimrecPackage.add_primrec " ^
  31.247 +      mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
  31.248 +    \val thy = thy\n"
  31.249 +  end;
  31.250 +
  31.251 +(* either names and axioms or just axioms *)
  31.252 +val primrec_decl = 
  31.253 +    ((repeat1 ((ident -- string) || (string >> pair "_")))) >> mk_primrec_decl;
  31.254 +
  31.255 +
  31.256 +
  31.257  
  31.258  (** augment thy syntax **)
  31.259  
  31.260 @@ -146,9 +156,10 @@
  31.261   ["inductive", "coinductive", "datatype", "codatatype", "and", "|",
  31.262    "<=", "domains", "intrs", "monos", "con_defs", "type_intrs",
  31.263    "type_elims"]
  31.264 - [("inductive", inductive_decl ""),
  31.265 -  ("coinductive", inductive_decl "Co"),
  31.266 -  ("datatype", datatype_decl ""),
  31.267 -  ("codatatype", datatype_decl "Co")];
  31.268 + [section "inductive"   "" (inductive_decl false),
  31.269 +  section "coinductive" "" (inductive_decl true),
  31.270 +  section "datatype"    "" (datatype_decl false),
  31.271 +  section "codatatype"  "" (datatype_decl true),
  31.272 +  section "primrec"     "" primrec_decl];
  31.273  
  31.274  end;
    32.1 --- a/src/ZF/typechk.ML	Mon Dec 28 16:58:11 1998 +0100
    32.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.3 @@ -1,33 +0,0 @@
    32.4 -(*  Title:      ZF/typechk
    32.5 -    ID:         $Id$
    32.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    32.7 -    Copyright   1991  University of Cambridge
    32.8 -
    32.9 -Tactics for type checking -- from CTT
   32.10 -*)
   32.11 -
   32.12 -fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
   32.13 -      not (is_Var (head_of a))
   32.14 -  | is_rigid_elem _ = false;
   32.15 -
   32.16 -(*Try solving a:A by assumption provided a is rigid!*) 
   32.17 -val test_assume_tac = SUBGOAL(fn (prem,i) =>
   32.18 -    if is_rigid_elem (Logic.strip_assums_concl prem)
   32.19 -    then  assume_tac i  else  eq_assume_tac i);
   32.20 -
   32.21 -(*Type checking solves a:?A (a rigid, ?A maybe flexible).  
   32.22 -  match_tac is too strict; would refuse to instantiate ?A*)
   32.23 -fun typechk_step_tac tyrls =
   32.24 -    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
   32.25 -
   32.26 -fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
   32.27 -
   32.28 -val ZF_typechecks =
   32.29 -    [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
   32.30 -
   32.31 -(*Instantiates variables in typing conditions.
   32.32 -  drawback: does not simplify conjunctions*)
   32.33 -fun type_auto_tac tyrls hyps = SELECT_GOAL
   32.34 -    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
   32.35 -           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
   32.36 -