src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 56858 0c3d0bc98abe
parent 56767 9b311dbd0f55
child 57038 2114f3224b2c
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 05 08:30:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 05 09:30:20 2014 +0200
     1.3 @@ -21,8 +21,10 @@
     1.4       weak_case_cong: thm,
     1.5       split: thm,
     1.6       split_asm: thm,
     1.7 +     disc_defs: thm list,
     1.8       disc_thmss: thm list list,
     1.9       discIs: thm list,
    1.10 +     sel_defs: thm list,
    1.11       sel_thmss: thm list list,
    1.12       disc_excludesss: thm list list list,
    1.13       disc_exhausts: thm list,
    1.14 @@ -90,8 +92,10 @@
    1.15     weak_case_cong: thm,
    1.16     split: thm,
    1.17     split_asm: thm,
    1.18 +   disc_defs: thm list,
    1.19     disc_thmss: thm list list,
    1.20     discIs: thm list,
    1.21 +   sel_defs: thm list,
    1.22     sel_thmss: thm list list,
    1.23     disc_excludesss: thm list list list,
    1.24     disc_exhausts: thm list,
    1.25 @@ -103,9 +107,9 @@
    1.26     case_eq_ifs: thm list};
    1.27  
    1.28  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    1.29 -    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
    1.30 -    disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms,
    1.31 -    case_eq_ifs} =
    1.32 +    case_thms, case_cong, weak_case_cong, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
    1.33 +    sel_thmss, disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits,
    1.34 +    sel_split_asms, case_eq_ifs} =
    1.35    {ctrs = map (Morphism.term phi) ctrs,
    1.36     casex = Morphism.term phi casex,
    1.37     discs = map (Morphism.term phi) discs,
    1.38 @@ -119,8 +123,10 @@
    1.39     weak_case_cong = Morphism.thm phi weak_case_cong,
    1.40     split = Morphism.thm phi split,
    1.41     split_asm = Morphism.thm phi split_asm,
    1.42 +   disc_defs = map (Morphism.thm phi) disc_defs,
    1.43     disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    1.44     discIs = map (Morphism.thm phi) discIs,
    1.45 +   sel_defs = map (Morphism.thm phi) sel_defs,
    1.46     sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
    1.47     disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss,
    1.48     disc_exhausts = map (Morphism.thm phi) disc_exhausts,
    1.49 @@ -692,12 +698,12 @@
    1.50              (thm, asm_thm)
    1.51            end;
    1.52  
    1.53 -        val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms,
    1.54 -             nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms,
    1.55 -             sel_exhaust_thms, all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms,
    1.56 -             sel_split_asm_thms, case_eq_if_thms) =
    1.57 +        val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
    1.58 +             discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
    1.59 +             disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, safe_collapse_thms,
    1.60 +             expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
    1.61            if no_discs_sels then
    1.62 -            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    1.63 +            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    1.64            else
    1.65              let
    1.66                val udiscs = map (rapp u) discs;
    1.67 @@ -908,10 +914,10 @@
    1.68                    |> Thm.close_derivation
    1.69                  end;
    1.70              in
    1.71 -              (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms,
    1.72 -               nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, [disc_exhaust_thm],
    1.73 -               [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm],
    1.74 -               [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
    1.75 +              (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
    1.76 +               discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
    1.77 +               [disc_exhaust_thm], [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms,
    1.78 +               [expand_thm], [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
    1.79              end;
    1.80  
    1.81          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    1.82 @@ -956,11 +962,12 @@
    1.83            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
    1.84             nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
    1.85             case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
    1.86 -           split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
    1.87 -           discIs = discI_thms, sel_thmss = sel_thmss, disc_excludesss = disc_exclude_thmsss,
    1.88 -           disc_exhausts = disc_exhaust_thms, sel_exhausts = sel_exhaust_thms,
    1.89 -           collapses = all_collapse_thms, expands = expand_thms, sel_splits = sel_split_thms,
    1.90 -           sel_split_asms = sel_split_asm_thms, case_eq_ifs = case_eq_if_thms};
    1.91 +           split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
    1.92 +           disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss,
    1.93 +           disc_excludesss = disc_exclude_thmsss, disc_exhausts = disc_exhaust_thms,
    1.94 +           sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
    1.95 +           sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
    1.96 +           case_eq_ifs = case_eq_if_thms};
    1.97        in
    1.98          (ctr_sugar,
    1.99           lthy