src/HOL/Tools/BNF/bnf_fp_n2m.ML
author traytel
Mon Nov 24 15:50:10 2014 +0100 (2014-11-24)
changeset 59049 0d1bfc982501
parent 58634 9f10d82e8188
child 59058 a78612c67ec0
permissions -rw-r--r--
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
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@56484
    10
  val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
blanchet@58180
    11
    BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
blanchet@56484
    12
    typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
blanchet@56484
    13
    BNF_FP_Util.fp_result * local_theory
blanchet@53303
    14
end;
blanchet@53303
    15
blanchet@53303
    16
structure BNF_FP_N2M : BNF_FP_N2M =
blanchet@53303
    17
struct
blanchet@53303
    18
blanchet@53303
    19
open BNF_Def
blanchet@53303
    20
open BNF_Util
traytel@55803
    21
open BNF_Comp
blanchet@53303
    22
open BNF_FP_Util
blanchet@53303
    23
open BNF_FP_Def_Sugar
blanchet@53303
    24
open BNF_Tactics
blanchet@53303
    25
open BNF_FP_N2M_Tactics
blanchet@53303
    26
blanchet@53303
    27
fun force_typ ctxt T =
blanchet@56638
    28
  Term.map_types Type_Infer.paramify_vars
blanchet@53303
    29
  #> Type.constraint T
blanchet@53303
    30
  #> Syntax.check_term ctxt
blanchet@53303
    31
  #> singleton (Variable.polymorphic ctxt);
blanchet@53303
    32
blanchet@53303
    33
fun mk_prod_map f g =
blanchet@53303
    34
  let
blanchet@53303
    35
    val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
blanchet@53303
    36
    val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
blanchet@53303
    37
  in
blanchet@55932
    38
    Const (@{const_name map_prod},
blanchet@53303
    39
      fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
blanchet@53303
    40
  end;
blanchet@53303
    41
blanchet@55931
    42
fun mk_map_sum f g =
blanchet@53303
    43
  let
blanchet@53303
    44
    val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
blanchet@53303
    45
    val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
blanchet@53303
    46
  in
blanchet@55931
    47
    Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
blanchet@53303
    48
  end;
blanchet@53303
    49
blanchet@58340
    50
fun construct_mutualized_fp fp mutual_cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss)
blanchet@58340
    51
    bnfs (absT_infos : absT_info list) lthy =
blanchet@53303
    52
  let
traytel@55803
    53
    fun of_fp_res get =
blanchet@55539
    54
      map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
blanchet@53303
    55
blanchet@55966
    56
    fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
blanchet@55966
    57
    fun co_swap pair = case_fp fp I swap pair;
traytel@55803
    58
    val mk_co_comp = HOLogic.mk_comp o co_swap;
blanchet@55966
    59
    val co_productC = BNF_FP_Rec_Sugar_Util.case_fp fp @{type_name prod} @{type_name sum};
traytel@55803
    60
blanchet@53303
    61
    val dest_co_algT = co_swap o dest_funT;
blanchet@55966
    62
    val co_alg_argT = case_fp fp range_type domain_type;
blanchet@55966
    63
    val co_alg_funT = case_fp fp domain_type range_type;
blanchet@55966
    64
    val mk_co_product = curry (case_fp fp mk_convol mk_case_sum);
blanchet@55966
    65
    val mk_map_co_product = case_fp fp mk_prod_map mk_map_sum;
blanchet@55966
    66
    val co_proj1_const = case_fp fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
blanchet@55966
    67
    val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT);
blanchet@55966
    68
    val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT;
blanchet@55966
    69
    val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
traytel@55803
    70
traytel@55803
    71
    val fp_absT_infos = map #absT_info fp_sugars;
traytel@55803
    72
    val fp_bnfs = of_fp_res #bnfs;
traytel@55803
    73
    val pre_bnfs = map #pre_bnf fp_sugars;
blanchet@57397
    74
    val nesting_bnfss =
blanchet@57397
    75
      map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars;
blanchet@57397
    76
    val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss;
