Email Gateway (Aug 22 2022 at 14:32): Email Gateway (Aug 22 2022 at 14:32):From: Zhe Hou <zhe.hou@hotmail.com>
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
Email Gateway (Aug 22 2022 at 14:37):From: Daniel.Matichuk@data61.csiro.au
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:
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).
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"›)
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.
Last updated: Apr 26 2024 at 20:16 UTC