Isabelle trivial issue: “Max (S::nat set) = 0” implies all elements of S are zero

Question

I was trying to prove the following implication:

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.*)

I thought this would be rather trivial, which is why I tried to get a proof using sledgehammer. Unfortunately this failed. Either my definition is wrong or there is some difficulties with automatic proofs involving big operators like Max.

I tried to get a better understanding of Max and max by looking at their definitions as well as any documentation I could find. As I previously ran into a problem with Isabelle which in the end turned out to require a lot of experience despite its trivial appearance ("Why won't Isabelle simplify the body of my "if _ then _ else" construct?"), I decided to post this question here.

Answer 1

The theorem as such will not be provable, as Max is defined via fold1, which in turn is a definition that (to the best of my knowledge) only works with finite sets. For finite sets sledgehammer is successful:

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’s handling of partial functions is a bit unfortunate, and the fact that

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

is a theorem (sledgehammer finds it) probably makes newcomers to Isabelle uneasy. (If only the result were -1/12...). But it’s something we have to live with.