author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 18678  dd0c569fa43d 
permissions  rwrr 
1464  1 
(* Title: FOLP/ex/int.ML 
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: 

2603
4988dda71c0b
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); 

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

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

14 
by (IntPr.mp_tac 1); 
4988dda71c0b
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 
(*Note: for PROPOSITIONAL formulae... 

19 
~A is classically provable iff it is intuitionistically provable. 

20 
Therefore A is classically provable iff ~~A is intuitionistically provable. 

21 

22 
Let Q be the conjuction of the propositions A~A, one for each atom A in 

23 
P. If P is provable classically, then clearly P&Q is provable 

24 
intuitionistically, so ~~(P&Q) is also provable intuitionistically. 

25 
The latter is intuitionistically equivalent to ~~P&~~Q, hence to ~~P, 

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

27 
~~P is intuitionstically equivalent to P. [Andy Pitts] 

28 
*) 

29 

17480  30 
goal (theory "IFOLP") "?p : ~~(P&Q) <> ~~P & ~~Q"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

31 
by (IntPr.fast_tac 1); 
0  32 
result(); 
33 

17480  34 
goal (theory "IFOLP") "?p : ~~~P <> ~P"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

35 
by (IntPr.fast_tac 1); 
0  36 
result(); 
37 

17480  38 
goal (theory "IFOLP") "?p : ~~((P > Q  R) > (P>Q)  (P>R))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

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

17480  42 
goal (theory "IFOLP") "?p : (P<>Q) <> (Q<>P)"; 
2603
4988dda71c0b
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 

47 
writeln"Lemmas for the propositional doublenegation translation"; 

48 

17480  49 
goal (theory "IFOLP") "?p : P > ~~P"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

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

17480  53 
goal (theory "IFOLP") "?p : ~~(~~P > P)"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

54 
by (IntPr.fast_tac 1); 
0  55 
result(); 
56 

17480  57 
goal (theory "IFOLP") "?p : ~~P & ~~(P > Q) > ~~Q"; 
2603
4988dda71c0b
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 

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

63 

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

17480  65 
goal (theory "IFOLP") "?p : ((P>Q) > P) > P"; 
18678  66 
by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; 
0  67 
(*Check that subgoals remain: proof failed.*) 
68 
getgoal 1; 

69 

17480  70 
goal (theory "IFOLP") "?p : (P&Q>R) > (P>R)  (Q>R)"; 
18678  71 
by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; 
0  72 
getgoal 1; 
73 

74 

75 
writeln"Intuitionistic FOL: propositional problems based on Pelletier."; 

76 

77 
writeln"Problem ~~1"; 

17480  78 
goal (theory "IFOLP") "?p : ~~((P>Q) <> (~Q > ~P))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

79 
by (IntPr.fast_tac 1); 
0  80 
result(); 
81 
(*5 secs*) 

82 

83 

84 
writeln"Problem ~~2"; 

17480  85 
goal (theory "IFOLP") "?p : ~~(~~P <> P)"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

86 
by (IntPr.fast_tac 1); 
0  87 
result(); 
88 
(*1 secs*) 

89 

90 

91 
writeln"Problem 3"; 

17480  92 
goal (theory "IFOLP") "?p : ~(P>Q) > (Q>P)"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

93 
by (IntPr.fast_tac 1); 
0  94 
result(); 
95 

96 
writeln"Problem ~~4"; 

17480  97 
goal (theory "IFOLP") "?p : ~~((~P>Q) <> (~Q > P))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

98 
by (IntPr.fast_tac 1); 
0  99 
result(); 
100 
(*9 secs*) 

101 

102 
writeln"Problem ~~5"; 

17480  103 
goal (theory "IFOLP") "?p : ~~((PQ>PR) > P(Q>R))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

104 
by (IntPr.fast_tac 1); 
0  105 
result(); 
106 
(*10 secs*) 

107 

108 

109 
writeln"Problem ~~6"; 

17480  110 
goal (theory "IFOLP") "?p : ~~(P  ~P)"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

111 
by (IntPr.fast_tac 1); 
0  112 
result(); 
113 

114 
writeln"Problem ~~7"; 

17480  115 
goal (theory "IFOLP") "?p : ~~(P  ~~~P)"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

116 
by (IntPr.fast_tac 1); 
0  117 
result(); 
118 

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

17480  120 
goal (theory "IFOLP") "?p : ~~(((P>Q) > P) > P)"; 
2603
4988dda71c0b
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 9"; 

17480  125 
goal (theory "IFOLP") "?p : ((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"; 
2603
4988dda71c0b
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 

131 
writeln"Problem 10"; 

17480  132 
goal (theory "IFOLP") "?p : (Q>R) > (R>P&Q) > (P>(QR)) > (P<>Q)"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

133 
by (IntPr.fast_tac 1); 
0  134 
result(); 
135 

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

17480  137 
goal (theory "IFOLP") "?p : P<>P"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

138 
by (IntPr.fast_tac 1); 
0  139 

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

17480  141 
goal (theory "IFOLP") "?p : ~~(((P <> Q) <> R) <> (P <> (Q <> R)))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