blanchet@57397
    77
    val fp_or_nesting_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_or_nesting_bnfss);
traytel@55803
    78
traytel@55803
    79
    val fp_absTs = map #absT fp_absT_infos;
traytel@55803
    80
    val fp_repTs = map #repT fp_absT_infos;
traytel@55803
    81
    val fp_abss = map #abs fp_absT_infos;
traytel@55803
    82
    val fp_reps = map #rep fp_absT_infos;
traytel@55803
    83
    val fp_type_definitions = map #type_definition fp_absT_infos;
traytel@55803
    84
traytel@55803
    85
    val absTs = map #absT absT_infos;
traytel@55803
    86
    val repTs = map #repT absT_infos;
traytel@55803
    87
    val absTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) absTs;
traytel@55803
    88
    val repTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) repTs;
traytel@55803
    89
    val abss = map #abs absT_infos;
traytel@55803
    90
    val reps = map #rep absT_infos;
traytel@55803
    91
    val abs_inverses = map #abs_inverse absT_infos;
traytel@55803
    92
    val type_definitions = map #type_definition absT_infos;
traytel@55803
    93
traytel@55803
    94
    val n = length bnfs;
traytel@55803
    95
    val deads = fold (union (op =)) Dss resDs;
traytel@55803
    96
    val As = subtract (op =) deads (map TFree resBs);
traytel@55803
    97
    val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
traytel@55803
    98
    val m = length As;
traytel@55803
    99
    val live = m + n;
traytel@55803
   100
traytel@55803
   101
    val ((Xs, Bs), names_lthy) = names_lthy
traytel@55803
   102
      |> mk_TFrees n
traytel@55803
   103
      ||>> mk_TFrees m;
traytel@55803
   104
traytel@55803
   105
    val allAs = As @ Xs;
traytel@55803
   106
    val allBs = Bs @ Xs;
traytel@55803
   107
    val phiTs = map2 mk_pred2T As Bs;
traytel@55803
   108
    val thetaBs = As ~~ Bs;
traytel@55803
   109
    val fpTs' = map (Term.typ_subst_atomic thetaBs) fpTs;
traytel@55803
   110
    val fold_thetaAs = Xs ~~ fpTs;
traytel@55803
   111
    val fold_thetaBs = Xs ~~ fpTs';
traytel@55803
   112
    val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs;
traytel@55803
   113
    val pre_phiTs = map2 mk_pred2T fpTs fpTs';
blanchet@53303
   114
blanchet@53303
   115
    val ((ctors, dtors), (xtor's, xtors)) =
blanchet@53303
   116
      let
traytel@55803
   117
        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors);
traytel@55803
   118
        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors);
blanchet@53303
   119
      in
blanchet@55966
   120
        ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors))
blanchet@53303
   121
      end;
blanchet@53303
   122
traytel@55803
   123
    val absATs = map (domain_type o fastype_of) ctors;
traytel@55803
   124
    val absBTs = map (Term.typ_subst_atomic thetaBs) absATs;
blanchet@53303
   125
    val xTs = map (domain_type o fastype_of) xtors;
blanchet@53303
   126
    val yTs = map (domain_type o fastype_of) xtor's;
blanchet@53303
   127
wenzelm@58634
   128
    val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
wenzelm@58634
   129
    val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
traytel@55819
   130
    val fp_repAs = map2 mk_rep absATs fp_reps;
traytel@55819
   131
    val fp_repBs = map2 mk_rep absBTs fp_reps;
traytel@55803
   132
blanchet@53303
   133
    val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
blanchet@53303
   134
      |> mk_Frees' "R" phiTs
blanchet@53303
   135
      ||>> mk_Frees "S" pre_phiTs
blanchet@53303
   136
      ||>> mk_Frees "x" xTs
blanchet@53303
   137
      ||>> mk_Frees "y" yTs;
blanchet@53303
   138
blanchet@53303
   139
    val rels =
blanchet@53303
   140
      let
blanchet@57397
   141
        fun find_rel T As Bs = fp_or_nesting_bnfss
blanchet@55394
   142
          |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
