I came across a proof in Isabelle/HOL that shows the Drinker's Principle. I do understand the entire proof; however, I do not understand very well the next proof case in the Drinker's Principle proof:
assume "∀x. drunk x"
then have "drunk a ⟶ (∀x. drunk x)" for a ..
then show ?thesis ..
Why does the proof also prove "drunk a ⟶ (∀x. drunk x)"? I think it is enough ∀x. drunk x to show ∃x. drunk x.
The entire proof as follows:
theorem Drinker's_Principle: "∃x. drunk x ⟶ (∀x. drunk x)"
proof cases
assume "∀x. drunk x"
then have "drunk a ⟶ (∀x. drunk x)" for a ..
then show ?thesis ..
next
assume "¬ (∀x. drunk x)"
then have "∃x. ¬ drunk x" by (rule de_Morgan)
then obtain a where "¬ drunk a" ..
have "drunk a ⟶ (∀x. drunk x)"
proof
assume "drunk a"
with ‹¬ drunk a› show "∀x. drunk x" by contradiction
qed
then show ?thesis ..
qed
I think it is enough ∀x. drunk x to show ∃x. drunk x.
That's what we are actually doing: the for a at the end of the the statement
then have "drunk a ⟶ (∀x. drunk x)" for a ..
is Isar's way of saying that there is a witness a of "drunk a ⟶ (∀x. drunk x)". The next line of the proof then uses this to prove the version of the statement with the existential premise.