src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
author blanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 54006 9fe1bd54d437
parent 53974 612505263257
child 54009 f138452e8265
permissions -rw-r--r--
renamed theory file
     1 (*  Title:      HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
     2     Author:     Lorenz Panny, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2013
     5 
     6 Library for recursor and corecursor sugar.
     7 *)
     8 
     9 signature BNF_FP_REC_SUGAR_UTIL =
    10 sig
    11   datatype rec_call =
    12     No_Rec of int |
    13     Direct_Rec of int (*before*) * int (*after*) |
    14     Indirect_Rec of int
    15 
    16   datatype corec_call =
    17     Dummy_No_Corec of int |
    18     No_Corec of int |
    19     Direct_Corec of int (*stop?*) * int (*end*) * int (*continue*) |
    20     Indirect_Corec of int
    21 
    22   type rec_ctr_spec =
    23     {ctr: term,
    24      offset: int,
    25      calls: rec_call list,
    26      rec_thm: thm}
    27 
    28   type corec_ctr_spec =
    29     {ctr: term,
    30      disc: term,
    31      sels: term list,
    32      pred: int option,
    33      calls: corec_call list,
    34      discI: thm,
    35      sel_thms: thm list,
    36      collapse: thm,
    37      corec_thm: thm,
    38      disc_corec: thm,
    39      sel_corecs: thm list}
    40 
    41   type rec_spec =
    42     {recx: term,
    43      nested_map_idents: thm list,
    44      nested_map_comps: thm list,
    45      ctr_specs: rec_ctr_spec list}
    46 
    47   type corec_spec =
    48     {corec: term,
    49      nested_maps: thm list,
    50      nested_map_idents: thm list,
    51      nested_map_comps: thm list,
    52      ctr_specs: corec_ctr_spec list}
    53 
    54   val s_not: term -> term
    55   val mk_conjs: term list -> term
    56   val mk_disjs: term list -> term
    57   val s_not_disj: term -> term list
    58   val negate_conj: term list -> term list
    59   val negate_disj: term list -> term list
    60 
    61   val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
    62     typ list -> term -> term -> term -> term
    63   val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
    64     typ list -> term -> term
    65   val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
    66     (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term
    67   val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
    68   val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
    69     typ list -> term -> term
    70   val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
    71     typ list -> term -> 'a -> 'a
    72   val case_thms_of_term: Proof.context -> typ list -> term ->
    73     thm list * thm list * thm list * thm list
    74 
    75   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
    76     ((term * term list list) list) list -> local_theory ->
    77     (bool * rec_spec list * typ list * thm * thm list) * local_theory
    78   val corec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
    79     ((term * term list list) list) list -> local_theory ->
    80     (bool * corec_spec list * typ list * thm * thm * thm list * thm list) * local_theory
    81 end;
    82 
    83 structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
    84 struct
    85 
    86 open Ctr_Sugar
    87 open BNF_Util
    88 open BNF_Def
    89 open BNF_FP_Util
    90 open BNF_FP_Def_Sugar
    91 open BNF_FP_N2M_Sugar
    92 
    93 datatype rec_call =
    94   No_Rec of int |
    95   Direct_Rec of int * int |
    96   Indirect_Rec of int;
    97 
    98 datatype corec_call =
    99   Dummy_No_Corec of int |
   100   No_Corec of int |
   101   Direct_Corec of int * int * int |
   102   Indirect_Corec of int;
   103 
   104 type rec_ctr_spec =
   105   {ctr: term,
   106    offset: int,
   107    calls: rec_call list,
   108    rec_thm: thm};
   109 
   110 type corec_ctr_spec =
   111   {ctr: term,
   112    disc: term,
   113    sels: term list,
   114    pred: int option,
   115    calls: corec_call list,
   116    discI: thm,
   117    sel_thms: thm list,
   118    collapse: thm,
   119    corec_thm: thm,
   120    disc_corec: thm,
   121    sel_corecs: thm list};
   122 
   123 type rec_spec =
   124   {recx: term,
   125    nested_map_idents: thm list,
   126    nested_map_comps: thm list,
   127    ctr_specs: rec_ctr_spec list};
   128 
   129 type corec_spec =
   130   {corec: term,
   131    nested_maps: thm list,
   132    nested_map_idents: thm list,
   133    nested_map_comps: thm list,
   134    ctr_specs: corec_ctr_spec list};
   135 
   136 val id_def = @{thm id_def};
   137 
   138 exception AINT_NO_MAP of term;
   139 
   140 fun ill_formed_rec_call ctxt t =
   141   error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
   142 fun ill_formed_corec_call ctxt t =
   143   error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
   144 fun invalid_map ctxt t =
   145   error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
   146 fun unexpected_rec_call ctxt t =
   147   error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t));
   148 fun unexpected_corec_call ctxt t =
   149   error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
   150 
   151 fun s_not @{const True} = @{const False}
   152   | s_not @{const False} = @{const True}
   153   | s_not (@{const Not} $ t) = t
   154   | s_not t = HOLogic.mk_not t
   155 
   156 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
   157 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
   158 
   159 val s_not_disj = map s_not o HOLogic.disjuncts;
   160 
   161 fun negate_conj [t] = s_not_disj t
   162   | negate_conj ts = [mk_disjs (map s_not ts)];
   163 
   164 fun negate_disj [t] = s_not_disj t
   165   | negate_disj ts = [mk_disjs (map (mk_conjs o s_not_disj) ts)];
   166 
   167 fun factor_out_types ctxt massage destU U T =
   168   (case try destU U of
   169     SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
   170   | NONE => invalid_map ctxt);
   171 
   172 fun map_flattened_map_args ctxt s map_args fs =
   173   let
   174     val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs;
   175     val flat_fs' = map_args flat_fs;
   176   in
   177     permute_like (op aconv) flat_fs fs flat_fs'
   178   end;
   179 
   180 fun massage_indirect_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
   181   let
   182     val typof = curry fastype_of1 bound_Ts;
   183     val build_map_fst = build_map ctxt (fst_const o fst);
   184 
   185     val yT = typof y;
   186     val yU = typof y';
   187 
   188     fun y_of_y' () = build_map_fst (yU, yT) $ y';
   189     val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
   190 
   191     fun massage_direct_fun U T t =
   192       if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
   193       else HOLogic.mk_comp (t, build_map_fst (U, T));
   194 
   195     fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
   196         (case try (dest_map ctxt s) t of
   197           SOME (map0, fs) =>
   198           let
   199             val Type (_, ran_Ts) = range_type (typof t);
   200             val map' = mk_map (length fs) Us ran_Ts map0;
   201             val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
   202           in
   203             Term.list_comb (map', fs')
   204           end
   205         | NONE => raise AINT_NO_MAP t)
   206       | massage_map _ _ t = raise AINT_NO_MAP t
   207     and massage_map_or_map_arg U T t =
   208       if T = U then
   209         if has_call t then unexpected_rec_call ctxt t else t
   210       else
   211         massage_map U T t
   212         handle AINT_NO_MAP _ => massage_direct_fun U T t;
   213 
   214     fun massage_call (t as t1 $ t2) =
   215         if t2 = y then
   216           massage_map yU yT (elim_y t1) $ y'
   217           handle AINT_NO_MAP t' => invalid_map ctxt t'
   218         else
   219           ill_formed_rec_call ctxt t
   220       | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
   221   in
   222     massage_call
   223   end;
   224 
   225 fun fold_rev_let_if_case ctxt f bound_Ts t =
   226   let
   227     val thy = Proof_Context.theory_of ctxt;
   228 
   229     fun fld conds t =
   230       (case Term.strip_comb t of
   231         (Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
   232       | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
   233         fld (conds @ HOLogic.conjuncts cond) then_branch
   234         o fld (conds @ s_not_disj cond) else_branch
   235       | (Const (c, _), args as _ :: _ :: _) =>
   236         let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
   237           if n >= 0 andalso n < length args then
   238             (case fastype_of1 (bound_Ts, nth args n) of
   239               Type (s, Ts) =>
   240               (case dest_case ctxt s Ts t of
   241                 NONE => apsnd (f conds t)
   242               | SOME (conds', branches) =>
   243                 apfst (cons s) o fold_rev (uncurry fld)
   244                   (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
   245             | _ => apsnd (f conds t))
   246           else
   247             apsnd (f conds t)
   248         end
   249       | _ => apsnd (f conds t))
   250   in
   251     fld [] t o pair []
   252   end;
   253 
   254 fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
   255 
   256 fun massage_let_if_case ctxt has_call massage_leaf =
   257   let
   258     val thy = Proof_Context.theory_of ctxt;
   259 
   260     fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
   261 
   262     fun massage_abs bound_Ts (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) t)
   263       | massage_abs bound_Ts t = massage_rec bound_Ts t
   264     and massage_rec bound_Ts t =
   265       let val typof = curry fastype_of1 bound_Ts in
   266         (case Term.strip_comb t of
   267           (Const (@{const_name Let}, _), [arg1, arg2]) =>
   268           massage_rec bound_Ts (betapply (arg2, arg1))
   269         | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
   270           let val branches' = map (massage_rec bound_Ts) branches in
   271             Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
   272           end
   273         | (Const (c, _), args as _ :: _ :: _) =>
   274           let
   275             val gen_T = Sign.the_const_type thy c;
   276             val (gen_branch_Ts, gen_body_fun_T) = strip_fun_type gen_T;
   277             val n = length gen_branch_Ts;
   278           in
   279             if n < length args then
   280               (case gen_body_fun_T of
   281                 Type (_, [Type (T_name, _), _]) =>
   282                 if case_of ctxt T_name = SOME c then
   283                   let
   284                     val (branches, obj_leftovers) = chop n args;
   285                     val branches' = map (massage_abs bound_Ts o Envir.eta_long bound_Ts) branches;
   286                     val branch_Ts' = map typof branches';
   287                     val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers --->
   288                       snd (strip_typeN (num_binder_types (hd gen_branch_Ts)) (hd branch_Ts')));
   289                   in
   290                     Term.list_comb (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
   291                   end
   292                 else
   293                   massage_leaf bound_Ts t
   294               | _ => massage_leaf bound_Ts t)
   295             else
   296               massage_leaf bound_Ts t
   297           end
   298         | _ => massage_leaf bound_Ts t)
   299       end
   300   in
   301     massage_rec
   302   end;
   303 
   304 val massage_direct_corec_call = massage_let_if_case;
   305 
   306 fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
   307   let
   308     val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
   309 
   310     fun massage_direct_call bound_Ts U T t =
   311       if has_call t then factor_out_types ctxt (raw_massage_call bound_Ts) dest_sumT U T t
   312       else build_map_Inl (T, U) $ t;
   313 
   314     fun massage_direct_fun bound_Ts U T t =
   315       let
   316         val var = Var ((Name.uu, Term.maxidx_of_term t + 1),
   317           domain_type (fastype_of1 (bound_Ts, t)));
   318       in
   319         Term.lambda var (massage_direct_call bound_Ts U T (t $ var))
   320       end;
   321 
   322     fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
   323         (case try (dest_map ctxt s) t of
   324           SOME (map0, fs) =>
   325           let
   326             val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t));
   327             val map' = mk_map (length fs) dom_Ts Us map0;
   328             val fs' =
   329               map_flattened_map_args ctxt s (map3 (massage_map_or_map_arg bound_Ts) Us Ts) fs;
   330           in
   331             Term.list_comb (map', fs')
   332           end
   333         | NONE => raise AINT_NO_MAP t)
   334       | massage_map _ _ _ t = raise AINT_NO_MAP t
   335     and massage_map_or_map_arg bound_Ts U T t =
   336       if T = U then
   337         if has_call t then unexpected_corec_call ctxt t else t
   338       else
   339         massage_map bound_Ts U T t
   340         handle AINT_NO_MAP _ => massage_direct_fun bound_Ts U T t;
   341 
   342     fun massage_call bound_Ts U T =
   343       massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
   344         if has_call t then
   345           (case U of
   346             Type (s, Us) =>
   347             (case try (dest_ctr ctxt s) t of
   348               SOME (f, args) =>
   349               let
   350                 val typof = curry fastype_of1 bound_Ts;
   351                 val f' = mk_ctr Us f
   352                 val f'_T = typof f';
   353                 val arg_Ts = map typof args;
   354               in
   355                 Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
   356               end
   357             | NONE =>
   358               (case t of
   359                 t1 $ t2 =>
   360                 (if has_call t2 then
   361                   massage_direct_call bound_Ts U T t
   362                 else
   363                   massage_map bound_Ts U T t1 $ t2
   364                   handle AINT_NO_MAP _ => massage_direct_call bound_Ts U T t)
   365               | Abs (s, T', t') =>
   366                 Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
   367               | _ => massage_direct_call bound_Ts U T t))
   368           | _ => ill_formed_corec_call ctxt t)
   369         else
   370           build_map_Inl (T, U) $ t) bound_Ts;
   371 
   372     val T = fastype_of1 (bound_Ts, t);
   373   in
   374     if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
   375   end;
   376 
   377 fun expand_ctr_term ctxt s Ts t =
   378   (case ctr_sugar_of ctxt s of
   379     SOME {ctrs, casex, ...} =>
   380     Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t
   381   | NONE => raise Fail "expand_ctr_term");
   382 
   383 fun expand_corec_code_rhs ctxt has_call bound_Ts t =
   384   (case fastype_of1 (bound_Ts, t) of
   385     Type (s, Ts) =>
   386     massage_let_if_case ctxt has_call (fn _ => fn t =>
   387       if can (dest_ctr ctxt s) t then t else expand_ctr_term ctxt s Ts t) bound_Ts t
   388   | _ => raise Fail "expand_corec_code_rhs");
   389 
   390 fun massage_corec_code_rhs ctxt massage_ctr =
   391   massage_let_if_case ctxt (K false)
   392     (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb);
   393 
   394 fun fold_rev_corec_code_rhs ctxt f =
   395   snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
   396 
   397 fun case_thms_of_term ctxt bound_Ts t =
   398   let
   399     val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
   400     val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
   401   in
   402     (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
   403      maps #sel_split_asms ctr_sugars)
   404   end;
   405 
   406 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
   407 fun indexedd xss = fold_map indexed xss;
   408 fun indexeddd xsss = fold_map indexedd xsss;
   409 fun indexedddd xssss = fold_map indexeddd xssss;
   410 
   411 fun find_index_eq hs h = find_index (curry (op =) h) hs;
   412 
   413 (*FIXME: remove special cases for products and sum once they are registered as datatypes*)
   414 fun map_thms_of_typ ctxt (Type (s, _)) =
   415     if s = @{type_name prod} then
   416       @{thms map_pair_simp}
   417     else if s = @{type_name sum} then
   418       @{thms sum_map.simps}
   419     else
   420       (case fp_sugar_of ctxt s of
   421         SOME {index, mapss, ...} => nth mapss index
   422       | NONE => [])
   423   | map_thms_of_typ _ _ = [];
   424 
   425 val lose_co_rec = false (*FIXME: try true?*);
   426 
   427 fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
   428   let
   429     val thy = Proof_Context.theory_of lthy;
   430 
   431     val ((missing_arg_Ts, perm0_kks,
   432           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
   433             co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy') =
   434       nested_to_mutual_fps lose_co_rec Least_FP bs arg_Ts get_indices callssss0 lthy;
   435 
   436     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
   437 
   438     val indices = map #index fp_sugars;
   439     val perm_indices = map #index perm_fp_sugars;
   440 
   441     val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
   442     val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
   443     val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
   444 
   445     val nn0 = length arg_Ts;
   446     val nn = length perm_fpTs;
   447     val kks = 0 upto nn - 1;
   448     val perm_ns = map length perm_ctr_Tsss;
   449     val perm_mss = map (map length) perm_ctr_Tsss;
   450 
   451     val perm_Cs = map (body_type o fastype_of o co_rec_of o of_fp_sugar (#xtor_co_iterss o #fp_res))
   452       perm_fp_sugars;
   453     val perm_fun_arg_Tssss =
   454       mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1);
   455 
   456     fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
   457     fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
   458 
   459     val induct_thms = unpermute0 (conj_dests nn induct_thm);
   460 
   461     val fpTs = unpermute perm_fpTs;
   462     val Cs = unpermute perm_Cs;
   463 
   464     val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
   465     val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
   466 
   467     val substA = Term.subst_TVars As_rho;
   468     val substAT = Term.typ_subst_TVars As_rho;
   469     val substCT = Term.typ_subst_TVars Cs_rho;
   470 
   471     val perm_Cs' = map substCT perm_Cs;
   472 
   473     fun offset_of_ctr 0 _ = 0
   474       | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
   475         length ctrs + offset_of_ctr (n - 1) ctr_sugars;
   476 
   477     fun call_of [i] [T] = (if exists_subtype_in Cs T then Indirect_Rec else No_Rec) i
   478       | call_of [i, i'] _ = Direct_Rec (i, i');
   479 
   480     fun mk_ctr_spec ctr offset fun_arg_Tss rec_thm =
   481       let
   482         val (fun_arg_hss, _) = indexedd fun_arg_Tss 0;
   483         val fun_arg_hs = flat_rec_arg_args fun_arg_hss;
   484         val fun_arg_iss = map (map (find_index_eq fun_arg_hs)) fun_arg_hss;
   485       in
   486         {ctr = substA ctr, offset = offset, calls = map2 call_of fun_arg_iss fun_arg_Tss,
   487          rec_thm = rec_thm}
   488       end;
   489 
   490     fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss =
   491       let
   492         val ctrs = #ctrs (nth ctr_sugars index);
   493         val rec_thmss = co_rec_of (nth iter_thmsss index);
   494         val k = offset_of_ctr index ctr_sugars;
   495         val n = length ctrs;
   496       in
   497         map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thmss
   498       end;
   499 
   500     fun mk_spec ({T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...}
   501       : fp_sugar) =
   502       {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
   503        nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
   504        nested_map_comps = map map_comp_of_bnf nested_bnfs,
   505        ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
   506   in
   507     ((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms),
   508      lthy')
   509   end;
   510 
   511 fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
   512   let
   513     val thy = Proof_Context.theory_of lthy;
   514 
   515     val ((missing_res_Ts, perm0_kks,
   516           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
   517             co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') =
   518       nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
   519 
   520     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
   521 
   522     val indices = map #index fp_sugars;
   523     val perm_indices = map #index perm_fp_sugars;
   524 
   525     val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
   526     val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
   527     val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
   528 
   529     val nn0 = length res_Ts;
   530     val nn = length perm_fpTs;
   531     val kks = 0 upto nn - 1;
   532     val perm_ns = map length perm_ctr_Tsss;
   533 
   534     val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
   535       of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
   536     val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
   537       mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
   538 
   539     val (perm_p_hss, h) = indexedd perm_p_Tss 0;
   540     val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;
   541     val (perm_f_hssss, _) = indexedddd perm_f_Tssss h';
   542 
   543     val fun_arg_hs =
   544       flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
   545 
   546     fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
   547     fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
   548 
   549     val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms;
   550 
   551     val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
   552     val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
   553     val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
   554 
   555     val f_Tssss = unpermute perm_f_Tssss;
   556     val fpTs = unpermute perm_fpTs;
   557     val Cs = unpermute perm_Cs;
   558 
   559     val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
   560     val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
   561 
   562     val substA = Term.subst_TVars As_rho;
   563     val substAT = Term.typ_subst_TVars As_rho;
   564     val substCT = Term.typ_subst_TVars Cs_rho;
   565 
   566     val perm_Cs' = map substCT perm_Cs;
   567 
   568     fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
   569         (if exists_subtype_in Cs T then Indirect_Corec
   570          else if nullary then Dummy_No_Corec
   571          else No_Corec) g_i
   572       | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
   573 
   574     fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm
   575         disc_corec sel_corecs =
   576       let val nullary = not (can dest_funT (fastype_of ctr)) in
   577         {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
   578          calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
   579          collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec,
   580          sel_corecs = sel_corecs}
   581       end;
   582 
   583     fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss
   584         coiter_thmsss disc_coitersss sel_coiterssss =
   585       let
   586         val ctrs = #ctrs (nth ctr_sugars index);
   587         val discs = #discs (nth ctr_sugars index);
   588         val selss = #selss (nth ctr_sugars index);
   589         val p_ios = map SOME p_is @ [NONE];
   590         val discIs = #discIs (nth ctr_sugars index);
   591         val sel_thmss = #sel_thmss (nth ctr_sugars index);
   592         val collapses = #collapses (nth ctr_sugars index);
   593         val corec_thms = co_rec_of (nth coiter_thmsss index);
   594         val disc_corecs = co_rec_of (nth disc_coitersss index);
   595         val sel_corecss = co_rec_of (nth sel_coiterssss index);
   596       in
   597         map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses
   598           corec_thms disc_corecs sel_corecss
   599       end;
   600 
   601     fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
   602           disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
   603         p_is q_isss f_isss f_Tsss =
   604       {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
   605        nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
   606        nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
   607        nested_map_comps = map map_comp_of_bnf nested_bnfs,
   608        ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
   609          disc_coitersss sel_coiterssss};
   610   in
   611     ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
   612       co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
   613       strong_co_induct_of coinduct_thmss), lthy')
   614   end;
   615 
   616 end;