# HG changeset patch
# User blanchet
# Date 1406154240 -7200
# Node ID e88b5f59cadedd35b5949d69cd0429d2236cf12d
# Parent  c80fc5576271a6d46d74a9325c291bb1d18a183a
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)

diff -r c80fc5576271 -r e88b5f59cade src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Jul 23 23:16:44 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
@@ -190,6 +190,8 @@
 
 val isN = "is_";
 val unN = "un_";
+val notN = "not_";
+
 fun mk_unN 1 1 suf = unN ^ suf
   | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
 
@@ -261,9 +263,6 @@
 
 val name_of_ctr = name_of_const "constructor";
 
-val notN = "not_";
-val isN = "is_";
-
 fun name_of_disc t =
   (case head_of t of
     Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
@@ -994,6 +993,26 @@
           |> map (fn (thmN, thms, attrs) =>
             ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
 
+        val (noted, lthy') =
+          lthy
+          |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
+          |> fold (Spec_Rules.add Spec_Rules.Equational)
+            (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
+          |> fold (Spec_Rules.add Spec_Rules.Equational)
+            (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
+          |> Local_Theory.declaration {syntax = false, pervasive = true}
+               (fn phi => Case_Translation.register
+                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
+          |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
+          |> not no_code ?
+             Local_Theory.declaration {syntax = false, pervasive = false}
+               (fn phi => Context.mapping
+                  (add_ctr_code fcT_name (map (Morphism.typ phi) As)
+                     (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
+                     (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
+                  I)
+          |> Local_Theory.notes (anonymous_notes @ notes)
+
         val ctr_sugar =
           {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
            nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
@@ -1003,28 +1022,10 @@
            disc_excludesss = disc_exclude_thmsss, disc_exhausts = disc_exhaust_thms,
            sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
            sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
-           case_eq_ifs = case_eq_if_thms};
+           case_eq_ifs = case_eq_if_thms}
+          |> morph_ctr_sugar (substitute_noted_thm noted);
       in
-        (ctr_sugar,
-         lthy
-         |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
-         |> fold (Spec_Rules.add Spec_Rules.Equational)
-           (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
-         |> fold (Spec_Rules.add Spec_Rules.Equational)
-           (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
-         |> Local_Theory.declaration {syntax = false, pervasive = true}
-              (fn phi => Case_Translation.register
-                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
-         |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
-         |> not no_code ?
-            Local_Theory.declaration {syntax = false, pervasive = false}
-              (fn phi => Context.mapping
-                (add_ctr_code fcT_name (map (Morphism.typ phi) As)
-                  (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
-                  (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
-                I)
-         |> Local_Theory.notes (anonymous_notes @ notes) |> snd
-         |> register_ctr_sugar fcT_name ctr_sugar)
+        (ctr_sugar, lthy' |> register_ctr_sugar fcT_name ctr_sugar)
       end;
   in
     (goalss, after_qed, lthy')
diff -r c80fc5576271 -r e88b5f59cade src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Jul 23 23:16:44 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jul 24 00:24:00 2014 +0200
@@ -68,6 +68,8 @@
   val certifyT: Proof.context -> typ -> ctyp
   val certify: Proof.context -> term -> cterm
 
+  val substitute_noted_thm: (string * thm list) list -> morphism
+
   val standard_binding: binding
   val parse_binding_colon: binding parser
   val parse_opt_binding_colon: binding parser
@@ -234,6 +236,11 @@
 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
 
+fun substitute_noted_thm noted =
+  let val tab = fold (fold (Thmtab.default o `I) o snd) noted Thmtab.empty in
+    Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm" (perhaps (Thmtab.lookup tab))
+  end
+
 (* The standard binding stands for a name generated following the canonical convention (e.g.,
    "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no
    binding at all, depending on the context. *)