问题标签 [isabelle]

假设我们有一些谓词

和一个inductive结束它

第一个参数“a_b”的归纳是固定的。"a_b" 是一个元组，导致语法有些难看。不幸的是，伊莎贝尔不允许我写类似for "(a,b)".

如何为这个归纳谓词创建更好的介绍和归纳规则？

这个问题与我之前关于 type classes的 SO question 有关。我问这个问题是为了建立一个关于语言环境的未来问题。我不认为类型类适用于我正在尝试做的事情，但是类型类的工作方式让我了解了我想要从语言环境中得到什么。

下面，当我使用大括号符号{0,0}时，它并不代表普通的 HOL 大括号，而是代表0空集。

一些文件，如果你想要的话

• A_i130424a.thy - ASCII 友好的 THY。
• i130424a.thy - 非 ASCII 友好的 THY。
• i130424a_DOC.pdf - 显示行号的 PDF。
• MFZ_DOC.pdf - 与之相关的主要项目。
• 此问题的GitHub 文件夹和MFZ GitHub文件夹。

题前谈话

我描述了我在 THY 中所做的事情（包括在底部），然后我基本上会问，“我可以在这里做些什么来解决这个问题，以便我可以使用类型类吗？”

与上面链接的 SO 问题一样，我试图与Groups.thy semigroup_add联系起来。我所做的是使用创建我的类型的子类型sT，typedef然后尝试将一些基本函数常量和运算符提升到新类型中，例如我的联合运算符geU、我的空集emS、我的无序对集paS和我的成员资格谓词inP.

这不起作用，因为我试图将新类型视为子集。特别是，我的新类型应该表示 set { {0,0} }，它旨在成为平凡半群的一部分，一个只有一个元素的半群。

问题是无序对公理声明如果集合x存在则集合(paS x x)存在，而联合公理声明如果集合x存在则集合(geU x)存在。因此，当我尝试将联合运算符提升到我的新类型中时，证明者神奇地知道我需要证明(geU{0,0} = {0,0})，这是不正确的，但{0,0}我的新类型中只有一个元素，所以它必须是那样的。

问题

我可以解决这个问题吗？在我看来，我将集合和子集与类型和子类型进行比较，我知道它们并不相同。调用我的主要类型sT和我的子类型subT。我需要的是所有使用 type 定义的运算符，sT例如，在被视为sT => sTtypesubT时为 type 工作。使用 type 定义的新运算符和常量，例如 type 的函数，它们会以某种方式工作，就像神奇地应该与这些东西一起工作。 subTsTsubTsubT => subT

发表问题谈话

在这里，我通过 THY 中的行号指出发生了什么。行号将显示在 PDF 和 GitHub 站点上。

在第 21 到 71 行中有四个部分，我将相关的常量、符号和公理组合在一起。

1. 类型sT、隶属谓词inP/PIn和等式公理（21 到 33）。
2. 空集emS/SEm和空集公理（37 到 45）。
3. 无序对常数paS/SPa和无序对公理（49 到 58）。
4. 联合常数geU/UGe和联合公理（62 到 71）。

从第 75 行开始，我创建了一个新类型，typedef然后将其实例化为 type class semigroup_add。

在我尝试提升我的无序对函数{.x,y.}（第 108 行）和我的联合函数(geU x)（第 114 行）之前，没有任何问题。

在 Isar 命令下方，我显示的输出告诉我我需要证明某些集合等于{0,0}，这是无法证明的事实。

这是 ASCII 友好的源代码，我从上面链接的 THY 中删除了一些注释和行：

我想了解 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的理论文件时，如何在当前理论文件中隐藏这样的常量？换句话说，我想确保这f是一个自由变量。我不想更改导入的文件。

This questions extends the question How to hide defined constants.

I import theory A, B, and C, maybe in future also D, E, ... All theories define a function f. I want to hide the definition of f in my current theory without changing the imported theories. When I write term f I get A.f. When I add hide_const (open) f to my current theory, A.f is hidden but now I get B.f as f. How can I completely hide f? I need something like (hide_const (open) f)+.

首先，在对类型类了解不多的情况下，似乎类型类是重载类型符号的最佳方式，除非我不能使用类型类，或者不知道如何使用。我没有使用类型类。

其次，我很确定我不想覆盖对所有类型都有意义的运算符的符号，例如\<in>, \<times>, *,\<union>等。

但是，诸如此类的运算符+对我的 type 没有任何意义sT，尽管这与我的第一点有关。我最终希望+type 有多种含义sT => sT => sT，我认为这不会发生。

示例的四个版本

为了使我的问题具体化并表明我不是唯一一个有问题的人，我从Klein 的课程中​​举了一个简单的例子，文件是Demo14.thy。

在示例的四个版本之后，我问：“对于第四个示例，我可以摆脱警告吗？”

他从一个没有警告或错误的简单示例开始：

他使用\<cdot>, 这代表了我到目前为止所做的事情，而不是使用 Isabelle/HOL 已经声称的符号。

我将他的更改\<cdot>为+，我得到一个错误：

在查看了 HOL 源代码后，我看到+已经为 type 定义了它('a => 'a => 'a)，特别是为某些类型类。

我修改semi2以确保它不是'a单独的，然后我只收到警告：

我真正关心的是第四个版本，它给出了一个警告，即使我已经插入(x::sT)：

警告是：

总结和问题

对于我自己，我将其总结如下： 运算符+已在许多地方定义，尤其是 type 'a => 'a => 'a，它通常也为sT => sT => sT. 正因为如此，证明者做了​​很多工作，在最终弄清楚 mysemi4是唯一+为 type 定义的地方之后sT => sT => sT，它让我使用它。

我不知道我的摘要，但我可以修复semi4它不给我警告吗？

*（注意：给定示例，从数学上讲，使用符号代替会更有意义+，但这*是我不想覆盖的符号。）

假设我有一个二元运算符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。

这是 Isabelle 代码生成的后续内容：容器的抽象引理？：

我想为the_question以下理论生成代码：

问题是方程smaller不适合代码生成，因为它提到了抽象函数small。

现在根据 Andreas 对我最后一个问题的回答和关于数据细化的论文，下一步是为小数集引入一种类型，并smaller为该类型创建一个定义：

现在smaller'是可执行的。据我了解，我需要将操作重新定义small list为操作small_list：

我可以为the_question. 但是 的定义small_list_all不适合代码生成，因为它提到了抽象态射small。如何使small_list_all可执行文件？

（请注意，我无法展开 的代码方程a_pred，因为问题实际上发生在实际递归的代码方程中a_pred。另外，我想避免涉及在运行时重新检查不变量的黑客行为。）

我有一个by eval有点慢的证明，我想优化代码。by eval为了不那么盲目地这样做，如果 jEdit 可以显示进行证明所花费的时间，那就太好了。

Isabelle 2013 有可能吗？

In Isabelle's NEWS file, I found

Command 'typedef' now works within a local theory context -- without introducing dependencies on parameters or assumptions, which is not possible in Isabelle/Pure/HOL. Note that the logical environment may contain multiple interpretations of local typedefs (with different non-emptiness proofs), even in a global theory context.

(which dates back to Isabelle2009-2). Is this the latest news with respect to typedef and local theory contexts? Further, what does the restriction "without introducing dependencies on parameters or assumptions" actually mean?

If it would mean that I cannot use locale parameters in the defining set of a typedef, then I would not consider typedef to be localized at all (since the only allowed instances can easily be moved outside the local context, or am I missing something?).

Is it (or should it, or will it ever be) possible to do something along the lines (where the set used for a typedef depends on the locale parameter V):

for which I currently obtain: