如何在Isabelle的ML级别轻松编写简单的策略？
在Isabelle理论文件中，我可以编写简单的一行策略，如下所示：
apply (clarsimp simp: split_def split: prod.splits)然而，我发现，当我开始编写ML代码来自动化校样、生成ML tactic对象时，这些一行代码变得相当冗长：
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类型的函数，将是理想的解决方案。
回答 3
Stack Overflow用户
发布于 2013-03-06 02:51:39
我看到了各种可能性，这有点取决于你的应用程序的上下文，什么是最好的。请注意，通常情况下，用于自动证明的单个ML代码在很久以前是很常见的，但现在相对较少。例如，将相当小的HOL-Bali (始于1997年)中的自定义战术数量与法新社的大JinjaThreads (始于2007年，一直持续到最近)进行比较。
嵌套像@{tactic}这样的ML反引号在原则上是可行的，但你很快就会遇到更多的问题，比如如果你的定理参数应该再次是Isar或ML源，会发生什么。
与ML中的反引用策略构建块不同，一种更基本的方法是在Isar中引用您的证明过程，给出如下的常规方法语法：
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)))
*}在这里，我首先用Isabelle/ML定义了一个传统的foo_tac，然后用通常的Isar方法将它包装起来作为证明方法。后者意味着您有像SIMPLE_METHOD这样的包装器负责将“连锁事实”推入您的目标状态，而CHANGED则负责确保Isar方法取得进展(如simp或auto)。
foo_tac示例假设您对上下文(或其简单集)的修改是恒定的，通过硬连接的拆分规则。如果你想在那里有更多的参数，你可以把它包含在具体的方法语法中。请注意，Method.sections在这方面已经相当成熟了。isar-ref手册的“定义证明方法”一节给出了更多基本的参数解析器。您还应该通过搜索method_setup (在Isabelle/Isar中)或Method.setup (在Isabelle/ML中)的源代码来查看现有示例。
如果你仍然想做ML反引号而不是具体的方法语法，你可以尝试@{context}的一个变体，它允许像这样的修饰符：
@{context simp add: ...}这有点投机性，是当场发明的，可能会被证明是一种糟糕的做法。正如我已经说过的，在Isabelle中细粒度的策略编程在最近几年变得有点过时，尽管ML是Isabelle框架中不可或缺的一部分。如果您在更多的应用程序上下文中提出了更具体的问题，我们可以重新考虑反引号方法。
Stack Overflow用户
发布于 2016-01-04 05:03:50
除了其他答案之外，我认为值得一提的是，Isabelle2015中有一种新的高级策略/证明方法构造语言(类似于Coq中的Ltac )，名为Eisbach，旨在更容易理解和维护。
Stack Overflow用户
发布于 2013-03-11 11:39:29
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} *})如你所愿。
https://stackoverflow.com/questions/15217009
复制相似问题
腾讯云开发者
