author | immler |
Thu, 03 May 2018 15:07:14 +0200 | |
changeset 68073 | fad29d2a17a5 |
parent 63585 | f4a308fdf664 |
permissions | -rw-r--r-- |
33026 | 1 |
(* Title: HOL/Isar_Examples/Peirce.thy |
61932 | 2 |
Author: Makarius |
6444
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 |
|
58882 | 5 |
section \<open>Peirce's Law\<close> |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
6 |
|
31758 | 7 |
theory Peirce |
63585 | 8 |
imports Main |
31758 | 9 |
begin |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
10 |
|
61932 | 11 |
text \<open> |
12 |
We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. This is an inherently |
|
13 |
non-intuitionistic statement, so its proof will certainly involve some form |
|
14 |
of classical contradiction. |
|
7860 | 15 |
|
61541 | 16 |
The first proof is again a well-balanced combination of plain backward and |
17 |
forward reasoning. The actual classical step is where the negated goal may |
|
18 |
be introduced as additional assumption. This eventually leads to a |
|
61932 | 19 |
contradiction.\<^footnote>\<open>The rule involved there is negation elimination; it holds in |
20 |
intuitionistic logic as well.\<close>\<close> |
|
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 |
|
58614 | 31 |
with \<open>\<not> A\<close> show B by contradiction |
10007 | 32 |
qed |
58614 | 33 |
with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A .. |
10007 | 34 |
qed |
35 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
36 |
|
61932 | 37 |
text \<open> |
38 |
In the subsequent version the reasoning is rearranged by means of ``weak |
|
39 |
assumptions'' (as introduced by \<^theory_text>\<open>presume\<close>). Before assuming the negated |
|
40 |
goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put into place in order to |
|
41 |
solve the main problem. Nevertheless, we do not get anything for free, but |
|
42 |
have to establish \<open>A \<longrightarrow> B\<close> later on. The overall effect is that of a logical |
|
43 |
\<^emph>\<open>cut\<close>. |
|
7860 | 44 |
|
61932 | 45 |
Technically speaking, whenever some goal is solved by \<^theory_text>\<open>show\<close> in the context |
46 |
of weak assumptions then the latter give rise to new subgoals, which may be |
|
47 |
established separately. In contrast, strong assumptions (as introduced by |
|
48 |
\<^theory_text>\<open>assume\<close>) are solved immediately. |
|
49 |
\<close> |
|
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" |
58614 | 57 |
with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A .. |
10007 | 58 |
next |
55640 | 59 |
assume "\<not> A" |
60 |
show "A \<longrightarrow> B" |
|
10007 | 61 |
proof |
62 |
assume A |
|
58614 | 63 |
with \<open>\<not> A\<close> 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 |
|
61932 | 68 |
text \<open> |
69 |
Note that the goals stemming from weak assumptions may be even left until |
|
70 |
qed time, where they get eventually solved ``by assumption'' as well. In |
|
71 |
that case there is really no fundamental difference between the two kinds of |
|
72 |
assumptions, apart from the order of reducing the individual parts of the |
|
73 |
proof configuration. |
|
7860 | 74 |
|
61932 | 75 |
Nevertheless, the ``strong'' mode of plain assumptions is quite important in |
76 |
practice to achieve robustness of proof text interpretation. By forcing both |
|
77 |
the conclusion \<^emph>\<open>and\<close> the assumptions to unify with the pending goal to be |
|
78 |
solved, goal selection becomes quite deterministic. For example, |
|
79 |
decomposition with rules of the ``case-analysis'' type usually gives rise to |
|
80 |
several goals that only differ in there local contexts. With strong |
|
61541 | 81 |
assumptions these may be still solved in any order in a predictable way, |
61932 | 82 |
while weak ones would quickly lead to great confusion, eventually demanding |
83 |
even some backtracking. |
|
84 |
\<close> |
|
7860 | 85 |
|
10007 | 86 |
end |