src/Sequents/LK/Propositional.thy
author wenzelm
Sat Feb 01 18:00:28 2014 +0100 (2014-02-01)
changeset 55229 08f2ebb65078
parent 41959 b460124855b8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
simplified sessions;
wenzelm@41959
     1
(*  Title:      Sequents/LK/Propositional.thy
wenzelm@21426
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@21426
     3
    Copyright   1992  University of Cambridge
wenzelm@21426
     4
*)
wenzelm@21426
     5
wenzelm@21426
     6
header {* Classical sequent calculus: examples with propositional connectives *}
wenzelm@21426
     7
wenzelm@21426
     8
theory Propositional
wenzelm@55229
     9
imports "../LK"
wenzelm@21426
    10
begin
wenzelm@21426
    11
wenzelm@21426
    12
text "absorptive laws of & and | "
wenzelm@21426
    13
wenzelm@21426
    14
lemma "|- P & P <-> P"
wenzelm@21426
    15
  by fast_prop
wenzelm@21426
    16
wenzelm@21426
    17
lemma "|- P | P <-> P"
wenzelm@21426
    18
  by fast_prop
wenzelm@21426
    19
wenzelm@21426
    20
wenzelm@21426
    21
text "commutative laws of & and | "
wenzelm@21426
    22
wenzelm@21426
    23
lemma "|- P & Q  <->  Q & P"
wenzelm@21426
    24
  by fast_prop
wenzelm@21426
    25
wenzelm@21426
    26
lemma "|- P | Q  <->  Q | P"
wenzelm@21426
    27
  by fast_prop
wenzelm@21426
    28
wenzelm@21426
    29
wenzelm@21426
    30
text "associative laws of & and | "
wenzelm@21426
    31
wenzelm@21426
    32
lemma "|- (P & Q) & R  <->  P & (Q & R)"
wenzelm@21426
    33
  by fast_prop
wenzelm@21426
    34
wenzelm@21426
    35
lemma "|- (P | Q) | R  <->  P | (Q | R)"
wenzelm@21426
    36
  by fast_prop
wenzelm@21426
    37
wenzelm@21426
    38
wenzelm@21426
    39
text "distributive laws of & and | "
wenzelm@21426
    40
wenzelm@21426
    41
lemma "|- (P & Q) | R  <-> (P | R) & (Q | R)"
wenzelm@21426
    42
  by fast_prop
wenzelm@21426
    43
wenzelm@21426
    44
lemma "|- (P | Q) & R  <-> (P & R) | (Q & R)"
wenzelm@21426
    45
  by fast_prop
wenzelm@21426
    46
wenzelm@21426
    47
wenzelm@21426
    48
text "Laws involving implication"
wenzelm@21426
    49
wenzelm@21426
    50
lemma "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"
wenzelm@21426
    51
  by fast_prop
wenzelm@21426
    52
wenzelm@21426
    53
lemma "|- (P & Q --> R) <-> (P--> (Q-->R))"
wenzelm@21426
    54
  by fast_prop
wenzelm@21426
    55
wenzelm@21426
    56
lemma "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
wenzelm@21426
    57
  by fast_prop
wenzelm@21426
    58
wenzelm@21426
    59
wenzelm@21426
    60
text "Classical theorems"
wenzelm@21426
    61
wenzelm@21426
    62
lemma "|- P|Q --> P| ~P&Q"
wenzelm@21426
    63
  by fast_prop
wenzelm@21426
    64
wenzelm@21426
    65
lemma "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)"
wenzelm@21426
    66
  by fast_prop
wenzelm@21426
    67
wenzelm@21426
    68
lemma "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)"
wenzelm@21426
    69
  by fast_prop
wenzelm@21426
    70
wenzelm@21426
    71
lemma "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)"
wenzelm@21426
    72
  by fast_prop
wenzelm@21426
    73
wenzelm@21426
    74
wenzelm@21426
    75
(*If and only if*)
wenzelm@21426
    76
wenzelm@21426
    77
lemma "|- (P<->Q) <-> (Q<->P)"
wenzelm@21426
    78
  by fast_prop
wenzelm@21426
    79
