我正在尝试学习isabelle/Isar，并从Rings.thy提供的关于mod的简单证明中理解它。第一行是有意义的，因为它使用了前面的定理，并通过对称重写了它。但是接下来的两行看起来真的很奇怪。它们中的每一个都声明相同的东西等于它自己(例如"a div b = a div b")。它们没有连接到引理中的q或r来证明
浏览 11提问于2021-01-19得票数 1
我还在尝试对Isabelle中的语义平等进行推理。我想比较两个公式，看看它们是否相等。以前有人告诉我，我需要使用quotienttypes。所以我试着给自己定义一个quotiernttype，但是很明显，我的定义并不完整，因为在定义之后，我似乎不能写任何代码。到目前为止我的代码是：imports Mainno_notation plus (infixl "+" 65)
typedecl basicFor
浏览 8提问于2016-01-20得票数 1
我注意到，在使用Isabelle/HOL Isar时，有几种方法可以处理通用量化。我正在尝试以一种适合本科生理解和复制的风格来编写一些证明(这就是我使用Isar的原因！)我对如何以一种好的方式表达通用量化感到困惑。
例如，在Coq中，我可以编写forall x, P(x)，然后我可能会说“归纳x”，这将根据相应的归纳原理自动生成目标。然而，在Isabelle</e
浏览 0提问于2015-12-28得票数 7
3回答
其中一个写着“命令的非法应用”定理“在顶层”，所以我假设你不能简单地在顶层定义一个定理，并且维基百科的页面没有提供一个完整的初始示例。我将这个定理包装在如下理论中：imports Main伊莎贝尔停止了对定理的抱怨，但在定理的第二行，它现在说：Failed to parse proposition
它也在</
浏览 4提问于2014-07-31得票数 3
我只想用命题逻辑(如notI、notE、impI、impE)中的基本自然演绎规则(ND)将这一证明转化为ab练习(供我学习)。等)。我可以很容易地在应用脚本中做到这一点： apply (rule impI) (* A ⟹ A ∨ B *) apply (rule disjI1) (* A ⟹ A *)但我试图证明Isar<
浏览 2提问于2020-05-12得票数 1
回答已采纳
具体来说，我讨论的是cases vs case_tac和induct vs indut_tac (虽然了解tac的一般含义是很好的，因为我还在使用其他方法，比如cut_tac)。我注意到我不能用用例，也不能在⋀绑定变量中引入apply，但是如果它是一个结构化的证明，我可以使用。为什么？ lemma "¬(∀x. ¬(P x)) ⟹ ∃x.apply (case_tac "P x")
apply (erule
浏览 4提问于2021-06-05得票数 0
回答已采纳
1回答
会籍证明
、
我需要证明以下几点：在简单的英语中，我需要证明"min_list (x#xs)“的返回值始终是(x#xs)的成员我试过：apply(auto)find_theorems min_list
现在的分目标太长了，
浏览 0提问于2019-05-01得票数 2
回答已采纳
1回答
我刚从伊莎贝尔开始我的第一步，但是，对于定理证明器和证明助手来说，我有点迷失了。我主要对函数式分析或代数的应用程序感兴趣--我看过这些文档，我试图用语言环境来获得我自己的例子，但我遇到了一些非常基本的问题。begin
apply (rule assocm)这只是一个证明证明命令在</
浏览 2提问于2016-11-30得票数 2
我已经阅读了第8章讨论类型，在所谓的教程，伴随着伊莎贝尔发行(标题A高级逻辑证明助理)。我阅读了Florian的文档标题Isabelle/HOL类型类层次结构(也是Isabelle发行版的一部分)。我找到了那个理论文件中的引用，看了“高阶逻辑证明助手”第8.4.5节，我发现自然数型nat是线性有序半环，int型是有序环，real型是有序域。更重要的是，“所有涉及除法的抽象性质都需要
浏览 5提问于2021-01-21得票数 1
回答已采纳
2回答
我正面临着以下引理的问题，我认为它应该是正确的。我可以通过很小的步骤使证明达到某一点，但是我还没有找到证明整个引理的方法。
浏览 1提问于2013-06-07得票数 1
回答已采纳
对于一个uni项目，我正在和Iabelle/HOL 2018年一起做一个证明。我在应用明显的结果时出错了。然而，这个错误并没有说明出了什么问题。我有一个最低限度的例子如下：
我将命题公式定义为type1，然后我有一个尾递归函数，它简单地收集每个子公式。也许有更好的方法来做到这一点。我只是尝试以最简单的方式复制错误。然后，我想展示一个简单的
浏览 1提问于2019-07-24得票数 1
回答已采纳
2回答
当用户试图证明auto或sledgehammer没有立即证明的东西时，是否有一种“通用”的非正式算法可供Isabelle用户遵循？一种通用的方法，用于计算auto是否需要用户制定的额外引理才能成功，或者如果更好，则使用其他证明方法。
一个相关的问题是:是否可以在某个地方找到一个表，其中包含所有证明方法以及应用它们的上下文？当我通读时，各种方法(一些方法的<
浏览 4提问于2017-02-19得票数 6
我最近开始学习Isabelle，但我找不到一个非常重要的问题的答案:人们如何才能一步一步地推理Isabelle找到的“证明”？当然，我了解了Isar的“证明”，但1.这样的Isar证明并不总是能被Sledgehammer找到，2.即使Isar证明也不总是给出一步一步的推理。例如，我的一个定理的
浏览 3提问于2015-06-07得票数 9
下面是数学中的一个小定理：
设u不是A的元素，v也不是B的元素，f是从A到B的内射函数.设A‘=A并{u}，B’=B并{v}，定义g: A‘-> B’，如果x在A中，且g(u) =v，则g也是内射的.，如果Q.f是内射的，那么(Extend Q).f也是内射的，我希望我的语法或多或少是正确的。我想在Isabelle/Isar<em
浏览 8提问于2019-03-07得票数 2
1回答
我经常发现，“auto”并不能解决一个对我来说很简单的方程，至少对涉及∪、∩和-的术语进行一些搜索。goal (1 subgoal):我可以绕过它(例如by auto (metis Diff_eq Diff_idemp))，但我想知道是否存在一些我缺少的自动化也许是一些专用的simp集，比如用于set操作的ac_simps？
浏览 2提问于2014-07-10得票数 1
回答已采纳
--record x :: nat cond :: "Point ⇒ Point ⇒ " abs (x point1 - x point2) = 1 ∨ abs (y point1 - y point2) = 1"我对伊莎贝尔还是很陌生的</
浏览 0提问于2018-12-10得票数 0
回答已采纳
1回答
此模式生成器在给定位置生成一个具有给定数字的列表，所有其他值均为零。lng = 下面的引理旨在证明生成的列表在给定位置包含正确的值case by auto这似乎是一个正确的证明；但是，将生成器函数的反表达式中的val更改为(if p
浏览 0提问于2020-05-13得票数 2
回答已采纳
1回答
什么是公理K？
、、、
我注意到自从HoTT以来，关于"Axiom K“的讨论越来越多。我相信这与模式匹配有关。我很惊讶在TAPL、ATTAPL或PFPL中找不到引用。
什么是Axiom K？是否用于ML风格的模式匹配，就像在SML中一样(或者仅仅是dependent pattern 作为Axiom K的适当参考？
浏览 88提问于2016-08-31得票数 37
回答已采纳
偶尔也会有一个引理，其中try0崩溃了Isabelle/JEdit。那么，只有进程id上的kill -9才能工作。(我做了一些谷歌搜索，但找不到任何相关信息。)
浏览 1提问于2014-02-21得票数 0
回答已采纳
在下面的示例中，我想使用simp来证明简单类型的lambda演算中的一些术语是类型检查。我添加了每个类型检查规则作为simp的重写规则，因此simp执行条件重写并在此过程中创建示意图变量。但是，在重写某些重写的辅助条件时，simp会卡住涉及原理图变量的重写术语，因为它不会实例化它们：begin
type_synonym var = stringt1.3 = typ
浏览 2提问于2018-06-03得票数 0
云服务器
ICP备案
腾讯会议
云直播
对象存储
腾讯云开发者
