author  paulson 
Fri, 28 Feb 1997 15:44:32 +0100  
changeset 2687  b7c86d3c9d0a 
parent 2601  b301958c465d 
child 3835  9a5a4e123859 
permissions  rwrr 
1459  1 
(* Title: FOL/ex/int 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 

6 
Intuitionistic FirstOrder Logic 

7 

8 
Singlestep commands: 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

9 
by (IntPr.step_tac 1); 
0  10 
by (biresolve_tac safe_brls 1); 
11 
by (biresolve_tac haz_brls 1); 

12 
by (assume_tac 1); 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

13 
by (IntPr.safe_tac 1); 
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

14 
by (IntPr.mp_tac 1); 
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

15 
by (IntPr.fast_tac 1); 
0  16 
*) 
17 

18 
writeln"File FOL/ex/int."; 

19 

1006  20 
(*Metatheorem (for PROPOSITIONAL formulae...): 
21 
P is classically provable iff ~~P is intuitionistically provable. 

22 
Therefore ~P is classically provable iff it is intuitionistically provable. 

0  23 

1006  24 
Proof: Let Q be the conjuction of the propositions A~A, one for each atom A 
25 
in P. Now ~~Q is intuitionistically provable because ~~(A~A) is and because 

26 
~~ distributes over &. If P is provable classically, then clearly Q>P is 

27 
provable intuitionistically, so ~~(Q>P) is also provable intuitionistically. 

28 
The latter is intuitionistically equivalent to ~~Q>~~P, hence to ~~P, since 

29 
~~Q is intuitionistically provable. Finally, if P is a negation then ~~P is 

30 
intuitionstically equivalent to P. [Andy Pitts] *) 

0  31 

32 
goal IFOL.thy "~~(P&Q) <> ~~P & ~~Q"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

33 
by (IntPr.fast_tac 1); 
0  34 
result(); 
35 

1006  36 
(* ~~ does NOT distribute over  *) 
37 

38 
goal IFOL.thy "~~(P>Q) <> (~~P > ~~Q)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

39 
by (IntPr.fast_tac 1); 
1006  40 
result(); 
41 

0  42 
goal IFOL.thy "~~~P <> ~P"; 
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

43 
by (IntPr.fast_tac 1); 
0  44 
result(); 
45 

46 
goal IFOL.thy "~~((P > Q  R) > (P>Q)  (P>R))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

47 
by (IntPr.fast_tac 1); 
0  48 
result(); 
49 

50 
goal IFOL.thy "(P<>Q) <> (Q<>P)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

51 
by (IntPr.fast_tac 1); 
0  52 
result(); 
53 

54 

55 
writeln"Lemmas for the propositional doublenegation translation"; 

56 

57 
goal IFOL.thy "P > ~~P"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

58 
by (IntPr.fast_tac 1); 
0  59 
result(); 
60 

61 
goal IFOL.thy "~~(~~P > P)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

62 
by (IntPr.fast_tac 1); 
0  63 
result(); 
64 

65 
goal IFOL.thy "~~P & ~~(P > Q) > ~~Q"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

66 
by (IntPr.fast_tac 1); 
0  67 
result(); 
68 

69 

70 
writeln"The following are classically but not constructively valid."; 

71 

72 
(*The attempt to prove them terminates quickly!*) 

73 
goal IFOL.thy "((P>Q) > P) > P"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

74 
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; 
0  75 
(*Check that subgoals remain: proof failed.*) 
76 
getgoal 1; 

77 

78 
goal IFOL.thy "(P&Q>R) > (P>R)  (Q>R)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

79 
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; 
0  80 
getgoal 1; 
81 

82 

2687  83 
writeln"de Bruijn formulae"; 
84 

85 
(*de Bruijn formula with three predicates*) 

86 
goal IFOL.thy "((P<>Q) > P&Q&R) & \ 

87 
\ ((Q<>R) > P&Q&R) & \ 

88 
\ ((R<>P) > P&Q&R) > P&Q&R"; 

89 
by (IntPr.fast_tac 1); 

90 
result(); 

91 

92 

93 
(*de Bruijn formula with five predicates*) 

94 
goal IFOL.thy "((P<>Q) > P&Q&R&S&T) & \ 

95 
\ ((Q<>R) > P&Q&R&S&T) & \ 

96 
\ ((R<>S) > P&Q&R&S&T) & \ 

