src/HOL/BNF/Tools/bnf_def.ML
changeset 55058 4e700eb471d4
parent 55057 6b0fcbeebaba
child 55059 ef2e0fb783c6
     1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Jan 20 18:24:55 2014 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,1393 +0,0 @@
     1.4 -(*  Title:      HOL/BNF/Tools/bnf_def.ML
     1.5 -    Author:     Dmitriy Traytel, TU Muenchen
     1.6 -    Author:     Jasmin Blanchette, TU Muenchen
     1.7 -    Copyright   2012
     1.8 -
     1.9 -Definition of bounded natural functors.
    1.10 -*)
    1.11 -
    1.12 -signature BNF_DEF =
    1.13 -sig
    1.14 -  type bnf
    1.15 -  type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
    1.16 -
    1.17 -  val morph_bnf: morphism -> bnf -> bnf
    1.18 -  val eq_bnf: bnf * bnf -> bool
    1.19 -  val bnf_of: Proof.context -> string -> bnf option
    1.20 -  val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
    1.21 -
    1.22 -  val name_of_bnf: bnf -> binding
    1.23 -  val T_of_bnf: bnf -> typ
    1.24 -  val live_of_bnf: bnf -> int
    1.25 -  val lives_of_bnf: bnf -> typ list
    1.26 -  val dead_of_bnf: bnf -> int
    1.27 -  val deads_of_bnf: bnf -> typ list
    1.28 -  val nwits_of_bnf: bnf -> int
    1.29 -
    1.30 -  val mapN: string
    1.31 -  val relN: string
    1.32 -  val setN: string
    1.33 -  val mk_setN: int -> string
    1.34 -  val mk_witN: int -> string
    1.35 -
    1.36 -  val map_of_bnf: bnf -> term
    1.37 -  val sets_of_bnf: bnf -> term list
    1.38 -  val rel_of_bnf: bnf -> term
    1.39 -
    1.40 -  val mk_T_of_bnf: typ list -> typ list -> bnf -> typ
    1.41 -  val mk_bd_of_bnf: typ list -> typ list -> bnf -> term
    1.42 -  val mk_map_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    1.43 -  val mk_rel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    1.44 -  val mk_sets_of_bnf: typ list list -> typ list list -> bnf -> term list
    1.45 -  val mk_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list
    1.46 -
    1.47 -  val bd_Card_order_of_bnf: bnf -> thm
    1.48 -  val bd_Cinfinite_of_bnf: bnf -> thm
    1.49 -  val bd_Cnotzero_of_bnf: bnf -> thm
    1.50 -  val bd_card_order_of_bnf: bnf -> thm
    1.51 -  val bd_cinfinite_of_bnf: bnf -> thm
    1.52 -  val collect_set_map_of_bnf: bnf -> thm
    1.53 -  val in_bd_of_bnf: bnf -> thm
    1.54 -  val in_cong_of_bnf: bnf -> thm
    1.55 -  val in_mono_of_bnf: bnf -> thm
    1.56 -  val in_rel_of_bnf: bnf -> thm
    1.57 -  val map_comp0_of_bnf: bnf -> thm
    1.58 -  val map_comp_of_bnf: bnf -> thm
    1.59 -  val map_cong0_of_bnf: bnf -> thm
    1.60 -  val map_cong_of_bnf: bnf -> thm
    1.61 -  val map_def_of_bnf: bnf -> thm
    1.62 -  val map_id0_of_bnf: bnf -> thm
    1.63 -  val map_id_of_bnf: bnf -> thm
    1.64 -  val map_transfer_of_bnf: bnf -> thm
    1.65 -  val le_rel_OO_of_bnf: bnf -> thm
    1.66 -  val rel_def_of_bnf: bnf -> thm
    1.67 -  val rel_Grp_of_bnf: bnf -> thm
    1.68 -  val rel_OO_of_bnf: bnf -> thm
    1.69 -  val rel_OO_Grp_of_bnf: bnf -> thm
    1.70 -  val rel_cong_of_bnf: bnf -> thm
    1.71 -  val rel_conversep_of_bnf: bnf -> thm
    1.72 -  val rel_mono_of_bnf: bnf -> thm
    1.73 -  val rel_mono_strong_of_bnf: bnf -> thm
    1.74 -  val rel_eq_of_bnf: bnf -> thm
    1.75 -  val rel_flip_of_bnf: bnf -> thm
    1.76 -  val set_bd_of_bnf: bnf -> thm list
    1.77 -  val set_defs_of_bnf: bnf -> thm list
    1.78 -  val set_map0_of_bnf: bnf -> thm list
    1.79 -  val set_map_of_bnf: bnf -> thm list
    1.80 -  val wit_thms_of_bnf: bnf -> thm list
    1.81 -  val wit_thmss_of_bnf: bnf -> thm list list
    1.82 -
    1.83 -  val mk_map: int -> typ list -> typ list -> term -> term
    1.84 -  val mk_rel: int -> typ list -> typ list -> term -> term
    1.85 -  val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term
    1.86 -  val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term
    1.87 -  val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
    1.88 -  val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list ->
    1.89 -    'a list
    1.90 -
    1.91 -  val mk_witness: int list * term -> thm list -> nonemptiness_witness
    1.92 -  val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
    1.93 -  val wits_of_bnf: bnf -> nonemptiness_witness list
    1.94 -
    1.95 -  val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
    1.96 -
    1.97 -  datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
    1.98 -  datatype fact_policy = Dont_Note | Note_Some | Note_All
    1.99 -
   1.100 -  val bnf_note_all: bool Config.T
   1.101 -  val bnf_timing: bool Config.T
   1.102 -  val user_policy: fact_policy -> Proof.context -> fact_policy
   1.103 -  val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context ->
   1.104 -    Proof.context
   1.105 -
   1.106 -  val print_bnfs: Proof.context -> unit
   1.107 -  val prepare_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
   1.108 -    (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option ->
   1.109 -    binding -> binding -> binding list ->
   1.110 -    (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
   1.111 -    string * term list *
   1.112 -    ((thm list -> {context: Proof.context, prems: thm list} -> tactic) option * term list list) *
   1.113 -    ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
   1.114 -    local_theory * thm list
   1.115 -
   1.116 -  val define_bnf_consts: const_policy -> fact_policy -> typ list option ->
   1.117 -    binding -> binding -> binding list ->
   1.118 -    (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
   1.119 -      ((typ list * typ list * typ list * typ) *
   1.120 -       (term * term list * term * (int list * term) list * term) *
   1.121 -       (thm * thm list * thm * thm list * thm) *
   1.122 -       ((typ list -> typ list -> typ list -> term) *
   1.123 -        (typ list -> typ list -> term -> term) *
   1.124 -        (typ list -> typ list -> typ -> typ) *
   1.125 -        (typ list -> typ list -> typ list -> term) *
   1.126 -        (typ list -> typ list -> typ list -> term))) * local_theory
   1.127 -
   1.128 -  val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
   1.129 -    ({prems: thm list, context: Proof.context} -> tactic) list ->
   1.130 -    ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
   1.131 -    binding -> binding list ->
   1.132 -    (((((binding * typ) * term) * term list) * term) * term list) * term option ->
   1.133 -    local_theory -> bnf * local_theory
   1.134 -end;
   1.135 -
   1.136 -structure BNF_Def : BNF_DEF =
   1.137 -struct
   1.138 -
   1.139 -open BNF_Util
   1.140 -open BNF_Tactics
   1.141 -open BNF_Def_Tactics
   1.142 -
   1.143 -val fundefcong_attrs = @{attributes [fundef_cong]};
   1.144 -
   1.145 -type axioms = {
   1.146 -  map_id0: thm,
   1.147 -  map_comp0: thm,
   1.148 -  map_cong0: thm,
   1.149 -  set_map0: thm list,
   1.150 -  bd_card_order: thm,
   1.151 -  bd_cinfinite: thm,
   1.152 -  set_bd: thm list,
   1.153 -  le_rel_OO: thm,
   1.154 -  rel_OO_Grp: thm
   1.155 -};
   1.156 -
   1.157 -fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), le_rel_OO), rel) =
   1.158 -  {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o,
   1.159 -   bd_cinfinite = cinf, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel};
   1.160 -
   1.161 -fun dest_cons [] = raise List.Empty
   1.162 -  | dest_cons (x :: xs) = (x, xs);
   1.163 -
   1.164 -fun mk_axioms n thms = thms
   1.165 -  |> map the_single
   1.166 -  |> dest_cons
   1.167 -  ||>> dest_cons
   1.168 -  ||>> dest_cons
   1.169 -  ||>> chop n
   1.170 -  ||>> dest_cons
   1.171 -  ||>> dest_cons
   1.172 -  ||>> chop n
   1.173 -  ||>> dest_cons
   1.174 -  ||> the_single
   1.175 -  |> mk_axioms';
   1.176 -
   1.177 -fun zip_axioms mid mcomp mcong smap bdco bdinf sbd le_rel_OO rel =
   1.178 -  [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel];
   1.179 -
   1.180 -fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
   1.181 -  le_rel_OO, rel_OO_Grp} =
   1.182 -  zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd le_rel_OO
   1.183 -    rel_OO_Grp;
   1.184 -
   1.185 -fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
   1.186 -  le_rel_OO, rel_OO_Grp} =
   1.187 -  {map_id0 = f map_id0,
   1.188 -    map_comp0 = f map_comp0,
   1.189 -    map_cong0 = f map_cong0,
   1.190 -    set_map0 = map f set_map0,
   1.191 -    bd_card_order = f bd_card_order,
   1.192 -    bd_cinfinite = f bd_cinfinite,
   1.193 -    set_bd = map f set_bd,
   1.194 -    le_rel_OO = f le_rel_OO,
   1.195 -    rel_OO_Grp = f rel_OO_Grp};
   1.196 -
   1.197 -val morph_axioms = map_axioms o Morphism.thm;
   1.198 -
   1.199 -type defs = {
   1.200 -  map_def: thm,
   1.201 -  set_defs: thm list,
   1.202 -  rel_def: thm
   1.203 -}
   1.204 -
   1.205 -fun mk_defs map sets rel = {map_def = map, set_defs = sets, rel_def = rel};
   1.206 -
   1.207 -fun map_defs f {map_def, set_defs, rel_def} =
   1.208 -  {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def};
   1.209 -
   1.210 -val morph_defs = map_defs o Morphism.thm;
   1.211 -
   1.212 -type facts = {
   1.213 -  bd_Card_order: thm,
   1.214 -  bd_Cinfinite: thm,
   1.215 -  bd_Cnotzero: thm,
   1.216 -  collect_set_map: thm lazy,
   1.217 -  in_bd: thm lazy,
   1.218 -  in_cong: thm lazy,
   1.219 -  in_mono: thm lazy,
   1.220 -  in_rel: thm lazy,
   1.221 -  map_comp: thm lazy,
   1.222 -  map_cong: thm lazy,
   1.223 -  map_id: thm lazy,
   1.224 -  map_transfer: thm lazy,
   1.225 -  rel_eq: thm lazy,
   1.226 -  rel_flip: thm lazy,
   1.227 -  set_map: thm lazy list,
   1.228 -  rel_cong: thm lazy,
   1.229 -  rel_mono: thm lazy,
   1.230 -  rel_mono_strong: thm lazy,
   1.231 -  rel_Grp: thm lazy,
   1.232 -  rel_conversep: thm lazy,
   1.233 -  rel_OO: thm lazy
   1.234 -};
   1.235 -
   1.236 -fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
   1.237 -    map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono
   1.238 -    rel_mono_strong rel_Grp rel_conversep rel_OO = {
   1.239 -  bd_Card_order = bd_Card_order,
   1.240 -  bd_Cinfinite = bd_Cinfinite,
   1.241 -  bd_Cnotzero = bd_Cnotzero,
   1.242 -  collect_set_map = collect_set_map,
   1.243 -  in_bd = in_bd,
   1.244 -  in_cong = in_cong,
   1.245 -  in_mono = in_mono,
   1.246 -  in_rel = in_rel,
   1.247 -  map_comp = map_comp,
   1.248 -  map_cong = map_cong,
   1.249 -  map_id = map_id,
   1.250 -  map_transfer = map_transfer,
   1.251 -  rel_eq = rel_eq,
   1.252 -  rel_flip = rel_flip,
   1.253 -  set_map = set_map,
   1.254 -  rel_cong = rel_cong,
   1.255 -  rel_mono = rel_mono,
   1.256 -  rel_mono_strong = rel_mono_strong,
   1.257 -  rel_Grp = rel_Grp,
   1.258 -  rel_conversep = rel_conversep,
   1.259 -  rel_OO = rel_OO};
   1.260 -
   1.261 -fun map_facts f {
   1.262 -  bd_Card_order,
   1.263 -  bd_Cinfinite,
   1.264 -  bd_Cnotzero,
   1.265 -  collect_set_map,
   1.266 -  in_bd,
   1.267 -  in_cong,
   1.268 -  in_mono,
   1.269 -  in_rel,
   1.270 -  map_comp,
   1.271 -  map_cong,
   1.272 -  map_id,
   1.273 -  map_transfer,
   1.274 -  rel_eq,
   1.275 -  rel_flip,
   1.276 -  set_map,
   1.277 -  rel_cong,
   1.278 -  rel_mono,
   1.279 -  rel_mono_strong,
   1.280 -  rel_Grp,
   1.281 -  rel_conversep,
   1.282 -  rel_OO} =
   1.283 -  {bd_Card_order = f bd_Card_order,
   1.284 -    bd_Cinfinite = f bd_Cinfinite,
   1.285 -    bd_Cnotzero = f bd_Cnotzero,
   1.286 -    collect_set_map = Lazy.map f collect_set_map,
   1.287 -    in_bd = Lazy.map f in_bd,
   1.288 -    in_cong = Lazy.map f in_cong,
   1.289 -    in_mono = Lazy.map f in_mono,
   1.290 -    in_rel = Lazy.map f in_rel,
   1.291 -    map_comp = Lazy.map f map_comp,
   1.292 -    map_cong = Lazy.map f map_cong,
   1.293 -    map_id = Lazy.map f map_id,
   1.294 -    map_transfer = Lazy.map f map_transfer,
   1.295 -    rel_eq = Lazy.map f rel_eq,
   1.296 -    rel_flip = Lazy.map f rel_flip,
   1.297 -    set_map = map (Lazy.map f) set_map,
   1.298 -    rel_cong = Lazy.map f rel_cong,
   1.299 -    rel_mono = Lazy.map f rel_mono,
   1.300 -    rel_mono_strong = Lazy.map f rel_mono_strong,
   1.301 -    rel_Grp = Lazy.map f rel_Grp,
   1.302 -    rel_conversep = Lazy.map f rel_conversep,
   1.303 -    rel_OO = Lazy.map f rel_OO};
   1.304 -
   1.305 -val morph_facts = map_facts o Morphism.thm;
   1.306 -
   1.307 -type nonemptiness_witness = {
   1.308 -  I: int list,
   1.309 -  wit: term,
   1.310 -  prop: thm list
   1.311 -};
   1.312 -
   1.313 -fun mk_witness (I, wit) prop = {I = I, wit = wit, prop = prop};
   1.314 -fun map_witness f g {I, wit, prop} = {I = I, wit = f wit, prop = map g prop};
   1.315 -fun morph_witness phi = map_witness (Morphism.term phi) (Morphism.thm phi);
   1.316 -
   1.317 -datatype bnf = BNF of {
   1.318 -  name: binding,
   1.319 -  T: typ,
   1.320 -  live: int,
   1.321 -  lives: typ list, (*source type variables of map*)
   1.322 -  lives': typ list, (*target type variables of map*)
   1.323 -  dead: int,
   1.324 -  deads: typ list,
   1.325 -  map: term,
   1.326 -  sets: term list,
   1.327 -  bd: term,
   1.328 -  axioms: axioms,
   1.329 -  defs: defs,
   1.330 -  facts: facts,
   1.331 -  nwits: int,
   1.332 -  wits: nonemptiness_witness list,
   1.333 -  rel: term
   1.334 -};
   1.335 -
   1.336 -(* getters *)
   1.337 -
   1.338 -fun rep_bnf (BNF bnf) = bnf;
   1.339 -val name_of_bnf = #name o rep_bnf;
   1.340 -val T_of_bnf = #T o rep_bnf;
   1.341 -fun mk_T_of_bnf Ds Ts bnf =
   1.342 -  let val bnf_rep = rep_bnf bnf
   1.343 -  in Term.typ_subst_atomic ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)) (#T bnf_rep) end;
   1.344 -val live_of_bnf = #live o rep_bnf;
   1.345 -val lives_of_bnf = #lives o rep_bnf;
   1.346 -val dead_of_bnf = #dead o rep_bnf;
   1.347 -val deads_of_bnf = #deads o rep_bnf;
   1.348 -val axioms_of_bnf = #axioms o rep_bnf;
   1.349 -val facts_of_bnf = #facts o rep_bnf;
   1.350 -val nwits_of_bnf = #nwits o rep_bnf;
   1.351 -val wits_of_bnf = #wits o rep_bnf;
   1.352 -
   1.353 -fun flatten_type_args_of_bnf bnf dead_x xs =
   1.354 -  let
   1.355 -    val Type (_, Ts) = T_of_bnf bnf;
   1.356 -    val lives = lives_of_bnf bnf;
   1.357 -    val deads = deads_of_bnf bnf;
   1.358 -  in
   1.359 -    permute_like (op =) (deads @ lives) Ts (replicate (length deads) dead_x @ xs)
   1.360 -  end;
   1.361 -
   1.362 -(*terms*)
   1.363 -val map_of_bnf = #map o rep_bnf;
   1.364 -val sets_of_bnf = #sets o rep_bnf;
   1.365 -fun mk_map_of_bnf Ds Ts Us bnf =
   1.366 -  let val bnf_rep = rep_bnf bnf;
   1.367 -  in
   1.368 -    Term.subst_atomic_types
   1.369 -      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#map bnf_rep)
   1.370 -  end;
   1.371 -fun mk_sets_of_bnf Dss Tss bnf =
   1.372 -  let val bnf_rep = rep_bnf bnf;
   1.373 -  in
   1.374 -    map2 (fn (Ds, Ts) => Term.subst_atomic_types
   1.375 -      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts))) (Dss ~~ Tss) (#sets bnf_rep)
   1.376 -  end;
   1.377 -val bd_of_bnf = #bd o rep_bnf;
   1.378 -fun mk_bd_of_bnf Ds Ts bnf =
   1.379 -  let val bnf_rep = rep_bnf bnf;
   1.380 -  in Term.subst_atomic_types ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)) (#bd bnf_rep) end;
   1.381 -fun mk_wits_of_bnf Dss Tss bnf =
   1.382 -  let
   1.383 -    val bnf_rep = rep_bnf bnf;
   1.384 -    val wits = map (fn x => (#I x, #wit x)) (#wits bnf_rep);
   1.385 -  in
   1.386 -    map2 (fn (Ds, Ts) => apsnd (Term.subst_atomic_types
   1.387 -      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)))) (Dss ~~ Tss) wits
   1.388 -  end;
   1.389 -val rel_of_bnf = #rel o rep_bnf;
   1.390 -fun mk_rel_of_bnf Ds Ts Us bnf =
   1.391 -  let val bnf_rep = rep_bnf bnf;
   1.392 -  in
   1.393 -    Term.subst_atomic_types
   1.394 -      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#rel bnf_rep)
   1.395 -  end;
   1.396 -
   1.397 -(*thms*)
   1.398 -val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
   1.399 -val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf;
   1.400 -val bd_Card_order_of_bnf = #bd_Card_order o #facts o rep_bnf;
   1.401 -val bd_Cinfinite_of_bnf = #bd_Cinfinite o #facts o rep_bnf;
   1.402 -val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf;
   1.403 -val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf;
   1.404 -val in_bd_of_bnf = Lazy.force o #in_bd o #facts o rep_bnf;
   1.405 -val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
   1.406 -val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
   1.407 -val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
   1.408 -val map_def_of_bnf = #map_def o #defs o rep_bnf;
   1.409 -val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
   1.410 -val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
   1.411 -val map_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf;
   1.412 -val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf;
   1.413 -val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
   1.414 -val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
   1.415 -val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
   1.416 -val le_rel_OO_of_bnf = #le_rel_OO o #axioms o rep_bnf;
   1.417 -val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
   1.418 -val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
   1.419 -val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
   1.420 -val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
   1.421 -val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
   1.422 -val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf;
   1.423 -val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
   1.424 -val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
   1.425 -val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
   1.426 -val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
   1.427 -val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
   1.428 -val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
   1.429 -val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
   1.430 -val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf;
   1.431 -val wit_thms_of_bnf = maps #prop o wits_of_bnf;
   1.432 -val wit_thmss_of_bnf = map #prop o wits_of_bnf;
   1.433 -
   1.434 -fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel =
   1.435 -  BNF {name = name, T = T,
   1.436 -       live = live, lives = lives, lives' = lives', dead = dead, deads = deads,
   1.437 -       map = map, sets = sets, bd = bd,
   1.438 -       axioms = axioms, defs = defs, facts = facts,
   1.439 -       nwits = length wits, wits = wits, rel = rel};
   1.440 -
   1.441 -fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
   1.442 -  dead = dead, deads = deads, map = map, sets = sets, bd = bd,
   1.443 -  axioms = axioms, defs = defs, facts = facts,
   1.444 -  nwits = nwits, wits = wits, rel = rel}) =
   1.445 -  BNF {name = Morphism.binding phi name, T = Morphism.typ phi T,
   1.446 -    live = live, lives = List.map (Morphism.typ phi) lives,
   1.447 -    lives' = List.map (Morphism.typ phi) lives',
   1.448 -    dead = dead, deads = List.map (Morphism.typ phi) deads,
   1.449 -    map = Morphism.term phi map, sets = List.map (Morphism.term phi) sets,
   1.450 -    bd = Morphism.term phi bd,
   1.451 -    axioms = morph_axioms phi axioms,
   1.452 -    defs = morph_defs phi defs,
   1.453 -    facts = morph_facts phi facts,
   1.454 -    nwits = nwits,
   1.455 -    wits = List.map (morph_witness phi) wits,
   1.456 -    rel = Morphism.term phi rel};
   1.457 -
   1.458 -fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...},
   1.459 -  BNF {T = T2, live = live2, dead = dead2, ...}) =
   1.460 -  Type.could_unify (T1, T2) andalso live1 = live2 andalso dead1 = dead2;
   1.461 -
   1.462 -structure Data = Generic_Data
   1.463 -(
   1.464 -  type T = bnf Symtab.table;
   1.465 -  val empty = Symtab.empty;
   1.466 -  val extend = I;
   1.467 -  val merge = Symtab.merge eq_bnf;
   1.468 -);
   1.469 -
   1.470 -fun bnf_of ctxt =
   1.471 -  Symtab.lookup (Data.get (Context.Proof ctxt))
   1.472 -  #> Option.map (morph_bnf (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
   1.473 -
   1.474 -
   1.475 -(* Utilities *)
   1.476 -
   1.477 -fun normalize_set insts instA set =
   1.478 -  let
   1.479 -    val (T, T') = dest_funT (fastype_of set);
   1.480 -    val A = fst (Term.dest_TVar (HOLogic.dest_setT T'));
   1.481 -    val params = Term.add_tvar_namesT T [];
   1.482 -  in Term.subst_TVars ((A :: params) ~~ (instA :: insts)) set end;
   1.483 -
   1.484 -fun normalize_rel ctxt instTs instA instB rel =
   1.485 -  let
   1.486 -    val thy = Proof_Context.theory_of ctxt;
   1.487 -    val tyenv =
   1.488 -      Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_pred2T instA instB))
   1.489 -        Vartab.empty;
   1.490 -  in Envir.subst_term (tyenv, Vartab.empty) rel end
   1.491 -  handle Type.TYPE_MATCH => error "Bad relator";
   1.492 -
   1.493 -fun normalize_wit insts CA As wit =
   1.494 -  let
   1.495 -    fun strip_param (Ts, T as Type (@{type_name fun}, [T1, T2])) =
   1.496 -        if Type.raw_instance (CA, T) then (Ts, T) else strip_param (T1 :: Ts, T2)
   1.497 -      | strip_param x = x;
   1.498 -    val (Ts, T) = strip_param ([], fastype_of wit);
   1.499 -    val subst = Term.add_tvar_namesT T [] ~~ insts;
   1.500 -    fun find y = find_index (fn x => x = y) As;
   1.501 -  in
   1.502 -    (map (find o Term.typ_subst_TVars subst) (rev Ts), Term.subst_TVars subst wit)
   1.503 -  end;
   1.504 -
   1.505 -fun minimize_wits wits =
   1.506 - let
   1.507 -   fun minimize done [] = done
   1.508 -     | minimize done ((I, wit) :: todo) =
   1.509 -       if exists (fn (J, _) => subset (op =) (J, I)) (done @ todo)
   1.510 -       then minimize done todo
   1.511 -       else minimize ((I, wit) :: done) todo;
   1.512 - in minimize [] wits end;
   1.513 -
   1.514 -fun mk_map live Ts Us t =
   1.515 -  let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
   1.516 -    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   1.517 -  end;
   1.518 -
   1.519 -fun mk_rel live Ts Us t =
   1.520 -  let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in
   1.521 -    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   1.522 -  end;
   1.523 -
   1.524 -fun build_map_or_rel mk const of_bnf dest ctxt build_simple =
   1.525 -  let
   1.526 -    fun build (TU as (T, U)) =
   1.527 -      if T = U then
   1.528 -        const T
   1.529 -      else
   1.530 -        (case TU of
   1.531 -          (Type (s, Ts), Type (s', Us)) =>
   1.532 -          if s = s' then
   1.533 -            let
   1.534 -              val bnf = the (bnf_of ctxt s);
   1.535 -              val live = live_of_bnf bnf;
   1.536 -              val mapx = mk live Ts Us (of_bnf bnf);
   1.537 -              val TUs' = map dest (fst (strip_typeN live (fastype_of mapx)));
   1.538 -            in Term.list_comb (mapx, map build TUs') end
   1.539 -          else
   1.540 -            build_simple TU
   1.541 -        | _ => build_simple TU);
   1.542 -  in build end;
   1.543 -
   1.544 -val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT;
   1.545 -val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
   1.546 -
   1.547 -fun map_flattened_map_args ctxt s map_args fs =
   1.548 -  let
   1.549 -    val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs;
   1.550 -    val flat_fs' = map_args flat_fs;
   1.551 -  in
   1.552 -    permute_like (op aconv) flat_fs fs flat_fs'
   1.553 -  end;
   1.554 -
   1.555 -
   1.556 -(* Names *)
   1.557 -
   1.558 -val mapN = "map";
   1.559 -val setN = "set";
   1.560 -fun mk_setN i = setN ^ nonzero_string_of_int i;
   1.561 -val bdN = "bd";
   1.562 -val witN = "wit";
   1.563 -fun mk_witN i = witN ^ nonzero_string_of_int i;
   1.564 -val relN = "rel";
   1.565 -
   1.566 -val bd_card_orderN = "bd_card_order";
   1.567 -val bd_cinfiniteN = "bd_cinfinite";
   1.568 -val bd_Card_orderN = "bd_Card_order";
   1.569 -val bd_CinfiniteN = "bd_Cinfinite";
   1.570 -val bd_CnotzeroN = "bd_Cnotzero";
   1.571 -val collect_set_mapN = "collect_set_map";
   1.572 -val in_bdN = "in_bd";
   1.573 -val in_monoN = "in_mono";
   1.574 -val in_relN = "in_rel";
   1.575 -val map_id0N = "map_id0";
   1.576 -val map_idN = "map_id";
   1.577 -val map_comp0N = "map_comp0";
   1.578 -val map_compN = "map_comp";
   1.579 -val map_cong0N = "map_cong0";
   1.580 -val map_congN = "map_cong";
   1.581 -val map_transferN = "map_transfer";
   1.582 -val rel_eqN = "rel_eq";
   1.583 -val rel_flipN = "rel_flip";
   1.584 -val set_map0N = "set_map0";
   1.585 -val set_mapN = "set_map";
   1.586 -val set_bdN = "set_bd";
   1.587 -val rel_GrpN = "rel_Grp";
   1.588 -val rel_conversepN = "rel_conversep";
   1.589 -val rel_monoN = "rel_mono"
   1.590 -val rel_mono_strongN = "rel_mono_strong"
   1.591 -val rel_comppN = "rel_compp";
   1.592 -val rel_compp_GrpN = "rel_compp_Grp";
   1.593 -
   1.594 -datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
   1.595 -
   1.596 -datatype fact_policy = Dont_Note | Note_Some | Note_All;
   1.597 -
   1.598 -val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
   1.599 -val bnf_timing = Attrib.setup_config_bool @{binding bnf_timing} (K false);
   1.600 -
   1.601 -fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
   1.602 -
   1.603 -val smart_max_inline_size = 25; (*FUDGE*)
   1.604 -
   1.605 -fun note_bnf_thms fact_policy qualify' bnf_b bnf =
   1.606 -  let
   1.607 -    val axioms = axioms_of_bnf bnf;
   1.608 -    val facts = facts_of_bnf bnf;
   1.609 -    val wits = wits_of_bnf bnf;
   1.610 -    val qualify =
   1.611 -      let val (_, qs, _) = Binding.dest bnf_b;
   1.612 -      in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify' end;
   1.613 -  in
   1.614 -    (if fact_policy = Note_All then
   1.615 -      let
   1.616 -        val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits);
   1.617 -        val notes =
   1.618 -          [(bd_card_orderN, [#bd_card_order axioms]),
   1.619 -            (bd_cinfiniteN, [#bd_cinfinite axioms]),
   1.620 -            (bd_Card_orderN, [#bd_Card_order facts]),
   1.621 -            (bd_CinfiniteN, [#bd_Cinfinite facts]),
   1.622 -            (bd_CnotzeroN, [#bd_Cnotzero facts]),
   1.623 -            (collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
   1.624 -            (in_bdN, [Lazy.force (#in_bd facts)]),
   1.625 -            (in_monoN, [Lazy.force (#in_mono facts)]),
   1.626 -            (in_relN, [Lazy.force (#in_rel facts)]),
   1.627 -            (map_comp0N, [#map_comp0 axioms]),
   1.628 -            (map_id0N, [#map_id0 axioms]),
   1.629 -            (map_transferN, [Lazy.force (#map_transfer facts)]),
   1.630 -            (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
   1.631 -            (set_map0N, #set_map0 axioms),
   1.632 -            (set_bdN, #set_bd axioms)] @
   1.633 -            (witNs ~~ wit_thmss_of_bnf bnf)
   1.634 -            |> map (fn (thmN, thms) =>
   1.635 -              ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []),
   1.636 -              [(thms, [])]));
   1.637 -        in
   1.638 -          Local_Theory.notes notes #> snd
   1.639 -        end
   1.640 -      else
   1.641 -        I)
   1.642 -    #> (if fact_policy <> Dont_Note then
   1.643 -        let
   1.644 -          val notes =
   1.645 -            [(map_compN, [Lazy.force (#map_comp facts)], []),
   1.646 -            (map_cong0N, [#map_cong0 axioms], []),
   1.647 -            (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
   1.648 -            (map_idN, [Lazy.force (#map_id facts)], []),
   1.649 -            (rel_comppN, [Lazy.force (#rel_OO facts)], []),
   1.650 -            (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
   1.651 -            (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
   1.652 -            (rel_eqN, [Lazy.force (#rel_eq facts)], []),
   1.653 -            (rel_flipN, [Lazy.force (#rel_flip facts)], []),
   1.654 -            (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
   1.655 -            (rel_monoN, [Lazy.force (#rel_mono facts)], []),
   1.656 -            (set_mapN, map Lazy.force (#set_map facts), [])]
   1.657 -            |> filter_out (null o #2)
   1.658 -            |> map (fn (thmN, thms, attrs) =>
   1.659 -              ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)),
   1.660 -                attrs), [(thms, [])]));
   1.661 -        in
   1.662 -          Local_Theory.notes notes #> snd
   1.663 -        end
   1.664 -      else
   1.665 -        I)
   1.666 -  end;
   1.667 -
   1.668 -
   1.669 -(* Define new BNFs *)
   1.670 -
   1.671 -fun define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
   1.672 -  ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy =
   1.673 -  let
   1.674 -    val live = length set_rhss;
   1.675 -
   1.676 -    val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
   1.677 -
   1.678 -    fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
   1.679 -
   1.680 -    fun maybe_define user_specified (b, rhs) lthy =
   1.681 -      let
   1.682 -        val inline =
   1.683 -          (user_specified orelse fact_policy = Dont_Note) andalso
   1.684 -          (case const_policy of
   1.685 -            Dont_Inline => false
   1.686 -          | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
   1.687 -          | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_size
   1.688 -          | Do_Inline => true)
   1.689 -      in
   1.690 -        if inline then
   1.691 -          ((rhs, Drule.reflexive_thm), lthy)
   1.692 -        else
   1.693 -          let val b = b () in
   1.694 -            apfst (apsnd snd) (Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs))
   1.695 -              lthy)
   1.696 -          end
   1.697 -      end;
   1.698 -
   1.699 -    fun maybe_restore lthy_old lthy =
   1.700 -      lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
   1.701 -
   1.702 -    val map_bind_def =
   1.703 -      (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
   1.704 -         map_rhs);
   1.705 -    val set_binds_defs =
   1.706 -      let
   1.707 -        fun set_name i get_b =
   1.708 -          (case try (nth set_bs) (i - 1) of
   1.709 -            SOME b => if Binding.is_empty b then get_b else K b
   1.710 -          | NONE => get_b) #> def_qualify;
   1.711 -        val bs = if live = 1 then [set_name 1 (fn () => mk_prefix_binding setN)]
   1.712 -          else map (fn i => set_name i (fn () => mk_prefix_binding (mk_setN i))) (1 upto live);
   1.713 -      in bs ~~ set_rhss end;
   1.714 -    val bd_bind_def = (fn () => def_qualify (mk_prefix_binding bdN), bd_rhs);
   1.715 -
   1.716 -    val ((((bnf_map_term, raw_map_def),
   1.717 -      (bnf_set_terms, raw_set_defs)),
   1.718 -      (bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) =
   1.719 -        no_defs_lthy
   1.720 -        |> maybe_define true map_bind_def
   1.721 -        ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs
   1.722 -        ||>> maybe_define true bd_bind_def
   1.723 -        ||> `(maybe_restore no_defs_lthy);
   1.724 -
   1.725 -    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.726 -
   1.727 -
   1.728 -    val bnf_map_def = Morphism.thm phi raw_map_def;
   1.729 -    val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;
   1.730 -    val bnf_bd_def = Morphism.thm phi raw_bd_def;
   1.731 -
   1.732 -    val bnf_map = Morphism.term phi bnf_map_term;
   1.733 -
   1.734 -    (*TODO: handle errors*)
   1.735 -    (*simple shape analysis of a map function*)
   1.736 -    val ((alphas, betas), (Calpha, _)) =
   1.737 -      fastype_of bnf_map
   1.738 -      |> strip_typeN live
   1.739 -      |>> map_split dest_funT
   1.740 -      ||> dest_funT
   1.741 -      handle TYPE _ => error "Bad map function";
   1.742 -
   1.743 -    val Calpha_params = map TVar (Term.add_tvarsT Calpha []);
   1.744 -
   1.745 -    val bnf_T = Morphism.typ phi T_rhs;
   1.746 -    val bad_args = Term.add_tfreesT bnf_T [];
   1.747 -    val _ = if null bad_args then () else error ("Locally fixed type arguments " ^
   1.748 -      commas_quote (map (Syntax.string_of_typ no_defs_lthy o TFree) bad_args));
   1.749 -
   1.750 -    val bnf_sets =
   1.751 -      map2 (normalize_set Calpha_params) alphas (map (Morphism.term phi) bnf_set_terms);
   1.752 -    val bnf_bd =
   1.753 -      Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ Calpha_params)
   1.754 -        (Morphism.term phi bnf_bd_term);
   1.755 -
   1.756 -    (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*)
   1.757 -    val deads = (case Ds_opt of
   1.758 -      NONE => subtract (op =) (alphas @ betas) (map TVar (Term.add_tvars bnf_map []))
   1.759 -    | SOME Ds => map (Morphism.typ phi) Ds);
   1.760 -
   1.761 -    (*TODO: further checks of type of bnf_map*)
   1.762 -    (*TODO: check types of bnf_sets*)
   1.763 -    (*TODO: check type of bnf_bd*)
   1.764 -    (*TODO: check type of bnf_rel*)
   1.765 -
   1.766 -    fun mk_bnf_map Ds As' Bs' =
   1.767 -      Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As') @ (betas ~~ Bs')) bnf_map;
   1.768 -    fun mk_bnf_t Ds As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
   1.769 -    fun mk_bnf_T Ds As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
   1.770 -
   1.771 -    val (((As, Bs), Ds), names_lthy) = lthy
   1.772 -      |> mk_TFrees live
   1.773 -      ||>> mk_TFrees live
   1.774 -      ||>> mk_TFrees (length deads);
   1.775 -    val RTs = map2 (curry HOLogic.mk_prodT) As Bs;
   1.776 -    val pred2RTs = map2 mk_pred2T As Bs;
   1.777 -    val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst
   1.778 -    val CA = mk_bnf_T Ds As Calpha;
   1.779 -    val CR = mk_bnf_T Ds RTs Calpha;
   1.780 -    val setRs =
   1.781 -      map3 (fn R => fn T => fn U =>
   1.782 -          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs;
   1.783 -
   1.784 -    (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
   1.785 -      Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
   1.786 -    val OO_Grp =
   1.787 -      let
   1.788 -        val map1 = Term.list_comb (mk_bnf_map Ds RTs As, map fst_const RTs);
   1.789 -        val map2 = Term.list_comb (mk_bnf_map Ds RTs Bs, map snd_const RTs);
   1.790 -        val bnf_in = mk_in setRs (map (mk_bnf_t Ds RTs) bnf_sets) CR;
   1.791 -      in
   1.792 -        mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2)
   1.793 -        |> fold_rev Term.absfree Rs'
   1.794 -      end;
   1.795 -
   1.796 -    val rel_rhs = the_default OO_Grp rel_rhs_opt;
   1.797 -
   1.798 -    val rel_bind_def =
   1.799 -      (fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b),
   1.800 -         rel_rhs);
   1.801 -
   1.802 -    val wit_rhss =
   1.803 -      if null wit_rhss then
   1.804 -        [fold_rev Term.absdummy As (Term.list_comb (mk_bnf_map Ds As As,
   1.805 -          map2 (fn T => fn i => Term.absdummy T (Bound i)) As (live downto 1)) $
   1.806 -          Const (@{const_name undefined}, CA))]
   1.807 -      else wit_rhss;
   1.808 -    val nwits = length wit_rhss;
   1.809 -    val wit_binds_defs =
   1.810 -      let
   1.811 -        val bs = if nwits = 1 then [fn () => def_qualify (mk_prefix_binding witN)]
   1.812 -          else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits);
   1.813 -      in bs ~~ wit_rhss end;
   1.814 -
   1.815 -    val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
   1.816 -      lthy
   1.817 -      |> maybe_define (is_some rel_rhs_opt) rel_bind_def
   1.818 -      ||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs
   1.819 -      ||> `(maybe_restore lthy);
   1.820 -
   1.821 -    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.822 -    val bnf_rel_def = Morphism.thm phi raw_rel_def;
   1.823 -    val bnf_rel = Morphism.term phi bnf_rel_term;
   1.824 -    fun mk_bnf_rel Ds As' Bs' =
   1.825 -      normalize_rel lthy (map2 mk_pred2T As' Bs') (mk_bnf_T Ds As' Calpha) (mk_bnf_T Ds Bs' Calpha)
   1.826 -        bnf_rel;
   1.827 -
   1.828 -    val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs;
   1.829 -    val bnf_wits =
   1.830 -      map (normalize_wit Calpha_params Calpha alphas o Morphism.term phi) bnf_wit_terms;
   1.831 -
   1.832 -    fun mk_OO_Grp Ds' As' Bs' =
   1.833 -      Term.subst_atomic_types ((Ds ~~ Ds') @ (As ~~ As') @ (Bs ~~ Bs')) OO_Grp;
   1.834 -  in
   1.835 -    (((alphas, betas, deads, Calpha),
   1.836 -     (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
   1.837 -     (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
   1.838 -     (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy)
   1.839 -  end;
   1.840 -
   1.841 -fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs
   1.842 -  ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
   1.843 -  no_defs_lthy =
   1.844 -  let
   1.845 -    val fact_policy = mk_fact_policy no_defs_lthy;
   1.846 -    val bnf_b = qualify raw_bnf_b;
   1.847 -    val live = length raw_sets;
   1.848 -
   1.849 -    val T_rhs = prep_typ no_defs_lthy raw_bnf_T;
   1.850 -    val map_rhs = prep_term no_defs_lthy raw_map;
   1.851 -    val set_rhss = map (prep_term no_defs_lthy) raw_sets;
   1.852 -    val bd_rhs = prep_term no_defs_lthy raw_bd;
   1.853 -    val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
   1.854 -    val rel_rhs_opt = Option.map (prep_term no_defs_lthy) raw_rel_opt;
   1.855 -
   1.856 -    fun err T =
   1.857 -      error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
   1.858 -        " as unnamed BNF");
   1.859 -
   1.860 -    val (bnf_b, key) =
   1.861 -      if Binding.eq_name (bnf_b, Binding.empty) then
   1.862 -        (case T_rhs of
   1.863 -          Type (C, Ts) => if forall (can dest_TFree) Ts
   1.864 -            then (Binding.qualified_name C, C) else err T_rhs
   1.865 -        | T => err T)
   1.866 -      else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
   1.867 -
   1.868 -    val (((alphas, betas, deads, Calpha),
   1.869 -     (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
   1.870 -     (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
   1.871 -     (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) =
   1.872 -       define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
   1.873 -         ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy;
   1.874 -
   1.875 -    val dead = length deads;
   1.876 -
   1.877 -    val ((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), (Ts, T)) = lthy
   1.878 -      |> mk_TFrees live
   1.879 -      ||>> mk_TFrees live
   1.880 -      ||>> mk_TFrees live
   1.881 -      ||>> mk_TFrees dead
   1.882 -      ||>> mk_TFrees live
   1.883 -      ||>> mk_TFrees live
   1.884 -      ||> fst o mk_TFrees 1
   1.885 -      ||> the_single
   1.886 -      ||> `(replicate live);
   1.887 -
   1.888 -    val mk_bnf_map = mk_bnf_map_Ds Ds;
   1.889 -    val mk_bnf_t = mk_bnf_t_Ds Ds;
   1.890 -    val mk_bnf_T = mk_bnf_T_Ds Ds;
   1.891 -
   1.892 -    val pred2RTs = map2 mk_pred2T As' Bs';
   1.893 -    val pred2RTsAsCs = map2 mk_pred2T As' Cs;
   1.894 -    val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
   1.895 -    val pred2RT's = map2 mk_pred2T Bs' As';
   1.896 -    val self_pred2RTs = map2 mk_pred2T As' As';
   1.897 -    val transfer_domRTs = map2 mk_pred2T As' B1Ts;
   1.898 -    val transfer_ranRTs = map2 mk_pred2T Bs' B2Ts;
   1.899 -
   1.900 -    val CA' = mk_bnf_T As' Calpha;
   1.901 -    val CB' = mk_bnf_T Bs' Calpha;
   1.902 -    val CC' = mk_bnf_T Cs Calpha;
   1.903 -    val CB1 = mk_bnf_T B1Ts Calpha;
   1.904 -    val CB2 = mk_bnf_T B2Ts Calpha;
   1.905 -
   1.906 -    val bnf_map_AsAs = mk_bnf_map As' As';
   1.907 -    val bnf_map_AsBs = mk_bnf_map As' Bs';
   1.908 -    val bnf_map_AsCs = mk_bnf_map As' Cs;
   1.909 -    val bnf_map_BsCs = mk_bnf_map Bs' Cs;
   1.910 -    val bnf_sets_As = map (mk_bnf_t As') bnf_sets;
   1.911 -    val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets;
   1.912 -    val bnf_bd_As = mk_bnf_t As' bnf_bd;
   1.913 -    fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
   1.914 -
   1.915 -    val pre_names_lthy = lthy;
   1.916 -    val (((((((((((((((fs, gs), hs), x), y), zs), ys), As),
   1.917 -      As_copy), bs), Rs), Rs_copy), Ss),
   1.918 -      transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
   1.919 -      |> mk_Frees "f" (map2 (curry op -->) As' Bs')
   1.920 -      ||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs)
   1.921 -      ||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
   1.922 -      ||>> yield_singleton (mk_Frees "x") CA'
   1.923 -      ||>> yield_singleton (mk_Frees "y") CB'
   1.924 -      ||>> mk_Frees "z" As'
   1.925 -      ||>> mk_Frees "y" Bs'
   1.926 -      ||>> mk_Frees "A" (map HOLogic.mk_setT As')
   1.927 -      ||>> mk_Frees "A" (map HOLogic.mk_setT As')
   1.928 -      ||>> mk_Frees "b" As'
   1.929 -      ||>> mk_Frees "R" pred2RTs
   1.930 -      ||>> mk_Frees "R" pred2RTs
   1.931 -      ||>> mk_Frees "S" pred2RTsBsCs
   1.932 -      ||>> mk_Frees "R" transfer_domRTs
   1.933 -      ||>> mk_Frees "S" transfer_ranRTs;
   1.934 -
   1.935 -    val fs_copy = map2 (retype_free o fastype_of) fs gs;
   1.936 -    val x_copy = retype_free CA' y;
   1.937 -
   1.938 -    val rel = mk_bnf_rel pred2RTs CA' CB';
   1.939 -    val relAsAs = mk_bnf_rel self_pred2RTs CA' CA';
   1.940 -    val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
   1.941 -
   1.942 -    val map_id0_goal =
   1.943 -      let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in
   1.944 -        mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')
   1.945 -      end;
   1.946 -
   1.947 -    val map_comp0_goal =
   1.948 -      let
   1.949 -        val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
   1.950 -        val comp_bnf_map_app = HOLogic.mk_comp
   1.951 -          (Term.list_comb (bnf_map_BsCs, gs), Term.list_comb (bnf_map_AsBs, fs));
   1.952 -      in
   1.953 -        fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
   1.954 -      end;
   1.955 -
   1.956 -    fun mk_map_cong_prem x z set f f_copy =
   1.957 -      Logic.all z (Logic.mk_implies
   1.958 -        (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
   1.959 -        mk_Trueprop_eq (f $ z, f_copy $ z)));
   1.960 -
   1.961 -    val map_cong0_goal =
   1.962 -      let
   1.963 -        val prems = map4 (mk_map_cong_prem x) zs bnf_sets_As fs fs_copy;
   1.964 -        val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
   1.965 -          Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
   1.966 -      in
   1.967 -        fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq))
   1.968 -      end;
   1.969 -
   1.970 -    val set_map0s_goal =
   1.971 -      let
   1.972 -        fun mk_goal setA setB f =
   1.973 -          let
   1.974 -            val set_comp_map =
   1.975 -              HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs));
   1.976 -            val image_comp_set = HOLogic.mk_comp (mk_image f, setA);
   1.977 -          in
   1.978 -            fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set))
   1.979 -          end;
   1.980 -      in
   1.981 -        map3 mk_goal bnf_sets_As bnf_sets_Bs fs
   1.982 -      end;
   1.983 -
   1.984 -    val card_order_bd_goal = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As);
   1.985 -
   1.986 -    val cinfinite_bd_goal = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As);
   1.987 -
   1.988 -    val set_bds_goal =
   1.989 -      let
   1.990 -        fun mk_goal set =
   1.991 -          Logic.all x (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (set $ x)) bnf_bd_As));
   1.992 -      in
   1.993 -        map mk_goal bnf_sets_As
   1.994 -      end;
   1.995 -
   1.996 -    val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC';
   1.997 -    val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC';
   1.998 -    val rel_OO_lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss);
   1.999 -    val rel_OO_rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
  1.1000 -    val le_rel_OO_goal =
  1.1001 -      fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_rhs rel_OO_lhs));
  1.1002 -
  1.1003 -    val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs),
  1.1004 -      Term.list_comb (mk_OO_Grp Ds As' Bs', Rs)));
  1.1005 -
  1.1006 -    val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal
  1.1007 -      card_order_bd_goal cinfinite_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal;
  1.1008 -
  1.1009 -    fun mk_wit_goals (I, wit) =
  1.1010 -      let
  1.1011 -        val xs = map (nth bs) I;
  1.1012 -        fun wit_goal i =
  1.1013 -          let
  1.1014 -            val z = nth zs i;
  1.1015 -            val set_wit = nth bnf_sets_As i $ Term.list_comb (wit, xs);
  1.1016 -            val concl = HOLogic.mk_Trueprop
  1.1017 -              (if member (op =) I i then HOLogic.mk_eq (z, nth bs i)
  1.1018 -              else @{term False});
  1.1019 -          in
  1.1020 -            fold_rev Logic.all (z :: xs)
  1.1021 -              (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set_wit)), concl))
  1.1022 -          end;
  1.1023 -      in
  1.1024 -        map wit_goal (0 upto live - 1)
  1.1025 -      end;
  1.1026 -
  1.1027 -    val triv_wit_tac = mk_trivial_wit_tac bnf_wit_defs;
  1.1028 -
  1.1029 -    val wit_goalss =
  1.1030 -      (if null raw_wits then SOME triv_wit_tac else NONE, map mk_wit_goals bnf_wit_As);
  1.1031 -
  1.1032 -    fun after_qed mk_wit_thms thms lthy =
  1.1033 -      let
  1.1034 -        val (axioms, nontriv_wit_thms) = apfst (mk_axioms live) (chop (length goals) thms);
  1.1035 -
  1.1036 -        val bd_Card_order = #bd_card_order axioms RS @{thm conjunct2[OF card_order_on_Card_order]};
  1.1037 -        val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order];
  1.1038 -        val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
  1.1039 -
  1.1040 -        fun mk_collect_set_map () =
  1.1041 -          let
  1.1042 -            val defT = mk_bnf_T Ts Calpha --> HOLogic.mk_setT T;
  1.1043 -            val collect_map = HOLogic.mk_comp
  1.1044 -              (mk_collect (map (mk_bnf_t Ts) bnf_sets) defT,
  1.1045 -              Term.list_comb (mk_bnf_map As' Ts, hs));
  1.1046 -            val image_collect = mk_collect
  1.1047 -              (map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As)
  1.1048 -              defT;
  1.1049 -            (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
  1.1050 -            val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
  1.1051 -          in
  1.1052 -            Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map0 axioms)))
  1.1053 -            |> Thm.close_derivation
  1.1054 -          end;
  1.1055 -
  1.1056 -        val collect_set_map = Lazy.lazy mk_collect_set_map;
  1.1057 -
  1.1058 -        fun mk_in_mono () =
  1.1059 -          let
  1.1060 -            val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_leq) As As_copy;
  1.1061 -            val in_mono_goal =
  1.1062 -              fold_rev Logic.all (As @ As_copy)
  1.1063 -                (Logic.list_implies (prems_mono, HOLogic.mk_Trueprop
  1.1064 -                  (mk_leq (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
  1.1065 -          in
  1.1066 -            Goal.prove_sorry lthy [] [] in_mono_goal (K (mk_in_mono_tac live))
  1.1067 -            |> Thm.close_derivation
  1.1068 -          end;
  1.1069 -
  1.1070 -        val in_mono = Lazy.lazy mk_in_mono;
  1.1071 -
  1.1072 -        fun mk_in_cong () =
  1.1073 -          let
  1.1074 -            val prems_cong = map2 (curry mk_Trueprop_eq) As As_copy;
  1.1075 -            val in_cong_goal =
  1.1076 -              fold_rev Logic.all (As @ As_copy)
  1.1077 -                (Logic.list_implies (prems_cong,
  1.1078 -                  mk_Trueprop_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA')));
  1.1079 -          in
  1.1080 -            Goal.prove_sorry lthy [] [] in_cong_goal
  1.1081 -              (K ((TRY o hyp_subst_tac lthy THEN' rtac refl) 1))
  1.1082 -            |> Thm.close_derivation
  1.1083 -          end;
  1.1084 -
  1.1085 -        val in_cong = Lazy.lazy mk_in_cong;
  1.1086 -
  1.1087 -        val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
  1.1088 -        val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms));
  1.1089 -
  1.1090 -        fun mk_map_cong () =
  1.1091 -          let
  1.1092 -            val prem0 = mk_Trueprop_eq (x, x_copy);
  1.1093 -            val prems = map4 (mk_map_cong_prem x_copy) zs bnf_sets_As fs fs_copy;
  1.1094 -            val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
  1.1095 -              Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy);
  1.1096 -            val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
  1.1097 -              (Logic.list_implies (prem0 :: prems, eq));
  1.1098 -          in
  1.1099 -            Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac lthy (#map_cong0 axioms))
  1.1100 -            |> Thm.close_derivation
  1.1101 -          end;
  1.1102 -
  1.1103 -        val map_cong = Lazy.lazy mk_map_cong;
  1.1104 -
  1.1105 -        val set_map = map (fn thm => Lazy.lazy (fn () => mk_set_map thm)) (#set_map0 axioms);
  1.1106 -
  1.1107 -        val wit_thms =
  1.1108 -          if null nontriv_wit_thms then mk_wit_thms (map Lazy.force set_map) else nontriv_wit_thms;
  1.1109 -
  1.1110 -        fun mk_in_bd () =
  1.1111 -          let
  1.1112 -            val bdT = fst (dest_relT (fastype_of bnf_bd_As));
  1.1113 -            val bdTs = replicate live bdT;
  1.1114 -            val bd_bnfT = mk_bnf_T bdTs Calpha;
  1.1115 -            val surj_imp_ordLeq_inst = (if live = 0 then TrueI else
  1.1116 -              let
  1.1117 -                val ranTs = map (fn AT => mk_sumT (AT, HOLogic.unitT)) As';
  1.1118 -                val funTs = map (fn T => bdT --> T) ranTs;
  1.1119 -                val ran_bnfT = mk_bnf_T ranTs Calpha;
  1.1120 -                val (revTs, Ts) = `rev (bd_bnfT :: funTs);
  1.1121 -                val cTs = map (SOME o certifyT lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
  1.1122 -                val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs)
  1.1123 -                  (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
  1.1124 -                    map Bound (live - 1 downto 0)) $ Bound live));
  1.1125 -                val cts = [NONE, SOME (certify lthy tinst)];
  1.1126 -              in
  1.1127 -                Drule.instantiate' cTs cts @{thm surj_imp_ordLeq}
  1.1128 -              end);
  1.1129 -            val bd = mk_cexp
  1.1130 -              (if live = 0 then ctwo
  1.1131 -                else mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo)
  1.1132 -              (mk_csum bnf_bd_As (mk_card_of (HOLogic.mk_UNIV bd_bnfT)));
  1.1133 -            val in_bd_goal =
  1.1134 -              fold_rev Logic.all As
  1.1135 -                (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd));
  1.1136 -          in
  1.1137 -            Goal.prove_sorry lthy [] [] in_bd_goal
  1.1138 -              (mk_in_bd_tac live surj_imp_ordLeq_inst
  1.1139 -                (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
  1.1140 -                (map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms)
  1.1141 -                bd_Card_order bd_Cinfinite bd_Cnotzero)
  1.1142 -            |> Thm.close_derivation
  1.1143 -          end;
  1.1144 -
  1.1145 -        val in_bd = Lazy.lazy mk_in_bd;
  1.1146 -
  1.1147 -        val rel_OO_Grp = #rel_OO_Grp axioms;
  1.1148 -        val rel_OO_Grps = no_refl [rel_OO_Grp];
  1.1149 -
  1.1150 -        fun mk_rel_Grp () =
  1.1151 -          let
  1.1152 -            val lhs = Term.list_comb (rel, map2 mk_Grp As fs);
  1.1153 -            val rhs = mk_Grp (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
  1.1154 -            val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
  1.1155 -          in
  1.1156 -            Goal.prove_sorry lthy [] [] goal
  1.1157 -              (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id)
  1.1158 -                (Lazy.force map_comp) (map Lazy.force set_map))
  1.1159 -            |> Thm.close_derivation
  1.1160 -          end;
  1.1161 -
  1.1162 -        val rel_Grp = Lazy.lazy mk_rel_Grp;
  1.1163 -
  1.1164 -        fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
  1.1165 -        fun mk_rel_concl f = HOLogic.mk_Trueprop
  1.1166 -          (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy)));
  1.1167 -
  1.1168 -        fun mk_rel_mono () =
  1.1169 -          let
  1.1170 -            val mono_prems = mk_rel_prems mk_leq;
  1.1171 -            val mono_concl = mk_rel_concl (uncurry mk_leq);
  1.1172 -          in
  1.1173 -            Goal.prove_sorry lthy [] []
  1.1174 -              (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
  1.1175 -              (K (mk_rel_mono_tac rel_OO_Grps (Lazy.force in_mono)))
  1.1176 -            |> Thm.close_derivation
  1.1177 -          end;
  1.1178 -
  1.1179 -        fun mk_rel_cong () =
  1.1180 -          let
  1.1181 -            val cong_prems = mk_rel_prems (curry HOLogic.mk_eq);
  1.1182 -            val cong_concl = mk_rel_concl HOLogic.mk_eq;
  1.1183 -          in
  1.1184 -            Goal.prove_sorry lthy [] []
  1.1185 -              (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
  1.1186 -              (fn _ => (TRY o hyp_subst_tac lthy THEN' rtac refl) 1)
  1.1187 -            |> Thm.close_derivation
  1.1188 -          end;
  1.1189 -
  1.1190 -        val rel_mono = Lazy.lazy mk_rel_mono;
  1.1191 -        val rel_cong = Lazy.lazy mk_rel_cong;
  1.1192 -
  1.1193 -        fun mk_rel_eq () =
  1.1194 -          Goal.prove_sorry lthy [] []
  1.1195 -            (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
  1.1196 -              HOLogic.eq_const CA'))
  1.1197 -            (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id0 axioms)))
  1.1198 -          |> Thm.close_derivation;
  1.1199 -
  1.1200 -        val rel_eq = Lazy.lazy mk_rel_eq;
  1.1201 -
  1.1202 -        fun mk_rel_conversep () =
  1.1203 -          let
  1.1204 -            val relBsAs = mk_bnf_rel pred2RT's CB' CA';
  1.1205 -            val lhs = Term.list_comb (relBsAs, map mk_conversep Rs);
  1.1206 -            val rhs = mk_conversep (Term.list_comb (rel, Rs));
  1.1207 -            val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
  1.1208 -            val le_thm = Goal.prove_sorry lthy [] [] le_goal
  1.1209 -              (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
  1.1210 -                (Lazy.force map_comp) (map Lazy.force set_map))
  1.1211 -              |> Thm.close_derivation
  1.1212 -            val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
  1.1213 -          in
  1.1214 -            Goal.prove_sorry lthy [] [] goal
  1.1215 -              (K (mk_rel_conversep_tac le_thm (Lazy.force rel_mono)))
  1.1216 -            |> Thm.close_derivation
  1.1217 -          end;
  1.1218 -
  1.1219 -        val rel_conversep = Lazy.lazy mk_rel_conversep;
  1.1220 -
  1.1221 -        fun mk_rel_OO () =
  1.1222 -          Goal.prove_sorry lthy [] []
  1.1223 -            (fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs)))
  1.1224 -            (mk_rel_OO_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
  1.1225 -              (Lazy.force map_comp) (map Lazy.force set_map))
  1.1226 -          |> Thm.close_derivation
  1.1227 -          |> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]);
  1.1228 -
  1.1229 -        val rel_OO = Lazy.lazy mk_rel_OO;
  1.1230 -
  1.1231 -        fun mk_in_rel () = trans OF [rel_OO_Grp, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD};
  1.1232 -
  1.1233 -        val in_rel = Lazy.lazy mk_in_rel;
  1.1234 -
  1.1235 -        fun mk_rel_flip () =
  1.1236 -          let
  1.1237 -            val rel_conversep_thm = Lazy.force rel_conversep;
  1.1238 -            val cts = map (SOME o certify lthy) Rs;
  1.1239 -            val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
  1.1240 -          in
  1.1241 -            unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
  1.1242 -            |> singleton (Proof_Context.export names_lthy pre_names_lthy)
  1.1243 -          end;
  1.1244 -
  1.1245 -        val rel_flip = Lazy.lazy mk_rel_flip;
  1.1246 -
  1.1247 -        fun mk_rel_mono_strong () =
  1.1248 -          let
  1.1249 -            fun mk_prem setA setB R S a b =
  1.1250 -              HOLogic.mk_Trueprop
  1.1251 -                (mk_Ball (setA $ x) (Term.absfree (dest_Free a)
  1.1252 -                  (mk_Ball (setB $ y) (Term.absfree (dest_Free b)
  1.1253 -                    (HOLogic.mk_imp (R $ a $ b, S $ a $ b))))));
  1.1254 -            val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) :: 
  1.1255 -              map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
  1.1256 -            val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y);
  1.1257 -          in
  1.1258 -            Goal.prove_sorry lthy [] []
  1.1259 -              (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
  1.1260 -              (mk_rel_mono_strong_tac (Lazy.force in_rel) (map Lazy.force set_map))
  1.1261 -            |> Thm.close_derivation
  1.1262 -          end;
  1.1263 -
  1.1264 -        val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
  1.1265 -
  1.1266 -        fun mk_map_transfer () =
  1.1267 -          let
  1.1268 -            val rels = map2 mk_fun_rel transfer_domRs transfer_ranRs;
  1.1269 -            val rel = mk_fun_rel
  1.1270 -              (Term.list_comb (mk_bnf_rel transfer_domRTs CA' CB1, transfer_domRs))
  1.1271 -              (Term.list_comb (mk_bnf_rel transfer_ranRTs CB' CB2, transfer_ranRs));
  1.1272 -            val concl = HOLogic.mk_Trueprop
  1.1273 -              (fold_rev mk_fun_rel rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts);
  1.1274 -          in
  1.1275 -            Goal.prove_sorry lthy [] []
  1.1276 -              (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
  1.1277 -              (mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel)
  1.1278 -                (map Lazy.force set_map) (#map_cong0 axioms) (Lazy.force map_comp))
  1.1279 -            |> Thm.close_derivation
  1.1280 -          end;
  1.1281 -
  1.1282 -        val map_transfer = Lazy.lazy mk_map_transfer;
  1.1283 -
  1.1284 -        val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
  1.1285 -
  1.1286 -        val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
  1.1287 -          in_mono in_rel map_comp map_cong map_id map_transfer rel_eq rel_flip set_map
  1.1288 -          rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
  1.1289 -
  1.1290 -        val wits = map2 mk_witness bnf_wits wit_thms;
  1.1291 -
  1.1292 -        val bnf_rel =
  1.1293 -          Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;
  1.1294 -
  1.1295 -        val bnf = mk_bnf bnf_b Calpha live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms
  1.1296 -          defs facts wits bnf_rel;
  1.1297 -      in
  1.1298 -        (bnf, lthy |> note_bnf_thms fact_policy qualify bnf_b bnf)
  1.1299 -      end;
  1.1300 -
  1.1301 -    val one_step_defs =
  1.1302 -      no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
  1.1303 -  in
  1.1304 -    (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
  1.1305 -  end;
  1.1306 -
  1.1307 -fun register_bnf key (bnf, lthy) =
  1.1308 -  (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
  1.1309 -    (fn phi => Data.map (Symtab.default (key, morph_bnf phi bnf))) lthy);
  1.1310 -
  1.1311 -fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
  1.1312 -  (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
  1.1313 -  let
  1.1314 -    fun mk_wits_tac set_maps =
  1.1315 -      K (TRYALL Goal.conjunction_tac) THEN'
  1.1316 -      (case triv_tac_opt of
  1.1317 -        SOME tac => tac set_maps
  1.1318 -      | NONE => fn {context = ctxt, prems} =>
  1.1319 -          unfold_thms_tac ctxt one_step_defs THEN wit_tac {context = ctxt, prems = prems});
  1.1320 -    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
  1.1321 -    fun mk_wit_thms set_maps =
  1.1322 -      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
  1.1323 -        |> Conjunction.elim_balanced (length wit_goals)
  1.1324 -        |> map2 (Conjunction.elim_balanced o length) wit_goalss
  1.1325 -        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
  1.1326 -  in
  1.1327 -    map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
  1.1328 -      goals (map (fn tac => fn {context = ctxt, prems} =>
  1.1329 -        unfold_thms_tac ctxt one_step_defs THEN tac {context = ctxt, prems = prems}) tacs)
  1.1330 -    |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
  1.1331 -  end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs;
  1.1332 -
  1.1333 -val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
  1.1334 -  let
  1.1335 -    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
  1.1336 -    fun mk_triv_wit_thms tac set_maps =
  1.1337 -      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
  1.1338 -        (K (TRYALL Goal.conjunction_tac) THEN' tac set_maps)
  1.1339 -        |> Conjunction.elim_balanced (length wit_goals)
  1.1340 -        |> map2 (Conjunction.elim_balanced o length) wit_goalss
  1.1341 -        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
  1.1342 -    val (mk_wit_thms, nontriv_wit_goals) = 
  1.1343 -      (case triv_tac_opt of
  1.1344 -        NONE => (fn _ => [], map (map (rpair [])) wit_goalss)
  1.1345 -      | SOME tac => (mk_triv_wit_thms tac, []));
  1.1346 -  in
  1.1347 -    Proof.unfolding ([[(defs, [])]])
  1.1348 -      (Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms)
  1.1349 -        (map (single o rpair []) goals @ nontriv_wit_goals) lthy)
  1.1350 -  end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_typ Syntax.read_term NONE
  1.1351 -    Binding.empty Binding.empty [];
  1.1352 -
  1.1353 -fun print_bnfs ctxt =
  1.1354 -  let
  1.1355 -    fun pretty_set sets i = Pretty.block
  1.1356 -      [Pretty.str (mk_setN (i + 1) ^ ":"), Pretty.brk 1,
  1.1357 -          Pretty.quote (Syntax.pretty_term ctxt (nth sets i))];
  1.1358 -
  1.1359 -    fun pretty_bnf (key, BNF {T = T, map = map, sets = sets, bd = bd,
  1.1360 -      live = live, lives = lives, dead = dead, deads = deads, ...}) =
  1.1361 -      Pretty.big_list
  1.1362 -        (Pretty.string_of (Pretty.block [Pretty.str key, Pretty.str ":", Pretty.brk 1,
  1.1363 -          Pretty.quote (Syntax.pretty_typ ctxt T)]))
  1.1364 -        ([Pretty.block [Pretty.str "live:", Pretty.brk 1, Pretty.str (string_of_int live),
  1.1365 -            Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) lives)],
  1.1366 -          Pretty.block [Pretty.str "dead:", Pretty.brk 1, Pretty.str (string_of_int dead),
  1.1367 -            Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) deads)],
  1.1368 -          Pretty.block [Pretty.str (mapN ^ ":"), Pretty.brk 1,
  1.1369 -            Pretty.quote (Syntax.pretty_term ctxt map)]] @
  1.1370 -          List.map (pretty_set sets) (0 upto length sets - 1) @
  1.1371 -          [Pretty.block [Pretty.str (bdN ^ ":"), Pretty.brk 1,
  1.1372 -            Pretty.quote (Syntax.pretty_term ctxt bd)]]);
  1.1373 -  in
  1.1374 -    Pretty.big_list "BNFs:" (map pretty_bnf (Symtab.dest (Data.get (Context.Proof ctxt))))
  1.1375 -    |> Pretty.writeln
  1.1376 -  end;
  1.1377 -
  1.1378 -val _ =
  1.1379 -  Outer_Syntax.improper_command @{command_spec "print_bnfs"}
  1.1380 -    "print all bounded natural functors"
  1.1381 -    (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
  1.1382 -
  1.1383 -val _ =
  1.1384 -  Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
  1.1385 -    "register a type as a bounded natural functor"
  1.1386 -    (parse_opt_binding_colon -- Parse.typ --|
  1.1387 -       (Parse.reserved "map" -- @{keyword ":"}) -- Parse.term --
  1.1388 -       (Scan.option ((Parse.reserved "sets" -- @{keyword ":"}) |--
  1.1389 -         Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) >> the_default []) --|
  1.1390 -       (Parse.reserved "bd" -- @{keyword ":"}) -- Parse.term --
  1.1391 -       (Scan.option ((Parse.reserved "wits" -- @{keyword ":"}) |--
  1.1392 -         Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) >> the_default []) --
  1.1393 -       Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term)
  1.1394 -       >> bnf_cmd);
  1.1395 -
  1.1396 -end;