src/HOL/Isar_Examples/Peirce.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (23 months ago) changeset 66695 91500c024c7f parent 63585 f4a308fdf664 permissions -rw-r--r--
tuned;
```     1 (*  Title:      HOL/Isar_Examples/Peirce.thy
```
```     2     Author:     Makarius
```
```     3 *)
```
```     4
```
```     5 section \<open>Peirce's Law\<close>
```
```     6
```
```     7 theory Peirce
```
```     8   imports Main
```
```     9 begin
```
```    10
```
```    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.
```
```    15
```
```    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>
```
```    21
```
```    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
```
```    36
```
```    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>.
```
```    44
```
```    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>
```
```    50
```
```    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
```
```    67
```
```    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.
```
```    74
```
```    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>
```
```    85
```
```    86 end
```