How can I easily write simple tactics at the ML level of Isabelle?

Question

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, to produce an ML tactic object, these one-liners become rather verbose:

clarsimp_tac (Context.proof_map (
    Simplifier.map_ss (fold Splitter.add_split @{thms prod.splits})
    #> Simplifier.map_ss (fn ss => ss addsimps [@{thm split_def}]))
  @{context}) 1

Is there an easier way to write the simple one-line tactics at the Isabelle/ML level?

For example, something like an anti-quotation: @{tactic "clarsimp simp: split_def split: prod.splits"} producing a function of type context -> tactic, would be an ideal solution.

Answer 1

I see a variety of possibilities, it depends a bit on the context of your the application what is best. Note that in general, individual ML code for proof automated used to be common-place in the very old times, but it is relatively rare today. For example, compare the amount of custom tactics in rather small HOL-Bali (started in 1997) with the large JinjaThreads in AFP (started in 2007 and continued until recently).

Nesting ML antiquotations like @{tactic} would in principle work, but you would quickly run into further questions, like what happens if your theorem arguments should be again Isar or ML source.

Instead of antiquoting tactic building blocks in ML, a more basic approach is to quote your proof precedure in Isar by giving it regular method syntax like this:

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've first made a conventional foo_tac definition in Isabelle/ML, and then wrapped it up the usual Isar way as proof method. The latter means you have wrappers like SIMPLE_METHOD taking care of pushing "chained facts" into your goal state, and CHANGED to ensure that the Isar method makes progress (like simp or auto).

The foo_tac example assumes that your modification of the context (or its simpset) is constant, by the hard-wired split rules. If you want to have further parameters there, you can include that in the concrete method syntax. Note that Method.sections is already quite sophisticated in this respect. More basic argument parsers are given in the section "Defining proof methods" of the isar-ref manual. You should also look at existing examples by searching the sources for method_setup (in Isabelle/Isar) or Method.setup (in Isabelle/ML).

If you still want to do ML antiquotations instead of concrete method syntax, one could try a variant of @{context} that allows modifiers like this:

@{context simp add: ...}

That is a bit speculative, invented on the spot, and might turn out as bad practice. As I've said, fine-grained tactic programming in Isabelle became a bit out of use in recent years, although ML is an integral part of the Isabelle framework. If you pose a more concrete question with more of the application context, we can reconsider the antiquotation approach.

Answer 2

Additional to the other answers, I think it's worth mentioning that there is a new high-level tactic/proof method construction language (similar to Ltac in Coq) called Eisbach in Isabelle2015, which aims to be easier to understand and maintain.

Answer 3

The Method class appear to provide enough of an interface to extract out a tactic, via a cases_tactic 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
*}

which can then be used as follows:

lemma "(a :: nat) * (b + 1) = (a * b) + a"
  by (tactic {* @{tactic "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"} @{context} *})

as desired.