src/HOL/Isar_Examples/Drinker.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 37671 fa53d267dab3
child 47960 e462d33ca960
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 31758
diff changeset
     1
(*  Title:      HOL/Isar_Examples/Drinker.thy
16356
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
     3
*)
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
     4
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
     5
header {* The Drinker's Principle *}
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
     6
31758
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 16531
diff changeset
     7
theory Drinker
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 16531
diff changeset
     8
imports Main
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 16531
diff changeset
     9
begin
16356
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    10
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    11
text {* Here is another example of classical reasoning: the Drinker's
16531
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    12
  Principle says that for some person, if he is drunk, everybody else
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    13
  is drunk!
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    14
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    15
  We first prove a classical part of de-Morgan's law. *}
16356
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    16
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    17
lemma de_Morgan:
16531
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    18
  assumes "\<not> (\<forall>x. P x)"
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    19
  shows "\<exists>x. \<not> P x"
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    20
  using assms
16531
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    21
proof (rule contrapos_np)
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    22
  assume a: "\<not> (\<exists>x. \<not> P x)"
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    23
  show "\<forall>x. P x"
16356
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    24
  proof
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    25
    fix x show "P x"
16356
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    26
    proof (rule classical)
16531
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    27
      assume "\<not> P x"
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    28
      then have "\<exists>x. \<not> P x" ..
9b442d0e5c0c improved proof;
wenzelm
parents: 16417
diff changeset
    29
      with a show ?thesis by contradiction
16356
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    30
    qed
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    31
  qed
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    32
qed
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    33
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    34
theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    35
proof cases
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    36
  fix a assume "\<forall>x. drunk x"
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    37
  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    38
  then show ?thesis ..
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    39
next
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    40
  assume "\<not> (\<forall>x. drunk x)"
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    41
  then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
16356
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    42
  then obtain a where a: "\<not> drunk a" ..
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    43
  have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    44
  proof
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    45
    assume "drunk a"
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    46
    with a show "\<forall>x. drunk x" by contradiction
16356
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    47
  qed
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    48
  then show ?thesis ..
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    49
qed
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    50
94011cf701a4 added Isar_examples/Drinker.thy;
wenzelm
parents:
diff changeset
    51
end