src/HOL/Tools/BNF/bnf_fp_n2m.ML
author blanchet
Wed Feb 12 08:35:56 2014 +0100 (2014-02-12)
changeset 55394 d5ebe055b599
parent 55067 a452de24a877
child 55414 eab03e9cee8a
permissions -rw-r--r--
more liberal merging of BNFs and constructor sugar
* * *
make sure that the cache doesn't produce 'DUP's
blanchet@55061
     1
(*  Title:      HOL/Tools/BNF/bnf_fp_n2m.ML
blanchet@53303
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@53303
     3
    Copyright   2013
blanchet@53303
     4
blanchet@53303
     5
Flattening of nested to mutual (co)recursion.
blanchet@53303
     6
*)
blanchet@53303
     7
blanchet@53303
     8
signature BNF_FP_N2M =
blanchet@53303
     9
sig
blanchet@53303
    10
  val construct_mutualized_fp: BNF_FP_Util.fp_kind  -> typ list -> BNF_FP_Def_Sugar.fp_sugar list ->
blanchet@53303
    11
    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
blanchet@53303
    12
    local_theory -> BNF_FP_Util.fp_result * local_theory
blanchet@53303
    13
end;
blanchet@53303
    14
blanchet@53303
    15
structure BNF_FP_N2M : BNF_FP_N2M =
blanchet@53303
    16
struct
blanchet@53303
    17
blanchet@53303
    18
open BNF_Def
blanchet@53303
    19
open BNF_Util
blanchet@53303
    20
open BNF_FP_Util
blanchet@53303
    21
open BNF_FP_Def_Sugar
blanchet@53303
    22
open BNF_Tactics
blanchet@53303
    23
open BNF_FP_N2M_Tactics
blanchet@53303
    24
blanchet@53303
    25
fun force_typ ctxt T =
blanchet@54233
    26
  map_types Type_Infer.paramify_vars
blanchet@53303
    27
  #> Type.constraint T
blanchet@53303
    28
  #> Syntax.check_term ctxt
blanchet@53303
    29
  #> singleton (Variable.polymorphic ctxt);
blanchet@53303
    30
blanchet@53303
    31
fun mk_prod_map f g =
blanchet@53303
    32
  let
blanchet@53303
    33
    val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
blanchet@53303
    34
    val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
blanchet@53303
    35
  in
