# HG changeset patch
# User paulson
# Date 892206928 -7200
# Node ID 02b7c759159be11248eba779097dee04780e5a5c
# Parent  8428d4699d58d027ac7c7d31f7d5c2be3abe937d
Fixed bug in inductive sections to allow disjunctive premises;
added tracing flag trace_induct

diff -r 8428d4699d58 -r 02b7c759159b src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Thu Apr 09 12:31:35 1998 +0200
+++ b/src/ZF/add_ind_def.ML	Fri Apr 10 13:15:28 1998 +0200
@@ -165,8 +165,11 @@
              | _ => rec_tms ~~          (*define the sets as Parts*)
                     map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
 
-    val dummy = 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 ()
+
   in  thy |> PureThy.add_store_defs_i axpairs  end
 
 
diff -r 8428d4699d58 -r 02b7c759159b src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Thu Apr 09 12:31:35 1998 +0200
+++ b/src/ZF/ind_syntax.ML	Fri Apr 10 13:15:28 1998 +0200
@@ -12,6 +12,9 @@
 structure Ind_Syntax =
 struct
 
+(*Print tracing messages during processing of "inductive" theory sections*)
+val trace = ref false;
+
 (** Abstract syntax definitions for ZF **)
 
 val iT = Type("i",[]);
@@ -124,3 +127,5 @@
 
 end;
 
+
+val trace_induct = Ind_Syntax.trace;
diff -r 8428d4699d58 -r 02b7c759159b src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Thu Apr 09 12:31:35 1998 +0200
+++ b/src/ZF/indrule.ML	Fri Apr 10 13:15:28 1998 +0200
@@ -62,7 +62,7 @@
   in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
   handle Bind => error"Recursion term not found in conclusion";
 
-(*Reduces backtracking by delivering the correct premise to each goal.
+(*Minimizes backtracking by delivering the correct premise to each goal.
   Intro rules with extra Vars in premises still cause some backtracking *)
 fun ind_tac [] 0 = all_tac
   | ind_tac(prem::prems) i = 
@@ -74,13 +74,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 FOL_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.  *)
 val min_ss = empty_ss
       setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
@@ -98,8 +100,12 @@
         DETERM (etac Intr_elim.raw_induct 1),
         (*Push Part inside Collect*)
         full_simp_tac (min_ss addsimps [Part_Collect]) 1,
-        REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE'
-                           hyp_subst_tac)),
+        (*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, exE, conjE] 
+                           ORELSE' hyp_subst_tac)),
         ind_tac (rev prems) (length prems) ]);
 
 (*** Prove the simultaneous induction rule ***)
@@ -165,7 +171,8 @@
 	     [cut_facts_tac prems 1, 
 	      REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
 		      lemma_tac 1)]))
-  else TrueI;
+  else (writeln "  [ No mutual induction rule needed ]";
+        TrueI);
 
 (*Mutual induction follows by freeness of Inl/Inr.*)
 
@@ -184,7 +191,7 @@
 *)
 val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos RLN (2,[rev_subsetD]);
 
-(*Avoids backtracking by delivering the correct premise to each goal*)
+(*Minimizes backtracking by delivering the correct premise to each goal*)
 fun mutual_ind_tac [] 0 = all_tac
   | mutual_ind_tac(prem::prems) i = 
       DETERM