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

问题描述

我想将“大”自然数定义为大于 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

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

标签： isabelle

该命令locale记录在 Isar-ref 和文档“Tutorial to Locales and Locale Interpretation”中。此外，还有许多相关出版物以更详细和更正式的方式描述了实现/语法。我想到的一份文件是Clemens Ballarin在 Isabelle/Isar 中的 Locales 和 Locale Expressions 。它已经过时了，但是（在我看来）它提供了比 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）。参考文件提供了更多细节。

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

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

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

问题描述

解决方案

推荐阅读