src/HOL/Isar_examples/Peirce.thy
author wenzelm
Thu Oct 14 16:02:39 1999 +0200 (1999-10-14)
changeset 7869 c007f801cd59
parent 7860 7819547df4d8
child 7874 180364256231
permissions -rw-r--r--
improved presentation;
wenzelm@6444
     1
(*  Title:      HOL/Isar_examples/Peirce.thy
wenzelm@6444
     2
    ID:         $Id$
wenzelm@6444
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6444
     4
*)
wenzelm@6444
     5
wenzelm@7860
     6
header {* Peirce's Law *};
wenzelm@6444
     7
wenzelm@7748
     8
theory Peirce = Main:;
wenzelm@6444
     9
wenzelm@7860
    10
text {*
wenzelm@7860
    11
 We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.  This is
wenzelm@7860
    12
 an inherently non-intuitionistic statement, so its proof will
wenzelm@7860
    13
 certainly involve some form of classical contradiction.
wenzelm@7860
    14
wenzelm@7860
    15
 The first proof is again a well-balanced combination of plain
wenzelm@7860
    16
 backward and forward reasoning.  The actual classical reasoning step
wenzelm@7860
    17
 is where the negated goal is introduced as additional assumption.
wenzelm@7860
    18
 This eventually leads to a contradiction.\footnote{The rule involved
wenzelm@7860
    19
 here is negation elimination; it holds in intuitionistic logic as
wenzelm@7860
    20
 well.}
wenzelm@7860
    21
*};
wenzelm@7860
    22
wenzelm@6493
    23
theorem "((A --> B) --> A) --> A";
wenzelm@6444
    24
proof;
wenzelm@6892
    25
  assume aba: "(A --> B) --> A";
wenzelm@6444
    26
  show A;
wenzelm@6444
    27
  proof (rule classical);
wenzelm@7448
    28
    assume "~ A";
wenzelm@7448
    29
    have "A --> B";
wenzelm@6444
    30
    proof;
wenzelm@7448
    31
      assume A;
wenzelm@7448
    32
      thus B; by contradiction;
wenzelm@6444
    33
    qed;
wenzelm@7448
    34
    with aba; show A; ..;
wenzelm@6444
    35
  qed;
wenzelm@6444
    36
qed;
wenzelm@6444
    37
wenzelm@7860
    38
text {*
wenzelm@7860
    39
 The subsequent version rearranges the reasoning by means of ``weak
wenzelm@7860
    40
 assumptions'' (as introduced by \isacommand{presume}).  Before
wenzelm@7860
    41
 assuming the negated goal $\neg A$, its intended consequence $A \impl
wenzelm@7860
    42
 B$ is put into place in order to solve the main problem.
wenzelm@7860
    43
 Nevertheless, we do not get anything for free, but have to establish
wenzelm@7860
    44
 $A \impl B$ later on.  The overall effect is that of a \emph{cut}.
wenzelm@7860
    45
wenzelm@7860
    46
 Technically speaking, whenever some goal is solved by
wenzelm@7860
    47
 \isacommand{show} in the context of weak assumptions then the latter
wenzelm@7860
    48
 give rise to new subgoals, which may be established separately.  In
wenzelm@7860
    49
 contrast, strong assumptions (as introduced by \isacommand{assume})
wenzelm@7860
    50
 are solved immediately.
wenzelm@7860
    51
*};
wenzelm@7860
    52
wenzelm@6493
    53
theorem "((A --> B) --> A) --> A";
wenzelm@6444
    54
proof;
wenzelm@6892
    55
  assume aba: "(A --> B) --> A";
wenzelm@6444
    56
  show A;
wenzelm@6444
    57
  proof (rule classical);
wenzelm@7448
    58
    presume "A --> B";
wenzelm@7448
    59
    with aba; show A; ..;
wenzelm@6854
    60
  next;
wenzelm@6892
    61
    assume not_a: "~ A";
wenzelm@6444
    62
    show "A --> B";
wenzelm@6444
    63
    proof;
wenzelm@7448
    64
      assume A;
wenzelm@7448
    65
      with not_a; show B; ..;
wenzelm@6444
    66
    qed;
wenzelm@6444
    67
  qed;
wenzelm@6444
    68
qed;
wenzelm@6444
    69
wenzelm@7860
    70
text {*
wenzelm@7860
    71
 Note that the goals stemming from weak assumptions may be even left
wenzelm@7860
    72
 until qed time, where they get eventually solved ``by assumption'' as
wenzelm@7860
    73
 well.  In that case there is really no big difference between the two
wenzelm@7860
    74
 kinds of assumptions, apart from the order of reducing the individual
wenzelm@7860
    75
 parts of the proof configuration.
wenzelm@7860
    76
wenzelm@7860
    77
 Nevertheless, the ``strong'' mode of plain assumptions is quite
wenzelm@7860
    78
 important in practice to achieve robustness of proof document
wenzelm@7860
    79
 interpretation.  By forcing both the conclusion \emph{and} the
wenzelm@7869
    80
 assumptions to unify with the pending goal to be solved, goal
wenzelm@7869
    81
 selection becomes quite deterministic.  For example, decomposition
wenzelm@7869
    82
 with ``case-analysis'' type rules usually give rise to several goals
wenzelm@7869
    83
 that only differ in there local contexts.  With strong assumptions
wenzelm@7869
    84
 these may be still solved in any order in a predictable way, while
wenzelm@7869
    85
 weak ones would quickly lead to great confusion, eventually demanding
wenzelm@7869
    86
 even some backtracking.
wenzelm@7860
    87
*};
wenzelm@7860
    88
wenzelm@6444
    89
end;