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



On Mon, 11 Mar 2013, David Greenaway wrote:

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:

The "Method" class provides an interface

That is the *structure* Method in Isabelle/ML. SML is free from any object-oriented concepts. You should do justice to what the oo-guys tried to do several decades ago by using their terminology properly.

    * While this doesn't provide any benefits over a direct call to "mk_tac" just
    * yet, in the future it may generate code to avoid parsing the tactic at
    * run-time.
    *)
   val tactic_antiquotation_setup =
   let
     val parse_string =
       ((Args.context -- Scan.lift Args.name) >> snd)
         #>> ML_Syntax.print_string
         #>> (fn s => "mk_tac " ^ s)
         #>> ML_Syntax.atomic
   in
     ML_Antiquote.inline @{binding "tactic"} parse_string
   end

Parsing at runtime gets you back to LISP-style dynamic macro programming. ML_Antiquote.value should do the job statically at compile time. Sometimes this requires auxiliary data in the context, to transport abstract values between the runtime/compile time of Isabelle/ML. E.g. see how the @{thm} antiquotation is done. (To get to its implementation you write something like ML {* @{thm refl} *} and use hover-click in Isabelle/jEdit on "thm".)


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.

The next one will ask for arguments that are not just constants like Suc_eq_plus1, but ML expressions at run-time.


	Makarius




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