# HG changeset patch
# User desharna
# Date 1418984243 -3600
# Node ID 776964a0589f1c7abcf3046b3efb68119f2fb81f
# Parent  962ad3942ea7656c0f124f42cd336dad85a3abe8
generate 'case_distrib' for Ctr_Sugars

diff -r 962ad3942ea7 -r 776964a0589f src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jan 05 00:07:01 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 19 11:17:23 2014 +0100
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Martin Desharnais, TU Muenchen
     Copyright   2012, 2013
 
 Wrapping existing freely generated type's constructors.
@@ -23,6 +24,7 @@
      case_thms: thm list,
      case_cong: thm,
      case_cong_weak: thm,
+     case_distribs: thm list,
      split: thm,
      split_asm: thm,
      disc_defs: thm list,
@@ -111,6 +113,7 @@
    case_thms: thm list,
    case_cong: thm,
    case_cong_weak: thm,
+   case_distribs: thm list,
    split: thm,
    split_asm: thm,
    disc_defs: thm list,
@@ -128,9 +131,9 @@
    case_eq_ifs: thm list};
 
 fun morph_ctr_sugar phi ({kind, T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
-    case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
-    sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels,
-    split_sel_asms, case_eq_ifs} : ctr_sugar) =
+    case_thms, case_cong, case_cong_weak, case_distribs, split, split_asm, disc_defs, disc_thmss,
+    discIs, sel_defs, sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands,
+    split_sels, split_sel_asms, case_eq_ifs} : ctr_sugar) =
   {kind = kind,
    T = Morphism.typ phi T,
    ctrs = map (Morphism.term phi) ctrs,
@@ -144,6 +147,7 @@
    case_thms = map (Morphism.thm phi) case_thms,
    case_cong = Morphism.thm phi case_cong,
    case_cong_weak = Morphism.thm phi case_cong_weak,
+   case_distribs = map (Morphism.thm phi) case_distribs,
    split = Morphism.thm phi split,
    split_asm = Morphism.thm phi split_asm,
    disc_defs = map (Morphism.thm phi) disc_defs,
@@ -244,6 +248,7 @@
 val splitsN = "splits";
 val split_selsN = "split_sels";
 val case_cong_weak_thmsN = "case_cong_weak";
+val case_distribN = "case_distrib";
 
 val cong_attrs = @{attributes [cong]};
 val dest_attrs = @{attributes [dest]};
@@ -394,10 +399,10 @@
 
     fun qualify mandatory = Binding.qualify mandatory fc_b_name;
 
-    val (unsorted_As, B) =
+    val (unsorted_As, [B, C]) =
       no_defs_lthy
       |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0)
-      ||> the_single o fst o mk_TFrees 1;
+      ||> fst o mk_TFrees 2;
 
     val As = map2 (resort_tfree_or_tvar o snd o dest_TFree_or_TVar) As0 unsorted_As;
 
