max - Isabelle 琐碎问题：“Max (S::nat set) = 0”意味着 S 的所有元素都为零

Question

我试图证明以下含义：

lemma Max_lemma:
  fixes s::nat and S :: "nat set"
  shows " ((Max S) = (0::nat)) ⟹ (∀ s ∈ S . (s = 0))"
sorry
(* 
  Note: I added additional parentheses just to be sure.*)

我认为这将是相当微不足道的，这就是为什么我尝试使用大锤来证明。不幸的是，这失败了。要么我的定义是错误的，要么涉及像 Max 这样的大运营商的自动证明存在一些困难。

我试图通过查看它们的定义以及我能找到的任何文档来更好地理解 Max 和 max。正如我之前遇到过 Isabelle 的一个问题，尽管它看起来微不足道（“为什么 Isabelle 不简化我的“if _ then _ else”构造的主体？ ”），但最终结果证明它需要大量经验，我决定在这里发布这个问题。

Answer 1

这样的定理将无法证明，正如Max通过 定义的那样fold1，这又是一个定义（据我所知）仅适用于有限集。对于有限集大锤是成功的：

lemma Max_lemma:
  fixes s::nat and S :: "nat set"
  assumes "finite S"
  shows " ((Max S) = (0::nat)) ⟹ (∀ s ∈ S . (s = 0))"
using assms by (metis Max_ge le_0_eq)

Isabelle 对偏函数的处理有点不幸，事实上

"(∑n ∈ {1::nat..}. n) = 0"

是一个定理（大锤发现它）可能会让伊莎贝尔的新手感到不安。（如果只有结果是-1/12 ...）。但这是我们必须忍受的。