--- a/src/HOL/Tools/Function/fun_cases.ML Mon Sep 30 13:35:05 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML Mon Sep 30 13:45:17 2013 +0200
@@ -17,19 +17,6 @@
structure Fun_Cases : FUN_CASES =
struct
-local
-
-val refl_thin =
- Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
- (fn _ => assume_tac 1);
-val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
-val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
-
-fun simp_case_tac ctxt i =
- EVERY' [elim_tac, TRY o asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
-
-in
-
fun mk_fun_cases ctxt prop =
let
val thy = Proof_Context.theory_of ctxt;
@@ -44,9 +31,9 @@
val {elims, pelims, is_partial, ...} = info;
val elims = if is_partial then pelims else the elims;
val cprop = cterm_of thy prop;
- val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
fun mk_elim rl =
- Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
+ Thm.implies_intr cprop
+ (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
|> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
in
(case get_first (try mk_elim) (flat elims) of
@@ -54,9 +41,6 @@
| NONE => err ())
end;
-end;
-
-
fun gen_fun_cases prep_att prep_prop args lthy =
let
val thy = Proof_Context.theory_of lthy;
--- a/src/HOL/Tools/inductive.ML Mon Sep 30 13:35:05 2013 +0200
+++ b/src/HOL/Tools/inductive.ML Mon Sep 30 13:45:17 2013 +0200
@@ -30,6 +30,7 @@
val get_monos: Proof.context -> thm list
val mono_add: attribute
val mono_del: attribute
+ val mk_cases_tac: Proof.context -> tactic
val mk_cases: Proof.context -> term -> thm
val inductive_forall_def: thm
val rulify: Proof.context -> thm -> thm
@@ -540,6 +541,8 @@
in
+fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
+
fun mk_cases ctxt prop =
let
val thy = Proof_Context.theory_of ctxt;
@@ -551,9 +554,9 @@
val elims = Induct.find_casesP ctxt prop;
val cprop = Thm.cterm_of thy prop;
- val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
fun mk_elim rl =
- Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
+ Thm.implies_intr cprop
+ (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
|> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
in
(case get_first (try mk_elim) elims of