src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 54900 136fe16e726a
parent 54740 91f54d386680
child 54970 891141de5672
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4       disc_thmss: thm list list,
     1.5       discIs: thm list,
     1.6       sel_thmss: thm list list,
     1.7 +     disc_excludesss: thm list list list,
     1.8       disc_exhausts: thm list,
     1.9       sel_exhausts: thm list,
    1.10       collapses: thm list,
    1.11 @@ -85,6 +86,7 @@
    1.12     disc_thmss: thm list list,
    1.13     discIs: thm list,
    1.14     sel_thmss: thm list list,
    1.15 +   disc_excludesss: thm list list list,
    1.16     disc_exhausts: thm list,
    1.17     sel_exhausts: thm list,
    1.18     collapses: thm list,
    1.19 @@ -99,7 +101,8 @@
    1.20  
    1.21  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    1.22      case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
    1.23 -    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_ifs} =
    1.24 +    disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms,
    1.25 +    case_eq_ifs} =
    1.26    {ctrs = map (Morphism.term phi) ctrs,
    1.27     casex = Morphism.term phi casex,
    1.28     discs = map (Morphism.term phi) discs,
    1.29 @@ -116,6 +119,7 @@
    1.30     disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    1.31     discIs = map (Morphism.thm phi) discIs,
    1.32     sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
    1.33 +   disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss,
    1.34     disc_exhausts = map (Morphism.thm phi) disc_exhausts,
    1.35     sel_exhausts = map (Morphism.thm phi) sel_exhausts,
    1.36     collapses = map (Morphism.thm phi) collapses,
    1.37 @@ -657,10 +661,11 @@
    1.38            end;
    1.39  
    1.40          val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
    1.41 -             disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
    1.42 -             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
    1.43 +             disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms, sel_exhaust_thms,
    1.44 +             all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms,
    1.45 +             case_eq_if_thms) =
    1.46            if no_discs_sels then
    1.47 -            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    1.48 +            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    1.49            else
    1.50              let
    1.51                val udiscs = map (rapp u) discs;
    1.52 @@ -873,9 +878,9 @@
    1.53                  end;
    1.54              in
    1.55                (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
    1.56 -               nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
    1.57 -               all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
    1.58 -               [sel_split_asm_thm], [case_eq_if_thm])
    1.59 +               nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, [disc_exhaust_thm],
    1.60 +               [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm],
    1.61 +               [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
    1.62              end;
    1.63  
    1.64          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    1.65 @@ -919,10 +924,10 @@
    1.66             nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
    1.67             case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
    1.68             split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
    1.69 -           discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
    1.70 -           sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
    1.71 -           sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
    1.72 -           case_eq_ifs = case_eq_if_thms};
    1.73 +           discIs = discI_thms, sel_thmss = sel_thmss, disc_excludesss = disc_exclude_thmsss,
    1.74 +           disc_exhausts = disc_exhaust_thms, sel_exhausts = sel_exhaust_thms,
    1.75 +           collapses = all_collapse_thms, expands = expand_thms, sel_splits = sel_split_thms,
    1.76 +           sel_split_asms = sel_split_asm_thms, case_eq_ifs = case_eq_if_thms};
    1.77        in
    1.78          (ctr_sugar,
    1.79           lthy