|
(* 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.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
