src/HOL/Isar_examples/Peirce.thy
 author krauss Fri Nov 24 13:44:51 2006 +0100 (2006-11-24) changeset 21512 3786eb1b69d6 parent 16417 9bc16273c2d4 child 23373 ead82c82da9e permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     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