Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Tools/BNF/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 103 kB image not shown  

Quellcode-Bibliothek bnf_lift.ML   Interaktion und
PortierbarkeitSML

 
(*  Title:      HOL/Tools/BNF/bnf_lift.ML
    Author:     Julian Biendarra, TU Muenchen
    Author:     Basil Fürer, ETH Zurich
    Author:     Joshua Schneider, ETH Zurich
    Author:     Dmitriy Traytel, ETH Zurich
    Copyright   2015, 2019

Lifting of BNFs through typedefs.
*)

signature BNF_LIFT =
sig
  datatype lift_bnf_option =
    Plugins_Option of Proof.context -> Plugin_Name.filter
  | No_Warn_Wits
  | No_Warn_Transfer
  val copy_bnf:
    (((lift_bnf_option list * (binding option * (string * sort option)) list) *
      string) * thm option) * (binding * binding * binding) ->
      local_theory -> local_theory
  val copy_bnf_cmd:
    (((lift_bnf_option list * (binding option * (string * string option)) list) *
      string) * (Facts.ref * Token.src list) option) * (binding * binding * binding) ->
      local_theory -> local_theory
  val lift_bnf:
    ((((lift_bnf_option list * (binding option * (string * sort option)) list) *
      string) * term list option) * thm list option) * (binding * binding * binding) ->
      ({context: Proof.context, prems: thm list} -> tactic) list ->
      local_theory -> local_theory
  val lift_bnf_cmd:
     ((((lift_bnf_option list * (binding option * (string * string option)) list) *
       string) * string list) * (Facts.ref * Token.src list) list option) *
       (binding * binding * binding) -> local_theory -> Proof.state
end

structure BNF_Lift : BNF_LIFT =
struct

open Ctr_Sugar_Tactics
open BNF_Util
open BNF_Comp
open BNF_Def


datatype lift_bnf_option =
  Plugins_Option of Proof.context -> Plugin_Name.filter
| No_Warn_Wits
| No_Warn_Transfer;

datatype equiv_thm = Typedef | Quotient of thm

(** Util **)

fun last2 [x, y] = ([], (x, y))
  | last2 (x :: xs) = last2 xs |>> (fn y => x :: y)
  | last2 [] = raise Match;

fun strip3 thm = (case Term.strip_comb (HOLogic.dest_Trueprop (Thm.prop_of thm)) of
    (_, [x1, x2, x3]) => (x1, x2, x3)
  | _ => error "strip3: wrong number of arguments");

val mk_Free = yield_singleton o mk_Frees;

fun TWICE t = t THEN' t;

fun prove lthy fvars tm tac =
  Goal.prove_sorry lthy (map (fst o dest_Free) fvars) [] tm (fn {context, ...} => tac context);

(** Term construction **)

fun mk_relT aT bT = aT --> bT --> HOLogic.boolT;
fun mk_relcompp r s = let
    val (rT, sT) = apply2 fastype_of (r, s);
    val ((xT, _), (_, zTs)) = apply2 dest_funT (rT, sT);
    val T = rT --> sT --> mk_relT xT (fst (dest_funT zTs));
  in Const (@{const_name relcompp}, T) $ r $ s end;
val mk_OO = fold_rev mk_relcompp;

(* option from sum *)
fun mk_MaybeT T = mk_sumT (HOLogic.unitT, T);
fun mk_Nothing T = BNF_FP_Util.mk_Inl T HOLogic.unit;
val Just_const = BNF_FP_Util.Inr_const HOLogic.unitT;
fun mk_Just tm = Just_const (fastype_of tm) $ tm;
fun Maybe_map_const T =
  let val (xT, yT) = dest_funT T in
    Const (@{const_name map_sum}, (HOLogic.unitT --> HOLogic.unitT) --> T --> mk_MaybeT xT --> mk_MaybeT yT) $
      HOLogic.id_const HOLogic.unitT
  end;
fun mk_Maybe_map tm = Maybe_map_const (fastype_of tm) $ tm;
fun fromJust_const T = Const (@{const_name sum.projr}, mk_MaybeT T --> T)

fun rel_Maybe_const T U =
  Const (@{const_name rel_sum}, (HOLogic.unitT --> HOLogic.unitT --> HOLogic.boolT) -->
    (T --> U --> HOLogic.boolT) --> mk_MaybeT T --> mk_MaybeT U --> HOLogic.boolT) $
  HOLogic.eq_const HOLogic.unitT
fun set_Maybe_const T = Const (@{const_name Basic_BNFs.setr}, mk_MaybeT T --> HOLogic.mk_setT T)

fun Inf_const T = Const (@{const_name Inf}, HOLogic.mk_setT T --> T);

fun Image_const T =
  let
    val relT = HOLogic.mk_setT (HOLogic.mk_prodT (T, T));
    val setT = HOLogic.mk_setT T;
  in Const (@{const_name Image}, relT --> setT --> setT) end;

fun bot_const T = Const (@{const_name bot}, T);

