Quelle Drinker.thy Sprache: Isabelle

(*  Title:      HOL/Examples/Drinker.thy
    Author:     Makarius
*)

section \<open>The Drinker's Principle\<close>

theory Drinker
  imports Main
begin

text \<open>
  Here is another example of classical reasoning: the Drinker's Principle says
  that for some person, if he is drunk, everybody else is drunk!

  We first prove a classical part of de-Morgan's law.
\<close>

lemma de_Morgan:
  assumes "\ (\x. P x)"
  shows "\x. \ P x"
proof (rule classical)
  assume "\x. \ P x"
  have "\x. P x"
  proof
    fix x show "P x"
    proof (rule classical)
      assume "\ P x"
      then have "\x. \ P x" ..
      with \<open>\<nexists>x. \<not> P x\<close> show ?thesis by contradiction
    qed
  qed
  with \<open>\<not> (\<forall>x. P x)\<close> show ?thesis by contradiction
qed

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 \<open>\<not> drunk a\<close> show "\<forall>x. drunk x" by contradiction
  qed
  then show ?thesis ..
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.