# HG changeset patch # User paulson # Date 819626968 -3600 # Node ID f5f97ee67cbb7d41c24ebaade9143a30f3c599ea # Parent c0f6a1887518ca95c2ec13ad93df59a344c1d926 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. diff -r c0f6a1887518 -r f5f97ee67cbb src/ZF/Inductive.ML --- 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); - diff -r c0f6a1887518 -r f5f97ee67cbb src/ZF/add_ind_def.ML --- 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 = diff -r c0f6a1887518 -r f5f97ee67cbb src/ZF/constructor.ML --- 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; diff -r c0f6a1887518 -r f5f97ee67cbb src/ZF/ind_syntax.ML --- 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; diff -r c0f6a1887518 -r f5f97ee67cbb src/ZF/indrule.ML --- 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; diff -r c0f6a1887518 -r f5f97ee67cbb src/ZF/intr_elim.ML --- 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; diff -r c0f6a1887518 -r f5f97ee67cbb src/ZF/thy_syntax.ML --- 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