问题标签 [isar]

在 Isar 风格的 Isabelle 证明中，这很有效：

这里调用的隐含规则proof是rule conjE。但是我应该放什么让它不仅仅适用于一个析取：

我想了解 Isabelle/HOL 亚型。我在对我最后一个 SO 问题的部分回答中解释了为什么它对我很重要：

尝试将类型类和子类型视为集合和子集

基本上，我只有一种类型，所以如果我可以通过子类型利用 HOL 类型的力量，这可能对我有用。

我在 Isabelle 文档、Web 和 Isabelle 邮件列表中进行了搜索。使用了“子类型”这个词，虽然不多，而且它似乎不是 Isabelle 词汇表中非常重要的一部分。

部分地，我只想知道如何正确使用“子类型”这个词。我不想在 Isabelle 中将某些不是子类型的东西称为子类型。

根据 Wiki，子类型是特定于语言的：

https://en.wikipedia.org/wiki/Subtyping

重要的最后一部分；请命令

有人可以给我一个创建 Isar 子类型的 Isar 命令列表吗？我正在调查typedef，正如上面链接的问题中所解释的那样。我倾向于称其为子类型，但isar-ref.pdf在解释命令时不使用“子类型”。

如果还有其他方法可以创建 Isabelle/HOL 子类型，我想知道。

假设我有一个二元运算符f :: "sT => sT => sT"。我想定义f它为克莱因四组实现一个 4x4 乘法表，在 Wiki 上显示：

http://en.wikipedia.org/wiki/Klein_four-group

在这里，我要做的就是创建一个包含 16 个条目的表。首先，我定义了四个这样的常量：

然后我定义我的函数来实现表中的 16 个条目：

我不知道如何在 Isar 中进行任何类似普通的编程，并且我在 Isabelle 用户的列表中看到，据说（某些）类似编程的结构在语言中被有意淡化了。

前几天，我试图创建一个简单的、人为的函数，在找到if, then, else源文件中的使用后，我在isar-ref.pdf中找不到对这些命令的引用。

在查看教程时，我看到definition了以一种直接的方式定义函数，除此之外，我只看到有关递归和归纳函数的信息，它们需要datatype，而我的情况比这更简单。

如果留给我自己的设备，我想我会尝试datatype为上面显示的这 4 个常量定义 a，然后创建一些转换函数，以便最终得到一个二元运算符f :: sT => sT => sT。我在尝试使用时有点搞砸了fun，但这并不是一件简单的事情。

我做了一些fun实验inductive

更新：我在这里添加了一些材料来回应评论告诉我编程和证明是我可以找到答案的地方。看来我可能会误入理想的 Stackoverflow 格式。

我做了一些基本的实验，主要是用fun，但也用inductive. 我很快就放弃了归纳法。这是我从简单示例中得到的错误类型：

我的乘法表不是归纳法，所以我不认为这inductive是我应该花时间去追求的。

“模式匹配”在这里似乎是一个关键思想，所以我尝试了fun. 这是一些试图fun仅与标准函数类型一起使用的非常混乱的代码：

我遇到了这种错误，我在Programming and Proving中读过这样的内容：

“递归函数是通过对数据类型构造函数进行模式匹配来有趣地定义的。

fun这一切都给新手一个需要的印象datatype。至于它的大哥function，我不知道。

似乎在这里，我需要的只是一个具有 16 个基本情况的递归函数，这将定义我的乘法表。

是function答案吗？

在编辑这个问题时，我想起function了过去，这是function在工作：

try 的输出告诉我它可以被证明（更新：我认为它实际上告诉我只有 1 个证明步骤可以被证明。）：

我不知道那是什么意思。我只知道function因为试图证明不一致。我只知道它没有抱怨那么多。如果function像这样使用是我定义乘法表的方式，那么我很高兴。

尽管如此，作为一个争论的类型，我没有function在教程中学习。几个月前我在参考手册中了解到它，但我仍然不太了解如何使用它。

我有一个function我用 证明的auto，但幸运的是，这个功能可能不好。这增加了function的神秘感。function在 Isabelle/HOL中定义递归函数中有关于的信息，它比较fun和function。

但是，我还没有看到funorfunction不使用递归数据类型的示例，例如nator 'a list。可能我看的不够仔细。

抱歉，这很冗长，这不是一个直接的问题，但是没有伊莎贝尔的教程可以将一个人直接从 A 带到 B。

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

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

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

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

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

此外，Isar 还具有在 Isar 证明块中引入事实assume的命令。presume从我在文档中看到和阅读的内容来看，它不需要在目标中明确列出假设（假设？），并且似乎添加了一个案例来表明假设的陈述遵循其他目标。

所以问题是：我什么时候用presume代替assume，我可以用什么好技巧presume？

Isabelle 有两种证明方式：旧的“应用”方式，证明只是一个链

声明，以及新的“结构化”Isar 风格。我自己，我觉得两者都很有用；“应用”风格更简洁，因此对于无趣的技术引理很方便，而“结构化”风格对于主要定理很方便。

有时我喜欢从一种风格切换到另一种风格，中等证明。从“应用”样式切换到“结构化”样式很容易：我只是插入

在我的应用链中。我的问题是：如何从“结构化”样式切换回“应用”样式？

举一个更具体的例子：假设我有五个子目标。我发出一些“应用”指令来发送前两个子目标。然后我开始进行结构化证明以省去第三个证明。我还有两个子目标：我如何为这些返回“应用”样式？

我创建了一个小证明，目的是创建一个用于next证明案例的示例：

这可以在不丢失细节的情况下简化吗？使用一些神奇的技巧不是我想要的。欢迎改进使用 Isar 的风格。

我试图证明一个存在定理

但我无法完成证明。所以我有必要y，但我怎样才能将它投入到最初的目标中呢？

在 Isar 中，人们使用assume目标的前提，以便她可以使用它来构建结论。

伊莎贝尔/伊萨尔参考 说

这是 的唯一用途assume，即从目标的前提中获取事实吗？

更新：由于有些人认为这太宽泛了，我不明白，我试图重新提出这个问题。

该手册描述了assume. 但它的用途是什么？这是否仅限于我从目标的前提中获得事实的情况？