97 
\ ((S<>T) > P&Q&R&S&T) & \ 

98 
\ ((T<>P) > P&Q&R&S&T) > P&Q&R&S&T"; 

99 
by (IntPr.fast_tac 1); 

100 
result(); 

101 

102 

0  103 
writeln"Intuitionistic FOL: propositional problems based on Pelletier."; 
104 

105 
writeln"Problem ~~1"; 

106 
goal IFOL.thy "~~((P>Q) <> (~Q > ~P))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

107 
by (IntPr.fast_tac 1); 
0  108 
result(); 
109 
(*5 secs*) 

110 

111 

112 
writeln"Problem ~~2"; 

113 
goal IFOL.thy "~~(~~P <> P)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

114 
by (IntPr.fast_tac 1); 
0  115 
result(); 
116 
(*1 secs*) 

117 

118 

119 
writeln"Problem 3"; 

120 
goal IFOL.thy "~(P>Q) > (Q>P)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

121 
by (IntPr.fast_tac 1); 
0  122 
result(); 
123 

124 
writeln"Problem ~~4"; 

125 
goal IFOL.thy "~~((~P>Q) <> (~Q > P))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

126 
by (IntPr.fast_tac 1); 
0  127 
result(); 
128 
(*9 secs*) 

129 

130 
writeln"Problem ~~5"; 

131 
goal IFOL.thy "~~((PQ>PR) > P(Q>R))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

132 
by (IntPr.fast_tac 1); 
0  133 
result(); 
134 
(*10 secs*) 

135 

136 

137 
writeln"Problem ~~6"; 

138 
goal IFOL.thy "~~(P  ~P)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

139 
by (IntPr.fast_tac 1); 
0  140 
result(); 
141 

142 
writeln"Problem ~~7"; 

143 
goal IFOL.thy "~~(P  ~~~P)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

144 
by (IntPr.fast_tac 1); 
0  145 
result(); 
146 

147 
writeln"Problem ~~8. Peirce's law"; 

148 
goal IFOL.thy "~~(((P>Q) > P) > P)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

149 
by (IntPr.fast_tac 1); 
0  150 
result(); 
151 

152 
writeln"Problem 9"; 

153 
goal IFOL.thy "((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

154 
by (IntPr.fast_tac 1); 
0  155 
result(); 
156 
(*9 secs*) 

157 

158 

159 
writeln"Problem 10"; 

160 
goal IFOL.thy "(Q>R) > (R>P&Q) > (P>(QR)) > (P<>Q)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

161 
by (IntPr.fast_tac 1); 
0  162 
result(); 
163 

164 
writeln"11. Proved in each direction (incorrectly, says Pelletier!!) "; 

165 
goal IFOL.thy "P<>P"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

166 
by (IntPr.fast_tac 1); 
0  167 

168 
writeln"Problem ~~12. Dijkstra's law "; 

169 
goal IFOL.thy "~~(((P <> Q) <> R) <> (P <> (Q <> R)))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

170 
by (IntPr.fast_tac 1); 
0  171 
result(); 
172 

173 
goal IFOL.thy "((P <> Q) <> R) > ~~(P <> (Q <> R))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

174 
by (IntPr.fast_tac 1); 
0  175 
result(); 
176 

177 
writeln"Problem 13. Distributive law"; 

178 
goal IFOL.thy "P  (Q & R) <> (P  Q) & (P  R)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

179 
by (IntPr.fast_tac 1); 
0  180 
result(); 
181 

182 
writeln"Problem ~~14"; 

183 
goal IFOL.thy "~~((P <> Q) <> ((Q  ~P) & (~QP)))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

184 
by (IntPr.fast_tac 1); 
0  185 
result(); 
186 

187 
writeln"Problem ~~15"; 

188 
goal IFOL.thy "~~((P > Q) <> (~P  Q))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

189 
by (IntPr.fast_tac 1); 
0  190 
result(); 
191 

192 
writeln"Problem ~~16"; 

193 
goal IFOL.thy "~~((P>Q)  (Q>P))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

194 
by (IntPr.fast_tac 1); 
0  195 
result(); 
196 

197 
writeln"Problem ~~17"; 

198 
goal IFOL.thy 

199 
"~~(((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S)))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

200 
by (IntPr.fast_tac 1); 
0  201 
result(); 
202 

