src/HOL/Isar_examples/Peirce.thy
author wenzelm
Fri, 23 Apr 1999 11:50:17 +0200
changeset 6493 3489490c948d
parent 6444 2ebe9e630cab
child 6746 cf6ad8d22793
permissions -rw-r--r--
tuned;
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
6493
wenzelm
parents: 6444
diff changeset
     5
Peirce's law: examples of classical proof.
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     6
*)
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     7
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     8
theory Peirce = Main:;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     9
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    10
6493
wenzelm
parents: 6444
diff changeset
    11
theorem "((A --> B) --> A) --> A";
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    12
proof;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    13
  assume ABA: "(A --> B) --> A";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    14
  show A;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    15
  proof (rule classical);
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    16
    assume notA: "~ A";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    17
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    18
    have AB: "A --> B";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    19
    proof;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    20
      assume A: A;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    21
      from notA A; show B; ..;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    22
    qed;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    23
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    24
    from ABA AB; show A; ..;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    25
  qed;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    26
qed;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    27
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    28
6493
wenzelm
parents: 6444
diff changeset
    29
theorem "((A --> B) --> A) --> A";
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    30
proof;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    31
  assume ABA: "(A --> B) --> A";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    32
  show A;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    33
  proof (rule classical);
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    34
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    35
    assume AB: "A --> B";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    36
    from ABA AB; show A; ..;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    37
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    38
    next;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    39
    assume notA: "~ A";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    40
    show "A --> B";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    41
    proof;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    42
      assume A: A;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    43
      from notA A; show B; ..;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    44
    qed;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    45
  qed;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    46
qed;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    47
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    48
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    49
end;