src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57983 6edc3529bb4e
parent 57882 38bf4de248a6
child 57984 cbe9a16f8e11
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4       distincts: thm list,
     1.5       case_thms: thm list,
     1.6       case_cong: thm,
     1.7 -     weak_case_cong: thm,
     1.8 +     case_cong_weak: thm,
     1.9       split: thm,
    1.10       split_asm: thm,
    1.11       disc_defs: thm list,
    1.12 @@ -26,13 +26,13 @@
    1.13       discIs: thm list,
    1.14       sel_defs: thm list,
    1.15       sel_thmss: thm list list,
    1.16 -     disc_excludesss: thm list list list,
    1.17 -     disc_exhausts: thm list,
    1.18 -     sel_exhausts: thm list,
    1.19 +     distinct_discsss: thm list list list,
    1.20 +     exhaust_discs: thm list,
    1.21 +     exhaust_sels: thm list,
    1.22       collapses: thm list,
    1.23       expands: thm list,
    1.24 -     sel_splits: thm list,
    1.25 -     sel_split_asms: thm list,
    1.26 +     split_sels: thm list,
    1.27 +     split_sel_asms: thm list,
    1.28       case_eq_ifs: thm list};
    1.29  
    1.30    val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
    1.31 @@ -90,7 +90,7 @@
    1.32     distincts: thm list,
    1.33     case_thms: thm list,
    1.34     case_cong: thm,
    1.35 -   weak_case_cong: thm,
    1.36 +   case_cong_weak: thm,
    1.37     split: thm,
    1.38     split_asm: thm,
    1.39     disc_defs: thm list,
    1.40 @@ -98,19 +98,19 @@
    1.41     discIs: thm list,
    1.42     sel_defs: thm list,
    1.43     sel_thmss: thm list list,
    1.44 -   disc_excludesss: thm list list list,
    1.45 -   disc_exhausts: thm list,
    1.46 -   sel_exhausts: thm list,
    1.47 +   distinct_discsss: thm list list list,
    1.48 +   exhaust_discs: thm list,
    1.49 +   exhaust_sels: thm list,
    1.50     collapses: thm list,
    1.51     expands: thm list,
    1.52 -   sel_splits: thm list,
    1.53 -   sel_split_asms: thm list,
    1.54 +   split_sels: thm list,
    1.55 +   split_sel_asms: thm list,
    1.56     case_eq_ifs: thm list};
    1.57  
    1.58  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    1.59 -    case_thms, case_cong, weak_case_cong, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
    1.60 -    sel_thmss, disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits,
    1.61 -    sel_split_asms, case_eq_ifs} =
    1.62 +    case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
    1.63 +    sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels,
    1.64 +    split_sel_asms, case_eq_ifs} =
    1.65    {ctrs = map (Morphism.term phi) ctrs,
    1.66     casex = Morphism.term phi casex,
    1.67     discs = map (Morphism.term phi) discs,
    1.68 @@ -121,7 +121,7 @@
    1.69     distincts = map (Morphism.thm phi) distincts,
    1.70     case_thms = map (Morphism.thm phi) case_thms,
    1.71     case_cong = Morphism.thm phi case_cong,
    1.72 -   weak_case_cong = Morphism.thm phi weak_case_cong,
    1.73 +   case_cong_weak = Morphism.thm phi case_cong_weak,
    1.74     split = Morphism.thm phi split,
    1.75     split_asm = Morphism.thm phi split_asm,
    1.76     disc_defs = map (Morphism.thm phi) disc_defs,
    1.77 @@ -129,13 +129,13 @@
    1.78     discIs = map (Morphism.thm phi) discIs,
    1.79     sel_defs = map (Morphism.thm phi) sel_defs,
    1.80     sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
    1.81 -   disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss,
    1.82 -   disc_exhausts = map (Morphism.thm phi) disc_exhausts,
    1.83 -   sel_exhausts = map (Morphism.thm phi) sel_exhausts,
    1.84 +   distinct_discsss = map (map (map (Morphism.thm phi))) distinct_discsss,
    1.85 +   exhaust_discs = map (Morphism.thm phi) exhaust_discs,
    1.86 +   exhaust_sels = map (Morphism.thm phi) exhaust_sels,
    1.87     collapses = map (Morphism.thm phi) collapses,
    1.88     expands = map (Morphism.thm phi) expands,
    1.89 -   sel_splits = map (Morphism.thm phi) sel_splits,
    1.90 -   sel_split_asms = map (Morphism.thm phi) sel_split_asms,
    1.91 +   split_sels = map (Morphism.thm phi) split_sels,
    1.92 +   split_sel_asms = map (Morphism.thm phi) split_sel_asms,
    1.93     case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
    1.94  
    1.95  val transfer_ctr_sugar =
    1.96 @@ -200,23 +200,23 @@
    1.97  val case_congN = "case_cong";
    1.98  val case_eq_ifN = "case_eq_if";
    1.99  val collapseN = "collapse";
   1.100 -val disc_excludeN = "disc_exclude";
   1.101 -val disc_exhaustN = "disc_exhaust";
   1.102  val discN = "disc";
   1.103  val discIN = "discI";
   1.104  val distinctN = "distinct";
   1.105 +val distinct_discN = "distinct_disc";
   1.106  val exhaustN = "exhaust";
   1.107 +val exhaust_discN = "exhaust_disc";
   1.108  val expandN = "expand";
   1.109  val injectN = "inject";
   1.110  val nchotomyN = "nchotomy";
   1.111  val selN = "sel";
   1.112 -val sel_exhaustN = "sel_exhaust";
   1.113 -val sel_splitN = "sel_split";
   1.114 -val sel_split_asmN = "sel_split_asm";
   1.115 +val exhaust_selN = "exhaust_sel";
   1.116  val splitN = "split";
   1.117 +val split_asmN = "split_asm";
   1.118 +val split_selN = "split_sel";
   1.119 +val split_sel_asmN = "split_sel_asm";
   1.120  val splitsN = "splits";
   1.121 -val split_asmN = "split_asm";
   1.122 -val weak_case_cong_thmsN = "weak_case_cong";
   1.123 +val case_cong_weak_thmsN = "case_cong_weak";
   1.124  
   1.125  val cong_attrs = @{attributes [cong]};
   1.126  val dest_attrs = @{attributes [dest]};
   1.127 @@ -677,7 +677,7 @@
   1.128                ks goals inject_thmss distinct_thmsss
   1.129            end;
   1.130  
   1.131 -        val (case_cong_thm, weak_case_cong_thm) =
   1.132 +        val (case_cong_thm, case_cong_weak_thm) =
   1.133            let
   1.134              fun mk_prem xctr xs xf xg =
   1.135                fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
   1.136 @@ -733,9 +733,9 @@
   1.137            end;
   1.138  
   1.139          val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
   1.140 -             discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
   1.141 -             disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, safe_collapse_thms,
   1.142 -             expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
   1.143 +             discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
   1.144 +             exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms,
   1.145 +             expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms) =
   1.146            if no_discs_sels then
   1.147              ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
   1.148            else
   1.149 @@ -827,7 +827,7 @@
   1.150                  flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings
   1.151                    discI_thms);
   1.152  
   1.153 -              val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
   1.154 +              val (distinct_disc_thms, (distinct_disc_thmsss', distinct_disc_thmsss)) =
   1.155                  let
   1.156                    fun mk_goal [] = []
   1.157                      | mk_goal [((_, udisc), (_, udisc'))] =
   1.158 @@ -843,25 +843,25 @@
   1.159                    val half_goalss = map mk_goal half_pairss;
   1.160                    val half_thmss =
   1.161                      map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
   1.162 -                        fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal])
   1.163 +                        fn disc_thm => [prove (mk_half_distinct_disc_tac lthy m discD disc_thm) goal])
   1.164                        half_goalss half_pairss (flat disc_thmss');
   1.165  
   1.166                    val other_half_goalss = map (mk_goal o map swap) half_pairss;
   1.167                    val other_half_thmss =
   1.168 -                    map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
   1.169 +                    map2 (map2 (prove o mk_other_half_distinct_disc_tac)) half_thmss
   1.170                        other_half_goalss;
   1.171                  in
   1.172                    join_halves n half_thmss other_half_thmss ||> `transpose
   1.173                    |>> has_alternate_disc_def ? K []
   1.174                  end;
   1.175  
   1.176 -              val disc_exhaust_thm =
   1.177 +              val exhaust_disc_thm =
   1.178                  let
   1.179                    fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
   1.180                    val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
   1.181                  in
   1.182                    Goal.prove_sorry lthy [] [] goal (fn _ =>
   1.183 -                    mk_disc_exhaust_tac n exhaust_thm discI_thms)
   1.184 +                    mk_exhaust_disc_tac n exhaust_thm discI_thms)
   1.185                    |> Thm.close_derivation
   1.186                  end;
   1.187  
   1.188 @@ -890,13 +890,13 @@
   1.189                val swapped_all_collapse_thms =
   1.190                  map2 (fn m => fn thm => if m = 0 then thm else thm RS sym) ms all_collapse_thms;
   1.191  
   1.192 -              val sel_exhaust_thm =
   1.193 +              val exhaust_sel_thm =
   1.194                  let
   1.195                    fun mk_prem usel_ctr = mk_imp_p [mk_Trueprop_eq (u, usel_ctr)];
   1.196                    val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem usel_ctrs));
   1.197                  in
   1.198                    Goal.prove_sorry lthy [] [] goal (fn _ =>
   1.199 -                    mk_sel_exhaust_tac n disc_exhaust_thm swapped_all_collapse_thms)
   1.200 +                    mk_exhaust_sel_tac n exhaust_disc_thm swapped_all_collapse_thms)
   1.201                    |> Thm.close_derivation
   1.202                  end;
   1.203  
   1.204 @@ -919,14 +919,14 @@
   1.205                      map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
   1.206                  in
   1.207                    Goal.prove_sorry lthy [] [] goal (fn _ =>
   1.208 -                    mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
   1.209 -                      (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
   1.210 -                      disc_exclude_thmsss')
   1.211 +                    mk_expand_tac lthy n ms (inst_thm u exhaust_disc_thm)
   1.212 +                      (inst_thm v exhaust_disc_thm) uncollapse_thms distinct_disc_thmsss
   1.213 +                      distinct_disc_thmsss')
   1.214                    |> singleton (Proof_Context.export names_lthy lthy)
   1.215                    |> Thm.close_derivation
   1.216                  end;
   1.217  
   1.218 -              val (sel_split_thm, sel_split_asm_thm) =
   1.219 +              val (split_sel_thm, split_sel_asm_thm) =
   1.220                  let
   1.221                    val zss = map (K []) xss;
   1.222                    val goal = mk_split_goal usel_ctrs zss usel_fs;
   1.223 @@ -949,9 +949,9 @@
   1.224                  end;
   1.225              in
   1.226                (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
   1.227 -               discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
   1.228 -               [disc_exhaust_thm], [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms,
   1.229 -               [expand_thm], [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
   1.230 +               discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
   1.231 +               [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms,
   1.232 +               [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm])
   1.233              end;
   1.234  
   1.235          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
   1.236 @@ -966,30 +966,28 @@
   1.237             (flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)]
   1.238            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   1.239  
   1.240 -        (* "exhaust" is deliberately put first to avoid apparent circular dependencies in the proof
   1.241 -           objects, which would confuse MaSh. *)
   1.242          val notes =
   1.243 -          [(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
   1.244 -           (caseN, case_thms, code_nitpicksimp_simp_attrs),
   1.245 +          [(caseN, case_thms, code_nitpicksimp_simp_attrs),
   1.246             (case_congN, [case_cong_thm], []),
   1.247 +           (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
   1.248             (case_eq_ifN, case_eq_if_thms, []),
   1.249             (collapseN, safe_collapse_thms, simp_attrs),
   1.250             (discN, flat nontriv_disc_thmss, simp_attrs),
   1.251             (discIN, nontriv_discI_thms, []),
   1.252 -           (disc_excludeN, disc_exclude_thms, dest_attrs),
   1.253 -           (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
   1.254             (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
   1.255 +           (distinct_discN, distinct_disc_thms, dest_attrs),
   1.256 +           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
   1.257 +           (exhaust_discN, exhaust_disc_thms, [exhaust_case_names_attr]),
   1.258 +           (exhaust_selN, exhaust_sel_thms, [exhaust_case_names_attr]),
   1.259             (expandN, expand_thms, []),
   1.260             (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
   1.261             (nchotomyN, [nchotomy_thm], []),
   1.262             (selN, all_sel_thms, code_nitpicksimp_simp_attrs),
   1.263 -           (sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]),
   1.264 -           (sel_splitN, sel_split_thms, []),
   1.265 -           (sel_split_asmN, sel_split_asm_thms, []),
   1.266 +           (split_selN, split_sel_thms, []),
   1.267 +           (split_sel_asmN, split_sel_asm_thms, []),
   1.268             (splitN, [split_thm], []),
   1.269             (split_asmN, [split_asm_thm], []),
   1.270 -           (splitsN, [split_thm, split_asm_thm], []),
   1.271 -           (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
   1.272 +           (splitsN, [split_thm, split_asm_thm], [])]
   1.273            |> filter_out (null o #2)
   1.274            |> map (fn (thmN, thms, attrs) =>
   1.275              ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
   1.276 @@ -1019,12 +1017,12 @@
   1.277          val ctr_sugar =
   1.278            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
   1.279             nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
   1.280 -           case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
   1.281 +           case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm,
   1.282             split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
   1.283             disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss,
   1.284 -           disc_excludesss = disc_exclude_thmsss, disc_exhausts = disc_exhaust_thms,
   1.285 -           sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
   1.286 -           sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
   1.287 +           distinct_discsss = distinct_disc_thmsss, exhaust_discs = exhaust_disc_thms,
   1.288 +           exhaust_sels = exhaust_sel_thms, collapses = all_collapse_thms, expands = expand_thms,
   1.289 +           split_sels = split_sel_thms, split_sel_asms = split_sel_asm_thms,
   1.290             case_eq_ifs = case_eq_if_thms}
   1.291            |> morph_ctr_sugar (substitute_noted_thm noted);
   1.292        in