到目前为止,我在Isabelle的以下风格中使用矛盾来编写证据(使用Jeremy Siek的模式):
lemma "<expression>"
proof -
{
assume "¬ <expression>"
then have False sorry
}
then show ?thesis by blast
qed
有没有一种方法可以在没有嵌套的原始校样块的情况下工作{ ... }？
我想在一个名为理论的理论中定义我自己的列表类型List,但是已经存在一个具有该名称的理论.是否有比它更轻量级的理论Main？
有时,当我在写申请风格的证明,我就想办法修改论证方法 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!])+
它会停止在这个脚本无法解决的第一个目标上.
让我们假设我想要显示以下引理
lemma "? A; B; C ? ? D"
我得到了目标
1. A ? B ? C ? D
但是,我不需要B.我怎样才能将目标转移到类似的东西上
1. A ? C ? D
我不想改变原始lemma陈述,只是改变申请风格的当前目标.
此外assume,Isar还有presume在Isar证明块中引入事实的命令.从我在文档中看到和阅读的内容来看,它不需要在目标中明确列出假设(推定？),并且似乎添加了一个案例来表明假定的陈述来自其他目标.
所以问题是:我什么时候使用presume而不是assume,我可以用什么好的技巧presume？
我是一个Isabelle新手,我对⋀和∀之间以及⟹和between之间的关系感到困惑(实际上,很多).
我有以下目标(这是一个高度简化的版本,我最终得到了一个真实的证明):
??x. P x ? P z; P y? ? P z
我想通过专业化x与y得到⟦Py⟹Pz来证明; Py⟧⟧Pz,然后使用modus ponens.这有助于证明非常相似:
??x. P x ? P z; P y? ? P z
但我无法让它为上述目标而努力.
有没有办法将前一个目标转变为后者？如果没有,这是因为它们在逻辑上是不同的陈述,在这种情况下有人可以帮我理解差异吗？
我一直在努力学习虽然原则上我喜欢异步防爆检查的主意,用伊莎贝尔2016年,我不喜欢伊莎贝尔/ jEdit的为许多原因,其中最严重的是,它使用了太多的内存(为了我).
如果我可以使用Isabelle 2016中的旧版Proof General,那就太棒了.我将变量设置isa-isabelle-command为指向bin/isabelleIsabelle分发目录下的文件.当我使用Proof General的菜单启动Isabelle时,Emacs挂起,当我打断它时C-g,我在*isabelle*缓冲区中得到以下内容.
> val it = (): unit
^BException- ERROR "Bad socket name: \"I\"" raised
我知道这个站点上的旧帖子表明,Proof General用来与定理证明者通信的Isabelle组件被删除了.这是(仍然)Isabelle 2016的真实情况吗？如何在较新版本的Isabelle中使用Proof General？
我在 Isabelle/HOL 中有一些定义和定理，需要在 HOL 中使用这些相同的定义和定理。手动翻译代码当然是可能的，但很麻烦。有没有（半）自动执行这种翻译的程序？
如果由于某种原因这是不可能的，请解释原因，因为这对我来说是一个重要的学习。
一年半前，我开始在 Isabelle 编写证明程序。那时我主要写 Isabelle/Isar 证明。最近，我一直在做一些 Isabelle/ML 级别的编程。我发现这篇描述 Isar 结构的博士论文非常鼓舞人心。我想知道是否有类似的来源可以了解 Isabelle 的基础。我在1989 年找到了这篇论文，在 1990 年找到了 Larry Paulson 的这篇论文。这是否描述了系统的当前基础？
更新：
我在Joshua Chen 的论文中找到了迄今为止对 Isabelle/Pure 最清楚的解释。关于内核如何隐藏定理创建有单独的关注。但这似乎是一种基于抽象数据类型的语言特性。
更新 2
在 Isabelle 的邮件列表的主题Explanation of derivation in Isabelle'sformal system下已经有一些讨论。指出的进一步参考是Isabelle/Isar implementation reference。这是上述博士论文的修订版。
我一直在 Isabelle 2019 会议上工作，该会议已经变得有点大，并且在某些时候我无法再isabelle build在我的 8G RAM 机器上使用它来构建它。尽管如此，当我使用 jEdit（运行isabelle jedit -d .）打开主理论文件时，会话的构建没有问题。
如何调整构建过程，使其像图形界面一样顺利运行？
接下来，我将提供更多细节。
主要症状是 Poly/ML 过程在某个时刻停止；它并没有真正失败，但不会在合理的时间内终止（大约 20 分钟，当成功构建在我的计算机中需要 3' 时）。
在开发过程中，调整使用ML_OPTIONSto"--minheap 5500"就足以解决这个问题，但后来我们决定将会话分成两部分（不再添加代码，只是更改了 ROOT 文件），之后没有进一步调整解决了问题。另一方面，一台具有 16G RAM 的机器无需任何进一步设置就可以毫无问题地构建。
编辑。我检查了 jEdit 使用的选项；那些相关的（我相信）是--minheap 500 --gcthreads 0（最后一个是默认值）。我尝试了这些但没有成功。我还注意到 build 命令有一个不同的--eval Command_Line.tool0 (fn () => (Build.build "/tmp/isabelle-pedro/buildNNNNNNNNNNNNN"))选项，其中NNNNNNNNNNNNN有一些数字。