--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/Peirce.thy Tue Oct 20 19:37:09 2009 +0200
@@ -0,0 +1,90 @@
+(* Title: HOL/Isar_Examples/Peirce.thy
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+header {* Peirce's Law *}
+
+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
+ 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 "(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