Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: json.scala Sprache: Isabelle

Original von: 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

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.