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 

1464

10 
writeln"File FOLP/ex/prop.ML";

0

11 


12 


13 
writeln"commutative laws of & and  ";

5061

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

0

15 
by tac;


16 
result();


17 

5061

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

0

19 
by tac;


20 
result();


21 


22 


23 
writeln"associative laws of & and  ";

5061

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

0

25 
by tac;


26 
result();


27 

5061

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

0

29 
by tac;


30 
result();


31 


32 


33 


34 
writeln"distributive laws of & and  ";

5061

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

0

36 
by tac;


37 
result();


38 

5061

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

0

40 
by tac;


41 
result();


42 

5061

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

0

44 
by tac;


45 
result();


46 


47 

5061

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

0

49 
by tac;


50 
result();


51 


52 


53 
writeln"Laws involving implication";


54 

5061

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

0

56 
by tac;


57 
result();


58 


59 

5061

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

0

61 
by tac;


62 
result();


63 


64 

5061

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

0

66 
by tac;


67 
result();


68 

5061

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

0

70 
by tac;


71 
result();


72 

5061

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

0

74 
by tac;


75 
result();


76 


77 


78 
writeln"Propositionsastypes";


79 


80 
(*The combinator K*)

5061

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

0

82 
by tac;


83 
result();


84 


85 
(*The combinator S*)

5061

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

0

87 
by tac;


88 
result();


89 


90 


91 
(*Converse is classical*)

5061

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

0

93 
by tac;


94 
result();


95 

5061

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

0

97 
by tac;


98 
result();


99 


100 


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


102 


103 
(* stabimp *)

5061

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

0

105 
by tac;


106 
result();


107 


108 
(* stabtopeirce *)

5061

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

1459

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

0

111 
by tac;


112 
result();


113 


114 
(* peirceimp1 *)

5061

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

1459

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

0

117 
by tac;


118 
result();


119 


120 
(* peirceimp2 *)

5061

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

0

122 
by tac;


123 
result();


124 


125 
(* mints *)

5061

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

0

127 
by tac;


128 
result();


129 


130 
(* mintssolovev *)

5061

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

0

132 
by tac;


133 
result();


134 


135 
(* tatsuta *)

5061

136 
Goal "?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 *)

5061

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

0

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.";
