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



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 background is that I am writing tools[1] to automatically convert
C code into an abstract(ish) monadic form with the goal of easing
reasoning. As part of this, I frequently need to write ML code that
dynamically generates theorems and then proceeds to prove them. A simple
way of writing tactics such as the one above would be helpful both in
quick-and-dirty prototyping of ML proof procedures, but ideally would
also be clean enough for "production quality code".

Does anyone have any hints or tips?

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.

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.

We still need to work out, why this direction did not look appealing to your application. I have browsed through the AutoCorres 0.1 sources, but did not see the totally unusual problem that requires completely different approaches to what people are already used to. It might be there nonetheless, and this is why be have switched to the more interactive mailing list.


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.

Although we first need to sort out what is conceptually the right way to go. Antiquotations are some kind of ML preprocessor macros, and that is not something you do without thinking several times about it.


	Makarius





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