src/HOL/Tools/BNF/bnf_fp_util.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59642 929984c529d3
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
     1 (*  Title:      HOL/Tools/BNF/bnf_fp_util.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Author:     Martin Desharnais, TU Muenchen
     5     Author:     Stefan Berghofer, TU Muenchen
     6     Copyright   2012, 2013, 2014
     7 
     8 Shared library for the datatype and codatatype constructions.
     9 *)
    10 
    11 signature BNF_FP_UTIL =
    12 sig
    13   type fp_result =
    14     {Ts: typ list,
    15      bnfs: BNF_Def.bnf list,
    16      ctors: term list,
    17      dtors: term list,
    18      xtor_co_recs: term list,
    19      xtor_co_induct: thm,
    20      dtor_ctors: thm list,
    21      ctor_dtors: thm list,
    22      ctor_injects: thm list,
    23      dtor_injects: thm list,
    24      xtor_maps: thm list,
    25      xtor_setss: thm list list,
    26      xtor_rels: thm list,
    27      xtor_co_rec_thms: thm list,
    28      xtor_co_rec_o_maps: thm list,
    29      xtor_rel_co_induct: thm,
    30      dtor_set_inducts: thm list,
    31      xtor_co_rec_transfers: thm list}
    32 
    33   val morph_fp_result: morphism -> fp_result -> fp_result
    34 
    35   val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
    36 
    37   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
    38 
    39   val IITN: string
    40   val LevN: string
    41   val algN: string
    42   val behN: string
    43   val bisN: string
    44   val carTN: string
    45   val caseN: string
    46   val coN: string
    47   val coinductN: string
    48   val coinduct_strongN: string
    49   val corecN: string
    50   val corec_discN: string
    51   val corec_disc_iffN: string
    52   val ctorN: string
    53   val ctor_dtorN: string
    54   val ctor_exhaustN: string
    55   val ctor_induct2N: string
    56   val ctor_inductN: string
    57   val ctor_injectN: string
    58   val ctor_foldN: string
    59   val ctor_fold_o_mapN: string
    60   val ctor_fold_transferN: string
    61   val ctor_fold_uniqueN: string
    62   val ctor_mapN: string
    63   val ctor_map_uniqueN: string
    64   val ctor_recN: string
    65   val ctor_rec_o_mapN: string
    66   val ctor_rec_transferN: string
    67   val ctor_rec_uniqueN: string
    68   val ctor_relN: string
    69   val ctor_rel_inductN: string
    70   val ctor_set_inclN: string
    71   val ctor_set_set_inclN: string
    72   val dtorN: string
    73   val dtor_coinductN: string
    74   val dtor_corecN: string
    75   val dtor_corec_o_mapN: string
    76   val dtor_corec_transferN: string
    77   val dtor_corec_uniqueN: string
    78   val dtor_ctorN: string
    79   val dtor_exhaustN: string
    80   val dtor_injectN: string
    81   val dtor_mapN: string
    82   val dtor_map_coinductN: string
    83   val dtor_map_coinduct_strongN: string
    84   val dtor_map_uniqueN: string
    85   val dtor_relN: string
    86   val dtor_rel_coinductN: string
    87   val dtor_set_inclN: string
    88   val dtor_set_set_inclN: string
    89   val dtor_coinduct_strongN: string
    90   val dtor_unfoldN: string
    91   val dtor_unfold_o_mapN: string
    92   val dtor_unfold_transferN: string
    93   val dtor_unfold_uniqueN: string
    94   val exhaustN: string
    95   val colN: string
    96   val inductN: string
    97   val injectN: string
    98   val isNodeN: string
    99   val lsbisN: string
   100   val mapN: string
   101   val map_uniqueN: string
   102   val min_algN: string
   103   val morN: string
   104   val nchotomyN: string
   105   val recN: string
   106   val rel_casesN: string
   107   val rel_coinductN: string
   108   val rel_inductN: string
   109   val rel_injectN: string
   110   val rel_introsN: string
   111   val rel_distinctN: string
   112   val rel_selN: string
   113   val rvN: string
   114   val corec_selN: string
   115   val set_inclN: string
   116   val set_set_inclN: string
   117   val setN: string
   118   val simpsN: string
   119   val strTN: string
   120   val str_initN: string
   121   val sum_bdN: string
   122   val sum_bdTN: string
   123   val uniqueN: string
   124 
   125   (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *)
   126   val mk_ctor_setN: int -> string
   127   val mk_dtor_setN: int -> string
   128   val mk_dtor_set_inductN: int -> string
   129   val mk_set_inductN: int -> string
   130 
   131   val co_prefix: BNF_Util.fp_kind -> string
   132 
   133   val split_conj_thm: thm -> thm list
   134   val split_conj_prems: int -> thm -> thm
   135 
   136   val mk_sumTN: typ list -> typ
   137   val mk_sumTN_balanced: typ list -> typ
   138   val mk_tupleT_balanced: typ list -> typ
   139   val mk_sumprodT_balanced: typ list list -> typ
   140 
   141   val mk_proj: typ -> int -> int -> term
   142 
   143   val mk_convol: term * term -> term
   144   val mk_rel_prod: term -> term -> term
   145   val mk_rel_sum: term -> term -> term
   146 
   147   val Inl_const: typ -> typ -> term
   148   val Inr_const: typ -> typ -> term
   149   val mk_tuple_balanced: term list -> term
   150   val mk_tuple1_balanced: typ list -> term list -> term
   151 
   152   val mk_case_sum: term * term -> term
   153   val mk_case_sumN: term list -> term
   154   val mk_case_absumprod: typ -> term -> term list -> term list list -> term list list -> term
   155 
   156   val mk_Inl: typ -> term -> term
   157   val mk_Inr: typ -> term -> term
   158   val mk_absumprod: typ -> term -> int -> int -> term list -> term
   159 
   160   val dest_sumT: typ -> typ * typ
   161   val dest_sumTN_balanced: int -> typ -> typ list
   162   val dest_tupleT_balanced: int -> typ -> typ list
   163   val dest_absumprodT: typ -> typ -> int -> int list -> typ -> typ list list
   164 
   165   val If_const: typ -> term
   166 
   167   val mk_Field: term -> term
   168   val mk_If: term -> term -> term -> term
   169   val mk_union: term * term -> term
   170 
   171   val mk_absumprodE: thm -> int list -> thm
   172 
   173   val mk_sum_caseN: int -> int -> thm
   174   val mk_sum_caseN_balanced: int -> int -> thm
   175 
   176   val mk_sum_Cinfinite: thm list -> thm
   177   val mk_sum_card_order: thm list -> thm
   178 
   179   val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
   180     term list -> term list -> term list -> term list -> term list ->
   181     ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
   182   val mk_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
   183     term list -> term list -> term list -> term list ->
   184     ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list
   185   val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
   186     thm list -> thm list -> thm list
   187 
   188   val mk_coinduct_strong_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
   189 
   190   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
   191       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
   192     binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
   193     local_theory -> (BNF_Def.bnf list * BNF_Comp.absT_info list) * 'a
   194   val fp_antiquote_setup: binding -> theory -> theory
   195 end;
   196 
   197 structure BNF_FP_Util : BNF_FP_UTIL =
   198 struct
   199 
   200 open Ctr_Sugar
   201 open BNF_Comp
   202 open BNF_Def
   203 open BNF_Util
   204 
   205 type fp_result =
   206   {Ts: typ list,
   207    bnfs: BNF_Def.bnf list,
   208    ctors: term list,
   209    dtors: term list,
   210    xtor_co_recs: term list,
   211    xtor_co_induct: thm,
   212    dtor_ctors: thm list,
   213    ctor_dtors: thm list,
   214    ctor_injects: thm list,
   215    dtor_injects: thm list,
   216    xtor_maps: thm list,
   217    xtor_setss: thm list list,
   218    xtor_rels: thm list,
   219    xtor_co_rec_thms: thm list,
   220    xtor_co_rec_o_maps: thm list,
   221    xtor_rel_co_induct: thm,
   222    dtor_set_inducts: thm list,
   223    xtor_co_rec_transfers: thm list};
   224 
   225 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
   226     dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss,
   227     xtor_rels, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
   228     dtor_set_inducts, xtor_co_rec_transfers} =
   229   {Ts = map (Morphism.typ phi) Ts,
   230    bnfs = map (morph_bnf phi) bnfs,
   231    ctors = map (Morphism.term phi) ctors,
   232    dtors = map (Morphism.term phi) dtors,
   233    xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
   234    xtor_co_induct = Morphism.thm phi xtor_co_induct,
   235    dtor_ctors = map (Morphism.thm phi) dtor_ctors,
   236    ctor_dtors = map (Morphism.thm phi) ctor_dtors,
   237    ctor_injects = map (Morphism.thm phi) ctor_injects,
   238    dtor_injects = map (Morphism.thm phi) dtor_injects,
   239    xtor_maps = map (Morphism.thm phi) xtor_maps,
   240    xtor_setss = map (map (Morphism.thm phi)) xtor_setss,
   241    xtor_rels = map (Morphism.thm phi) xtor_rels,
   242    xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
   243    xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
   244    xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,
   245    dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts,
   246    xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers};
   247 
   248 fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   249   then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
   250     "ms")
   251   else (); Timer.startRealTimer ());
   252 
   253 val preN = "pre_"
   254 val rawN = "raw_"
   255 
   256 val coN = "co"
   257 val unN = "un"
   258 val algN = "alg"
   259 val IITN = "IITN"
   260 val foldN = "fold"
   261 val unfoldN = unN ^ foldN
   262 val uniqueN = "_unique"
   263 val transferN = "_transfer"
   264 val simpsN = "simps"
   265 val ctorN = "ctor"
   266 val dtorN = "dtor"
   267 val ctor_foldN = ctorN ^ "_" ^ foldN
   268 val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
   269 val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
   270 val ctor_fold_o_mapN = ctor_foldN ^ "_o_" ^ mapN
   271 val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
   272 val dtor_unfold_o_mapN = dtor_unfoldN ^ "_o_" ^ mapN
   273 val ctor_fold_transferN = ctor_foldN ^ transferN
   274 val dtor_unfold_transferN = dtor_unfoldN ^ transferN
   275 val ctor_mapN = ctorN ^ "_" ^ mapN
   276 val dtor_mapN = dtorN ^ "_" ^ mapN
   277 val map_uniqueN = mapN ^ uniqueN
   278 val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN
   279 val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN
   280 val min_algN = "min_alg"
   281 val morN = "mor"
   282 val bisN = "bis"
   283 val lsbisN = "lsbis"
   284 val sum_bdTN = "sbdT"
   285 val sum_bdN = "sbd"
   286 val carTN = "carT"
   287 val strTN = "strT"
   288 val isNodeN = "isNode"
   289 val LevN = "Lev"
   290 val rvN = "recover"
   291 val behN = "beh"
   292 val setN = "set"
   293 val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN
   294 val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN
   295 fun mk_set_inductN i = mk_setN i ^ "_induct"
   296 val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN
   297 
   298 val str_initN = "str_init"
   299 val recN = "rec"
   300 val corecN = coN ^ recN
   301 val ctor_recN = ctorN ^ "_" ^ recN
   302 val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN
   303 val ctor_rec_transferN = ctor_recN ^ transferN
   304 val ctor_rec_uniqueN = ctor_recN ^ uniqueN
   305 val dtor_corecN = dtorN ^ "_" ^ corecN
   306 val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN
   307 val dtor_corec_transferN = dtor_corecN ^ transferN
   308 val dtor_corec_uniqueN = dtor_corecN ^ uniqueN
   309 
   310 val ctor_dtorN = ctorN ^ "_" ^ dtorN
   311 val dtor_ctorN = dtorN ^ "_" ^ ctorN
   312 val nchotomyN = "nchotomy"
   313 val injectN = "inject"
   314 val exhaustN = "exhaust"
   315 val ctor_injectN = ctorN ^ "_" ^ injectN
   316 val ctor_exhaustN = ctorN ^ "_" ^ exhaustN
   317 val dtor_injectN = dtorN ^ "_" ^ injectN
   318 val dtor_exhaustN = dtorN ^ "_" ^ exhaustN
   319 val ctor_relN = ctorN ^ "_" ^ relN
   320 val dtor_relN = dtorN ^ "_" ^ relN
   321 val inductN = "induct"
   322 val coinductN = coN ^ inductN
   323 val ctor_inductN = ctorN ^ "_" ^ inductN
   324 val ctor_induct2N = ctor_inductN ^ "2"
   325 val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
   326 val dtor_coinductN = dtorN ^ "_" ^ coinductN
   327 val coinduct_strongN = coinductN ^ "_strong"
   328 val dtor_map_coinduct_strongN = dtor_mapN ^ "_" ^ coinduct_strongN
   329 val dtor_coinduct_strongN = dtorN ^ "_" ^ coinduct_strongN
   330 val colN = "col"
   331 val set_inclN = "set_incl"
   332 val ctor_set_inclN = ctorN ^ "_" ^ set_inclN
   333 val dtor_set_inclN = dtorN ^ "_" ^ set_inclN
   334 val set_set_inclN = "set_set_incl"
   335 val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN
   336 val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN
   337 
   338 val caseN = "case"
   339 val discN = "disc"
   340 val corec_discN = corecN ^ "_" ^ discN
   341 val iffN = "_iff"
   342 val corec_disc_iffN = corec_discN ^ iffN
   343 val distinctN = "distinct"
   344 val rel_distinctN = relN ^ "_" ^ distinctN
   345 val injectN = "inject"
   346 val rel_casesN = relN ^ "_cases"
   347 val rel_injectN = relN ^ "_" ^ injectN
   348 val rel_introsN = relN ^ "_intros"
   349 val rel_coinductN = relN ^ "_" ^ coinductN
   350 val rel_selN = relN ^ "_sel"
   351 val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN
   352 val rel_inductN = relN ^ "_" ^ inductN
   353 val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN
   354 val selN = "sel"
   355 val corec_selN = corecN ^ "_" ^ selN
   356 
   357 fun co_prefix fp = case_fp fp "" "co";
   358 
   359 fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
   360 
   361 val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT;
   362 
   363 fun dest_tupleT_balanced 0 @{typ unit} = []
   364   | dest_tupleT_balanced n T = Balanced_Tree.dest HOLogic.dest_prodT n T;
   365 
   366 fun dest_absumprodT absT repT n ms =
   367   map2 dest_tupleT_balanced ms o dest_sumTN_balanced n o mk_repT absT repT;
   368 
   369 val mk_sumTN = Library.foldr1 mk_sumT;
   370 val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
   371 
   372 fun mk_tupleT_balanced [] = HOLogic.unitT
   373   | mk_tupleT_balanced Ts = Balanced_Tree.make HOLogic.mk_prodT Ts;
   374 
   375 val mk_sumprodT_balanced = mk_sumTN_balanced o map mk_tupleT_balanced;
   376 
   377 fun mk_proj T n k =
   378   let val (binders, _) = strip_typeN n T in
   379     fold_rev (fn T => fn t => Abs (Name.uu, T, t)) binders (Bound (n - k - 1))
   380   end;
   381 
   382 fun mk_convol (f, g) =
   383   let
   384     val (fU, fTU) = `range_type (fastype_of f);
   385     val ((gT, gU), gTU) = `dest_funT (fastype_of g);
   386     val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
   387   in Const (@{const_name convol}, convolT) $ f $ g end;
   388 
   389 fun mk_rel_prod R S =
   390   let
   391     val ((A1, A2), RT) = `dest_pred2T (fastype_of R);
   392     val ((B1, B2), ST) = `dest_pred2T (fastype_of S);
   393     val rel_prodT = RT --> ST --> mk_pred2T (HOLogic.mk_prodT (A1, B1)) (HOLogic.mk_prodT (A2, B2));
   394   in Const (@{const_name rel_prod}, rel_prodT) $ R $ S end;
   395 
   396 fun mk_rel_sum R S =
   397   let
   398     val ((A1, A2), RT) = `dest_pred2T (fastype_of R);
   399     val ((B1, B2), ST) = `dest_pred2T (fastype_of S);
   400     val rel_sumT = RT --> ST --> mk_pred2T (mk_sumT (A1, B1)) (mk_sumT (A2, B2));
   401   in Const (@{const_name rel_sum}, rel_sumT) $ R $ S end;
   402 
   403 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
   404 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
   405 
   406 fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
   407 fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
   408 
   409 fun mk_prod1 bound_Ts (t, u) =
   410   HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
   411 
   412 fun mk_tuple1_balanced _ [] = HOLogic.unit
   413   | mk_tuple1_balanced bound_Ts ts = Balanced_Tree.make (mk_prod1 bound_Ts) ts;
   414 
   415 val mk_tuple_balanced = mk_tuple1_balanced [];
   416 
   417 fun mk_absumprod absT abs0 n k ts =
   418   let val abs = mk_abs absT abs0;
   419   in abs $ Sum_Tree.mk_inj (domain_type (fastype_of abs)) n k (mk_tuple_balanced ts) end;
   420 
   421 fun mk_case_sum (f, g) =
   422   let
   423     val (fT, T') = dest_funT (fastype_of f);
   424     val (gT, _) = dest_funT (fastype_of g);
   425   in
   426     Sum_Tree.mk_sumcase fT gT T' f g
   427   end;
   428 
   429 val mk_case_sumN = Library.foldr1 mk_case_sum;
   430 val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum;
   431 
   432 fun mk_tupled_fun f x xs =
   433   if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
   434 
   435 fun mk_case_absumprod absT rep fs xss xss' =
   436   HOLogic.mk_comp (mk_case_sumN_balanced (@{map 3} mk_tupled_fun fs (map mk_tuple_balanced xss) xss'),
   437     mk_rep absT rep);
   438 
   439 fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
   440 fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
   441 
   442 fun mk_Field r =
   443   let val T = fst (dest_relT (fastype_of r));
   444   in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
   445 
   446 val mk_union = HOLogic.mk_binop @{const_name sup};
   447 
   448 (*dangerous; use with monotonic, converging functions only!*)
   449 fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
   450 
   451 (* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *)
   452 fun split_conj_thm th =
   453   ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
   454 
   455 fun split_conj_prems limit th =
   456   let
   457     fun split n i th =
   458       if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
   459   in split limit 1 th end;
   460 
   461 fun mk_obj_sumEN_balanced n =
   462   Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
   463     (replicate n asm_rl);
   464 
   465 fun mk_tupled_allIN_balanced 0 = @{thm unit_all_impI}
   466   | mk_tupled_allIN_balanced n =
   467     let
   468       val (tfrees, _) = BNF_Util.mk_TFrees n @{context};
   469       val T = mk_tupleT_balanced tfrees;
   470     in
   471       @{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
   472       |> Drule.instantiate' [SOME (Thm.global_ctyp_of @{theory} T)] []
   473       |> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
   474       |> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
   475       |> Thm.varifyT_global
   476     end;
   477 
   478 fun mk_absumprodE type_definition ms =
   479   let val n = length ms in
   480     mk_obj_sumEN_balanced n OF map mk_tupled_allIN_balanced ms RS
   481       (type_definition RS @{thm type_copy_obj_one_point_absE})
   482   end;
   483 
   484 fun mk_sum_caseN 1 1 = refl
   485   | mk_sum_caseN _ 1 = @{thm sum.case(1)}
   486   | mk_sum_caseN 2 2 = @{thm sum.case(2)}
   487   | mk_sum_caseN n k = trans OF [@{thm case_sum_step(2)}, mk_sum_caseN (n - 1) (k - 1)];
   488 
   489 fun mk_sum_step base step thm =
   490   if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm];
   491 
   492 fun mk_sum_caseN_balanced 1 1 = refl
   493   | mk_sum_caseN_balanced n k =
   494     Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)},
   495       right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k;
   496 
   497 fun mk_sum_Cinfinite [thm] = thm
   498   | mk_sum_Cinfinite (thm :: thms) = @{thm Cinfinite_csum_weak} OF [thm, mk_sum_Cinfinite thms];
   499 
   500 fun mk_sum_card_order [thm] = thm
   501   | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
   502 
   503 fun mk_xtor_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
   504   let
   505     val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
   506     val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
   507     fun mk_xtor fp' xtor x = if fp = fp' then xtor $ x else x;
   508     val dtor = mk_xtor Greatest_FP;
   509     val ctor = mk_xtor Least_FP;
   510     fun flip f x y = if fp = Greatest_FP then f y x else f x y;
   511 
   512     fun mk_prem pre_relphi phi x y xtor xtor' =
   513       HOLogic.mk_Trueprop (list_all_free [x, y] (flip (curry HOLogic.mk_imp)
   514         (pre_relphi $ (dtor xtor x) $ (dtor xtor' y)) (phi $ (ctor xtor x) $ (ctor xtor' y))));
   515     val prems = @{map 6} mk_prem pre_relphis pre_phis xs ys xtors xtor's;
   516 
   517     val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   518       (map2 (flip mk_leq) relphis pre_phis));
   519   in
   520     Goal.prove_sorry lthy (map (fst o dest_Free) (phis @ pre_phis)) prems concl tac
   521     |> Thm.close_derivation
   522     |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
   523   end;
   524 
   525 fun mk_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy =
   526   let
   527     val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_iphis)) pre_rels;
   528     val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
   529     fun flip f x y = if fp = Greatest_FP then f y x else f x y;
   530 
   531     val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_ophis;
   532     fun mk_transfer relphi pre_phi un_fold un_fold' =
   533       fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold';
   534     val transfers = @{map 4} mk_transfer relphis pre_ophis un_folds un_folds';
   535 
   536     val goal = fold_rev Logic.all (phis @ pre_ophis)
   537       (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
   538   in
   539     Goal.prove_sorry lthy [] [] goal tac
   540     |> Thm.close_derivation
   541     |> split_conj_thm
   542   end;
   543 
   544 fun mk_xtor_un_fold_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps
   545     map_cong0s =
   546   let
   547     val n = length sym_map_comps;
   548     val rewrite_comp_comp2 = case_fp fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2};
   549     val rewrite_comp_comp = case_fp fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
   550     val map_cong_passive_args1 = replicate m (case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   551     val map_cong_active_args1 = replicate n (if is_rec
   552       then case_fp fp @{thm convol_o} @{thm o_case_sum} RS fun_cong
   553       else refl);
   554     val map_cong_passive_args2 = replicate m (case_fp fp @{thm comp_id} @{thm id_comp} RS fun_cong);
   555     val map_cong_active_args2 = replicate n (if is_rec
   556       then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id}
   557       else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   558     fun mk_map_congs passive active =
   559       map (fn thm => thm OF (passive @ active) RS @{thm ext}) map_cong0s;
   560     val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
   561     val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;
   562 
   563     fun mk_rewrites map_congs = map2 (fn sym_map_comp => fn map_cong =>
   564       mk_trans sym_map_comp map_cong RS rewrite_comp_comp) sym_map_comps map_congs;
   565     val rewrite1s = mk_rewrites map_cong1s;
   566     val rewrite2s = mk_rewrites map_cong2s;
   567     val unique_prems =
   568       @{map 4} (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 =>
   569         mk_trans (rewrite_comp_comp2 OF [xtor_map, un_fold])
   570           (mk_trans rewrite1 (mk_sym rewrite2)))
   571       xtor_maps xtor_un_folds rewrite1s rewrite2s;
   572   in
   573     split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
   574   end;
   575 
   576 fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
   577   let
   578     val n = Thm.nprems_of coind;
   579     val m = Thm.nprems_of (hd rel_monos) - n;
   580     fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
   581       |> apply2 (Thm.cterm_of ctxt);
   582     val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
   583     fun mk_unfold rel_eq rel_mono =
   584       let
   585         val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
   586         val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
   587       in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS eqTrueI end;
   588     val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
   589       imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
   590   in
   591     Thm.instantiate ([], insts) coind
   592     |> unfold_thms ctxt unfolds
   593   end;
   594 
   595 fun fp_bnf construct_fp bs resBs Ds0 fp_eqs lthy =
   596   let
   597     val time = time lthy;
   598     val timer = time (Timer.startRealTimer ());
   599 
   600     val nn = length fp_eqs;
   601     val (Xs, rhsXs) = split_list fp_eqs;
   602 
   603     fun flatten_tyargs Ass =
   604       subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
   605 
   606     fun raw_qualify base_b =
   607       let val (_, qs, n) = Binding.dest base_b;
   608       in
   609         Binding.prefix_name rawN
   610         #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
   611         #> Binding.conceal
   612       end;
   613 
   614     val ((bnfs, (deadss, livess)), accum) =
   615       apfst (apsnd split_list o split_list)
   616         (@{fold_map 2}
   617           (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
   618           ((empty_comp_cache, empty_unfolds), lthy));
   619 
   620     fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
   621       #> Binding.conceal;
   622 
   623     val Ass = map (map dest_TFree) livess;
   624     val Ds' = fold (fold Term.add_tfreesT) deadss [];
   625     val Ds = union (op =) Ds' Ds0;
   626     val missing = resBs |> fold (subtract (op =)) (Ds' :: Ass);
   627     val (dead_phantoms, live_phantoms) = List.partition (member (op =) Ds0) missing;
   628     val resBs' = resBs |> fold (subtract (op =)) [dead_phantoms, Ds];
   629 
   630     val timer = time (timer "Construction of BNFs");
   631 
   632     val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) =
   633       normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum;
   634 
   635     val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
   636 
   637     fun pre_qualify b = Binding.qualify false (Binding.name_of b)
   638       #> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
   639 
   640     val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
   641       @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
   642         bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy'
   643       |>> split_list
   644       |>> apsnd split_list;
   645 
   646     val timer = time (timer "Normalization & sealing of BNFs");
   647 
   648     val res = construct_fp bs resBs (map TFree dead_phantoms, deadss) pre_bnfs absT_infos lthy'';
   649 
   650     val timer = time (timer "FP construction in total");
   651   in
   652     timer; ((pre_bnfs, absT_infos), res)
   653   end;
   654 
   655 fun fp_antiquote_setup binding =
   656   Thy_Output.antiquotation binding (Args.type_name {proper = true, strict = true})
   657     (fn {source = src, context = ctxt, ...} => fn fcT_name =>
   658        (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
   659          NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
   660        | SOME {T = T0, ctrs = ctrs0, ...} =>
   661          let
   662            val freezeT = Term.map_atyps (fn TVar ((s, _), S) => TFree (s, S) | T => T);
   663 
   664            val T = freezeT T0;
   665            val ctrs = map (Term.map_types freezeT) ctrs0;
   666 
   667            val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
   668            fun pretty_ctr ctr =
   669              Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr ::
   670                map pretty_typ_bracket (binder_types (fastype_of ctr))));
   671            val pretty_co_datatype =
   672              Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 ::
   673                Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 ::
   674                flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs)));
   675          in
   676            Thy_Output.output ctxt
   677              (Thy_Output.maybe_pretty_source (K (K pretty_co_datatype)) ctxt src [()])
   678          end));
   679 
   680 end;