142 
by (IntPr.fast_tac 1); 
0  143 
result(); 
144 

17480  145 
goal (theory "IFOLP") "?p : ((P <> Q) <> R) > ~~(P <> (Q <> R))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

146 
by (IntPr.fast_tac 1); 
0  147 
result(); 
148 

149 
writeln"Problem 13. Distributive law"; 

17480  150 
goal (theory "IFOLP") "?p : P  (Q & R) <> (P  Q) & (P  R)"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

151 
by (IntPr.fast_tac 1); 
0  152 
result(); 
153 

154 
writeln"Problem ~~14"; 

17480  155 
goal (theory "IFOLP") "?p : ~~((P <> Q) <> ((Q  ~P) & (~QP)))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

156 
by (IntPr.fast_tac 1); 
0  157 
result(); 
158 

159 
writeln"Problem ~~15"; 

17480  160 
goal (theory "IFOLP") "?p : ~~((P > Q) <> (~P  Q))"; 
2603
4988dda71c0b
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"Problem ~~16"; 

17480  165 
goal (theory "IFOLP") "?p : ~~((P>Q)  (Q>P))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

166 
by (IntPr.fast_tac 1); 
0  167 
result(); 
168 

169 
writeln"Problem ~~17"; 

17480  170 
goal (theory "IFOLP") 
0  171 
"?p : ~~(((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S)))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

172 
by (IntPr.fast_tac 1); 
0  173 
(*over 5 minutes??  printing the proof term takes 40 secs!!*) 
174 
result(); 

175 

176 

177 
writeln"** Examples with quantifiers **"; 

178 

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

180 

17480  181 
goal (theory "IFOLP") "?p : (EX x. P(x)>Q) > (ALL x. P(x)) > Q"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

182 
by (IntPr.fast_tac 1); 
0  183 
result(); 
184 

17480  185 
goal (theory "IFOLP") "?p : ((ALL x. P(x))>Q) > ~ (ALL x. P(x) & ~Q)"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

186 
by (IntPr.fast_tac 1); 
0  187 
result(); 
188 

17480  189 
goal (theory "IFOLP") "?p : ((ALL x. ~P(x))>Q) > ~ (ALL x. ~ (P(x)Q))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

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

17480  193 
goal (theory "IFOLP") "?p : (ALL x. P(x))  Q > (ALL x. P(x)  Q)"; 
2603
4988dda71c0b
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 

17480  197 
goal (theory "IFOLP") "?p : (EX x. P > Q(x)) > (P > (EX x. Q(x)))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

198 
by (IntPr.fast_tac 1); 
0  199 
result(); 
200 

201 

202 

203 

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

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

206 

17480  207 
goal (theory "IFOLP") "?p : ((ALL x. P(x))>Q) > (EX x. P(x)>Q)"; 
18678  208 
by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; 
0  209 
getgoal 1; 
210 

17480  211 
goal (theory "IFOLP") "?p : (P > (EX x. Q(x))) > (EX x. P>Q(x))"; 
18678  212 
by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; 
0  213 
getgoal 1; 
214 

17480  215 
goal (theory "IFOLP") "?p : (ALL x. P(x)  Q) > ((ALL x. P(x))  Q)"; 
18678  216 
by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; 
0  217 
getgoal 1; 
218 

17480  219 
goal (theory "IFOLP") "?p : (ALL x. ~~P(x)) > ~~(ALL x. P(x))"; 
18678  220 
by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; 
0  221 
getgoal 1; 
222 

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

17480  224 
goal (theory "IFOLP") "?p : EX x. Q(x) > (ALL x. Q(x))"; 
18678  225 
by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected"; 
0  226 
getgoal 1; 
227 

228 

229 
writeln"Hard examples with quantifiers"; 

230 

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

15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset

232 
Some will require quantifier duplication  not currently available*) 
0  233 

234 
writeln"Problem ~~18"; 

17480  235 
goal (theory "IFOLP") "?p : ~~(EX y. ALL x. P(y)>P(x))"; 
0  236 
(*NOT PROVED*) 
237 

238 
writeln"Problem ~~19"; 

17480  239 
goal (theory "IFOLP") "?p : ~~(EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x)))"; 
0  240 
(*NOT PROVED*) 
241 

242 
writeln"Problem 20"; 

