products/Sources/formale Sprachen/COBOL/Test-Suite/SQL M/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Drinker.thy   Sprache: Unknown

(*  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.0 Sekunden  (vorverarbeitet)  ]