src/HOL/Isar_examples/Peirce.thy
 author haftmann Mon Jan 30 08:20:56 2006 +0100 (2006-01-30) changeset 18851 9502ce541f01 parent 16417 9bc16273c2d4 child 23373 ead82c82da9e permissions -rw-r--r--
1 (*  Title:      HOL/Isar_examples/Peirce.thy
2     ID:         $Id$
3     Author:     Markus Wenzel, TU Muenchen
4 *)
6 header {* Peirce's Law *}
8 theory Peirce imports Main begin
10 text {*
11  We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.  This is
12  an inherently non-intuitionistic statement, so its proof will
13  certainly involve some form of classical contradiction.
15  The first proof is again a well-balanced combination of plain
16  backward and forward reasoning.  The actual classical step is where
17  the negated goal may be introduced as additional assumption.  This
19  is negation elimination; it holds in intuitionistic logic as well.}
20 *}
22 theorem "((A --> B) --> A) --> A"
23 proof
24   assume aba: "(A --> B) --> A"
25   show A
26   proof (rule classical)
27     assume "~ A"
28     have "A --> B"
29     proof
30       assume A
32     qed
33     with aba show A ..
34   qed
35 qed
37 text {*
38  In the subsequent version the reasoning is rearranged by means of
39  weak assumptions'' (as introduced by \isacommand{presume}).  Before
40  assuming the negated goal $\neg A$, its intended consequence $A \impl 41 B$ is put into place in order to solve the main problem.
42  Nevertheless, we do not get anything for free, but have to establish
43  $A \impl B$ later on.  The overall effect is that of a logical
44  \emph{cut}.
46  Technically speaking, whenever some goal is solved by
47  \isacommand{show} in the context of weak assumptions then the latter
48  give rise to new subgoals, which may be established separately.  In
49  contrast, strong assumptions (as introduced by \isacommand{assume})
50  are solved immediately.
51 *}
53 theorem "((A --> B) --> A) --> A"
54 proof
55   assume aba: "(A --> B) --> A"
56   show A
57   proof (rule classical)
58     presume "A --> B"
59     with aba show A ..
60   next
61     assume "~ A"
62     show "A --> B"
63     proof
64       assume A
66     qed
67   qed
68 qed
70 text {*
71  Note that the goals stemming from weak assumptions may be even left
72  until qed time, where they get eventually solved by assumption'' as
73  well.  In that case there is really no fundamental difference between
74  the two kinds of assumptions, apart from the order of reducing the
75  individual parts of the proof configuration.
77  Nevertheless, the strong'' mode of plain assumptions is quite
78  important in practice to achieve robustness of proof text
79  interpretation.  By forcing both the conclusion \emph{and} the
80  assumptions to unify with the pending goal to be solved, goal
81  selection becomes quite deterministic.  For example, decomposition
82  with rules of the case-analysis'' type usually gives rise to
83  several goals that only differ in there local contexts.  With strong
84  assumptions these may be still solved in any order in a predictable
85  way, while weak ones would quickly lead to great confusion,
86  eventually demanding even some backtracking.
87 *}
89 end