--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Thu Aug 30 14:52:39 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Thu Aug 30 15:57:14 2012 +0200
@@ -7,6 +7,7 @@
signature BNF_SUGAR_TACTICS =
sig
+ val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
@@ -20,6 +21,10 @@
open BNF_Tactics
open BNF_FP_Util
+fun eq_True_or_False thm =
+ thm RS @{thm eq_False[THEN iffD2]}
+ handle THM _ => thm RS @{thm eq_True[THEN iffD2]}
+
fun mk_nchotomy_tac n exhaust =
(rtac allI THEN' rtac exhaust THEN'
EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
@@ -45,7 +50,16 @@
else
REPEAT_DETERM_N m o etac exE THEN'
hyp_subst_tac THEN'
- K (Local_Defs.unfold_tac ctxt sel_thms) THEN'
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
rtac refl)) 1;
+fun mk_case_disc_tac ctxt exhaust case_thms disc_thms sel_thmss =
+ let val base_unfolds = @{thms if_True if_False} @ map eq_True_or_False disc_thms in
+ (rtac exhaust THEN'
+ EVERY' (map2 (fn case_thm => fn sel_thms => EVERY' [
+ hyp_subst_tac THEN'
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt (base_unfolds @ sel_thms)) THEN'
+ rtac case_thm]) case_thms sel_thmss)) 1
+ end;
+
end;