generate 'disc_eq_case' for Ctr_Sugars

--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Jan 05 06:56:15 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Fri Dec 19 11:18:58 2014 +0100
@@ -66,8 +66,6 @@
   val mk_nthN: int -> term -> int -> term
 
   (*parameterized thms*)
-  val eqTrueI: thm
-  val eqFalseI: thm
   val prod_injectD: thm
   val prod_injectI: thm
   val ctrans: thm
@@ -345,8 +343,6 @@
 fun mk_sym thm = thm RS sym;
 
 (*TODO: antiquote heavily used theorems once*)
-val eqTrueI = @{thm iffD2[OF eq_True]};
-val eqFalseI =  @{thm iffD2[OF eq_False]};
 val prod_injectD = @{thm iffD1[OF prod.inject]};
 val prod_injectI = @{thm iffD2[OF prod.inject]};
 val ctrans = @{thm ordLeq_transitive};

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jan 05 06:56:15 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 19 11:18:58 2014 +0100
@@ -30,6 +30,7 @@
      disc_defs: thm list,
      disc_thmss: thm list list,
      discIs: thm list,
+     disc_eq_cases: thm list,
      sel_defs: thm list,
      sel_thmss: thm list list,
      distinct_discsss: thm list list list,
@@ -119,6 +120,7 @@
    disc_defs: thm list,
    disc_thmss: thm list list,
    discIs: thm list,
+   disc_eq_cases: thm list,
    sel_defs: thm list,
    sel_thmss: thm list list,
    distinct_discsss: thm list list list,
@@ -132,8 +134,8 @@
 
 fun morph_ctr_sugar phi ({kind, T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
     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) =
+    discIs, disc_eq_cases, 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,
@@ -153,6 +155,7 @@
    disc_defs = map (Morphism.thm phi) disc_defs,
    disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    discIs = map (Morphism.thm phi) discIs,
+   disc_eq_cases = map (Morphism.thm phi) disc_eq_cases,
    sel_defs = map (Morphism.thm phi) sel_defs,
    sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
    distinct_discsss = map (map (map (Morphism.thm phi))) distinct_discsss,
@@ -232,6 +235,7 @@
 val collapseN = "collapse";
 val discN = "disc";
 val discIN = "discI";
+val disc_eq_caseN = "disc_eq_case";
 val distinctN = "distinct";
 val distinct_discN = "distinct_disc";
 val exhaustN = "exhaust";
@@ -505,6 +509,7 @@
     val case0 = Morphism.term phi raw_case;
     val casex = mk_case As B case0;
     val casexC = mk_case As C case0;
+    val casexBool = mk_case As HOLogic.boolT case0;
 
     val fcase = Term.list_comb (casex, fs);
 
@@ -770,9 +775,9 @@
         val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
              discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
              exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms,
-             expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms) =
+             expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms, disc_eq_case_thms) =
           if no_discs_sels then
-            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
+            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
           else
             let
               val udiscs = map (rapp u) discs;
@@ -982,11 +987,28 @@
                   |> singleton (Proof_Context.export names_lthy lthy)
                   |> Thm.close_derivation
                 end;
+
+              val disc_eq_case_thms =
+                let
+                  fun term_of_bool b = if b then @{term True} else @{term False};
+                  fun mk_case_args n = map_index (fn (k, argTs) =>
+                    fold_rev Term.absdummy argTs (term_of_bool (n = k))) ctr_Tss;
+                  val goals = map_index (fn (n, udisc) =>
+                    mk_Trueprop_eq (udisc, list_comb (casexBool, mk_case_args n) $ u)) udiscs;
+                in
+                  Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+                    (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (certify ctxt u)
+                       exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms)
+                  |> Conjunction.elim_balanced (length goals)
+                  |> Proof_Context.export names_lthy lthy
+                  |> map Thm.close_derivation
+                end;
             in
               (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
                discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
                [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms,
-               [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm])
+               [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm],
+               disc_eq_case_thms)
             end;
 
         val case_distrib_thm =
@@ -1026,6 +1048,7 @@
            (collapseN, safe_collapse_thms, if ms = [0] then [] else simp_attrs),
            (discN, flat nontriv_disc_thmss, simp_attrs),
            (discIN, nontriv_discI_thms, []),
+           (disc_eq_caseN, disc_eq_case_thms, []),
            (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
            (distinct_discN, distinct_disc_thms, dest_attrs),
            (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
@@ -1073,11 +1096,11 @@
            distincts = distinct_thms, case_thms = case_thms, case_cong = case_cong_thm,
            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}
+           disc_thmss = disc_thmss, discIs = discI_thms, disc_eq_cases = disc_eq_case_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)

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Mon Jan 05 06:56:15 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Fri Dec 19 11:18:58 2014 +0100
@@ -23,6 +23,8 @@
   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
+  val mk_disc_eq_case_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list ->
+    tactic
   val mk_exhaust_disc_tac: int -> thm -> thm list -> tactic
   val mk_exhaust_sel_tac: int -> thm -> thm list -> tactic
   val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
@@ -93,6 +95,14 @@
        REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
        SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
 
+fun mk_disc_eq_case_tac ctxt ct exhaust discs distincts cases =
+  HEADGOAL Goal.conjunction_tac THEN
+  ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+    (hyp_subst_tac ctxt THEN'
+     SELECT_GOAL (unfold_thms_tac ctxt (@{thms not_True_eq_False not_False_eq_True} @ cases @
+       ((refl :: discs @ distincts) RL [eqTrueI, eqFalseI]))) THEN'
+     resolve_tac @{thms TrueI True_not_False False_not_True}));
+
 fun mk_expand_tac ctxt n ms uexhaust_disc vexhaust_disc uncollapses distinct_discsss
     distinct_discsss' =
   if ms = [0] then

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Jan 05 06:56:15 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Dec 19 11:18:58 2014 +0100
@@ -74,6 +74,10 @@
 
   val ss_only: thm list -> Proof.context -> Proof.context
 
+  (*parameterized thms*)
+  val eqTrueI: thm
+  val eqFalseI: thm
+
   val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
   val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
     tactic
@@ -251,6 +255,9 @@
 
 fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
 
+val eqTrueI = @{thm iffD2[OF eq_True]};
+val eqFalseI =  @{thm iffD2[OF eq_False]};
+
 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
 fun WRAP gen_before gen_after xs core_tac =
   fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;

--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Jan 05 06:56:15 2015 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Fri Dec 19 11:18:58 2014 +0100
@@ -116,6 +116,7 @@
      disc_defs = [],
      disc_thmss = [],
      discIs = [],
+     disc_eq_cases = [],
      sel_defs = [],
      sel_thmss = [],
      distinct_discsss = [],

--- a/src/HOL/Tools/record.ML	Mon Jan 05 06:56:15 2015 +0100
+++ b/src/HOL/Tools/record.ML	Fri Dec 19 11:18:58 2014 +0100
@@ -1787,9 +1787,9 @@
      discs = [], selss = [], exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject],
      distincts = [], case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,
      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 = []};
+     disc_thmss = [], discIs = [], disc_eq_cases = [], sel_defs = [], sel_thmss = [sel_thms],
+     distinct_discsss = [], exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [],
+     split_sels = [], split_sel_asms = [], case_eq_ifs = []};
 
 
 (* definition *)