如何将假设传递给语言环境的解释

Question

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

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

的元素的 add 操作

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

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

但是为了证明我的目标，我无法获得所有元素实际上满足谓词 P 我只剩下一个通用目标例如 add zero a = a 我已经为我的集合中的元素证明了这一点。

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

Answer 1

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

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

学习教程和参考资料后，查看文档中的第 5.7 节可能也会有用 "The Isabelle/Isar Reference Manual"。

I would like to use some properties of my structure in the proof required by a locale interpretation

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

Locales may be instantiated, and the resulting instantiated declarations added to the current context. This requires proof (of the instantiated specification) and is called locale interpretation.

当您使用一组适当陈述的参数调用命令 interpretation 时，命令执行的目标仅取决于参数。您提供的证明已履行目标的证明不会对'resulting instantiated declarations'产生任何影响。因此，从技术上讲，您是否使用您明确提到的函数的属性来证明解释并不重要。

I would like to interpret then the set of my elements as a structure that satisfy some locale, e.g. monoid: interpretation "{s . P s}" :: monoid "(add)" "(zero)"

如果您查看参考手册（第 5.7.3 节）中命令 interpretation 的说明，您会发现该命令采用 'locale expression' 作为其输入参数。 'locale expression' 在参考手册的第 5.7.1 节中有描述。在这里，我对语言环境表达式进行了显着简化（不完整）的描述：

qualifier : name pos_insts

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

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

返回文档您还会找到字段的描述 'qualifier':

Instances have an optional qualifier which applies to names in declarations

...

Qualifiers only affect name spaces; they play no role in determining whether one locale instance subsumes another.

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

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

回到你的例子，如果你指的是理论HOL-Groups中的语言环境monoid，那么，如果你研究它的规范以及语言环境的规范semigroup ，您将能够推断出语言环境 monoid 有两个与之关联的参数：f 和 z。没有其他参数，与语言环境关联的幺半群的 'carrier set' 由给定类型的所有项组成。

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

总而言之，理论 HOL-Groups 中的语言环境 monoid 不适合表示显式载体集上的幺半群，该载体集是给定类型项的真子集。

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

更新

应评论中问题作者的要求，我提供了一个从理论 HOL-Algebra.Group:

解释语言环境 monoid 的例子

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

如何将假设传递给语言环境的解释

How to pass assumptions to interpretation of locale

isabelle

isar