问题标签 [hol]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
functional-programming - 如何在 Isabelle 中定义 if then else 表达式？
它向我抱怨我有一个解析错误，但我在手册中找不到正确的语法应该是什么......
错误：
isabelle - 是否可以在 Isar 中编写非自动形式化？
我有以下内容：
我认为这取决于基本推理规则，但阅读Isar 参考手册rule部分的文档9.4.3 Structured Methods后发现，它使用了具有各种规则的 Classical Reasoner。并且，将by子句替换为..也解决了目标，因此不需要提及隐含消除和连词介绍。
是否可以在 Isar 中编写严格的形式化，即不使用程序文本中未明确的任何自动化和额外规则？类似于 HOL4 中的前向证明。
isabelle - 为什么我们不能在进行规则反转时*直接*对归纳定义的谓词进行案例分析？
似乎有一些关于归纳谓词的东西我不明白，因为我不断遇到它们的问题。我最近的努力是用ev具体语义书籍第 5 章中归纳定义的谓词来理解案例分析。
假设我正在证明
我试图在 Isabelle/HOL 中立即开始证明，但是当我尝试或给出奇怪的目标时它会抱怨：
这表明：
这不是我所期望的。
当我传递n到案例时，我们改为对自然数的定义进行归纳（注意其他时候它ev正确地进行了归纳，请参见后面的示例）：
给出：
这不是我所期望的。但是请注意，即使作为参数，以下内容也可以工作（即它ev不是对自然数进行归纳） ：n
我意识到首先假设ev n然后声明显示必须有一些魔力，ev (n-2)否则不会发生错误。
我理解规则倒置的想法（通过分析可能导致它的案例，得出要反向证明的给定事实）。对于“偶数”谓词，规则反转是：
这基于归纳定义的谓词是有意义的：
但我不明白。为什么不直接做案例工作？或者为什么这个语法无效：
或这个：
等等
我认为症结在于，在处理归纳定义谓词时，我不知道这种归纳是否适用于目标或假设，但从教科书的文字来看：
名称规则倒置强调我们是在倒推：通过哪些规则可以证明某些给定的事实？
我假设它正在对目标应用规则倒置，因为它说“通过哪些规则可以证明某些给定的事实”。
此外，ev ==> ev (n-2)书中的这个例子也无济于事，因为前提和结论都ev涉及。
规则倒置的案例分析如何真正发挥作用，为什么我们需要首先假设 Isabelle 为案例分析提供合理的目标？
isabelle - 当证明开始时，我们如何强制 Isabelle 向我们揭示它在 Isar 的后台应用了什么规则？
我试图证明：
我做了：
它给了我非常漂亮的目标：
这可能会使我的证明可读。
似乎它在后台应用了某种案例。但是当我编写案例时，证明立即完成，而不是明确显示上述规则反转案例。看：
这表明：
这意味着我可以只放置一个qed.
我怎样才能弄清楚 Isar 在 Isabelle 中自动执行的（介绍？）规则？
isabelle - 当证明已经完成但给出“未能完善任何未决目标”错误时，为什么我不能在 Isabelle 中明确说明我的案例？
我正在阅读具体语义的第 5 章。
我在处理这个玩具示例证明时遇到了一些错误：
我知道这比需要的多（因为by cases）神奇地解决了所有问题并给出了完整的证明，但我想明确说明这些情况。
我试过这个：
但是如果我把鼠标放在上面，?cases我会收到 Isabelle（类型检查器？）验证员的投诉：
这个错误是什么意思？
case为什么我不能用这里的语法明确证明？即使是微不足道的？
问题是，您如何立即结案？
如果没有要证明的案例，您可以立即使用 qed 关闭证明。
稍后会引用，但我无法使其适用于真实的证明。
isabelle - 如何使用 OpenTheory 将 HOL-light 格式的定理转换为 Isabelle 格式的定理
目前，我有几个 HOL-light 格式的定理（连同证明），我想将它们转换成 Isabelle 格式的定理。我知道 OpenTheory ( http://www.gilith.com/opentheory/ ) 可以做到，但我不知道从哪里开始，因为我找不到任何可以参考的详细教程/示例。因此，我想知道从哪里开始可能是一个好点。提前非常感谢！
isabelle - 如何从 HOL 获取 ML 值？
我有一个这样的嵌入式 ML 代码：
谁能给我一个从 HOL 获取这些值的代码示例？
predicate - 用 Isabelle 证明谓词逻辑
我试图证明以下引理：
lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"
我试图从消除 forall 量词开始，所以这就是我尝试过的：
最后我刚刚开始根据之前申请的结果采取行动，但对我来说似乎是错误的，可能是因为一开始有一些错误......有人可以向我解释我的错误以及如何正确完成这个证明?
提前致谢
coq - 在列表中查找正常工作的定理
我正在证明关于在列表中查找的定理。我一直在证明，如果你真的发现了什么，那么它就是真的。什么样的引理或策略可能有助于证明这类定理？我的意思是，在这种情况下，列表上的归纳似乎是不够的。但是这个定理仍然是肯定的。
（这是 HOL4 定义的翻译，也缺少这种定理）
定理的 HOL 版本：
integer - 在 HOL 中证明非负整数是有根据的。（或者只是他们的归纳原理。）
我想在 HOL 中证明非负整数是有根据的。一个人怎么能做到？
我知道，自然数和非负数之间存在双射。
这种双射以两种方式保持顺序。
归纳原理适用于自然数。
从归纳原则遵循最小数原则。
如果我有正数的归纳原理，那么我可以重复证明并证明非负整数的最小数原理。
因此，我认为主要问题浓缩为以下问题：
如何证明非负数的归纳原理？
原则：