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.