--- a/src/HOL/Isar_examples/Peirce.thy Tue Oct 20 19:36:52 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-(* 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