src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58352 37745650a3f4
parent 58340 5f6f48e87de6
child 58375 7b92932ffea5
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Sep 16 19:23:37 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Sep 16 19:23:37 2014 +0200
     1.3 @@ -331,28 +331,31 @@
     1.4                    |> force_typ names_lthy smapT
     1.5                    |> hidden_to_unit;
     1.6                  val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
     1.7 -                fun mk_smap_arg TU =
     1.8 -                  (if domain_type TU = range_type TU then
     1.9 -                    HOLogic.id_const (domain_type TU)
    1.10 +                fun mk_smap_arg T_to_U =
    1.11 +                  (if domain_type T_to_U = range_type T_to_U then
    1.12 +                    HOLogic.id_const (domain_type T_to_U)
    1.13                    else
    1.14                      let
    1.15 -                      val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
    1.16 +                      val (TY, (U, X)) = T_to_U |> dest_co_algT ||> dest_co_productT;
    1.17                        val T = mk_co_algT TY U;
    1.18 -                      fun mk_co_proj TU = build_map lthy [] (fn TU =>
    1.19 -                        let
    1.20 -                          val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT
    1.21 -                        in
    1.22 -                          if T1 = U then co_proj1_const TU
    1.23 -                          else mk_co_comp (mk_co_proj (co_swap (T1, U)),
    1.24 -                            co_proj1_const (co_swap (mk_co_productT T1 T2, T1)))
    1.25 -                        end) TU;
    1.26 +                      fun mk_co_proj TU =
    1.27 +                        build_map lthy [] (fn TU =>
    1.28 +                          let val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT in
    1.29 +                            if T1 = U then co_proj1_const TU
    1.30 +                            else mk_co_comp (mk_co_proj (co_swap (T1, U)),
    1.31 +                              co_proj1_const (co_swap (mk_co_productT T1 T2, T1)))
    1.32 +                          end)
    1.33 +                          TU;
    1.34 +                      fun default () =
    1.35 +                        mk_co_product (mk_co_proj (dest_funT T))
    1.36 +                          (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))));
    1.37                      in
    1.38 -                      if not (can dest_co_productT TY)
    1.39 -                      then mk_co_product (mk_co_proj (dest_funT T))
    1.40 -                        (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
    1.41 -                      else mk_map_co_product
    1.42 -                        (mk_co_proj (co_swap (dest_co_productT TY |> fst, U)))
    1.43 -                        (HOLogic.id_const X)
    1.44 +                      if can dest_co_productT TY then
    1.45 +                        mk_map_co_product (mk_co_proj (co_swap (dest_co_productT TY |> fst, U)))
    1.46 +                          (HOLogic.id_const X)
    1.47 +                        handle TYPE _ => default () (*N2M involving "prod" type*)
    1.48 +                      else
    1.49 +                        default ()
    1.50                      end)
    1.51                  val smap_args = map mk_smap_arg smap_argTs;
    1.52                in
    1.53 @@ -441,8 +444,9 @@
    1.54          val Rep_o_Abss = maps mk_Rep_o_Abs type_definitions;
    1.55  
    1.56          fun tac {context = ctxt, prems = _} =
    1.57 -          unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs, fp_pre_map_defs,
    1.58 -            fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss, Rep_o_Abss]) THEN
    1.59 +          unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs,
    1.60 +            fp_pre_map_defs, fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss,
    1.61 +            Rep_o_Abss]) THEN
    1.62            CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
    1.63        in
    1.64          Library.foldr1 HOLogic.mk_conj goals