blanchet@53303
    36
    Const (@{const_name map_pair},
blanchet@53303
    37
      fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
blanchet@53303
    38
  end;
blanchet@53303
    39
blanchet@53303
    40
fun mk_sum_map f g =
blanchet@53303
    41
  let
blanchet@53303
    42
    val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
blanchet@53303
    43
    val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
blanchet@53303
    44
  in
blanchet@53303
    45
    Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
blanchet@53303
    46
  end;
blanchet@53303
    47
blanchet@53303
    48
fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
blanchet@53303
    49
  let
blanchet@53303
    50
    fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars;
blanchet@53303
    51
blanchet@53303
    52
    val n = length bnfs;
blanchet@53303
    53
    val deads = fold (union (op =)) Dss resDs;
blanchet@53303
    54
    val As = subtract (op =) deads (map TFree resBs);
blanchet@53303
    55
    val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
blanchet@53303
    56
    val m = length As;
blanchet@53303
    57
    val live = m + n;
blanchet@53303
    58
    val ((Xs, Bs), names_lthy) = names_lthy
blanchet@53303
    59
      |> mk_TFrees n
blanchet@53303
    60
      ||>> mk_TFrees m;
blanchet@53303
    61
    val allAs = As @ Xs;
blanchet@53303
    62
    val phiTs = map2 mk_pred2T As Bs;
blanchet@53303
    63
    val theta = As ~~ Bs;
blanchet@53303
    64
    val fpTs' = map (Term.typ_subst_atomic theta) fpTs;
blanchet@53303
    65
    val pre_phiTs = map2 mk_pred2T fpTs fpTs';
blanchet@53303
    66
blanchet@53303
    67
    fun mk_co_algT T U = fp_case fp (T --> U) (U --> T);
blanchet@53303
    68
    fun co_swap pair = fp_case fp I swap pair;
blanchet@53303
    69
    val dest_co_algT = co_swap o dest_funT;
blanchet@53303
    70
    val co_alg_argT = fp_case fp range_type domain_type;
blanchet@53303
    71
    val co_alg_funT = fp_case fp domain_type range_type;
blanchet@53303
    72
    val mk_co_product = curry (fp_case fp mk_convol mk_sum_case);
blanchet@53303
    73
    val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map;
blanchet@53303
    74
    val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
blanchet@53303
    75
    val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
blanchet@53303
    76
    val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
blanchet@53303
    77
blanchet@53303
    78
    val ((ctors, dtors), (xtor's, xtors)) =
blanchet@53303
    79
      let
blanchet@53303
    80
        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors);
blanchet@53303
    81
        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors);
blanchet@53303
    82
      in
blanchet@53303
    83
        ((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
blanchet@53303
    84
      end;
blanchet@53303
    85
blanchet@53303
    86
    val xTs = map (domain_type o fastype_of) xtors;
blanchet@53303
    87
    val yTs = map (domain_type o fastype_of) xtor's;
blanchet@53303
    88
blanchet@53303
    89
    val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
blanchet@53303
    90
      |> mk_Frees' "R" phiTs
blanchet@53303
    91
      ||>> mk_Frees "S" pre_phiTs
blanchet@53303
    92
      ||>> mk_Frees "x" xTs
blanchet@53303
    93
      ||>> mk_Frees "y" yTs;
blanchet@53303
    94
blanchet@53303
    95
    val fp_bnfs = steal #bnfs;
blanchet@53303
    96
    val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars;
blanchet@53303
    97
    val pre_bnfss = map #pre_bnfs fp_sugars;
blanchet@53303
    98
    val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
blanchet@53303
    99
    val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
blanchet@55394
   100
    val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
blanchet@53303
   101
blanchet@53303
   102
    val rels =
blanchet@53303
   103
      let
blanchet@53303
   104
        fun find_rel T As Bs = fp_nesty_bnfss
blanchet@55394
   105
          |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
blanchet@53303
   106
          |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
blanchet@53303
   107
          |> Option.map (fn bnf =>
blanchet@53303
   108
            let val live = live_of_bnf bnf;
blanchet@53303
   109
            in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
blanchet@53303
   110
          |> the_default (HOLogic.eq_const T, 0);
blanchet@53303
   111
blanchet@53303
   112
        fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) =
blanchet@53303
   113
              let
blanchet@53303
   114
                val (rel, live) = find_rel T Ts Us;
blanchet@53303
   115
                val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T;
blanchet@53303
   116
                val rels = map2 mk_rel Ts' Us';
blanchet@53303
   117
              in
blanchet@53303
   118
                Term.list_comb (rel, rels)
blanchet@53303
   119
              end
traytel@54244
   120
          | mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As)
traytel@54244
   121
              handle General.Subscript => HOLogic.eq_const T)
blanchet@53303
   122
          | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
blanchet@53303
   123
      in
traytel@54298
   124
        map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs'
blanchet@53303
   125
      end;
blanchet@53303
   126
blanchet@53303
   127
    val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
blanchet@53303
   128
blanchet@53303
   129
    val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;
blanchet@53303
   130
    val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm)
blanchet@53303
   131
      |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss;
blanchet@53303
   132
blanchet@53303
   133
    val rel_defs = map rel_def_of_bnf bnfs;
blanchet@53303
   134
    val rel_monos = map rel_mono_of_bnf bnfs;
blanchet@53303
   135
blanchet@53303
   136
    val rel_xtor_co_induct_thm =
blanchet@53303
   137
      mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's
blanchet@53303
   138
        (mk_rel_xtor_co_induct_tactic fp rel_xtor_co_inducts rel_defs rel_monos) lthy;
