(* Title: HOL/Isar_examples/Peirce.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
header {* Peirce's Law *};
theory Peirce = Main:;
text {*
We consider Peirce's Law: $((A \impl B) \impl A) \impl A$. This is
an inherently non-intuitionistic statement, so its proof will
certainly involve some form of classical contradiction.
The first proof is again a well-balanced combination of plain
backward and forward reasoning. The actual classical step is where
the negated goal may be introduced as additional assumption. This
eventually leads to a contradiction.\footnote{The rule involved there
is negation elimination; it holds in intuitionistic logic as well.}
*};
theorem "((A --> B) --> A) --> A";
proof;
assume aba: "(A --> B) --> A";
show A;
proof (rule classical);
assume "~ A";
have "A --> B";
proof;
assume A;
thus B; by contradiction;
qed;
with aba; show A; ..;
qed;
qed;
text {*
In the subsequent version the reasoning is rearranged by means of
``weak assumptions'' (as introduced by \isacommand{presume}). Before
assuming the negated goal $\neg A$, its intended consequence $A \impl
B$ is put into place in order to solve the main problem.
Nevertheless, we do not get anything for free, but have to establish
$A \impl B$ later on. The overall effect is that of a logical
\emph{cut}.
Technically speaking, whenever some goal is solved by
\isacommand{show} in the context of weak assumptions then the latter
give rise to new subgoals, which may be established separately. In
contrast, strong assumptions (as introduced by \isacommand{assume})
are solved immediately.
*};
theorem "((A --> B) --> A) --> A";
proof;
assume aba: "(A --> B) --> A";
show A;
proof (rule classical);
presume "A --> B";
with aba; show A; ..;
next;
assume "~ A";
show "A --> B";
proof;
assume A;
thus B; by contradiction;
qed;
qed;
qed;
text {*
Note that the goals stemming from weak assumptions may be even left
until qed time, where they get eventually solved ``by assumption'' as
well. In that case there is really no fundamental difference between
the two kinds of assumptions, apart from the order of reducing the
individual parts of the proof configuration.
Nevertheless, the ``strong'' mode of plain assumptions is quite
important in practice to achieve robustness of proof document
interpretation. By forcing both the conclusion \emph{and} the
assumptions to unify with the pending goal to be solved, goal
selection becomes quite deterministic. For example, decomposition
with ``case-analysis'' type rules usually give rise to several goals
that only differ in there local contexts. With strong assumptions
these may be still solved in any order in a predictable way, while
weak ones would quickly lead to great confusion, eventually demanding
even some backtracking.
*};
end;