# HG changeset patch
# User blanchet
# Date 1346418243 -7200
# Node ID 3510b943dd5b0bed9a172c65a77dfc5de952f707
# Parent  58d3c939f91a5f7d19b727d2749020b0e77f8ea8
optimized "mk_split_tac" + use "notes"

diff -r 58d3c939f91a -r 3510b943dd5b 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
@@ -191,8 +191,6 @@
         val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
           (hd thmss, apsnd (chop (n * n)) (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)]
@@ -201,9 +199,10 @@
 
         val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
 
-        val distinct_thmsss =
+        val (distinct_thmsss', distinct_thmsss) =
           map2 (map2 append) (Library.chop_groups n half_distinct_thmss)
-            (transpose (Library.chop_groups n other_half_distinct_thmss));
+            (transpose (Library.chop_groups n other_half_distinct_thmss))
+          |> `transpose;
         val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss);
 
         val nchotomy_thm =
@@ -248,7 +247,7 @@
               | mk_thm _ not_disc [distinct] = distinct RS not_disc;
             fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss;
           in
-            map3 mk_thms discI_thms not_disc_thms (transpose distinct_thmsss)
+            map3 mk_thms discI_thms not_disc_thms distinct_thmsss'
             |> `transpose
           end;
 
@@ -351,7 +350,7 @@
 
             val split_thm =
               Skip_Proof.prove lthy [] [] goal
-                (fn _ => mk_split_tac exhaust_thm' case_thms inject_thms distinct_thms)
+                (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss)
               |> singleton (Proof_Context.export names_lthy lthy)
             val split_asm_thm =
               Skip_Proof.prove lthy [] [] goal_asm (fn {context = ctxt, ...} =>
@@ -364,26 +363,26 @@
         (* TODO: case syntax *)
         (* TODO: attributes (simp, case_names, etc.) *)
 
-        fun note thmN thms =
-          snd o Local_Theory.note
-            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
+        val notes =
+          [(case_congN, [case_cong_thm]),
+           (case_discsN, [case_disc_thm]),
+           (casesN, case_thms),
+           (ctr_selsN, ctr_sel_thms),
+           (discsN, (flat disc_thmss)),
+           (disc_disjointN, disc_disjoint_thms),
+           (disc_exhaustN, [disc_exhaust_thm]),
+           (distinctN, distinct_thms),
+           (exhaustN, [exhaust_thm]),
+           (injectN, (flat inject_thmss)),
+           (nchotomyN, [nchotomy_thm]),
+           (selsN, (flat sel_thmss)),
+           (splitN, [split_thm]),
+           (split_asmN, [split_asm_thm]),
+           (weak_case_cong_thmsN, [weak_case_cong_thm])]
+          |> map (fn (thmN, thms) =>
+            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
       in
-        lthy
-        |> note case_congN [case_cong_thm]
-        |> note case_discsN [case_disc_thm]
-        |> note casesN case_thms
-        |> note ctr_selsN ctr_sel_thms
-        |> note discsN (flat disc_thmss)
-        |> note disc_disjointN disc_disjoint_thms
-        |> note disc_exhaustN [disc_exhaust_thm]
-        |> note distinctN distinct_thms
-        |> note exhaustN [exhaust_thm]
-        |> note injectN inject_thms
-        |> note nchotomyN [nchotomy_thm]
-        |> note selsN (flat sel_thmss)
-        |> note splitN [split_thm]
-        |> note split_asmN [split_asm_thm]
-        |> note weak_case_cong_thmsN [weak_case_cong_thm]
+        lthy |> Local_Theory.notes notes |> snd
       end;
   in
     (goals, after_qed, lthy')
diff -r 58d3c939f91a -r 3510b943dd5b 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,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: thm -> thm list -> thm list -> thm list -> tactic
+  val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic
   val mk_split_asm_tac: Proof.context -> thm -> tactic
 end;
 
@@ -75,10 +75,12 @@
 
 val naked_ctxt = Proof_Context.init_global @{theory HOL};
 
-fun mk_split_tac exhaust' case_thms injects distincts =
+fun mk_split_tac exhaust' case_thms injectss distinctsss =
   rtac exhaust' 1 THEN
-  ALLGOALS (hyp_subst_tac THEN'
-    simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts))) THEN
+  ALLGOALS (fn k =>
+    (hyp_subst_tac THEN'
+     simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @
+       flat (nth distinctsss (k - 1))))) k) THEN
   ALLGOALS (blast_tac naked_ctxt);
 
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};