have 'Ctr_Sugar' register its 'Spec_Rules'
authorblanchet
Fri Feb 14 07:53:45 2014 +0100 (2014-02-14)
changeset 5546456fa33537869
parent 55463 942c2153b5b4
child 55465 0d31c0546286
have 'Ctr_Sugar' register its 'Spec_Rules'
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     1.3 @@ -569,8 +569,9 @@
     1.4            val (bs, attrss) = map_split (fst o nth specs) poss;
     1.5            val notes =
     1.6              map3 (fn b => fn attrs => fn thm =>
     1.7 -              ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs), [([thm], [])]))
     1.8 -            bs attrss thms;
     1.9 +                ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs),
    1.10 +                 [([thm], [])]))
    1.11 +              bs attrss thms;
    1.12          in
    1.13            ((Binding.qualify true prefix (Binding.name simpsN), []), [(thms, [])]) :: notes
    1.14          end);
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     2.3 @@ -653,10 +653,10 @@
     2.4              (thm, asm_thm)
     2.5            end;
     2.6  
     2.7 -        val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
     2.8 -             disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms, sel_exhaust_thms,
     2.9 -             all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms,
    2.10 -             case_eq_if_thms) =
    2.11 +        val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms,
    2.12 +             nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms,
    2.13 +             sel_exhaust_thms, all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms,
    2.14 +             sel_split_asm_thms, case_eq_if_thms) =
    2.15            if no_discs_sels then
    2.16              ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    2.17            else
    2.18 @@ -738,9 +738,8 @@
    2.19                    map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
    2.20                  end;
    2.21  
    2.22 -              val nontriv_disc_thms =
    2.23 -                flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
    2.24 -                  disc_bindings disc_thmss);
    2.25 +              val nontriv_disc_thmss =
    2.26 +                map2 (fn b => if is_disc_binding_valid b then I else K []) disc_bindings disc_thmss;
    2.27  
    2.28                fun is_discI_boring b =
    2.29                  (n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding);
    2.30 @@ -870,7 +869,7 @@
    2.31                    |> Thm.close_derivation
    2.32                  end;
    2.33              in
    2.34 -              (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
    2.35 +              (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms,
    2.36                 nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, [disc_exhaust_thm],
    2.37                 [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm],
    2.38                 [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
    2.39 @@ -879,11 +878,13 @@
    2.40          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    2.41          val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
    2.42  
    2.43 +        val nontriv_disc_eq_thmss =
    2.44 +          map (map (fn th => th RS @{thm eq_False[THEN iffD2]}
    2.45 +            handle THM _ => th RS @{thm eq_True[THEN iffD2]})) nontriv_disc_thmss;
    2.46 +
    2.47          val anonymous_notes =
    2.48            [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
    2.49 -           (map (fn th => th RS @{thm eq_False[THEN iffD2]}
    2.50 -              handle THM _ => th RS @{thm eq_True[THEN iffD2]}) nontriv_disc_thms,
    2.51 -            code_nitpicksimp_attrs)]
    2.52 +           (flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)]
    2.53            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    2.54  
    2.55          val notes =
    2.56 @@ -891,7 +892,7 @@
    2.57             (case_congN, [case_cong_thm], []),
    2.58             (case_eq_ifN, case_eq_if_thms, []),
    2.59             (collapseN, safe_collapse_thms, simp_attrs),
    2.60 -           (discN, nontriv_disc_thms, simp_attrs),
    2.61 +           (discN, flat nontriv_disc_thmss, simp_attrs),
    2.62             (discIN, nontriv_discI_thms, []),
    2.63             (disc_excludeN, disc_exclude_thms, dest_attrs),
    2.64             (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
    2.65 @@ -924,6 +925,9 @@
    2.66        in
    2.67          (ctr_sugar,
    2.68           lthy
    2.69 +         |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
    2.70 +         |> Spec_Rules.add Spec_Rules.Equational (flat selss, all_sel_thms)
    2.71 +         |> fold (Spec_Rules.add Spec_Rules.Equational) (map single discs ~~ nontriv_disc_eq_thmss)
    2.72           |> Local_Theory.declaration {syntax = false, pervasive = true}
    2.73                (fn phi => Case_Translation.register
    2.74                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs))