问题标签 [isabelle]

在 Isabelle 中，有时会遇到重复子目标的情况。例如，想象以下证明脚本：

有目标：

有没有办法就地消除重复的子目标，所以不需要重复证明？

我有以下伊莎贝尔目标：

战术simp, fast, clarsimp, blast,fastforce等都没有在目标上取得任何进展，尽管它非常简单。

为什么 Isabelle 不只是简化if构造体，使 "a ≠ a" 和 "b ≠ b" 都变为False，从而解决目标？

我正在用 Isabelle 生成 Scala 代码。如何为我的 Scala 文件指定标题？例如，我想要这样的东西：

如何指定要使用的包？例如，要使用包GENERATED，文件应该以单词开头package GENERATED。

到目前为止，我得到的最好的想法是code_include第二个参数为空的命令 ( "")。如果我选择更长的第二个参数，Efficient_Nat理论首先会发出它的代码。但我必须写到文件的开头。

这个解决方案有多邪恶？如果它不是那么邪恶，我怎么能添加诸如当前日期、当前你的文件以及export_code发生的行之类的东西。我还可以添加我导出的代码方程式但不添加它们的体面吗？

假设我有一个定理：

我想用类似命令non_ASCII_thm_name的东西定义一个 ASCII 名称。notation例如，像这样：

Isar 命令只能与常量一起使用notation。abbreviation是否有允许我这样做的 Isar 命令？

最好，我希望我的 Isar 命令提供的只是同义词。例如，如果我使用sledgehammer，最好只存在一个定理 ，non_ASCII_thm_name这样sledgehammer就不会使用额外的事实ASCII_thm_name。

如何在 Isabelle 中定义一个函数，该函数根据其参数的类型或使用它的上下文的类型而具有不同的定义？

例如，我可能想is_default用 type定义一个函数'a ⇒ bool，其中每种不同的类型'a都有一个可能不同的“默认值”。（为了论证，我还假设现有的概念如zero不合适。）

发布答案跟进问题

Brian 提供了一个答案，建议的解决方案是使用提升和转移。但是，我找不到足够的关于提升和转移的教程信息来了解如何调整他的答案以完成我需要做的事情。

在这里，我在黑暗中工作，并使用作为即插即用模板给出的答案来提出这个后续问题。

我初始代码中的命令为我typedef trivAlg = "{x::sT. x = emS}"提供了一个新类型，它是母类型的子集sT。

我有我的会员操作员consts inP :: "sT => sT => bool"，所以在我对提升和转移的天真看法中，因为我的monoid_add0 已被定义为常量emS::sT，我可以做出这样的声明，(emS::sT) inP emS我想做这样的事情：

所以，我尝试使用提升让我的操作员使用这样inP的类型trivAlg：

theorem但是，由于我使用的类型sT与我的使用trivAlg不兼容，因此我遇到了类型冲突。

如果可以添加答案以向我展示如何让我inP使用类型，trivAlg我将不胜感激。或者，也许我离题了。

（原始）问题的预备知识

我有我的 type sT，它代表“一切都是一个集合”。到目前为止，我所有的常量和操作符都是用单一类型定义的sT。例如，我的空集、成员运算符和联合运算符定义如下：

我现在正在做一些早期调查，以了解我是否可以将 my与Groups.thysT中的广义组联系起来。

从HOL 文档中，我试图从 Groups 的 4.2、4.3 和 4.4 节以及 Nat 的 15.2 和 15.3 节中获取示例。

在这里，我几乎要回答我的问题，但我不知道我是否在问一个聪明的问题。我想我知道的是，解决方案可能只使用语言环境、子语言环境和解释，而不是类型类。

我一直在看locales.pdf和classes.pdf，所以我知道语言环境和类是交织在一起的。我也一直在查看IsarMathLib以了解在那里如何使用语言环境、子语言环境和解释。

问题

我的问题是，在下面我的微不足道的代数结构中trivAlg，这是一个用 定义的新类型typedef，我如何使用类型类进行设置，以便我可以将我的常量（例如emS，上面列出的）inP与geUtype 的元素一起使用trivAlg？

在我列出下面的代码之后，我会问一些关于Groups.thy中特定代码行的问题。

编码

关于 Groups.thy 的后续问题

在 Groups.thy 的第 151 到 155 行，有以下代码：

没有一个文档可以教我如何使用类、语言环境、子语言环境和解释，所以我不知道它到底告诉了我什么。

如果我想使用semigroup_addGroups.thy 中的那个，我可以选择将它用作类型类还是区域设置？

假设我有一个引理mylem: foo ?a = bar ?a，我需要将它应用到一个目标上，该目标有两次出现foo，例如baz (foo (f p q)) (foo (g r s))，但只出现在其中一个位置上。我知道有两种方法可以做到这一点，而不必写出所有的p, q...，这可能是复杂的表达式。

• 使用apply (subst mylem)后跟适当数量（此处为 0 或 1）的back命令。
• 使用apply (subst mylem[where a = 'foo x y', standard]), wherex和y是未绑定的名称。

这里的使用subst只是为了演示；我真的很想修改引理，例如，rule当有多个可能的匹配项我想以这种方式消除歧义时使用它。

这两种方法对我来说都是不好的风格。有没有更好的方法来实现这一目标？

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

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

当 Isabelle 在 ProofGeneral 中显示目标时，假设呈现为在它们周围有括号，如下所示：

然而，在 Isabelle/jEdit 中，这似乎已更改为元含义箭头：

虽然我知道前者有些不标准，但我发现它更容易阅读。有没有办法修改 Isabelle/jEdit 的行为，以旧的 ProofGeneral 样式打印出目标？

我正在试验代码生成器。我的理论包含一个编码不变量的数据类型：

现在我想导出is_one. 看来我首先必须为代码生成器设置数据类型，如下所示：

现在我可以定义一个is_one不违反抽象的代码方程：

问题1：我可以避免将定义small_one拉出is_one吗？

现在我有一个小项目的复合值：

在这种形式下，我无法使用它导出代码（“代码方程式 foo 中的抽象违规...”）。

问题 2：如何[code abstract]为这样的值定义引理？似乎代码生成器不接受形式的引理map to_nat foo = ...。