blanchet@53303
   139
blanchet@53303
   140
    val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
blanchet@53303
   141
    val map_id0s = no_refl (map map_id0_of_bnf bnfs);
blanchet@53303
   142
blanchet@53303
   143
    val xtor_co_induct_thm =
blanchet@53303
   144
      (case fp of
blanchet@53303
   145
        Least_FP =>
blanchet@53303
   146
          let
blanchet@53303
   147
            val (Ps, names_lthy) = names_lthy
blanchet@53303
   148
              |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
blanchet@53303
   149
            fun mk_Grp_id P =
blanchet@53303
   150
              let val T = domain_type (fastype_of P);
blanchet@53303
   151
              in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
blanchet@53303
   152
            val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
blanchet@53303
   153
          in
blanchet@53303
   154
            cterm_instantiate_pos cts rel_xtor_co_induct_thm
blanchet@53303
   155
            |> singleton (Proof_Context.export names_lthy lthy)
blanchet@53303
   156
            |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
blanchet@53303
   157
            |> funpow n (fn thm => thm RS spec)
blanchet@53303
   158
            |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
blanchet@53303
   159
            |> unfold_thms lthy @{thms Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)}
blanchet@53303
   160
            |> unfold_thms lthy @{thms subset_iff mem_Collect_eq
blanchet@53303
   161
               atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
blanchet@53303
   162
            |> unfold_thms lthy (maps set_defs_of_bnf bnfs)
blanchet@53303
   163
          end
blanchet@53303
   164
      | Greatest_FP =>
blanchet@53303
   165
          let
blanchet@53303
   166
            val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
blanchet@53303
   167
          in
blanchet@53303
   168
            cterm_instantiate_pos cts rel_xtor_co_induct_thm
blanchet@53303
   169
            |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
blanchet@53303
   170
            |> funpow (2 * n) (fn thm => thm RS spec)
wenzelm@54742
   171
            |> Conv.fconv_rule (Object_Logic.atomize lthy)
blanchet@53303
   172
            |> funpow n (fn thm => thm RS mp)
blanchet@53303
   173
          end);
blanchet@53303
   174
blanchet@53303
   175
    val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
blanchet@53303
   176
    val fold_pre_deads_only_Ts = map2 (fn Ds => mk_T_of_bnf Ds (replicate live dummyT)) Dss bnfs;
blanchet@53303
   177
    val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs;
blanchet@53303
   178
    val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
blanchet@53303
   179
blanchet@53303
   180
    val fold_strTs = map2 mk_co_algT fold_preTs Xs;
blanchet@53303
   181
    val rec_strTs = map2 mk_co_algT rec_preTs Xs;
blanchet@53303
   182
    val resTs = map2 mk_co_algT fpTs Xs;
blanchet@53303
   183
blanchet@53303
   184
    val (((fold_strs, fold_strs'), (rec_strs, rec_strs')), names_lthy) = names_lthy
blanchet@53303
   185
      |> mk_Frees' "s" fold_strTs
blanchet@53303
   186
      ||>> mk_Frees' "s" rec_strTs;
blanchet@53303
   187
blanchet@53303
   188
    val co_iters = steal #xtor_co_iterss;