203 
(*Dijkstra's "Golden Rule"*) 

204 
goal IFOL.thy "(P&Q) <> P <> Q <> (PQ)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

205 
by (IntPr.fast_tac 1); 
0  206 
result(); 
207 

208 

232  209 
writeln"****Examples with quantifiers****"; 
0  210 

211 

212 
writeln"The converse is classical in the following implications..."; 

213 

214 
goal IFOL.thy "(EX x.P(x)>Q) > (ALL x.P(x)) > Q"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

215 
by (IntPr.fast_tac 1); 
0  216 
result(); 
217 

218 
goal IFOL.thy "((ALL x.P(x))>Q) > ~ (ALL x. P(x) & ~Q)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

219 
by (IntPr.fast_tac 1); 
0  220 
result(); 
221 

222 
goal IFOL.thy "((ALL x. ~P(x))>Q) > ~ (ALL x. ~ (P(x)Q))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

223 
by (IntPr.fast_tac 1); 
0  224 
result(); 
225 

226 
goal IFOL.thy "(ALL x.P(x))  Q > (ALL x. P(x)  Q)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

227 
by (IntPr.fast_tac 1); 
0  228 
result(); 
229 

230 
goal IFOL.thy "(EX x. P > Q(x)) > (P > (EX x. Q(x)))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

231 
by (IntPr.fast_tac 1); 
0  232 
result(); 
233 

234 

235 

236 

237 
writeln"The following are not constructively valid!"; 

238 
(*The attempt to prove them terminates quickly!*) 

239 

240 
goal IFOL.thy "((ALL x.P(x))>Q) > (EX x.P(x)>Q)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

241 
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; 
0  242 
getgoal 1; 
243 

244 
goal IFOL.thy "(P > (EX x.Q(x))) > (EX x. P>Q(x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

245 
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; 
0  246 
getgoal 1; 
247 

248 
goal IFOL.thy "(ALL x. P(x)  Q) > ((ALL x.P(x))  Q)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

249 
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; 
0  250 
getgoal 1; 
251 

252 
goal IFOL.thy "(ALL x. ~~P(x)) > ~~(ALL x. P(x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

253 
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; 
0  254 
getgoal 1; 
255 

256 
(*Classically but not intuitionistically valid. Proved by a bug in 1986!*) 

257 
goal IFOL.thy "EX x. Q(x) > (ALL x. Q(x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

258 
by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected"; 
0  259 
getgoal 1; 
260 

261 

262 
writeln"Hard examples with quantifiers"; 

263 

264 
(*The ones that have not been proved are not known to be valid! 

265 
Some will require quantifier duplication  not currently available*) 

266 

267 
writeln"Problem ~~18"; 

268 
goal IFOL.thy "~~(EX y. ALL x. P(y)>P(x))"; 

269 
(*NOT PROVED*) 

270 

271 
writeln"Problem ~~19"; 

272 
goal IFOL.thy "~~(EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x)))"; 

273 
(*NOT PROVED*) 

274 

275 
writeln"Problem 20"; 

276 
goal IFOL.thy "(ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w))) \ 

277 
\ > (EX x y. P(x) & Q(y)) > (EX z. R(z))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

278 
by (IntPr.fast_tac 1); 
0  279 
result(); 
280 

281 
writeln"Problem 21"; 

282 
goal IFOL.thy "(EX x. P>Q(x)) & (EX x. Q(x)>P) > ~~(EX x. P<>Q(x))"; 

2573
f3e04805895a
Correction to Problem 24 (with unsatisfactory proof)
paulson
parents:
1459
diff
changeset

283 
(*NOT PROVED; needs quantifier duplication*) 
0  284 

285 
writeln"Problem 22"; 

286 
goal IFOL.thy "(ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

287 
by (IntPr.fast_tac 1); 
0  288 
result(); 
289 

290 
writeln"Problem ~~23"; 

291 
goal IFOL.thy "~~ ((ALL x. P  Q(x)) <> (P  (ALL x. Q(x))))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

292 
by (IntPr.best_tac 1); 
0  293 
result(); 
294 

295 
writeln"Problem 24"; 

296 
goal IFOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) > Q(x)R(x)) & \ 

2573
f3e04805895a
Correction to Problem 24 (with unsatisfactory proof)
paulson
parents:
1459
diff
changeset

297 
\ (~(EX x.P(x)) > (EX x.Q(x))) & (ALL x. Q(x)R(x) > S(x)) \ 
f3e04805895a
Correction to Problem 24 (with unsatisfactory proof)
paulson
parents:
1459
diff
changeset

