src/HOL/Tools/inductive_package.ML
changeset 11682 d9063229b4a1
parent 11628 e57a6e51715e
child 11740 86ac4189a1c1
--- a/src/HOL/Tools/inductive_package.ML	Thu Oct 04 15:39:00 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 04 15:39:43 2001 +0200
@@ -295,7 +295,7 @@
 val all_not_allowed = 
     "Introduction rule must not have a leading \"!!\" quantifier";
 
-val atomize_cterm = hol_rewrite_cterm inductive_atomize;
+val atomize_cterm = full_rewrite_cterm inductive_atomize;
 
 in
 
@@ -543,14 +543,26 @@
   the given defs.  Cannot simply use the local con_defs because con_defs=[]
   for inference systems. (??) *)
 
+local
+
 (*cprop should have the form t:Si where Si is an inductive set*)
+val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
 
-val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
+(*delete needless equality assumptions*)
+val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
+val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
+val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
+
+fun simp_case_tac solved ss i =
+  EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
+  THEN_MAYBE (if solved then no_tac else all_tac);
+
+in
 
 fun mk_cases_i elims ss cprop =
   let
     val prem = Thm.assume cprop;
-    val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac;
+    val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   in
     (case get_first (try mk_elim) elims of
@@ -569,6 +581,8 @@
     val (_, {elims, ...}) = the_inductive thy c;
   in mk_cases_i elims ss cprop end;
 
+end;
+
 
 (* inductive_cases(_i) *)