@@ -445,13 +450,14 @@
 
     val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    val (((((((([exh_y], (xss, xss')), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) =
+    val ((((((((([exh_y], (xss, xss')), yss), fs), gs), [h]), [u', v']), [w]), (p, p')), names_lthy) =
       no_defs_lthy
       |> mk_Frees "y" [fcT] (* for compatibility with "datatype_realizer.ML" *)
       ||>> mk_Freess' "x" ctr_Tss
       ||>> mk_Freess "y" ctr_Tss
       ||>> mk_Frees "f" case_Ts
       ||>> mk_Frees "g" case_Ts
+      ||>> mk_Frees "h" [B --> C]
       ||>> (apfst (map (rpair fcT)) oo Variable.variant_fixes) [fc_b_name, fc_b_name ^ "'"]
       ||>> mk_Frees "z" [B]
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
@@ -497,6 +503,7 @@
 
     val case0 = Morphism.term phi raw_case;
     val casex = mk_case As B case0;
+    val casexC = mk_case As C case0;
 
     val fcase = Term.list_comb (casex, fs);
 
@@ -662,8 +669,9 @@
 
     val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss;
 
-    fun after_qed ([exhaust_thm] :: thmss) lthy =
+    fun after_qed thmss0 lthy =
       let
+        val [exhaust_thm] :: thmss = thmss0
         val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
 
         val rho_As = map (apply2 (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
@@ -981,6 +989,20 @@
                [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm])
             end;
 
+        val case_distrib_thm =
+          let
+            val args = @{map 2} (fn f => fn argTs =>
+              let val (args, _) = mk_Frees "x" argTs lthy in
+                fold_rev Term.lambda args (h $ list_comb (f, args))
+              end) fs ctr_Tss;
+            val goal = mk_Trueprop_eq (h $ ufcase, list_comb (casexC, args) $ u);
+          in
+            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+              mk_case_distrib_tac ctxt (certify ctxt u) exhaust_thm case_thms)
+            |> singleton (Proof_Context.export names_lthy lthy)
+            |> Thm.close_derivation
+          end;
+
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
         val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
 
@@ -999,6 +1021,7 @@
           [(caseN, case_thms, code_attrs @ nitpicksimp_attrs @ simp_attrs),
            (case_congN, [case_cong_thm], []),
            (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
+           (case_distribN, [case_distrib_thm], []),
            (case_eq_ifN, case_eq_if_thms, []),
            (collapseN, safe_collapse_thms, if ms = [0] then [] else simp_attrs),
            (discN, flat nontriv_disc_thmss, simp_attrs),
@@ -1048,12 +1071,13 @@
           {kind = kind, T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss,
            exhaust = exhaust_thm, nchotomy = nchotomy_thm, injects = inject_thms,
            distincts = distinct_thms, case_thms = case_thms, case_cong = case_cong_thm,
-           case_cong_weak = case_cong_weak_thm, split = split_thm, split_asm = split_asm_thm,
-           disc_defs = disc_defs, disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs,
-           sel_thmss = sel_thmss, distinct_discsss = distinct_disc_thmsss,
-           exhaust_discs = exhaust_disc_thms, exhaust_sels = exhaust_sel_thms,
-           collapses = all_collapse_thms, expands = expand_thms, split_sels = split_sel_thms,
-           split_sel_asms = split_sel_asm_thms, case_eq_ifs = case_eq_if_thms}
+           case_cong_weak = case_cong_weak_thm, case_distribs = [case_distrib_thm], split = split_thm,
+           split_asm = split_asm_thm, disc_defs = disc_defs, disc_thmss = disc_thmss,
+           discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss,
+           distinct_discsss = distinct_disc_thmsss, exhaust_discs = exhaust_disc_thms,
+           exhaust_sels = exhaust_sel_thms, collapses = all_collapse_thms, expands = expand_thms,
+           split_sels = split_sel_thms, split_sel_asms = split_sel_asm_thms,
+           case_eq_ifs = case_eq_if_thms}
           |> morph_ctr_sugar (substitute_noted_thm noted);
       in
         (ctr_sugar, lthy' |> register_ctr_sugar plugins ctr_sugar)
diff -r 962ad3942ea7 -r 776964a0589f src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Mon Jan 05 00:07:01 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Fri Dec 19 11:17:23 2014 +0100
@@ -19,6 +19,7 @@
   val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
   val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
   val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
+  val mk_case_distrib_tac: Proof.context -> cterm -> thm -> thm list -> tactic
   val mk_case_eq_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
     thm list list -> tactic
   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
@@ -144,6 +145,10 @@
          else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
   end;
 
+fun mk_case_distrib_tac ctxt ct exhaust cases =
+  HEADGOAL (rtac (cterm_instantiate_pos [SOME ct] exhaust)) THEN
+  ALLGOALS (hyp_subst_tac ctxt THEN' SELECT_GOAL (unfold_thms_tac ctxt cases) THEN' rtac refl);
+
 fun mk_case_cong_tac ctxt uexhaust cases =
   HEADGOAL (rtac uexhaust THEN'
     EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
diff -r 962ad3942ea7 -r 776964a0589f src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Jan 05 00:07:01 2015 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Fri Dec 19 11:17:23 2014 +0100
@@ -110,6 +110,7 @@
      case_thms = case_rewrites,
      case_cong = case_cong,
      case_cong_weak = case_cong_weak,
+     case_distribs = [],
      split = split,
      split_asm = split_asm,
      disc_defs = [],
diff -r 962ad3942ea7 -r 776964a0589f src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Jan 05 00:07:01 2015 +0100
+++ b/src/HOL/Tools/record.ML	Fri Dec 19 11:17:23 2014 +0100
@@ -1786,10 +1786,10 @@
     {kind = Ctr_Sugar.Record, T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy,
      discs = [], selss = [], exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject],
      distincts = [], case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,
-     split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [],
-     discIs = [], sel_defs = [], sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [],
-     exhaust_sels = [], collapses = [], expands = [], split_sels = [], split_sel_asms = [],
-     case_eq_ifs = []};
+     case_distribs = [], split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [],
+     disc_thmss = [], discIs = [], sel_defs = [], sel_thmss = [sel_thms], distinct_discsss = [],
+     exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [], split_sels = [],
+     split_sel_asms = [], case_eq_ifs = []};
 
 
 (* definition *)