blanchet@53303
   143
          |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
blanchet@53303
   144
          |> Option.map (fn bnf =>
blanchet@53303
   145
            let val live = live_of_bnf bnf;
blanchet@53303
   146
            in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
blanchet@53303
   147
          |> the_default (HOLogic.eq_const T, 0);
blanchet@53303
   148
blanchet@53303
   149
        fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) =
blanchet@53303
   150
              let
blanchet@53303
   151
                val (rel, live) = find_rel T Ts Us;
blanchet@53303
   152
                val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T;
blanchet@53303
   153
                val rels = map2 mk_rel Ts' Us';
blanchet@53303
   154
              in
blanchet@53303
   155
                Term.list_comb (rel, rels)
blanchet@53303
   156
              end
traytel@54244
   157
          | mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As)
traytel@54244
   158
              handle General.Subscript => HOLogic.eq_const T)
blanchet@53303
   159
          | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
blanchet@53303
   160
      in
traytel@54298
   161
        map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs'
blanchet@53303
   162
      end;
blanchet@53303
   163
blanchet@53303
   164
    val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
blanchet@53303
   165
blanchet@55539
   166
    val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
desharna@58579
   167
    val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct)
blanchet@55539
   168
      |> map (unfold_thms lthy (id_apply :: rel_unfolds));
blanchet@53303
   169
blanchet@53303
   170
    val rel_defs = map rel_def_of_bnf bnfs;
blanchet@53303
   171
    val rel_monos = map rel_mono_of_bnf bnfs;
blanchet@53303
   172
traytel@55803
   173
    fun cast castA castB pre_rel =
traytel@55803
   174
      let
traytel@55803
   175
        val castAB = mk_vimage2p (Term.subst_atomic_types fold_thetaAs castA)
traytel@55803
   176
          (Term.subst_atomic_types fold_thetaBs castB);
traytel@55803
   177
      in
traytel@55803
   178
        fold_rev (fold_rev Term.absdummy) [phiTs, pre_phiTs]
traytel@55803
   179
          (castAB $ Term.list_comb (pre_rel, map Bound (live - 1 downto 0)))
traytel@55803
   180
      end;
traytel@55803
   181
traytel@55803
   182
    val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs;
traytel@55803
   183
    val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs;
traytel@55803
   184
blanchet@58375
   185
    val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
blanchet@58375
   186
    val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
traytel@58203
   187
traytel@59049
   188
    val rel_xtor_co_inducts_inst =
traytel@59049
   189
      let
traytel@59049
   190
        val extract =
traytel@59049
   191
          case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
traytel@59049
   192
        val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
traytel@59049
   193
        val thetas = AList.group (op =)
traytel@59049
   194
          (mutual_cliques ~~ map (pairself (certify lthy)) (raw_phis ~~ pre_phis));
traytel@59049
   195
      in
traytel@59049
   196
        map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas)
traytel@59049
   197
        mutual_cliques rel_xtor_co_inducts
traytel@59049
   198
      end
traytel@59049
   199
desharna@58579
   200
    val xtor_rel_co_induct =
wenzelm@58634
   201
      mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys
traytel@59049
   202
        xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts_inst rel_defs
blanchet@58375
   203
          rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
traytel@55803
   204
        lthy;
blanchet@53303
   205
blanchet@53303
   206
    val map_id0s = no_refl (map map_id0_of_bnf bnfs);
blanchet@53303
   207
blanchet@53303
   208
    val xtor_co_induct_thm =
