[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.