src/HOL/Isar_examples/Peirce.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 23373 ead82c82da9e
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/Isar_examples/Peirce.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {* Peirce's Law *}
     7 
     8 theory Peirce imports Main begin
     9 
    10 text {*
    11  We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.  This is
    12  an inherently non-intuitionistic statement, so its proof will
    13  certainly involve some form of classical contradiction.
    14 
    15  The first proof is again a well-balanced combination of plain
    16  backward and forward reasoning.  The actual classical step is where
    17  the negated goal may be introduced as additional assumption.  This
    18  eventually leads to a contradiction.\footnote{The rule involved there
    19  is negation elimination; it holds in intuitionistic logic as well.}
    20 *}
    21 
    22 theorem "((A --> B) --> A) --> A"
    23 proof
    24   assume aba: "(A --> B) --> A"
    25   show A
    26   proof (rule classical)
    27     assume "~ A"
    28     have "A --> B"
    29     proof
    30       assume A
    31       thus B by contradiction
    32     qed
    33     with aba show A ..
    34   qed
    35 qed
    36 
    37 text {*
    38  In the subsequent version the reasoning is rearranged by means of
    39  ``weak assumptions'' (as introduced by \isacommand{presume}).  Before
    40  assuming the negated goal $\neg A$, its intended consequence $A \impl
    41  B$ is put into place in order to solve the main problem.
    42  Nevertheless, we do not get anything for free, but have to establish
    43  $A \impl B$ later on.  The overall effect is that of a logical
    44  \emph{cut}.
    45 
    46  Technically speaking, whenever some goal is solved by
    47  \isacommand{show} in the context of weak assumptions then the latter
    48  give rise to new subgoals, which may be established separately.  In
    49  contrast, strong assumptions (as introduced by \isacommand{assume})
    50  are solved immediately.
    51 *}
    52 
    53 theorem "((A --> B) --> A) --> A"
    54 proof
    55   assume aba: "(A --> B) --> A"
    56   show A
    57   proof (rule classical)
    58     presume "A --> B"
    59     with aba show A ..
    60   next
    61     assume "~ A"
    62     show "A --> B"
    63     proof
    64       assume A
    65       thus B by contradiction
    66     qed
    67   qed
    68 qed
    69 
    70 text {*
    71  Note that the goals stemming from weak assumptions may be even left
    72  until qed time, where they get eventually solved ``by assumption'' as
    73  well.  In that case there is really no fundamental difference between
    74  the two kinds of assumptions, apart from the order of reducing the
    75  individual parts of the proof configuration.
    76 
    77  Nevertheless, the ``strong'' mode of plain assumptions is quite
    78  important in practice to achieve robustness of proof text
    79  interpretation.  By forcing both the conclusion \emph{and} the
    80  assumptions to unify with the pending goal to be solved, goal
    81  selection becomes quite deterministic.  For example, decomposition
    82  with rules of the ``case-analysis'' type usually gives rise to
    83  several goals that only differ in there local contexts.  With strong
    84  assumptions these may be still solved in any order in a predictable
    85  way, while weak ones would quickly lead to great confusion,
    86  eventually demanding even some backtracking.
    87 *}
    88 
    89 end