blanchet@53303
   189
    val ns = map (length o #pre_bnfs) fp_sugars;
blanchet@53303
   190
    fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
blanchet@53303
   191
      | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
blanchet@53303
   192
      | substT _ T = T;
blanchet@53303
   193
    fun force_iter is_rec i TU TU_rec raw_iters =
blanchet@53303
   194
      let
blanchet@53303
   195
        val approx_fold = un_fold_of raw_iters
blanchet@53303
   196
          |> force_typ names_lthy
blanchet@53303
   197
            (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
blanchet@53303
   198
        val TUs = binder_fun_types (Term.typ_subst_atomic (Xs ~~ fpTs) (fastype_of approx_fold));
blanchet@53303
   199
        val js = find_indices Type.could_unify
blanchet@53303
   200
          TUs (map (Term.typ_subst_atomic (Xs ~~ fpTs)) fold_strTs);
blanchet@53303
   201
        val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
blanchet@53303
   202
        val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
blanchet@53303
   203
      in
blanchet@53303
   204
        force_typ names_lthy (Tpats ---> TU) iter
blanchet@53303
   205
      end;
blanchet@53303
   206
blanchet@53303
   207
    fun mk_iter b_opt is_rec iters lthy TU =
blanchet@53303
   208
      let
blanchet@53303
   209
        val x = co_alg_argT TU;
blanchet@53303
   210
        val i = find_index (fn T => x = T) Xs;
blanchet@53303
   211
        val TUiter =
blanchet@53303
   212
          (case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
blanchet@53303
   213
            NONE => nth co_iters i
blanchet@53303
   214
              |> force_iter is_rec i
blanchet@53303
   215
                (TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
blanchet@53303
   216
                (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
blanchet@53303
   217
          | SOME f => f);
blanchet@53303
   218
        val TUs = binder_fun_types (fastype_of TUiter);
blanchet@53303
   219
        val iter_preTs = if is_rec then rec_preTs else fold_preTs;
blanchet@53303
   220
        val iter_strs = if is_rec then rec_strs else fold_strs;
blanchet@53303
   221
        fun mk_s TU' =
blanchet@53303
   222
          let
blanchet@53303
   223
            val i = find_index (fn T => co_alg_argT TU' = T) Xs;
blanchet@54233
   224
            val sF = co_alg_funT TU';
blanchet@53303
   225
            val F = nth iter_preTs i;
blanchet@53303
   226
            val s = nth iter_strs i;
blanchet@53303
   227
          in
blanchet@53303
   228
            (if sF = F then s
blanchet@53303
   229
            else
blanchet@53303
   230
              let
blanchet@53303
   231
                val smapT = replicate live dummyT ---> mk_co_algT sF F;
blanchet@53303
   232
                fun hidden_to_unit t =
blanchet@53303
   233
                  Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
blanchet@53303
   234
                val smap = map_of_bnf (nth bnfs i)
blanchet@53303
   235
                  |> force_typ names_lthy smapT
blanchet@53303
   236
                  |> hidden_to_unit;
blanchet@53303
   237
                val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
blanchet@54233
   238
                fun mk_smap_arg TU =
blanchet@53303
   239
                  (if domain_type TU = range_type TU then
blanchet@53303
   240
                    HOLogic.id_const (domain_type TU)
blanchet@53303
   241
                  else if is_rec then
blanchet@53303
   242
                    let
blanchet@53303
   243
                      val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
blanchet@53303
   244
                      val T = mk_co_algT TY U;
blanchet@53303
   245
                    in
blanchet@53303
   246
                      (case try (force_typ lthy T o build_map lthy co_proj1_const o dest_funT) T of
blanchet@53303
   247
                        SOME f => mk_co_product f
blanchet@53303
   248
                          (fst (fst (mk_iter NONE is_rec iters lthy (mk_co_algT TY X))))
blanchet@53303
   249
                      | NONE => mk_map_co_product
blanchet@53303
   250
                          (build_map lthy co_proj1_const
blanchet@53303
   251
                            (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
blanchet@53303
   252
                          (HOLogic.id_const X))
blanchet@53303
   253
                    end
blanchet@53303
   254
                  else
blanchet@53303
   255
                    fst (fst (mk_iter NONE is_rec iters lthy TU)))
blanchet@53303
   256
                val smap_args = map mk_smap_arg smap_argTs;
blanchet@53303
   257
              in
blanchet@53303
   258
                HOLogic.mk_comp (co_swap (s, Term.list_comb (smap, smap_args)))
blanchet@53303
   259
              end)
blanchet@53303
   260
          end;
blanchet@53303
   261
        val t = Term.list_comb (TUiter, map mk_s TUs);
blanchet@53303
   262
      in
blanchet@53303
   263
        (case b_opt of
blanchet@53303
   264
          NONE => ((t, Drule.dummy_thm), lthy)
blanchet@54233
   265
        | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.conceal (Thm.def_binding b), []),
blanchet@53303
   266
            fold_rev Term.absfree (if is_rec then rec_strs' else fold_strs') t)) lthy |>> apsnd snd)
blanchet@53303
   267
      end;
blanchet@53303
   268
blanchet@53303
   269
    fun mk_iters is_rec name lthy =
blanchet@53303
   270
      fold2 (fn TU => fn b => fn ((iters, defs), lthy) =>
blanchet@53303
   271
        mk_iter (SOME b) is_rec iters lthy TU |>> (fn (f, d) => (f :: iters, d :: defs)))
blanchet@53303
   272
      resTs (map (Binding.suffix_name ("_" ^ name)) bs) (([], []), lthy)
blanchet@53303
   273
      |>> apfst rev o apsnd rev;
blanchet@53303
   274
    val foldN = fp_case fp ctor_foldN dtor_unfoldN;
blanchet@53303
   275
    val recN = fp_case fp ctor_recN dtor_corecN;
traytel@53331
   276
    val (((raw_un_folds, raw_un_fold_defs), (raw_co_recs, raw_co_rec_defs)), (lthy, raw_lthy)) =
blanchet@53303
   277
      lthy
blanchet@53303
   278
      |> mk_iters false foldN
blanchet@53303
   279
      ||>> mk_iters true recN
traytel@53331
   280
      ||> `Local_Theory.restore;
blanchet@53303
   281
traytel@53331
   282
    val phi = Proof_Context.export_morphism raw_lthy lthy;
blanchet@53303
   283
blanchet@53303
   284
    val un_folds = map (Morphism.term phi) raw_un_folds;
blanchet@53303
   285
    val co_recs = map (Morphism.term phi) raw_co_recs;
blanchet@53303
   286
blanchet@53303
   287
    val (xtor_un_fold_thms, xtor_co_rec_thms) =
blanchet@53303
   288
      let
blanchet@53303
   289
        val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
blanchet@53303
   290
        val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_co_recs;
blanchet@53303
   291
        val fold_mapTs = co_swap (As @ fpTs, As @ Xs);
blanchet@53303
   292
        val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs);
blanchet@53303
   293
        val pre_fold_maps =
blanchet@53303
   294
          map2 (fn Ds => fn bnf =>
blanchet@53303
   295
            Term.list_comb (uncurry (mk_map_of_bnf Ds) fold_mapTs bnf,
blanchet@53303
   296
              map HOLogic.id_const As @ folds))
blanchet@53303
   297
          Dss bnfs;
blanchet@53303
   298
        val pre_rec_maps =
blanchet@53303
   299
          map2 (fn Ds => fn bnf =>
blanchet@53303
   300
            Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf,
blanchet@53303
   301
              map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs))
blanchet@53303
   302
          Dss bnfs;
blanchet@53303
   303
blanchet@53303
   304
        fun mk_goals f xtor s smap =
blanchet@53303
   305
          ((f, xtor), (s, smap))
blanchet@53303
   306
          |> pairself (HOLogic.mk_comp o co_swap)
blanchet@53303
   307
          |> HOLogic.mk_eq;
blanchet@53303
   308
blanchet@53303
   309
        val fold_goals = map4 mk_goals folds xtors fold_strs pre_fold_maps
blanchet@53303
   310
        val rec_goals = map4 mk_goals recs xtors rec_strs pre_rec_maps;
blanchet@53303
   311
blanchet@53303
   312
        fun mk_thms ss goals tac =
blanchet@53303
   313
          Library.foldr1 HOLogic.mk_conj goals
blanchet@53303
   314
          |> HOLogic.mk_Trueprop
blanchet@53303
   315
          |> fold_rev Logic.all ss
traytel@53331
   316
          |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac)
blanchet@53303
   317
          |> Thm.close_derivation
blanchet@53303
   318
          |> Morphism.thm phi
blanchet@53303
   319
          |> split_conj_thm
blanchet@53303
   320
          |> map (fn thm => thm RS @{thm comp_eq_dest});
blanchet@53303
   321
blanchet@53303
   322
        val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
blanchet@53303
   323
        val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
blanchet@53303
   324
blanchet@53303
   325
        val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss;
blanchet@53303
   326
        val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss;
blanchet@53303
   327
blanchet@53303
   328
        val fp_xtor_co_iterss = steal #xtor_co_iter_thmss;
blanchet@53303
   329
        val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
blanchet@53303
   330
        val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
blanchet@53303
   331
blanchet@53303
   332
        val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
blanchet@53303
   333
        val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
blanchet@53303
   334
        val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
blanchet@55067
   335
        val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
blanchet@55067
   336
          o_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
blanchet@53303
   337
        val rec_thms = fold_thms @ fp_case fp
blanchet@53303
   338
          @{thms fst_convol map_pair_o_convol convol_o}
blanchet@53303
   339
          @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};
blanchet@53303
   340
        val map_thms = no_refl (maps (fn bnf =>
blanchet@53303
   341
          [map_comp0_of_bnf bnf RS sym, map_id0_of_bnf bnf]) fp_nesty_bnfs);
blanchet@53303
   342
blanchet@53303
   343
        fun mk_tac defs o_map_thms xtor_thms thms {context = ctxt, prems = _} =
blanchet@53303
   344
          unfold_thms_tac ctxt
blanchet@53303
   345
            (flat [thms, defs, pre_map_defs, fp_pre_map_defs, xtor_thms, o_map_thms, map_thms]) THEN
blanchet@53303
   346
          CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
blanchet@53303
   347
blanchet@53303
   348
        val fold_tac = mk_tac raw_un_fold_defs fp_fold_o_maps fp_xtor_un_folds fold_thms;
blanchet@53303
   349
        val rec_tac = mk_tac raw_co_rec_defs fp_rec_o_maps fp_xtor_co_recs rec_thms;
blanchet@53303
   350
      in
blanchet@53303
   351
        (mk_thms fold_strs fold_goals fold_tac, mk_thms rec_strs rec_goals rec_tac)
blanchet@53303
   352
      end;
blanchet@53303
   353
blanchet@53303
   354
    (* These results are half broken. This is deliberate. We care only about those fields that are
blanchet@53753
   355
       used by "primrec_new", "primcorecursive", and "datatype_new_compat". *)
blanchet@53303
   356
    val fp_res =
blanchet@53303
   357
      ({Ts = fpTs,
blanchet@53303
   358
        bnfs = steal #bnfs,
blanchet@53303
   359
        dtors = dtors,
blanchet@53303
   360
        ctors = ctors,
blanchet@53303
   361
        xtor_co_iterss = transpose [un_folds, co_recs],
blanchet@53303
   362
        xtor_co_induct = xtor_co_induct_thm,
blanchet@53303
   363
        dtor_ctors = steal #dtor_ctors (*too general types*),
blanchet@53303
   364
        ctor_dtors = steal #ctor_dtors (*too general types*),
blanchet@53303
   365
        ctor_injects = steal #ctor_injects (*too general types*),
blanchet@53303
   366
        dtor_injects = steal #dtor_injects (*too general types*),
blanchet@53303
   367
        xtor_map_thms = steal #xtor_map_thms (*too general types and terms*),
blanchet@53303
   368
        xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*),
blanchet@53303
   369
        xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*),
blanchet@53303
   370
        xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
blanchet@53303
   371
        xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
blanchet@53303
   372
        rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
wenzelm@54740
   373
       |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
blanchet@53303
   374
  in
blanchet@53303
   375
    (fp_res, lthy)
blanchet@54242
   376
  end;
blanchet@53303
   377
blanchet@53303
   378
end;