generate "disc_exhaust" property

--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 13:42:05 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 14:27:26 2012 +0200
@@ -2039,7 +2039,7 @@
     val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms;
     val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms;
     val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms;
-    val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms;
+    val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms;
 
     val bij_fld_thms =
       map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms;
@@ -2047,7 +2047,7 @@
     val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms;
     val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms;
     val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
-    val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms;
+    val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
 
     val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld =>
       iffD1 OF [unf_inject, trans  OF [coiter, unf_fld RS sym]])

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Aug 30 13:42:05 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Aug 30 14:27:26 2012 +0200
@@ -1162,7 +1162,7 @@
     val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms;
     val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms;
     val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms;
-    val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms;
+    val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms;
 
     val bij_fld_thms =
       map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms;
@@ -1170,7 +1170,7 @@
     val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms;
     val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms;
     val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
-    val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms;
+    val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
 
     val timer = time (timer "unf definitions & thms");
 

--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 13:42:05 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 14:27:26 2012 +0200
@@ -131,9 +131,10 @@
     val discs = map (mk_disc_or_sel As) discs0;
     val selss = map (map (mk_disc_or_sel As)) selss0;
 
+    fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p);
+
     val goal_exhaust =
       let
-        fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p);
         fun mk_prem xctr xs =
           fold_rev Logic.all xs (mk_imp_p [HOLogic.mk_Trueprop (HOLogic.mk_eq (v, xctr))]);
       in
@@ -175,7 +176,7 @@
           let
             val goal =
               HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v',
-                   Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
+                Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
           in
             Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
           end;
@@ -222,8 +223,8 @@
           let
             fun get_disc_thm k k' = nth disc_thms ((k' - 1) * n + (k - 1));
             fun mk_goal ((_, disc), (_, disc')) =
-              Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
-                HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)));
+              Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
+                HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v))));
             fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
 
             val bundles = ks ~~ ms ~~ disc_defs ~~ discs;
@@ -242,7 +243,13 @@
             half_thms @ other_half_thms
           end;
 
-        val disc_exhaust_thms = [];
+        val disc_exhaust_thm =
+          let
+            fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)];
+            val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs));
+          in
+            Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms)
+          end;
 
         val ctr_sel_thms = [];
 
@@ -269,7 +276,7 @@
         |> note ctr_selsN ctr_sel_thms
         |> note discsN disc_thms
         |> note disc_disjointN disc_disjoint_thms
-        |> note disc_exhaustN disc_exhaust_thms
+        |> note disc_exhaustN [disc_exhaust_thm]
         |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
         |> note exhaustN [exhaust_thm]
         |> note injectN inject_thms

--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 13:42:05 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 14:27:26 2012 +0200
@@ -7,14 +7,16 @@
 
 signature BNF_SUGAR_TACTICS =
 sig
+  val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
+  val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
   val mk_nchotomy_tac: int -> thm -> tactic
-  val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
   val mk_other_half_disc_disjoint_tac: thm -> tactic
 end;
 
 structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
 struct
 
+open BNF_Tactics
 open BNF_FP_Util
 
 fun mk_nchotomy_tac n exhaust =
@@ -30,4 +32,9 @@
 fun mk_other_half_disc_disjoint_tac half_thm =
   (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
 
+fun mk_disc_exhaust_tac n exhaust discIs =
+  (rtac exhaust THEN'
+   EVERY' (map2 (fn k => fn discI =>
+     dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
+
 end;