--- 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) *)