src/HOL/Isar_Examples/Peirce.thy
 author wenzelm Sat, 07 Apr 2012 16:41:59 +0200 changeset 47389 e8552cba702d parent 37671 fa53d267dab3 child 55640 abc140f21caa permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

(*  Title:      HOL/Isar_Examples/Peirce.thy
Author:     Markus Wenzel, TU Muenchen
*)

theory Peirce
imports Main
begin

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
there is negation elimination; it holds in intuitionistic logic as
well.} *}

theorem "((A --> B) --> A) --> A"
proof
assume "(A --> B) --> A"
show A
proof (rule classical)
assume "~ A"
have "A --> B"
proof
assume A
with ~ A show B by contradiction
qed
with (A --> B) --> A 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 "(A --> B) --> A"
show A
proof (rule classical)
presume "A --> B"
with (A --> B) --> A show A ..
next
assume "~ A"
show "A --> B"
proof
assume A
with ~ A show 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 text
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 rules of the case-analysis'' type usually gives 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