# HG changeset patch
# User blanchet
# Date 1346837842 -7200
# Node ID c15a7123605c971bb0c17ac84c892ef3e696e132
# Parent  feb984727eec30c123ff8d2fb59ceeb6cc7f6f4b
made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation)

diff -r feb984727eec -r c15a7123605c src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:18:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:37:22 2012 +0200
@@ -424,7 +424,7 @@
             val goal = mk_Trueprop_eq (caseB_fs $ v, mk_rhs discs fs selss);
           in
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-              mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
+              mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)
             |> singleton (Proof_Context.export names_lthy lthy)
           end;
 
diff -r feb984727eec -r c15a7123605c src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 11:18:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 11:37:22 2012 +0200
@@ -9,7 +9,8 @@
 sig
   val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
   val mk_case_cong_tac: thm -> thm list -> tactic
-  val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
+  val mk_case_eq_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
+    tactic
   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
   val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
@@ -29,8 +30,10 @@
 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 mk_case_if_P_or_not_Ps n k thms =
+  let val (negs, pos) = split_last thms in
+    map (fn thm => thm RS @{thm if_not_P}) negs @ (if k = n then [] else [pos RS @{thm if_P}])
+  end;
 
 fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
 
@@ -71,13 +74,12 @@
       SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
       rtac refl)) 1;
 
-fun mk_case_eq_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
+fun mk_case_eq_tac ctxt n exhaust' case_thms disc_thmss' sel_thmss =
   (rtac exhaust' THEN'
    EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms =>
-       EVERY' [hyp_subst_tac THEN'
-         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;
+       EVERY' [hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)),
+         rtac case_thm])
+     case_thms (map2 (mk_case_if_P_or_not_Ps n) (1 upto n) (triangle 1 disc_thmss')) sel_thmss)) 1;
 
 fun mk_case_cong_tac exhaust' case_thms =
   (rtac exhaust' THEN'