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.
--- a/src/ZF/Inductive.ML Fri Dec 22 10:48:59 1995 +0100
+++ b/src/ZF/Inductive.ML Fri Dec 22 11:09:28 1995 +0100
@@ -12,8 +12,9 @@
Products are used only to derive "streamlined" induction rules for relations
*)
-local open Ind_Syntax
-in
+val iT = Ind_Syntax.iT
+and oT = Ind_Syntax.oT;
+
structure Lfp =
struct
val oper = Const("lfp", [iT,iT-->iT]--->iT)
@@ -49,21 +50,33 @@
val inr_iff = Inr_iff
val distinct = Inl_Inr_iff
val distinct' = Inr_Inl_iff
+ val free_SEs = Ind_Syntax.mk_free_SEs
+ [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
end;
-end;
+
functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end)
: sig include INTR_ELIM INDRULE end =
-struct
-structure Intr_elim =
- Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and
- Pr=Standard_Prod and Su=Standard_Sum);
+let
+ structure Intr_elim =
+ Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and
+ Pr=Standard_Prod and Su=Standard_Sum);
-structure Indrule =
- Indrule_Fun (structure Inductive=Inductive and
- Pr=Standard_Prod and Su=Standard_Sum and Intr_elim=Intr_elim);
-
-open Intr_elim Indrule
+ structure Indrule =
+ Indrule_Fun (structure Inductive=Inductive and
+ Pr=Standard_Prod and Su=Standard_Sum and
+ Intr_elim=Intr_elim)
+in
+ struct
+ val thy = Intr_elim.thy
+ val defs = Intr_elim.defs
+ val bnd_mono = Intr_elim.bnd_mono
+ val dom_subset = Intr_elim.dom_subset
+ val intrs = Intr_elim.intrs
+ val elim = Intr_elim.elim
+ val mk_cases = Intr_elim.mk_cases
+ open Indrule
+ end
end;
@@ -71,8 +84,6 @@
(structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
-local open Ind_Syntax
-in
structure Gfp =
struct
val oper = Const("gfp", [iT,iT-->iT]--->iT)
@@ -108,8 +119,9 @@
val inr_iff = QInr_iff
val distinct = QInl_QInr_iff
val distinct' = QInr_QInl_iff
+ val free_SEs = Ind_Syntax.mk_free_SEs
+ [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
end;
-end;
signature COINDRULE =
@@ -121,17 +133,23 @@
functor CoInd_section_Fun
(Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end)
: sig include INTR_ELIM COINDRULE end =
-struct
-structure Intr_elim =
- Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and
- Pr=Quine_Prod and Su=Quine_Sum);
-
-open Intr_elim
-val coinduct = raw_induct
+let
+ structure Intr_elim =
+ Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and
+ Pr=Quine_Prod and Su=Quine_Sum);
+in
+ struct
+ val thy = Intr_elim.thy
+ val defs = Intr_elim.defs
+ val bnd_mono = Intr_elim.bnd_mono
+ val dom_subset = Intr_elim.dom_subset
+ val intrs = Intr_elim.intrs
+ val elim = Intr_elim.elim
+ val mk_cases = Intr_elim.mk_cases
+ val coinduct = Intr_elim.raw_induct
+ end
end;
-
structure CoInd =
Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
-
--- a/src/ZF/add_ind_def.ML Fri Dec 22 10:48:59 1995 +0100
+++ b/src/ZF/add_ind_def.ML Fri Dec 22 11:09:28 1995 +0100
@@ -60,6 +60,7 @@
val inr_iff : thm (*injectivity of inr, using <->*)
val distinct : thm (*distinctness of inl, inr using <->*)
val distinct' : thm (*distinctness of inr, inl using <->*)
+ val free_SEs : thm list (*elim rules for SU, and pair_iff!*)
end;
signature ADD_INDUCTIVE_DEF =
--- a/src/ZF/constructor.ML Fri Dec 22 10:48:59 1995 +0100
+++ b/src/ZF/constructor.ML Fri Dec 22 11:09:28 1995 +0100
@@ -28,14 +28,13 @@
(*Proves theorems relating to constructors*)
functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
-struct
-open Logic Const Ind_Syntax;
+let
(*1st element is the case definition; others are the constructors*)
-val big_case_name = big_rec_name ^ "_case";
+val big_case_name = Const.big_rec_name ^ "_case";
-val con_defs = get_def thy big_case_name ::
- map (get_def thy o #2) (flat con_ty_lists);
+val con_defs = get_def Const.thy big_case_name ::
+ map (get_def Const.thy o #2) (flat Const.con_ty_lists);
(** Prove the case theorem **)
@@ -48,10 +47,11 @@
(*Each equation has the form
rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
fun mk_case_equation (((id,T,syn), name, args, prems), case_free) =
- mk_tprop (eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
- $ (list_comb (case_free, args))) ;
+ Ind_Syntax.mk_tprop
+ (Ind_Syntax.eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
+ $ (list_comb (case_free, args))) ;
-val case_trans = hd con_defs RS def_trans
+val case_trans = hd con_defs RS Ind_Syntax.def_trans
and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
(*Proves a single case equation. Could use simp_tac, but it's slower!*)
@@ -64,26 +64,30 @@
fun prove_case_equation (arg,con_def) =
prove_goalw_cterm []
- (cterm_of (sign_of thy) (mk_case_equation arg))
+ (cterm_of (sign_of Const.thy) (mk_case_equation arg))
(case_tacsf con_def);
-val free_iffs =
- map standard (con_defs RL [def_swap_iff]) @
+val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
+
+in
+ struct
+ val con_defs = con_defs
+
+ val free_iffs = con_iffs @
[Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
-val free_SEs = map (gen_make_elim [conjE,FalseE]) (free_iffs RL [iffD1]);
-
-val free_cs = ZF_cs addSEs free_SEs;
+ val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
-(*Typical theorems have the form ~con1=con2, con1=con2==>False,
- con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
-fun mk_free s =
- prove_goalw thy con_defs s
- (fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]);
+ (*Typical theorems have the form ~con1=con2, con1=con2==>False,
+ con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
+ fun mk_free s =
+ prove_goalw Const.thy con_defs s
+ (fn prems => [cut_facts_tac prems 1,
+ fast_tac (ZF_cs addSEs free_SEs) 1]);
-val case_eqns = map prove_case_equation
- (flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
-
+ val case_eqns = map prove_case_equation
+ (flat Const.con_ty_lists ~~ big_case_args ~~ tl con_defs);
+ end
end;
--- a/src/ZF/ind_syntax.ML Fri Dec 22 10:48:59 1995 +0100
+++ b/src/ZF/ind_syntax.ML Fri Dec 22 11:09:28 1995 +0100
@@ -133,5 +133,14 @@
val refl_thin = prove_goal IFOL.thy "!!P. [| a=a; P |] ==> P"
(fn _ => [assume_tac 1]);
+(*Includes rules for succ and Pair since they are common constructions*)
+val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0,
+ Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
+ make_elim succ_inject,
+ refl_thin, conjE, exE, disjE];
+
+(*Turns iff rules into safe elimination rules*)
+fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
+
end;
--- a/src/ZF/indrule.ML Fri Dec 22 10:48:59 1995 +0100
+++ b/src/ZF/indrule.ML Fri Dec 22 11:09:28 1995 +0100
@@ -17,15 +17,15 @@
functor Indrule_Fun
(structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
- and Pr: PR and Su : SU and Intr_elim: INTR_ELIM) : INDRULE =
-struct
-open Logic Ind_Syntax Inductive Intr_elim;
+ and Pr: PR and Su : SU and
+ Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE =
+let
-val sign = sign_of thy;
+val sign = sign_of Inductive.thy;
-val (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
+val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms);
-val big_rec_name = space_implode "_" rec_names;
+val big_rec_name = space_implode "_" Intr_elim.rec_names;
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
val _ = writeln " Proving the induction rule...";
@@ -42,9 +42,10 @@
fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
(Const("op :",_)$t$X), iprems) =
(case gen_assoc (op aconv) (ind_alist, X) of
- Some pred => prem :: mk_tprop (pred $ t) :: iprems
+ Some pred => prem :: Ind_Syntax.mk_tprop (pred $ t) :: iprems
| None => (*possibly membership in M(rec_tm), for M monotone*)
- let fun mk_sb (rec_tm,pred) = (rec_tm, Collect_const$rec_tm$pred)
+ let fun mk_sb (rec_tm,pred) =
+ (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
in subst_free (map mk_sb ind_alist) prem :: iprems end)
| add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
@@ -52,11 +53,11 @@
fun induct_prem ind_alist intr =
let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
val iprems = foldr (add_induct_prem ind_alist)
- (strip_imp_prems intr,[])
- val (t,X) = rule_concl intr
+ (Logic.strip_imp_prems intr,[])
+ val (t,X) = Ind_Syntax.rule_concl intr
val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
- val concl = mk_tprop (pred $ t)
- in list_all_free (quantfrees, list_implies (iprems,concl)) end
+ val concl = Ind_Syntax.mk_tprop (pred $ t)
+ in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
handle Bind => error"Recursion term not found in conclusion";
(*Reduces backtracking by delivering the correct premise to each goal.
@@ -66,17 +67,19 @@
DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN
ind_tac prems (i-1);
-val pred = Free(pred_name, iT-->oT);
+val pred = Free(pred_name, Ind_Syntax.iT --> Ind_Syntax.oT);
-val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;
+val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms))
+ Inductive.intr_tms;
val quant_induct =
prove_goalw_cterm part_rec_defs
- (cterm_of sign (list_implies (ind_prems,
- mk_tprop (mk_all_imp(big_rec_tm,pred)))))
+ (cterm_of sign
+ (Logic.list_implies (ind_prems,
+ Ind_Syntax.mk_tprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))
(fn prems =>
[rtac (impI RS allI) 1,
- DETERM (etac raw_induct 1),
+ DETERM (etac Intr_elim.raw_induct 1),
(*Push Part inside Collect*)
asm_full_simp_tac (FOL_ss addsimps [Part_Collect]) 1,
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE'
@@ -89,9 +92,13 @@
(*Sigmas and Cartesian products may nest ONLY to the right!*)
fun mk_pred_typ (t $ A $ Abs(_,_,B)) =
- if t = Pr.sigma then iT --> mk_pred_typ B
- else iT --> oT
- | mk_pred_typ _ = iT --> oT
+ if t = Pr.sigma then Ind_Syntax.iT --> mk_pred_typ B
+ else Ind_Syntax.iT --> Ind_Syntax.oT
+ | mk_pred_typ _ = Ind_Syntax.iT --> Ind_Syntax.oT
+
+(*For testing whether the inductive set is a relation*)
+fun is_sigma (t$_$_) = (t = Pr.sigma)
+ | is_sigma _ = false;
(*Given a recursive set and its domain, return the "fsplit" predicate
and a conclusion for the simultaneous induction rule.
@@ -100,34 +107,38 @@
mutual recursion to invariably be a disjoint sum.*)
fun mk_predpair rec_tm =
let val rec_name = (#1 o dest_Const o head_of) rec_tm
- val T = mk_pred_typ dom_sum
+ val T = mk_pred_typ Inductive.dom_sum
val pfree = Free(pred_name ^ "_" ^ rec_name, T)
val frees = mk_frees "za" (binder_types T)
val qconcl =
- foldr mk_all (frees,
- imp $ (mem_const $ foldr1 (app Pr.pair) frees $ rec_tm)
+ foldr Ind_Syntax.mk_all (frees,
+ Ind_Syntax.imp $
+ (Ind_Syntax.mem_const $ foldr1 (app Pr.pair) frees $
+ rec_tm)
$ (list_comb (pfree,frees)))
- in (ap_split Pr.fsplit_const pfree (binder_types T),
+ in (Ind_Syntax.ap_split Pr.fsplit_const pfree (binder_types T),
qconcl)
end;
-val (preds,qconcls) = split_list (map mk_predpair rec_tms);
+val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
(*Used to form simultaneous induction lemma*)
fun mk_rec_imp (rec_tm,pred) =
- imp $ (mem_const $ Bound 0 $ rec_tm) $ (pred $ Bound 0);
+ Ind_Syntax.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $
+ (pred $ Bound 0);
(*To instantiate the main induction rule*)
val induct_concl =
- mk_tprop(mk_all_imp(big_rec_tm,
- Abs("z", iT,
- fold_bal (app conj)
- (map mk_rec_imp (rec_tms~~preds)))))
-and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
+ Ind_Syntax.mk_tprop(Ind_Syntax.mk_all_imp(big_rec_tm,
+ Abs("z", Ind_Syntax.iT,
+ fold_bal (app Ind_Syntax.conj)
+ (map mk_rec_imp (Inductive.rec_tms~~preds)))))
+and mutual_induct_concl =
+ Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls);
val lemma = (*makes the link between the two induction rules*)
prove_goalw_cterm part_rec_defs
- (cterm_of sign (mk_implies (induct_concl,mutual_induct_concl)))
+ (cterm_of sign (Logic.mk_implies (induct_concl,mutual_induct_concl)))
(fn prems =>
[cut_facts_tac prems 1,
REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1
@@ -141,7 +152,7 @@
val mut_ss =
FOL_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
-val all_defs = con_defs@part_rec_defs;
+val all_defs = Inductive.con_defs @ part_rec_defs;
(*Removes Collects caused by M-operators in the intro rules. It is very
hard to simplify
@@ -149,7 +160,7 @@
where t==Part(tf,Inl) and f==Part(tf,Inr) to list({v: tf. P_t(v)}).
Instead the following rules extract the relevant conjunct.
*)
-val cmonos = [subset_refl RS Collect_mono] RL monos RLN (2,[rev_subsetD]);
+val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos RLN (2,[rev_subsetD]);
(*Avoids backtracking by delivering the correct premise to each goal*)
fun mutual_ind_tac [] 0 = all_tac
@@ -164,7 +175,7 @@
simp_tac (mut_ss addsimps [Part_iff]) 1 THEN
IF_UNSOLVED (*simp_tac may have finished it off!*)
((*simplify assumptions, but don't accept new rewrite rules!*)
- asm_full_simp_tac (mut_ss setmksimps K[]) 1 THEN
+ asm_full_simp_tac (mut_ss setmksimps (fn _=>[])) 1 THEN
(*unpackage and use "prem" in the corresponding place*)
REPEAT (rtac impI 1) THEN
rtac (rewrite_rule all_defs prem) 1 THEN
@@ -179,8 +190,9 @@
val mutual_induct_fsplit =
prove_goalw_cterm []
(cterm_of sign
- (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
- mutual_induct_concl)))
+ (Logic.list_implies
+ (map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms,
+ mutual_induct_concl)))
(fn prems =>
[rtac (quant_induct RS lemma) 1,
mutual_ind_tac (rev prems) (length prems)]);
@@ -191,11 +203,19 @@
dtac Pr.fsplitD,
etac Pr.fsplitE, (*apparently never used!*)
bound_hyp_subst_tac]))
- THEN prune_params_tac;
+ THEN prune_params_tac
+
+in
+ struct
+ (*strip quantifier*)
+ val induct = standard (quant_induct RS spec RSN (2,rev_mp));
-(*strip quantifier*)
-val induct = standard (quant_induct RS spec RSN (2,rev_mp));
-
-val mutual_induct = rule_by_tactic fsplit_tac mutual_induct_fsplit;
-
+ (*Just "True" unless significantly different from induct, with mutual
+ recursion or because it involves tuples. This saves storage.*)
+ val mutual_induct =
+ if length Intr_elim.rec_names > 1 orelse
+ is_sigma Inductive.dom_sum
+ then rule_by_tactic fsplit_tac mutual_induct_fsplit
+ else TrueI;
+ end
end;
--- a/src/ZF/intr_elim.ML Fri Dec 22 10:48:59 1995 +0100
+++ b/src/ZF/intr_elim.ML Fri Dec 22 11:09:28 1995 +0100
@@ -15,8 +15,8 @@
val type_elims : thm list (*type-checking elim rules*)
end;
-(*internal items*)
-signature INDUCTIVE_I =
+
+signature INDUCTIVE_I = (** Terms read from the theory section **)
sig
val rec_tms : term list (*the recursive sets*)
val dom_sum : term (*their common domain*)
@@ -28,37 +28,39 @@
val thy : theory (*copy of input theory*)
val defs : thm list (*definitions made in thy*)
val bnd_mono : thm (*monotonicity for the lfp definition*)
- val unfold : thm (*fixed-point equation*)
val dom_subset : thm (*inclusion of recursive set in dom*)
val intrs : thm list (*introduction rules*)
val elim : thm (*case analysis theorem*)
+ val mk_cases : thm list -> string -> thm (*generates case theorems*)
+ end;
+
+signature INTR_ELIM_AUX = (** Used to make induction rules **)
+ sig
val raw_induct : thm (*raw induction rule from Fp.induct*)
- val mk_cases : thm list -> string -> thm (*generates case theorems*)
val rec_names : string list (*names of recursive sets*)
- val sumprod_free_SEs : thm list (*destruct rules for Su and Pr*)
end;
(*prove intr/elim rules for a fixedpoint definition*)
functor Intr_elim_Fun
(structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
- and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
-struct
-open Logic Inductive Ind_Syntax;
+ and Fp: FP and Pr : PR and Su : SU)
+ : sig include INTR_ELIM INTR_ELIM_AUX end =
+let
-val rec_names = map (#1 o dest_Const o head_of) rec_tms;
+val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
val big_rec_name = space_implode "_" rec_names;
-val _ = deny (big_rec_name mem map ! (stamps_of_thy thy))
+val _ = deny (big_rec_name mem map ! (stamps_of_thy Inductive.thy))
("Definition " ^ big_rec_name ^
" would clash with the theory of the same name!");
(*fetch fp definitions from the theory*)
val big_rec_def::part_rec_defs =
- map (get_def thy)
+ map (get_def Inductive.thy)
(case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
-val sign = sign_of thy;
+val sign = sign_of Inductive.thy;
(********)
val _ = writeln " Proving monotonicity...";
@@ -68,10 +70,10 @@
val bnd_mono =
prove_goalw_cterm []
- (cterm_of sign (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
+ (cterm_of sign (Ind_Syntax.mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
(fn _ =>
[rtac (Collect_subset RS bnd_monoI) 1,
- REPEAT (ares_tac (basic_monos @ monos) 1)]);
+ REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);
val dom_subset = standard (big_rec_def RS Fp.subs);
@@ -89,7 +91,7 @@
(*To type-check recursive occurrences of the inductive sets, possibly
enclosed in some monotonic operator M.*)
val rec_typechecks =
- [dom_subset] RL (asm_rl :: ([Part_trans] RL monos)) RL [subsetD];
+ [dom_subset] RL (asm_rl :: ([Part_trans] RL Inductive.monos)) RL [subsetD];
(*Type-checking is hardest aspect of proof;
disjIn selects the correct disjunct after unfolding*)
@@ -104,13 +106,14 @@
backtracking may occur if the premises have extra variables!*)
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 ORELSE assume_tac 2),
(*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
- rewrite_goals_tac con_defs,
+ rewrite_goals_tac Inductive.con_defs,
REPEAT (rtac refl 2),
(*Typechecking; this can fail*)
REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks
- ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
+ ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::
+ Inductive.type_elims)
ORELSE' hyp_subst_tac)),
- DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::type_intrs) 1)];
+ DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::Inductive.type_intrs) 1)];
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
val mk_disj_rls =
@@ -119,48 +122,46 @@
in accesses_bal(f, g, asm_rl) end;
val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
- (map (cterm_of sign) intr_tms ~~
- map intro_tacsf (mk_disj_rls(length intr_tms)));
+ (map (cterm_of sign) Inductive.intr_tms ~~
+ map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
(********)
val _ = writeln " Proving the elimination rule...";
-(*Includes rules for succ and Pair since they are common constructions*)
-val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0,
- Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
- make_elim succ_inject,
- refl_thin, conjE, exE, disjE];
-
-(*Standard sum/products for datatypes, variant ones for codatatypes;
- We always include Pair_inject above*)
-val sumprod_free_SEs =
- map (gen_make_elim [conjE,FalseE])
- ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]
- RL [iffD1]);
-
(*Breaks down logical connectives in the monotonic function*)
val basic_elim_tac =
- REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
+ REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
ORELSE' bound_hyp_subst_tac))
THEN prune_params_tac
(*Mutual recursion: collapse references to Part(D,h)*)
THEN fold_tac part_rec_defs;
-val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
+in
+ struct
+ val thy = Inductive.thy;
+
+ val defs = big_rec_def :: part_rec_defs;
-(*Applies freeness of the given constructors, which *must* be unfolded by
- the given defs. Cannot simply use the local con_defs because con_defs=[]
- for inference systems. *)
-fun con_elim_tac defs =
- rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
+ val bnd_mono = bnd_mono
+ and dom_subset = dom_subset
+ and intrs = intrs;
+
+ val elim = rule_by_tactic basic_elim_tac
+ (unfold RS Ind_Syntax.equals_CollectD);
-(*String s should have the form t:Si where Si is an inductive set*)
-fun mk_cases defs s =
- rule_by_tactic (con_elim_tac defs)
- (assume_read thy s RS elim);
+ val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
-val defs = big_rec_def :: part_rec_defs;
+ (*Applies freeness of the given constructors, which *must* be unfolded by
+ the given defs. Cannot simply use the local con_defs because
+ con_defs=[] for inference systems.
+ String s should have the form t:Si where Si is an inductive set*)
+ fun mk_cases defs s =
+ rule_by_tactic (rewrite_goals_tac defs THEN
+ basic_elim_tac THEN
+ fold_tac defs)
+ (assume_read Inductive.thy s RS elim);
-val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
+ val rec_names = rec_names
+ end
end;
--- a/src/ZF/thy_syntax.ML Fri Dec 22 10:48:59 1995 +0100
+++ b/src/ZF/thy_syntax.ML Fri Dec 22 11:09:28 1995 +0100
@@ -24,36 +24,38 @@
in
(";\n\n\
\structure " ^ stri_name ^ " =\n\
- \ let open Ind_Syntax in\n\
\ struct\n\
\ val _ = writeln \"" ^ co ^
"Inductive definition " ^ big_rec_name ^ "\"\n\
- \ val rec_tms\t= map (readtm (sign_of thy) iT) "
+ \ val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) "
^ srec_tms ^ "\n\
- \ and dom_sum\t= readtm (sign_of thy) iT " ^ sdom_sum ^ "\n\
+ \ and dom_sum\t= readtm (sign_of thy) Ind_Syntax.iT " ^ sdom_sum ^ "\n\
\ and intr_tms\t= map (readtm (sign_of thy) propT)\n"
^ sintrs ^ "\n\
- \ end\n\
- \ end;\n\n\
+ \ end;\n\n\
\val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^
stri_name ^ ".rec_tms, " ^
stri_name ^ ".dom_sum, " ^
stri_name ^ ".intr_tms)"
,
"structure " ^ big_rec_name ^ " =\n\
- \ struct\n\
+ \ let\n\
\ val _ = writeln \"Proofs for " ^ co ^
"Inductive definition " ^ big_rec_name ^ "\"\n\
\ structure Result = " ^ co ^ "Ind_section_Fun\n\
- \ (open " ^ stri_name ^ "\n\
- \ val thy\t\t= thy\n\
- \ val monos\t\t= " ^ monos ^ "\n\
- \ val con_defs\t\t= " ^ con_defs ^ "\n\
- \ val type_intrs\t= " ^ type_intrs ^ "\n\
- \ val type_elims\t= " ^ type_elims ^ ");\n\n\
+ \\t (open " ^ stri_name ^ "\n\
+ \\t val thy\t\t= thy\n\
+ \\t val monos\t\t= " ^ monos ^ "\n\
+ \\t val con_defs\t\t= " ^ con_defs ^ "\n\
+ \\t val type_intrs\t= " ^ type_intrs ^ "\n\
+ \\t val type_elims\t= " ^ type_elims ^ ")\n\
+ \ in\n\
+ \ struct\n\
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
\ open Result\n\
- \ end\n"
+ \ end\n\
+ \ end;\n\n\
+ \structure " ^ stri_name ^ " = struct end;\n\n"
)
end
val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
@@ -80,24 +82,23 @@
and srec_tms = mk_list (map fst rec_pairs)
and scons = mk_scons rec_pairs
and sdom_sum =
- if dom = "" then co ^ "data_domain rec_tms" (*default*)
- else "readtm (sign_of thy) iT " ^ dom
+ if dom = "" then (*default domain: univ or quniv*)
+ "Ind_Syntax." ^ co ^ "data_domain rec_tms"
+ else "readtm (sign_of thy) Ind_Syntax.iT " ^ dom
val stri_name = big_rec_name ^ "_Intrnl"
val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
in
(";\n\n\
\structure " ^ stri_name ^ " =\n\
- \ let open Ind_Syntax in\n\
\ struct\n\
\ val _ = writeln \"" ^ co ^
"Datatype definition " ^ big_rec_name ^ "\"\n\
- \ val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\
+ \ val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) " ^ srec_tms ^ "\n\
\ val dom_sum\t= " ^ sdom_sum ^ "\n\
- \ and con_ty_lists\t= read_constructs (sign_of thy)\n"
+ \ and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n"
^ scons ^ "\n\
- \ val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\
- \ end\n\
- \ end;\n\n\
+ \ val intr_tms\t= Ind_Syntax.mk_all_intr_tms (rec_tms, con_ty_lists)\n\
+ \ end;\n\n\
\val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^
mk_list (map quote rec_names) ^ ", " ^
stri_name ^ ".con_ty_lists) \n\
@@ -107,19 +108,23 @@
stri_name ^ ".intr_tms)"
,
"structure " ^ big_rec_name ^ " =\n\
- \ struct\n\
+ \ let\n\
\ val _ = writeln \"Proofs for " ^ co ^
"Datatype definition " ^ big_rec_name ^ "\"\n\
\ structure Result = " ^ co ^ "Data_section_Fun\n\
- \ (open " ^ stri_name ^ "\n\
- \ val thy\t\t= thy\n\
- \ val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
- \ val monos\t\t= " ^ monos ^ "\n\
- \ val type_intrs\t= " ^ type_intrs ^ "\n\
- \ val type_elims\t= " ^ type_elims ^ ");\n\n\
+ \\t (open " ^ stri_name ^ "\n\
+ \\t val thy\t\t= thy\n\
+ \\t val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
+ \\t val monos\t\t= " ^ monos ^ "\n\
+ \\t val type_intrs\t= " ^ type_intrs ^ "\n\
+ \\t val type_elims\t= " ^ type_elims ^ ");\n\
+ \ in\n\
+ \ struct\n\
\ val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
\ open Result\n\
- \ end\n"
+ \ end\n\
+ \ end;\n\n\
+ \structure " ^ stri_name ^ " = struct end;\n\n"
)
end
fun optstring s = optional (s $$-- string) "\"[]\"" >> trim