Added maps, sets, rels to "simps" thm collection
authorblanchet
Tue Apr 30 13:23:52 2013 +0200 (2013-04-30)
changeset 5183556523caf372f
parent 51834 8deb369ee70b
child 51836 4d6dcd51dd52
Added maps, sets, rels to "simps" thm collection
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 12:26:41 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 13:23:52 2013 +0200
     1.3 @@ -217,7 +217,7 @@
     1.4  val mk_fold_fun_typess = map2 (map2 (curry (op --->)));
     1.5  val mk_rec_fun_typess = mk_fold_fun_typess oo massage_rec_fun_arg_typesss;
     1.6  
     1.7 -fun mk_fold_rec_terms_and_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy =
     1.8 +fun mk_fold_rec_terms_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy =
     1.9    let
    1.10      val y_Tsss = map3 mk_rec_like_fun_arg_typess ns mss ctor_fold_fun_Ts;
    1.11      val g_Tss = mk_fold_fun_typess y_Tsss Css;
    1.12 @@ -236,7 +236,7 @@
    1.13      (((gss, g_Tss, ysss), (hss, h_Tss, zsss)), lthy)
    1.14    end;
    1.15  
    1.16 -fun mk_unfold_corec_terms_and_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy =
    1.17 +fun mk_unfold_corec_terms_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy =
    1.18    let
    1.19      (*avoid "'a itself" arguments in coiterators and corecursors*)
    1.20      fun repair_arity [0] = [1]
    1.21 @@ -378,8 +378,8 @@
    1.22      val (_, ctor_fold_fun_Ts) = mk_fp_rec_like true As Cs ctor_folds0;
    1.23      val (_, ctor_rec_fun_Ts) = mk_fp_rec_like true As Cs ctor_recs0;
    1.24  
    1.25 -    val (((gss, g_Tss, ysss), (hss, h_Tss, zsss)), names_lthy0) =
    1.26 -      mk_fold_rec_terms_and_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
    1.27 +    val (((gss, _, _), (hss, _, _)), names_lthy0) =
    1.28 +      mk_fold_rec_terms_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
    1.29  
    1.30      val ((((ps, ps'), xsss), us'), names_lthy) =
    1.31        names_lthy0
    1.32 @@ -549,7 +549,7 @@
    1.33      val sel_thmsss = map #sel_thmss ctr_wrap_ress;
    1.34  
    1.35      val ((cs, cpss, ((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)), names_lthy0) =
    1.36 -      mk_unfold_corec_terms_and_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy;
    1.37 +      mk_unfold_corec_terms_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy;
    1.38  
    1.39      val (((rs, us'), vs'), names_lthy) =
    1.40        names_lthy0
    1.41 @@ -961,10 +961,10 @@
    1.42            (cs, cpss, unfold_only as ((_, crssss, cgssss), (_, g_Tsss, _)),
    1.43             corec_only as ((_, csssss, chssss), (_, h_Tsss, _)))), _) =
    1.44        if lfp then
    1.45 -        mk_fold_rec_terms_and_types fpTs Css ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
    1.46 +        mk_fold_rec_terms_types fpTs Css ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
    1.47          |>> rpair ([], [], (([], [], []), ([], [], [])), (([], [], []), ([], [], [])))
    1.48        else
    1.49 -        mk_unfold_corec_terms_and_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
    1.50 +        mk_unfold_corec_terms_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
    1.51          |>> pair (([], [], []), ([], [], []));
    1.52  
    1.53      fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
    1.54 @@ -1067,83 +1067,88 @@
    1.55            end;
    1.56  
    1.57          fun derive_maps_sets_rels (ctr_wrap_res, lthy) =
    1.58 -          let
    1.59 -            val rel_flip = rel_flip_of_bnf fp_bnf;
    1.60 -            val nones = replicate live NONE;
    1.61 +          if live = 0 then
    1.62 +            ((([], [], [], []), ctr_wrap_res), lthy)
    1.63 +          else
    1.64 +            let
    1.65 +              val rel_flip = rel_flip_of_bnf fp_bnf;
    1.66 +              val nones = replicate live NONE;
    1.67  
    1.68 -            val ctor_cong =
    1.69 -              if lfp then
    1.70 -                Drule.dummy_thm
    1.71 -              else
    1.72 -                let val ctor' = mk_ctor Bs ctor in
    1.73 -                  cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong
    1.74 -                end;
    1.75 +              val ctor_cong =
    1.76 +                if lfp then
    1.77 +                  Drule.dummy_thm
    1.78 +                else
    1.79 +                  let val ctor' = mk_ctor Bs ctor in
    1.80 +                    cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong
    1.81 +                  end;
    1.82  
    1.83 -            fun mk_cIn ify =
    1.84 -              certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo
    1.85 -              mk_InN_balanced (ify ctr_sum_prod_T) n;
    1.86 -
    1.87 -            val cxIns = map2 (mk_cIn I) tuple_xs ks;
    1.88 -            val cyIns = map2 (mk_cIn B_ify) tuple_ys ks;
    1.89 +              fun mk_cIn ify =
    1.90 +                certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo
    1.91 +                mk_InN_balanced (ify ctr_sum_prod_T) n;
    1.92  
    1.93 -            fun mk_map_thm ctr_def' cxIn =
    1.94 -              fold_thms lthy [ctr_def']
    1.95 -                (unfold_thms lthy (pre_map_def ::
    1.96 -                     (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
    1.97 -                   (cterm_instantiate_pos (nones @ [SOME cxIn])
    1.98 -                      (if lfp then fp_map_thm else fp_map_thm RS ctor_cong)))
    1.99 -              |> singleton (Proof_Context.export names_lthy no_defs_lthy);
   1.100 +              val cxIns = map2 (mk_cIn I) tuple_xs ks;
   1.101 +              val cyIns = map2 (mk_cIn B_ify) tuple_ys ks;
   1.102  
   1.103 -            fun mk_set_thm fp_set_thm ctr_def' cxIn =
   1.104 -              fold_thms lthy [ctr_def']
   1.105 -                (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @
   1.106 -                     (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
   1.107 -                   (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
   1.108 -              |> singleton (Proof_Context.export names_lthy no_defs_lthy);
   1.109 +              fun mk_map_thm ctr_def' cxIn =
   1.110 +                fold_thms lthy [ctr_def']
   1.111 +                  (unfold_thms lthy (pre_map_def ::
   1.112 +                       (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
   1.113 +                     (cterm_instantiate_pos (nones @ [SOME cxIn])
   1.114 +                        (if lfp then fp_map_thm else fp_map_thm RS ctor_cong)))
   1.115 +                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
   1.116  
   1.117 -            fun mk_set_thms fp_set_thm = map2 (mk_set_thm fp_set_thm) ctr_defs' cxIns;
   1.118 +              fun mk_set_thm fp_set_thm ctr_def' cxIn =
   1.119 +                fold_thms lthy [ctr_def']
   1.120 +                  (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @
   1.121 +                       (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
   1.122 +                     (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
   1.123 +                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
   1.124  
   1.125 -            val map_thms = map2 mk_map_thm ctr_defs' cxIns;
   1.126 -            val set_thmss = map mk_set_thms fp_set_thms;
   1.127 +              fun mk_set_thms fp_set_thm = map2 (mk_set_thm fp_set_thm) ctr_defs' cxIns;
   1.128  
   1.129 -            val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
   1.130 +              val map_thms = map2 mk_map_thm ctr_defs' cxIns;
   1.131 +              val set_thmss = map mk_set_thms fp_set_thms;
   1.132 +
   1.133 +              val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
   1.134  
   1.135 -            fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
   1.136 -              fold_thms lthy ctr_defs'
   1.137 -                 (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
   1.138 -                      (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
   1.139 -                    (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
   1.140 -              |> postproc
   1.141 -              |> singleton (Proof_Context.export names_lthy no_defs_lthy);
   1.142 +              fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
   1.143 +                fold_thms lthy ctr_defs'
   1.144 +                   (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
   1.145 +                        (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
   1.146 +                      (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
   1.147 +                |> postproc
   1.148 +                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
   1.149  
   1.150 -            fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
   1.151 -              mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
   1.152 +              fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
   1.153 +                mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
   1.154  
   1.155 -            val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
   1.156 +              val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
   1.157  
   1.158 -            fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
   1.159 -              mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
   1.160 -                cxIn cyIn;
   1.161 +              fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
   1.162 +                mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
   1.163 +                  cxIn cyIn;
   1.164  
   1.165 -            fun mk_other_half_rel_distinct_thm thm =
   1.166 -              flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
   1.167 +              fun mk_other_half_rel_distinct_thm thm =
   1.168 +                flip_rels lthy live thm
   1.169 +                RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
   1.170  
   1.171 -            val half_rel_distinct_thmss =
   1.172 -              map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
   1.173 -            val other_half_rel_distinct_thmss =
   1.174 -              map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss;
   1.175 -            val (rel_distinct_thms, _) =
   1.176 -              join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
   1.177 +              val half_rel_distinct_thmss =
   1.178 +                map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
   1.179 +              val other_half_rel_distinct_thmss =
   1.180 +                map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss;
   1.181 +              val (rel_distinct_thms, _) =
   1.182 +                join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
   1.183  
   1.184 -            val notes =
   1.185 -              [(mapN, map_thms, code_simp_attrs),
   1.186 -               (rel_distinctN, rel_distinct_thms, code_simp_attrs),
   1.187 -               (rel_injectN, rel_inject_thms, code_simp_attrs),
   1.188 -               (setsN, flat set_thmss, code_simp_attrs)]
   1.189 -              |> massage_simple_notes fp_b_name;
   1.190 -          in
   1.191 -            (ctr_wrap_res, lthy |> Local_Theory.notes notes |> snd)
   1.192 -          end;
   1.193 +              val notes =
   1.194 +                [(mapN, map_thms, code_simp_attrs),
   1.195 +                 (rel_distinctN, rel_distinct_thms, code_simp_attrs),
   1.196 +                 (rel_injectN, rel_inject_thms, code_simp_attrs),
   1.197 +                 (setsN, flat set_thmss, code_simp_attrs)]
   1.198 +                |> massage_simple_notes fp_b_name;
   1.199 +            in
   1.200 +              (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_wrap_res),
   1.201 +               lthy |> Local_Theory.notes notes |> snd)
   1.202 +            end;
   1.203  
   1.204          fun define_fold_rec no_defs_lthy =
   1.205            let
   1.206 @@ -1263,25 +1268,29 @@
   1.207              ((unfold, corec, unfold_def, corec_def), lthy')
   1.208            end;
   1.209  
   1.210 -        val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
   1.211 -
   1.212 -        fun massage_res ((ctr_wrap_res, rec_like_res), lthy) =
   1.213 -          (((ctrs, xss, ctr_defs, ctr_wrap_res), rec_like_res), lthy);
   1.214 +        fun massage_res (((maps_sets_rels, ctr_wrap_res), rec_like_res), lthy) =
   1.215 +          (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_wrap_res)), rec_like_res), lthy);
   1.216        in
   1.217 -        (wrap #> (live > 0 ? derive_maps_sets_rels) ##>> define_rec_likes #> massage_res, lthy')
   1.218 +        (wrap
   1.219 +         #> derive_maps_sets_rels
   1.220 +         ##>> (if lfp then define_fold_rec else define_unfold_corec)
   1.221 +         #> massage_res, lthy')
   1.222        end;
   1.223  
   1.224 -    fun wrap_types_and_more (wrap_types_and_mores, lthy) =
   1.225 -      fold_map I wrap_types_and_mores lthy
   1.226 -      |>> apsnd split_list4 o apfst split_list4 o split_list;
   1.227 +    fun wrap_types_etc (wrap_types_etcs, lthy) =
   1.228 +      fold_map I wrap_types_etcs lthy
   1.229 +      |>> apsnd split_list4 o apfst (apsnd split_list4 o apfst split_list4 o split_list)
   1.230 +        o split_list;
   1.231  
   1.232 -    (* TODO: Add map, sets, rel simps *)
   1.233      val mk_simp_thmss =
   1.234 -      map3 (fn {injects, distincts, case_thms, ...} => fn rec_likes => fn fold_likes =>
   1.235 -        injects @ distincts @ case_thms @ rec_likes @ fold_likes);
   1.236 +      map7 (fn {injects, distincts, case_thms, ...} => fn rec_likes => fn fold_likes =>
   1.237 +        fn mapsx => fn rel_injects => fn rel_distincts => fn setss =>
   1.238 +          injects @ distincts @ case_thms @ rec_likes @ fold_likes @ mapsx @ rel_injects
   1.239 +          @ rel_distincts @ flat setss);
   1.240  
   1.241      fun derive_and_note_induct_fold_rec_thms_for_types
   1.242 -        (((ctrss, _, ctr_defss, ctr_wrap_ress), (folds, recs, fold_defs, rec_defs)), lthy) =
   1.243 +        ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_wrap_ress)),
   1.244 +          (folds, recs, fold_defs, rec_defs)), lthy) =
   1.245        let
   1.246          val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
   1.247               (rec_thmss, rec_attrs)) =
   1.248 @@ -1291,7 +1300,8 @@
   1.249  
   1.250          val induct_type_attr = Attrib.internal o K o Induct.induct_type;
   1.251  
   1.252 -        val simp_thmss = mk_simp_thmss ctr_wrap_ress rec_thmss fold_thmss;
   1.253 +        val simp_thmss =
   1.254 +          mk_simp_thmss ctr_wrap_ress rec_thmss fold_thmss mapsx rel_injects rel_distincts setss;
   1.255  
   1.256          val common_notes =
   1.257            (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
   1.258 @@ -1310,7 +1320,8 @@
   1.259        end;
   1.260  
   1.261      fun derive_and_note_coinduct_unfold_corec_thms_for_types
   1.262 -        (((ctrss, _, ctr_defss, ctr_wrap_ress), (unfolds, corecs, unfold_defs, corec_defs)), lthy) =
   1.263 +        ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_wrap_ress)),
   1.264 +          (unfolds, corecs, unfold_defs, corec_defs)), lthy) =
   1.265        let
   1.266          val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms,
   1.267                coinduct_attrs),
   1.268 @@ -1331,7 +1342,8 @@
   1.269          val simp_thmss =
   1.270            mk_simp_thmss ctr_wrap_ress
   1.271              (map3 flat_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
   1.272 -            (map3 flat_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss);
   1.273 +            (map3 flat_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss)
   1.274 +            mapsx rel_injects rel_distincts setss;
   1.275  
   1.276          val anonymous_notes =
   1.277            [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
   1.278 @@ -1371,7 +1383,7 @@
   1.279          pre_set_defss ~~ pre_rel_defs ~~ fp_map_thms ~~ fp_set_thmss ~~ fp_rel_thms ~~ ns ~~ kss ~~
   1.280          mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
   1.281          raw_sel_defaultsss)
   1.282 -      |> wrap_types_and_more
   1.283 +      |> wrap_types_etc
   1.284        |> (if lfp then derive_and_note_induct_fold_rec_thms_for_types
   1.285            else derive_and_note_coinduct_unfold_corec_thms_for_types);
   1.286