问题标签 [isabelle]

假设我们正在使用一对类型('a × 'a)并为它定义一个fun模式匹配。

如果我现在有一个a_btype 变量，('a × 'a)我如何(a,b)在应用样式证明中将其替换为它的对表示。例如，显示以下引理的最佳方式是什么？我该如何test a_b c替换test (a,b) c？

这是否也适用于假设中的对？

disj_union我想提升到商类型 ( ) 的集合上有一个部分定义的运算符 (下面natq)。从道德上讲，我认为这应该没问题，因为总是可以在等价类中找到定义了运算符 [*] 的一些代表。但是，我无法完成提升定义保留等价性的证明，因为disj_union只是部分定义。在下面的理论文件中，我提出了一种我找到的定义disj_union运算符的方法，但我不喜欢它，因为它具有很多功能，abs而且Rep我认为它很难使用（对吗？）。

使用 Isabelle 中的商来定义这种事情的好方法是什么？

[*] 这有点像如何只在绑定变量不冲突的条件下定义避免捕获替换；始终可以通过重命名为 alpha 等价类中的另一个代表来满足的条件。

我有以下目标：

我想将此目标分解为六个子目标P 0，P 1，P 2，P 3和。这很容易做到。但是用于执行此操作的相关规则是什么？我问是因为我的实际目标看起来更像这样：P 4P 5apply autoauto

并且apply auto不会以同样的方式打破这个目标（它给了我

反而）。

考虑以下愚蠢的例子

接下来我想使用strict_subset引理并替换A两者A，B它会这样做，但是它将现有的重命名A为Aa，完全违背了引入引理的目的。

如果我使用派生引理strict_subset2，一切都会很好，所以我相信我的推理是合理的。

关键是大多数标准引理都是形式strict_subset而不是形式strict_subset2，伊莎贝尔的制造者不可能让我strict_subset2先自己制作，所以，我一定做错了什么。

我想明白为什么A要改名？我认为这与打字系统有关，因为我认为我还看到了只要类型完全正确，元通用量化就不是问题的例子。

另一个问题是我是否可以以A某种方式阻止重命名？

当然，很可能这两个问题实际上都与真正正确的答案无关，因为我对伊莎贝尔还是很陌生。

PS。是否也可以从 Isabelle 那里获得漂亮的符号？

假设我有一套A ⊆ nat. 我想在 Isabelle 中建模一个函数f : A ⇒ Y。我可以使用任何一个：

1. 偏函数，即 type 之一nat ⇒ Y option，或
2. 一个总函数，即nat ⇒ Y未指定输入的类型之一不在A.

我想知道哪个是“更好”的选择。我看到几个因素：

• “偏函数”方法更好，因为它更容易比较偏函数的相等性。也就是说，如果我想看看是否f等于另一个函数g : A ⇒ Y，那么我就说f = g。要比较未指定的总函数f和g，我不得不说∀x ∈ A. f x = g x。

• “未指定的总函数”方法更好，因为我不必一直关心构造/解构option类型。例如，如果f是一个未指定的总函数，并且x ∈ A，那么我只能说f x，但如果f是一个部分函数，​​我不得不说(the ∘ f) x。再举一个例子，对部分函数进行函数组合比对总函数进行函数组合更棘手。

对于与此问题相关的具体实例，请考虑以下形式化简单图形的尝试。

图由一组节点、它们之间的边关系以及label每个节点的边关系组成。我们只关心位于 中的节点的标签V。那么，应该label是带有 的部分函数node ⇒ 'a option，dom label = V​​还是应该只是在 之外未指定的总函数V？

在 Isabelle 中，人们经常可以达到证明目标，其中中间类型的术语对证明的正确性至关重要。例如，考虑以下引理将nat42 转换为'a wordthen 再返回：

现在这个陈述的真假取决于 的类型of_nat 42：如果是32 word，那么这个陈述是真的，如果它是一个2 word，那么这个陈述是假的。

不幸的是，我似乎无法让 Isabelle 向我展示这种中间类型。

我尝试了以下方法：

• declare [[show_types]]
• declare [[show_sorts]]
• local_setup {* Config.put show_all_types true *}

所有这些都只显示：

在紧要关头，可以这样做：

确实得到了原始转储term，但我希望有更好的方法。

有没有一种在证明目标中显示中间项类型的好方法？

鉴于我对代码生成有一个非常简单的定义。它仅针对某些情况定义，否则会引发运行时异常。

现在我想显示blubb正确。应该忽略抛出异常的情况（从我的角度来看，而不是从数学的角度来看）。但是，我最终得到了一个假设某个任意值X是undefined. 以下引理或多或少等同于子目标。我想显示False，因为我想忽略抛出异常（即undefined返回）的情况。

这是无法证明的。

显示可能引发异常或处理的函数正确性的最佳方法是什么undefined？这与这个问题有关。

这个问题是指使用 Isabelle/HOL 定理证明器生成代码。

当我distinct在列表中导出函数的代码时

我得到以下代码

此代码具有二次运行时。有更快的版本吗？我想"~~/src/HOL/Library/Code_Char"在我的理论开始时导入字符串，并为列表设置有效的代码生成。一个更好的实现distinct是在 O(n log n) 中对列表进行排序并遍历列表一次。但我想一个人可以做得更好吗？

无论如何，是否有更快的实现distinct，也许还有其他Main可用的功能？

当我apply (rule)在应用脚本中使用时，通常会选择适当的规则。这同样适用proof于结构化证明。我在哪里可以了解/查找使用的规则的名称？

我从 Isabelle/HOL 理论手册中阅读了代码生成。不过，我还是觉得有点失落。我在哪里需要类似的东西linorder？我如何使用例如红黑树来加快速度？locale在程序细化的上下文中如何使用？...

是否有一些教程可以开始细化？如果没有，是否有一些简短的、独立的、正确的示例？

我们可以开发一个例子吗？

让我们假设我们有A :: 'a set并且我们知道finite A。我们如何继续生成例如有效的代码a ∈ A？

我们如何表达我们对finite A. 我们如何才能将数学理论（a ∈ A）与代码生成和优化分开？