use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
authorblanchet
Thu Jul 24 00:24:00 2014 +0200 (2014-07-24)
changeset 57629e88b5f59cade
parent 57628 c80fc5576271
child 57630 04ab38720b50
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Jul 23 23:16:44 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -190,6 +190,8 @@
     1.4  
     1.5  val isN = "is_";
     1.6  val unN = "un_";
     1.7 +val notN = "not_";
     1.8 +
     1.9  fun mk_unN 1 1 suf = unN ^ suf
    1.10    | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
    1.11  
    1.12 @@ -261,9 +263,6 @@
    1.13  
    1.14  val name_of_ctr = name_of_const "constructor";
    1.15  
    1.16 -val notN = "not_";
    1.17 -val isN = "is_";
    1.18 -
    1.19  fun name_of_disc t =
    1.20    (case head_of t of
    1.21      Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
    1.22 @@ -994,6 +993,26 @@
    1.23            |> map (fn (thmN, thms, attrs) =>
    1.24              ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
    1.25  
    1.26 +        val (noted, lthy') =
    1.27 +          lthy
    1.28 +          |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
    1.29 +          |> fold (Spec_Rules.add Spec_Rules.Equational)
    1.30 +            (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
    1.31 +          |> fold (Spec_Rules.add Spec_Rules.Equational)
    1.32 +            (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
    1.33 +          |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.34 +               (fn phi => Case_Translation.register
    1.35 +                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
    1.36 +          |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
    1.37 +          |> not no_code ?
    1.38 +             Local_Theory.declaration {syntax = false, pervasive = false}
    1.39 +               (fn phi => Context.mapping
    1.40 +                  (add_ctr_code fcT_name (map (Morphism.typ phi) As)
    1.41 +                     (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
    1.42 +                     (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
    1.43 +                  I)
    1.44 +          |> Local_Theory.notes (anonymous_notes @ notes)
    1.45 +
    1.46          val ctr_sugar =
    1.47            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
    1.48             nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
    1.49 @@ -1003,28 +1022,10 @@
    1.50             disc_excludesss = disc_exclude_thmsss, disc_exhausts = disc_exhaust_thms,
    1.51             sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
    1.52             sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
    1.53 -           case_eq_ifs = case_eq_if_thms};
    1.54 +           case_eq_ifs = case_eq_if_thms}
    1.55 +          |> morph_ctr_sugar (substitute_noted_thm noted);
    1.56        in
    1.57 -        (ctr_sugar,
    1.58 -         lthy
    1.59 -         |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
    1.60 -         |> fold (Spec_Rules.add Spec_Rules.Equational)
    1.61 -           (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
    1.62 -         |> fold (Spec_Rules.add Spec_Rules.Equational)
    1.63 -           (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
    1.64 -         |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.65 -              (fn phi => Case_Translation.register
    1.66 -                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
    1.67 -         |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
    1.68 -         |> not no_code ?
    1.69 -            Local_Theory.declaration {syntax = false, pervasive = false}
    1.70 -              (fn phi => Context.mapping
    1.71 -                (add_ctr_code fcT_name (map (Morphism.typ phi) As)
    1.72 -                  (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
    1.73 -                  (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
    1.74 -                I)
    1.75 -         |> Local_Theory.notes (anonymous_notes @ notes) |> snd
    1.76 -         |> register_ctr_sugar fcT_name ctr_sugar)
    1.77 +        (ctr_sugar, lthy' |> register_ctr_sugar fcT_name ctr_sugar)
    1.78        end;
    1.79    in
    1.80      (goalss, after_qed, lthy')
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Jul 23 23:16:44 2014 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jul 24 00:24:00 2014 +0200
     2.3 @@ -68,6 +68,8 @@
     2.4    val certifyT: Proof.context -> typ -> ctyp
     2.5    val certify: Proof.context -> term -> cterm
     2.6  
     2.7 +  val substitute_noted_thm: (string * thm list) list -> morphism
     2.8 +
     2.9    val standard_binding: binding
    2.10    val parse_binding_colon: binding parser
    2.11    val parse_opt_binding_colon: binding parser
    2.12 @@ -234,6 +236,11 @@
    2.13  fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
    2.14  fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
    2.15  
    2.16 +fun substitute_noted_thm noted =
    2.17 +  let val tab = fold (fold (Thmtab.default o `I) o snd) noted Thmtab.empty in
    2.18 +    Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm" (perhaps (Thmtab.lookup tab))
    2.19 +  end
    2.20 +
    2.21  (* The standard binding stands for a name generated following the canonical convention (e.g.,
    2.22     "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no
    2.23     binding at all, depending on the context. *)