# HG changeset patch
# User blanchet
# Date 1346418243 -7200
# Node ID c4a34ae5504d8d16acc71cd3fd97f2c72682066b
# Parent  bd3e33ee762d6eaf1daba93c5a54373a68b76a92
generate "split_asm" property

diff -r bd3e33ee762d -r c4a34ae5504d src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -316,21 +316,34 @@
             |> pairself (singleton (Proof_Context.export names_lthy lthy))
           end;
 
-        val split_thm =
+        val (split_thm, split_asm_thm) =
           let
-            fun mk_clause xctr xs f_xs =
+            fun mk_conjunct xctr xs f_xs =
               list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs));
+            fun mk_disjunct xctr xs f_xs =
+              list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr),
+                HOLogic.mk_not (q $ f_xs)));
+
+            val lhs = q $ (mk_caseofB_term eta_fs $ v);
+
             val goal =
-              mk_Trueprop_eq (q $ (mk_caseofB_term eta_fs $ v),
-                Library.foldr1 HOLogic.mk_conj (map3 mk_clause xctrs xss xfs));
+              mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
+            val goal_asm =
+              mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
+                (map3 mk_disjunct xctrs xss xfs)));
+
+            val split_thm =
+              Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+                mk_split_tac ctxt exhaust_thm' case_thms inject_thms distinct_thms)
+              |> singleton (Proof_Context.export names_lthy lthy)
+            val split_asm_thm =
+              Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} =>
+                mk_split_asm_tac ctxt split_thm)
+              |> singleton (Proof_Context.export names_lthy lthy)
           in
-            Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-              mk_split_tac ctxt exhaust_thm' case_thms inject_thms distinct_thms)
-            |> singleton (Proof_Context.export names_lthy lthy)
+            (split_thm, split_asm_thm)
           end;
 
-        val split_asm_thm = TrueI;
-
         (* TODO: case syntax *)
         (* TODO: attributes (simp, case_names, etc.) *)
 
diff -r bd3e33ee762d -r c4a34ae5504d 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
@@ -14,7 +14,8 @@
   val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
   val mk_nchotomy_tac: int -> thm -> tactic
   val mk_other_half_disc_disjoint_tac: thm -> tactic
-  val mk_split_tac:  Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
+  val mk_split_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
+  val mk_split_asm_tac: Proof.context -> thm -> tactic
 end;
 
 structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
@@ -77,4 +78,11 @@
     simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts) HOL_basic_ss)) THEN
   ALLGOALS (blast_tac ctxt);
 
+val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
+
+fun mk_split_asm_tac ctxt split =
+  rtac (split RS trans) 1 THEN
+  Local_Defs.unfold_tac ctxt split_asm_thms THEN
+  rtac refl 1;
+
 end;