Improving space efficiency of inductive/datatype definitions.
authorpaulson
Fri Dec 22 11:09:28 1995 +0100 (1995-12-22)
changeset 1418f5f97ee67cbb
parent 1417 c0f6a1887518
child 1419 a6a034a47a71
Improving space efficiency of inductive/datatype definitions.
Reduce usage of "open" and change struct open X; D end to
let open X in struct D end end whenever possible -- removes X from the final
structure. Especially needed for functors Intr_elim and Indrule.

intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of
generating a new one. Inductive defs no longer export sumprod_free_SEs

ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM.
It is never used outside, is easily recovered using
bnd_mono and def_lfp_Tarski, and takes up considerable store.

Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items
no longer exported.

mutual_induct is simply "True" unless it is going to be
significantly different from induct -- either because there is mutual
recursion or because it involves tuples.
src/ZF/Inductive.ML
src/ZF/add_ind_def.ML
src/ZF/constructor.ML
src/ZF/ind_syntax.ML
src/ZF/indrule.ML
src/ZF/intr_elim.ML
src/ZF/thy_syntax.ML
     1.1 --- a/src/ZF/Inductive.ML	Fri Dec 22 10:48:59 1995 +0100
     1.2 +++ b/src/ZF/Inductive.ML	Fri Dec 22 11:09:28 1995 +0100
     1.3 @@ -12,8 +12,9 @@
     1.4  Products are used only to derive "streamlined" induction rules for relations
     1.5  *)
     1.6  
     1.7 -local open Ind_Syntax
     1.8 -in
     1.9 +val iT = Ind_Syntax.iT
    1.10 +and oT = Ind_Syntax.oT;
    1.11 +
    1.12  structure Lfp =
    1.13    struct
    1.14    val oper	= Const("lfp",      [iT,iT-->iT]--->iT)
    1.15 @@ -49,21 +50,33 @@
    1.16    val inr_iff	= Inr_iff
    1.17    val distinct	= Inl_Inr_iff
    1.18    val distinct' = Inr_Inl_iff
    1.19 +  val free_SEs  = Ind_Syntax.mk_free_SEs 
    1.20 +            [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
    1.21    end;
    1.22 -end;
    1.23 +
    1.24  
    1.25  functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
    1.26    : sig include INTR_ELIM INDRULE end =
    1.27 -struct
    1.28 -structure Intr_elim = 
    1.29 -    Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
    1.30 -		  Pr=Standard_Prod and Su=Standard_Sum);
    1.31 +let
    1.32 +  structure Intr_elim = 
    1.33 +      Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
    1.34 +		    Pr=Standard_Prod and Su=Standard_Sum);
    1.35  
    1.36 -structure Indrule = 
    1.37 -    Indrule_Fun (structure Inductive=Inductive and 
    1.38 -		 Pr=Standard_Prod and Su=Standard_Sum and Intr_elim=Intr_elim);
    1.39 -
    1.40 -open Intr_elim Indrule
    1.41 +  structure Indrule = 
    1.42 +      Indrule_Fun (structure Inductive=Inductive and 
    1.43 +		   Pr=Standard_Prod and Su=Standard_Sum and 
    1.44 +		       Intr_elim=Intr_elim)
    1.45 +in 
    1.46 +   struct 
    1.47 +   val thy	= Intr_elim.thy
    1.48 +   val defs	= Intr_elim.defs
    1.49 +   val bnd_mono	= Intr_elim.bnd_mono
    1.50 +   val dom_subset = Intr_elim.dom_subset
    1.51 +   val intrs	= Intr_elim.intrs
    1.52 +   val elim	= Intr_elim.elim
    1.53 +   val mk_cases	= Intr_elim.mk_cases
    1.54 +   open Indrule 
    1.55 +   end
    1.56  end;
    1.57  
    1.58  
    1.59 @@ -71,8 +84,6 @@
    1.60      (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
    1.61  
    1.62  
    1.63 -local open Ind_Syntax
    1.64 -in
    1.65  structure Gfp =
    1.66    struct
    1.67    val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
    1.68 @@ -108,8 +119,9 @@
    1.69    val inr_iff	= QInr_iff
    1.70    val distinct	= QInl_QInr_iff
    1.71    val distinct' = QInr_QInl_iff
    1.72 +  val free_SEs  = Ind_Syntax.mk_free_SEs 
    1.73 +            [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
    1.74    end;
    1.75 -end;
    1.76  
    1.77  
    1.78  signature COINDRULE =
    1.79 @@ -121,17 +133,23 @@
    1.80  functor CoInd_section_Fun
    1.81   (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
    1.82      : sig include INTR_ELIM COINDRULE end =
    1.83 -struct
    1.84 -structure Intr_elim = 
    1.85 -    Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
    1.86 -		  Pr=Quine_Prod and Su=Quine_Sum);
    1.87 -
    1.88 -open Intr_elim 
    1.89 -val coinduct = raw_induct
    1.90 +let
    1.91 +  structure Intr_elim = 
    1.92 +      Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
    1.93 +		    Pr=Quine_Prod and Su=Quine_Sum);
    1.94 +in
    1.95 +   struct
    1.96 +   val thy	= Intr_elim.thy
    1.97 +   val defs	= Intr_elim.defs
    1.98 +   val bnd_mono	= Intr_elim.bnd_mono
    1.99 +   val dom_subset = Intr_elim.dom_subset
   1.100 +   val intrs	= Intr_elim.intrs
   1.101 +   val elim	= Intr_elim.elim
   1.102 +   val mk_cases	= Intr_elim.mk_cases
   1.103 +   val coinduct = Intr_elim.raw_induct
   1.104 +   end
   1.105  end;
   1.106  
   1.107 -
   1.108  structure CoInd = 
   1.109      Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
   1.110  
   1.111 -
     2.1 --- a/src/ZF/add_ind_def.ML	Fri Dec 22 10:48:59 1995 +0100
     2.2 +++ b/src/ZF/add_ind_def.ML	Fri Dec 22 11:09:28 1995 +0100
     2.3 @@ -60,6 +60,7 @@
     2.4    val inr_iff	: thm			(*injectivity of inr, using <->*)
     2.5    val distinct	: thm			(*distinctness of inl, inr using <->*)
     2.6    val distinct'	: thm			(*distinctness of inr, inl using <->*)
     2.7 +  val free_SEs  : thm list		(*elim rules for SU, and pair_iff!*)
     2.8    end;
     2.9  
    2.10  signature ADD_INDUCTIVE_DEF =
     3.1 --- a/src/ZF/constructor.ML	Fri Dec 22 10:48:59 1995 +0100
     3.2 +++ b/src/ZF/constructor.ML	Fri Dec 22 11:09:28 1995 +0100
     3.3 @@ -28,14 +28,13 @@
     3.4  (*Proves theorems relating to constructors*)
     3.5  functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
     3.6                        Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
     3.7 -struct
     3.8 -open Logic Const Ind_Syntax;
     3.9 +let
    3.10  
    3.11  (*1st element is the case definition; others are the constructors*)
    3.12 -val big_case_name = big_rec_name ^ "_case";
    3.13 +val big_case_name = Const.big_rec_name ^ "_case";
    3.14  
    3.15 -val con_defs = get_def thy big_case_name :: 
    3.16 -               map (get_def thy o #2) (flat con_ty_lists);
    3.17 +val con_defs = get_def Const.thy big_case_name :: 
    3.18 +               map (get_def Const.thy o #2) (flat Const.con_ty_lists);
    3.19  
    3.20  (** Prove the case theorem **)
    3.21  
    3.22 @@ -48,10 +47,11 @@
    3.23  (*Each equation has the form 
    3.24    rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
    3.25  fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = 
    3.26 -    mk_tprop (eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
    3.27 -		         $ (list_comb (case_free, args))) ;
    3.28 +    Ind_Syntax.mk_tprop
    3.29 +      (Ind_Syntax.eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
    3.30 +       $ (list_comb (case_free, args))) ;
    3.31  
    3.32 -val case_trans = hd con_defs RS def_trans
    3.33 +val case_trans = hd con_defs RS Ind_Syntax.def_trans
    3.34  and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
    3.35  
    3.36  (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
    3.37 @@ -64,26 +64,30 @@
    3.38  
    3.39  fun prove_case_equation (arg,con_def) =
    3.40      prove_goalw_cterm [] 
    3.41 -        (cterm_of (sign_of thy) (mk_case_equation arg))
    3.42 +        (cterm_of (sign_of Const.thy) (mk_case_equation arg))
    3.43          (case_tacsf con_def);
    3.44  
    3.45 -val free_iffs = 
    3.46 -    map standard (con_defs RL [def_swap_iff]) @
    3.47 +val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
    3.48 +
    3.49 +in
    3.50 +  struct
    3.51 +  val con_defs = con_defs
    3.52 +
    3.53 +  val free_iffs = con_iffs @ 
    3.54      [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
    3.55  
    3.56 -val free_SEs   = map (gen_make_elim [conjE,FalseE]) (free_iffs RL [iffD1]);
    3.57 -
    3.58 -val free_cs = ZF_cs addSEs free_SEs;
    3.59 +  val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
    3.60  
    3.61 -(*Typical theorems have the form ~con1=con2, con1=con2==>False,
    3.62 -  con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
    3.63 -fun mk_free s =
    3.64 -    prove_goalw thy con_defs s
    3.65 -      (fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]);
    3.66 +  (*Typical theorems have the form ~con1=con2, con1=con2==>False,
    3.67 +    con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
    3.68 +  fun mk_free s =
    3.69 +      prove_goalw Const.thy con_defs s
    3.70 +	(fn prems => [cut_facts_tac prems 1, 
    3.71 +		      fast_tac (ZF_cs addSEs free_SEs) 1]);
    3.72  
    3.73 -val case_eqns = map prove_case_equation 
    3.74 -		    (flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
    3.75 -
    3.76 +  val case_eqns = map prove_case_equation 
    3.77 +	      (flat Const.con_ty_lists ~~ big_case_args ~~ tl con_defs);
    3.78 +  end
    3.79  end;
    3.80  
    3.81  
     4.1 --- a/src/ZF/ind_syntax.ML	Fri Dec 22 10:48:59 1995 +0100
     4.2 +++ b/src/ZF/ind_syntax.ML	Fri Dec 22 11:09:28 1995 +0100
     4.3 @@ -133,5 +133,14 @@
     4.4  val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
     4.5       (fn _ => [assume_tac 1]);
     4.6  
     4.7 +(*Includes rules for succ and Pair since they are common constructions*)
     4.8 +val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
     4.9 +		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
    4.10 +		make_elim succ_inject, 
    4.11 +		refl_thin, conjE, exE, disjE];
    4.12 +
    4.13 +(*Turns iff rules into safe elimination rules*)
    4.14 +fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
    4.15 +
    4.16  end;
    4.17  
     5.1 --- a/src/ZF/indrule.ML	Fri Dec 22 10:48:59 1995 +0100
     5.2 +++ b/src/ZF/indrule.ML	Fri Dec 22 11:09:28 1995 +0100
     5.3 @@ -17,15 +17,15 @@
     5.4  
     5.5  functor Indrule_Fun
     5.6      (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
     5.7 -     and Pr: PR and Su : SU and Intr_elim: INTR_ELIM) : INDRULE  =
     5.8 -struct
     5.9 -open Logic Ind_Syntax Inductive Intr_elim;
    5.10 +     and Pr: PR and Su : SU and 
    5.11 +     Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE  =
    5.12 +let
    5.13  
    5.14 -val sign = sign_of thy;
    5.15 +val sign = sign_of Inductive.thy;
    5.16  
    5.17 -val (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
    5.18 +val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms);
    5.19  
    5.20 -val big_rec_name = space_implode "_" rec_names;
    5.21 +val big_rec_name = space_implode "_" Intr_elim.rec_names;
    5.22  val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
    5.23  
    5.24  val _ = writeln "  Proving the induction rule...";
    5.25 @@ -42,9 +42,10 @@
    5.26  fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ 
    5.27  		 (Const("op :",_)$t$X), iprems) =
    5.28       (case gen_assoc (op aconv) (ind_alist, X) of
    5.29 -	  Some pred => prem :: mk_tprop (pred $ t) :: iprems
    5.30 +	  Some pred => prem :: Ind_Syntax.mk_tprop (pred $ t) :: iprems
    5.31  	| None => (*possibly membership in M(rec_tm), for M monotone*)
    5.32 -	    let fun mk_sb (rec_tm,pred) = (rec_tm, Collect_const$rec_tm$pred)
    5.33 +	    let fun mk_sb (rec_tm,pred) = 
    5.34 +			(rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
    5.35  	    in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
    5.36    | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
    5.37  
    5.38 @@ -52,11 +53,11 @@
    5.39  fun induct_prem ind_alist intr =
    5.40    let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
    5.41        val iprems = foldr (add_induct_prem ind_alist)
    5.42 -			 (strip_imp_prems intr,[])
    5.43 -      val (t,X) = rule_concl intr
    5.44 +			 (Logic.strip_imp_prems intr,[])
    5.45 +      val (t,X) = Ind_Syntax.rule_concl intr
    5.46        val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
    5.47 -      val concl = mk_tprop (pred $ t)
    5.48 -  in list_all_free (quantfrees, list_implies (iprems,concl)) end
    5.49 +      val concl = Ind_Syntax.mk_tprop (pred $ t)
    5.50 +  in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
    5.51    handle Bind => error"Recursion term not found in conclusion";
    5.52  
    5.53  (*Reduces backtracking by delivering the correct premise to each goal.
    5.54 @@ -66,17 +67,19 @@
    5.55      	DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN
    5.56  	ind_tac prems (i-1);
    5.57  
    5.58 -val pred = Free(pred_name, iT-->oT);
    5.59 +val pred = Free(pred_name, Ind_Syntax.iT --> Ind_Syntax.oT);
    5.60  
    5.61 -val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;
    5.62 +val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
    5.63 +                    Inductive.intr_tms;
    5.64  
    5.65  val quant_induct = 
    5.66      prove_goalw_cterm part_rec_defs 
    5.67 -      (cterm_of sign (list_implies (ind_prems, 
    5.68 -				    mk_tprop (mk_all_imp(big_rec_tm,pred)))))
    5.69 +      (cterm_of sign 
    5.70 +       (Logic.list_implies (ind_prems, 
    5.71 +		Ind_Syntax.mk_tprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))
    5.72        (fn prems =>
    5.73         [rtac (impI RS allI) 1,
    5.74 -	DETERM (etac raw_induct 1),
    5.75 +	DETERM (etac Intr_elim.raw_induct 1),
    5.76  	(*Push Part inside Collect*)
    5.77  	asm_full_simp_tac (FOL_ss addsimps [Part_Collect]) 1,
    5.78  	REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE'
    5.79 @@ -89,9 +92,13 @@
    5.80  
    5.81  (*Sigmas and Cartesian products may nest ONLY to the right!*)
    5.82  fun mk_pred_typ (t $ A $ Abs(_,_,B)) = 
    5.83 -        if t = Pr.sigma  then  iT --> mk_pred_typ B
    5.84 -                         else  iT --> oT
    5.85 -  | mk_pred_typ _           =  iT --> oT
    5.86 +        if t = Pr.sigma  then  Ind_Syntax.iT --> mk_pred_typ B
    5.87 +                         else  Ind_Syntax.iT --> Ind_Syntax.oT
    5.88 +  | mk_pred_typ _           =  Ind_Syntax.iT --> Ind_Syntax.oT
    5.89 +
    5.90 +(*For testing whether the inductive set is a relation*)
    5.91 +fun is_sigma (t$_$_) = (t = Pr.sigma)
    5.92 +  | is_sigma _       =  false;
    5.93  
    5.94  (*Given a recursive set and its domain, return the "fsplit" predicate
    5.95    and a conclusion for the simultaneous induction rule.
    5.96 @@ -100,34 +107,38 @@
    5.97    mutual recursion to invariably be a disjoint sum.*)
    5.98  fun mk_predpair rec_tm = 
    5.99    let val rec_name = (#1 o dest_Const o head_of) rec_tm
   5.100 -      val T = mk_pred_typ dom_sum
   5.101 +      val T = mk_pred_typ Inductive.dom_sum
   5.102        val pfree = Free(pred_name ^ "_" ^ rec_name, T)
   5.103        val frees = mk_frees "za" (binder_types T)
   5.104        val qconcl = 
   5.105 -	foldr mk_all (frees, 
   5.106 -		      imp $ (mem_const $ foldr1 (app Pr.pair) frees $ rec_tm)
   5.107 +	foldr Ind_Syntax.mk_all (frees, 
   5.108 +	                Ind_Syntax.imp $ 
   5.109 +			  (Ind_Syntax.mem_const $ foldr1 (app Pr.pair) frees $
   5.110 +			   rec_tm)
   5.111  			  $ (list_comb (pfree,frees)))
   5.112 -  in  (ap_split Pr.fsplit_const pfree (binder_types T), 
   5.113 +  in  (Ind_Syntax.ap_split Pr.fsplit_const pfree (binder_types T), 
   5.114        qconcl)  
   5.115    end;
   5.116  
   5.117 -val (preds,qconcls) = split_list (map mk_predpair rec_tms);
   5.118 +val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
   5.119  
   5.120  (*Used to form simultaneous induction lemma*)
   5.121  fun mk_rec_imp (rec_tm,pred) = 
   5.122 -    imp $ (mem_const $ Bound 0 $ rec_tm) $  (pred $ Bound 0);
   5.123 +    Ind_Syntax.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $ 
   5.124 +                     (pred $ Bound 0);
   5.125  
   5.126  (*To instantiate the main induction rule*)
   5.127  val induct_concl = 
   5.128 - mk_tprop(mk_all_imp(big_rec_tm,
   5.129 -		     Abs("z", iT, 
   5.130 -			 fold_bal (app conj) 
   5.131 -			          (map mk_rec_imp (rec_tms~~preds)))))
   5.132 -and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
   5.133 + Ind_Syntax.mk_tprop(Ind_Syntax.mk_all_imp(big_rec_tm,
   5.134 +	     Abs("z", Ind_Syntax.iT, 
   5.135 +		 fold_bal (app Ind_Syntax.conj) 
   5.136 +		 (map mk_rec_imp (Inductive.rec_tms~~preds)))))
   5.137 +and mutual_induct_concl =
   5.138 + Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls);
   5.139  
   5.140  val lemma = (*makes the link between the two induction rules*)
   5.141      prove_goalw_cterm part_rec_defs 
   5.142 -	  (cterm_of sign (mk_implies (induct_concl,mutual_induct_concl)))
   5.143 +	  (cterm_of sign (Logic.mk_implies (induct_concl,mutual_induct_concl)))
   5.144  	  (fn prems =>
   5.145  	   [cut_facts_tac prems 1, 
   5.146  	    REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1
   5.147 @@ -141,7 +152,7 @@
   5.148  val mut_ss = 
   5.149      FOL_ss addsimps   [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
   5.150  
   5.151 -val all_defs = con_defs@part_rec_defs;
   5.152 +val all_defs = Inductive.con_defs @ part_rec_defs;
   5.153  
   5.154  (*Removes Collects caused by M-operators in the intro rules.  It is very
   5.155    hard to simplify
   5.156 @@ -149,7 +160,7 @@
   5.157    where t==Part(tf,Inl) and f==Part(tf,Inr) to  list({v: tf. P_t(v)}).
   5.158    Instead the following rules extract the relevant conjunct.
   5.159  *)
   5.160 -val cmonos = [subset_refl RS Collect_mono] RL monos RLN (2,[rev_subsetD]);
   5.161 +val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos RLN (2,[rev_subsetD]);
   5.162  
   5.163  (*Avoids backtracking by delivering the correct premise to each goal*)
   5.164  fun mutual_ind_tac [] 0 = all_tac
   5.165 @@ -164,7 +175,7 @@
   5.166  	   simp_tac (mut_ss addsimps [Part_iff]) 1  THEN
   5.167  	   IF_UNSOLVED (*simp_tac may have finished it off!*)
   5.168  	     ((*simplify assumptions, but don't accept new rewrite rules!*)
   5.169 -	      asm_full_simp_tac (mut_ss setmksimps K[]) 1  THEN
   5.170 +	      asm_full_simp_tac (mut_ss setmksimps (fn _=>[])) 1  THEN
   5.171  	      (*unpackage and use "prem" in the corresponding place*)
   5.172  	      REPEAT (rtac impI 1)  THEN
   5.173  	      rtac (rewrite_rule all_defs prem) 1  THEN
   5.174 @@ -179,8 +190,9 @@
   5.175  val mutual_induct_fsplit = 
   5.176      prove_goalw_cterm []
   5.177  	  (cterm_of sign
   5.178 -	   (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
   5.179 -			  mutual_induct_concl)))
   5.180 +	   (Logic.list_implies 
   5.181 +	      (map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms,
   5.182 +	       mutual_induct_concl)))
   5.183  	  (fn prems =>
   5.184  	   [rtac (quant_induct RS lemma) 1,
   5.185  	    mutual_ind_tac (rev prems) (length prems)]);
   5.186 @@ -191,11 +203,19 @@
   5.187  			      dtac Pr.fsplitD,
   5.188  			      etac Pr.fsplitE,	(*apparently never used!*)
   5.189  			      bound_hyp_subst_tac]))
   5.190 -    THEN prune_params_tac;
   5.191 +    THEN prune_params_tac
   5.192 +
   5.193 +in
   5.194 +  struct
   5.195 +  (*strip quantifier*)
   5.196 +  val induct = standard (quant_induct RS spec RSN (2,rev_mp));
   5.197  
   5.198 -(*strip quantifier*)
   5.199 -val induct = standard (quant_induct RS spec RSN (2,rev_mp));
   5.200 -
   5.201 -val mutual_induct = rule_by_tactic fsplit_tac mutual_induct_fsplit;
   5.202 -
   5.203 +  (*Just "True" unless significantly different from induct, with mutual
   5.204 +    recursion or because it involves tuples.  This saves storage.*)
   5.205 +  val mutual_induct = 
   5.206 +      if length Intr_elim.rec_names > 1 orelse
   5.207 +	 is_sigma Inductive.dom_sum 
   5.208 +      then rule_by_tactic fsplit_tac mutual_induct_fsplit
   5.209 +      else TrueI;
   5.210 +  end
   5.211  end;
     6.1 --- a/src/ZF/intr_elim.ML	Fri Dec 22 10:48:59 1995 +0100
     6.2 +++ b/src/ZF/intr_elim.ML	Fri Dec 22 11:09:28 1995 +0100
     6.3 @@ -15,8 +15,8 @@
     6.4    val type_elims : thm list		(*type-checking elim rules*)
     6.5    end;
     6.6  
     6.7 -(*internal items*)
     6.8 -signature INDUCTIVE_I =
     6.9 +
    6.10 +signature INDUCTIVE_I =		(** Terms read from the theory section **)
    6.11    sig
    6.12    val rec_tms    : term list		(*the recursive sets*)
    6.13    val dom_sum    : term			(*their common domain*)
    6.14 @@ -28,37 +28,39 @@
    6.15    val thy        : theory               (*copy of input theory*)
    6.16    val defs	 : thm list		(*definitions made in thy*)
    6.17    val bnd_mono   : thm			(*monotonicity for the lfp definition*)
    6.18 -  val unfold     : thm			(*fixed-point equation*)
    6.19    val dom_subset : thm			(*inclusion of recursive set in dom*)
    6.20    val intrs      : thm list		(*introduction rules*)
    6.21    val elim       : thm			(*case analysis theorem*)
    6.22 +  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
    6.23 +  end;
    6.24 +
    6.25 +signature INTR_ELIM_AUX =	(** Used to make induction rules **)
    6.26 +  sig
    6.27    val raw_induct : thm			(*raw induction rule from Fp.induct*)
    6.28 -  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
    6.29    val rec_names  : string list		(*names of recursive sets*)
    6.30 -  val sumprod_free_SEs : thm list       (*destruct rules for Su and Pr*)
    6.31    end;
    6.32  
    6.33  (*prove intr/elim rules for a fixedpoint definition*)
    6.34  functor Intr_elim_Fun
    6.35      (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
    6.36 -     and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
    6.37 -struct
    6.38 -open Logic Inductive Ind_Syntax;
    6.39 +     and Fp: FP and Pr : PR and Su : SU) 
    6.40 +    : sig include INTR_ELIM INTR_ELIM_AUX end =
    6.41 +let
    6.42  
    6.43 -val rec_names = map (#1 o dest_Const o head_of) rec_tms;
    6.44 +val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
    6.45  val big_rec_name = space_implode "_" rec_names;
    6.46  
    6.47 -val _ = deny (big_rec_name  mem  map ! (stamps_of_thy thy))
    6.48 +val _ = deny (big_rec_name  mem  map ! (stamps_of_thy Inductive.thy))
    6.49               ("Definition " ^ big_rec_name ^ 
    6.50  	      " would clash with the theory of the same name!");
    6.51  
    6.52  (*fetch fp definitions from the theory*)
    6.53  val big_rec_def::part_rec_defs = 
    6.54 -  map (get_def thy)
    6.55 +  map (get_def Inductive.thy)
    6.56        (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
    6.57  
    6.58  
    6.59 -val sign = sign_of thy;
    6.60 +val sign = sign_of Inductive.thy;
    6.61  
    6.62  (********)
    6.63  val _ = writeln "  Proving monotonicity...";
    6.64 @@ -68,10 +70,10 @@
    6.65  
    6.66  val bnd_mono = 
    6.67      prove_goalw_cterm [] 
    6.68 -      (cterm_of sign (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
    6.69 +      (cterm_of sign (Ind_Syntax.mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
    6.70        (fn _ =>
    6.71         [rtac (Collect_subset RS bnd_monoI) 1,
    6.72 -	REPEAT (ares_tac (basic_monos @ monos) 1)]);
    6.73 +	REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);
    6.74  
    6.75  val dom_subset = standard (big_rec_def RS Fp.subs);
    6.76  
    6.77 @@ -89,7 +91,7 @@
    6.78  (*To type-check recursive occurrences of the inductive sets, possibly
    6.79    enclosed in some monotonic operator M.*)
    6.80  val rec_typechecks = 
    6.81 -   [dom_subset] RL (asm_rl :: ([Part_trans] RL monos)) RL [subsetD];
    6.82 +   [dom_subset] RL (asm_rl :: ([Part_trans] RL Inductive.monos)) RL [subsetD];
    6.83  
    6.84  (*Type-checking is hardest aspect of proof;
    6.85    disjIn selects the correct disjunct after unfolding*)
    6.86 @@ -104,13 +106,14 @@
    6.87       backtracking may occur if the premises have extra variables!*)
    6.88     DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 ORELSE assume_tac 2),
    6.89     (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
    6.90 -   rewrite_goals_tac con_defs,
    6.91 +   rewrite_goals_tac Inductive.con_defs,
    6.92     REPEAT (rtac refl 2),
    6.93     (*Typechecking; this can fail*)
    6.94     REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
    6.95 -		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
    6.96 +		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::
    6.97 +					    Inductive.type_elims)
    6.98  		      ORELSE' hyp_subst_tac)),
    6.99 -   DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::type_intrs) 1)];
   6.100 +   DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::Inductive.type_intrs) 1)];
   6.101  
   6.102  (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
   6.103  val mk_disj_rls = 
   6.104 @@ -119,48 +122,46 @@
   6.105      in  accesses_bal(f, g, asm_rl)  end;
   6.106  
   6.107  val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
   6.108 -            (map (cterm_of sign) intr_tms ~~ 
   6.109 -	     map intro_tacsf (mk_disj_rls(length intr_tms)));
   6.110 +            (map (cterm_of sign) Inductive.intr_tms ~~ 
   6.111 +	     map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
   6.112  
   6.113  (********)
   6.114  val _ = writeln "  Proving the elimination rule...";
   6.115  
   6.116 -(*Includes rules for succ and Pair since they are common constructions*)
   6.117 -val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
   6.118 -		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
   6.119 -		make_elim succ_inject, 
   6.120 -		refl_thin, conjE, exE, disjE];
   6.121 -
   6.122 -(*Standard sum/products for datatypes, variant ones for codatatypes;
   6.123 -  We always include Pair_inject above*)
   6.124 -val sumprod_free_SEs = 
   6.125 -    map (gen_make_elim [conjE,FalseE])
   6.126 -	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
   6.127 -	 RL [iffD1]);
   6.128 -
   6.129  (*Breaks down logical connectives in the monotonic function*)
   6.130  val basic_elim_tac =
   6.131 -    REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
   6.132 +    REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
   6.133  	      ORELSE' bound_hyp_subst_tac))
   6.134      THEN prune_params_tac
   6.135          (*Mutual recursion: collapse references to Part(D,h)*)
   6.136      THEN fold_tac part_rec_defs;
   6.137  
   6.138 -val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
   6.139 +in
   6.140 +  struct
   6.141 +  val thy = Inductive.thy;
   6.142 +
   6.143 +  val defs = big_rec_def :: part_rec_defs;
   6.144  
   6.145 -(*Applies freeness of the given constructors, which *must* be unfolded by
   6.146 -  the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   6.147 -  for inference systems. *)
   6.148 -fun con_elim_tac defs =
   6.149 -    rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
   6.150 +  val bnd_mono   = bnd_mono
   6.151 +  and dom_subset = dom_subset
   6.152 +  and intrs      = intrs;
   6.153 +
   6.154 +  val elim = rule_by_tactic basic_elim_tac 
   6.155 +		  (unfold RS Ind_Syntax.equals_CollectD);
   6.156  
   6.157 -(*String s should have the form t:Si where Si is an inductive set*)
   6.158 -fun mk_cases defs s = 
   6.159 -    rule_by_tactic (con_elim_tac defs)
   6.160 -      (assume_read thy s  RS  elim);
   6.161 +  val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
   6.162  
   6.163 -val defs = big_rec_def :: part_rec_defs;
   6.164 +  (*Applies freeness of the given constructors, which *must* be unfolded by
   6.165 +      the given defs.  Cannot simply use the local con_defs because  
   6.166 +      con_defs=[] for inference systems. 
   6.167 +    String s should have the form t:Si where Si is an inductive set*)
   6.168 +  fun mk_cases defs s = 
   6.169 +      rule_by_tactic (rewrite_goals_tac defs THEN 
   6.170 +		      basic_elim_tac THEN
   6.171 +		      fold_tac defs)
   6.172 +	(assume_read Inductive.thy s  RS  elim);
   6.173  
   6.174 -val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
   6.175 +  val rec_names = rec_names
   6.176 +  end
   6.177  end;
   6.178  
     7.1 --- a/src/ZF/thy_syntax.ML	Fri Dec 22 10:48:59 1995 +0100
     7.2 +++ b/src/ZF/thy_syntax.ML	Fri Dec 22 11:09:28 1995 +0100
     7.3 @@ -24,36 +24,38 @@
     7.4          in
     7.5  	   (";\n\n\
     7.6              \structure " ^ stri_name ^ " =\n\
     7.7 -            \ let open Ind_Syntax in\n\
     7.8              \  struct\n\
     7.9              \  val _ = writeln \"" ^ co ^ 
    7.10  	               "Inductive definition " ^ big_rec_name ^ "\"\n\
    7.11 -            \  val rec_tms\t= map (readtm (sign_of thy) iT) "
    7.12 +            \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) "
    7.13  	                     ^ srec_tms ^ "\n\
    7.14 -            \  and dom_sum\t= readtm (sign_of thy) iT " ^ sdom_sum ^ "\n\
    7.15 +            \  and dom_sum\t= readtm (sign_of thy) Ind_Syntax.iT " ^ sdom_sum ^ "\n\
    7.16              \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
    7.17  	                     ^ sintrs ^ "\n\
    7.18 -            \  end\n\
    7.19 -            \ end;\n\n\
    7.20 +            \  end;\n\n\
    7.21              \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
    7.22  	       stri_name ^ ".rec_tms, " ^
    7.23                 stri_name ^ ".dom_sum, " ^
    7.24                 stri_name ^ ".intr_tms)"
    7.25             ,
    7.26  	    "structure " ^ big_rec_name ^ " =\n\
    7.27 -            \  struct\n\
    7.28 +            \ let\n\
    7.29              \  val _ = writeln \"Proofs for " ^ co ^ 
    7.30  	               "Inductive definition " ^ big_rec_name ^ "\"\n\
    7.31              \  structure Result = " ^ co ^ "Ind_section_Fun\n\
    7.32 -            \  (open " ^ stri_name ^ "\n\
    7.33 -            \   val thy\t\t= thy\n\
    7.34 -            \   val monos\t\t= " ^ monos ^ "\n\
    7.35 -            \   val con_defs\t\t= " ^ con_defs ^ "\n\
    7.36 -            \   val type_intrs\t= " ^ type_intrs ^ "\n\
    7.37 -            \   val type_elims\t= " ^ type_elims ^ ");\n\n\
    7.38 +            \\t  (open " ^ stri_name ^ "\n\
    7.39 +            \\t   val thy\t\t= thy\n\
    7.40 +            \\t   val monos\t\t= " ^ monos ^ "\n\
    7.41 +            \\t   val con_defs\t\t= " ^ con_defs ^ "\n\
    7.42 +            \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
    7.43 +            \\t   val type_elims\t= " ^ type_elims ^ ")\n\
    7.44 +            \ in\n\
    7.45 +            \  struct\n\
    7.46              \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
    7.47              \  open Result\n\
    7.48 -            \  end\n"
    7.49 +            \  end\n\
    7.50 +            \ end;\n\n\
    7.51 +            \structure " ^ stri_name ^ " = struct end;\n\n"
    7.52  	   )
    7.53  	end
    7.54        val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
    7.55 @@ -80,24 +82,23 @@
    7.56  	    and srec_tms = mk_list (map fst rec_pairs)
    7.57              and scons    = mk_scons rec_pairs
    7.58              and sdom_sum = 
    7.59 -		if dom = ""  then co ^ "data_domain rec_tms" (*default*)
    7.60 -		else "readtm (sign_of thy) iT " ^ dom
    7.61 +		if dom = "" then  (*default domain: univ or quniv*)
    7.62 +		    "Ind_Syntax." ^ co ^ "data_domain rec_tms"
    7.63 +		else "readtm (sign_of thy) Ind_Syntax.iT " ^ dom
    7.64              val stri_name = big_rec_name ^ "_Intrnl"
    7.65              val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
    7.66          in
    7.67  	   (";\n\n\
    7.68              \structure " ^ stri_name ^ " =\n\
    7.69 -            \ let open Ind_Syntax in\n\
    7.70              \  struct\n\
    7.71              \  val _ = writeln \"" ^ co ^ 
    7.72  	               "Datatype definition " ^ big_rec_name ^ "\"\n\
    7.73 -            \  val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\
    7.74 +            \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) " ^ srec_tms ^ "\n\
    7.75              \  val dom_sum\t= " ^ sdom_sum ^ "\n\
    7.76 -            \  and con_ty_lists\t= read_constructs (sign_of thy)\n" 
    7.77 +            \  and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n" 
    7.78  	           ^ scons ^ "\n\
    7.79 -            \  val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\
    7.80 -            \  end\n\
    7.81 -            \ end;\n\n\
    7.82 +            \  val intr_tms\t= Ind_Syntax.mk_all_intr_tms (rec_tms, con_ty_lists)\n\
    7.83 +            \  end;\n\n\
    7.84              \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ 
    7.85  	         mk_list (map quote rec_names) ^ ", " ^ 
    7.86                   stri_name ^ ".con_ty_lists) \n\
    7.87 @@ -107,19 +108,23 @@
    7.88                 stri_name ^ ".intr_tms)"
    7.89             ,
    7.90  	    "structure " ^ big_rec_name ^ " =\n\
    7.91 -            \  struct\n\
    7.92 +            \ let\n\
    7.93              \  val _ = writeln \"Proofs for " ^ co ^ 
    7.94  	               "Datatype definition " ^ big_rec_name ^ "\"\n\
    7.95              \  structure Result = " ^ co ^ "Data_section_Fun\n\
    7.96 -            \  (open " ^ stri_name ^ "\n\
    7.97 -            \   val thy\t\t= thy\n\
    7.98 -            \   val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
    7.99 -            \   val monos\t\t= " ^ monos ^ "\n\
   7.100 -            \   val type_intrs\t= " ^ type_intrs ^ "\n\
   7.101 -            \   val type_elims\t= " ^ type_elims ^ ");\n\n\
   7.102 +            \\t  (open " ^ stri_name ^ "\n\
   7.103 +            \\t   val thy\t\t= thy\n\
   7.104 +            \\t   val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
   7.105 +            \\t   val monos\t\t= " ^ monos ^ "\n\
   7.106 +            \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
   7.107 +            \\t   val type_elims\t= " ^ type_elims ^ ");\n\
   7.108 +            \ in\n\
   7.109 +            \  struct\n\
   7.110              \  val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
   7.111              \  open Result\n\
   7.112 -            \  end\n"
   7.113 +            \  end\n\
   7.114 +            \ end;\n\n\
   7.115 +            \structure " ^ stri_name ^ " = struct end;\n\n"
   7.116  	   )
   7.117  	end
   7.118        fun optstring s = optional (s $$-- string) "\"[]\"" >> trim