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