饮酒者原则

Question

我在 Isabelle/HOL 中发现了一个证明饮酒者原理的证明。我确实理解整个证明；但是，我不太了解饮酒者原理证明中的下一个证明案例：

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

为什么证明也证明了“醉了一个⟶(∀x.醉了x)”？我觉得够了∀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

Answer 1

I think it is enough ∀x. drunk x to show ∃x. drunk x.

这就是我们实际做的：语句末尾的 for a

then have "drunk a ⟶ (∀x. drunk x)" for a ..

是Isar的说法，有"drunk a ⟶ (∀x. drunk x)"的证人a。证明的下一行然后使用它来证明具有存在前提的语句版本。

饮酒者原则

Drinker's Principle

predicate

isabelle