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


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.


I can use this to somewhat emulate the [1!] feature¹ suggested on
isabelle-dev, without patching Isabelle:

  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"
  have B
  apply ((tactic {* SOLVE (@{tactic "rule y"} @{context}) *})[1]) -- "does not solve it, hence fails"

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"

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.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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