# HG changeset patch
# User paulson
# Date 892208542 -7200
# Node ID 013ba4c438329c39e6f3e0629a832cc0c560c233
# Parent  79cc986bc4d737bb58b46268629265166d44efd1
Fixed bug in inductive sections to allow disjunctive premises;
added tracing flag trace_induct

diff -r 79cc986bc4d7 -r 013ba4c43832 src/HOL/add_ind_def.ML
--- a/src/HOL/add_ind_def.ML	Fri Apr 10 13:41:04 1998 +0200
+++ b/src/HOL/add_ind_def.ML	Fri Apr 10 13:42:22 1998 +0200
@@ -151,7 +151,10 @@
              | _ => rec_tms ~~          (*define the sets as Parts*)
                     map (subst_atomic [(freeX, big_rec_tm)]) parts));
 
-    val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
+    (*tracing: print the fixedpoint definition*)
+    val _ = if !Ind_Syntax.trace then
+		seq (writeln o Sign.string_of_term sign o #2) axpairs
+            else ()
   
     (*Detect occurrences of operator, even with other types!*)
     val _ = (case rec_names inter (add_term_names (lfp_rhs,[])) of
diff -r 79cc986bc4d7 -r 013ba4c43832 src/HOL/ind_syntax.ML
--- a/src/HOL/ind_syntax.ML	Fri Apr 10 13:41:04 1998 +0200
+++ b/src/HOL/ind_syntax.ML	Fri Apr 10 13:42:22 1998 +0200
@@ -13,6 +13,9 @@
 structure Ind_Syntax =
 struct
 
+(*Print tracing messages during processing of "inductive" theory sections*)
+val trace = ref false;
+
 (** Abstract syntax definitions for HOL **)
 
 open HOLogic;
@@ -92,3 +95,6 @@
                 refl_thin, conjE, exE, disjE];
 
 end;
+
+
+val trace_induct = Ind_Syntax.trace;
diff -r 79cc986bc4d7 -r 013ba4c43832 src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Fri Apr 10 13:41:04 1998 +0200
+++ b/src/HOL/indrule.ML	Fri Apr 10 13:42:22 1998 +0200
@@ -65,7 +65,7 @@
   in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
   handle Bind => error"Recursion term not found in conclusion";
 
-(*Avoids backtracking by delivering the correct premise to each goal*)
+(*Minimizes backtracking by delivering the correct premise to each goal*)
 fun ind_tac [] 0 = all_tac
   | ind_tac(prem::prems) i = 
         DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN
@@ -76,13 +76,15 @@
 val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
                     Inductive.intr_tms;
 
-(*Debugging code...
-val _ = writeln "ind_prems = ";
-val _ = seq (writeln o Sign.string_of_term sign) ind_prems;
-*)
+val _ = if !Ind_Syntax.trace then 
+            (writeln "ind_prems = ";
+	     seq (writeln o Sign.string_of_term sign) ind_prems;
+	     writeln "raw_induct = "; print_thm Intr_elim.raw_induct)
+        else ();
+
 
 (*We use a MINIMAL simpset because others (such as HOL_ss) contain too many
-  simplifications.  If the premises get simplified, then the proofs will 
+  simplifications.  If the premises get simplified, then the proofs could 
   fail.  This arose with a premise of the form {(F n,G n)|n . True}, which
   expanded to something containing ...&True. *)
 val min_ss = HOL_basic_ss;
@@ -97,7 +99,11 @@
        [rtac (impI RS allI) 1,
         DETERM (etac Intr_elim.raw_induct 1),
         full_simp_tac (min_ss addsimps [Part_Collect]) 1,
-        REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
+        (*This CollectE and disjE separates out the introduction rules*)
+	REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
+	(*Now break down the individual cases.  No disjE here in case
+          some premise involves disjunction.*)
+        REPEAT (FIRSTGOAL (eresolve_tac [CollectE, IntE, exE, conjE] 
                            ORELSE' hyp_subst_tac)),
         ind_tac (rev prems) (length prems)])
     handle e => print_sign_exn sign e;
@@ -161,7 +167,8 @@
 	    REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN
 		    lemma_tac 1)])
       handle e => print_sign_exn sign e)
-  else TrueI;
+  else (writeln "  [ No mutual induction rule needed ]";
+        TrueI);
 
 (*Mutual induction follows by freeness of Inl/Inr.*)