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

Question

我想将“大”自然数定义为大于 10 的自然数，将“小”自然数定义为小于 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，但证明并不令人满意，因为它根本没有引用语言环境 Small：

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

此外，我如何表达不存在既大又小的整数？同样，我可以证明这一点，但只需要不参考语言环境：

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

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

Answer 1

命令locale 记录在 Isar-ref 和文档“语言环境和语言环境解释教程”中。此外，还有许多相关出版物以更详细和更正式的方式描述了实现/语法。我想到的一份文件是 Clemens Ballarin 的 Locales and Locale Expressions in Isabelle/Isar。它已经过时了，但（在我看来）它提供了比 Isar-ref 和教程更详细的基本概念解释。具体请参见上述文档中的第 3.3 节：“语言环境谓词和语言环境的内部表示”。

---

但是我该如何表达和证明 7 不是小呢？我可以证明 不小于 5，但证明不令人满意，因为它 根本不涉及区域设置 Small：

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

lemma "¬Small 7" unfolding Small_def by auto

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

---

此外，我将如何表达不存在既大的整数 和小？

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

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

---

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

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