*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Easily using built-in tactics at the ML level (and/or using a method as a tactic)*From*: Joachim Breitner <breitner at kit.edu>*Date*: Mon, 11 Mar 2013 12:40:44 +0100*In-reply-to*: <513D55C3.6010402@nicta.com.au>*References*: <5139409A.1070008@nicta.com.au> <513D55C3.6010402@nicta.com.au>

Hi, Am Montag, den 11.03.2013, 14:55 +1100 schrieb David Greenaway: > On 08/03/13 12:36, David Greenaway wrote: > > In an Isabelle theory file, I can write simple one-line tactics such > > as the following: > > > > apply (clarsimp simp: split_def split: prod.splits) > > > > I find, however, when I start writing ML code to automate proofs, > > producing a ML tactic object is far more verbose: > [...] > > Does anyone have any hints or tips? > > With the help of Thomas Sewell, I came up with the following solution: > > [..] > > This can then be used in ML code to generate a tactic: > > lemma "(a :: nat) * (b + 1) = (a * b) + a" > by (tactic {* @{tactic "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"} @{context} *}) > > Hopefully this helps somebody other than just me. Nice! I can use this to somewhat emulate the [1!] feature¹ suggested on isabelle-dev, without patching Isabelle: notepad begin assume x: "B" assume y: "A ⟹ B" assume z: A have B apply ((tactic {* SOLVE (@{tactic "rule x"} @{context}) *})[1]) -- "solves the goal, so it works" done have B apply ((tactic {* SOLVE (@{tactic "rule y"} @{context}) *})[1]) -- "does not solve it, hence fails" sorry Unfortunately, it does not parse complete method text with , | + ...: have B apply ((tactic {* SOLVE (@{tactic "rule y, rule z"} @{context}) *})[1]) -- "should solve, but doesn't parse" done Do you think that would be possible as well? I tried to find a way, but a parsed sequence of proof methods is a Method.text, which is interpreted by Proof.apply_text, and I did not find a way to turn a aggregate Method.text to a Method.method to use with Method.apply. Thanks, Joachim ¹ https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-March/003911.html -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**References**:

- Previous by Date: [isabelle] Transfer rule for transfer_forall
- Next by Date: Re: [isabelle] Transfer rule for transfer_forall
- Previous by Thread: Re: [isabelle] Easily using built-in tactics at the ML level (and/or using a method as a tactic)
- Next by Thread: Re: [isabelle] partial_function
- Cl-isabelle-users March 2013 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