# HG changeset patch
# User paulson
# Date 1033737792 -7200
# Node ID 282fbabec8625daf44bbef75f77f3423f18f53e8
# Parent  ca86e84ce200a8f6e004d13ee8efabe3daf02b77
Fixed bug involving inductive definitions having equalities in the premises,
e.g.  n = Suc(m).

diff -r ca86e84ce200 -r 282fbabec862 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Oct 04 09:56:48 2002 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Oct 04 15:23:12 2002 +0200
@@ -31,6 +31,7 @@
 signature INDUCTIVE_PACKAGE =
 sig
   val quiet_mode: bool ref
+  val trace: bool ref
   val unify_consts: Sign.sg -> term list -> term list -> term list * term list
   val split_rule_vars: term list -> thm -> thm
   val get_inductive: theory -> string -> ({names: string list, coind: bool} *
@@ -165,6 +166,7 @@
 (** misc utilities **)
 
 val quiet_mode = ref false;
+val trace = ref false;  (*for debugging*)
 fun message s = if ! quiet_mode then () else writeln s;
 fun clean_message s = if ! quick_and_dirty then () else message s;
 
@@ -412,6 +414,7 @@
       end;
 
     val ind_prems = map mk_ind_prem intr_ts;
+
     val factors = foldl (mg_prod_factors preds) ([], ind_prems);
 
     (* make conclusions for induction rules *)
@@ -624,6 +627,11 @@
     val (preds, ind_prems, mutual_ind_concl, factors) =
       mk_indrule cs cTs params intr_ts;
 
+    val dummy = if !trace then
+		(writeln "ind_prems = ";
+		 seq (writeln o Sign.string_of_term sign) ind_prems)
+	    else ();
+
     (* make predicate for instantiation of abstract induction rule *)
 
     fun mk_ind_pred _ [P] = P
@@ -651,20 +659,27 @@
              nth_elem (find_index_eq c cs, preds)))))
         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
 
+    val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
+
+    val dummy = if !trace then
+		(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
+	    else ();
+
     val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
         [rtac (impI RS allI) 1,
-         DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
+         DETERM (etac raw_fp_induct 1),
          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
          fold_goals_tac rec_sets_defs,
          (*This CollectE and disjE separates out the introduction rules*)
          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
          (*Now break down the individual cases.  No disjE here in case
            some premise involves disjunction.*)
-         REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
-         rewrite_goals_tac sum_case_rewrites,
+         REPEAT (FIRSTGOAL (etac conjE)),
+         ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
          EVERY (map (fn prem =>
-           DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
+			DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1 APPEND 
+						hyp_subst_tac 1)) prems)]);
 
     val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>