Isabelle是一名通用证明助理，以Isabelle / HOL为主要实例。
关于映射的两个问题： [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 ∉ ℚ” 问...
我理解 ccontr 是如何工作的，但是我不确定如何（或者即使可能）在用假设声明的引理上使用它。 举个简单的例子，一切都很好： 引理l1：“A⊆B⟶A∩...
我试图理解“继承”在语言环境/解释级别上是如何工作的。我有一个抽象语言环境 (locA)，其中定义了一个方法 (g)。我有一个具体的语言环境（locB），wh...
我正在使用 Isabelle 来验证 C 程序。在验证过程中，我使用c-parser install-C-file加载代码，但是出现了以下问题： 尝试导致指针衰减
我正在尝试为类似 C 的语言定义语法。为了简单起见，它只有算术表达式、变量声明和语句块： type_synonym vname = nat
我一直在尝试“移植”一些在 Isabelle 中形式化的命令式语言（IMP2）：https://www.isa-afp.org/sessions/imp2/#Semantics.html 到阿格达。 首先，这是一些初步翻译...
我尝试在证明中使用大锤并得到这样的输出 大锤打... 吸血鬼找到了证据…… 仅从这些事实得出“False”：SymbolicE、const_bool_simp、ptype_bool_not、
路径元素“C:\Isabelle\Isabelle2023 mp\MLTEMPb14572”中存在非法字符“:”
当我在cygwin中输入isabelle build -bv CParserTest命令时，出现以下错误 [isabelle] *** 路径元素“C:\Isabelle\Isabelle2023 mp\
将算术表达式转换为 Isabelle 中的多项式系数列表。无法证明乘法表达式的算法
简介 算术表达式的数据类型定义为 数据类型 exp = Var |常数 int |添加 exp |多重expexp 我正在尝试实现一个函数，coeffs :: exp ⟹ int list，...
我正在尝试为具体语义学中的第 7 章问题 1 生成结构化的 Isar 证明，但我在为归纳案例定义正确的假设和归纳假设时遇到困难...
我是伊莎贝尔的新手，遇到了一个我正在努力解决的问题。我有以下引理： 导入 Main HOL.HOL HOL.Real "HOL-Library.Sum_of_Squares" 引理 修复 r :: 重新...
Isabelle Nitpick 超出了基数限制 65536；该怎么办？
我收到了来自 Isabelle 的 Nitpick 工具的“已达到限制：基数过高 (65536)”错误： 挑剔的公式... [...] 类型 'a 通过了单调性测试；挑剔也许可以跳过...
刚开始学习Isabelle/ISAR，想尝试一些基本的逻辑证明。我的核心问题是，即使我直接从说明手册中复制校样，我仍然会出错......