# HG changeset patch
# User blanchet
# Date 1380059492 -7200
# Node ID 60b89c05317fbe48e183729f603bb05c98047d77
# Parent  c9aefa1fc451d7c3ff4fa25f507a18073dd401d8
generalized tactics

diff -r c9aefa1fc451 -r 60b89c05317f src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Tue Sep 24 23:10:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Tue Sep 24 23:51:32 2013 +0200
@@ -8,8 +8,8 @@
 signature BNF_FP_REC_SUGAR_TACTICS =
 sig
   val mk_primcorec_assumption_tac: Proof.context -> tactic
-  val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic
-  val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic
+  val mk_primcorec_code_tac: thm list -> thm list -> thm -> thm list -> tactic
+  val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> int list -> thm list -> tactic
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
     thm list list list -> thm list -> thm list -> thm list -> tactic
@@ -74,20 +74,21 @@
 fun mk_primcorec_sel_of_ctr_tac sel f_ctr =
   HEADGOAL (etac (f_ctr RS arg_cong RS trans) THEN' rtac sel);
 
-fun mk_primcorec_code_of_ctr_case_tac ctxt m f_ctr =
-  HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN
+fun mk_primcorec_code_of_ctr_case_tac ctxt eq_caseIs m f_ctr =
+  HEADGOAL (REPEAT o resolve_tac (@{thm eq_ifI} :: eq_caseIs)) THEN
   mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
   REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN
   (* FIXME: Something like (ss_only @{thms if_True if_False not_False_eq_True simp_thms} ctxt) *)
   HEADGOAL (asm_simp_tac ctxt);
 
-fun mk_primcorec_code_of_ctr_tac ctxt ms ctr_thms =
-  EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt) ms ctr_thms);
+fun mk_primcorec_code_of_ctr_tac ctxt eq_caseIs ms ctr_thms =
+  EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt eq_caseIs) ms ctr_thms);
 
-fun mk_primcorec_code_tac ctxt raw collapses =
-  HEADGOAL (rtac (raw RS trans)) THEN unfold_thms_tac ctxt @{thms split_ifs} THEN
-  Method.intros_tac @{thms conjI impI} [] THEN
-  REPEAT (HEADGOAL (rtac refl ORELSE' (etac notE THEN' atac) ORELSE'
-    eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
+fun mk_primcorec_code_tac eq_caseIs disc_excludes raw collapses =
+  HEADGOAL (rtac (raw RS trans) THEN'
+    REPEAT o (resolve_tac (maps (fn thm => [thm, thm RS sym]) (@{thm eq_ifI} :: eq_caseIs)) ORELSE'
+      rtac refl ORELSE' (etac notE THEN' atac) ORELSE'
+      (dresolve_tac disc_excludes THEN' etac notE THEN' atac) ORELSE'
+      eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
 
 end;