--- a/src/HOL/indrule.ML Wed Apr 30 13:39:56 1997 +0200
+++ b/src/HOL/indrule.ML Wed Apr 30 13:40:40 1997 +0200
@@ -148,15 +148,20 @@
resolve_tac [allI, impI, conjI, Part_eqI, refl],
dresolve_tac [spec, mp, splitD]];
+val need_mutual = length Intr_elim.rec_names > 1;
+
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 (rewrite_goals_tac [split RS eq_reflection] THEN
- lemma_tac 1)])
- handle e => print_sign_exn sign e;
+ if need_mutual then
+ (writeln " Proving the mutual induction rule...";
+ 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 (rewrite_goals_tac [split RS eq_reflection] THEN
+ lemma_tac 1)])
+ handle e => print_sign_exn sign e)
+ else TrueI;
(*Mutual induction follows by freeness of Inl/Inr.*)
@@ -193,9 +198,8 @@
) i)
THEN mutual_ind_tac prems (i-1);
-val _ = writeln " Proving the mutual induction rule...";
-
val mutual_induct_split =
+ if need_mutual then
prove_goalw_cterm []
(cterm_of sign
(Logic.list_implies (map (induct_prem (Inductive.rec_tms ~~ preds))
@@ -204,7 +208,8 @@
(fn prems =>
[rtac (quant_induct RS lemma) 1,
mutual_ind_tac (rev prems) (length prems)])
- handle e => print_sign_exn sign e;
+ handle e => print_sign_exn sign e
+ else TrueI;
(** Uncurrying the predicate in the ordinary induction rule **)
@@ -224,9 +229,6 @@
induct0));
(*Just "True" unless there's true mutual recursion. This saves storage.*)
- val mutual_induct =
- if length Intr_elim.rec_names > 1
- then Prod_Syntax.remove_split mutual_induct_split
- else TrueI;
+ val mutual_induct = Prod_Syntax.remove_split mutual_induct_split
end
end;