src/HOL/Isar_Examples/Peirce.thy
 changeset 37671 fa53d267dab3 parent 33026 8f35633c4922 child 55640 abc140f21caa
     1.1 --- a/src/HOL/Isar_Examples/Peirce.thy	Thu Jul 01 14:32:57 2010 +0200
1.2 +++ b/src/HOL/Isar_Examples/Peirce.thy	Thu Jul 01 18:31:46 2010 +0200
1.3 @@ -8,17 +8,16 @@
1.4  imports Main
1.5  begin
1.6
1.7 -text {*
1.8 - We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.  This is
1.9 - an inherently non-intuitionistic statement, so its proof will
1.10 - certainly involve some form of classical contradiction.
1.11 +text {* We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.
1.12 +  This is an inherently non-intuitionistic statement, so its proof
1.13 +  will certainly involve some form of classical contradiction.
1.14
1.15 - The first proof is again a well-balanced combination of plain
1.16 - backward and forward reasoning.  The actual classical step is where
1.17 - the negated goal may be introduced as additional assumption.  This
1.19 - is negation elimination; it holds in intuitionistic logic as well.}
1.20 -*}
1.21 +  The first proof is again a well-balanced combination of plain
1.22 +  backward and forward reasoning.  The actual classical step is where
1.23 +  the negated goal may be introduced as additional assumption.  This
1.25 +  there is negation elimination; it holds in intuitionistic logic as
1.26 +  well.} *}
1.27
1.28  theorem "((A --> B) --> A) --> A"
1.29  proof
1.30 @@ -35,21 +34,19 @@
1.31    qed
1.32  qed
1.33
1.34 -text {*
1.35 - In the subsequent version the reasoning is rearranged by means of
1.36 - weak assumptions'' (as introduced by \isacommand{presume}).  Before
1.37 - assuming the negated goal $\neg A$, its intended consequence $A \impl 1.38 - B$ is put into place in order to solve the main problem.
1.39 - Nevertheless, we do not get anything for free, but have to establish
1.40 - $A \impl B$ later on.  The overall effect is that of a logical
1.41 - \emph{cut}.
1.42 +text {* In the subsequent version the reasoning is rearranged by means
1.43 +  of weak assumptions'' (as introduced by \isacommand{presume}).
1.44 +  Before assuming the negated goal $\neg A$, its intended consequence
1.45 +  $A \impl B$ is put into place in order to solve the main problem.
1.46 +  Nevertheless, we do not get anything for free, but have to establish
1.47 +  $A \impl B$ later on.  The overall effect is that of a logical
1.48 +  \emph{cut}.
1.49
1.50 - Technically speaking, whenever some goal is solved by
1.51 - \isacommand{show} in the context of weak assumptions then the latter
1.52 - give rise to new subgoals, which may be established separately.  In
1.53 - contrast, strong assumptions (as introduced by \isacommand{assume})
1.54 - are solved immediately.
1.55 -*}
1.56 +  Technically speaking, whenever some goal is solved by
1.57 +  \isacommand{show} in the context of weak assumptions then the latter
1.58 +  give rise to new subgoals, which may be established separately.  In
1.59 +  contrast, strong assumptions (as introduced by \isacommand{assume})
1.60 +  are solved immediately. *}
1.61
1.62  theorem "((A --> B) --> A) --> A"
1.63  proof
1.64 @@ -68,23 +65,21 @@
1.65    qed
1.66  qed
1.67
1.68 -text {*
1.69 - Note that the goals stemming from weak assumptions may be even left
1.70 - until qed time, where they get eventually solved by assumption'' as
1.71 - well.  In that case there is really no fundamental difference between
1.72 - the two kinds of assumptions, apart from the order of reducing the
1.73 - individual parts of the proof configuration.
1.74 +text {* Note that the goals stemming from weak assumptions may be even
1.75 +  left until qed time, where they get eventually solved by
1.76 +  assumption'' as well.  In that case there is really no fundamental
1.77 +  difference between the two kinds of assumptions, apart from the
1.78 +  order of reducing the individual parts of the proof configuration.
1.79
1.80 - Nevertheless, the strong'' mode of plain assumptions is quite
1.81 - important in practice to achieve robustness of proof text
1.82 - interpretation.  By forcing both the conclusion \emph{and} the
1.83 - assumptions to unify with the pending goal to be solved, goal
1.84 - selection becomes quite deterministic.  For example, decomposition
1.85 - with rules of the case-analysis'' type usually gives rise to
1.86 - several goals that only differ in there local contexts.  With strong
1.87 - assumptions these may be still solved in any order in a predictable
1.88 - way, while weak ones would quickly lead to great confusion,
1.89 - eventually demanding even some backtracking.
1.90 -*}
1.91 +  Nevertheless, the strong'' mode of plain assumptions is quite
1.92 +  important in practice to achieve robustness of proof text
1.93 +  interpretation.  By forcing both the conclusion \emph{and} the
1.94 +  assumptions to unify with the pending goal to be solved, goal
1.95 +  selection becomes quite deterministic.  For example, decomposition
1.96 +  with rules of the case-analysis'' type usually gives rise to
1.97 +  several goals that only differ in there local contexts.  With strong
1.98 +  assumptions these may be still solved in any order in a predictable
1.99 +  way, while weak ones would quickly lead to great confusion,
1.100 +  eventually demanding even some backtracking. *}
1.101
1.102  end