max - 伊莎贝尔琐碎的问题 : “Max (S::nat set) = 0” implies all elements of S are zero

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 的问题，尽管它看起来很琐碎，但最终证明需要大量经验(“Why won't Isabelle simplify the body of my "if _ then _ else" construct?”)，所以我决定在这里发布这个问题。

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"

是一个定理(sledgehammer 发现了它)可能会让 Isabelle 的新人感到不安。 (要是结果是-1/12 ...就好了)。但这是我们必须忍受的事情。