--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Thu Aug 30 22:38:12 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Fri Aug 31 15:04:03 2012 +0200
@@ -14,6 +14,7 @@
val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
val mk_nchotomy_tac: int -> thm -> tactic
val mk_other_half_disc_disjoint_tac: thm -> tactic
+ val mk_split_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
end;
structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
@@ -26,7 +27,7 @@
thm RS @{thm eq_False[THEN iffD2]}
handle THM _ => thm RS @{thm eq_True[THEN iffD2]}
-fun context_ss_only thms = map_simpset (fn ss => Simplifier.clear_ss ss addsimps thms)
+fun ss_only thms ss = Simplifier.clear_ss ss addsimps thms
fun mk_nchotomy_tac n exhaust =
(rtac allI THEN' rtac exhaust THEN'
@@ -66,6 +67,14 @@
end;
fun mk_case_cong_tac ctxt exhaust' case_thms =
- rtac exhaust' 1 THEN ALLGOALS (clarsimp_tac (context_ss_only case_thms ctxt));
+ rtac exhaust' 1 THEN ALLGOALS (clarsimp_tac (map_simpset (ss_only case_thms) ctxt));
+
+val naked_ctxt = Proof_Context.init_global @{theory HOL};
+
+fun mk_split_tac ctxt exhaust' case_thms injects distincts =
+ rtac exhaust' 1 THEN
+ ALLGOALS (hyp_subst_tac THEN'
+ simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts) HOL_basic_ss)) THEN
+ ALLGOALS (blast_tac ctxt);
end;