blanchet@53303
   209
      (case fp of
blanchet@53303
   210
        Least_FP =>
blanchet@53303
   211
          let
blanchet@53303
   212
            val (Ps, names_lthy) = names_lthy
blanchet@53303
   213
              |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
blanchet@53303
   214
            fun mk_Grp_id P =
blanchet@53303
   215
              let val T = domain_type (fastype_of P);
blanchet@53303
   216
              in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
blanchet@53303
   217
            val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
traytel@55803
   218
            fun mk_fp_type_copy_thms thm = map (curry op RS thm)
traytel@55803
   219
              @{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
traytel@55803
   220
            fun mk_type_copy_thms thm = map (curry op RS thm)
traytel@55803
   221
              @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
blanchet@53303
   222
          in
desharna@58579
   223
            cterm_instantiate_pos cts xtor_rel_co_induct
blanchet@53303
   224
            |> singleton (Proof_Context.export names_lthy lthy)
blanchet@58375
   225
            |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
blanchet@58375
   226
                fp_or_nesting_rel_eqs)
blanchet@53303
   227
            |> funpow n (fn thm => thm RS spec)
blanchet@53303
   228
            |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
blanchet@55854
   229
            |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
traytel@55803
   230
               Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
traytel@55803
   231
               maps mk_fp_type_copy_thms fp_type_definitions @
traytel@55803
   232
               maps mk_type_copy_thms type_definitions)
blanchet@53303
   233
            |> unfold_thms lthy @{thms subset_iff mem_Collect_eq
blanchet@53303
   234
               atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
blanchet@53303
   235
          end
blanchet@53303
   236
      | Greatest_FP =>
blanchet@53303
   237
          let
blanchet@53303
   238
            val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
blanchet@53303
   239
          in
desharna@58579
   240
            cterm_instantiate_pos cts xtor_rel_co_induct
blanchet@58375
   241
            |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
blanchet@58375
   242
                fp_or_nesting_rel_eqs)
blanchet@53303
   243
            |> funpow (2 * n) (fn thm => thm RS spec)
wenzelm@54742
   244
            |> Conv.fconv_rule (Object_Logic.atomize lthy)
blanchet@53303
   245
            |> funpow n (fn thm => thm RS mp)
blanchet@53303
   246
          end);
blanchet@53303
   247
blanchet@53303
   248
    val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
blanchet@53303
   249
    val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
blanchet@53303
   250
blanchet@53303
   251
    val rec_strTs = map2 mk_co_algT rec_preTs Xs;
blanchet@53303
   252
    val resTs = map2 mk_co_algT fpTs Xs;
blanchet@53303
   253
