1459

1 
(* Title: FOL/ex/prop

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1991 University of Cambridge


5 


6 
FirstOrder Logic: propositional examples (intuitionistic and classical)


7 
Needs declarations of the theory "thy" and the tactic "tac"


8 
*)


9 


10 
writeln"File FOL/ex/prop.";


11 


12 


13 
writeln"commutative laws of & and  ";


14 
goal thy "?p : P & Q > Q & P";


15 
by tac;


16 
result();


17 


18 
goal thy "?p : P  Q > Q  P";


19 
by tac;


20 
result();


21 


22 


23 
writeln"associative laws of & and  ";


24 
goal thy "?p : (P & Q) & R > P & (Q & R)";


25 
by tac;


26 
result();


27 


28 
goal thy "?p : (P  Q)  R > P  (Q  R)";


29 
by tac;


30 
result();


31 


32 


33 


34 
writeln"distributive laws of & and  ";


35 
goal thy "?p : (P & Q)  R > (P  R) & (Q  R)";


36 
by tac;


37 
result();


38 


39 
goal thy "?p : (P  R) & (Q  R) > (P & Q)  R";


40 
by tac;


41 
result();


42 


43 
goal thy "?p : (P  Q) & R > (P & R)  (Q & R)";


44 
by tac;


45 
result();


46 


47 


48 
goal thy "?p : (P & R)  (Q & R) > (P  Q) & R";


49 
by tac;


50 
result();


51 


52 


53 
writeln"Laws involving implication";


54 


55 
goal thy "?p : (P>R) & (Q>R) <> (PQ > R)";


56 
by tac;


57 
result();


58 


59 


60 
goal thy "?p : (P & Q > R) <> (P> (Q>R))";


61 
by tac;


62 
result();


63 


64 


65 
goal thy "?p : ((P>R)>R) > ((Q>R)>R) > (P&Q>R) > R";


66 
by tac;


67 
result();


68 


69 
goal thy "?p : ~(P>R) > ~(Q>R) > ~(P&Q>R)";


70 
by tac;


71 
result();


72 


73 
goal thy "?p : (P > Q & R) <> (P>Q) & (P>R)";


74 
by tac;


75 
result();


76 


77 


78 
writeln"Propositionsastypes";


79 


80 
(*The combinator K*)


81 
goal thy "?p : P > (Q > P)";


82 
by tac;


83 
result();


84 


85 
(*The combinator S*)


86 
goal thy "?p : (P>Q>R) > (P>Q) > (P>R)";


87 
by tac;


88 
result();


89 


90 


91 
(*Converse is classical*)


92 
goal thy "?p : (P>Q)  (P>R) > (P > Q  R)";


93 
by tac;


94 
result();


95 


96 
goal thy "?p : (P>Q) > (~Q > ~P)";


97 
by tac;


98 
result();


99 


100 


101 
writeln"Schwichtenberg's examples (via T. Nipkow)";


102 


103 
(* stabimp *)


104 
goal thy "?p : (((Q>R)>R)>Q) > (((P>Q)>R)>R)>P>Q";


105 
by tac;


106 
result();


107 


108 
(* stabtopeirce *)


109 
goal thy "?p : (((P > R) > R) > P) > (((Q > R) > R) > Q) \

1459

110 
\ > ((P > Q) > P) > P";

0

111 
by tac;


112 
result();


113 


114 
(* peirceimp1 *)


115 
goal thy "?p : (((Q > R) > Q) > Q) \

1459

116 
\ > (((P > Q) > R) > P > Q) > P > Q";

0

117 
by tac;


118 
result();


119 


120 
(* peirceimp2 *)


121 
goal thy "?p : (((P > R) > P) > P) > ((P > Q > R) > P) > P";


122 
by tac;


123 
result();


124 


125 
(* mints *)


126 
goal thy "?p : ((((P > Q) > P) > P) > Q) > Q";


127 
by tac;


128 
result();


129 


130 
(* mintssolovev *)


131 
goal thy "?p : (P > (Q > R) > Q) > ((P > Q) > R) > R";


132 
by tac;


133 
result();


134 


135 
(* tatsuta *)


136 
goal thy "?p : (((P7 > P1) > P10) > P4 > P5) \

1459

137 
\ > (((P8 > P2) > P9) > P3 > P10) \


138 
\ > (P1 > P8) > P6 > P7 \


139 
\ > (((P3 > P2) > P9) > P4) \


140 
\ > (P1 > P3) > (((P6 > P1) > P2) > P9) > P5";

0

141 
by tac;


142 
result();


143 


144 
(* tatsuta1 *)


145 
goal thy "?p : (((P8 > P2) > P9) > P3 > P10) \


146 
\ > (((P3 > P2) > P9) > P4) \


147 
\ > (((P6 > P1) > P2) > P9) \


148 
\ > (((P7 > P1) > P10) > P4 > P5) \


149 
\ > (P1 > P3) > (P1 > P8) > P6 > P7 > P5";


150 
by tac;


151 
result();


152 


153 
writeln"Reached end of file.";
