1

我想在语言环境解释所需的证明中使用我的结构的一些属性

例如，假设我定义了谓词 P 并证明了一些关于对满足谓词的元素的操作的引理（add是一个封闭的二元运算，add是关联的并且存在zero中性元素）addP

我想将我的元素集解释为满足某些语言环境的结构，例如monoid

interpretation "{s . P s}" :: monoid "(add)" "(zero)"
unfolding
  monoid_def
using
  add_is_associative
  zero_is_neutral

但是在我的证明目标中，我无法得到所有元素实际上都满足谓词P，并且我留下了一个通用目标，例如add zero a = a我已经证明了我的集合中的元素。

如何在我的目标中强制所有元素都满足谓词P？

4

1 回答 1

1

我将尝试对您的问题发表评论。如果您发现我的评论不足以回答您的问题，请随时在评论中提出更多问题。

首先，我想提一下，Isabelle 的标准文档中有一个关于语言环境和语言环境解释的很好的教程。该文档的名称是“Tutorial to Locales and Locale Interpretation”（由 Clemens Ballarin 撰写）。该文档还包含一些有用的参考资料。

在学习了教程和参考资料之后，查看文档“Isabelle/Isar 参考手册”中的第 5.7 节也可能会有所帮助。

我想在语言环境解释所需的证明中使用我的结构的一些属性

参考手册中对语言环境解释的描述指出

可以实例化语言环境，并将生成的实例化声明添加到当前上下文中。这需要（实例化规范的）证明，称为语言环境解释。

当您interpretation使用一组适当声明的参数调用命令时，该命令实现的目标仅取决于参数。您提供的证明已解除目标的证明对“产生的实例化声明”没有影响。因此，从技术上讲，您是否使用您明确提到的函数的属性来证明解释并不重要。

我想将我的元素集解释为 满足某些语言环境的结构，例如monoid： interpretation "{s . P s}" :: monoid "(add)" "(zero)"

如果您查看interpretation参考手册（第 5.7.3 节）中的命令规范，您会意识到该命令采用“语言环境表达式”作为其输入参数。“语言环境表达式”在参考手册的第 5.7.1 节中进行了描述。在这里，我对语言环境表达式进行了显着简化（不完整）的描述：

qualifier : name pos_insts

字段“限定符”是可选的，字段“名称”保留用于您尝试解释的语言环境的名称。因此，"{s . P s}" :: monoid "(add)" "(zero)"您在问题中提供的表达式不是有效的语言环境表达式。我只能猜测您的意思是使用单冒号而不是双冒号::，即"{s . P s}" : monoid "(add)" "(zero)"我将根据这个假设继续回答。

在您提供的示例中，“限定符”是"{s . P s}"，“名称”是monoid，“pos_insts”实际上是名称后指定的术语。

返回文档，您还将找到字段“限定符”的描述：

实例有一个可选的限定符，适用于声明中的名称

...

限定符只影响名称空间；它们在确定一个语言环境实例是否包含另一个语言环境实例方面没有任何作用。

因此，"{s . P s}"您指定的限定符只能对声明的名称产生影响。它不会影响命令及其输出的目标。

interpretation "{s . P s}" : monoid "(add)" "(zero)"

回到您的示例，如果您monoid从理论中引用语言环境HOL-Groups，那么，如果您研究其规范以及语言环境的规范semigroup，您将能够推断该语言环境monoid有两个与之相关的参数：f和z. 没有其他参数，并且与区域相关联的 monoid 的“载体集”由给定类型的所有术语组成。

locale monoid = semigroup +
  fixes z :: 'a ("❙1")
  assumes left_neutral [simp]: "❙1 ❙* a = a"
  assumes right_neutral [simp]: "a ❙* ❙1 = a"

总之，monoid该理论的语言环境HOL-Groups不适合在作为给定类型术语的适当子集的显式载体集上表示幺半群。

对于您的应用程序，您将需要使用表示显式载体集上的幺半群的语言环境，例如，monoidtheory中的语言环境HOL-Algebra.Group。您可以在理论中看到其解释的示例HOL-Algebra.IntRing。

更新

monoid根据评论中给出问题的作者的要求，我提供了一个从理论中解释语言环境的示例HOL-Algebra.Group：

theory SO_Question
  imports "HOL-Algebra.Group"

begin

abbreviation even_monoid :: "int monoid" ("⇩2") where 
  "even_monoid ≡ ⦇carrier = {x. x mod 2 = 0}, mult = (+), one = 0::int⦈"

interpretation even_monoid: monoid ⇩2
  by unfold_locales auto+

end
于 2019-05-30T19:56:26.243 回答