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