author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 63585 f4a308fdf664
permissions -rw-r--r--
     1 (*  Title:      HOL/Isar_Examples/Peirce.thy
     2     Author:     Makarius
     3 *)
     5 section \<open>Peirce's Law\<close>
     7 theory Peirce
     8   imports Main
     9 begin
    11 text \<open>
    12   We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. This is an inherently
    13   non-intuitionistic statement, so its proof will certainly involve some form
    14   of classical contradiction.
    16   The first proof is again a well-balanced combination of plain backward and
    17   forward reasoning. The actual classical step is where the negated goal may
    18   be introduced as additional assumption. This eventually leads to a
    19   contradiction.\<^footnote>\<open>The rule involved there is negation elimination; it holds in
    20   intuitionistic logic as well.\<close>\<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>
    38   In the subsequent version the reasoning is rearranged by means of ``weak
    39   assumptions'' (as introduced by \<^theory_text>\<open>presume\<close>). Before assuming the negated
    40   goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put into place in order to
    41   solve the main problem. Nevertheless, we do not get anything for free, but
    42   have to establish \<open>A \<longrightarrow> B\<close> later on. The overall effect is that of a logical
    43   \<^emph>\<open>cut\<close>.
    45   Technically speaking, whenever some goal is solved by \<^theory_text>\<open>show\<close> in the context
    46   of weak assumptions then the latter give rise to new subgoals, which may be
    47   established separately. In contrast, strong assumptions (as introduced by
    48   \<^theory_text>\<open>assume\<close>) are solved immediately.
    49 \<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>
    69   Note that the goals stemming from weak assumptions may be even left until
    70   qed time, where they get eventually solved ``by assumption'' as well. In
    71   that case there is really no fundamental difference between the two kinds of
    72   assumptions, apart from the order of reducing the individual parts of the
    73   proof configuration.
    75   Nevertheless, the ``strong'' mode of plain assumptions is quite important in
    76   practice to achieve robustness of proof text interpretation. By forcing both
    77   the conclusion \<^emph>\<open>and\<close> the assumptions to unify with the pending goal to be
    78   solved, goal selection becomes quite deterministic. For example,
    79   decomposition 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 way,
    82   while weak ones would quickly lead to great confusion, eventually demanding
    83   even some backtracking.
    84 \<close>
    86 end