有时,当我在写申请风格的证明,我就想办法修改论证方法 foo来
尝试
foo第一个目标.如果它解决了目标,那就好; 如果它没有解决它,恢复到原始状态并失败.
这出现在以下代码中:
qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+
在进一步改变之后,调用simp将不再完全解决目标,然后这将循环.如果我可以指定类似的东西
qed (solve_goal(subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail))+
或(替代建议的synatx)
qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)!)+
或者(甚至更好的语法)
qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+
它会停止在这个脚本无法解决的第一个目标上.
在伊莎贝尔的NEWS档案中，我发现
\n\n\n命令“typedef”现在在本地理论上下文中工作——无需引入对参数或假设的依赖，而这在 Isabelle/Pure/HOL 中是不可能的。请注意，即使在全局理论上下文中，逻辑环境也可能包含局部 typedef 的多种解释（具有不同的非空性证明）。
\n
（可以追溯到 Isabelle2009-2）。这是关于typedef当地理论背景的最新消息吗？此外，“不引入对参数或假设的依赖”的限制实际上意味着什么？
如果这意味着我不能在 a 的定义集中使用区域设置参数typedef，那么我根本不会考虑typedef本地化（因为唯一允许的实例可以轻松地移到本地上下文之外，或者我是否遗漏了某些内容？）。
是否（或者应该，或者将会）可以沿着线做一些事情（其中用于 a 的集合取决于typedeflocale 参数V）：
datatype (\'a, \'b) "term" = Var \'b | Fun \'a "(\'a, \'b) term list"\n\nlocale term_algebra =\n fixes F :: "\'a set"\n and V :: "\'b set"\nbegin\n\ndefinition "domain \xce\xb1 = {x : V. \xce\xb1 x ~= Var x}"\n\ntypedef (\'a, \'b) subst =\n "{\xce\xb1 :: \'b => (\'a, …有时<statement> solve_direct（我通常通过调用<statement> try）列出一些库定理并说“当前的目标可以直接解决：……”。
设<theorem>一个搜索结果solve_direct，然后在大多数情况下我可以证明<statement> by (rule theorem)。
然而，有时这样的证明不被接受，导致错误信息“应用初始证明方法失败”。
是否有一种通用的、不同的技术来重用由 找到的定理solve_direct？
还是要看个人情况？我可以尝试找出一个最小的例子并将其附加到这个问题上。
在 Isabelle，我经常发现我可以使用不同的求解器成功地证明一个目标。
通常，我更愿意使用可以证明目标的最弱求解器。根据我目前与 Isabelle 的经验，我目前的理解是，按照强度增加和速度降低的顺序，常见的逻辑求解器排名如下（即何时rule和simp两者都起作用，rule应该使用等）：
rule < simp < auto < fastforce < force
这样对吗？这里blast适合放哪里？
我检查编程和伊莎贝尔/ HOL（PDF）证明和与伊莎贝尔/ HOL具体语义，但无法找到答案。
如何在 Isabelle 中将集合转换为列表？
我对带有签名的函数定义感兴趣：
"'a set => 'a list"
我该如何定义这个？
问题
我想知道在 Isabelle 中是否有一种自然的编码方式是这样的语法：
type_synonym Var = string
datatype Value = VInt int | ...
datatype Cmd = Skip | NonDeterministicChoice "Cmd set" | ...
动机是根据非确定性选择定义一些规范命令，例如：
Magic == NonDeterministicChoice {}
Rely c r z = Defined using set compreehension and NonDeterministicChoice
Isabelle 抱怨“Cmd set”中类型“Cmd”的递归出现，即：
不支持通过类型表达式“Cmd set”中的类型构造函数“Set.set”递归出现类型“Cmd”。使用“bnf”命令将“Set.set”注册为有界自然函子以允许嵌套（共）递归通过它
在我使用 set 时查看 Isabelle 错误消息，我无法弄清楚如何在这种情况下为“set”类型注册有界自然函子，因此我决定尝试一种推测性解决方案。
投机解决方案
相反，如果我使用归纳定义的数据类型，例如列表，伊莎贝尔不会抱怨，例如
datatype Cmd = Skip | NonDeterministicChoice "Cmd list" | ...
列表在这里不是正确的抽象，但我试一试看看它是否有效。使用列表的直接效果是，我需要使用序列过滤而不是使用集合理解，然后问题就变成了假设存在两个列表：一个包含Cmd 的所有元素，另一个包含Value 的所有元素。
我声明了两个未解释的常量：
consts Values :: "Value list"
consts Programs :: "Cmd …我想在较弱的笔记本电脑上使用 Isabelle，并将繁重的定理搜索/证明委托给网络上的服务器。我猜想这之前已经完成了，但我找不到此任务的教程或报告。
Isabelle系统手册描述了如何自行运行 Isabelle 后端。但是，我从手册中不明白如何将现有前端之一（例如Isabelle/jEdit）连接到这样的进程。理想情况下，该设置应该适用于多个用户（并且理论文件位于用户系统上）。
到目前为止，我能实现的最好结果是在服务器上运行所有 Isabelle/jEdit，并通过 SSH/X11 转发从 Linux 笔记本电脑访问它。这很酷，但不完全是我的想法。还有其他方法吗？
TL;DR：Isar 语言有编码约定吗？是否有必要尊重jEdit的折叠策略？
我的团队正在研究数学的形式化，因此我们的主要目的之一是获得可读的证明。考虑到这一点，我们尝试以中间事实（和标签，如果有的话）脱颖而出的方式编写证明：
from fact1 have
1: "Foo"
using Thm1 Thm2 by auto
then have
2: "Bar = FooBar"
by simp
also from 1 have
" ... = BarFoo"
by blast
除了有时这会产生大量“短线”（顺便说一句，我不知道这是否真的是一个问题）之外，它在某种程度上与 jEdit 折叠策略不兼容；折叠后，之前的代码块将如下所示：
from fact1 have
then have
also from 1 have
完全掩盖了论点。下面的格式也许更好：
from fact1
have 1: "Foo"
using Thm1 Thm2 by auto
then
have 2: "Bar = FooBar"
by simp
also from 1
have " ... = BarFoo"
by blast
并且，折叠之后，
from fact1
have 1: "Foo"
then …例如，Isabelle 可以将“and”表示为“^”，“or”表示为“v”……有没有办法获得所有这些类型的运算符/构造函数的完整列表？