blanchet@55894
   254
    val ((rec_strs, rec_strs'), names_lthy) = names_lthy
blanchet@55894
   255
      |> mk_Frees' "s" rec_strTs;
blanchet@53303
   256
blanchet@55868
   257
    val co_recs = of_fp_res #xtor_co_recs;
blanchet@55539
   258
    val ns = map (length o #Ts o #fp_res) fp_sugars;
blanchet@55539
   259
traytel@55803
   260
    val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
traytel@55803
   261
traytel@55899
   262
    fun foldT_of_recT recT =
traytel@55899
   263
      let
traytel@57802
   264
        val ((FTXs, Ys), TX) = strip_fun_type recT |>> map_split dest_co_algT;
traytel@57802
   265
        val Zs = union op = Xs Ys;
traytel@55899
   266
        fun subst (Type (C, Ts as [_, X])) =
traytel@57802
   267
            if C = co_productC andalso member op = Zs X then X else Type (C, map subst Ts)
traytel@55899
   268
          | subst (Type (C, Ts)) = Type (C, map subst Ts)
traytel@55899
   269
          | subst T = T;
traytel@55899
   270
      in
traytel@57802
   271
        map2 (mk_co_algT o subst) FTXs Ys ---> TX
traytel@55899
   272
      end;
traytel@55899
   273
traytel@57802
   274
    fun force_rec i TU raw_rec =
blanchet@53303
   275
      let
traytel@55803
   276
        val thy = Proof_Context.theory_of lthy;
traytel@55803
   277
traytel@55899
   278
        val approx_rec = raw_rec
traytel@57802
   279
          |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU);
traytel@55803
   280
        val subst = Term.typ_subst_atomic fold_thetaAs;
traytel@55803
   281
traytel@55803
   282
        fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
wenzelm@58634
   283
        val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
traytel@55803
   284
traytel@55803
   285
        val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
traytel@55803
   286
traytel@55803
   287
        val fold_pre_deads_only_Ts =
traytel@58162
   288
          map (typ_subst_nonatomic_sorted (map (rpair dummyT)
traytel@58162
   289
            (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs';
traytel@55803
   290
blanchet@58340
   291
        val (mutual_clique, TUs) =
traytel@56487
   292
          map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
traytel@55478
   293
          |>> map subst
traytel@56487
   294
          |> `(fn (_, Ys) =>
blanchet@58340
   295
            nth mutual_cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
traytel@56487
   296
          ||> uncurry (map2 mk_co_algT);
blanchet@58340
   297
        val cands = mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs;
traytel@56487
   298
        val js = find_indices (fn ((cl, cand), TU) =>
blanchet@58340
   299
          cl = mutual_clique andalso Type.could_unify (TU, cand)) TUs cands;
blanchet@53303
   300
        val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
blanchet@53303
   301
      in
blanchet@55894
   302
        force_typ names_lthy (Tpats ---> TU) raw_rec
blanchet@53303
   303
      end;
blanchet@53303
   304
traytel@55803
   305
    fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
blanchet@55966
   306
      case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
traytel@55803
   307
        (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t)));
traytel@55803
   308
blanchet@55894
   309
    fun mk_rec b_opt recs lthy TU =
blanchet@53303
   310
      let
traytel@55803
   311
        val thy = Proof_Context.theory_of lthy;
traytel@55803
   312
blanchet@53303
   313
        val x = co_alg_argT TU;
blanchet@53303
   314
        val i = find_index (fn T => x = T) Xs;
blanchet@55894
   315
        val TUrec =
blanchet@55894
   316
          (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
traytel@57802
   317
            NONE => force_rec i TU (nth co_recs i)
blanchet@53303
   318
          | SOME f => f);
traytel@55803
   319
blanchet@55894
   320
        val TUs = binder_fun_types (fastype_of TUrec);
traytel@55803
   321
blanchet@53303
   322
        fun mk_s TU' =
blanchet@53303
   323
          let
traytel@55803
   324
            fun mk_absT_fp_repT repT absT = mk_absT thy repT absT ooo mk_repT;
traytel@55803
   325
blanchet@53303
   326
            val i = find_index (fn T => co_alg_argT TU' = T) Xs;
traytel@55803
   327
            val fp_abs = nth fp_abss i;
traytel@55803
   328
            val fp_rep = nth fp_reps i;
traytel@55803
   329
            val abs = nth abss i;
traytel@55803
   330
            val rep = nth reps i;
blanchet@54233
   331
            val sF = co_alg_funT TU';
traytel@55803
   332
            val sF' =
traytel@55803
   333
              mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF
traytel@55803
   334
                handle Term.TYPE _ => sF;
blanchet@55894
   335
            val F = nth rec_preTs i;
blanchet@55894
   336
            val s = nth rec_strs i;
blanchet@53303
   337
          in
traytel@55803
   338
            if sF = F then s
traytel@55803
   339
            else if sF' = F then mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s
blanchet@53303
   340
            else
blanchet@53303
   341
              let
traytel@55803
   342
                val smapT = replicate live dummyT ---> mk_co_algT sF' F;
blanchet@53303
   343
                fun hidden_to_unit t =
blanchet@53303
   344
                  Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
blanchet@53303
   345
                val smap = map_of_bnf (nth bnfs i)
blanchet@53303
   346
                  |> force_typ names_lthy smapT
blanchet@53303
   347
                  |> hidden_to_unit;
blanchet@53303
   348
                val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
blanchet@58352
   349
                fun mk_smap_arg T_to_U =
blanchet@58352
   350
                  (if domain_type T_to_U = range_type T_to_U then
blanchet@58352
   351
                    HOLogic.id_const (domain_type T_to_U)
blanchet@55894
   352
                  else
blanchet@53303
   353
                    let
blanchet@58352
   354
                      val (TY, (U, X)) = T_to_U |> dest_co_algT ||> dest_co_productT;
blanchet@53303
   355
                      val T = mk_co_algT TY U;
blanchet@58352
   356
                      fun mk_co_proj TU =
blanchet@58352
   357
                        build_map lthy [] (fn TU =>
blanchet@58352
   358
                          let val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT in
blanchet@58352
   359
                            if T1 = U then co_proj1_const TU
blanchet@58352
   360
                            else mk_co_comp (mk_co_proj (co_swap (T1, U)),
blanchet@58352
   361
                              co_proj1_const (co_swap (mk_co_productT T1 T2, T1)))
blanchet@58352
   362
                          end)
blanchet@58352
   363
                          TU;
blanchet@58352
   364
                      fun default () =
blanchet@58352
   365
                        mk_co_product (mk_co_proj (dest_funT T))
blanchet@58352
   366
                          (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))));
blanchet@53303
   367
                    in
blanchet@58352
   368
                      if can dest_co_productT TY then
blanchet@58352
   369
                        mk_map_co_product (mk_co_proj (co_swap (dest_co_productT TY |> fst, U)))
blanchet@58352
   370
                          (HOLogic.id_const X)
blanchet@58352
   371
                        handle TYPE _ => default () (*N2M involving "prod" type*)
blanchet@58352
   372
                      else
blanchet@58352
   373
                        default ()
blanchet@55894
   374
                    end)
blanchet@53303
   375
                val smap_args = map mk_smap_arg smap_argTs;
blanchet@53303
   376
              in
traytel@55803
   377
                mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep
traytel@55803
   378
                  (mk_co_comp (s, Term.list_comb (smap, smap_args)))
traytel@55803
   379
              end
blanchet@53303
   380
          end;
blanchet@55894
   381
        val t = Term.list_comb (TUrec, map mk_s TUs);
blanchet@53303
   382
      in
blanchet@53303
   383
        (case b_opt of
blanchet@53303
   384
          NONE => ((t, Drule.dummy_thm), lthy)
blanchet@54233
   385
        | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.conceal (Thm.def_binding b), []),
blanchet@55894
   386
            fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd)
blanchet@53303
   387
      end;
blanchet@53303
   388
blanchet@55966
   389
    val recN = case_fp fp ctor_recN dtor_corecN;
blanchet@55894
   390
    fun mk_recs lthy =
blanchet@55894
   391
      fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
blanchet@55894
   392
        mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
blanchet@55894
   393
      resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
desharna@57527
   394
      |>> map_prod rev rev;
blanchet@55894
   395
    val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy
blanchet@55894
   396
      |> mk_recs
traytel@53331
   397
      ||> `Local_Theory.restore;
blanchet@53303
   398
traytel@53331
   399
    val phi = Proof_Context.export_morphism raw_lthy lthy;
blanchet@53303
   400
blanchet@53303
   401
    val co_recs = map (Morphism.term phi) raw_co_recs;
blanchet@53303
   402
desharna@58578
   403
    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_maps
traytel@56486
   404
      |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
blanchet@55868
   405
blanchet@55894
   406
    val xtor_co_rec_thms =
blanchet@53303
   407
      let
blanchet@53303
   408
        val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_co_recs;
blanchet@53303
   409
        val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs);
blanchet@53303
   410
        val pre_rec_maps =
blanchet@53303
   411
          map2 (fn Ds => fn bnf =>
blanchet@53303
   412
            Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf,
blanchet@53303
   413
              map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs))
blanchet@53303
   414
          Dss bnfs;
blanchet@53303
   415
traytel@55803
   416
        fun mk_goals f xtor s smap fp_abs fp_rep abs rep =
traytel@55803
   417
          let
traytel@55803
   418
            val lhs = mk_co_comp (f, xtor);
traytel@55803
   419
            val rhs = mk_co_comp (s, smap);
traytel@55803
   420
          in
traytel@55803
   421
            HOLogic.mk_eq (lhs,
traytel@55803
   422
              mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs))
traytel@55803
   423
                fp_abs fp_rep abs rep rhs)
traytel@55803
   424
          end;
blanchet@53303
   425
wenzelm@58634
   426
        val goals = @{map 8} mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
blanchet@53303
   427
blanchet@53303
   428
        val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
blanchet@53303
   429
        val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
blanchet@53303
   430
traytel@55803
   431
        val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
traytel@55803
   432
blanchet@55868
   433
        val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
blanchet@53303
   434
blanchet@55966
   435
        val fold_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
blanchet@55932
   436
          map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
blanchet@55932
   437
          @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
blanchet@55966
   438
        val rec_thms = fold_thms @ case_fp fp
traytel@57802
   439
          @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod}
