问题标签 [isabelle]

When defining an inductive predicate I can choose which parameters are fixed and which not. For a contrived example consider:

Is it somehow possible to turn this into an inductively defined set with one fixed and one non-fixed parameter?

is rejected with the error message:

I know that I can define a set based on the inductive predicate version (e.g., Foo P b = {(x, y). foo P b x x}), but then I always have to unfold it before I can apply induction or case-analysis (or have to introduce corresponding rules for Foo, which seems a bit redundant).

我有一个结构如下的伊莎贝尔证明：

第一个案例实际上有几页长，所以在阅读第二个案例时，普通读者甚至我自己都不清楚它False指的是什么。（嗯，它实际上是，但不是来自阅读，仅在交互式环境中：如果，例如，在 Isabelle/jEdit 中，将光标放在 之后case False，您将n ≠ 0在“输出”面板中的“this”下看到。）

那么是否有一种语法允许明确假设“False”情况，这样读者既不必与 IDE 交互，也不必向上滚动到proof关键字，但可以看到正确的假设？

到目前为止，我在 Isabelle 中以以下风格编写了矛盾证明（使用Jeremy Siek的模式）：

有没有嵌套原始证明块的方法{ ... }？

这是一个初学者的问题。

我正在阅读教程“Isabelle/HOL 中的编程和证明”。

我想打印“1 + 2”的结果。

所以我写道：

这使：

我想看看结果，即“3”。我怎么能在伊莎贝尔做到这一点？如果我在定理证明器中对“1+2”进行归一化，则会显示结果 3。我只想在伊莎贝尔做同样的事情。

请注意，我昨天开始使用 Isabelle。

在我的 Isabelle 形式化中，我正在处理有限的自然数集，在这些集上我想考虑具有线性顺序属性的函数。

我看到图书馆中有几种不同的订单形式，但我不确定要重用哪一种。在大多数情况下，我想检查它们是否为线性顺序的那些函数将简单地通过使用库运算符（如<( less)）来定义，但在某些情况下，它们可能被定义为更复杂的库函数组合。

我试过HOL/Library/Order_Relation了，但似乎没有连接到<；例如，我无法自动证明以下引理：

（我确信有更好的方法将函数转换为关系，但这不是这里的重点。）

如果有一些现成的库可以让我知道，我会很感激。以数学上优雅的方式对此进行建模现在对我来说并不是最重要的，所以现在我正在考虑使用将有理数或实数分配给我的集合中的自然数的函数，然后<在这些有理数/实数上使用数字。

我正在使用向量的自定义实现作为函数，其域是自然数的有限“索引集”，并且其图像是某种可以定义最大值的类型，通常是real. v例如，我可以有一个带有v 1 = 2.7和的二维向量v 3 = 4.2。

在这样的向量上，我想定义一个类似“arg max”的运算符，它告诉我最大分量的索引，3在上面的例子中v。我说的是“the”索引，因为“arg max”like 运算符将另外接受一个打破平局的函数，以应用于具有值的组件。（背景是拍卖中的出价。）

我知道Max在有限集上是使用定义fold1的（我还不明白它是如何工作的）。我尝试了这个，它本身就被接受了，但是对于我想做的其他事情却没有用：

请注意，此外，我想证明我的“arg max”之类的运算符的某些属性，这可能需要归纳。我知道有finite_ne_induct对有限集进行归纳的规则。好的，但我也希望能够以可以评估的方式定义我的运算符（例如，在尝试使用具体的有限集时），但是评估

具有预期的返回值1给了我以下错误：

因此，我求助于将有限集转换为列表。在列表上，我已经能够定义运算符，并通过使用list_nonempty_induct.

基于工作列表的定义如下所示：

我没有成功地直接在有限集的构造函数上定义一个函数。以下不起作用：

它给了我错误信息

这可能是因为列表构造函数被定义为 a datatype，而有限集仅被定义为一个inductive方案？

不管怎样——你知道在有限集上定义这个函数的方法吗？要么直接写下来，要么通过一些类似折叠的效用函数？

大约 2-3 周前，我开始学习定理证明者 Isabelle。我仍然是一个绝对的初学者，到目前为止，我一直在学习“Isabelle/HOL 中的编程和证明”教程。

到目前为止，我发现的关于矩阵的唯一帮助是查看HOL 库中的源代码。

现在我想学习如何证明矩阵的性质。矩阵的 lambda 语法对我来说仍然是新的。有没有关于在 Isabelle 中使用矩阵的教程或基本/中级示例？

在我的伊莎贝尔理论中，我有一个具有常数因子的矩阵：

我可以计算转置矩阵：

在我看来，后者应该相当于

根据 的定义transpose。但是这是错误的。我的错误是什么？

顺便说一下，转置的定义是：

我面临以下引理的问题，我认为这应该是正确的。我可以通过小步骤使证明工作到某个点，但是我还没有找到证明整个引理的方法。

如何通过 thf 在 Isabelle 中创建对象逻辑？

我发现在文档中创建对象逻辑是

在 Isabelle/Isar 参考手册中。

我还应该阅读关于对象逻辑和特别是使用 thf 的哪些内容？

THF 是在这里的论文中输入的高阶形式