src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57629 e88b5f59cade
parent 57260 8747af0d1012
child 57631 959caab43a3d
     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')