Re: [isabelle] Easily using built-in tactics at the ML level (and/or using a method as a tactic)

```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:

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
Description: This is a digitally signed message part

• References:

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