--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Fri Aug 31 15:04:03 2012 +0200
@@ -25,9 +25,11 @@
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 triangle _ [] = []
+ | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss
+
+fun mk_if_P_or_not_P thm =
+ thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P}
fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
@@ -61,11 +63,11 @@
fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
(rtac exhaust' THEN'
- EVERY' (map3 (fn case_thm => fn disc_thms => fn sel_thms => EVERY' [
+ EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [
hyp_subst_tac THEN'
- SELECT_GOAL (Local_Defs.unfold_tac ctxt
- (@{thms if_True if_False} @ disc_thms @ sel_thms)) THEN'
- rtac case_thm]) case_thms (map (map eq_True_or_False) disc_thmss') sel_thmss)) 1;
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN'
+ rtac case_thm]) case_thms
+ (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1;
fun mk_case_cong_tac exhaust' case_thms =
(rtac exhaust' THEN'