Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
authorkuncar
Fri Dec 05 14:14:36 2014 +0100 (2014-12-05)
changeset 602294cd6462c1fda
parent 60228 32dd7adba5a4
child 60230 4857d553c52c
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
src/HOL/Lifting.thy
src/HOL/Lifting_Set.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/Lifting/lifting_util.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Lifting.thy	Fri Dec 05 14:14:36 2014 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Fri Dec 05 14:14:36 2014 +0100
     1.3 @@ -265,6 +265,13 @@
     1.4    shows "part_equivp (eq_onp P)"
     1.5    using typedef_to_part_equivp [OF assms] by simp
     1.6  
     1.7 +lemma type_definition_Quotient_not_empty: "Quotient (eq_onp P) Abs Rep T \<Longrightarrow> \<exists>x. P x"
     1.8 +unfolding eq_onp_def by (drule Quotient_rep_reflp) blast
     1.9 +
    1.10 +lemma type_definition_Quotient_not_empty_witness: "Quotient (eq_onp P) Abs Rep T \<Longrightarrow> P (Rep undefined)"
    1.11 +unfolding eq_onp_def by (drule Quotient_rep_reflp) blast
    1.12 +
    1.13 +
    1.14  text {* Generating transfer rules for quotients. *}
    1.15  
    1.16  context
    1.17 @@ -538,6 +545,12 @@
    1.18  
    1.19  end
    1.20  
    1.21 +(* needed for lifting_def_code_dt.ML (moved from Lifting_Set) *)
    1.22 +lemma right_total_UNIV_transfer: 
    1.23 +  assumes "right_total A"
    1.24 +  shows "(rel_set A) (Collect (Domainp A)) UNIV"
    1.25 +  using assms unfolding right_total_def rel_set_def Domainp_iff by blast
    1.26 +
    1.27  subsection {* ML setup *}
    1.28  
    1.29  ML_file "Tools/Lifting/lifting_util.ML"
    1.30 @@ -555,6 +568,7 @@
    1.31  ML_file "Tools/Lifting/lifting_term.ML"
    1.32  ML_file "Tools/Lifting/lifting_def.ML"
    1.33  ML_file "Tools/Lifting/lifting_setup.ML"
    1.34 +ML_file "Tools/Lifting/lifting_def_code_dt.ML"
    1.35  
    1.36  hide_const (open) POS NEG
    1.37  
     2.1 --- a/src/HOL/Lifting_Set.thy	Fri Dec 05 14:14:36 2014 +0100
     2.2 +++ b/src/HOL/Lifting_Set.thy	Fri Dec 05 14:14:36 2014 +0100
     2.3 @@ -205,10 +205,7 @@
     2.4    shows "(rel_set A ===> rel_set A ===> op =) (op \<subseteq>) (op \<subseteq>)"
     2.5    unfolding subset_eq [abs_def] by transfer_prover
     2.6  
     2.7 -lemma right_total_UNIV_transfer[transfer_rule]: 
     2.8 -  assumes "right_total A"
     2.9 -  shows "(rel_set A) (Collect (Domainp A)) UNIV"
    2.10 -  using assms unfolding right_total_def rel_set_def Domainp_iff by blast
    2.11 +declare right_total_UNIV_transfer[transfer_rule]
    2.12  
    2.13  lemma UNIV_transfer [transfer_rule]:
    2.14    assumes "bi_total A"
     3.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Dec 05 14:14:36 2014 +0100
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Dec 05 14:14:36 2014 +0100
     3.3 @@ -23,6 +23,7 @@
     3.4    val mk_lift_const_of_lift_def: typ -> lift_def -> term
     3.5  
     3.6    type config = { notes: bool }
     3.7 +  val map_config: (bool -> bool) -> config -> config
     3.8    val default_config: config
     3.9  
    3.10    val generate_parametric_transfer_rule:
    3.11 @@ -48,10 +49,6 @@
    3.12      config -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 
    3.13      local_theory -> lift_def * local_theory
    3.14  
    3.15 -  val lift_def_cmd:
    3.16 -    (binding * string option * mixfix) * string * (Facts.ref * Token.src list) list ->
    3.17 -    local_theory -> Proof.state
    3.18 -
    3.19    val can_generate_code_cert: thm -> bool
    3.20  end
    3.21  
    3.22 @@ -123,6 +120,7 @@
    3.23  (* Config *)
    3.24  
    3.25  type config = { notes: bool };
    3.26 +fun map_config f1 { notes = notes } = { notes = f1 notes }
    3.27  val default_config = { notes = true };
    3.28  
    3.29  (* Reflexivity prover *)
    3.30 @@ -744,76 +742,4 @@
    3.31  fun lift_def config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def config)
    3.32    var qty rhs tac par_thms lthy
    3.33  
    3.34 -(*
    3.35 -
    3.36 -  lifting_definition command. It opens a proof of a corresponding respectfulness 
    3.37 -  theorem in a user-friendly, readable form. Then add_lift_def is called internally.
    3.38 -
    3.39 -*)
    3.40 -
    3.41 -fun lift_def_cmd (raw_var, rhs_raw, par_xthms) lthy =
    3.42 -  let
    3.43 -    val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy 
    3.44 -    val var = (binding, mx)
    3.45 -    val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
    3.46 -    val par_thms = Attrib.eval_thms lthy par_xthms
    3.47 -    val (goal, after_qed) = prepare_lift_def (add_lift_def default_config) var qty rhs par_thms lthy
    3.48 -  in
    3.49 -    Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy
    3.50 -  end
    3.51 -
    3.52 -fun quot_thm_err ctxt (rty, qty) pretty_msg =
    3.53 -  let
    3.54 -    val error_msg = cat_lines
    3.55 -       ["Lifting failed for the following types:",
    3.56 -        Pretty.string_of (Pretty.block
    3.57 -         [Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]),
    3.58 -        Pretty.string_of (Pretty.block
    3.59 -         [Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]),
    3.60 -        "",
    3.61 -        (Pretty.string_of (Pretty.block
    3.62 -         [Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))]
    3.63 -  in
    3.64 -    error error_msg
    3.65 -  end
    3.66 -
    3.67 -fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
    3.68 -  let
    3.69 -    val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt 
    3.70 -    val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
    3.71 -    val error_msg = cat_lines
    3.72 -       ["Lifting failed for the following term:",
    3.73 -        Pretty.string_of (Pretty.block
    3.74 -         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]),
    3.75 -        Pretty.string_of (Pretty.block
    3.76 -         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]),
    3.77 -        "",
    3.78 -        (Pretty.string_of (Pretty.block
    3.79 -         [Pretty.str "Reason:", 
    3.80 -          Pretty.brk 2, 
    3.81 -          Pretty.str "The type of the term cannot be instantiated to",
    3.82 -          Pretty.brk 1,
    3.83 -          Pretty.quote (Syntax.pretty_typ ctxt rty_forced),
    3.84 -          Pretty.str "."]))]
    3.85 -    in
    3.86 -      error error_msg
    3.87 -    end
    3.88 -
    3.89 -fun lift_def_cmd_with_err_handling (raw_var, rhs_raw, par_xthms) lthy =
    3.90 -  (lift_def_cmd (raw_var, rhs_raw, par_xthms) lthy
    3.91 -    handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
    3.92 -    handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) => 
    3.93 -      check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw)
    3.94 -
    3.95 -(* parser and command *)
    3.96 -val liftdef_parser =
    3.97 -  (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
    3.98 -    --| @{keyword "is"} -- Parse.term -- 
    3.99 -      Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1
   3.100 -val _ =
   3.101 -  Outer_Syntax.local_theory_to_proof @{command_keyword lift_definition}
   3.102 -    "definition for constants over the quotient type"
   3.103 -      (liftdef_parser >> lift_def_cmd_with_err_handling)
   3.104 -
   3.105 -
   3.106  end (* structure *)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Fri Dec 05 14:14:36 2014 +0100
     4.3 @@ -0,0 +1,647 @@
     4.4 +(*  Title:      HOL/Tools/Lifting/lifting_def_code_dt.ML
     4.5 +    Author:     Ondrej Kuncar
     4.6 +
     4.7 +Workaround that allows us to execute lifted constants that have
     4.8 +as a return type a datatype containing a subtype; lift_definition command
     4.9 +*)
    4.10 +
    4.11 +signature LIFTING_DEF_CODE_DT =
    4.12 +sig
    4.13 +  type rep_isom_data
    4.14 +  val isom_of_rep_isom_data: rep_isom_data -> term
    4.15 +  val transfer_of_rep_isom_data: rep_isom_data -> thm
    4.16 +  val bundle_name_of_rep_isom_data: rep_isom_data -> string
    4.17 +  val pointer_of_rep_isom_data: rep_isom_data -> string
    4.18 +
    4.19 +  type code_dt
    4.20 +  val rty_of_code_dt: code_dt -> typ
    4.21 +  val qty_of_code_dt: code_dt -> typ
    4.22 +  val wit_of_code_dt: code_dt -> term
    4.23 +  val wit_thm_of_code_dt: code_dt -> thm
    4.24 +  val rep_isom_data_of_code_dt: code_dt -> rep_isom_data option
    4.25 +  val morph_code_dt: morphism -> code_dt -> code_dt
    4.26 +  val mk_witness_of_code_dt: typ -> code_dt -> term
    4.27 +  val mk_rep_isom_of_code_dt: typ -> code_dt -> term option
    4.28 +
    4.29 +  val code_dt_of: Proof.context -> typ * typ -> code_dt option
    4.30 +  val code_dt_of_global: theory -> typ * typ -> code_dt option
    4.31 +  val all_code_dt_of: Proof.context -> code_dt list
    4.32 +  val all_code_dt_of_global: theory -> code_dt list
    4.33 +
    4.34 +  type config_code_dt = { code_dt: bool, lift_config: Lifting_Def.config }
    4.35 +  val default_config_code_dt: config_code_dt
    4.36 +
    4.37 +  val add_lift_def_code_dt:
    4.38 +    config_code_dt -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory ->
    4.39 +      Lifting_Def.lift_def * local_theory
    4.40 +
    4.41 +  val lift_def_code_dt:
    4.42 +    config_code_dt -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list ->
    4.43 +    local_theory -> Lifting_Def.lift_def * local_theory
    4.44 +
    4.45 +  val lift_def_cmd:
    4.46 +    string list * (binding * string option * mixfix) * string * (Facts.ref * Token.src list) list ->
    4.47 +    local_theory -> Proof.state
    4.48 +end
    4.49 +
    4.50 +structure Lifting_Def_Code_Dt: LIFTING_DEF_CODE_DT =
    4.51 +struct
    4.52 +
    4.53 +open Ctr_Sugar_Util BNF_Util BNF_FP_Util BNF_FP_Def_Sugar Lifting_Def Lifting_Util
    4.54 +
    4.55 +(** data structures **)
    4.56 +
    4.57 +(* all type variables in qty are in rty *)
    4.58 +datatype rep_isom_data = REP_ISOM of { isom: term, transfer: thm, bundle_name: string, pointer: string }
    4.59 +fun isom_of_rep_isom_data (REP_ISOM rep_isom) = #isom rep_isom;
    4.60 +fun transfer_of_rep_isom_data (REP_ISOM rep_isom) = #transfer rep_isom;
    4.61 +fun bundle_name_of_rep_isom_data (REP_ISOM rep_isom) = #bundle_name rep_isom;
    4.62 +fun pointer_of_rep_isom_data (REP_ISOM rep_isom) = #pointer rep_isom;
    4.63 +
    4.64 +datatype code_dt = CODE_DT of { rty: typ, qty: typ, wit: term, wit_thm: thm,
    4.65 +  rep_isom_data: rep_isom_data option };
    4.66 +fun rty_of_code_dt (CODE_DT code_dt) = #rty code_dt;
    4.67 +fun qty_of_code_dt (CODE_DT code_dt) = #qty code_dt;
    4.68 +fun wit_of_code_dt (CODE_DT code_dt) = #wit code_dt;
    4.69 +fun wit_thm_of_code_dt (CODE_DT code_dt) = #wit_thm code_dt;
    4.70 +fun rep_isom_data_of_code_dt (CODE_DT code_dt) = #rep_isom_data code_dt;
    4.71 +fun rty_equiv (T, U) = Type.raw_instance (T, U) andalso Type.raw_instance (U, T);
    4.72 +val code_dt_eq = rty_equiv o apply2 rty_of_code_dt;
    4.73 +fun term_of_code_dt code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt |> HOLogic.mk_prodT
    4.74 +  |> Net.encode_type |> single;
    4.75 +
    4.76 +(* modulo renaming, typ must contain TVars *)
    4.77 +fun is_code_dt_of_type (rty, qty) code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt
    4.78 +  |> HOLogic.mk_prodT |> curry rty_equiv (HOLogic.mk_prodT (rty, qty));
    4.79 +
    4.80 +fun mk_rep_isom_data isom transfer bundle_name pointer =
    4.81 +  REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer}
    4.82 +
    4.83 +fun mk_code_dt rty qty wit wit_thm rep_isom_data =
    4.84 +  CODE_DT { rty = rty, qty = qty, wit = wit, wit_thm = wit_thm, rep_isom_data = rep_isom_data };
    4.85 +
    4.86 +fun map_rep_isom_data f1 f2 f3 f4
    4.87 +  (REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer }) =
    4.88 +  REP_ISOM { isom = f1 isom, transfer = f2 transfer, bundle_name = f3 bundle_name, pointer = f4 pointer };
    4.89 +
    4.90 +fun map_code_dt f1 f2 f3 f4 f5 f6 f7 f8
    4.91 +  (CODE_DT {rty = rty, qty = qty, wit = wit, wit_thm = wit_thm, rep_isom_data = rep_isom_data}) =
    4.92 +  CODE_DT {rty = f1 rty, qty = f2 qty, wit = f3 wit, wit_thm = f4 wit_thm,
    4.93 +    rep_isom_data = Option.map (map_rep_isom_data f5 f6 f7 f8) rep_isom_data};
    4.94 +
    4.95 +fun update_rep_isom isom transfer binding pointer i = mk_code_dt (rty_of_code_dt i) (qty_of_code_dt i)
    4.96 +  (wit_of_code_dt i) (wit_thm_of_code_dt i) (SOME (mk_rep_isom_data isom transfer binding pointer))
    4.97 +
    4.98 +fun morph_code_dt phi =
    4.99 +  let
   4.100 +    val mty = Morphism.typ phi
   4.101 +    val mterm = Morphism.term phi
   4.102 +    val mthm = Morphism.thm phi
   4.103 +  in
   4.104 +    map_code_dt mty mty mterm mthm mterm mthm I I
   4.105 +  end
   4.106 +
   4.107 +val transfer_code_dt = morph_code_dt o Morphism.transfer_morphism;
   4.108 +
   4.109 +structure Data = Generic_Data
   4.110 +(
   4.111 +  type T = code_dt Item_Net.T
   4.112 +  val empty = Item_Net.init code_dt_eq term_of_code_dt
   4.113 +  val extend = I
   4.114 +  val merge = Item_Net.merge
   4.115 +);
   4.116 +
   4.117 +fun code_dt_of_generic context (rty, qty) =
   4.118 +  let
   4.119 +    val typ = HOLogic.mk_prodT (rty, qty)
   4.120 +    val prefiltred = Item_Net.retrieve_matching (Data.get context) (Net.encode_type typ)
   4.121 +  in
   4.122 +    prefiltred |> filter (is_code_dt_of_type (rty, qty))
   4.123 +    |> map (transfer_code_dt (Context.theory_of context)) |> find_first (fn _ => true)
   4.124 +  end;
   4.125 +
   4.126 +fun code_dt_of ctxt (rty, qty) =
   4.127 +  let
   4.128 +    val sch_rty = Logic.type_map (singleton (Variable.polymorphic ctxt)) rty
   4.129 +    val sch_qty = Logic.type_map (singleton (Variable.polymorphic ctxt)) qty
   4.130 +  in
   4.131 +    code_dt_of_generic (Context.Proof ctxt) (sch_rty, sch_qty)
   4.132 +  end;
   4.133 +
   4.134 +fun code_dt_of_global thy (rty, qty) =
   4.135 +  let
   4.136 +    val sch_rty = Logic.varifyT_global rty
   4.137 +    val sch_qty = Logic.varifyT_global qty
   4.138 +  in
   4.139 +    code_dt_of_generic (Context.Theory thy) (sch_rty, sch_qty)
   4.140 +  end;
   4.141 +
   4.142 +fun all_code_dt_of_generic context =
   4.143 +    Item_Net.content (Data.get context) |> map (transfer_code_dt (Context.theory_of context));
   4.144 +
   4.145 +val all_code_dt_of = all_code_dt_of_generic o Context.Proof;
   4.146 +val all_code_dt_of_global = all_code_dt_of_generic o Context.Theory;
   4.147 +
   4.148 +fun update_code_dt code_dt =
   4.149 +  Local_Theory.declaration {syntax = false, pervasive = true}
   4.150 +    (fn phi => Data.map (Item_Net.update (morph_code_dt phi code_dt)));
   4.151 +
   4.152 +fun mk_match_of_code_dt qty code_dt = Vartab.empty |> Type.raw_match (qty_of_code_dt code_dt, qty)
   4.153 +  |> Vartab.dest |> map (fn (x, (S, T)) => (TVar (x, S), T));
   4.154 +
   4.155 +fun mk_witness_of_code_dt qty code_dt =
   4.156 +  Term.subst_atomic_types (mk_match_of_code_dt qty code_dt) (wit_of_code_dt code_dt)
   4.157 +
   4.158 +fun mk_rep_isom_of_code_dt qty code_dt = Option.map
   4.159 +  (isom_of_rep_isom_data #> Term.subst_atomic_types (mk_match_of_code_dt qty code_dt))
   4.160 +    (rep_isom_data_of_code_dt code_dt)
   4.161 +
   4.162 +
   4.163 +(** unique name for a type **)
   4.164 +
   4.165 +fun var_name name sort = if sort = @{sort "{type}"} orelse sort = [] then ["x" ^ name]
   4.166 +  else "x" ^ name :: "x_" :: sort @ ["x_"];
   4.167 +
   4.168 +fun concat_Tnames (Type (name, ts)) = name :: maps concat_Tnames ts
   4.169 +  | concat_Tnames (TFree (name, sort)) = var_name name sort
   4.170 +  | concat_Tnames (TVar ((name, _), sort)) = var_name name sort;
   4.171 +
   4.172 +fun unique_Tname (rty, qty) =
   4.173 +  let
   4.174 +    val Tnames = map Long_Name.base_name (concat_Tnames rty @ ["x_x"] @ concat_Tnames qty);
   4.175 +  in
   4.176 +    fold (Binding.qualify false) (tl Tnames) (Binding.name (hd Tnames))
   4.177 +  end;
   4.178 +
   4.179 +(** witnesses **)
   4.180 +
   4.181 +fun mk_undefined T = Const (@{const_name undefined}, T);
   4.182 +
   4.183 +fun mk_witness quot_thm =
   4.184 +  let
   4.185 +    val wit_thm = quot_thm RS @{thm type_definition_Quotient_not_empty_witness}
   4.186 +    val wit = quot_thm_rep quot_thm $ mk_undefined (quot_thm_rty_qty quot_thm |> snd)
   4.187 +  in
   4.188 +    (wit, wit_thm)
   4.189 +  end
   4.190 +
   4.191 +(** config **)
   4.192 +
   4.193 +type config_code_dt = { code_dt: bool, lift_config: config }
   4.194 +val default_config_code_dt = { code_dt = false, lift_config = default_config }
   4.195 +
   4.196 +
   4.197 +(** Main code **)
   4.198 +
   4.199 +val ld_no_notes = { notes = false }
   4.200 +
   4.201 +fun comp_lift_error _ _ = error "Composition of abstract types has not been implemented yet."
   4.202 +
   4.203 +fun lift qty (quot_thm, (lthy, rel_eq_onps)) =
   4.204 +  let
   4.205 +    val quot_thm = Lifting_Term.force_qty_type lthy qty quot_thm
   4.206 +    val (rty, qty) = quot_thm_rty_qty quot_thm;
   4.207 +  in
   4.208 +    if is_none (code_dt_of lthy (rty, qty)) then
   4.209 +      let
   4.210 +        val (wit, wit_thm) = (mk_witness quot_thm
   4.211 +          handle THM _ => error ("code_dt: " ^ quote (Tname qty) ^ " was not defined as a subtype."))
   4.212 +        val code_dt = mk_code_dt rty qty wit wit_thm NONE
   4.213 +      in
   4.214 +        (quot_thm, (update_code_dt code_dt lthy |> Local_Theory.restore, rel_eq_onps))
   4.215 +      end
   4.216 +    else
   4.217 +      (quot_thm, (lthy, rel_eq_onps))
   4.218 +  end;
   4.219 +
   4.220 +fun case_tac rule ctxt i st =
   4.221 +  (Subgoal.FOCUS_PARAMS (fn {params, ...} => HEADGOAL(rtac
   4.222 +    (Ctr_Sugar_Util.cterm_instantiate_pos [SOME (params |> hd |> snd)] rule))) ctxt i st);
   4.223 +
   4.224 +fun bundle_name_of_bundle_binding binding phi context  =
   4.225 +  Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi binding);
   4.226 +
   4.227 +fun prove_schematic_quot_thm actions ctxt = Lifting_Term.prove_schematic_quot_thm actions
   4.228 + (Lifting_Info.get_quotients ctxt) ctxt
   4.229 +
   4.230 +fun prove_code_dt (rty, qty) lthy =
   4.231 +  let
   4.232 +    val (fold_quot_thm: (local_theory * thm list) Lifting_Term.fold_quot_thm) =
   4.233 +      { constr = constr, lift = lift, comp_lift = comp_lift_error };
   4.234 +  in prove_schematic_quot_thm fold_quot_thm lthy (rty, qty) (lthy, []) |> snd end
   4.235 +and add_lift_def_code_dt config var qty rhs rsp_thm par_thms lthy =
   4.236 +  let
   4.237 +    fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   4.238 +    fun ret_rel_conv conv ctm =
   4.239 +      case (Thm.term_of ctm) of
   4.240 +        Const (@{const_name "rel_fun"}, _) $ _ $ _ =>
   4.241 +          binop_conv2 Conv.all_conv conv ctm
   4.242 +        | _ => conv ctm
   4.243 +    fun R_conv rel_eq_onps = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
   4.244 +      then_conv Transfer.bottom_rewr_conv rel_eq_onps
   4.245 +
   4.246 +    val (ret_lift_def, lthy) = add_lift_def (#lift_config config) var qty rhs rsp_thm par_thms lthy
   4.247 +  in
   4.248 +    if (not (#code_dt config) orelse (code_eq_of_lift_def ret_lift_def <> NONE_EQ))
   4.249 +    then  (ret_lift_def, lthy)
   4.250 +    else
   4.251 +      let
   4.252 +        val lift_def = inst_of_lift_def lthy qty ret_lift_def
   4.253 +        val rty = rty_of_lift_def lift_def
   4.254 +        val rty_ret = body_type rty
   4.255 +        val qty_ret = body_type qty
   4.256 +
   4.257 +        val (lthy, rel_eq_onps) = prove_code_dt (rty_ret, qty_ret) lthy
   4.258 +        val code_dt = code_dt_of lthy (rty_ret, qty_ret)
   4.259 +      in
   4.260 +        if is_none code_dt orelse is_none (rep_isom_data_of_code_dt (the code_dt)) then (ret_lift_def, lthy)
   4.261 +        else
   4.262 +          let
   4.263 +            val code_dt = the code_dt
   4.264 +            val rhs = dest_comb (rhs_of_lift_def lift_def) |> snd
   4.265 +            val rep_isom_data = code_dt |> rep_isom_data_of_code_dt |> the
   4.266 +            val qty_code_dt_bundle_name = bundle_name_of_rep_isom_data rep_isom_data
   4.267 +            val rep_isom = mk_rep_isom_of_code_dt qty_ret code_dt |> the
   4.268 +            val lthy = Bundle.includes [qty_code_dt_bundle_name] lthy
   4.269 +            fun qty_isom_of_rep_isom rep = rep |> dest_Const |> snd |> domain_type
   4.270 +            val qty_isom = qty_isom_of_rep_isom rep_isom
   4.271 +            val f'_var = (Binding.suffix_name "_aux" (fst var), NoSyn);
   4.272 +            val f'_qty = strip_type qty |> fst |> rpair qty_isom |> op --->
   4.273 +            val f'_rsp_rel = Lifting_Term.equiv_relation lthy (rty, f'_qty);
   4.274 +            val rsp = rsp_thm_of_lift_def lift_def
   4.275 +            val rel_eq_onps_conv = HOLogic.Trueprop_conv (ret_rel_conv (R_conv rel_eq_onps))
   4.276 +            val rsp_norm = Conv.fconv_rule rel_eq_onps_conv rsp
   4.277 +            val f'_rsp_goal = HOLogic.mk_Trueprop (f'_rsp_rel $ rhs $ rhs);
   4.278 +            val f'_rsp = Goal.prove_sorry lthy [] [] f'_rsp_goal
   4.279 +              (K (HEADGOAL (CONVERSION (rel_eq_onps_conv) THEN' rtac rsp_norm)))
   4.280 +              |> Thm.close_derivation
   4.281 +            val (f'_lift_def, lthy) = add_lift_def ld_no_notes f'_var f'_qty rhs f'_rsp [] lthy
   4.282 +            val f'_lift_def = inst_of_lift_def lthy f'_qty f'_lift_def
   4.283 +            val f'_lift_const = mk_lift_const_of_lift_def f'_qty f'_lift_def
   4.284 +            val args_lthy = lthy
   4.285 +            val (args, lthy) = mk_Frees "x" (binder_types qty) lthy
   4.286 +            val f_alt_def_goal_lhs = list_comb (lift_const_of_lift_def lift_def, args);
   4.287 +            val f_alt_def_goal_rhs = rep_isom $ list_comb (f'_lift_const, args);
   4.288 +            val f_alt_def_goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (f_alt_def_goal_lhs, f_alt_def_goal_rhs));
   4.289 +            fun f_alt_def_tac ctxt i =
   4.290 +              EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt,
   4.291 +                SELECT_GOAL (Local_Defs.unfold_tac ctxt [id_apply]), rtac refl] i;
   4.292 +            val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data
   4.293 +            val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
   4.294 +              [([rep_isom_transfer], [Transfer.transfer_add])])] lthy
   4.295 +            val f_alt_def = Goal.prove_sorry transfer_lthy [] [] f_alt_def_goal
   4.296 +              (fn {context = ctxt, prems = _} => HEADGOAL (f_alt_def_tac ctxt))
   4.297 +              |> Thm.close_derivation
   4.298 +              |> singleton (Variable.export lthy args_lthy)
   4.299 +            val lthy = args_lthy
   4.300 +            val lthy =  lthy
   4.301 +              |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def])
   4.302 +              |> snd
   4.303 +              |> Lifting_Setup.lifting_forget (pointer_of_rep_isom_data rep_isom_data)
   4.304 +          in
   4.305 +            (ret_lift_def, lthy)
   4.306 +          end
   4.307 +       end
   4.308 +    end
   4.309 +and mk_rep_isom qty_isom_bundle (rty, qty, qty_isom) lthy =
   4.310 +  let
   4.311 +    val (rty_name, typs) = dest_Type rty
   4.312 +    val (_, qty_typs) = dest_Type qty
   4.313 +    val fp = BNF_FP_Def_Sugar.fp_sugar_of lthy rty_name
   4.314 +    val fp = if is_some fp then the fp
   4.315 +      else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.")
   4.316 +    val ctr_sugar = fp |> #fp_ctr_sugar |> #ctr_sugar
   4.317 +    val ctrs = map (Ctr_Sugar.mk_ctr typs) (#ctrs ctr_sugar);
   4.318 +    val qty_ctrs = map (Ctr_Sugar.mk_ctr qty_typs) (#ctrs ctr_sugar);
   4.319 +    val ctr_Tss = map (dest_Const #> snd #> binder_types) ctrs;
   4.320 +    val qty_ctr_Tss = map (dest_Const #> snd #> binder_types) qty_ctrs;
   4.321 +
   4.322 +    fun lazy_prove_code_dt (rty, qty) lthy =
   4.323 +      if is_none (code_dt_of lthy (rty, qty)) then prove_code_dt (rty, qty) lthy |> fst else lthy;
   4.324 +
   4.325 +    val lthy = fold2 (fold2 (lazy_prove_code_dt oo pair)) ctr_Tss qty_ctr_Tss lthy
   4.326 +
   4.327 +    val n = length ctrs;
   4.328 +    val ks = 1 upto n;
   4.329 +    val (xss, _) = mk_Freess "x" ctr_Tss lthy;
   4.330 +
   4.331 +    fun sel_retT (rty' as Type (s, rtys'), qty' as Type (s', qtys')) =
   4.332 +        if (rty', qty') = (rty, qty) then qty_isom else (if s = s'
   4.333 +          then Type (s, map sel_retT (rtys' ~~ qtys')) else qty')
   4.334 +      | sel_retT (_, qty') = qty';
   4.335 +
   4.336 +    val sel_argss = @{map 5} (fn k => fn xs => @{map 3} (fn x => fn rty => fn qty =>
   4.337 +      (k, (qty, sel_retT (rty,qty)), (xs, x)))) ks xss xss ctr_Tss qty_ctr_Tss;
   4.338 +
   4.339 +    fun mk_sel_casex (_, _, (_, x)) = Ctr_Sugar.mk_case typs (x |> dest_Free |> snd) (#casex ctr_sugar);
   4.340 +    val dis_casex = Ctr_Sugar.mk_case typs HOLogic.boolT (#casex ctr_sugar);
   4.341 +    fun mk_sel_case_args lthy ctr_Tss ks (k, (qty, _), (xs, x)) =
   4.342 +      let
   4.343 +        val T = x |> dest_Free |> snd;
   4.344 +        fun gen_undef_wit Ts wits =
   4.345 +          case code_dt_of lthy (T, qty) of
   4.346 +            SOME code_dt =>
   4.347 +              (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_witness_of_code_dt qty code_dt),
   4.348 +                wit_thm_of_code_dt code_dt :: wits)
   4.349 +            | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T), wits)
   4.350 +      in
   4.351 +        @{fold_map 2} (fn Ts => fn k' => fn wits =>
   4.352 +          (if k = k' then (fold_rev Term.lambda xs x, wits) else gen_undef_wit Ts wits)) ctr_Tss ks []
   4.353 +      end;
   4.354 +    fun mk_sel_rhs arg =
   4.355 +      let val (sel_rhs, wits) = mk_sel_case_args lthy ctr_Tss ks arg
   4.356 +      in (arg |> #2, wits, list_comb (mk_sel_casex arg, sel_rhs)) end;
   4.357 +    fun mk_dis_case_args args k  = map (fn (k', arg) => (if k = k'
   4.358 +      then fold_rev Term.lambda arg @{const True} else fold_rev Term.lambda arg @{const False})) args;
   4.359 +    val sel_rhs = map (map mk_sel_rhs) sel_argss
   4.360 +    val dis_rhs = map (fn k => list_comb (dis_casex, mk_dis_case_args (ks ~~ xss) k)) ks
   4.361 +    val dis_qty = qty_isom --> HOLogic.boolT;
   4.362 +    val uTname = unique_Tname (rty, qty)
   4.363 +    val dis_names = map (fn k => Binding.qualified true ("dis" ^ string_of_int k) uTname) ks;
   4.364 +
   4.365 +    val (diss, lthy) = @{fold_map 2} (fn b => fn rhs => fn lthy =>
   4.366 +      lift_def ld_no_notes (b, NoSyn) dis_qty rhs (K all_tac) [] lthy
   4.367 +      |> apfst (mk_lift_const_of_lift_def dis_qty)) dis_names dis_rhs lthy
   4.368 +
   4.369 +    fun lift_sel_tac exhaust_rule dt_rules wits ctxt i =
   4.370 +      (Method.insert_tac wits THEN' case_tac exhaust_rule ctxt THEN_ALL_NEW (
   4.371 +      EVERY' [hyp_subst_tac ctxt, Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules),
   4.372 +        REPEAT_DETERM o etac conjE, atac])) i
   4.373 +    val pred_simps = Transfer.lookup_pred_data lthy (Tname rty) |> the |> Transfer.pred_simps
   4.374 +    val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps)
   4.375 +    val sel_names = map (fn (k, xs) => map (fn k' => Binding.qualified true
   4.376 +      ("sel" ^ string_of_int k ^ string_of_int k') uTname) (1 upto length xs)) (ks ~~ ctr_Tss);
   4.377 +    val (selss, lthy) = @{fold_map 2} (@{fold_map 2} (fn b => fn ((_, qty_ret), wits, rhs) => fn lthy =>
   4.378 +      lift_def_code_dt { code_dt = true, lift_config = ld_no_notes }
   4.379 +        (b, NoSyn) (qty_isom --> qty_ret) rhs (HEADGOAL o sel_tac wits) [] lthy
   4.380 +      |> apfst (mk_lift_const_of_lift_def (qty_isom --> qty_ret)))) sel_names sel_rhs lthy
   4.381 +
   4.382 +    fun lift_isom_tac ctxt = Local_Defs.unfold_tac ctxt [id_apply] THEN HEADGOAL atac;
   4.383 +
   4.384 +    val (rep_isom_lift_def, lthy) = lift_def ld_no_notes (Binding.qualified true "Rep_isom" uTname, NoSyn)
   4.385 +      (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] lthy
   4.386 +      |> apfst (inst_of_lift_def lthy (qty_isom --> qty));
   4.387 +    val (abs_isom, lthy) = lift_def ld_no_notes (Binding.qualified true "Abs_isom" uTname, NoSyn)
   4.388 +      (qty --> qty_isom) (HOLogic.id_const rty) lift_isom_tac [] lthy
   4.389 +      |> apfst (mk_lift_const_of_lift_def (qty --> qty_isom));
   4.390 +
   4.391 +    fun mk_type_definition newT oldT RepC AbsC A =
   4.392 +      let
   4.393 +        val typedefC =
   4.394 +          Const (@{const_name type_definition},
   4.395 +            (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
   4.396 +      in typedefC $ RepC $ AbsC $ A end;
   4.397 +
   4.398 +    val rep_isom = lift_const_of_lift_def rep_isom_lift_def
   4.399 +    val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
   4.400 +      HOLogic.mk_Trueprop;
   4.401 +
   4.402 +      fun typ_isom_tac ctxt i =
   4.403 +        EVERY' [ SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms type_definition_def}),
   4.404 +          DETERM o Transfer.transfer_tac true ctxt, Raw_Simplifier.rewrite_goal_tac ctxt
   4.405 +            (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
   4.406 +           rtac TrueI] i;
   4.407 +
   4.408 +    val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
   4.409 +      [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
   4.410 +       (@{thms Domain_eq_top}, [Transfer.transfer_domain_add]) ])] lthy;
   4.411 +
   4.412 +    val quot_thm_isom = Goal.prove_sorry transfer_lthy [] [] typedef_goal
   4.413 +      (fn {context = ctxt, prems = _} => typ_isom_tac ctxt 1)
   4.414 +      |> Thm.close_derivation
   4.415 +      |> singleton (Variable.export transfer_lthy lthy)
   4.416 +      |> (fn thm => @{thm UNIV_typedef_to_Quotient} OF [thm, @{thm reflexive}])
   4.417 +
   4.418 +    val qty_isom_name = Tname qty_isom;
   4.419 +
   4.420 +    val quot_isom_rep =
   4.421 +      let
   4.422 +        val (quotients : Lifting_Term.quotients) = Symtab.insert (Lifting_Info.quotient_eq) (qty_isom_name,
   4.423 +          {quot_thm = quot_thm_isom, pcr_info = NONE}) Symtab.empty
   4.424 +        val id_actions = { constr = K I, lift = K I, comp_lift = K I }
   4.425 +      in
   4.426 +        fn ctxt => fn (rty, qty) => Lifting_Term.prove_schematic_quot_thm id_actions quotients
   4.427 +          ctxt (rty, qty) () |> fst |> Lifting_Term.force_qty_type ctxt qty
   4.428 +          |> quot_thm_rep
   4.429 +      end;
   4.430 +
   4.431 +    val x_lthy = lthy
   4.432 +    val (x, lthy) = yield_singleton (mk_Frees "x") qty_isom lthy;
   4.433 +
   4.434 +    fun mk_ctr ctr ctr_Ts sels =
   4.435 +      let
   4.436 +        val sel_ret_Ts = map (dest_Const #> snd #> body_type) sels;
   4.437 +
   4.438 +        fun rep_isom lthy t (rty, qty) =
   4.439 +          let
   4.440 +            val rep = quot_isom_rep lthy (rty, qty)
   4.441 +          in
   4.442 +            if is_Const rep andalso (rep |> dest_Const |> fst) = @{const_name id} then
   4.443 +              t else rep $ t
   4.444 +          end;
   4.445 +      in
   4.446 +        @{fold 3} (fn sel => fn ctr_T => fn sel_ret_T => fn ctr =>
   4.447 +          ctr $ rep_isom lthy (sel $ x) (ctr_T, sel_ret_T)) sels ctr_Ts sel_ret_Ts ctr
   4.448 +      end;
   4.449 +
   4.450 +    (* stolen from Metis *)
   4.451 +    exception BREAK_LIST
   4.452 +    fun break_list (x :: xs) = (x, xs)
   4.453 +      | break_list _ = raise BREAK_LIST
   4.454 +
   4.455 +    val (ctr, ctrs) = qty_ctrs |> rev |> break_list;
   4.456 +    val (ctr_Ts, ctr_Tss) = qty_ctr_Tss |> rev |> break_list;
   4.457 +    val (sel, rselss) = selss |> rev |> break_list;
   4.458 +    val rdiss = rev diss |> tl;
   4.459 +
   4.460 +    val first_ctr = mk_ctr ctr ctr_Ts sel;
   4.461 +
   4.462 +    fun mk_If_ctr dis ctr ctr_Ts sel elsex = mk_If (dis$x) (mk_ctr ctr ctr_Ts sel) elsex;
   4.463 +
   4.464 +    val rhs = @{fold 4} mk_If_ctr rdiss ctrs ctr_Tss rselss first_ctr;
   4.465 +
   4.466 +    val rep_isom_code_goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (rep_isom$x, rhs));
   4.467 +
   4.468 +    local
   4.469 +      val rep_isom_code_tac_rules = map safe_mk_meta_eq @{thms refl id_apply if_splits simp_thms}
   4.470 +    in
   4.471 +      fun rep_isom_code_tac (ctr_sugar:Ctr_Sugar.ctr_sugar) ctxt i =
   4.472 +        let
   4.473 +          val exhaust = ctr_sugar |> #exhaust
   4.474 +          val cases = ctr_sugar |> #case_thms
   4.475 +          val map_ids = fp |> #fp_nesting_bnfs |> map BNF_Def.map_id0_of_bnf
   4.476 +          val simp_rules = map safe_mk_meta_eq (cases @ map_ids) @ rep_isom_code_tac_rules
   4.477 +        in
   4.478 +          EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o (Transfer.transfer_tac true ctxt),
   4.479 +            case_tac exhaust ctxt THEN_ALL_NEW EVERY' [hyp_subst_tac ctxt,
   4.480 +              Raw_Simplifier.rewrite_goal_tac ctxt simp_rules, rtac TrueI ]] i
   4.481 +        end
   4.482 +    end
   4.483 +
   4.484 +    val rep_isom_code = Goal.prove_sorry lthy [] [] rep_isom_code_goal
   4.485 +      (fn {context = ctxt, prems = _} => rep_isom_code_tac ctr_sugar ctxt 1)
   4.486 +      |> Thm.close_derivation
   4.487 +      |> singleton(Variable.export lthy x_lthy)
   4.488 +
   4.489 +    val lthy = x_lthy
   4.490 +    val pointer = Lifting_Setup.pointer_of_bundle_binding lthy qty_isom_bundle
   4.491 +    fun code_dt phi context = code_dt_of lthy (rty, qty) |> the |>
   4.492 +      update_rep_isom rep_isom (transfer_rules_of_lift_def rep_isom_lift_def |> hd)
   4.493 +       (bundle_name_of_bundle_binding qty_isom_bundle phi context) pointer;
   4.494 +    val lthy =
   4.495 +      lthy
   4.496 +      |> snd o Local_Theory.note ((Binding.empty, @{attributes [code]}), [rep_isom_code])
   4.497 +      |> Local_Theory.declaration {syntax = false, pervasive = true}
   4.498 +        (fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context)
   4.499 +      |> Local_Theory.restore
   4.500 +      |> Lifting_Setup.lifting_forget pointer
   4.501 +  in
   4.502 +    ((selss, diss, rep_isom_code), lthy)
   4.503 +  end
   4.504 +and constr qty (quot_thm, (lthy, rel_eq_onps)) =
   4.505 +  let
   4.506 +    val quot_thm = Lifting_Term.force_qty_type lthy qty quot_thm
   4.507 +    val (rty, qty) = quot_thm_rty_qty quot_thm
   4.508 +    val rty_name = Tname rty;
   4.509 +    val pred_data = Transfer.lookup_pred_data lthy rty_name
   4.510 +    val pred_data = if is_some pred_data then the pred_data
   4.511 +      else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.")
   4.512 +    val rel_eq_onp = safe_mk_meta_eq (Transfer.rel_eq_onp pred_data);
   4.513 +    val R_conv = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
   4.514 +      then_conv Conv.rewr_conv rel_eq_onp
   4.515 +    val quot_thm = Conv.fconv_rule(HOLogic.Trueprop_conv (Quotient_R_conv R_conv)) quot_thm;
   4.516 +  in
   4.517 +    if is_none (code_dt_of lthy (rty, qty)) then
   4.518 +      let
   4.519 +        val non_empty_pred = quot_thm RS @{thm type_definition_Quotient_not_empty}
   4.520 +        val pred = quot_thm_rel quot_thm |> dest_comb |> snd;
   4.521 +        val (pred, lthy) = yield_singleton (Variable.import_terms true) pred lthy;
   4.522 +        val TFrees = Term.add_tfreesT qty []
   4.523 +
   4.524 +        fun non_empty_typedef_tac non_empty_pred ctxt i =
   4.525 +          (SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' rtac non_empty_pred) i
   4.526 +
   4.527 +        val uTname = unique_Tname (rty, qty)
   4.528 +        val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
   4.529 +        val ((_, tcode_dt), lthy) = conceal_naming_result (typedef (Binding.concealed uTname, TFrees, NoSyn)
   4.530 +          Tdef_set NONE (fn lthy => non_empty_typedef_tac non_empty_pred lthy 1)) lthy;
   4.531 +        val type_definition_thm = tcode_dt |> snd |> #type_definition;
   4.532 +        val qty_isom = tcode_dt |> fst |> #abs_type;
   4.533 +
   4.534 +        val config = { notes = false}
   4.535 +        val (binding, lthy) = conceal_naming_result (Lifting_Setup.setup_by_typedef_thm
   4.536 +          config type_definition_thm) lthy
   4.537 +        val lthy = Local_Theory.restore lthy
   4.538 +        val (wit, wit_thm) = mk_witness quot_thm;
   4.539 +        val code_dt = mk_code_dt rty qty wit wit_thm NONE;
   4.540 +        val lthy = lthy
   4.541 +          |> update_code_dt code_dt
   4.542 +          |> Local_Theory.restore
   4.543 +          |> mk_rep_isom binding (rty, qty, qty_isom) |> snd
   4.544 +      in
   4.545 +        (quot_thm, (lthy, rel_eq_onp :: rel_eq_onps))
   4.546 +      end
   4.547 +    else
   4.548 +      (quot_thm, (lthy, rel_eq_onp :: rel_eq_onps))
   4.549 +  end
   4.550 +and lift_def_code_dt config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def_code_dt config)
   4.551 +  var qty rhs tac par_thms lthy
   4.552 +
   4.553 +
   4.554 +(** from parsed parameters to the config record **)
   4.555 +
   4.556 +fun map_config_code_dt f1 f2 { code_dt = code_dt, lift_config = lift_config } =
   4.557 +  { code_dt = f1 code_dt, lift_config = f2 lift_config }
   4.558 +
   4.559 +fun update_config_code_dt nval = map_config_code_dt (K nval) I
   4.560 +
   4.561 +val config_flags = [("code_dt", update_config_code_dt true)]
   4.562 +
   4.563 +fun evaluate_params params =
   4.564 +  let
   4.565 +    fun eval_param param config =
   4.566 +      case AList.lookup (op =) config_flags param of
   4.567 +        SOME update => update config
   4.568 +        | NONE => error ("Unknown parameter: " ^ (quote param))
   4.569 +  in
   4.570 +    fold eval_param params default_config_code_dt
   4.571 +  end
   4.572 +
   4.573 +(**
   4.574 +
   4.575 +  lift_definition command. It opens a proof of a corresponding respectfulness
   4.576 +  theorem in a user-friendly, readable form. Then add_lift_def_code_dt is called internally.
   4.577 +
   4.578 +**)
   4.579 +
   4.580 +fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy =
   4.581 +  let
   4.582 +    val config = evaluate_params params
   4.583 +    val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy
   4.584 +    val var = (binding, mx)
   4.585 +    val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
   4.586 +    val par_thms = Attrib.eval_thms lthy par_xthms
   4.587 +    val (goal, after_qed) = prepare_lift_def (add_lift_def_code_dt config) var qty rhs par_thms lthy
   4.588 +  in
   4.589 +    Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy
   4.590 +  end
   4.591 +
   4.592 +fun quot_thm_err ctxt (rty, qty) pretty_msg =
   4.593 +  let
   4.594 +    val error_msg = cat_lines
   4.595 +       ["Lifting failed for the following types:",
   4.596 +        Pretty.string_of (Pretty.block
   4.597 +         [Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]),
   4.598 +        Pretty.string_of (Pretty.block
   4.599 +         [Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]),
   4.600 +        "",
   4.601 +        (Pretty.string_of (Pretty.block
   4.602 +         [Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))]
   4.603 +  in
   4.604 +    error error_msg
   4.605 +  end
   4.606 +
   4.607 +fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
   4.608 +  let
   4.609 +    val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt
   4.610 +    val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
   4.611 +    val error_msg = cat_lines
   4.612 +       ["Lifting failed for the following term:",
   4.613 +        Pretty.string_of (Pretty.block
   4.614 +         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]),
   4.615 +        Pretty.string_of (Pretty.block
   4.616 +         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]),
   4.617 +        "",
   4.618 +        (Pretty.string_of (Pretty.block
   4.619 +         [Pretty.str "Reason:",
   4.620 +          Pretty.brk 2,
   4.621 +          Pretty.str "The type of the term cannot be instantiated to",
   4.622 +          Pretty.brk 1,
   4.623 +          Pretty.quote (Syntax.pretty_typ ctxt rty_forced),
   4.624 +          Pretty.str "."]))]
   4.625 +    in
   4.626 +      error error_msg
   4.627 +    end
   4.628 +
   4.629 +fun lift_def_cmd_with_err_handling (params, (raw_var, rhs_raw, par_xthms)) lthy =
   4.630 +  (lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy
   4.631 +    handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
   4.632 +    handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) =>
   4.633 +      check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw);
   4.634 +
   4.635 +val parse_param = Parse.name
   4.636 +val parse_params = Scan.optional (Args.parens (Parse.list parse_param)) [];
   4.637 +
   4.638 +(* parser and command *)
   4.639 +val liftdef_parser =
   4.640 +  parse_params --
   4.641 +  (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix') >> Parse.triple2)
   4.642 +    --| @{keyword "is"} -- Parse.term --
   4.643 +      Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1)
   4.644 +
   4.645 +val _ =
   4.646 +  Outer_Syntax.local_theory_to_proof @{command_keyword "lift_definition"}
   4.647 +    "definition for constants over the quotient type"
   4.648 +      (liftdef_parser >> lift_def_cmd_with_err_handling)
   4.649 +
   4.650 +end
     5.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Fri Dec 05 14:14:36 2014 +0100
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Fri Dec 05 14:14:36 2014 +0100
     5.3 @@ -16,6 +16,8 @@
     5.4    val quot_thm_rep: thm -> term
     5.5    val quot_thm_crel: thm -> term
     5.6    val quot_thm_rty_qty: thm -> typ * typ
     5.7 +  val Quotient_conv: conv -> conv -> conv -> conv -> conv
     5.8 +  val Quotient_R_conv: conv -> conv
     5.9  
    5.10    val undisch: thm -> thm
    5.11    val undisch_all: thm -> thm
    5.12 @@ -34,6 +36,7 @@
    5.13    val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option
    5.14    val instT_thm: Proof.context -> Type.tyenv -> thm -> thm
    5.15    val instT_morphism: Proof.context -> Type.tyenv -> morphism
    5.16 +  val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory
    5.17  end
    5.18  
    5.19  
    5.20 @@ -82,6 +85,11 @@
    5.21      (domain_type abs_type, range_type abs_type)
    5.22    end
    5.23  
    5.24 +fun Quotient_conv R_conv Abs_conv Rep_conv T_conv = Conv.combination_conv (Conv.combination_conv 
    5.25 +  (Conv.combination_conv (Conv.arg_conv R_conv) Abs_conv) Rep_conv) T_conv;
    5.26 +  
    5.27 +fun Quotient_R_conv R_conv = Quotient_conv R_conv Conv.all_conv Conv.all_conv Conv.all_conv;
    5.28 +
    5.29  fun undisch thm =
    5.30    let
    5.31      val assm = Thm.cprem_of thm 1
    5.32 @@ -149,4 +157,8 @@
    5.33      term = [Envir.subst_term_types env],
    5.34      fact = [map (instT_thm ctxt env)]};
    5.35  
    5.36 +fun conceal_naming_result f lthy = 
    5.37 +  let val old_lthy = lthy
    5.38 +  in lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming old_lthy end;
    5.39 +
    5.40  end
     6.1 --- a/src/HOL/Transfer.thy	Fri Dec 05 14:14:36 2014 +0100
     6.2 +++ b/src/HOL/Transfer.thy	Fri Dec 05 14:14:36 2014 +0100
     6.3 @@ -269,6 +269,8 @@
     6.4  lemma Domainp_refl[transfer_domain_rule]:
     6.5    "Domainp T = Domainp T" ..
     6.6  
     6.7 +lemma Domain_eq_top: "Domainp op= = top" by auto
     6.8 +
     6.9  lemma Domainp_prod_fun_eq[relator_domain]:
    6.10    "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
    6.11  by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)