author | blanchet |
Thu, 28 Aug 2014 07:30:16 +0200 | |
changeset 58066 | 96e987003a01 |
parent 55640 | abc140f21caa |
child 58614 | 7338eb25226c |
permissions | -rw-r--r-- |
33026 | 1 |
(* Title: HOL/Isar_Examples/Peirce.thy |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
3 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
4 |
|
10007 | 5 |
header {* Peirce's Law *} |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
6 |
|
31758 | 7 |
theory Peirce |
8 |
imports Main |
|
9 |
begin |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
10 |
|
37671 | 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. |
|
7860 | 14 |
|
37671 | 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.} *} |
|
7860 | 21 |
|
55640 | 22 |
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" |
10007 | 23 |
proof |
55640 | 24 |
assume "(A \<longrightarrow> B) \<longrightarrow> A" |
10007 | 25 |
show A |
26 |
proof (rule classical) |
|
55640 | 27 |
assume "\<not> A" |
28 |
have "A \<longrightarrow> B" |
|
10007 | 29 |
proof |
30 |
assume A |
|
55640 | 31 |
with `\<not> A` show B by contradiction |
10007 | 32 |
qed |
55640 | 33 |
with `(A \<longrightarrow> B) \<longrightarrow> A` show A .. |
10007 | 34 |
qed |
35 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
36 |
|
37671 | 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}. |
|
7860 | 44 |
|
37671 | 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. *} |
|
7860 | 50 |
|
55640 | 51 |
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" |
10007 | 52 |
proof |
55640 | 53 |
assume "(A \<longrightarrow> B) \<longrightarrow> A" |
10007 | 54 |
show A |
55 |
proof (rule classical) |
|
55640 | 56 |
presume "A \<longrightarrow> B" |
57 |
with `(A \<longrightarrow> B) \<longrightarrow> A` show A .. |
|
10007 | 58 |
next |
55640 | 59 |
assume "\<not> A" |
60 |
show "A \<longrightarrow> B" |
|
10007 | 61 |
proof |
62 |
assume A |
|
55640 | 63 |
with `\<not> A` show B by contradiction |
10007 | 64 |
qed |
65 |
qed |
|
66 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
67 |
|
37671 | 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. |
|
7860 | 73 |
|
37671 | 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. *} |
|
7860 | 84 |
|
10007 | 85 |
end |