Re: [isabelle] Turning an Eisbach method into a simple method



Hi Simon,

Eisbach methods arenât really structured or unstructured, they inherit that from the methods they comprise. This behaviour comes from how the combinators work, i.e. if you write â(-, rule)â then the âruleâ invocation gets the using context. There is certainly a case for treating this more explicitly in Eisbach: I was never convinced one way or the other what a sensible default should be.

My understanding is that you want to hide the âusingâ context from the Eisbach method, choosing instead to insert it into the goal state first. You are always free to write your own higher-order method in order to do this sort of fiddling:

method_setup simple_method =
 âMethod_Closure.method_text >> (fn m => fn ctxt => fn facts =>
   let
     val insert' = Method.Basic (K (Method.insert facts))
     val m' = Method.Combinator (Method.no_combinator_info, Method.Then, [insert', m])
   in Method_Closure.method_evaluate m' ctxt [] end)â

method use_spec = simple_method âerule specâ

lemma
  assumes P: "âx. P x"
  shows "P x"
  using P
  by use_spec

-Dan



> On 6 Apr 2016, at 6:44 PM, Simon Wimmer <wimmersimon at gmail.com> wrote:
>
> Dear Eisbach experts,
>
> I have an Eisbach method, which per default acts as "structured method"
> (like rule).
> However, I would like to turn it into a "simple method" (like simp, blast
> and friends) by essentially mimicking the behaviour of
>  apply -
>  apply <Eisbach method>
>
> Browsing the manuals and the source of method.ml, I wasn't able to figure
> out a way to do so. Is there an easy one?
>
> Simon


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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