wenzelm@21426
    80
lemma "|- ~ (P <-> ~P)"
wenzelm@21426
    81
  by fast_prop
wenzelm@21426
    82
wenzelm@21426
    83
wenzelm@21426
    84
(*Sample problems from 
wenzelm@21426
    85
  F. J. Pelletier, 
wenzelm@21426
    86
  Seventy-Five Problems for Testing Automatic Theorem Provers,
wenzelm@21426
    87
  J. Automated Reasoning 2 (1986), 191-216.
wenzelm@21426
    88
  Errata, JAR 4 (1988), 236-236.
wenzelm@21426
    89
*)
wenzelm@21426
    90
wenzelm@21426
    91
(*1*)
wenzelm@21426
    92
lemma "|- (P-->Q)  <->  (~Q --> ~P)"
wenzelm@21426
    93
  by fast_prop
wenzelm@21426
    94
wenzelm@21426
    95
(*2*)
wenzelm@21426
    96
lemma "|- ~ ~ P  <->  P"
wenzelm@21426
    97
  by fast_prop
wenzelm@21426
    98
wenzelm@21426
    99
(*3*)
wenzelm@21426
   100
lemma "|- ~(P-->Q) --> (Q-->P)"
wenzelm@21426
   101
  by fast_prop
wenzelm@21426
   102
wenzelm@21426
   103
(*4*)
wenzelm@21426
   104
lemma "|- (~P-->Q)  <->  (~Q --> P)"
wenzelm@21426
   105
  by fast_prop
wenzelm@21426
   106
wenzelm@21426
   107
(*5*)
wenzelm@21426
   108
lemma "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))"
wenzelm@21426
   109
  by fast_prop
wenzelm@21426
   110
wenzelm@21426
   111
(*6*)
wenzelm@21426
   112
lemma "|- P | ~ P"
wenzelm@21426
   113
  by fast_prop
wenzelm@21426
   114
wenzelm@21426
   115
(*7*)
wenzelm@21426
   116
lemma "|- P | ~ ~ ~ P"
wenzelm@21426
   117
  by fast_prop
wenzelm@21426
   118
wenzelm@21426
   119
(*8.  Peirce's law*)
wenzelm@21426
   120
lemma "|- ((P-->Q) --> P)  -->  P"
wenzelm@21426
   121
  by fast_prop
wenzelm@21426
   122
wenzelm@21426
   123
(*9*)
wenzelm@21426
   124
lemma "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
wenzelm@21426
   125
  by fast_prop
wenzelm@21426
   126
wenzelm@21426
   127
(*10*)
wenzelm@21426
   128
lemma "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q"
wenzelm@21426
   129
  by fast_prop
wenzelm@21426
   130
wenzelm@21426
   131
(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
wenzelm@21426
   132
lemma "|- P<->P"
wenzelm@21426
   133
  by fast_prop
wenzelm@21426
   134
wenzelm@21426
   135
(*12.  "Dijkstra's law"*)
wenzelm@21426
   136
lemma "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
wenzelm@21426
   137
  by fast_prop
wenzelm@21426
   138
wenzelm@21426
   139
(*13.  Distributive law*)
wenzelm@21426
   140
lemma "|- P | (Q & R)  <-> (P | Q) & (P | R)"
wenzelm@21426
   141
  by fast_prop
wenzelm@21426
   142
wenzelm@21426
   143
(*14*)
wenzelm@21426
   144
lemma "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
wenzelm@21426
   145
  by fast_prop
wenzelm@21426
   146
wenzelm@21426
   147
(*15*)
wenzelm@21426
   148
lemma "|- (P --> Q) <-> (~P | Q)"
wenzelm@21426
   149
  by fast_prop
wenzelm@21426
   150
wenzelm@21426
   151
(*16*)
wenzelm@21426
   152
lemma "|- (P-->Q) | (Q-->P)"
wenzelm@21426
   153
  by fast_prop
wenzelm@21426
   154
wenzelm@21426
   155
(*17*)
wenzelm@21426
   156
lemma "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
wenzelm@21426
   157
  by fast_prop
wenzelm@21426
   158
wenzelm@21426
   159
end