handle deep nesting in N2M
authortraytel
Wed Aug 06 16:00:11 2014 +0200 (2014-08-06)
changeset 578029c065009cd8a
parent 57801 4adfa833072b
child 57803 19f54b090cdd
handle deep nesting in N2M
src/HOL/BNF_Def.thy
src/HOL/Tools/BNF/bnf_fp_n2m.ML
     1.1 --- a/src/HOL/BNF_Def.thy	Wed Aug 06 10:20:50 2014 +0200
     1.2 +++ b/src/HOL/BNF_Def.thy	Wed Aug 06 16:00:11 2014 +0200
     1.3 @@ -159,6 +159,11 @@
     1.4  "case_sum f g \<circ> Inr = g"
     1.5  by auto
     1.6  
     1.7 +lemma map_sum_o_inj:
     1.8 +"map_sum f g o Inl = Inl o f"
     1.9 +"map_sum f g o Inr = Inr o g"
    1.10 +by auto
    1.11 +
    1.12  lemma card_order_csum_cone_cexp_def:
    1.13    "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|"
    1.14    unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order)
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Aug 06 10:20:50 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Aug 06 16:00:11 2014 +0200
     2.3 @@ -240,29 +240,26 @@
     2.4      val co_recs = of_fp_res #xtor_co_recs;
     2.5      val ns = map (length o #Ts o #fp_res) fp_sugars;
     2.6  
     2.7 -    fun substT rho (Type (@{type_name fun}, [T, U])) = substT rho T --> substT rho U
     2.8 -      | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
     2.9 -      | substT _ T = T;
    2.10 -
    2.11      val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
    2.12  
    2.13      fun foldT_of_recT recT =
    2.14        let
    2.15 -        val ((FTXs, Xs), TX) = strip_fun_type recT |>> map_split dest_co_algT;
    2.16 +        val ((FTXs, Ys), TX) = strip_fun_type recT |>> map_split dest_co_algT;
    2.17 +        val Zs = union op = Xs Ys;
    2.18          fun subst (Type (C, Ts as [_, X])) =
    2.19 -            if C = co_productC andalso member op = Xs X then X else Type (C, map subst Ts)
    2.20 +            if C = co_productC andalso member op = Zs X then X else Type (C, map subst Ts)
    2.21            | subst (Type (C, Ts)) = Type (C, map subst Ts)
    2.22            | subst T = T;
    2.23        in
    2.24 -        map2 (mk_co_algT o subst) FTXs Xs ---> TX
    2.25 +        map2 (mk_co_algT o subst) FTXs Ys ---> TX
    2.26        end;
    2.27  
    2.28 -    fun force_rec i TU TU_rec raw_rec =
    2.29 +    fun force_rec i TU raw_rec =
    2.30        let
    2.31          val thy = Proof_Context.theory_of lthy;
    2.32  
    2.33          val approx_rec = raw_rec
    2.34 -          |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU_rec);
    2.35 +          |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU);
    2.36          val subst = Term.typ_subst_atomic fold_thetaAs;
    2.37  
    2.38          fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
    2.39 @@ -299,9 +296,7 @@
    2.40          val i = find_index (fn T => x = T) Xs;
    2.41          val TUrec =
    2.42            (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
    2.43 -            NONE =>
    2.44 -              force_rec i TU
    2.45 -                (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs)) (nth co_recs i)
    2.46 +            NONE => force_rec i TU (nth co_recs i)
    2.47            | SOME f => f);
    2.48  
    2.49          val TUs = binder_fun_types (fastype_of TUrec);
    2.50 @@ -340,14 +335,21 @@
    2.51                      let
    2.52                        val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
    2.53                        val T = mk_co_algT TY U;
    2.54 +                      fun mk_co_proj TU = build_map lthy [] (fn TU =>
    2.55 +                        let
    2.56 +                          val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT
    2.57 +                        in
    2.58 +                          if T1 = U then co_proj1_const TU
    2.59 +                          else mk_co_comp (mk_co_proj (co_swap (T1, U)),
    2.60 +                            co_proj1_const (co_swap (mk_co_productT T1 T2, T1)))
    2.61 +                        end) TU;
    2.62                      in
    2.63 -                      (case try (force_typ names_lthy T o build_map lthy [] co_proj1_const o dest_funT) T of
    2.64 -                        SOME f => mk_co_product f
    2.65 -                          (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
    2.66 -                      | NONE => mk_map_co_product
    2.67 -                          (build_map lthy [] co_proj1_const
    2.68 -                            (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
    2.69 -                          (HOLogic.id_const X))
    2.70 +                      if not (can dest_co_productT TY)
    2.71 +                      then mk_co_product (mk_co_proj (dest_funT T))
    2.72 +                        (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
    2.73 +                      else mk_map_co_product
    2.74 +                        (mk_co_proj (co_swap (dest_co_productT TY |> fst, U)))
    2.75 +                        (HOLogic.id_const X)
    2.76                      end)
    2.77                  val smap_args = map mk_smap_arg smap_argTs;
    2.78                in
    2.79 @@ -413,8 +415,8 @@
    2.80            map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
    2.81            @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
    2.82          val rec_thms = fold_thms @ case_fp fp
    2.83 -          @{thms fst_convol map_prod_o_convol convol_o}
    2.84 -          @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
    2.85 +          @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod}
    2.86 +          @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)};
    2.87  
    2.88          val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
    2.89