--- a/src/HOL/indrule.ML Wed May 27 12:21:39 1998 +0200
+++ b/src/HOL/indrule.ML Wed May 27 12:22:32 1998 +0200
@@ -108,6 +108,11 @@
ind_tac (rev prems) (length prems)])
handle e => print_sign_exn sign e;
+val _ = if !Ind_Syntax.trace then
+ (writeln "quant_induct = "; print_thm quant_induct)
+ else ();
+
+
(*** Prove the simultaneous induction rule ***)
(*Make distinct predicates for each inductive set.
@@ -150,6 +155,14 @@
and mutual_induct_concl =
Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls);
+val _ = if !Ind_Syntax.trace then
+ (writeln ("induct_concl = " ^
+ Sign.string_of_term sign induct_concl);
+ writeln ("mutual_induct_concl = " ^
+ Sign.string_of_term sign mutual_induct_concl))
+ else ();
+
+
val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
resolve_tac [allI, impI, conjI, Part_eqI, refl],
dresolve_tac [spec, mp, splitD]];
@@ -170,6 +183,11 @@
else (writeln " [ No mutual induction rule needed ]";
TrueI);
+val _ = if !Ind_Syntax.trace then
+ (writeln "lemma = "; print_thm lemma)
+ else ();
+
+
(*Mutual induction follows by freeness of Inl/Inr.*)
(*Simplification largely reduces the mutual induction rule to the
--- a/src/ZF/indrule.ML Wed May 27 12:21:39 1998 +0200
+++ b/src/ZF/indrule.ML Wed May 27 12:22:32 1998 +0200
@@ -108,6 +108,11 @@
ORELSE' hyp_subst_tac)),
ind_tac (rev prems) (length prems) ]);
+val _ = if !Ind_Syntax.trace then
+ (writeln "quant_induct = "; print_thm quant_induct)
+ else ();
+
+
(*** Prove the simultaneous induction rule ***)
(*Make distinct predicates for each inductive set*)
@@ -155,6 +160,14 @@
and mutual_induct_concl =
FOLogic.mk_Trueprop(fold_bal (app FOLogic.conj) qconcls);
+val _ = if !Ind_Syntax.trace then
+ (writeln ("induct_concl = " ^
+ Sign.string_of_term sign induct_concl);
+ writeln ("mutual_induct_concl = " ^
+ Sign.string_of_term sign mutual_induct_concl))
+ else ();
+
+
val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
resolve_tac [allI, impI, conjI, Part_eqI],
dresolve_tac [spec, mp, Pr.fsplitD]];
@@ -174,6 +187,11 @@
else (writeln " [ No mutual induction rule needed ]";
TrueI);
+val _ = if !Ind_Syntax.trace then
+ (writeln "lemma = "; print_thm lemma)
+ else ();
+
+
(*Mutual induction follows by freeness of Inl/Inr.*)
(*Simplification largely reduces the mutual induction rule to the
@@ -189,7 +207,8 @@
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]);
+val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos
+ RLN (2,[rev_subsetD]);
(*Minimizes backtracking by delivering the correct premise to each goal*)
fun mutual_ind_tac [] 0 = all_tac