traytel@57802
   440
          @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)};
traytel@55803
   441
traytel@55810
   442
        val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
traytel@55803
   443
blanchet@53303
   444
        val map_thms = no_refl (maps (fn bnf =>
traytel@55803
   445
           let val map_comp0 = map_comp0_of_bnf bnf RS sym
blanchet@57397
   446
           in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end)
blanchet@57397
   447
          fp_or_nesting_bnfs) @
blanchet@55966
   448
          remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
traytel@55803
   449
          (map2 (fn thm => fn bnf =>
traytel@55803
   450
            @{thm type_copy_map_comp0_undo} OF
traytel@55803
   451
              (replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS
traytel@55803
   452
              rewrite_comp_comp)
traytel@55803
   453
          type_definitions bnfs);
traytel@55803
   454
traytel@57801
   455
        fun mk_Rep_o_Abs thm = (thm RS @{thm type_copy_Rep_o_Abs})
traytel@57801
   456
          |> (fn thm => [thm, thm RS rewrite_comp_comp]);
traytel@55803
   457
traytel@57801
   458
        val fp_Rep_o_Abss = maps mk_Rep_o_Abs fp_type_definitions;
traytel@57801
   459
        val Rep_o_Abss = maps mk_Rep_o_Abs type_definitions;
blanchet@53303
   460
blanchet@55894
   461
        fun tac {context = ctxt, prems = _} =
blanchet@58352
   462
          unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs,
blanchet@58352
   463
            fp_pre_map_defs, fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss,
blanchet@58352
   464
            Rep_o_Abss]) THEN
