src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55803 74d3fe9031d8
parent 55575 a5e33e18fb5c
child 55810 63d63d854fae
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Feb 28 12:04:40 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Feb 25 18:14:26 2014 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val construct_mutualized_fp: BNF_Util.fp_kind -> typ list -> BNF_FP_Def_Sugar.fp_sugar list ->
     1.6      binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
     1.7 -    local_theory -> BNF_FP_Util.fp_result * local_theory
     1.8 +    BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory
     1.9  end;
    1.10  
    1.11  structure BNF_FP_N2M : BNF_FP_N2M =
    1.12 @@ -17,6 +17,7 @@
    1.13  
    1.14  open BNF_Def
    1.15  open BNF_Util
    1.16 +open BNF_Comp
    1.17  open BNF_FP_Util
    1.18  open BNF_FP_Def_Sugar
    1.19  open BNF_Tactics
    1.20 @@ -45,28 +46,16 @@
    1.21      Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
    1.22    end;
    1.23  
    1.24 -fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs lthy =
    1.25 +fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
    1.26 +    absT_infos lthy =
    1.27    let
    1.28 -    fun steal_fp_res get =
    1.29 +    fun of_fp_res get =
    1.30        map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
    1.31  
    1.32 -    val n = length bnfs;
    1.33 -    val deads = fold (union (op =)) Dss resDs;
    1.34 -    val As = subtract (op =) deads (map TFree resBs);
    1.35 -    val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
    1.36 -    val m = length As;
    1.37 -    val live = m + n;
    1.38 -    val ((Xs, Bs), names_lthy) = names_lthy
    1.39 -      |> mk_TFrees n
    1.40 -      ||>> mk_TFrees m;
    1.41 -    val allAs = As @ Xs;
    1.42 -    val phiTs = map2 mk_pred2T As Bs;
    1.43 -    val theta = As ~~ Bs;
    1.44 -    val fpTs' = map (Term.typ_subst_atomic theta) fpTs;
    1.45 -    val pre_phiTs = map2 mk_pred2T fpTs fpTs';
    1.46 -
    1.47      fun mk_co_algT T U = fp_case fp (T --> U) (U --> T);
    1.48      fun co_swap pair = fp_case fp I swap pair;
    1.49 +    val mk_co_comp = HOLogic.mk_comp o co_swap;
    1.50 +
    1.51      val dest_co_algT = co_swap o dest_funT;
    1.52      val co_alg_argT = fp_case fp range_type domain_type;
    1.53      val co_alg_funT = fp_case fp domain_type range_type;
    1.54 @@ -75,30 +64,78 @@
    1.55      val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    1.56      val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
    1.57      val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
    1.58 +    val rewrite_comp_comp = fp_case fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
    1.59 +
    1.60 +    val fp_absT_infos = map #absT_info fp_sugars;
    1.61 +    val fp_bnfs = of_fp_res #bnfs;
    1.62 +    val pre_bnfs = map #pre_bnf fp_sugars;
    1.63 +    val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
    1.64 +    val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
    1.65 +    val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
    1.66 +
    1.67 +    val fp_absTs = map #absT fp_absT_infos;
    1.68 +    val fp_repTs = map #repT fp_absT_infos;
    1.69 +    val fp_abss = map #abs fp_absT_infos;
    1.70 +    val fp_reps = map #rep fp_absT_infos;
    1.71 +    val fp_type_definitions = map #type_definition fp_absT_infos;
    1.72 +
    1.73 +    val absTs = map #absT absT_infos;
    1.74 +    val repTs = map #repT absT_infos;
    1.75 +    val absTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) absTs;
    1.76 +    val repTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) repTs;
    1.77 +    val abss = map #abs absT_infos;
    1.78 +    val reps = map #rep absT_infos;
    1.79 +    val abs_inverses = map #abs_inverse absT_infos;
    1.80 +    val type_definitions = map #type_definition absT_infos;
    1.81 +
    1.82 +    val n = length bnfs;
    1.83 +    val deads = fold (union (op =)) Dss resDs;
    1.84 +    val As = subtract (op =) deads (map TFree resBs);
    1.85 +    val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
    1.86 +    val m = length As;
    1.87 +    val live = m + n;
    1.88 +
    1.89 +    val ((Xs, Bs), names_lthy) = names_lthy
    1.90 +      |> mk_TFrees n
    1.91 +      ||>> mk_TFrees m;
    1.92 +
    1.93 +    val allAs = As @ Xs;
    1.94 +    val allBs = Bs @ Xs;
    1.95 +    val phiTs = map2 mk_pred2T As Bs;
    1.96 +    val thetaBs = As ~~ Bs;
    1.97 +    val fpTs' = map (Term.typ_subst_atomic thetaBs) fpTs;
    1.98 +    val fold_thetaAs = Xs ~~ fpTs;
    1.99 +    val fold_thetaBs = Xs ~~ fpTs';
   1.100 +    val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs;
   1.101 +    val pre_phiTs = map2 mk_pred2T fpTs fpTs';
   1.102  
   1.103      val ((ctors, dtors), (xtor's, xtors)) =
   1.104        let
   1.105 -        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal_fp_res #ctors);
   1.106 -        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal_fp_res #dtors);
   1.107 +        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors);
   1.108 +        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors);
   1.109        in
   1.110 -        ((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
   1.111 +        ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (fp_case fp ctors dtors))
   1.112        end;
   1.113  
   1.114 +    val absATs = map (domain_type o fastype_of) ctors;
   1.115 +    val absBTs = map (Term.typ_subst_atomic thetaBs) absATs;
   1.116      val xTs = map (domain_type o fastype_of) xtors;
   1.117      val yTs = map (domain_type o fastype_of) xtor's;
   1.118  
   1.119 +    fun abs_of allAs Ds bnf = mk_abs (mk_T_of_bnf Ds allAs bnf) o #abs;
   1.120 +    fun rep_of absAT = mk_rep absAT o #rep;
   1.121 +
   1.122 +    val absAs = map3 (abs_of allAs) Dss bnfs absT_infos;
   1.123 +    val absBs = map3 (abs_of allBs) Dss bnfs absT_infos;
   1.124 +    val fp_repAs = map2 rep_of absATs fp_absT_infos;
   1.125 +    val fp_repBs = map2 rep_of absBTs fp_absT_infos;
   1.126 +
   1.127      val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
   1.128        |> mk_Frees' "R" phiTs
   1.129        ||>> mk_Frees "S" pre_phiTs
   1.130        ||>> mk_Frees "x" xTs
   1.131        ||>> mk_Frees "y" yTs;
   1.132  
   1.133 -    val fp_bnfs = steal_fp_res #bnfs;
   1.134 -    val pre_bnfs = map #pre_bnf fp_sugars;
   1.135 -    val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
   1.136 -    val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
   1.137 -    val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
   1.138 -
   1.139      val rels =
   1.140        let
   1.141          fun find_rel T As Bs = fp_nesty_bnfss
   1.142 @@ -127,15 +164,28 @@
   1.143      val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
   1.144  
   1.145      val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
   1.146 -    val rel_xtor_co_inducts = steal_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
   1.147 +    val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
   1.148        |> map (unfold_thms lthy (id_apply :: rel_unfolds));
   1.149  
   1.150      val rel_defs = map rel_def_of_bnf bnfs;
   1.151      val rel_monos = map rel_mono_of_bnf bnfs;
   1.152  
   1.153 +    fun cast castA castB pre_rel =
   1.154 +      let
   1.155 +        val castAB = mk_vimage2p (Term.subst_atomic_types fold_thetaAs castA)
   1.156 +          (Term.subst_atomic_types fold_thetaBs castB);
   1.157 +      in
   1.158 +        fold_rev (fold_rev Term.absdummy) [phiTs, pre_phiTs]
   1.159 +          (castAB $ Term.list_comb (pre_rel, map Bound (live - 1 downto 0)))
   1.160 +      end;
   1.161 +
   1.162 +    val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs;
   1.163 +    val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs;
   1.164 +
   1.165      val rel_xtor_co_induct_thm =
   1.166 -      mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's
   1.167 -        (mk_rel_xtor_co_induct_tactic fp rel_xtor_co_inducts rel_defs rel_monos) lthy;
   1.168 +      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys xtors
   1.169 +        xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos)
   1.170 +        lthy;
   1.171  
   1.172      val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
   1.173      val map_id0s = no_refl (map map_id0_of_bnf bnfs);
   1.174 @@ -150,16 +200,22 @@
   1.175                let val T = domain_type (fastype_of P);
   1.176                in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
   1.177              val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
   1.178 +            fun mk_fp_type_copy_thms thm = map (curry op RS thm)
   1.179 +              @{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
   1.180 +            fun mk_type_copy_thms thm = map (curry op RS thm)
   1.181 +              @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
   1.182            in
   1.183              cterm_instantiate_pos cts rel_xtor_co_induct_thm
   1.184              |> singleton (Proof_Context.export names_lthy lthy)
   1.185              |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
   1.186              |> funpow n (fn thm => thm RS spec)
   1.187              |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
   1.188 -            |> unfold_thms lthy @{thms Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)}
   1.189 +            |> unfold_thms lthy (@{thms vimage2p_comp comp_apply comp_id
   1.190 +               Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
   1.191 +               maps mk_fp_type_copy_thms fp_type_definitions @
   1.192 +               maps mk_type_copy_thms type_definitions)
   1.193              |> unfold_thms lthy @{thms subset_iff mem_Collect_eq
   1.194                 atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
   1.195 -            |> unfold_thms lthy (maps set_defs_of_bnf bnfs)
   1.196            end
   1.197        | Greatest_FP =>
   1.198            let
   1.199 @@ -173,8 +229,6 @@
   1.200            end);
   1.201  
   1.202      val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
   1.203 -    val fold_pre_deads_only_Ts = map2 (fn Ds => mk_T_of_bnf Ds (replicate live dummyT)) Dss bnfs;
   1.204 -    val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs;
   1.205      val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
   1.206  
   1.207      val fold_strTs = map2 mk_co_algT fold_preTs Xs;
   1.208 @@ -185,32 +239,52 @@
   1.209        |> mk_Frees' "s" fold_strTs
   1.210        ||>> mk_Frees' "s" rec_strTs;
   1.211  
   1.212 -    val co_iters = steal_fp_res #xtor_co_iterss;
   1.213 +    val co_iters = of_fp_res #xtor_co_iterss;
   1.214      val ns = map (length o #Ts o #fp_res) fp_sugars;
   1.215  
   1.216      fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
   1.217        | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
   1.218        | substT _ T = T;
   1.219  
   1.220 +    val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
   1.221 +
   1.222      fun force_iter is_rec i TU TU_rec raw_iters =
   1.223        let
   1.224 +        val thy = Proof_Context.theory_of lthy;
   1.225 +
   1.226          val approx_fold = un_fold_of raw_iters
   1.227            |> force_typ names_lthy
   1.228              (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
   1.229 -        val subst = Term.typ_subst_atomic (Xs ~~ fpTs);
   1.230 +        val subst = Term.typ_subst_atomic fold_thetaAs;
   1.231 +
   1.232 +        fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
   1.233 +        val mk_fp_absT_repTs = map5 mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
   1.234 +
   1.235 +        val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
   1.236 +
   1.237 +        val fold_pre_deads_only_Ts =
   1.238 +          map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ fpTs))) fold_preTs';
   1.239 +
   1.240          val TUs = map_split dest_co_algT (binder_fun_types (fastype_of approx_fold))
   1.241            |>> map subst
   1.242            |> uncurry (map2 mk_co_algT);
   1.243 -        val js = find_indices Type.could_unify TUs
   1.244 -          (map2 (fn T => fn U => mk_co_algT (subst T) U) fold_preTs Xs);
   1.245 +        val cands = map2 mk_co_algT fold_preTs' Xs;
   1.246 +
   1.247 +        val js = find_indices Type.could_unify TUs cands;
   1.248          val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
   1.249          val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
   1.250        in
   1.251          force_typ names_lthy (Tpats ---> TU) iter
   1.252        end;
   1.253  
   1.254 +    fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
   1.255 +      fp_case fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
   1.256 +        (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t)));
   1.257 +
   1.258      fun mk_iter b_opt is_rec iters lthy TU =
   1.259        let
   1.260 +        val thy = Proof_Context.theory_of lthy;
   1.261 +
   1.262          val x = co_alg_argT TU;
   1.263          val i = find_index (fn T => x = T) Xs;
   1.264          val TUiter =
   1.265 @@ -220,20 +294,32 @@
   1.266                  (TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
   1.267                  (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
   1.268            | SOME f => f);
   1.269 +
   1.270          val TUs = binder_fun_types (fastype_of TUiter);
   1.271          val iter_preTs = if is_rec then rec_preTs else fold_preTs;
   1.272          val iter_strs = if is_rec then rec_strs else fold_strs;
   1.273 +
   1.274          fun mk_s TU' =
   1.275            let
   1.276 +            fun mk_absT_fp_repT repT absT = mk_absT thy repT absT ooo mk_repT;
   1.277 +
   1.278              val i = find_index (fn T => co_alg_argT TU' = T) Xs;
   1.279 +            val fp_abs = nth fp_abss i;
   1.280 +            val fp_rep = nth fp_reps i;
   1.281 +            val abs = nth abss i;
   1.282 +            val rep = nth reps i;
   1.283              val sF = co_alg_funT TU';
   1.284 +            val sF' =
   1.285 +              mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF
   1.286 +                handle Term.TYPE _ => sF;
   1.287              val F = nth iter_preTs i;
   1.288              val s = nth iter_strs i;
   1.289            in
   1.290 -            (if sF = F then s
   1.291 +            if sF = F then s
   1.292 +            else if sF' = F then mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s
   1.293              else
   1.294                let
   1.295 -                val smapT = replicate live dummyT ---> mk_co_algT sF F;
   1.296 +                val smapT = replicate live dummyT ---> mk_co_algT sF' F;
   1.297                  fun hidden_to_unit t =
   1.298                    Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
   1.299                  val smap = map_of_bnf (nth bnfs i)
   1.300 @@ -260,8 +346,9 @@
   1.301                      fst (fst (mk_iter NONE is_rec iters lthy TU)))
   1.302                  val smap_args = map mk_smap_arg smap_argTs;
   1.303                in
   1.304 -                HOLogic.mk_comp (co_swap (s, Term.list_comb (smap, smap_args)))
   1.305 -              end)
   1.306 +                mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep
   1.307 +                  (mk_co_comp (s, Term.list_comb (smap, smap_args)))
   1.308 +              end
   1.309            end;
   1.310          val t = Term.list_comb (TUiter, map mk_s TUs);
   1.311        in
   1.312 @@ -306,13 +393,19 @@
   1.313                map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs))
   1.314            Dss bnfs;
   1.315  
   1.316 -        fun mk_goals f xtor s smap =
   1.317 -          ((f, xtor), (s, smap))
   1.318 -          |> pairself (HOLogic.mk_comp o co_swap)
   1.319 -          |> HOLogic.mk_eq;
   1.320 +        fun mk_goals f xtor s smap fp_abs fp_rep abs rep =
   1.321 +          let
   1.322 +            val lhs = mk_co_comp (f, xtor);
   1.323 +            val rhs = mk_co_comp (s, smap);
   1.324 +          in
   1.325 +            HOLogic.mk_eq (lhs,
   1.326 +              mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs))
   1.327 +                fp_abs fp_rep abs rep rhs)
   1.328 +          end;
   1.329  
   1.330 -        val fold_goals = map4 mk_goals folds xtors fold_strs pre_fold_maps
   1.331 -        val rec_goals = map4 mk_goals recs xtors rec_strs pre_rec_maps;
   1.332 +        val fold_goals =
   1.333 +          map8 mk_goals folds xtors fold_strs pre_fold_maps fp_abss fp_reps abss reps;
   1.334 +        val rec_goals = map8 mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
   1.335  
   1.336          fun mk_thms ss goals tac =
   1.337            Library.foldr1 HOLogic.mk_conj goals
   1.338 @@ -327,27 +420,42 @@
   1.339          val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
   1.340          val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
   1.341  
   1.342 -        val map_unfolds = maps (fn bnf => no_refl [map_def_of_bnf bnf]) pre_bnfs;
   1.343 -        val unfold_map = map (unfold_thms lthy (id_apply :: map_unfolds));
   1.344 +        val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
   1.345 +
   1.346 +        val fp_xtor_co_iterss = of_fp_res #xtor_co_iter_thmss;
   1.347 +        val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss;
   1.348 +        val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss;
   1.349  
   1.350 -        val fp_xtor_co_iterss = steal_fp_res #xtor_co_iter_thmss;
   1.351 -        val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
   1.352 -        val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
   1.353 -
   1.354 -        val fp_co_iter_o_mapss = steal_fp_res #xtor_co_iter_o_map_thmss;
   1.355 -        val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
   1.356 -        val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
   1.357 -        val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
   1.358 -          o_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
   1.359 +        val fp_co_iter_o_mapss = of_fp_res #xtor_co_iter_o_map_thmss;
   1.360 +        val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss;
   1.361 +        val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss;
   1.362 +        val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
   1.363 +          map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp sum_map.comp} @
   1.364 +          @{thms id_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
   1.365          val rec_thms = fold_thms @ fp_case fp
   1.366            @{thms fst_convol map_pair_o_convol convol_o}
   1.367            @{thms case_sum_o_inj(1) case_sum_o_sum_map o_case_sum};
   1.368 +
   1.369 +        val eq_thm_prop_untyped = op Term.aconv_untyped o pairself Thm.full_prop_of;
   1.370 +
   1.371          val map_thms = no_refl (maps (fn bnf =>
   1.372 -          [map_comp0_of_bnf bnf RS sym, map_id0_of_bnf bnf]) fp_nesty_bnfs);
   1.373 +           let val map_comp0 = map_comp0_of_bnf bnf RS sym
   1.374 +           in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @
   1.375 +          remove eq_thm_prop_untyped (fp_case fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
   1.376 +          (map2 (fn thm => fn bnf =>
   1.377 +            @{thm type_copy_map_comp0_undo} OF
   1.378 +              (replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS
   1.379 +              rewrite_comp_comp)
   1.380 +          type_definitions bnfs);
   1.381 +
   1.382 +        fun mk_Rep_o_Abs thm = thm RS @{thm type_copy_Rep_o_Abs} RS rewrite_comp_comp;
   1.383 +
   1.384 +        val fp_Rep_o_Abss = map mk_Rep_o_Abs fp_type_definitions;
   1.385 +        val Rep_o_Abss = map mk_Rep_o_Abs type_definitions;
   1.386  
   1.387          fun mk_tac defs o_map_thms xtor_thms thms {context = ctxt, prems = _} =
   1.388 -          unfold_thms_tac ctxt
   1.389 -            (flat [thms, defs, pre_map_defs, fp_pre_map_defs, xtor_thms, o_map_thms, map_thms]) THEN
   1.390 +          unfold_thms_tac ctxt (flat [thms, defs, pre_map_defs, fp_pre_map_defs,
   1.391 +            xtor_thms, o_map_thms, map_thms, fp_Rep_o_Abss, Rep_o_Abss]) THEN
   1.392            CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
   1.393  
   1.394          val fold_tac = mk_tac raw_un_fold_defs fp_fold_o_maps fp_xtor_un_folds fold_thms;
   1.395 @@ -360,20 +468,20 @@
   1.396         used by "primrec", "primcorecursive", and "datatype_compat". *)
   1.397      val fp_res =
   1.398        ({Ts = fpTs,
   1.399 -        bnfs = steal_fp_res #bnfs,
   1.400 +        bnfs = of_fp_res #bnfs,
   1.401          dtors = dtors,
   1.402          ctors = ctors,
   1.403          xtor_co_iterss = transpose [un_folds, co_recs],
   1.404          xtor_co_induct = xtor_co_induct_thm,
   1.405 -        dtor_ctors = steal_fp_res #dtor_ctors (*too general types*),
   1.406 -        ctor_dtors = steal_fp_res #ctor_dtors (*too general types*),
   1.407 -        ctor_injects = steal_fp_res #ctor_injects (*too general types*),
   1.408 -        dtor_injects = steal_fp_res #dtor_injects (*too general types*),
   1.409 -        xtor_map_thms = steal_fp_res #xtor_map_thms (*too general types and terms*),
   1.410 -        xtor_set_thmss = steal_fp_res #xtor_set_thmss (*too general types and terms*),
   1.411 -        xtor_rel_thms = steal_fp_res #xtor_rel_thms (*too general types and terms*),
   1.412 +        dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
   1.413 +        ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
   1.414 +        ctor_injects = of_fp_res #ctor_injects (*too general types*),
   1.415 +        dtor_injects = of_fp_res #dtor_injects (*too general types*),
   1.416 +        xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
   1.417 +        xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
   1.418 +        xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
   1.419          xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
   1.420 -        xtor_co_iter_o_map_thmss = steal_fp_res #xtor_co_iter_o_map_thmss
   1.421 +        xtor_co_iter_o_map_thmss = of_fp_res #xtor_co_iter_o_map_thmss
   1.422            (*theorem about old constant*),
   1.423          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
   1.424         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));