src/HOL/Isar_Examples/Peirce.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 55640 abc140f21caa child 58614 7338eb25226c permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
1 (*  Title:      HOL/Isar_Examples/Peirce.thy
2     Author:     Markus Wenzel, TU Muenchen
3 *)
5 header {* Peirce's Law *}
7 theory Peirce
8 imports Main
9 begin
11 text {* We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.
12   This is an inherently non-intuitionistic statement, so its proof
13   will 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
18   eventually leads to a contradiction.\footnote{The rule involved
19   there is negation elimination; it holds in intuitionistic logic as
20   well.} *}
22 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
23 proof
24   assume "(A \<longrightarrow> B) \<longrightarrow> A"
25   show A
26   proof (rule classical)
27     assume "\<not> A"
28     have "A \<longrightarrow> B"
29     proof
30       assume A
31       with \<not> A show B by contradiction
32     qed
33     with (A \<longrightarrow> B) \<longrightarrow> A show A ..
34   qed
35 qed
37 text {* In the subsequent version the reasoning is rearranged by means
38   of weak assumptions'' (as introduced by \isacommand{presume}).
39   Before assuming the negated goal $\neg A$, its intended consequence
40   $A \impl B$ is put into place in order to solve the main problem.
41   Nevertheless, we do not get anything for free, but have to establish
42   $A \impl B$ later on.  The overall effect is that of a logical
43   \emph{cut}.
45   Technically speaking, whenever some goal is solved by
46   \isacommand{show} in the context of weak assumptions then the latter
47   give rise to new subgoals, which may be established separately.  In
48   contrast, strong assumptions (as introduced by \isacommand{assume})
49   are solved immediately. *}
51 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
52 proof
53   assume "(A \<longrightarrow> B) \<longrightarrow> A"
54   show A
55   proof (rule classical)
56     presume "A \<longrightarrow> B"
57     with (A \<longrightarrow> B) \<longrightarrow> A show A ..
58   next
59     assume "\<not> A"
60     show "A \<longrightarrow> B"
61     proof
62       assume A
63       with \<not> A show B by contradiction
64     qed
65   qed
66 qed
68 text {* Note that the goals stemming from weak assumptions may be even
69   left until qed time, where they get eventually solved by
70   assumption'' as well.  In that case there is really no fundamental
71   difference between the two kinds of assumptions, apart from the
72   order of reducing the individual parts of the proof configuration.
74   Nevertheless, the strong'' mode of plain assumptions is quite
75   important in practice to achieve robustness of proof text
76   interpretation.  By forcing both the conclusion \emph{and} the
77   assumptions to unify with the pending goal to be solved, goal
78   selection becomes quite deterministic.  For example, decomposition
79   with rules of the case-analysis'' type usually gives rise to
80   several goals that only differ in there local contexts.  With strong
81   assumptions these may be still solved in any order in a predictable
82   way, while weak ones would quickly lead to great confusion,
83   eventually demanding even some backtracking. *}
85 end