1464

1 
(* Title: FOLP/ex/prop.ML

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"commutative laws of & and  ";

5061

11 
Goal "?p : P & Q > Q & P";

0

12 
by tac;


13 
result();


14 

5061

15 
Goal "?p : P  Q > Q  P";

0

16 
by tac;


17 
result();


18 


19 


20 
writeln"associative laws of & and  ";

5061

21 
Goal "?p : (P & Q) & R > P & (Q & R)";

0

22 
by tac;


23 
result();


24 

5061

25 
Goal "?p : (P  Q)  R > P  (Q  R)";

0

26 
by tac;


27 
result();


28 


29 


30 


31 
writeln"distributive laws of & and  ";

5061

32 
Goal "?p : (P & Q)  R > (P  R) & (Q  R)";

0

33 
by tac;


34 
result();


35 

5061

36 
Goal "?p : (P  R) & (Q  R) > (P & Q)  R";

0

37 
by tac;


38 
result();


39 

5061

40 
Goal "?p : (P  Q) & R > (P & R)  (Q & R)";

0

41 
by tac;


42 
result();


43 


44 

5061

45 
Goal "?p : (P & R)  (Q & R) > (P  Q) & R";

0

46 
by tac;


47 
result();


48 


49 


50 
writeln"Laws involving implication";


51 

5061

52 
Goal "?p : (P>R) & (Q>R) <> (PQ > R)";

0

53 
by tac;


54 
result();


55 


56 

5061

57 
Goal "?p : (P & Q > R) <> (P> (Q>R))";

0

58 
by tac;


59 
result();


60 


61 

5061

62 
Goal "?p : ((P>R)>R) > ((Q>R)>R) > (P&Q>R) > R";

0

63 
by tac;


64 
result();


65 

5061

66 
Goal "?p : ~(P>R) > ~(Q>R) > ~(P&Q>R)";

0

67 
by tac;


68 
result();


69 

5061

70 
Goal "?p : (P > Q & R) <> (P>Q) & (P>R)";

0

71 
by tac;


72 
result();


73 


74 


75 
writeln"Propositionsastypes";


76 


77 
(*The combinator K*)

5061

78 
Goal "?p : P > (Q > P)";

0

79 
by tac;


80 
result();


81 


82 
(*The combinator S*)

5061

83 
Goal "?p : (P>Q>R) > (P>Q) > (P>R)";

0

84 
by tac;


85 
result();


86 


87 


88 
(*Converse is classical*)

5061

89 
Goal "?p : (P>Q)  (P>R) > (P > Q  R)";

0

90 
by tac;


91 
result();


92 

5061

93 
Goal "?p : (P>Q) > (~Q > ~P)";

0

94 
by tac;


95 
result();


96 


97 


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


99 


100 
(* stabimp *)

5061

101 
Goal "?p : (((Q>R)>R)>Q) > (((P>Q)>R)>R)>P>Q";

0

102 
by tac;


103 
result();


104 


105 
(* stabtopeirce *)

5061

106 
Goal "?p : (((P > R) > R) > P) > (((Q > R) > R) > Q) \

1459

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

0

108 
by tac;


109 
result();


110 


111 
(* peirceimp1 *)

5061

112 
Goal "?p : (((Q > R) > Q) > Q) \

1459

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

0

114 
by tac;


115 
result();


116 


117 
(* peirceimp2 *)

5061

118 
Goal "?p : (((P > R) > P) > P) > ((P > Q > R) > P) > P";

0

119 
by tac;


120 
result();


121 


122 
(* mints *)

5061

123 
Goal "?p : ((((P > Q) > P) > P) > Q) > Q";

0

124 
by tac;


125 
result();


126 


127 
(* mintssolovev *)

5061

128 
Goal "?p : (P > (Q > R) > Q) > ((P > Q) > R) > R";

0

129 
by tac;


130 
result();


131 


132 
(* tatsuta *)

5061

133 
Goal "?p : (((P7 > P1) > P10) > P4 > P5) \

1459

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


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


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


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

0

138 
by tac;


139 
result();


140 


141 
(* tatsuta1 *)

5061

142 
Goal "?p : (((P8 > P2) > P9) > P3 > P10) \

0

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


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


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


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


147 
by tac;


148 
result();
