src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 57802 9c065009cd8a
parent 57801 4adfa833072b
child 58162 df15198c6309
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Aug 06 10:20:50 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Aug 06 16:00:11 2014 +0200
     1.3 @@ -240,29 +240,26 @@
     1.4      val co_recs = of_fp_res #xtor_co_recs;
     1.5      val ns = map (length o #Ts o #fp_res) fp_sugars;
     1.6  
     1.7 -    fun substT rho (Type (@{type_name fun}, [T, U])) = substT rho T --> substT rho U
     1.8 -      | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
     1.9 -      | substT _ T = T;
    1.10 -
    1.11      val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
    1.12  
    1.13      fun foldT_of_recT recT =
    1.14        let
    1.15 -        val ((FTXs, Xs), TX) = strip_fun_type recT |>> map_split dest_co_algT;
    1.16 +        val ((FTXs, Ys), TX) = strip_fun_type recT |>> map_split dest_co_algT;
    1.17 +        val Zs = union op = Xs Ys;
    1.18          fun subst (Type (C, Ts as [_, X])) =
    1.19 -            if C = co_productC andalso member op = Xs X then X else Type (C, map subst Ts)
    1.20 +            if C = co_productC andalso member op = Zs X then X else Type (C, map subst Ts)
    1.21            | subst (Type (C, Ts)) = Type (C, map subst Ts)
    1.22            | subst T = T;
    1.23        in
    1.24 -        map2 (mk_co_algT o subst) FTXs Xs ---> TX
    1.25 +        map2 (mk_co_algT o subst) FTXs Ys ---> TX
    1.26        end;
    1.27  
    1.28 -    fun force_rec i TU TU_rec raw_rec =
    1.29 +    fun force_rec i TU raw_rec =
    1.30        let
    1.31          val thy = Proof_Context.theory_of lthy;
    1.32  
    1.33          val approx_rec = raw_rec
    1.34 -          |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU_rec);
    1.35 +          |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU);
    1.36          val subst = Term.typ_subst_atomic fold_thetaAs;
    1.37  
    1.38          fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
    1.39 @@ -299,9 +296,7 @@
    1.40          val i = find_index (fn T => x = T) Xs;
    1.41          val TUrec =
    1.42            (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
    1.43 -            NONE =>
    1.44 -              force_rec i TU
    1.45 -                (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs)) (nth co_recs i)
    1.46 +            NONE => force_rec i TU (nth co_recs i)
    1.47            | SOME f => f);
    1.48  
    1.49          val TUs = binder_fun_types (fastype_of TUrec);
    1.50 @@ -340,14 +335,21 @@
    1.51                      let
    1.52                        val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
    1.53                        val T = mk_co_algT TY U;
    1.54 +                      fun mk_co_proj TU = build_map lthy [] (fn TU =>
    1.55 +                        let
    1.56 +                          val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT
    1.57 +                        in
    1.58 +                          if T1 = U then co_proj1_const TU
    1.59 +                          else mk_co_comp (mk_co_proj (co_swap (T1, U)),
    1.60 +                            co_proj1_const (co_swap (mk_co_productT T1 T2, T1)))
    1.61 +                        end) TU;
    1.62                      in
    1.63 -                      (case try (force_typ names_lthy T o build_map lthy [] co_proj1_const o dest_funT) T of
    1.64 -                        SOME f => mk_co_product f
    1.65 -                          (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
    1.66 -                      | NONE => mk_map_co_product
    1.67 -                          (build_map lthy [] co_proj1_const
    1.68 -                            (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
    1.69 -                          (HOLogic.id_const X))
    1.70 +                      if not (can dest_co_productT TY)
    1.71 +                      then mk_co_product (mk_co_proj (dest_funT T))
    1.72 +                        (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
    1.73 +                      else mk_map_co_product
    1.74 +                        (mk_co_proj (co_swap (dest_co_productT TY |> fst, U)))
    1.75 +                        (HOLogic.id_const X)
    1.76                      end)
    1.77                  val smap_args = map mk_smap_arg smap_argTs;
    1.78                in
    1.79 @@ -413,8 +415,8 @@
    1.80            map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
    1.81            @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
    1.82          val rec_thms = fold_thms @ case_fp fp
    1.83 -          @{thms fst_convol map_prod_o_convol convol_o}
    1.84 -          @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
    1.85 +          @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod}
    1.86 +          @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)};
    1.87  
    1.88          val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
    1.89