Isabelle是一名通用证明助理，以Isabelle / HOL为主要实例。
如何证明顺序命令C1；如果我们知道 C1 总是终止，那么 C2 总是可以执行到 C2？
我正在使用定理证明器来演示程序的进度。 程序的语义是使用小步关系定义的，表示为 ctran，程序配置之间。一个程序
为什么isabelle的预购需要提供less_and_less_eq
Isabelle 的 preorder 类需要同时提供 less_eq 和 less： 类别顺序 = 修复 less_eq :: "'a ⇒ 'a ⇒ bool" and less :: "'a ⇒ 'a ⇒ bool" 类别预购 = 订单 + 一个...
我想将自动应用于先前应用创建的所有证明目标，但不应用于其他目标。我只知道如何通过将所有内容放入子目标中来做到这一点。有更好的方法吗？ 引理栏： 假设...
isabelle clarsimp/fastforce 背景变成浅红色的含义
图像转为fastforce，背景为浅红色 这种情况在我的校样中不断发生。正如您所看到的，证明目标窗口是空白的。 fastforce上的浅红色背景是什么意思？同样的情况也发生了
有时，使用 XXX applyblast 可以释放一个证明目标，但 apply (blast mod: XXX) 不适用于任何 intro、elim 或 del 的 mod，无论有或没有！。 使用爆炸实际上有什么作用？
有没有办法一次执行多个apply（erule_tac x=... in allE）？有时，当我的假设中有多个 forall 时，Isabelle 在 erule_tac 之后对它们重新排序，这使得证明非常
记录r = 一个::nat b :: 自然数 c :: 自然 引理“P (r ⦇ a := 2, b := 3 ⦈) ⟹ P (r ⦇b := 3, a := 2⦈)” 应用自动 ― 〈不起作用〉 通过 (metis r.simps(5) r.simps(6) r.surjective) 为什么...
多年来，Isabelle 一直在从使用引号“...”过渡到使用漩涡花饰 <...> 来包装类型、对象逻辑术语和符号。截至目前（Isabelle 2023），它仍然相当
type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set" fun LTS_is_reachable :: "('q, 'a) LTS \ 'q \ '列表 \ 'q \
我正在尝试在 Isabelle2023 上运行 afp-2019-08-19 的不完整性。当我打开ROOT文件时 法新社章 会话不完整性 (AFP) = 遗传有限 + 描述“不完整的......
我正在尝试为一些图形计算定义归纳谓词： type_synonym 节点 = nat type_synonym 边缘 = nat 记录图= 节点 ::“节点集” 边缘 ::“边缘设置&qu...
关于映射的两个问题： [1] 这个引理是微不足道的 引理 [simp] : "(m(x ↦ v))|` {x} = [x ↦ v]" 但我怎样才能证明这两个引理呢？ 引理：“(m(x ↦ v))|`(dom(m) - {x}) = m&quo...
构造 Isabelle 中满足给定条件的所有元素的 Set 的函数
我正在尝试学习伊莎贝尔的布景构建，但我失败了。 假设您需要一个函数来给出所有小于给定数字的自然数。我认为这应该有效：...
我（仍然）在有限集上的递归函数上苦苦挣扎。我想在有限（有限）集合上定义一个特殊的笛卡尔积。我正在尝试实现的简化示例...
如何正确从HOL.Bit_Operations导入bit_nat的定义？ 工作代码，将定义复制到当前理论中： 理论刮擦 进口主营 开始 定义 bit_nat ::...
Isabelle/HOL 中的 primrec 和 fun 有什么区别？
我正在阅读 Isabelle 教程，并试图澄清我对使用 primrec 和 fun 的概念。到目前为止我搜索过的内容，包括这里的答案；我了解 pri 中的构造函数...
我正在尝试创建一个带有规则的数据类型，可以这么说，但我不确定从哪里开始（假设这是可能的！）。 例如，我有一个数据类型，一对（种类，值）定义为记录。我会...
在伊莎贝尔，为什么会这样 理论实例 导入平方根 开始 定理存在无理数：“∃x.x ∉ ℚ” 证明（规则exI） 使用 simp 的 sqrt_2_not_rat 显示“sqrt 2 ∉ ℚ” 问...