blanchet@53303
   465
          CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
blanchet@53303
   466
      in
blanchet@55894
   467
        Library.foldr1 HOLogic.mk_conj goals
blanchet@55894
   468
        |> HOLogic.mk_Trueprop
blanchet@55894
   469
        |> fold_rev Logic.all rec_strs
blanchet@55894
   470
        |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac)
blanchet@55894
   471
        |> Thm.close_derivation
blanchet@55894
   472
        |> Morphism.thm phi
blanchet@55894
   473
        |> split_conj_thm
blanchet@55894
   474
        |> map (fn thm => thm RS @{thm comp_eq_dest})
blanchet@53303
   475
      end;
blanchet@53303
   476
blanchet@53303
   477
    (* These results are half broken. This is deliberate. We care only about those fields that are
blanchet@55531
   478
       used by "primrec", "primcorecursive", and "datatype_compat". *)
blanchet@53303
   479
    val fp_res =
blanchet@55894
   480
      ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors,
blanchet@55868
   481
        xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
traytel@55803
   482
        dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
traytel@55803
   483
        ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
traytel@55803
   484
        ctor_injects = of_fp_res #ctor_injects (*too general types*),
traytel@55803
   485
        dtor_injects = of_fp_res #dtor_injects (*too general types*),
desharna@58583
   486
        xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
desharna@58584
   487
        xtor_setss = of_fp_res #xtor_setss (*too general types and terms*),
desharna@58585
   488
        xtor_rels = of_fp_res #xtor_rels (*too general types and terms*),
blanchet@55868
   489
        xtor_co_rec_thms = xtor_co_rec_thms,
desharna@58578
   490
        xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
desharna@58579
   491
        xtor_rel_co_induct = xtor_rel_co_induct,
desharna@58580
   492
        dtor_set_inducts = [],
desharna@58581
   493
        xtor_co_rec_transfers = []}
wenzelm@54740
   494
       |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
blanchet@53303
   495
  in
blanchet@53303
   496
    (fp_res, lthy)
blanchet@54242
   497
  end;
blanchet@53303
   498
blanchet@53303
   499
end;