author wenzelm
Tue Oct 07 20:59:46 2014 +0200 (2014-10-07)
changeset 58614 7338eb25226c
parent 55640 abc140f21caa
child 58882 6e2010ab8bd9
permissions -rw-r--r--
more cartouches;
more antiquotations;
     1 (*  Title:      HOL/Isar_Examples/Peirce.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     5 header \<open>Peirce's Law\<close>
     7 theory Peirce
     8 imports Main
     9 begin
    11 text \<open>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.
    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.}\<close>
    22 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
    23 proof
    24   assume "(A \<longrightarrow> B) \<longrightarrow> A"
    25   show A
    26   proof (rule classical)
    27     assume "\<not> A"
    28     have "A \<longrightarrow> B"
    29     proof
    30       assume A
    31       with \<open>\<not> A\<close> show B by contradiction
    32     qed
    33     with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
    34   qed
    35 qed
    37 text \<open>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}.
    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.\<close>
    51 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
    52 proof
    53   assume "(A \<longrightarrow> B) \<longrightarrow> A"
    54   show A
    55   proof (rule classical)
    56     presume "A \<longrightarrow> B"
    57     with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
    58   next
    59     assume "\<not> A"
    60     show "A \<longrightarrow> B"
    61     proof
    62       assume A
    63       with \<open>\<not> A\<close> show B by contradiction
    64     qed
    65   qed
    66 qed
    68 text \<open>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.
    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.\<close>
    85 end