--- 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;