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



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 to both generate a "method"
from a list of tokens, and to generate a "cases_tactic" from a method.
These can be combined as follows:

    (*
     * Generate an ML tactic object of the given Isar string.
     *
     * For example,
     *
     *   mk_tac "auto simp: field_simps intro!: ext" @{context}
     *
     * will generate the corresponding "tactic" object.
     *)
    fun mk_tac str ctxt =
    let
      val parsed_str = Outer_Syntax.scan Position.start str
          |> filter Token.is_proper
          |> Args.name
      val meth = Method.method (Proof_Context.theory_of ctxt)
          (Args.src (parsed_str, Position.start)) ctxt
    in
      Method.apply (K meth) ctxt [] #> Seq.map snd
    end

or alternatively as an anti-quotation:

    (*
     * Setup an antiquotation of the form:
     *
     *    @{tactic "auto simp: foo intro!: bar"}
     *
     * which returns an object of type "context -> tactic".
     *
     * 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

and setup in a theory file as follows:

    setup {*
      tactic_antiquotation_setup
    *}

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.

Cheers,
David

--


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.





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