# HG changeset patch
# User blanchet
# Date 1346335034 -7200
# Node ID 632ee0da3c5bdff8e5bf1647c8679a909537d81c
# Parent  d0f4f113e43de77c303be15c75566df1ef55e4a8
generate "case_disc" property

diff -r d0f4f113e43d -r 632ee0da3c5b src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 14:52:39 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 15:57:14 2012 +0200
@@ -78,7 +78,7 @@
     val caseofB = mk_caseof As B;
     val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    val (((((xss, yss), fs), (v, v')), p), _) = no_defs_lthy |>
+    val (((((xss, yss), fs), (v, v')), p), names_lthy) = no_defs_lthy |>
       mk_Freess "x" ctr_Tss
       ||>> mk_Freess "y" ctr_Tss
       ||>> mk_Frees "f" caseofB_Ts
@@ -265,7 +265,27 @@
               goals ms discD_thms sel_thmss
           end;
 
-        val case_disc_thms = [];
+        val case_disc_thm =
+          let
+            fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels);
+            fun mk_rhs _ [f] [sels] = mk_core f sels
+              | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) =
+                Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $
+                  (disc $ v) $ mk_core f sels $ mk_rhs discs fs selss;
+
+            val lhs = Term.list_comb (caseofB, eta_fs) $ v;
+            val rhs = mk_rhs discs fs selss;
+            val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+
+            val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
+            val exhaust_thm' =
+              Drule.instantiate' [] [SOME (certify lthy v)]
+                (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm));
+          in
+            Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+              mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thms sel_thmss)
+            |> singleton (Proof_Context.export names_lthy lthy)
+          end;
 
         val case_cong_thm = TrueI;
 
@@ -283,7 +303,7 @@
       in
         lthy
         |> note case_congN [case_cong_thm]
-        |> note case_discsN case_disc_thms
+        |> note case_discsN [case_disc_thm]
         |> note casesN case_thms
         |> note ctr_selsN ctr_sel_thms
         |> note discsN disc_thms
diff -r d0f4f113e43d -r 632ee0da3c5b src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- 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;