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" thenhave"\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" thenhave"drunk a \ (\x. drunk x)" for a .. thenshow ?thesis .. next assume"\ (\x. drunk x)" thenhave"\x. \ drunk x" by (rule de_Morgan) thenobtain 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 thenshow ?thesis .. qed
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.
