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

Hi Makarius,

On 10/03/13 06:47, Makarius wrote:
> On Fri, 8 Mar 2013, 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:
>>  clarsimp_tac (Context.proof_map (
>>      Simplifier.map_ss (fold Splitter.add_split @{thms prod.splits})
>>      #> Simplifier.map_ss (fn ss => ss addsimps [ at {thm split_def}]))
>>    @{context}) 1
> The first hint is off-topic: ML has values and functions over values,
> not "objects".  Someone else had also used the oo-term "method" for ML
> functions, but this is only adding confusion, and working against the
> intentions of the oo-guys some decades ago: the idea back then was to
> have unusual terminology ("objects", "methods", "classes") for unusual
> and groundbreaking concepts.

Thank you for the correction. I did understand a tactic is simply a "thm
-> thm Seq.seq", but have the bad habit of being imprecise in my

> Back to today's reality and the question how to work effectively and
> smoothly with Isabelle/ML, and how to write proof procedures in it.
> Here is part of my answer from the Stackoverflow thread again:
> ML {*
>    (*foo_tac -- the payload of what you want to do,
>      note the dependency on ctxt: Proof.context*)
>    fun foo_tac ctxt =
>      let
>        val my_ctxt =
>          ctxt |> Simplifier.map_simpset
>           (fold Splitter.add_split @{thms prod.splits} #>
>            Simplifier.add_simp @{thm split_def})
>      in ALLGOALS (clarsimp_tac my_ctxt) end
> *}
> method_setup foo = {*
>    (*concrete syntax like "clarsimp", "auto" etc.*)
>    Method.sections Clasimp.clasimp_modifiers >>
>      (*Isar method boilerplate*)
>      (fn _ => fn ctxt => SIMPLE_METHOD (CHANGED (foo_tac ctxt)))
> *}
> Here I had already applied some peep-hole optimization to make your
> initial version less awkward.  Instead of pasting together big ML
> expressions (also with antiquotations) in "apply tactic {* ... *}" you
> build up small ML tools like foo_tac and eventually wrap them up in
> concrete Isar syntax via method_setup, for example.

Your version is indeed cleaner than mine, but still not quite what I am
looking for.

I think the confusion comes from me not explaining fully what my goal
is. Your solution works well when 1 particular tactic needs to be used
in "n" locations. What I am trying to simplify is having "n" different
tactics each used in 1 single location (with that one location always
being inside an ML function).

In short, I am looking for syntactic sugar to make writing proof scripts
in ML less verbose. While a lot of the heavy lifting of such proof
scripts can be done in Isar and the result used as a "thm", I still find
that I need to carry out proofs inside ML (such as when the proof goal
is not known in advance).

> In your second question (actually answer) on Stackoverflow, you've had
> a function to parse strings into tactic values like this:
>    mk_tac "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"
> But that is better done at compile-time via ML antiquotations,
> speculatively like this:
>    @{metis Suc_eq_plus1 mult_Suc_right nat_add_commute}
> It is reasonably easy to implement such antiquotations -- they are
> part of the Isar user space just like methods, attributes etc. --
> I can also give some examples.

An anti-quotation that generates code similar to what I original wrote
(or perhaps what you corrected it to :) would be ideal.

Two problems that I have, though are:

    * I can't extract a list of valid methods names (or their associated
      tactic) from the "Method" structure;

    * Even if I could get a list of method names, I can't see a way of
      parsing method arguments into an AST without re-implementing the
      parsing logic of every single tactic. (Most tactics are not so
      bad, because they use one of three possible argument parsers.
      Nevertheless, as far as I can tell these would need to be
      reimplemented to produce an AST instead of directly modifying the
      proof context directly).

If you have any suggestions for solving these problems, I would be keen
to hear.

Thanks so much,



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.