# HG changeset patch # User paulson # Date 831571025 -7200 # Node ID fe0b459273f29f09833c33138c0bc0c7b03893b9 # Parent 96244c247b07a9da225d6aa5b3b981731b34776d Predicates are now uncurried in both induction rules, regardless of how tuples are nested. Only returns mutual_induct if there is true mutual recursion. diff -r 96244c247b07 -r fe0b459273f2 src/ZF/indrule.ML --- a/src/ZF/indrule.ML Wed May 08 17:54:07 1996 +0200 +++ b/src/ZF/indrule.ML Wed May 08 17:57:05 1996 +0200 @@ -17,7 +17,7 @@ functor Indrule_Fun (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end - and Pr: PR and Su : SU and + and Pr: PR and CP: CARTPROD and Su : SU and Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE = let @@ -90,15 +90,11 @@ (*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; +(*The components of the element type, several if it is a product*) +val elem_type = CP.pseudo_type Inductive.dom_sum; +val elem_factors = CP.factors elem_type; +val elem_frees = mk_frees "za" elem_factors; +val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees; (*Given a recursive set and its domain, return the "fsplit" predicate and a conclusion for the simultaneous induction rule. @@ -107,17 +103,16 @@ 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 pfree = Free(pred_name ^ "_" ^ rec_name, + elem_factors ---> Ind_Syntax.oT) 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) + foldr Ind_Syntax.mk_all + (elem_frees, + Ind_Syntax.imp $ + (Ind_Syntax.mem_const $ elem_tuple $ rec_tm) + $ (list_comb (pfree, elem_frees))) + in (CP.ap_split elem_type Ind_Syntax.oT pfree, + qconcl) end; val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms); @@ -129,21 +124,26 @@ (*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))))) + 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_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp], + resolve_tac [allI, impI, conjI, Part_eqI], + dresolve_tac [spec, mp, Pr.fsplitD]]; + 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)]); + REPEAT (rewrite_goals_tac [Pr.split_eq] THEN + lemma_tac 1)]); (*Mutual induction follows by freeness of Inl/Inr.*) @@ -197,25 +197,34 @@ [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 + + +(** Uncurrying the predicate in the ordinary induction rule **) + +(*instantiate the variable to a tuple, if it is non-trivial, in order to + allow the predicate to be "opened up". + The name "x.1" comes from the "RS spec" !*) +val inst = + case elem_frees of [_] => I + | _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)), + cterm_of sign elem_tuple)]); + +(*strip quantifier and the implication*) +val induct0 = inst (quant_induct RS spec RSN (2,rev_mp)); + in struct (*strip quantifier*) - val induct = standard (quant_induct RS spec RSN (2,rev_mp)); + val induct = standard + (CP.split_rule_var + (Var((pred_name,2), elem_type --> Ind_Syntax.oT), + induct0)); - (*Just "True" unless significantly different from induct, with mutual - recursion or because it involves tuples. This saves storage.*) + (*Just "True" unless there's true mutual recursion. 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 + if length Intr_elim.rec_names > 1 + then CP.remove_split mutual_induct_fsplit else TrueI; end end; diff -r 96244c247b07 -r fe0b459273f2 src/ZF/indrule.thy --- a/src/ZF/indrule.thy Wed May 08 17:54:07 1996 +0200 +++ b/src/ZF/indrule.thy Wed May 08 17:57:05 1996 +0200 @@ -1,3 +1,3 @@ (*Dummy theory to document dependencies *) -indrule = "ind_syntax" + "intr_elim" +indrule = "ind_syntax" + "cartprod" + "intr_elim"