--- a/src/HOL/Isar_Examples/Peirce.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Peirce.thy Thu Jul 01 18:31:46 2010 +0200
@@ -8,17 +8,16 @@
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.
+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.}
-*}
+ 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
@@ -35,21 +34,19 @@
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}.
+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.
-*}
+ 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
@@ -68,23 +65,21 @@
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.
+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.
-*}
+ 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