src/HOL/Isar_Examples/Peirce.thy
 author wenzelm Thu Jul 01 18:31:46 2010 +0200 (2010-07-01) changeset 37671 fa53d267dab3 parent 33026 8f35633c4922 child 55640 abc140f21caa permissions -rw-r--r--
misc tuning and modernization;
     1 (*  Title:      HOL/Isar_Examples/Peirce.thy

     2     Author:     Markus Wenzel, TU Muenchen

     3 *)

     4

     5 header {* Peirce's Law *}

     6

     7 theory Peirce

     8 imports Main

     9 begin

    10

    11 text {* We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.

    12   This is an inherently non-intuitionistic statement, so its proof

    13   will 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

    19   there is negation elimination; it holds in intuitionistic logic as

    20   well.} *}

    21

    22 theorem "((A --> B) --> A) --> A"

    23 proof

    24   assume "(A --> B) --> A"

    25   show A

    26   proof (rule classical)

    27     assume "~ A"

    28     have "A --> B"

    29     proof

    30       assume A

    31       with ~ A show B by contradiction

    32     qed

    33     with (A --> B) --> A show A ..

    34   qed

    35 qed

    36

    37 text {* In the subsequent version the reasoning is rearranged by means

    38   of weak assumptions'' (as introduced by \isacommand{presume}).

    39   Before assuming the negated goal $\neg A$, its intended consequence

    40   $A \impl B$ is put into place in order to solve the main problem.

    41   Nevertheless, we do not get anything for free, but have to establish

    42   $A \impl B$ later on.  The overall effect is that of a logical

    43   \emph{cut}.

    44

    45   Technically speaking, whenever some goal is solved by

    46   \isacommand{show} in the context of weak assumptions then the latter

    47   give rise to new subgoals, which may be established separately.  In

    48   contrast, strong assumptions (as introduced by \isacommand{assume})

    49   are solved immediately. *}

    50

    51 theorem "((A --> B) --> A) --> A"

    52 proof

    53   assume "(A --> B) --> A"

    54   show A

    55   proof (rule classical)

    56     presume "A --> B"

    57     with (A --> B) --> A show A ..

    58   next

    59     assume "~ A"

    60     show "A --> B"

    61     proof

    62       assume A

    63       with ~ A show B by contradiction

    64     qed

    65   qed

    66 qed

    67

    68 text {* Note that the goals stemming from weak assumptions may be even

    69   left until qed time, where they get eventually solved by

    70   assumption'' as well.  In that case there is really no fundamental

    71   difference between the two kinds of assumptions, apart from the

    72   order of reducing the individual parts of the proof configuration.

    73

    74   Nevertheless, the strong'' mode of plain assumptions is quite

    75   important in practice to achieve robustness of proof text

    76   interpretation.  By forcing both the conclusion \emph{and} the

    77   assumptions to unify with the pending goal to be solved, goal

    78   selection becomes quite deterministic.  For example, decomposition

    79   with rules of the case-analysis'' type usually gives rise to

    80   several goals that only differ in there local contexts.  With strong

    81   assumptions these may be still solved in any order in a predictable

    82   way, while weak ones would quickly lead to great confusion,

    83   eventually demanding even some backtracking. *}

    84

    85 end