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