summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/ZF/indrule.ML

author | paulson |

Fri, 22 Dec 1995 11:09:28 +0100 | |

changeset 1418 | f5f97ee67cbb |

parent 1104 | 141f73abbafc |

child 1461 | 6bcb44e4d6e5 |

permissions | -rw-r--r-- |

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.

(* Title: ZF/indrule.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Induction rule module -- for Inductive/Coinductive Definitions Proves a strong induction rule and a mutual induction rule *) signature INDRULE = sig val induct : thm (*main induction rule*) val mutual_induct : thm (*mutual induction rule*) end; functor Indrule_Fun (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end and Pr: PR and Su : SU and Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE = let val sign = sign_of Inductive.thy; val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms); val big_rec_name = 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..."; (*** Prove the main induction rule ***) val pred_name = "P"; (*name for predicate variables*) val big_rec_def::part_rec_defs = Intr_elim.defs; (*Used to make induction rules; ind_alist = [(rec_tm1,pred1),...] -- associates predicates with rec ops prem is a premise of an intr rule*) fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ (Const("op :",_)$t$X), iprems) = (case gen_assoc (op aconv) (ind_alist, X) of Some pred => prem :: 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, Ind_Syntax.Collect_const$rec_tm$pred) in subst_free (map mk_sb ind_alist) prem :: iprems end) | add_induct_prem ind_alist (prem,iprems) = prem :: iprems; (*Make a premise of the induction rule.*) fun induct_prem ind_alist intr = let val quantfrees = map dest_Free (term_frees intr \\ rec_params) val iprems = foldr (add_induct_prem ind_alist) (Logic.strip_imp_prems intr,[]) val (t,X) = Ind_Syntax.rule_concl intr val (Some pred) = gen_assoc (op aconv) (ind_alist, X) val concl = 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. Intro rules with extra Vars in premises still cause some backtracking *) fun ind_tac [] 0 = all_tac | ind_tac(prem::prems) i = DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN ind_tac prems (i-1); val pred = Free(pred_name, Ind_Syntax.iT --> Ind_Syntax.oT); 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 (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 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' hyp_subst_tac)), ind_tac (rev prems) (length prems) ]); (*** Prove the simultaneous induction rule ***) (*Make distinct predicates for each inductive set*) (*Sigmas and Cartesian products may nest ONLY to the right!*) fun mk_pred_typ (t $ A $ Abs(_,_,B)) = 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. NOTE. This will not work for mutually recursive predicates. Previously a summand 'domt' was also an argument, but this required the domain of mutual recursion to invariably be a disjoint sum.*) fun mk_predpair rec_tm = let val rec_name = (#1 o dest_Const o head_of) rec_tm val 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 Ind_Syntax.mk_all (frees, Ind_Syntax.imp $ (Ind_Syntax.mem_const $ foldr1 (app Pr.pair) frees $ rec_tm) $ (list_comb (pfree,frees))) in (Ind_Syntax.ap_split Pr.fsplit_const pfree (binder_types T), qconcl) end; val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms); (*Used to form simultaneous induction lemma*) fun mk_rec_imp (rec_tm,pred) = Ind_Syntax.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $ (pred $ Bound 0); (*To instantiate the main induction rule*) val induct_concl = 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 (Logic.mk_implies (induct_concl,mutual_induct_concl))) (fn prems => [cut_facts_tac prems 1, REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1 ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1 ORELSE dresolve_tac [spec, mp, Pr.fsplitD] 1)]); (*Mutual induction follows by freeness of Inl/Inr.*) (*Simplification largely reduces the mutual induction rule to the standard rule*) val mut_ss = FOL_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff]; val all_defs = Inductive.con_defs @ part_rec_defs; (*Removes Collects caused by M-operators in the intro rules. It is very hard to simplify list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))}) where t==Part(tf,Inl) and f==Part(tf,Inr) to list({v: tf. P_t(v)}). Instead the following rules extract the relevant conjunct. *) val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos RLN (2,[rev_subsetD]); (*Avoids backtracking by delivering the correct premise to each goal*) fun mutual_ind_tac [] 0 = all_tac | mutual_ind_tac(prem::prems) i = DETERM (SELECT_GOAL ( (*Simplify the assumptions and goal by unfolding Part and using freeness of the Sum constructors; proves all but one conjunct by contradiction*) rewrite_goals_tac all_defs THEN simp_tac (mut_ss addsimps [Part_iff]) 1 THEN IF_UNSOLVED (*simp_tac may have finished it off!*) ((*simplify assumptions, but don't accept new rewrite rules!*) 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 (*prem must not be REPEATed below: could loop!*) DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' eresolve_tac (conjE::mp::cmonos)))) ) i) THEN mutual_ind_tac prems (i-1); val _ = writeln " Proving the mutual induction rule..."; val mutual_induct_fsplit = prove_goalw_cterm [] (cterm_of sign (Logic.list_implies (map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms, mutual_induct_concl))) (fn prems => [rtac (quant_induct RS lemma) 1, mutual_ind_tac (rev prems) (length prems)]); (*Attempts to remove all occurrences of fsplit*) val fsplit_tac = REPEAT (SOMEGOAL (FIRST' [rtac Pr.fsplitI, dtac Pr.fsplitD, etac Pr.fsplitE, (*apparently never used!*) bound_hyp_subst_tac])) THEN prune_params_tac in struct (*strip quantifier*) val induct = standard (quant_induct RS spec RSN (2,rev_mp)); (*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;