# HG changeset patch
# User blanchet
# Date 1346418243 -7200
# Node ID bd3e33ee762d6eaf1daba93c5a54373a68b76a92
# Parent  8e124393c281488312e617bb9da820a59aac6b30
generate "split" property

diff -r 8e124393c281 -r bd3e33ee762d src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 22:38:12 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -39,7 +39,7 @@
 
 val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
 
-fun eta_expand_caseof_arg f xs = fold_rev Term.lambda xs (Term.list_comb (f, xs));
+fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
 fun prepare_sugar prep_term (((raw_ctrs, raw_caseof), disc_names), sel_namess) no_defs_lthy =
   let
@@ -82,20 +82,29 @@
     val caseofB = mk_caseof As B;
     val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    val (((((((xss, yss), fs), gs), (v, v')), w), p), names_lthy) = no_defs_lthy |>
+    fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs);
+
+    val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
       mk_Freess "x" ctr_Tss
       ||>> mk_Freess "y" ctr_Tss
       ||>> mk_Frees "f" caseofB_Ts
       ||>> mk_Frees "g" caseofB_Ts
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T
       ||>> yield_singleton (mk_Frees "w") T
-      ||>> yield_singleton (mk_Frees "P") HOLogic.boolT;
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
+
+    val q = Free (fst p', B --> HOLogic.boolT);
 
     val xctrs = map2 (curry Term.list_comb) ctrs xss;
     val yctrs = map2 (curry Term.list_comb) ctrs yss;
 
-    val eta_fs = map2 eta_expand_caseof_arg fs xss;
-    val eta_gs = map2 eta_expand_caseof_arg gs xss;
+    val xfs = map2 (curry Term.list_comb) fs xss;
+    val xgs = map2 (curry Term.list_comb) gs xss;
+
+    val eta_fs = map2 eta_expand_caseof_arg xss xfs;
+    val eta_gs = map2 eta_expand_caseof_arg xss xgs;
+
+    val caseofB_fs = Term.list_comb (caseofB, eta_fs);
 
     val exist_xs_v_eq_ctrs =
       map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss;
@@ -158,13 +167,7 @@
     val goal_half_distincts =
       map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq) (mk_half_pairs xctrs);
 
-    val goal_cases =
-      let
-        val lhs0 = Term.list_comb (caseofB, eta_fs);
-        fun mk_goal xctr xs f = mk_Trueprop_eq (lhs0 $ xctr, Term.list_comb (f, xs));
-      in
-        map3 mk_goal xctrs xss fs
-      end;
+    val goal_cases = map2 (fn xctr => fn xf => mk_Trueprop_eq (caseofB_fs $ xctr, xf)) xctrs xfs;
 
     val goals = [goal_exhaust] :: goal_injectss @ [goal_half_distincts, goal_cases];
 
@@ -173,6 +176,8 @@
         val ([exhaust_thm], (inject_thmss, [half_distinct_thms, case_thms])) =
           (hd thmss, chop n (tl thmss));
 
+        val inject_thms = flat inject_thmss;
+
         val exhaust_thm' =
           let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in
             Drule.instantiate' [] [SOME (certify lthy v)]
@@ -180,6 +185,7 @@
           end;
 
         val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms;
+        val distinct_thms = half_distinct_thms @ other_half_distinct_thms;
 
         val nchotomy_thm =
           let
@@ -281,10 +287,7 @@
               | 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 = mk_Trueprop_eq (lhs, rhs);
+            val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss);
           in
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
               mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thms sel_thmss)
@@ -296,11 +299,10 @@
             fun mk_prem xctr xs f g =
               fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
                 mk_Trueprop_eq (f, g)));
-            fun mk_caseof_term fs = Term.list_comb (caseofB, fs);
 
             val v_eq_w = mk_Trueprop_eq (v, w);
-            val caseof_fs = mk_caseof_term eta_fs;
-            val caseof_gs = mk_caseof_term eta_gs;
+            val caseof_fs = mk_caseofB_term eta_fs;
+            val caseof_gs = mk_caseofB_term eta_gs;
 
             val goal =
               Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs,
@@ -314,11 +316,23 @@
             |> pairself (singleton (Proof_Context.export names_lthy lthy))
           end;
 
-        val split_thms = [];
+        val split_thm =
+          let
+            fun mk_clause xctr xs f_xs =
+              list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs));
+            val goal =
+              mk_Trueprop_eq (q $ (mk_caseofB_term eta_fs $ v),
+                Library.foldr1 HOLogic.mk_conj (map3 mk_clause xctrs xss xfs));
+          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)
+          end;
 
-        val split_asm_thms = [];
+        val split_asm_thm = TrueI;
 
-        (* case syntax *)
+        (* TODO: case syntax *)
+        (* TODO: attributes (simp, case_names, etc.) *)
 
         fun note thmN thms =
           snd o Local_Theory.note
@@ -332,13 +346,13 @@
         |> note discsN disc_thms
         |> note disc_disjointN disc_disjoint_thms
         |> note disc_exhaustN [disc_exhaust_thm]
-        |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
+        |> note distinctN distinct_thms
         |> note exhaustN [exhaust_thm]
-        |> note injectN (flat inject_thmss)
+        |> note injectN inject_thms
         |> note nchotomyN [nchotomy_thm]
         |> note selsN (flat sel_thmss)
-        |> note splitN split_thms
-        |> note split_asmN split_asm_thms
+        |> note splitN [split_thm]
+        |> note split_asmN [split_asm_thm]
         |> note weak_case_cong_thmsN [weak_case_cong_thm]
       end;
   in
diff -r 8e124393c281 -r bd3e33ee762d src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 22:38:12 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -14,6 +14,7 @@
   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
 end;
 
 structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
@@ -26,7 +27,7 @@
   thm RS @{thm eq_False[THEN iffD2]}
   handle THM _ => thm RS @{thm eq_True[THEN iffD2]}
 
-fun context_ss_only thms = map_simpset (fn ss => Simplifier.clear_ss ss addsimps thms)
+fun ss_only thms ss = Simplifier.clear_ss ss addsimps thms
 
 fun mk_nchotomy_tac n exhaust =
   (rtac allI THEN' rtac exhaust THEN'
@@ -66,6 +67,14 @@
   end;
 
 fun mk_case_cong_tac ctxt exhaust' case_thms =
-  rtac exhaust' 1 THEN ALLGOALS (clarsimp_tac (context_ss_only case_thms ctxt));
+  rtac exhaust' 1 THEN ALLGOALS (clarsimp_tac (map_simpset (ss_only case_thms) ctxt));
+
+val naked_ctxt = Proof_Context.init_global @{theory HOL};
+
+fun mk_split_tac ctxt exhaust' case_thms injects distincts =
+  rtac exhaust' 1 THEN
+  ALLGOALS (hyp_subst_tac THEN'
+    simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts) HOL_basic_ss)) THEN
+  ALLGOALS (blast_tac ctxt);
 
 end;