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.18 - eventually leads to a contradiction.\footnote{The rule involved there
    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.24 +  eventually leads to a contradiction.\footnote{The rule involved
    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