10

在 Isabelle 理论文件中，我可以编写简单的单行策略，例如：

apply (clarsimp simp: split_def split: prod.splits)

然而，我发现，当我开始编写 ML 代码来自动化证明、生成 MLtactic对象时，这些单行代码变得相当冗长：

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

有没有更简单的方法可以在 Isabelle/ML 级别编写简单的单线战术？

例如，类似反引号：@{tactic "clarsimp simp: split_def split: prod.splits"}产生类型的函数context -> tactic，将是一个理想的解决方案。

4

3 回答 3

5

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.

于 2013-03-05T18:51:38.613 回答
3

除了其他答案之外，我认为值得一提的是，在 Isabelle2015 中有一种称为Eisbach的新的高级策略/证明方法构造语言（类似于 Coq 中的 Ltac） ，旨在更容易理解和维护。

于 2016-01-03T21:03:50.480 回答
1

该类Method似乎提供了足够的接口来提取策略，cases_tactic如下所示：

(*
 * 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

或者作为反引用：

(*
 * 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

并在理论文件中设置如下：

setup {*
  tactic_antiquotation_setup
*}

然后可以按如下方式使用：

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

如预期的。

于 2013-03-11T03:39:29.110 回答