Re: [isabelle] Method setup with arguments



The "classic" solution is to use the method_setup command and define a parser, here you'll most likely want "Args.term"

However in you're example you aren't passing a term to method1, you're passing the fact P (now a fact as a result of the match subgoal focus). You would have to use the Attribs.thm parser to do that. So there are a few solutions to your problem:

1. Define a method that takes a fact and extracts its underlying term:

  method_setup method1 = 
    âAttrib.thm >> (fn thm => fn ctxt => SIMPLE_METHOD (my_tac (Thm.prop_of thm)))â

  method method2 = (match premises in P:"?A â ?B" â âmethod1 Pâ)

  However here "method1" can only work inside a match/focus (where P is an assumed fact).

2. Define a method that takes a term and quote the premise back through to method1

  method_setup method1 = 
    âArgs.term >> (fn t => fn ctxt => SIMPLE_METHOD (my_tac t))â

  method method2 = (match premises in "A â B" for A B â âmethod1 "A â B"â)

3. As above, but bind the premise to a separate name first:

  method method2 = (match premises in P for P â âmatch (P) in "?A â ?B" â âmethod1 Pââ)

We can also define method1 with the "tactic" method, although it is maybe not as straightforward as it could be.

  method method1 for P = (tactic âmy_tac (Morphism.term morphism @{term P})â)

  The implicitly bound "morphism" here instructs the tactic to re-evaluate "P" in the evaluation environment of "method1" when it is executed. Using a bare "@{term P}" will not give the expected result.



> On 4 Nov. 2016, at 7:55 pm, Zhe Hou <zhe.hou at hotmail.com> wrote:
> 
> Hi,
> 
> Suppose I have already defined a ML function my_tac that takes a term as
> input and returns a tactic, now I want to setup a method (here called
> method1) to wrap it up. Is there a way to pass a term as an argument of the
> method?
> 
> For example, suppose I want to use method1 inside an Eisbach method called
> method2:
> 
> method method2 = (match premises in P:"?A /\ ?B" => <method1 P>)
> 
> How should I define the setup and parser for method1 so that I can pass the
> argument P as a term to my_tac?
> 
> Thank you very much!
> 
> Zhe 
> 
> 



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