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