src/HOL/Isar_Examples/Drinker.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 49930 defce6616890 child 58614 7338eb25226c permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
```     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 {* 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 lemma de_Morgan:
```
```    18   assumes "\<not> (\<forall>x. P x)"
```
```    19   shows "\<exists>x. \<not> P x"
```
```    20 proof (rule classical)
```
```    21   assume "\<not> (\<exists>x. \<not> P x)"
```
```    22   have "\<forall>x. P x"
```
```    23   proof
```
```    24     fix x show "P x"
```
```    25     proof (rule classical)
```
```    26       assume "\<not> P x"
```
```    27       then have "\<exists>x. \<not> P x" ..
```
```    28       with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
```
```    29     qed
```
```    30   qed
```
```    31   with `\<not> (\<forall>x. P x)` show ?thesis by contradiction
```
```    32 qed
```
```    33
```
```    34 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
```
```    35 proof cases
```
```    36   fix a assume "\<forall>x. drunk x"
```
```    37   then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
```
```    38   then show ?thesis ..
```
```    39 next
```
```    40   assume "\<not> (\<forall>x. drunk x)"
```
```    41   then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
```
```    42   then obtain a where a: "\<not> drunk a" ..
```
```    43   have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
```
```    44   proof
```
```    45     assume "drunk a"
```
```    46     with a show "\<forall>x. drunk x" by contradiction
```
```    47   qed
```
```    48   then show ?thesis ..
```
```    49 qed
```
```    50
```
```    51 end
```