fun mk_insert x S =
  Const (@{const_name Set.insert}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S;

fun mk_vimage f s =
  let val (xT, yT) = dest_funT (fastype_of f) in
    Const (@{const_name vimage}, (xT --> yT) --> HOLogic.mk_setT yT --> HOLogic.mk_setT xT) $ f $ s
  end;

fun mk_case_prod (x, y) tm = let
     val ((x, xT), (y, yT)) = apply2 dest_Free (x, y);
     val prodT = HOLogic.mk_prodT (xT, yT);
   in HOLogic.Collect_const prodT $ (Const (@{const_name case_prod},
       (xT --> yT --> HOLogic.boolT) --> prodT --> HOLogic.boolT) $ absfree (x, xT)
       (absfree (y, yT) tm)) end;

fun mk_Trueprop_implies (ps, c) =
  Logic.list_implies (map HOLogic.mk_Trueprop ps, HOLogic.mk_Trueprop c);

fun mk_Collect (v, tm) = let val (n, T) = dest_Free v in
  HOLogic.mk_Collect (n, T, tm) end;


(** witnesses **)
fun prepare_wits is_quotient RepT wits opts alphas wits_F var_as var_as' sets lthy =
  let
    fun binder_types_until_eq V T =
      let
        fun strip (TU as Type ("fun", [T, U])) = if V = TU then [] else T :: strip U
          | strip T = if V = T then [] else
              error ("Bad type for witness: " ^ quote (Syntax.string_of_typ lthy T));
      in strip T end;

    val Iwits = the_default wits_F (Option.map (map (`(map (fn T =>
      find_index (fn U => T = U) alphas) o binder_types_until_eq RepT o fastype_of))) wits);

    val Iwits = if is_quotient then
        let
          val subsumed_Iwits =
            filter (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) wits_F) Iwits;
          val _ =  if null subsumed_Iwits orelse exists (fn No_Warn_Wits => true | _ => false) opts
            then ()
            else
              let
                val (suffix1, suffix2, be) =
                  (if length subsumed_Iwits = 1 then ("", "", "is") else ("s", "es", "are"))
              in
                subsumed_Iwits
                |> map (Syntax.pretty_typ lthy o fastype_of o snd)
                |> Pretty.big_list
                  ("The following type" ^ suffix1 ^ " of nonemptiness witness" ^ suffix2 ^
                    " of the raw type's BNF " ^ be ^ " subsumed by the existing raw witnesses:")
                |> (fn pt => Pretty.chunks [pt,
                  Pretty.para ("You do not need to lift these subsumed witnesses.")])
                |> Pretty.string_of
                |> warning
              end;
        in
          filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) wits_F) Iwits
        end
      else Iwits;

    val wit_goals = maps (BNF_Def.mk_wit_goals var_as var_as' sets) Iwits;

    val lost_wits = if is_quotient then [] else
      filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) Iwits) wits_F;

    val _ =
      if null lost_wits orelse exists (fn No_Warn_Wits => true | _ => false) opts then ()
      else
        let
          val what = (if is_quotient then "quotient type" else "typedef");
          val (suffix1, suffix2, be) =
            (if length lost_wits = 1 then ("", "", "was") else ("s", "es", "were"))
        in
          lost_wits
          |> map (Syntax.pretty_typ lthy o fastype_of o snd)
          |> Pretty.big_list
            ("The following type" ^ suffix1 ^ " of nonemptiness witness" ^ suffix2 ^
              " of the raw type's BNF " ^ be ^ " lost:")
          |> (fn pt => Pretty.chunks [pt,
            Pretty.para ("You can specify a liftable witness (e.g., a term of one of the above types\
              \ that satisfies the " ^ what ^ "'s invariant)\
              \ using the annotation [wits: <term>].")])
          |> Pretty.string_of
          |> warning
        end;
  in (Iwits, wit_goals) end;


(** transfer theorems **)

fun mk_transfer_thms' bnf_F bnf_G name consts Tss crel_def pcrel_def defs lthy = let

    val live = length (#alphas Tss);

    val (pcrel_tm, crel_tm) = apply2 (Thm.prop_of #> Logic.dest_equals #> fst #> head_of)
      (pcrel_def, crel_def);

    val (var_Qs, var_Rs) = lthy
      |> fold Variable.declare_typ (#alphas Tss @ Library.union (op =) (#deads Tss) (#Ds0 Tss))
      |> mk_Frees "Q" (map2 mk_relT (#alphas Tss) (#betas Tss))
      ||>> mk_Frees "R" (map2 mk_relT (#gammas Tss) (#deltas Tss))
      |> fst;

    (* get the "pcrel :: args_raw => rep => abs \<Rightarrow> bool" term and instantiate types *)
    val (args_raw, (rep, abs)) = pcrel_tm
      |> fastype_of
      |> binder_types
      |> last2;
    val thy = Proof_Context.theory_of lthy;
    val tyenv_match = Vartab.empty
      |> Sign.typ_match thy ((rep, #rep Tss))
      |> Sign.typ_match thy ((abs, #abs Tss));
    val args = map (Envir.subst_type tyenv_match) args_raw;
    val (pcrel_a, pcrel_b) = Envir.subst_term (tyenv_match, Vartab.empty) pcrel_tm
      |> `(subst_atomic_types (#alphas Tss @ #betas Tss ~~ #gammas Tss @ #deltas Tss));

    (* match "crel :: ?a F \<Rightarrow> {a G} \<Rightarrow> bool" with "a G" *)
    val tyenv_match = Vartab.empty |> Sign.typ_match thy
      (crel_tm |> fastype_of |> binder_types |> tl |> hd, #abs Tss);
    val crel_b = Envir.subst_term (tyenv_match, Vartab.empty) crel_tm
      |> subst_atomic_types (#alphas Tss ~~ #betas Tss);
    val crel_d = subst_atomic_types (#betas Tss ~~ #deltas Tss) crel_b;

    (* instantiate pcrel with Qs and Rs*)
    val dead_args = map binder_types args
      |> map (fn [T,U] => if T = U then SOME T else NONE | _ => NONE);
    val parametrize = let
        fun go (SOME T :: dTs) tms = HOLogic.eq_const T :: go dTs tms
          | go (_ :: dTs) (tm :: tms) = tm :: go dTs tms
          | go (_ :: dTs) tms = go dTs tms
          | go _ _ = [];
      in go dead_args end;
    val pcrel_Qs = list_comb (pcrel_b, parametrize var_Qs);
    val pcrel_Rs = list_comb (pcrel_a, parametrize var_Rs);

    (* get the order of the dead variables right *)
    val Ds0 = Library.union (op =) (maps the_list dead_args) (#Ds0 Tss);
    val permute_Ds = (mk_T_of_bnf Ds0 (#betas Tss) bnf_G, nth (binder_types (type_of pcrel_Qs)) 1)
      |> apply2 (fn Type (_, Ts) => Ts | _ => []) |> op~~ |> typ_subst_atomic;
    val Ds0 = map permute_Ds Ds0;

    (* terms for sets of the set_transfer thms *)
    val rel_sets_Q = @{map 3} (fn aT => fn bT => fn Q =>
      mk_rel 1 [aT] [bT] @{term rel_set} $ Q) (#alphas Tss) (#betas Tss) var_Qs;

    (* rewrite rules for pcrel and BNF's relator: "pcrel Q = rel_F OO crel" *)
    fun mk_pcr_rel_F_eq Ts Us pcrel vs crel =
      let
        val thm = HOLogic.mk_Trueprop (HOLogic.mk_eq (pcrel, mk_relcompp (list_comb
          (mk_rel_of_bnf (#deads Tss) (Ts Tss) (Us Tss) bnf_F, vs)) crel));
        fun tac ctxt = unfold_thms_tac ctxt (pcrel_def :: defs @ @{thm id_bnf_apply} ::
          Transfer.get_relator_eq ctxt) THEN (HEADGOAL (rtac ctxt refl))
      in prove lthy vs thm tac |> mk_abs_def end;

    val pcr_rel_F_eqs =
      [mk_pcr_rel_F_eq #alphas #betas pcrel_Qs var_Qs crel_b,
       mk_pcr_rel_F_eq #gammas #deltas pcrel_Rs var_Rs crel_d];

    (* create transfer-relations from term('s type) *)
    fun mk_transfer_rel' i tm =
      let
        fun go T' (n, q) = case T' of
            Type ("fun", [T as Type ("fun", _), U]) =>
              go U (n+1, q) |>> mk_rel_fun (fst (go T (n, q)))
          | Type ("fun", [T, U]) =>
              go T (n, q) |-> (fn x => fn st => go U st |>> mk_rel_fun x)
          | Type (@{type_name bool}, _) => (HOLogic.eq_const HOLogic.boolT, (n, q))
          | Type (@{type_name set}, _) => (nth rel_sets_Q n, (n, q))
          | Type _ => (if q then pcrel_Qs else pcrel_Rs, (n, not q))
          | TFree _ => (nth (if q then var_Qs else var_Rs) n, (n, not q))
          | _ => raise Match
      in go (fastype_of tm) (i, true) |> fst end;

    (* prove transfer rules *)
    fun prove_transfer_thm' i vars new_tm const =
      let
        val tm = HOLogic.mk_Trueprop (mk_transfer_rel' i new_tm $ #raw const $ new_tm);
        val tac = (fn ctxt => unfold_thms_tac ctxt (pcr_rel_F_eqs @ [crel_def]) THEN
          #tac const {Rs=var_Rs,Qs=var_Qs} ctxt);
      in prove lthy vars tm tac end;
    val prove_transfer_thm = prove_transfer_thm' 0;
    (* map transfer: "((Q ===> R) ===> pcr_G Q ===> pcr_G R) map_F' map_G" *)
    val map_G = mk_map_of_bnf Ds0 (#betas Tss) (#deltas Tss) bnf_G;
    val map_transfer = prove_transfer_thm (var_Qs @ var_Rs) map_G (#map consts);
    (* pred_transfer: "((Q ===> (=)) ===> pcr_G Q ===> (=)) pred_F' pred_G" *)
    val pred_G = mk_pred_of_bnf Ds0 (#betas Tss) bnf_G;
    val pred_transfer = #pred consts |> Option.map (fn p =>
      ("pred", [prove_transfer_thm (var_Qs @ var_Rs) pred_G p]));
    (* rel_transfer: "((Q ===> R ===> (=)) ===> pcr_G Q ===> pcr_G R ===> (=)) rel_F' rel_G" *)
    val rel_G = mk_rel_of_bnf Ds0 (#betas Tss) (#deltas Tss) bnf_G;
    val rel_transfer = prove_transfer_thm (var_Qs @ var_Rs) rel_G (#rel consts);
    (* set_transfer: "(pcr_G Q ===> rel_set Q) set_F' set_G" *)
    val sets_G = mk_sets_of_bnf (replicate live Ds0) (replicate live (#betas Tss)) bnf_G;
    fun mk_set_transfer i set_G raw tac = prove_transfer_thm' i var_Qs set_G {raw=raw, tac=tac};
    val sets_transfer = @{map 4} mk_set_transfer
      (0 upto (live-1)) sets_G (#raws (#sets consts)) (#tacs (#sets consts));
    (* export transfer theorems *)
    val transform = Morphism.thm (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) |> map;
    val b = Binding.qualified_name name;
    val qualify =
      let val qs = Binding.path_of b;
      in fold_rev (fn (s, mand) => Binding.qualify mand s) qs end;
    fun mk_binding n = Binding.name (n ^ "_transfer_raw")
      |> Binding.qualify true (Binding.name_of b) |> qualify;
    val notes = [("map", [map_transfer]), ("rel", [rel_transfer])] @ the_list pred_transfer @
      [("set", sets_transfer)] |> map (fn (n, thms) =>
        ((mk_binding n, []), [(transform thms, @{attributes [transfer_rule]})]));

  in lthy |> Local_Theory.notes notes |> snd end;

(* transfer theorems for map, pred (in case of a typedef), rel and sets *)
fun mk_transfer_thms quiet bnf_F bnf_G name consts thm Tss defs lthy = let

    fun mk_crel_def quot_thm =
      (case thm of
        Quotient equiv => @{thm Quotient_crel_quotient} OF [quot_thm, equiv]
      | Typedef => hd ([quot_thm] RL @{thms Quotient_crel_typedef Quotient_crel_typecopy}));
    fun no_quotient _ = [Pretty.para ("No quotient theorem has been registered for " ^
        Binding.name_of (name_of_bnf bnf_G) ^ "."),
      Pretty.para "Use setup_lifting to register a quotient or type definition theorem."];
    fun wrong_quotient T lthy = [Pretty.para ("A wrong quotient theorem has been registered for " ^
        Binding.name_of (name_of_bnf bnf_G) ^ "."),
      Pretty.para ("Expected raw type " ^
        Pretty.string_of (Syntax.pretty_typ lthy (T_of_bnf bnf_F)) ^
        " but the quotient theorem has raw type " ^
        Pretty.string_of (Syntax.pretty_typ lthy T) ^ "."),
      Pretty.para "Use setup_lifting to register a different quotient or type definition theorem."];
    fun pcr_why _ = [Pretty.para ("The pcr_" ^ Binding.name_of (name_of_bnf bnf_G) ^
      " relator has not been defined.")];
    fun warn_transfer why lthy =
      (Pretty.para "The transfer theorems can't be generated:" ::  why lthy)
      |> Pretty.chunks |> Pretty.string_of |> warning |> K lthy;
    fun maybe_warn_transfer why = not quiet ? warn_transfer why;
  in
    case Lifting_Info.lookup_quotients lthy name of
      SOME {pcr_info, quot_thm} =>
        (let
          val crel_def = mk_crel_def quot_thm;
          val rty = Lifting_Util.quot_thm_rty_qty quot_thm |> fst;
          val thy = Proof_Context.theory_of lthy;
        in
          if Sign.typ_instance thy (rty, T_of_bnf bnf_F) then
          (case pcr_info of
            SOME {pcrel_def, ...} =>
              mk_transfer_thms' bnf_F bnf_G name consts Tss crel_def pcrel_def defs lthy
          | _ => maybe_warn_transfer pcr_why lthy)
          else maybe_warn_transfer (wrong_quotient rty) lthy
        end)
    | _ => maybe_warn_transfer no_quotient lthy
  end;


(** typedef_bnf **)

fun mk_typedef_transfer_tacs bnf_F bnf_G thms old_defs
  map_raw rel_raw pred_raw sets_raw = let

    val live = live_of_bnf bnf_G;
    val Abs_G_inverse = @{thm type_definition.Abs_inverse} OF [#typedef thms];
    val Rep_G = @{thm type_definition.Rep} OF [#typedef thms];

    fun common_tac addefs tac = (fn _ => fn ctxt =>
      HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt addefs),
        REPEAT_DETERM o rtac ctxt rel_funI,
        SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply}),
        REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE exE conjE},
        hyp_subst_tac ctxt]) THEN tac ctxt)

    fun map_tac ctxt = (HEADGOAL o EVERY')
      [rtac ctxt @{thm relcomppI},
      etac ctxt (mk_rel_funDN (live+1) (map_transfer_of_bnf bnf_F)),
      REPEAT_DETERM_N live o assume_tac ctxt,
      SELECT_GOAL (unfold_thms_tac ctxt [Abs_G_inverse OF [#map_closed thms] OF [Rep_G]]),
      REPEAT_DETERM o rtac ctxt refl];
    val map_tac = common_tac [#map old_defs] map_tac;

    fun rel_tac ctxt =
      HEADGOAL (etac ctxt (mk_rel_funDN (live+2) (rel_transfer_of_bnf bnf_F)) THEN'
        REPEAT_DETERM_N (live+1) o assume_tac ctxt);
    val rel_tac = common_tac (#rel old_defs :: @{thms vimage2p_def}) rel_tac;

    fun pred_tac ctxt =
      HEADGOAL (etac ctxt (mk_rel_funDN (live+1) (pred_transfer_of_bnf bnf_F)) THEN'
        REPEAT_DETERM_N live o (assume_tac ctxt));
    val pred_tac = common_tac [#pred old_defs] pred_tac;

    fun set_tac set_transfer_thm ctxt =
      HEADGOAL (etac ctxt (rel_funD OF [set_transfer_thm]));
    fun mk_set_tac set_def set_transfer = common_tac [set_def] (set_tac set_transfer);
    val set_tacs = map2 mk_set_tac (#sets old_defs) (set_transfer_of_bnf bnf_F);

  in {map={raw=map_raw,tac=map_tac},rel={raw=rel_raw,tac=rel_tac},
      sets={raws=sets_raw,tacs=set_tacs},pred=SOME{raw=pred_raw,tac=pred_tac}} end;

fun typedef_bnf thm wits specs map_b rel_b pred_b opts lthy =
  let
    val plugins =
      get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
        |> the_default Plugin_Name.default_filter;

    (* extract Rep Abs F RepT AbsT *)
    val (Rep_G, Abs_G, F) = strip3 thm;
    val typ_Abs_G = dest_funT (fastype_of Abs_G);
    val RepT = fst typ_Abs_G; (* F *)
    val AbsT = snd typ_Abs_G; (* G *)
    val AbsT_name = dest_Type_name AbsT;
    val tvs = AbsT |> dest_Type_args |> map (fst o dest_TVar);
    val alpha0s = map (TFree o snd) specs;

    val _ = length tvs = length alpha0s orelse
      error ("Expected " ^ string_of_int (length tvs) ^ " type argument(s) to " ^ quote AbsT_name);

    (* instantiate the new type variables newtvs to oldtvs *)
    val subst = subst_TVars (tvs ~~ alpha0s);
    val typ_subst = typ_subst_TVars (tvs ~~ alpha0s);

    val Rep_G = subst Rep_G;
    val Abs_G = subst Abs_G;
    val F = subst F;
    val RepT = typ_subst RepT;
    val AbsT = typ_subst AbsT;

    fun flatten_tyargs Ass =
      map dest_TFree alpha0s
      |> filter (fn T => exists (fn Ts => member op= Ts T) Ass);

    val Ds0 = filter (is_none o fst) specs |> map snd;

    (* get the bnf for RepT *)
    val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
      bnf_of_typ true Hardly_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
        Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy);

    val set_bs =
      map (fn T => find_index (fn U => T = U) alpha0s) alphas
      |> map (the_default Binding.empty o fst o nth specs);

    val _ = (case alphas of [] => error "No live variables" | _ => ());

    val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds @ #pred_unfolds unfolds;

    (* number of live variables *)
    val live = length alphas;

    (* state the three required properties *)
    val sorts = map Type.sort_of_atyp alphas;
    val names_lthy = fold Variable.declare_typ (alphas @ Library.union (op =) deads (map TFree Ds0)) lthy;
    val (((alphas', betas), betas'), names_lthy) = names_lthy
      |> mk_TFrees' sorts
      ||>> mk_TFrees' sorts
      ||>> mk_TFrees' sorts;

    val map_F = mk_map_of_bnf deads alphas betas bnf_F;

    val (typ_fs, typ_aF) = fastype_of map_F |> strip_typeN live ||> domain_type;
    val typ_pairs = map HOLogic.mk_prodT (alphas ~~ alphas');
    val typ_subst_pair = typ_subst_atomic (alphas ~~ typ_pairs);
    val typ_pair = typ_subst_pair RepT;
    val subst_b = subst_atomic_types (alphas ~~ betas);
    val subst_a' = subst_atomic_types (alphas ~~ alphas');
    val subst_pair = subst_atomic_types (alphas ~~ typ_pairs);
    val aF_set = F;
    val aF_set' = subst_a' F;
    val pairF_set = subst_pair F;
    val bF_set = subst_b F;
    val map_F_fst = mk_map_of_bnf deads typ_pairs alphas bnf_F;
    val map_F_snd = mk_map_of_bnf deads typ_pairs alphas' bnf_F
    val sets_F_pairs = mk_sets_of_bnf (replicate live deads) (replicate live typ_pairs) bnf_F
    val wits_F = mk_wits_of_bnf
      (replicate (nwits_of_bnf bnf_F) deads)
      (replicate (nwits_of_bnf bnf_F) alphas) bnf_F;

    (* val map_closed_F = @{term "\<And>f x. x \<in> F \<Longrightarrow> map_F f x \<in> F"}; *)
    val (var_fs, names_lthy) = mk_Frees "f" typ_fs names_lthy;
    val (var_x, names_lthy) = mk_Frees "x" [typ_aF] names_lthy |>> the_single;
    val mem_x = HOLogic.mk_Trueprop (HOLogic.mk_mem (var_x, aF_set));
    val map_f = list_comb (map_F, var_fs);
    val mem_map = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_f $ var_x, bF_set));
    val imp_map = Logic.mk_implies (mem_x, mem_map);
    val map_closed_F = fold_rev Logic.all var_fs (Logic.all var_x imp_map);

    (* val zip_closed_F =
      @{term "\<And>z. \<lbrakk>map_F fst z \<in> F; map_F snd z \<in> F\<rbrakk> \<Longrightarrow>
        \<exists>z' \<in> F. set_F z' \<subseteq> set_F z \<and> map_F fst z' = map_F fst z \<and> map_F snd z' = map_F snd z"}; *)
    val (var_z, names_lthy) = mk_Free "z" typ_pair names_lthy;
    val (var_z', names_lthy) = mk_Free "z'" typ_pair names_lthy;
    val (pairs, names_lthy) = mk_Frees "tmp" typ_pairs names_lthy;

    fun mk_map mfs f z = Term.list_comb (mfs, map (fst o Term.strip_comb o f) pairs) $ z;
    fun mk_set var = map (fn t => t $ var) sets_F_pairs;

    val (map_fst', map_fst) = apply2 (mk_map map_F_fst HOLogic.mk_fst) (var_z', var_z);
    val (map_snd', map_snd) = apply2 (mk_map map_F_snd HOLogic.mk_snd) (var_z', var_z);
    val mem_map_fst = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_fst, aF_set));
    val mem_map_snd = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_snd, aF_set'));
    val ex_conj = foldr1 HOLogic.mk_conj (map2 mk_leq (mk_set var_z') (mk_set var_z) @
      [HOLogic.mk_eq (map_fst', map_fst), HOLogic.mk_eq (map_snd', map_snd)]);
    val zip_concl = HOLogic.mk_Trueprop (mk_Bex pairF_set (absfree (dest_Free var_z') ex_conj));
    val zip_closed_F = Logic.all var_z (Logic.list_implies ([mem_map_fst, mem_map_snd], zip_concl));

    (* val wit_closed_F = @{term "wit_F a \<in> F"}; *)
    val (var_as, names_lthy) = mk_Frees "a" alphas names_lthy;
    val (var_bs, _) = mk_Frees "a" alphas names_lthy;
    val sets = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F;
    val (Iwits, wit_goals) =
      prepare_wits false RepT wits opts alphas wits_F var_as var_bs sets lthy;
    val wit_closed_Fs =
      Iwits |> map (fn (I, wit_F) =>
        let
          val vars = map (nth var_as) I;
          val wit_a = list_comb (wit_F, vars);
        in fold_rev Logic.all vars (HOLogic.mk_Trueprop (HOLogic.mk_mem (wit_a, aF_set))) end);

    val goals = [map_closed_F, zip_closed_F] @ wit_closed_Fs @
      (case wits of NONE => [] | _ => wit_goals);

    fun after_qed ([map_closed_thm] :: [zip_closed_thm] :: wit_thmss) lthy =
          let
            val (wit_closed_thms, wit_thms) =
              (case wits of
                NONE => (map the_single wit_thmss, wit_thms_of_bnf bnf_F)
              | _ => chop (length wit_closed_Fs) (map the_single wit_thmss))

            (*  construct map set bd rel wit *)
            (* val map_G = @{term "\<lambda>f. Abs_G o map_F f o Rep_G"}; *)
            val Abs_Gb = subst_b Abs_G;
            val map_G = fold_rev lambda var_fs
                (HOLogic.mk_comp (HOLogic.mk_comp (Abs_Gb, map_f), Rep_G));
            val map_raw = fold_rev lambda var_fs map_f;

            (* val sets_G = [@{term "set_F o Rep_G"}]; *)
            val sets_F = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F;
            val sets_G = map (fn set_F => HOLogic.mk_comp (set_F, Rep_G)) sets_F;

            (* val bd_G = @{term "bd_F"}; *)
            val bd_F = mk_bd_of_bnf deads alphas bnf_F;
            val bd_G = bd_F;

            (* val rel_G = @{term "\<lambda>R. BNF_Def.vimage2p Rep_G Rep_G (rel_F R)"}; *)
            val rel_F = mk_rel_of_bnf deads alphas betas bnf_F;
            val (typ_Rs, _) = strip_typeN live (fastype_of rel_F);

            val (var_Rs, names_lthy) = mk_Frees "R" typ_Rs lthy;
            val Rep_Gb = subst_b Rep_G;
            val rel_G = fold_rev absfree (map dest_Free var_Rs)
              (mk_vimage2p Rep_G Rep_Gb $ list_comb (rel_F, var_Rs));
            val rel_raw = fold_rev absfree (map dest_Free var_Rs) (list_comb (rel_F, var_Rs));

            (* val pred_G = @{term "\<lambda>P. pred_F P o Rep_G"}; *)
            val pred_F = mk_pred_of_bnf deads alphas bnf_F;
            val (typ_Ps, _) = strip_typeN live (fastype_of pred_F);

            val (var_Ps, names_lthy) = mk_Frees "P" typ_Ps names_lthy;
            val pred_G = fold_rev absfree (map dest_Free var_Ps)
              (HOLogic.mk_comp (list_comb (pred_F, var_Ps), Rep_G));
            val pred_raw = fold_rev absfree (map dest_Free var_Ps) (list_comb (pred_F, var_Ps));

            (* val wits_G = [@{term "Abs_G o wit_F"}]; *)
            val (var_as, _) = mk_Frees "a" alphas names_lthy;
            val wits_G =
              map (fn (I, wit_F) =>
                let
                  val vs = map (nth var_as) I;
                in fold_rev absfree (map dest_Free vs) (Abs_G $ (list_comb (wit_F, vs))) end)
              Iwits;

            (* tactics *)
            val Rep_thm = thm RS @{thm type_definition.Rep};
            val Abs_inverse_thm = thm RS @{thm type_definition.Abs_inverse};
            val Abs_inject_thm = thm RS @{thm type_definition.Abs_inject};
            val Rep_cases_thm = thm RS @{thm type_definition.Rep_cases};
            val Rep_inverse_thm = thm RS @{thm type_definition.Rep_inverse};

            fun map_id0_tac ctxt =
              HEADGOAL (EVERY' [rtac ctxt ext,
                SELECT_GOAL (unfold_thms_tac ctxt [map_id0_of_bnf bnf_F, id_apply, o_apply,
                  Rep_inverse_thm]),
                rtac ctxt refl]);

            fun map_comp0_tac ctxt =
              HEADGOAL (EVERY' [rtac ctxt ext,
                SELECT_GOAL (unfold_thms_tac ctxt [map_comp0_of_bnf bnf_F, o_apply,
                  Rep_thm RS (map_closed_thm RS Abs_inverse_thm)]),
                rtac ctxt refl]);

            fun map_cong0_tac ctxt =
              HEADGOAL (EVERY' ([SELECT_GOAL (unfold_thms_tac ctxt [o_apply]),
                rtac ctxt (([Rep_thm RS map_closed_thm, Rep_thm RS map_closed_thm] MRS
                  Abs_inject_thm) RS iffD2),
                rtac ctxt (map_cong0_of_bnf bnf_F)] @ replicate live (Goal.assume_rule_tac ctxt)));

            val set_map0s_tac =
              map (fn set_map => fn ctxt =>
                HEADGOAL (EVERY' [rtac ctxt ext,
                  SELECT_GOAL (unfold_thms_tac ctxt [set_map, o_apply,
                    Rep_thm RS (map_closed_thm RS Abs_inverse_thm)]),
                  rtac ctxt refl]))
              (set_map_of_bnf bnf_F);

            fun card_order_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_card_order_of_bnf bnf_F));

            fun cinfinite_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_cinfinite_of_bnf bnf_F));

            fun regularCard_bd_tac ctxt = HEADGOAL (rtac ctxt (bd_regularCard_of_bnf bnf_F));

            val set_bds_tac =
              map (fn set_bd => fn ctxt =>
                HEADGOAL (EVERY' [SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), rtac ctxt set_bd]))
              (set_bd_of_bnf bnf_F);

            fun le_rel_OO_tac ctxt =
              HEADGOAL (EVERY' [rtac ctxt @{thm vimage2p_relcompp_mono},
                rtac ctxt ((rel_OO_of_bnf bnf_F RS sym) RS @{thm ord_eq_le_trans}),
                rtac ctxt @{thm order_refl}]);

            fun rel_OO_Grp_tac ctxt =
              HEADGOAL (EVERY' ([SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt ext))),
                SELECT_GOAL (unfold_thms_tac ctxt (@{thms OO_Grp_alt mem_Collect_eq
                  o_apply vimage2p_def} @ in_rel_of_bnf bnf_F :: @{thms Bex_def mem_Collect_eq})),
                rtac ctxt iffI,
                SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [exE, conjE]))),
                forward_tac ctxt
                  [zip_closed_thm OF (replicate 2 (Rep_thm RSN (2, @{thm ssubst_mem})))],
                assume_tac ctxt,
                SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt @{thms bexE conjE}))),
                etac ctxt Rep_cases_thm,
                hyp_subst_tac ctxt,
                SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt exI))),
                rtac ctxt conjI] @
                replicate live
                  (EVERY' [TRY o rtac ctxt conjI, etac ctxt @{thm order_trans}, assume_tac ctxt]) @
                [SELECT_GOAL (REPEAT_DETERM (HEADGOAL (rtac ctxt conjI))),
                REPEAT_DETERM_N 2 o EVERY'
                  [rtac ctxt (trans OF [iffD2 OF [Abs_inject_thm OF
                      [map_closed_thm OF [Rep_thm], Rep_thm]], Rep_inverse_thm]),
                  etac ctxt trans, assume_tac ctxt],
                SELECT_GOAL (REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt [exE, conjE]))),
                rtac ctxt exI,
                rtac ctxt conjI] @
                replicate (live-1) (rtac ctxt conjI THEN' assume_tac ctxt) @
                [assume_tac ctxt,
                rtac ctxt conjI,
                REPEAT_DETERM_N 2 o EVERY'
                  [rtac ctxt (iffD1 OF [Abs_inject_thm OF [map_closed_thm OF [Rep_thm], Rep_thm]]),
                  etac ctxt (Rep_inverse_thm RS sym RSN (2, trans))]]));

            fun pred_set_tac ctxt =
              HEADGOAL (EVERY'
                [rtac ctxt (pred_set_of_bnf bnf_F RS @{thm arg_cong[of _ _ "\f. f \ _"]} RS trans),
                SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})),
                rtac ctxt refl]);

            fun wit_tac ctxt =
              HEADGOAL (EVERY'
                (map (fn thm => (EVERY'
                  [SELECT_GOAL (unfold_thms_tac ctxt (o_apply ::
                    (wit_closed_thms RL [Abs_inverse_thm]))),
                  dtac ctxt thm, assume_tac ctxt]))
                wit_thms));

            val tactics = [map_id0_tac, map_comp0_tac, map_cong0_tac] @ set_map0s_tac @
              [card_order_bd_tac, cinfinite_bd_tac, regularCard_bd_tac] @ set_bds_tac @
              [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac];

            val (bnf_G, lthy) = bnf_def Hardly_Inline (user_policy Note_Some) true I
              tactics wit_tac NONE map_b rel_b pred_b set_bs
              (((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G)
              lthy;

            val old_defs =
              {sets = set_defs_of_bnf bnf_G, map = map_def_of_bnf bnf_G, rel = rel_def_of_bnf bnf_G,
               pred = pred_def_of_bnf bnf_G};

            val unfold_morphism = Morphism.thm_morphism "BNF" (unfold_thms lthy defs);
            val (bnf_G, lthy) = morph_bnf_defs unfold_morphism bnf_G
              |> (fn bnf => note_bnf_defs bnf lthy);

            val quiet = exists (fn No_Warn_Transfer => true | _ => false) opts;

            val transfer_consts = mk_typedef_transfer_tacs bnf_F bnf_G
              {map_closed=map_closed_thm,typedef=thm} old_defs map_raw rel_raw pred_raw sets_F;
          in
            lthy |> BNF_Def.register_bnf plugins AbsT_name bnf_G |>
              mk_transfer_thms quiet bnf_F bnf_G AbsT_name transfer_consts Typedef
              {abs=typ_subst_atomic (alphas ~~ alphas') AbsT, rep=RepT, Ds0=map TFree Ds0,
               deads = deads, alphas=alphas, betas=alphas', gammas=betas, deltas=betas'} defs
          end
      | after_qed _ _ = raise Match;
  in
    (goals, after_qed, defs, lthy)
  end;


(** quotient_bnf **)

fun mk_quotient_transfer_tacs bnf_F Tss live qthms thms set_F'_thmss old_defs
  inst_REL_pos_distrI map_raw rel_raw sets_raw = let

    fun common_tac ctxt addefs = unfold_thms_tac ctxt (#REL qthms :: addefs) THEN
      (REPEAT_DETERM o HEADGOAL) (rtac ctxt rel_funI);

    (* quotient.map_transfer tactic *)
    val map_F_transfer = map_transfer_of_bnf bnf_F |> mk_rel_funDN (live+1);
    fun map_transfer_q _ ctxt =
      common_tac ctxt (#map old_defs :: @{thms o_def}) THEN
      (HEADGOAL o EVERY') [REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE},
        rtac ctxt @{thm relcomppI[rotated]}, hyp_subst_tac ctxt THEN' EVERY'
        (map (rtac ctxt) [#rel_abs qthms, #map_F_rsp thms, (#rep_abs_rsp qthms), (#reflp qthms)]),
        hyp_subst_tac ctxt, rtac ctxt map_F_transfer, REPEAT_DETERM_N (live+1) o assume_tac ctxt];

    (* quotient.rel_transfer tactic *)
    val rel_F_maps = rel_map_of_bnf bnf_F;
    val rel_F_map_iffD2s = map (fn thm => thm RS @{thm iffD2}) rel_F_maps;
    fun inst_REL_pos_distrI_order_refls vs aTs bTs ctxt = inst_REL_pos_distrI live vs aTs bTs ctxt
      OF (replicate (live+1) asm_rl @ replicate live @{thm order_refl});
    fun rel_transfer_q {Qs, Rs} ctxt = EVERY
      [common_tac ctxt [#rel old_defs, @{thm vimage2p_def}],
      HEADGOAL (rtac ctxt iffI),
      (REPEAT_DETERM o ALLGOALS)
        (eresolve_tac ctxt @{thms exE conjE relcomppE} ORELSE' hyp_subst_tac ctxt),
      (HEADGOAL o EVERY')
        [REPEAT_DETERM o dtac ctxt @{thm rel_fun_rel_OO1},
        rtac ctxt (inst_REL_pos_distrI 0 (map mk_conversep Qs) (#betas Tss) (#alphas Tss) ctxt),
        rtac ctxt @{thm relcomppI},
        rtac ctxt (#symp qthms),
        rtac ctxt (#map_F_rsp thms),
        rtac ctxt (#rep_abs_rsp qthms),
        rtac ctxt (#reflp qthms),
        rtac ctxt @{thm relcomppI},
        rtac ctxt (rel_flip_of_bnf bnf_F RS @{thm iffD1}),
        rtac ctxt (nth rel_F_map_iffD2s 0),
        rtac ctxt (nth rel_F_map_iffD2s 1),
        etac ctxt (#rel_monoD_rotated thms)],
      (REPEAT_DETERM_N live o HEADGOAL o EVERY')
        [rtac ctxt @{thm predicate2I},
        rtac ctxt @{thm conversepI},
        rtac ctxt @{thm Basic_BNFs.rel_sum_simps(4)[THEN iffD2]},
        etac ctxt @{thm conversepI}],
      (HEADGOAL o EVERY')
        [rtac ctxt (inst_REL_pos_distrI_order_refls Rs (#gammas Tss) (#deltas Tss) ctxt),
        (SELECT_GOAL o REPEAT_DETERM o HEADGOAL) (etac ctxt @{thm relcomppI}),
        rtac ctxt @{thm relcomppI[rotated]},
        rtac ctxt (#map_F_rsp thms),
        rtac ctxt (#rep_abs_rsp qthms OF [#reflp qthms]),
        SELECT_GOAL (unfold_thms_tac ctxt (@{thms rel_sum_simps} @ rel_F_maps)),
        assume_tac ctxt],
      (REPEAT_DETERM_N (2*live) o HEADGOAL)
        (rtac ctxt @{thm rel_sum_eq2_nonempty} ORELSE' rtac ctxt @{thm rel_sum_eq3_nonempty}),
      (REPEAT_DETERM_N live)
        (unfold_thms_tac ctxt @{thms sum.rel_compp[symmetric] eq_OO} THEN
        HEADGOAL (etac ctxt @{thm sum.rel_mono[OF order_refl]})),
      (HEADGOAL o EVERY')
        [(SELECT_GOAL o REPEAT_DETERM o HEADGOAL) (dtac ctxt @{thm rel_fun_rel_OO2}),
        rtac ctxt (inst_REL_pos_distrI 0 Qs (#alphas Tss) (#betas Tss) ctxt),
        rtac ctxt @{thm relcomppI},
        rtac ctxt (#reflp qthms),
        rtac ctxt @{thm relcomppI},
        rtac ctxt (nth rel_F_map_iffD2s 0),
        rtac ctxt (nth rel_F_map_iffD2s 1),
        etac ctxt (#rel_monoD_rotated thms)],
      (REPEAT_DETERM_N live o HEADGOAL o EVERY')
        [rtac ctxt @{thm predicate2I}, rtac ctxt @{thm rel_sum.intros(2)}, assume_tac ctxt],
      (HEADGOAL o EVERY')
        [rtac ctxt
          (inst_REL_pos_distrI_order_refls (map mk_conversep Rs) (#deltas Tss) (#gammas Tss) ctxt),
        rtac ctxt @{thm relcomppI},
        etac ctxt (rotate_prems 1 (#transp qthms)),
        rtac ctxt (#map_F_rsp thms),
        rtac ctxt (#rep_abs_rsp qthms OF [#reflp qthms]),
        etac ctxt @{thm relcomppI},
        rtac ctxt @{thm relcomppI},
        etac ctxt (#transp qthms),
        rtac ctxt (#symp qthms),
        rtac ctxt (#map_F_rsp thms),
        rtac ctxt (#rep_abs_rsp qthms),
        rtac ctxt (#reflp qthms),
        rtac ctxt @{thm relcomppI[rotated]},
        rtac ctxt (#reflp qthms),
        rtac ctxt (rel_flip_of_bnf bnf_F RS @{thm iffD1}),
        rtac ctxt (nth rel_F_map_iffD2s 0),
        rtac ctxt (nth rel_F_map_iffD2s 1),
        etac ctxt (#rel_monoD_rotated thms)],
      (REPEAT_DETERM_N live o HEADGOAL o EVERY')
        [rtac ctxt @{thm predicate2I},
        rtac ctxt @{thm conversepI},
        rtac ctxt @{thm rel_sum.intros(2)},
        etac ctxt @{thm conversepI}],
      (REPEAT_DETERM_N (2*live) o HEADGOAL)
        (rtac ctxt @{thm rel_sum_eq2_nonempty} ORELSE' rtac ctxt @{thm rel_sum_eq3_nonempty}),
      (REPEAT_DETERM_N live o EVERY)
        [unfold_thms_tac ctxt @{thms sum.rel_compp[symmetric] eq_OO},
        HEADGOAL (etac ctxt @{thm sum.rel_mono[OF order_refl]})]];

    (* quotient.set_transfer tactics *)
    fun set_transfer_q set_G_def set_F'_thms _ ctxt =
      let val set_F'_rsp = mk_rel_funDN 1 (#set_F'_respect set_F'_thms) in
        common_tac ctxt (set_G_def :: @{thms o_def}) THEN
        (HEADGOAL o EVERY')
          [etac ctxt @{thm relcomppE}, hyp_subst_tac ctxt,
          SELECT_GOAL (unfold_thms_tac ctxt
            [set_F'_rsp OF [#rep_abs qthms] OF [#reflp qthms], @{thm rel_set_def}]),
          dtac ctxt (#rel_F_rel_F' thms), rtac ctxt conjI] THEN
        (REPEAT_DETERM_N 2 o HEADGOAL o EVERY')
          [SELECT_GOAL (unfold_thms_tac ctxt [#rel_F'_set thms]),
          REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
          REPEAT_DETERM o dtac ctxt (mk_sym set_F'_rsp),
          SELECT_GOAL (unfold_thms_tac ctxt [#set_map_F' set_F'_thms]),
          rtac ctxt @{thm ballI}, dtac ctxt @{thm equalityD1[THEN subsetD]}, assume_tac ctxt,
          SELECT_GOAL (unfold_thms_tac ctxt @{thms image_iff}),
          etac ctxt @{thm bexE}, dtac ctxt set_mp, assume_tac ctxt,
          SELECT_GOAL (unfold_thms_tac ctxt @{thms mem_Collect_eq case_prod_beta}),
          rtac ctxt @{thm bexI}, hyp_subst_tac ctxt, assume_tac ctxt, etac ctxt @{thm hypsubst},
          etac ctxt @{thm imageI}, assume_tac ctxt]
      end;
  in
     {map={raw=map_raw, tac=map_transfer_q},
      rel={raw=rel_raw, tac=rel_transfer_q},
      sets={raws=sets_raw,tacs=map2 set_transfer_q (#sets old_defs) set_F'_thmss},
      pred=NONE}
  end;


fun quotient_bnf (equiv_thm, quot_thm) wits specs map_b rel_b pred_b opts lthy =
  let
    (* extract rep_G and abs_G *)
    val (equiv_rel, abs_G, rep_G) = strip3 quot_thm;
    val (repT, absT) = dest_funT (fastype_of abs_G); (* ("?'a F", "?'a G") *)
    val absT_name = dest_Type_name absT;

    val tvs = map (fst o dest_TVar) (dest_Type_args absT);
    val _ = length tvs = length specs orelse
      error ("Expected " ^ string_of_int (length tvs) ^
        " type argument" ^ (if (length tvs) = 1 then "" else "s") ^ " to " ^ quote absT_name);

    (* instantiate TVars *)
    val alpha0s = map (TFree o snd) specs;
    val typ_subst = typ_subst_TVars (tvs ~~ alpha0s);
    val (repT, absT) = apply2 typ_subst (repT, absT);

    (* get the bnf for RepT *)
    val Ds0 = filter (is_none o fst) specs |> map snd;

    fun flatten_tyargs Ass =
      map dest_TFree alpha0s |> filter (fn T => exists (fn Ts => member op= Ts T) Ass);

    val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
      bnf_of_typ true Hardly_Inline (Binding.qualify true absT_name) flatten_tyargs
        [] Ds0 repT ((empty_comp_cache, empty_unfolds), lthy);
    val live = length alphas;
    val _ = (if live = 0 then error "No live variables" else ());

    val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds;
    val set_bs =
      map (fn T => find_index (fn U => T = U) alpha0s) alphas
      |> map (the_default Binding.empty o fst o nth specs);

    (* create and instantiate all the needed type variables *)
    val subst = subst_TVars (tvs ~~ alpha0s);
    val (abs_G, rep_G) = apply2 subst (abs_G, rep_G);

    val sorts = map Type.sort_of_atyp alphas;
    val (((betas, gammas), deltas), names_lthy) = fold Variable.declare_typ (alphas @ deads) lthy
      |> mk_TFrees' sorts
      ||>> mk_TFrees' sorts
      ||>> mk_TFrees' sorts;

    fun subst_Ts tm Ts = subst_atomic_types (alphas ~~ Ts) tm;
    val subst_b = subst_atomic_types (alphas ~~ betas);
    val subst_Maybe = subst_atomic_types o map (swap o `mk_MaybeT);
    val equiv_rel_a = subst equiv_rel;
    val map_F = mk_map_of_bnf deads alphas betas bnf_F;
    val rel_F_ab = mk_rel_of_bnf deads alphas betas bnf_F;
    val rel_F_bc = mk_rel_of_bnf deads betas gammas bnf_F;
    val rel_F_ac = mk_rel_of_bnf deads alphas gammas bnf_F;
    val rel_F_option = mk_rel_of_bnf deads (map mk_MaybeT alphas) (map mk_MaybeT betas) bnf_F;
    val sets_F = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F;
    val wits_F = mk_wits_of_bnf
      (replicate (nwits_of_bnf bnf_F) deads) (replicate (nwits_of_bnf bnf_F) alphas) bnf_F;

    val (typ_fs, (typ_aF, typ_bF)) = strip_typeN live (fastype_of map_F) ||> dest_funT;
    val typ_MaybeF = typ_subst_atomic (alphas ~~ map mk_MaybeT alphas) typ_aF;
    val typ_a_sets = map HOLogic.mk_setT alphas;
    val typ_pairs = map HOLogic.mk_prodT (alphas ~~ betas);
    val typ_fs' = map (typ_subst_atomic (map (swap o `mk_MaybeT) betas)) typ_fs;

    (* create all the needed variables *)
    val ((((((((((((((((((((((var_Ps, var_Qs), var_Rs), var_x), var_x'), var_y), var_y'), var_mx),
      var_As), var_As'), var_Ss), var_Bs), var_as), var_as'), var_bs), var_bs'), var_R), var_fs),
      var_fs'), var_gs), var_gs'), var_z), var_ts) = names_lthy
        |> mk_Frees "Ps" (map2 mk_relT alphas betas)
        ||>> mk_Frees "Qs" (map2 mk_relT betas gammas)
        ||>> mk_Frees "Rs" (map2 mk_relT alphas gammas)
        ||>> mk_Free "x" typ_aF
        ||>> mk_Free "x'" typ_aF
        ||>> mk_Free "y" typ_bF
        ||>> mk_Free "y'" (typ_subst_atomic (alphas ~~ gammas) typ_aF)
        ||>> mk_Free "mx" typ_MaybeF
        ||>> mk_Frees "As" typ_a_sets
        ||>> mk_Frees "As'" typ_a_sets
        ||>> mk_Frees "Ss" (map HOLogic.mk_setT typ_a_sets)
        ||>> mk_Frees "Bs" (map HOLogic.mk_setT betas)
        ||>> mk_Frees "as" alphas
        ||>> mk_Frees "as'" alphas
        ||>> mk_Frees "bs" betas
        ||>> mk_Frees "bs'" betas
        ||>> mk_Free "R" (typ_aF --> typ_bF --> HOLogic.boolT)
        ||>> mk_Frees "fs" typ_fs
        ||>> mk_Frees "fs'" typ_fs'
        ||>> mk_Frees "gs" typ_fs
        ||>> mk_Frees "gs'" typ_fs'
        ||>> mk_Free "z" (typ_subst_atomic (alphas ~~ typ_pairs) typ_aF)
        ||>> mk_Frees "ts" typ_pairs
        |> fst;

    (* create local definitions `b = tm` with n arguments *)
    fun suffix tm s = Long_Name.base_name (dest_Const_name tm) ^ s;
    fun define lthy b n tm =
      let
        val b = Binding.qualify true absT_name (Binding.qualified_name b);
        val ((tm, (_, def)), (lthy, lthy_old)) = lthy
          |> (snd o Local_Theory.begin_nested)
          |> Local_Theory.define_internal (((Binding.concealed b, NoSyn), (Binding.empty_atts, tm)))
          ||> `Local_Theory.end_nested;
        val phi = Proof_Context.export_morphism lthy_old lthy;
        val tm = Term.subst_atomic_types
          (map (`(Morphism.typ phi)) (alphas @ betas @ gammas @ map TFree Ds0))
          (Morphism.term phi tm);
        val def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def));
      in ({def=def, tm=tm}, lthy) end;

    (* internally use REL, not the user-provided definition *)
    val (REL, lthy) = define lthy "REL" 0 equiv_rel_a;
    val REL_def = sym RS eq_reflection OF [#def REL];
    fun REL_rewr_all ctxt thm = Conv.fconv_rule
      (Conv.top_conv (fn _ => Conv.try_conv (Conv.rewr_conv REL_def)) ctxt) thm;

    val equiv_rel_a' = equiv_rel_a;
    val equiv_rel_a  = #tm REL;
    val (equiv_rel_b, equiv_rel_c) = apply2 (subst_Ts equiv_rel_a) (betas, gammas);

    (* rel_pos_distr: @{term "\<And>A B.
      A \<circ>\<circ> B \<noteq> bot \<Longrightarrow> REL \<circ>\<circ> rel_F A \<circ>\<circ> REL \<circ>\<circ> rel_F B \<circ>\<circ> REL \<le> REL \<circ>\<circ> rel_F (A \<circ>\<circ> B) \<circ>\<circ> REL"} *)
    fun compp_not_bot comp aT cT = let
        val T = mk_relT aT cT;
        val mk_eq = HOLogic.eq_const T;
      in HOLogic.mk_not (mk_eq $ comp $ bot_const T) end;
    val ab_comps = map2 mk_relcompp var_Ps var_Qs;
    val ne_comps = (@{map 3} compp_not_bot ab_comps alphas gammas);
    val ab_prem = foldr1 HOLogic.mk_conj ne_comps;

    val REL_pos_distrI_tm = let
        val le_relcomps = map2 mk_leq ab_comps var_Rs;
        val assm = mk_OO [equiv_rel_a, list_comb (rel_F_ab, var_Ps),
                    equiv_rel_b, list_comb (rel_F_bc, var_Qs)] equiv_rel_c;
        val concl = mk_OO [equiv_rel_a, list_comb (rel_F_ac, var_Rs)] equiv_rel_c;
      in
        mk_Trueprop_implies
          ([assm $ var_x $ var_y'] @ ne_comps @ le_relcomps, concl $ var_x $ var_y')
      end;

    val ab_concl = mk_leq
      (mk_OO [list_comb (rel_F_ab, var_Ps), equiv_rel_b] (list_comb (rel_F_bc, var_Qs)))
      (mk_OO [equiv_rel_a, list_comb (rel_F_ac, ab_comps)] (equiv_rel_c));
    val ab_imp = Logic.mk_implies (apply2 HOLogic.mk_Trueprop (ab_prem, ab_concl));
    val rel_pos_distr = fold_rev Logic.all (var_Ps @ var_Qs) ab_imp;

    (* {(x, y) . REL x y} *)
    fun mk_rel_pairs rel = mk_case_prod (var_x, var_x') (rel $ var_x $ var_x')
    val rel_pairs = mk_rel_pairs equiv_rel_a;

    (* rel_Inter: \<And>S. \<lbrakk> S \<noteq> {}; \<Inter>S \<noteq> {} \<rbrakk> \<Longrightarrow>
      (\<Inter>A\<in>S. {(x, y). REL x y} `` {x. set_F x \<subseteq> A}) \<subseteq> {(x, y). REL x y} `` {x. set_F x \<subseteq> \<Inter>S} *)
    fun rel_Inter_from_set_F (var_A, var_S) set_F = let

      val typ_aset = fastype_of var_A;

      (* \<Inter>S *)
      val inter_S = Inf_const typ_aset $ var_S;

      (* [S \<noteq> {}, \<Inter>S \<noteq> {}] *)
      fun not_empty x = let val ty = fastype_of x
        in HOLogic.mk_not (HOLogic.mk_eq (x, bot_const ty)) end;
      val prems = map (HOLogic.mk_Trueprop o not_empty) [var_S, inter_S];

      (* {x. set_F x \<subseteq> A} *)
      val setF_sub_A = mk_in [var_A] [set_F] typ_aF;

      (* {x. set_F x \<subseteq> \<Inter>S} *)
      val setF_sub_S = mk_in [inter_S] [set_F] typ_aF;

      val lhs = Inf_const (HOLogic.mk_setT typ_aF) $ (mk_image
        (absfree (dest_Free var_A) (Image_const typ_aF $ rel_pairs $ setF_sub_A)) $ var_S);
      val rhs = Image_const typ_aF $ rel_pairs $ setF_sub_S;
      val concl = HOLogic.mk_Trueprop (mk_leq lhs rhs);

     in Logic.all var_S (Logic.list_implies (prems, concl)) end;

    val rel_Inters = map2 rel_Inter_from_set_F (var_As ~~ var_Ss) sets_F;

    (* map_F_Just = map_F Just *)
    val map_F_Just = let
        val option_tys = map mk_MaybeT alphas;
        val somes = map Just_const alphas;
      in list_comb (subst_atomic_types (betas ~~ option_tys) map_F, somes) end;

    fun mk_set_F'_tm typ_a set_F =
      let
        val typ_aset = HOLogic.mk_setT typ_a;

        (* set_F' x = (\<Inter>y\<in>{y. REL (map_F Just x) y}. UNION (set_F y) set_Maybe) *)
        val sbind = mk_UNION (subst_Maybe alphas set_F $ var_mx) (set_Maybe_const typ_a);
        val collection = HOLogic.Collect_const typ_MaybeF $ absfree (dest_Free var_mx)
          (subst_Maybe alphas equiv_rel_a $ (map_F_Just $ var_x) $ var_mx);
        val set_F'_tm = lambda var_x
          (Inf_const typ_aset $ (mk_image (absfree (dest_Free var_mx) sbind) $ collection));
      in
        set_F'_tm
      end

    val sets = mk_sets_of_bnf (replicate live deads) (replicate live alphas) bnf_F;
    val sets' = map2 mk_set_F'_tm alphas sets;

    val (Iwits, wit_goals) =
      prepare_wits true repT wits opts alphas wits_F var_as var_as' sets' lthy;

    val goals = rel_pos_distr :: rel_Inters @
      (case wits of NONE => [] | _ => wit_goals);

    val plugins =
      get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) |>
      the_default Plugin_Name.default_filter;

    fun after_qed thmss lthy =
      (case thmss of [rel_pos_distr_thm0] :: thmss =>
        let
          val equiv_thm' = REL_rewr_all lthy equiv_thm;
          val rel_pos_distr_thm =
            @{thm equivp_add_relconj} OF [equiv_thm', equiv_thm', rel_pos_distr_thm0];

          val (rel_Inter_thms, wit_thmss) = apply2 (fn f => flat (f live thmss)) (take, drop);

          (* construct map_G, sets_G, bd_G, rel_G and wits_G *)

          (* map_G f = abs_G o map_F f o rep_G *)
          val map_G = fold_rev lambda var_fs (HOLogic.mk_comp (HOLogic.mk_comp
            (subst_Ts abs_G betas, list_comb (map_F, var_fs)), rep_G));
          val map_raw = fold_rev lambda var_fs (list_comb (map_F, var_fs))
            |> subst_atomic_types (betas ~~ gammas);

          (* Define set_G and the three auxiliary definitions (set_F', F_in, F_in') *)
          fun mk_set_G var_A set_F lthy = let
              val typ_a = HOLogic.dest_setT (fastype_of var_A);
              val set_F'_tm = mk_set_F'_tm typ_a set_F

              val (set_F', lthy) = define lthy (suffix set_F "'") 1 set_F'_tm;

              (* set_G = set_F' o rep_G *)
              val set_G = HOLogic.mk_comp (#tm set_F', rep_G);

              (* F_in A = {x. set_F x \<subseteq> A} *)
              val F_in_tm = lambda var_A (mk_in [var_A] [set_F] typ_aF);
              val (F_in, lthy) = define lthy (suffix set_F "_in") 1 F_in_tm;

              (* F_in' A = map_F Inr -` ({(x, y). REL x y} `` F_in (insert (Inl ()) (Inr ` A))) *)
              val F_in' = lambda var_A (mk_vimage map_F_Just (Image_const typ_MaybeF $
                subst_Maybe alphas rel_pairs $ (subst_Maybe alphas (#tm F_in) $ mk_insert
                  (mk_Nothing typ_a) (mk_image (Just_const typ_a) $ var_A))));
              val (F_in', lthy) = define lthy (suffix set_F "_in'") 1 F_in';

            in ((set_G, {set_F'=set_F', F_in=F_in, F_in'=F_in'}), lthy) end;

          val ((sets_G, set_F'_aux_defs), lthy) =
            @{fold_map 2} mk_set_G var_As sets_F lthy |>> split_list;

          (* bd_G = bd_F *)
          val bd_G = mk_bd_of_bnf deads alphas bnf_F;

          (* rel_F' A =
               BNF_Def.vimage2p (map_F Just) (map_F Just) ((\<cong>) OO rel_F (rel_Maybe A) OO (\<cong>)) *)
          val rel_Maybes = @{map 3} (fn v => fn aT => fn bT => rel_Maybe_const aT bT $ v);
          val rel_F'_tm = let val equiv_equiv_rel_option = subst_Ts equiv_rel_a' o map mk_MaybeT in
            mk_vimage2p map_F_Just (subst_atomic_types (alphas ~~ betas) map_F_Just) $
              mk_OO [equiv_equiv_rel_option alphas, list_comb (rel_F_option, rel_Maybes var_Ps alphas betas)]
              (equiv_equiv_rel_option betas) end;

          val (rel_F', lthy) =
            define lthy (suffix rel_F_ab "'") (live+2) (fold_rev lambda var_Ps rel_F'_tm);

          (* rel_G A = vimage2p rep_G rep_G (rel_F' A) *)
          val rel_G = fold_rev lambda var_Ps (mk_vimage2p rep_G (subst_Ts rep_G betas) $ rel_F'_tm);
          val rel_raw = fold_rev lambda var_Ps rel_F'_tm
            |> subst_atomic_types (betas ~~ gammas);

          (* auxiliary lemmas *)
          val bd_card_order = bd_card_order_of_bnf bnf_F;
          val bd_cinfinite = bd_cinfinite_of_bnf bnf_F;
          val bd_regularCard = bd_regularCard_of_bnf bnf_F;
          val in_rel = in_rel_of_bnf bnf_F;
          val map_F_comp = map_comp_of_bnf bnf_F;
          val map_F_comp0 = map_comp0_of_bnf bnf_F;
          val map_F_cong = map_cong_of_bnf bnf_F;
          val map_F_id0 = map_id0_of_bnf bnf_F;
          val map_F_id = map_id_of_bnf bnf_F;
          val rel_conversep = rel_conversep_of_bnf bnf_F;
          val rel_flip = rel_flip_of_bnf bnf_F;
          val rel_eq_onp = rel_eq_onp_of_bnf bnf_F;
          val rel_Grp = rel_Grp_of_bnf bnf_F;
          val rel_OO = rel_OO_of_bnf bnf_F;
          val rel_map = rel_map_of_bnf bnf_F;
          val rel_refl_strong = rel_refl_strong_of_bnf bnf_F;
          val set_bd_thms = set_bd_of_bnf bnf_F;
          val set_map_thms = set_map_of_bnf bnf_F;



          (* map_F_respect: @{term "((=) ===> REL ===> REL) map_F map_F"} *)
          val map_F_respect = HOLogic.mk_Trueprop (fold_rev mk_rel_fun (map2 (fn xT => fn yT =>
            HOLogic.eq_const (xT --> yT)) alphas betas @ [equiv_rel_a]) (equiv_rel_b) $ map_F $ map_F);

          fun map_F_respect_tac ctxt =
            HEADGOAL (EVERY'
             [REPEAT_DETERM_N (live + 1) o rtac ctxt @{thm rel_funI}, hyp_subst_tac ctxt,
              rtac ctxt (BNF_FP_Util.split_conj_prems live rel_pos_distr_thm0 OF
                replicate live @{thm Grp_conversep_nonempty} RS rev_mp),
              rtac ctxt impI, dtac ctxt @{thm predicate2D}, etac ctxt @{thm relcomppI2[rotated]},
              rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]},
              REPEAT_DETERM o resolve_tac ctxt @{thms CollectI conjI subset_UNIV},
              rtac ctxt (rel_flip RS iffD2),
              rtac ctxt (rel_Grp RS @{thm predicate2_eqD} RS iffD2), rtac ctxt @{thm GrpI[OF refl]},
              REPEAT_DETERM o resolve_tac ctxt @{thms CollectI conjI subset_UNIV},
              SELECT_GOAL (unfold_thms_tac ctxt (rel_eq_onp :: @{thms Grp_conversep_eq_onp})),
              etac ctxt @{thm predicate2D[OF rel_conj_eq_onp, rotated]},
              rtac ctxt equiv_thm']);

          val map_F_respect_thm = prove lthy [] map_F_respect map_F_respect_tac;

          val rel_funD = mk_rel_funDN (live+1);
          val map_F_rsp = (rel_funD map_F_respect_thm) OF (replicate live refl);
          fun map_F_rsp_of tms ctxt = (infer_instantiate' ctxt (NONE :: NONE
            :: map (SOME o Thm.cterm_of ctxt) tms) map_F_rsp)

          val qthms = let
              fun equivp_THEN thm = REL_rewr_all lthy equiv_thm RS thm;
              fun Quotient3_THEN thm = REL_rewr_all lthy quot_thm RS thm;
            in
              {abs_rep = Quotient3_THEN @{thm Quotient3_abs_rep},
               rel_abs = Quotient3_THEN @{thm Quotient3_rel_abs},
               rep_abs = Quotient3_THEN @{thm Quotient3_rep_abs},
               rep_reflp = Quotient3_THEN @{thm Quotient3_rep_reflp},
               rep_abs_rsp = Quotient3_THEN @{thm rep_abs_rsp},
               reflp = equivp_THEN @{thm equivp_reflp},
               symp = equivp_THEN @{thm equivp_symp},
               transp = equivp_THEN @{thm equivp_transp},
               REL = REL_def}
            end;

          (* lemma REL_OO_REL_left: REL OO REL OO R = REL OO R *)
          val REL_OO_REL_left_thm = let
              val tm = mk_Trueprop_eq
                (mk_OO [equiv_rel_a, equiv_rel_a] var_R, mk_relcompp equiv_rel_a var_R)
              fun tac ctxt = HEADGOAL (EVERY'
                [rtac ctxt ext,
                rtac ctxt ext,
                rtac ctxt iffI,
                TWICE (etac ctxt @{thm relcomppE}),
                rtac ctxt @{thm relcomppI},
                etac ctxt (#transp qthms),
                TWICE (assume_tac ctxt),
                etac ctxt @{thm relcomppE},
                etac ctxt @{thm relcomppI},
                rtac ctxt @{thm relcomppI},
                rtac ctxt (#reflp qthms),
                assume_tac ctxt]);
            in prove lthy [var_R] tm tac end;

          (* Generate theorems related to the setters *)
          val map_F_fs = list_comb (map_F, var_fs);

          (* aset aset asetset bset typ_b typ_b *)
          fun mk_set_F'_thmss (((((var_A, var_A'), var_S), var_B), var_b), var_b')
                set_F {set_F', F_in, F_in'} rel_Inter_thm set_map_F_thm (idx, vf) =
            let
              val (var_f, var_fs') = case vf of
                (f :: fs) => (f, fs)
                | _ => error "won't happen";

              val typ_a = fastype_of var_f |> dest_funT |> fst;
              val typ_b = fastype_of var_b;
              val (typ_asetset, typ_aset) = `HOLogic.mk_setT (fastype_of var_A);

              val map_F_fs_x = map_F_fs $ var_x;

              (* F_in'_mono: A \<subseteq> B \<Longrightarrow> F_in' A \<subseteq> F_in' B *)
              val F_in'_mono_tm = mk_Trueprop_implies
                ([mk_leq var_A var_A'], mk_leq (#tm F_in' $ var_A) (#tm F_in' $ var_A'));
              fun F_in'_mono_tac ctxt =
                unfold_thms_tac ctxt [#def F_in', #def F_in] THEN
                HEADGOAL (EVERY'
                  [rtac ctxt @{thm subsetI},
                  etac ctxt @{thm vimageE},
                  etac ctxt @{thm ImageE},
                  etac ctxt @{thm CollectE},
                  etac ctxt @{thm CollectE},
                  dtac ctxt @{thm case_prodD},
                  hyp_subst_tac ctxt,
                  rtac ctxt @{thm vimageI [OF refl]},
                  rtac ctxt @{thm ImageI},
                  rtac ctxt @{thm CollectI},
                  rtac ctxt @{thm case_prodI},
                  assume_tac ctxt ORELSE' rtac ctxt refl,
                  rtac ctxt @{thm CollectI},
                  etac ctxt @{thm subset_trans},
                  etac ctxt @{thm insert_mono [OF image_mono]}]);
              val F_in'_mono_thm = prove lthy [var_A, var_A'] F_in'_mono_tm F_in'_mono_tac;

              (* F_in'_Inter: F_in' (\<Inter>S) = (\<Inter>A\<in>S. F_in' A) *)
              val F_in'_Inter_tm = mk_Trueprop_eq ((#tm F_in' $ (Inf_const typ_aset $ var_S)),
                (Inf_const (HOLogic.mk_setT typ_aF) $ (mk_image (#tm F_in') $ var_S)));
              fun F_in'_Inter_tac ctxt =
                Local_Defs.unfold_tac ctxt [#def F_in', #def F_in]
                THEN HEADGOAL (rtac ctxt (infer_instantiate' ctxt
                  [SOME (Thm.cterm_of ctxt (HOLogic.mk_eq (var_S, bot_const typ_asetset)))] @{thm case_split})
                  THEN' EVERY' [
                    hyp_subst_tac ctxt,
                    SELECT_GOAL
                      (unfold_thms_tac ctxt @{thms Inter_empty INT_empty UNIV_sum_unit_conv}),
                    rtac ctxt @{thm set_eqI},
                    rtac ctxt iffI,
                    rtac ctxt @{thm UNIV_I},
                    rtac ctxt @{thm vimageI [OF refl]},
                    rtac ctxt @{thm ImageI},
                    rtac ctxt @{thm CollectI},
                    rtac ctxt @{thm case_prodI},
                    rtac ctxt (#reflp qthms),
                    rtac ctxt @{thm CollectI},
                    rtac ctxt subset_UNIV,
                    etac ctxt @{thm exE[OF ex_in_conv[THEN iffD2]]},
                    EqSubst.eqsubst_tac ctxt [0] @{thms image_INT[of _ UNIV _ id, simplified]},
                    rtac ctxt @{thm inj_Inr},
                    assume_tac ctxt,
                    SELECT_GOAL (unfold_thms_tac ctxt @{thms INT_extend_simps vimage_INT[symmetric]}),
                    rtac ctxt @{thm arg_cong2[where f=vimage, OF refl]},
                    rtac ctxt @{thm equalityI},
                    rtac ctxt @{thm subsetI},
                    rtac ctxt @{thm InterI},
                    etac ctxt @{thm imageE},
                    etac ctxt @{thm ImageE},
                    etac ctxt @{thm CollectE},
                    etac ctxt @{thm CollectE},
                    dtac ctxt @{thm case_prodD},
                    hyp_subst_tac ctxt,
                    rtac ctxt @{thm ImageI[OF CollectI]},
                    etac ctxt @{thm case_prodI} ORELSE' (SELECT_GOAL
                      (unfold_thms_tac ctxt @{thms prod.case}) THEN' rtac ctxt @{thm refl}),
                    rtac ctxt @{thm CollectI},
                    etac ctxt @{thm subset_trans},
                    etac ctxt @{thm INT_lower[OF imageI]},
                    rtac ctxt (@{thm subset_trans} OF [asm_rl, rel_Inter_thm]),
                    K (unfold_thms_tac ctxt @{thms image_image}),
                    rtac ctxt @{thm subset_refl},
                    K (unfold_thms_tac ctxt @{thms INT_extend_simps ex_in_conv[symmetric]}),
                    rtac ctxt exI,
                    rtac ctxt @{thm imageI},
                    assume_tac ctxt,
                    rtac ctxt exI,
                    rtac ctxt @{thm InterI},
                    etac ctxt @{thm imageE},
                    hyp_subst_tac ctxt,
                    rtac ctxt @{thm insertI1}]);

              val F_in'_Inter_thm = prove lthy [var_S] F_in'_Inter_tm F_in'_Inter_tac;

              (* set_F'_respect: (REL ===> (=)) set_F' set_F' *)
              val set_F'_respect_tm = HOLogic.mk_Trueprop (mk_rel_fun equiv_rel_a
                (HOLogic.eq_const typ_aset) $ #tm set_F' $ #tm set_F');
              fun set_F'_respect_tac ctxt = unfold_thms_tac ctxt (#def set_F' :: @{thms rel_fun_def})
                THEN HEADGOAL (EVERY'
                  [TWICE (rtac ctxt allI),
                  rtac ctxt impI,
                  dtac ctxt (map_F_rsp_of (map Just_const alphas) ctxt),
                  rtac ctxt @{thm INF_cong},
                  rtac ctxt @{thm Collect_eqI},
                  rtac ctxt iffI,
                  etac ctxt (#transp qthms OF [#symp qthms]),
                  assume_tac ctxt,
                  etac ctxt (#transp qthms),
                  assume_tac ctxt,
                  rtac ctxt refl]);

              (* F_in'_alt2: F_in' A = {x. set_F' x \<subseteq> A} *)
              val F_in'_alt2_tm = mk_Trueprop_eq
                (#tm F_in' $ var_A, mk_in [var_A] [#tm set_F'] typ_aF);
              fun F_in'_alt2_tac ctxt = HEADGOAL (rtac ctxt @{thm equalityI} THEN'
                (Subgoal.FOCUS o K) (unfold_thms_tac ctxt (map #def [set_F', F_in', F_in])) ctxt
                THEN' EVERY'
                  [rtac ctxt @{thm subsetI},
                  rtac ctxt @{thm CollectI},
                  rtac ctxt @{thm subsetI},
                  dtac ctxt @{thm vimageD},
                  etac ctxt @{thm ImageE},
                  etac ctxt @{thm CollectE},
                  etac ctxt @{thm CollectE},
                  dtac ctxt @{thm case_prodD},
                  dtac ctxt @{thm InterD},
                  rtac ctxt @{thm imageI[OF CollectI]},
                  etac ctxt (#symp qthms),
                  etac ctxt @{thm UnionE},
                  etac ctxt @{thm imageE},
                  hyp_subst_tac ctxt,
                  etac ctxt @{thm subset_lift_sum_unitD},
                  etac ctxt @{thm setr.cases},
                  hyp_subst_tac ctxt,
                  assume_tac ctxt])
                THEN unfold_thms_tac ctxt [#def set_F'] THEN
                (HEADGOAL o EVERY')
                  [rtac ctxt @{thm subsetI},
                  etac ctxt @{thm CollectE},
                  etac ctxt (@{thm subsetD} OF [F_in'_mono_thm]),
                  EqSubst.eqsubst_tac ctxt [0] [F_in'_Inter_thm],
                  rtac ctxt @{thm InterI}] THEN
                REPEAT_DETERM (HEADGOAL (etac ctxt @{thm imageE} THEN' hyp_subst_tac ctxt)) THEN
                (HEADGOAL o EVERY')
                  [etac ctxt @{thm CollectE},
                  SELECT_GOAL (unfold_thms_tac ctxt (map #def [F_in', F_in])),
                  rtac ctxt @{thm vimageI[OF refl]},
                  rtac ctxt @{thm ImageI},
                  rtac ctxt @{thm CollectI},
                  rtac ctxt @{thm case_prodI},
                  etac ctxt (#symp qthms),
                  rtac ctxt @{thm CollectI},
                  rtac ctxt @{thm subsetI},
                  rtac ctxt @{thm sum_insert_Inl_unit},
                  assume_tac ctxt,
                  hyp_subst_tac ctxt,
                  rtac ctxt @{thm imageI},
                  rtac ctxt @{thm UnionI},
                  rtac ctxt @{thm imageI},
                  assume_tac ctxt,
                  rtac ctxt @{thm setr.intros[OF refl]}];
              val F_in'_alt2_thm = prove lthy [var_A] F_in'_alt2_tm F_in'_alt2_tac;

              (* set_F'_alt: set_F' x = \<Inter>{A. x \<in> F_in' A} *)
              val set_F'_alt_tm = mk_Trueprop_eq (#tm set_F' $ var_x,
                Inf_const typ_aset $ mk_Collect (var_A, HOLogic.mk_mem (var_x, #tm F_in' $ var_A)));
              fun set_F'_alt_tac ctxt = unfold_thms_tac ctxt [F_in'_alt2_thm]
                THEN HEADGOAL (EVERY'
                  [rtac ctxt @{thm set_eqI},
                  rtac ctxt iffI,
                  rtac ctxt @{thm InterI},
                  etac ctxt @{thm CollectE},
                  etac ctxt @{thm CollectE},
                  dtac ctxt @{thm subsetD},
                  assume_tac ctxt,
                  assume_tac ctxt,
                  etac ctxt @{thm InterD},
                  rtac ctxt @{thm CollectI},
                  rtac ctxt @{thm CollectI},
                  rtac ctxt @{thm subset_refl}]);
              val set_F'_alt_thm = prove lthy [var_x] set_F'_alt_tm set_F'_alt_tac;

              (* map_F_in_F_in'I: x \<in> F_in' B \<Longrightarrow> map_F f x \<in> F_in' (f ` B) *)
              val map_F_in_F_in'I_tm = mk_Trueprop_implies ([HOLogic.mk_mem (var_x, #tm F_in' $ var_A')],
                HOLogic.mk_mem (map_F_fs_x, subst_b (#tm F_in') $ (mk_image var_f $ var_A')));
              fun map_F_in_F_in'I_tac ctxt =
                Local_Defs.unfold_tac ctxt (#def F_in' :: #def F_in :: @{thms Bex_def vimage_def Image_iff}) THEN
                HEADGOAL (EVERY'
--> --------------------

--> maximum size reached

--> --------------------

99%


¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.34Bemerkung:  (vorverarbeitet)  ¤

*Bot Zugriff




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.