--- a/src/HOL/ind_syntax.ML Tue May 07 18:14:39 1996 +0200
+++ b/src/HOL/ind_syntax.ML Tue May 07 18:15:51 1996 +0200
@@ -37,8 +37,8 @@
fun mk_prod (T1,T2) = Type("*", [T1,T2]);
-(*Maps the type T1*...*Tn to [T1,...,Tn], if nested to the right*)
-fun factors (Type("*", [T1,T2])) = T1 :: factors T2
+(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
+fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
| factors T = [T];
(*Make a correctly typed ordered pair*)
@@ -50,21 +50,41 @@
fun split_const(Ta,Tb,Tc) =
Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
-(*Given u expecting arguments of types [T1,...,Tn], create term of
- type T1*...*Tn => Tc using split. Here * associates to the LEFT*)
-fun ap_split_l Tc u [ ] = Abs("null", unitT, u)
- | ap_split_l Tc u [_] = u
- | ap_split_l Tc u (Ta::Tb::Ts) = ap_split_l Tc (split_const(Ta,Tb,Tc) $ u)
- (mk_prod(Ta,Tb) :: Ts);
+(*In ap_split S T u, term u expects separate arguments for the factors of S,
+ with result type T. The call creates a new term expecting one argument
+ of type S.*)
+fun ap_split (Type("*", [T1,T2])) T3 u =
+ split_const(T1,T2,T3) $
+ Abs("v", T1,
+ ap_split T2 T3
+ ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $
+ Bound 0))
+ | ap_split T T3 u = u;
+
+(*Makes a nested tuple from a list, following the product type structure*)
+fun mk_tuple (Type("*", [T1,T2])) tms =
+ mk_Pair (mk_tuple T1 tms,
+ mk_tuple T2 (drop (length (factors T1), tms)))
+ | mk_tuple T (t::_) = t;
-(*Given u expecting arguments of types [T1,...,Tn], create term of
- type T1*...*Tn => i using split. Here * associates to the RIGHT*)
-fun ap_split Tc u [ ] = Abs("null", unitT, u)
- | ap_split Tc u [_] = u
- | ap_split Tc u [Ta,Tb] = split_const(Ta,Tb,Tc) $ u
- | ap_split Tc u (Ta::Ts) =
- split_const(Ta, foldr1 mk_prod Ts, Tc) $
- (Abs("v", Ta, ap_split Tc (u $ Bound(length Ts - 2)) Ts));
+(*Attempts to remove occurrences of split, and pair-valued parameters*)
+val remove_split = rewrite_rule [split RS eq_reflection] o
+ rule_by_tactic (ALLGOALS split_all_tac);
+
+(*Uncurries any Var of function type in the rule*)
+fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
+ let val T' = factors T1 ---> T2
+ val newt = ap_split T1 T2 (Var(v,T'))
+ val cterm = Thm.cterm_of (#sign(rep_thm rl))
+ in
+ remove_split (instantiate ([], [(cterm t, cterm newt)]) rl)
+ end
+ | split_rule_var (t,rl) = rl;
+
+(*Uncurries ALL function variables occurring in a rule's conclusion*)
+fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl)
+ |> standard;
+
(** Disjoint sum type **)
--- a/src/HOL/indrule.ML Tue May 07 18:14:39 1996 +0200
+++ b/src/HOL/indrule.ML Tue May 07 18:15:51 1996 +0200
@@ -99,23 +99,26 @@
(*** Prove the simultaneous induction rule ***)
(*Make distinct predicates for each inductive set.
- Splits cartesian products in elem_type, IF nested to the right! *)
+ Splits cartesian products in elem_type, however nested*)
+
+(*The components of the element type, several if it is a product*)
+val elem_factors = Ind_Syntax.factors elem_type;
+val elem_frees = mk_frees "za" elem_factors;
+val elem_tuple = Ind_Syntax.mk_tuple elem_type elem_frees;
(*Given a recursive set, return the "split" predicate
and a conclusion for the simultaneous induction rule*)
fun mk_predpair rec_tm =
let val rec_name = (#1 o dest_Const o head_of) rec_tm
- val T = Ind_Syntax.factors elem_type ---> Ind_Syntax.boolT
- 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.boolT)
val qconcl =
foldr Ind_Syntax.mk_all
- (frees,
- Ind_Syntax.imp $ (Ind_Syntax.mk_mem
- (foldr1 Ind_Syntax.mk_Pair frees, rec_tm))
- $ (list_comb (pfree,frees)))
- in (Ind_Syntax.ap_split Ind_Syntax.boolT pfree (binder_types T),
- qconcl)
+ (elem_frees,
+ Ind_Syntax.imp $ (Ind_Syntax.mk_mem (elem_tuple, rec_tm))
+ $ (list_comb (pfree, elem_frees)))
+ in (Ind_Syntax.ap_split elem_type Ind_Syntax.boolT pfree,
+ qconcl)
end;
val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
@@ -135,15 +138,18 @@
and mutual_induct_concl =
Ind_Syntax.mk_Trueprop (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, refl],
+ dresolve_tac [spec, mp, splitD]];
+
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, refl] 1
- ORELSE dresolve_tac [spec, mp, splitD] 1)])
+ REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN
+ lemma_tac 1)])
handle e => print_sign_exn sign e;
(*Mutual induction follows by freeness of Inl/Inr.*)
@@ -151,9 +157,9 @@
(*Simplification largely reduces the mutual induction rule to the
standard rule*)
val mut_ss = simpset_of "Fun"
- addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq];
+ addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split];
-val all_defs = Inductive.con_defs @ part_rec_defs;
+val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs;
(*Removes Collects caused by M-operators in the intro rules*)
val cmonos = [subset_refl RS Int_Collect_mono] RL Inductive.monos RLN
@@ -172,7 +178,7 @@
simp_tac (mut_ss addsimps [Part_def]) 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
+ full_simp_tac mut_ss 1 THEN
(*unpackage and use "prem" in the corresponding place*)
REPEAT (rtac impI 1) THEN
rtac (rewrite_rule all_defs prem) 1 THEN
@@ -195,23 +201,27 @@
mutual_ind_tac (rev prems) (length prems)])
handle e => print_sign_exn sign e;
-(*Attempts to remove all occurrences of split*)
-val split_tac =
- REPEAT (SOMEGOAL (FIRST' [rtac splitI,
- dtac splitD,
- etac splitE,
- bound_hyp_subst_tac]))
- THEN prune_params_tac;
+(** Uncurrying the predicate in the ordinary induction rule **)
+
+(*The name "x.1" comes from the "RS spec" !*)
+val xvar = cterm_of sign (Var(("x",1), elem_type));
+
+(*strip quantifier and instantiate the variable to a tuple*)
+val induct0 = quant_induct RS spec RSN (2,rev_mp) |>
+ freezeT |> (*Because elem_type contains TFrees not TVars*)
+ instantiate ([], [(xvar, cterm_of sign elem_tuple)]);
in
struct
- (*strip quantifier*)
- val induct = standard (quant_induct RS spec RSN (2,rev_mp));
+ val induct = standard
+ (Ind_Syntax.split_rule_var
+ (Var((pred_name,2), elem_type --> Ind_Syntax.boolT),
+ induct0));
+ (*Just "True" unless there's true mutual recursion. This saves storage.*)
val mutual_induct =
- if length Intr_elim.rec_names > 1 orelse
- length (Ind_Syntax.factors elem_type) > 1
- then rule_by_tactic split_tac mutual_induct_split
+ if length Intr_elim.rec_names > 1
+ then Ind_Syntax.remove_split mutual_induct_split
else TrueI;
end
end;