我如何证明一个对象不解释语言环境？

Question

我想将 "big" 自然数定义为大于 10 的自然数，将 "small" 定义为小于 5 的自然数。我可以将这些定义表示为语言环境：

locale Big = 
  fixes k :: ‹nat›
  assumes ‹k > 10›

locale Small =
  fixes k :: ‹nat›
  assumes ‹k < 5›

然后我可以证明 11 是大数，2 是小数：

interpretation Big ‹11 :: nat› by (unfold_locales, simp)
interpretation Small ‹2 :: nat› by (unfold_locales, simp)

但是我如何表达和证明7不小呢？我可以证明它不小于 5，但证明并不令人满意，因为它根本不涉及 locale Small:

lemma ‹¬ ((7 :: nat) < (5 :: nat))› by simp

另外，不存在既大又小的整数怎么表达呢？同样，我可以证明这一点，但只能不参考语言环境：

lemma
  fixes k :: nat
  shows ‹¬ (k < 5 ∧ k > 10)›
  by simp

一般来说，我如何证明某事不是对一种或多种语言环境的解释？还是我滥用了语言环境机制？

Answer 1

命令 locale 记录在 Isar-ref 和文档 "Tutorial to Locales and Locale Interpretation" 中。此外，还有许多相关出版物以更详细和更正式的方式描述了 implementation/syntax。我想到的一份文件是 Clemens Ballarin 的 Locales and Locale Expressions in Isabelle/Isar。它已经过时，但（在我看来）它提供了比 Isar-ref 和教程更详尽的基本概念解释。特别是，请参阅上述文档中的第 3.3 节："Locale Predicates and the Internal Representation of Locales"。

But how would I express and prove that 7 is not Small? I can prove that it is not less than 5, but the proof is unsatisfactory since it does not refer to the locale Small at all:

使用语言环境谓词，您可以在您的问题中陈述定理，如下所示：

lemma "¬Small 7" unfolding Small_def by auto

明确使用语言环境谓词是否明智以及是否存在更好的选项来表达给定的想法取决于上下文。

Moreover, how would I express that no integer exists which is both Big and Small?

lemma "¬(Small x ∧ Big x)" unfolding Small_def Big_def by simp

以上的主要结论是语言环境谓词（例如Small）只是常量，命令locale提供了关于这些常量的几个定理，包括它们的定义（例如Small_def).参考文档提供了更多详细信息。

In general, how do I prove that something is not an interpretation of one or more locales? Or am I misusing the locale mechanism?

不幸的是，在我看来，这些问题需要澄清。总的来说，是否应该使用语言环境、class 或普通定义来定义给定概念取决于应用程序，并且在一定程度上取决于个人偏好。

我如何证明一个对象不解释语言环境？

How do I prove that an object does not interpret a locale?

isabelle