饮水原理

Question

我在Isabelle / HOL中遇到了一个证明饮酒者原则的证据。我确实了解整个证明；但是，我对饮酒者原则证明中的下一个证明案例不太了解：

  assume "∀x. drunk x"
  then have "drunk a ⟶ (∀x. drunk x)" for a ..
  then show ?thesis ..

为什么证明还证明“ 醉dr（∀x。醉x）”？我认为这已经足够了。显示[[x]。醉x。整个证明如下：

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

我在Isabelle / HOL中遇到了一个证明饮酒者原则的证据。我确实了解整个证明；但是，我对饮酒者原则证明中的下一个证明情况不太了解：...

Answer 1

我认为这足够了。喝醉了x以显示∃x。醉x。