# [isabelle] Accessing lift_definition from the ML-level

Dear all,
I have a question regarding the lifting package.
Is there some canonical way of simulating
lift_definition name :: typ is term <proof>
on the ML-level (where <proof> might be replaced by some tactic)
In the current interface I only found
val add_lift_def:
(binding * mixfix) -> typ -> term -> thm -> thm list -> local_theory -> local_theory
val lift_def_cmd:
(binding * string option * mixfix) * string * (Facts.ref * Args.src list) list -> local_theory -> Proof.state
where add_list_def seems more closely to what I need, but I have no clue what "thm" and "thm list" are good for.
If there would be something like the following, then everything is clear,
val add_lift_def:
(binding * mixfix) -> typ -> term -> tactic -> local_theory -> local_theory
but with the current add_lift_def and passing some thm and an empty thm list, I got complaints that
exception THM 1 raised (line 332 of "drule.ML"):
RSN: no unifiers
P defau
rel_fun (eq_onp (λx. x ∈ {(b, c). c ⟶ P b})) (eq_onp P) ?c ?c ⟹
?c' ≡ map_fun Test.Rep_restricted_cond Abs_restricted ?c ⟹
rel_fun Test.cr_restricted_cond cr_restricted ?c ?c'
Do I really have to create a theorem that unifies against internals in the lifting construction?
rel_fun (eq_onp (λx. x ∈ {(b, c). c ⟶ P b})) (eq_onp P) ?c ?c ⟹
?c' ≡ map_fun Test.Rep_restricted_cond Abs_restricted ?c ⟹
rel_fun Test.cr_restricted_cond cr_restricted ?c ?c' ?
To compare with, if I invoke the lift_definition command manually, the proof goal is
⋀prod. prod ∈ {(b, c). c ⟶ P b} ⟹ P (case prod of (b, c) ⇒ if c then b else defau)
so, some proof goal that I can easily discharge using "P defau" by (simp split: prod.splits)
Kind regards,
René

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*