# HG changeset patch
# User blanchet
# Date 1346418243 -7200
# Node ID 58d3c939f91a5f7d19b727d2749020b0e77f8ea8
# Parent  9f4a7ed344b42337bfcd1d7e7e94717ad129a955
optimized "mk_case_disc_tac" further

diff -r 9f4a7ed344b4 -r 58d3c939f91a src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- 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'