17480  243 
goal (theory "IFOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w))) \ 
0  244 
\ > (EX x y. P(x) & Q(y)) > (EX z. R(z))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

245 
by (IntPr.fast_tac 1); 
0  246 
result(); 
247 

248 
writeln"Problem 21"; 

17480  249 
goal (theory "IFOLP") 
0  250 
"?p : (EX x. P>Q(x)) & (EX x. Q(x)>P) > ~~(EX x. P<>Q(x))"; 
251 
(*NOT PROVED*) 

252 

253 
writeln"Problem 22"; 

17480  254 
goal (theory "IFOLP") "?p : (ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

255 
by (IntPr.fast_tac 1); 
0  256 
result(); 
257 

258 
writeln"Problem ~~23"; 

17480  259 
goal (theory "IFOLP") "?p : ~~ ((ALL x. P  Q(x)) <> (P  (ALL x. Q(x))))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

260 
by (IntPr.best_tac 1); 
0  261 
result(); 
262 

263 
writeln"Problem 24"; 

17480  264 
goal (theory "IFOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) > Q(x)R(x)) & \ 
3836  265 
\ (~(EX x. P(x)) > (EX x. Q(x))) & (ALL x. Q(x)R(x) > S(x)) \ 
2573
f3e04805895a
Correction to Problem 24 (with unsatisfactory proof)
paulson
parents:
1464
diff
changeset

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

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

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

269 
by (etac impE 1); 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

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

271 
by (IntPr.fast_tac 1); 
0  272 
result(); 
273 

274 
writeln"Problem 25"; 

17480  275 
goal (theory "IFOLP") "?p : (EX x. P(x)) & \ 
0  276 
\ (ALL x. L(x) > ~ (M(x) & R(x))) & \ 
277 
\ (ALL x. P(x) > (M(x) & L(x))) & \ 

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

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

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

280 
by (IntPr.best_tac 1); 
0  281 
result(); 
282 

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

17480  284 
goal (theory "IFOLP") "?p : (EX x. P(x)) & (EX y. Q(y)) \ 
0  285 
\ > ((ALL x. P(x)>R(x)) & (ALL y. Q(y)>S(y)) <> \ 
286 
\ (ALL x y. P(x) & Q(y) > R(x) & S(y)))"; 

2603
4988dda71c0b
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 ~~30"; 

17480  291 
goal (theory "IFOLP") "?p : (ALL x. (P(x)  Q(x)) > ~ R(x)) & \ 
0  292 
\ (ALL x. (Q(x) > ~ S(x)) > P(x) & R(x)) \ 
293 
\ > (ALL x. ~~S(x))"; 

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

294 
by (IntPr.fast_tac 1); 
0  295 
result(); 
296 

297 
writeln"Problem 31"; 

17480  298 
goal (theory "IFOLP") "?p : ~(EX x. P(x) & (Q(x)  R(x))) & \ 
0  299 
\ (EX x. L(x) & P(x)) & \ 
300 
\ (ALL x. ~ R(x) > M(x)) \ 

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

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

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

305 
writeln"Problem 32"; 

17480  306 
goal (theory "IFOLP") "?p : (ALL x. P(x) & (Q(x)R(x))>S(x)) & \ 
0  307 
\ (ALL x. S(x) & R(x) > L(x)) & \ 
308 
\ (ALL x. M(x) > R(x)) \ 

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

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

310 
by (IntPr.best_tac 1); (*SLOW*) 
0  311 
result(); 
312 

313 
writeln"Problem 39"; 

17480  314 
goal (theory "IFOLP") "?p : ~ (EX x. ALL y. F(y,x) <> ~F(y,y))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

315 
by (IntPr.fast_tac 1); 
0  316 
result(); 
317 

318 
writeln"Problem 40. AMENDED"; 

17480  319 
goal (theory "IFOLP") "?p : (EX y. ALL x. F(x,y) <> F(x,x)) > \ 
0  320 
\ ~(ALL x. EX y. ALL z. F(z,y) <> ~ F(z,x))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

321 
by (IntPr.fast_tac 1); 
0  322 
result(); 
323 

324 
writeln"Problem 44"; 

17480  325 
goal (theory "IFOLP") "?p : (ALL x. f(x) > \ 
1459  326 
\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ 
327 
\ (EX x. j(x) & (ALL y. g(y) > h(x,y))) \ 

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

329 
by (IntPr.fast_tac 1); 
0  330 
result(); 
331 

332 
writeln"Problem 48"; 

17480  333 
goal (theory "IFOLP") "?p : (a=b  c=d) & (a=c  b=d) > a=d  b=c"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

334 
by (IntPr.fast_tac 1); 
0  335 
result(); 
336 

337 
writeln"Problem 51"; 

17480  338 
goal (theory "IFOLP") 
0  339 
"?p : (EX z w. ALL x y. P(x,y) <> (x=z & y=w)) > \ 
340 
\ (EX z. ALL x. EX w. (ALL y. P(x,y) <> y=w) <> x=z)"; 

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

341 
by (IntPr.best_tac 1); (*60 seconds*) 
0  342 
result(); 
343 

344 
writeln"Problem 56"; 

17480  345 
goal (theory "IFOLP") 
0  346 
"?p : (ALL x. (EX y. P(y) & x=f(y)) > P(x)) <> (ALL x. P(x) > P(f(x)))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

347 
by (IntPr.fast_tac 1); 
0  348 
result(); 
349 

350 
writeln"Problem 57"; 

17480  351 
goal (theory "IFOLP") 
0  352 
"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \ 
353 
\ (ALL x y z. P(x,y) & P(y,z) > P(x,z)) > P(f(a,b), f(a,c))"; 

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

354 
by (IntPr.fast_tac 1); 
0  355 
result(); 
356 

357 
writeln"Problem 60"; 

17480  358 
goal (theory "IFOLP") 
0  359 
"?p : ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))"; 
2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2573
diff
changeset

360 
by (IntPr.fast_tac 1); 
0  361 
result(); 