21426

1 
(* Title: 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 " (PQ > 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 " PQ > 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 
SeventyFive Problems for Testing Automatic Theorem Provers,


87 
J. Automated Reasoning 2 (1986), 191216.


88 
Errata, JAR 4 (1988), 236236.


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 " ((PQ)>(PR)) > (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 " ((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"


125 
by fast_prop


126 


127 
(*10*)


128 
lemma "Q>R, R>P&Q, P>(QR)  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) & (~QP))"


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