298 
\ > ~~(EX x. P(x)&R(x))"; 
f3e04805895a
Correction to Problem 24 (with unsatisfactory proof)
paulson
parents:
1459
diff
changeset

299 
(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*) 
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

300 
by IntPr.safe_tac; 
2573
f3e04805895a
Correction to Problem 24 (with unsatisfactory proof)
paulson
parents:
1459
diff
changeset

301 
by (etac impE 1); 
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

302 
by (IntPr.fast_tac 1); 
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

303 
by (IntPr.fast_tac 1); 
0  304 
result(); 
305 

306 
writeln"Problem 25"; 

307 
goal IFOL.thy "(EX x. P(x)) & \ 

308 
\ (ALL x. L(x) > ~ (M(x) & R(x))) & \ 

309 
\ (ALL x. P(x) > (M(x) & L(x))) & \ 

310 
\ ((ALL x. P(x)>Q(x))  (EX x. P(x)&R(x))) \ 

311 
\ > (EX x. Q(x)&P(x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

312 
by (IntPr.best_tac 1); 
0  313 
result(); 
314 

315 
writeln"Problem ~~26"; 

1459  316 
goal IFOL.thy "(~~(EX x. p(x)) <> ~~(EX x. q(x))) & \ 
317 
\ (ALL x. ALL y. p(x) & q(y) > (r(x) <> s(y))) \ 

0  318 
\ > ((ALL x. p(x)>r(x)) <> (ALL x. q(x)>s(x)))"; 
319 
(*NOT PROVED*) 

320 

321 
writeln"Problem 27"; 

322 
goal IFOL.thy "(EX x. P(x) & ~Q(x)) & \ 

323 
\ (ALL x. P(x) > R(x)) & \ 

324 
\ (ALL x. M(x) & L(x) > P(x)) & \ 

325 
\ ((EX x. R(x) & ~ Q(x)) > (ALL x. L(x) > ~ R(x))) \ 

326 
\ > (ALL x. M(x) > ~L(x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

327 
by (IntPr.fast_tac 1); (*21 secs*) 
0  328 
result(); 
329 

330 
writeln"Problem ~~28. AMENDED"; 

331 
goal IFOL.thy "(ALL x. P(x) > (ALL x. Q(x))) & \ 

332 
\ (~~(ALL x. Q(x)R(x)) > (EX x. Q(x)&S(x))) & \ 

333 
\ (~~(EX x.S(x)) > (ALL x. L(x) > M(x))) \ 

334 
\ > (ALL x. P(x) & L(x) > M(x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

335 
by (IntPr.fast_tac 1); (*48 secs*) 
0  336 
result(); 
337 

338 
writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; 

339 
goal IFOL.thy "(EX x. P(x)) & (EX y. Q(y)) \ 

340 
\ > ((ALL x. P(x)>R(x)) & (ALL y. Q(y)>S(y)) <> \ 

341 
\ (ALL x y. P(x) & Q(y) > R(x) & S(y)))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

342 
by (IntPr.fast_tac 1); 
0  343 
result(); 
344 

345 
writeln"Problem ~~30"; 

346 
goal IFOL.thy "(ALL x. (P(x)  Q(x)) > ~ R(x)) & \ 

347 
\ (ALL x. (Q(x) > ~ S(x)) > P(x) & R(x)) \ 

348 
\ > (ALL x. ~~S(x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

349 
by (IntPr.fast_tac 1); 
0  350 
result(); 
351 

352 
writeln"Problem 31"; 

353 
goal IFOL.thy "~(EX x.P(x) & (Q(x)  R(x))) & \ 

354 
\ (EX x. L(x) & P(x)) & \ 

355 
\ (ALL x. ~ R(x) > M(x)) \ 

356 
\ > (EX x. L(x) & M(x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

357 
by (IntPr.fast_tac 1); 
0  358 
result(); 
359 

360 
writeln"Problem 32"; 

361 
goal IFOL.thy "(ALL x. P(x) & (Q(x)R(x))>S(x)) & \ 

362 
\ (ALL x. S(x) & R(x) > L(x)) & \ 

363 
\ (ALL x. M(x) > R(x)) \ 

364 
\ > (ALL x. P(x) & M(x) > L(x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

365 
by (IntPr.best_tac 1); 
0  366 
result(); 
367 

368 
writeln"Problem ~~33"; 

369 
goal IFOL.thy "(ALL x. ~~(P(a) & (P(x)>P(b))>P(c))) <> \ 

370 
\ (ALL x. ~~((~P(a)  P(x)  P(c)) & (~P(a)  ~P(b)  P(c))))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

371 
by (IntPr.best_tac 1); 
0  372 
result(); 
373 

374 

375 
writeln"Problem 36"; 

376 
goal IFOL.thy 

377 
"(ALL x. EX y. J(x,y)) & \ 

378 
\ (ALL x. EX y. G(x,y)) & \ 

379 
\ (ALL x y. J(x,y)  G(x,y) > (ALL z. J(y,z)  G(y,z) > H(x,z))) \ 

380 
\ > (ALL x. EX y. H(x,y))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

381 
by (IntPr.fast_tac 1); (*35 secs*) 
0  382 
result(); 
383 

384 
writeln"Problem 37"; 

385 
goal IFOL.thy 

386 
"(ALL z. EX w. ALL x. EX y. \ 

387 
\ ~~(P(x,z)>P(y,w)) & P(y,z) & (P(y,w) > (EX u.Q(u,w)))) & \ 

388 
\ (ALL x z. ~P(x,z) > (EX y. Q(y,z))) & \ 

389 
\ (~~(EX x y. Q(x,y)) > (ALL x. R(x,x))) \ 

390 
\ > ~~(ALL x. EX y. R(x,y))"; 

391 
(*NOT PROVED*) 

392 

393 
writeln"Problem 39"; 

394 
goal IFOL.thy "~ (EX x. ALL y. F(y,x) <> ~F(y,y))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

395 
by (IntPr.fast_tac 1); 
0  396 
result(); 
397 

398 
writeln"Problem 40. AMENDED"; 

399 
goal IFOL.thy "(EX y. ALL x. F(x,y) <> F(x,x)) > \ 

400 
\ ~(ALL x. EX y. ALL z. F(z,y) <> ~ F(z,x))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

401 
by (IntPr.fast_tac 1); 
0  402 
result(); 
403 

404 
writeln"Problem 44"; 

1459  405 
goal IFOL.thy "(ALL x. f(x) > \ 
406 
\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ 

407 
\ (EX x. j(x) & (ALL y. g(y) > h(x,y))) \ 

0  408 
\ > (EX x. j(x) & ~f(x))"; 
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

409 
by (IntPr.fast_tac 1); 
0  410 
result(); 
411 

412 
writeln"Problem 48"; 

413 
goal IFOL.thy "(a=b  c=d) & (a=c  b=d) > a=d  b=c"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

414 
by (IntPr.fast_tac 1); 
0  415 
result(); 
416 

417 
writeln"Problem 51"; 

418 
goal IFOL.thy 

419 
"(EX z w. ALL x y. P(x,y) <> (x=z & y=w)) > \ 

420 
\ (EX z. ALL x. EX w. (ALL y. P(x,y) <> y=w) <> x=z)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

421 
by (IntPr.best_tac 1); (*34 seconds*) 
0  422 
result(); 
423 

424 
writeln"Problem 52"; 

425 
(*Almost the same as 51. *) 

426 
goal IFOL.thy 

427 
"(EX z w. ALL x y. P(x,y) <> (x=z & y=w)) > \ 

428 
\ (EX w. ALL y. EX z. (ALL x. P(x,y) <> x=z) <> y=w)"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

429 
by (IntPr.best_tac 1); (*34 seconds*) 
0  430 
result(); 
431 

432 
writeln"Problem 56"; 

433 
goal IFOL.thy 

434 
"(ALL x. (EX y. P(y) & x=f(y)) > P(x)) <> (ALL x. P(x) > P(f(x)))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

435 
by (IntPr.fast_tac 1); 
0  436 
result(); 
437 

438 
writeln"Problem 57"; 

439 
goal IFOL.thy 

440 
"P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \ 

441 
\ (ALL x y z. P(x,y) & P(y,z) > P(x,z)) > P(f(a,b), f(a,c))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

442 
by (IntPr.fast_tac 1); 
0  443 
result(); 
444 

445 
writeln"Problem 60"; 

446 
goal IFOL.thy 

447 
"ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))"; 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

448 
by (IntPr.fast_tac 1); 
0  449 
result(); 
450 

451 
writeln"Reached end of file."; 