src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55464 56fa33537869
parent 55444 ec73f81e49e7
child 55468 98b25c51e9e5
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     1.3 @@ -653,10 +653,10 @@
     1.4              (thm, asm_thm)
     1.5            end;
     1.6  
     1.7 -        val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
     1.8 -             disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms, sel_exhaust_thms,
     1.9 -             all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms,
    1.10 -             case_eq_if_thms) =
    1.11 +        val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms,
    1.12 +             nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms,
    1.13 +             sel_exhaust_thms, all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms,
    1.14 +             sel_split_asm_thms, case_eq_if_thms) =
    1.15            if no_discs_sels then
    1.16              ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    1.17            else
    1.18 @@ -738,9 +738,8 @@
    1.19                    map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
    1.20                  end;
    1.21  
    1.22 -              val nontriv_disc_thms =
    1.23 -                flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
    1.24 -                  disc_bindings disc_thmss);
    1.25 +              val nontriv_disc_thmss =
    1.26 +                map2 (fn b => if is_disc_binding_valid b then I else K []) disc_bindings disc_thmss;
    1.27  
    1.28                fun is_discI_boring b =
    1.29                  (n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding);
    1.30 @@ -870,7 +869,7 @@
    1.31                    |> Thm.close_derivation
    1.32                  end;
    1.33              in
    1.34 -              (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
    1.35 +              (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms,
    1.36                 nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, [disc_exhaust_thm],
    1.37                 [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm],
    1.38                 [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
    1.39 @@ -879,11 +878,13 @@
    1.40          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    1.41          val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
    1.42  
    1.43 +        val nontriv_disc_eq_thmss =
    1.44 +          map (map (fn th => th RS @{thm eq_False[THEN iffD2]}
    1.45 +            handle THM _ => th RS @{thm eq_True[THEN iffD2]})) nontriv_disc_thmss;
    1.46 +
    1.47          val anonymous_notes =
    1.48            [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
    1.49 -           (map (fn th => th RS @{thm eq_False[THEN iffD2]}
    1.50 -              handle THM _ => th RS @{thm eq_True[THEN iffD2]}) nontriv_disc_thms,
    1.51 -            code_nitpicksimp_attrs)]
    1.52 +           (flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)]
    1.53            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    1.54  
    1.55          val notes =
    1.56 @@ -891,7 +892,7 @@
    1.57             (case_congN, [case_cong_thm], []),
    1.58             (case_eq_ifN, case_eq_if_thms, []),
    1.59             (collapseN, safe_collapse_thms, simp_attrs),
    1.60 -           (discN, nontriv_disc_thms, simp_attrs),
    1.61 +           (discN, flat nontriv_disc_thmss, simp_attrs),
    1.62             (discIN, nontriv_discI_thms, []),
    1.63             (disc_excludeN, disc_exclude_thms, dest_attrs),
    1.64             (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
    1.65 @@ -924,6 +925,9 @@
    1.66        in
    1.67          (ctr_sugar,
    1.68           lthy
    1.69 +         |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
    1.70 +         |> Spec_Rules.add Spec_Rules.Equational (flat selss, all_sel_thms)
    1.71 +         |> fold (Spec_Rules.add Spec_Rules.Equational) (map single discs ~~ nontriv_disc_eq_thmss)
    1.72           |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.73                (fn phi => Case_Translation.register
    1.74                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs))