simplify selectors in code views
authorblanchet
Mon May 05 09:30:20 2014 +0200 (2014-05-05)
changeset 568580c3d0bc98abe
parent 56857 aa2de99be748
child 56859 bc50d5e04e90
simplify selectors in code views
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Datatype/datatype_data.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon May 05 08:30:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon May 05 09:30:20 2014 +0200
     1.3 @@ -78,6 +78,7 @@
     1.4  type corec_spec =
     1.5    {corec: term,
     1.6     disc_exhausts: thm list,
     1.7 +   sel_defs: thm list,
     1.8     nested_maps: thm list,
     1.9     nested_map_idents: thm list,
    1.10     nested_map_comps: thm list,
    1.11 @@ -459,12 +460,11 @@
    1.12            disc_excludesss collapses corec_thms disc_corecs sel_corecss
    1.13        end;
    1.14  
    1.15 -    fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_rec = corec,
    1.16 +    fun mk_spec ({T, ctr_sugar as {disc_exhausts, sel_defs, ...}, co_rec = corec,
    1.17          co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
    1.18          sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
    1.19 -      {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec,
    1.20 -       disc_exhausts = disc_exhausts,
    1.21 -       nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
    1.22 +      {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts,
    1.23 +       sel_defs = sel_defs, nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
    1.24         nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
    1.25         nested_map_comps = map map_comp_of_bnf nested_bnfs,
    1.26         ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
    1.27 @@ -786,7 +786,9 @@
    1.28  
    1.29  fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)
    1.30      ({fun_args, ctr_no, prems, ...} : coeqn_data_disc) =
    1.31 -  if is_none (#pred (nth ctr_specs ctr_no)) then I else
    1.32 +  if is_none (#pred (nth ctr_specs ctr_no)) then
    1.33 +    I
    1.34 +  else
    1.35      s_conjs prems
    1.36      |> curry subst_bounds (List.rev fun_args)
    1.37      |> abs_tuple_balanced fun_args
    1.38 @@ -1171,9 +1173,10 @@
    1.39                  |> single
    1.40              end;
    1.41  
    1.42 -        fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
    1.43 +        fun prove_sel ({sel_defs, nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
    1.44                : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
    1.45 -            ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, eqn_pos, ...} : coeqn_data_sel) =
    1.46 +            ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, code_rhs_opt, eqn_pos, ...}
    1.47 +             : coeqn_data_sel) =
    1.48            let
    1.49              val SOME ctr_spec = find_first (curry (op =) ctr o #ctr) ctr_specs;
    1.50              val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs;
    1.51 @@ -1196,12 +1199,14 @@
    1.52                nested_map_idents nested_map_comps sel_corec k m excludesss
    1.53              |> K |> Goal.prove_sorry lthy [] [] goal
    1.54              |> Thm.close_derivation
    1.55 +            |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
    1.56              |> pair sel
    1.57              |> pair eqn_pos
    1.58            end;
    1.59  
    1.60 -        fun prove_ctr disc_alist sel_alist (disc_eqns : coeqn_data_disc list)
    1.61 -            (sel_eqns : coeqn_data_sel list) ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) =
    1.62 +        fun prove_ctr disc_alist sel_alist ({sel_defs, ...} : corec_spec)
    1.63 +            (disc_eqns : coeqn_data_disc list) (sel_eqns : coeqn_data_sel list)
    1.64 +            ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) =
    1.65            (* don't try to prove theorems when some sel_eqns are missing *)
    1.66            if not (exists (curry (op =) ctr o #ctr) disc_eqns)
    1.67                andalso not (exists (curry (op =) ctr o #ctr) sel_eqns)
    1.68 @@ -1212,17 +1217,17 @@
    1.69              []
    1.70            else
    1.71              let
    1.72 -              val (fun_name, fun_T, fun_args, prems, rhs_opt, eqn_pos) =
    1.73 +              val (fun_name, fun_T, fun_args, prems, ctr_rhs_opt, code_rhs_opt, eqn_pos) =
    1.74                  (find_first (curry (op =) ctr o #ctr) disc_eqns,
    1.75                   find_first (curry (op =) ctr o #ctr) sel_eqns)
    1.76                  |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x,
    1.77 -                  #ctr_rhs_opt x, #eqn_pos x))
    1.78 -                ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #ctr_rhs_opt x,
    1.79 -                  #eqn_pos x))
    1.80 +                  #ctr_rhs_opt x, #code_rhs_opt x, #eqn_pos x))
    1.81 +                ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [],
    1.82 +                  #ctr_rhs_opt x, #code_rhs_opt x, #eqn_pos x))
    1.83                  |> the o merge_options;
    1.84                val m = length prems;
    1.85                val goal =
    1.86 -                (case rhs_opt of
    1.87 +                (case ctr_rhs_opt of
    1.88                    SOME rhs => rhs
    1.89                  | NONE =>
    1.90                    filter (curry (op =) ctr o #ctr) sel_eqns
    1.91 @@ -1233,11 +1238,14 @@
    1.92                  |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
    1.93                  |> curry Logic.list_all (map dest_Free fun_args);
    1.94                val disc_thm_opt = AList.lookup (op =) disc_alist disc;
    1.95 -              val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist);
    1.96 +              val sel_thms = map (snd o snd) (filter (member (op =) sels o fst) sel_alist);
    1.97              in
    1.98 -              if prems = [@{term False}] then [] else
    1.99 +              if prems = [@{term False}] then
   1.100 +                []
   1.101 +              else
   1.102                  mk_primcorec_ctr_tac lthy m collapse disc_thm_opt sel_thms
   1.103                  |> K |> Goal.prove_sorry lthy [] [] goal
   1.104 +                |> is_some code_rhs_opt ? fold_thms lthy sel_defs (*mildly too aggressive*)
   1.105                  |> Thm.close_derivation
   1.106                  |> pair ctr
   1.107                  |> pair eqn_pos
   1.108 @@ -1274,7 +1282,9 @@
   1.109                    | NONE =>
   1.110                      let
   1.111                        fun prove_code_ctr ({ctr, sels, ...} : corec_ctr_spec) =
   1.112 -                        if not (exists (curry (op =) ctr o fst) ctr_alist) then NONE else
   1.113 +                        if not (exists (curry (op =) ctr o fst) ctr_alist) then
   1.114 +                          NONE
   1.115 +                        else
   1.116                            let
   1.117                              val prems = find_first (curry (op =) ctr o #ctr) disc_eqns
   1.118                                |> Option.map #prems |> the_default [];
   1.119 @@ -1337,7 +1347,7 @@
   1.120          val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss;
   1.121          val disc_thmss = map (map snd o sort_list_duplicates o flat) disc_alistss;
   1.122          val disc_thmsss' = map (map (map (snd o snd))) disc_alistss;
   1.123 -        val sel_thmss = map (map snd o sort_list_duplicates) sel_alists;
   1.124 +        val sel_thmss = map (map (fst o snd) o sort_list_duplicates) sel_alists;
   1.125  
   1.126          fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
   1.127              (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
   1.128 @@ -1366,8 +1376,8 @@
   1.129            disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss
   1.130            |> map sort_list_duplicates;
   1.131  
   1.132 -        val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists)
   1.133 -          disc_eqnss sel_eqnss ctr_specss;
   1.134 +        val ctr_alists = map6 (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists
   1.135 +          (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss;
   1.136          val ctr_thmss' = map (map snd) ctr_alists;
   1.137          val ctr_thmss = map (map snd o order_list) ctr_alists;
   1.138  
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 05 08:30:38 2014 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 05 09:30:20 2014 +0200
     2.3 @@ -21,8 +21,10 @@
     2.4       weak_case_cong: thm,
     2.5       split: thm,
     2.6       split_asm: thm,
     2.7 +     disc_defs: thm list,
     2.8       disc_thmss: thm list list,
     2.9       discIs: thm list,
    2.10 +     sel_defs: thm list,
    2.11       sel_thmss: thm list list,
    2.12       disc_excludesss: thm list list list,
    2.13       disc_exhausts: thm list,
    2.14 @@ -90,8 +92,10 @@
    2.15     weak_case_cong: thm,
    2.16     split: thm,
    2.17     split_asm: thm,
    2.18 +   disc_defs: thm list,
    2.19     disc_thmss: thm list list,
    2.20     discIs: thm list,
    2.21 +   sel_defs: thm list,
    2.22     sel_thmss: thm list list,
    2.23     disc_excludesss: thm list list list,
    2.24     disc_exhausts: thm list,
    2.25 @@ -103,9 +107,9 @@
    2.26     case_eq_ifs: thm list};
    2.27  
    2.28  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    2.29 -    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
    2.30 -    disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms,
    2.31 -    case_eq_ifs} =
    2.32 +    case_thms, case_cong, weak_case_cong, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
    2.33 +    sel_thmss, disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits,
    2.34 +    sel_split_asms, case_eq_ifs} =
    2.35    {ctrs = map (Morphism.term phi) ctrs,
    2.36     casex = Morphism.term phi casex,
    2.37     discs = map (Morphism.term phi) discs,
    2.38 @@ -119,8 +123,10 @@
    2.39     weak_case_cong = Morphism.thm phi weak_case_cong,
    2.40     split = Morphism.thm phi split,
    2.41     split_asm = Morphism.thm phi split_asm,
    2.42 +   disc_defs = map (Morphism.thm phi) disc_defs,
    2.43     disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    2.44     discIs = map (Morphism.thm phi) discIs,
    2.45 +   sel_defs = map (Morphism.thm phi) sel_defs,
    2.46     sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
    2.47     disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss,
    2.48     disc_exhausts = map (Morphism.thm phi) disc_exhausts,
    2.49 @@ -692,12 +698,12 @@
    2.50              (thm, asm_thm)
    2.51            end;
    2.52  
    2.53 -        val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms,
    2.54 -             nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms,
    2.55 -             sel_exhaust_thms, all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms,
    2.56 -             sel_split_asm_thms, case_eq_if_thms) =
    2.57 +        val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
    2.58 +             discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
    2.59 +             disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, safe_collapse_thms,
    2.60 +             expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
    2.61            if no_discs_sels then
    2.62 -            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    2.63 +            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    2.64            else
    2.65              let
    2.66                val udiscs = map (rapp u) discs;
    2.67 @@ -908,10 +914,10 @@
    2.68                    |> Thm.close_derivation
    2.69                  end;
    2.70              in
    2.71 -              (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thmss, discI_thms,
    2.72 -               nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, [disc_exhaust_thm],
    2.73 -               [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm],
    2.74 -               [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
    2.75 +              (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
    2.76 +               discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
    2.77 +               [disc_exhaust_thm], [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms,
    2.78 +               [expand_thm], [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
    2.79              end;
    2.80  
    2.81          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    2.82 @@ -956,11 +962,12 @@
    2.83            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
    2.84             nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
    2.85             case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
    2.86 -           split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
    2.87 -           discIs = discI_thms, sel_thmss = sel_thmss, disc_excludesss = disc_exclude_thmsss,
    2.88 -           disc_exhausts = disc_exhaust_thms, sel_exhausts = sel_exhaust_thms,
    2.89 -           collapses = all_collapse_thms, expands = expand_thms, sel_splits = sel_split_thms,
    2.90 -           sel_split_asms = sel_split_asm_thms, case_eq_ifs = case_eq_if_thms};
    2.91 +           split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
    2.92 +           disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss,
    2.93 +           disc_excludesss = disc_exclude_thmsss, disc_exhausts = disc_exhaust_thms,
    2.94 +           sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
    2.95 +           sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
    2.96 +           case_eq_ifs = case_eq_if_thms};
    2.97        in
    2.98          (ctr_sugar,
    2.99           lthy
     3.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 05 08:30:38 2014 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 05 09:30:20 2014 +0200
     3.3 @@ -109,8 +109,10 @@
     3.4     weak_case_cong = weak_case_cong,
     3.5     split = split,
     3.6     split_asm = split_asm,
     3.7 +   disc_defs = [],
     3.8     disc_thmss = [],
     3.9     discIs = [],
    3.10 +   sel_defs = [],
    3.11     sel_thmss = [],
    3.12     disc_excludesss = [],
    3.13     disc_exhausts = [],