*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Accessing lift_definition from the ML-level*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Fri, 3 Oct 2014 09:35:28 +0200*In-reply-to*: <B24807B6-CE22-4F9C-936A-9A309E4B2E44@uibk.ac.at>*References*: <B24807B6-CE22-4F9C-936A-9A309E4B2E44@uibk.ac.at>

Dear all, playing a little bit further, I could establish part of what I wanted by using lift_def_cmd and converting types and terms back to strings (which are immediately parsed again in lift_def_cmd) fun lift_def_ml (binding,mixfix) ty rhs ctxt tactic = let val ctxt' = Config.put show_markup false ctxt val term_to_string = Print_Mode.setmp [] (Syntax.string_of_term ctxt') val typ_to_string = Print_Mode.setmp [] (Syntax.string_of_typ ctxt') val state = Lifting_Def.lift_def_cmd ((binding, SOME (typ_to_string ty), mixfix), term_to_string rhs, []) ctxt in state end However, now I am left with turning a Proof.state into a context again (which should be done via the provided tactic). So, is there some common function of type state -> tactic -> context In proof.ML I only found functions like global_qed which take "Method.text_range option * bool", but no tactics. Kind regards, René Am 02.10.2014 um 18:09 schrieb René Thiemann <rene.thiemann at uibk.ac.at>: > 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é >

**Follow-Ups**:**Re: [isabelle] Accessing lift_definition from the ML-level***From:*Makarius

**References**:**[isabelle] Accessing lift_definition from the ML-level***From:*René Thiemann

- Previous by Date: Re: [isabelle] Conversion for translation into combinatory logic?
- Next by Date: [isabelle] linear programming
- Previous by Thread: [isabelle] Accessing lift_definition from the ML-level
- Next by Thread: Re: [isabelle] Accessing lift_definition from the ML-level
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list