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