Isabelle тривиальный вопрос: «Max (S :: нац набор) = 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, посмотрев их определения, а также любую документацию, которую я мог найти. Поскольку я ранее сталкивался с проблемой с 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) 

Изабеллы частичных функций является немного неудачным, и тот факт, что

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

теорема (кувалда находит), вероятно, делает новичкам Изабелле непросто. (Если только результат был -1/12 ...). Но с этим нам нужно жить.