src/HOL/Isar_examples/Drinker.thy
 author haftmann Mon Jan 30 08:20:56 2006 +0100 (2006-01-30) changeset 18851 9502ce541f01 parent 16531 9b442d0e5c0c child 31758 3edd5f813f01 permissions -rw-r--r--
```     1 (*  Title:      HOL/Isar_examples/Drinker.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Makarius
```
```     4 *)
```
```     5
```
```     6 header {* The Drinker's Principle *}
```
```     7
```
```     8 theory Drinker imports Main begin
```
```     9
```
```    10 text {*
```
```    11   Here is another example of classical reasoning: the Drinker's
```
```    12   Principle says that for some person, if he is drunk, everybody else
```
```    13   is drunk!
```
```    14
```
```    15   We first prove a classical part of de-Morgan's law.
```
```    16 *}
```
```    17
```
```    18 lemma deMorgan:
```
```    19   assumes "\<not> (\<forall>x. P x)"
```
```    20   shows "\<exists>x. \<not> P x"
```
```    21   using prems
```
```    22 proof (rule contrapos_np)
```
```    23   assume a: "\<not> (\<exists>x. \<not> P x)"
```
```    24   show "\<forall>x. P x"
```
```    25   proof
```
```    26     fix x
```
```    27     show "P x"
```
```    28     proof (rule classical)
```
```    29       assume "\<not> P x"
```
```    30       then have "\<exists>x. \<not> P x" ..
```
```    31       with a show ?thesis by contradiction
```
```    32     qed
```
```    33   qed
```
```    34 qed
```
```    35
```
```    36 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
```
```    37 proof cases
```
```    38   fix a assume "\<forall>x. drunk x"
```
```    39   then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
```
```    40   then show ?thesis ..
```
```    41 next
```
```    42   assume "\<not> (\<forall>x. drunk x)"
```
```    43   then have "\<exists>x. \<not> drunk x" by (rule deMorgan)
```
```    44   then obtain a where a: "\<not> drunk a" ..
```
```    45   have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
```
```    46   proof
```
```    47     assume "drunk a"
```
```    48     with a show "\<forall>x. drunk x" by (contradiction)
```
```    49   qed
```
```    50   then show ?thesis ..
```
```    51 qed
```
```    52
```
```    53 end
```