Re: [isabelle] Accessing lift_definition from the ML-level



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é
> 





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