author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 12  f17d542276b6 
permissions  rwrr 
0  1 
(* Title: FOL/ifol.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
Tactics and lemmas for ifol.thy (intuitionistic firstorder logic) 

7 
*) 

8 

9 
open IFOL; 

10 

11 
signature IFOL_LEMMAS = 

12 
sig 

13 
val allE: thm 

14 
val all_cong: thm 

15 
val all_dupE: thm 

16 
val all_impE: thm 

17 
val box_equals: thm 

18 
val conjE: thm 

19 
val conj_cong: thm 

20 
val conj_impE: thm 

21 
val contrapos: thm 

22 
val disj_cong: thm 

23 
val disj_impE: thm 

24 
val eq_cong: thm 

25 
val eq_mp_tac: int > tactic 

26 
val ex1I: thm 

12
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

27 
val ex_ex1I: thm 
0  28 
val ex1E: thm 
29 
val ex1_equalsE: thm 

30 
val ex1_cong: thm 

31 
val ex_cong: thm 

32 
val ex_impE: thm 

33 
val iffD1: thm 

34 
val iffD2: thm 

35 
val iffE: thm 

36 
val iffI: thm 

37 
val iff_cong: thm 

38 
val iff_impE: thm 

39 
val iff_refl: thm 

40 
val iff_sym: thm 

41 
val iff_trans: thm 

42 
val impE: thm 

43 
val imp_cong: thm 

44 
val imp_impE: thm 

45 
val mp_tac: int > tactic 

46 
val notE: thm 

47 
val notI: thm 

48 
val not_cong: thm 

49 
val not_impE: thm 

50 
val not_sym: thm 

51 
val not_to_imp: thm 

52 
val pred1_cong: thm 

53 
val pred2_cong: thm 

54 
val pred3_cong: thm 

55 
val pred_congs: thm list 

56 
val rev_mp: thm 

57 
val simp_equals: thm 

58 
val ssubst: thm 

59 
val subst_context: thm 

60 
val subst_context2: thm 

61 
val subst_context3: thm 

62 
val sym: thm 

63 
val trans: thm 

64 
val TrueI: thm 

65 
end; 

66 

67 

68 
structure IFOL_Lemmas : IFOL_LEMMAS = 

69 
struct 

70 

71 
val TrueI = prove_goalw IFOL.thy [True_def] "True" 

72 
(fn _ => [ (REPEAT (ares_tac [impI] 1)) ]); 

73 

74 
(*** Sequentstyle elimination rules for & > and ALL ***) 

75 

76 
val conjE = prove_goal IFOL.thy 

77 
"[ P&Q; [ P; Q ] ==> R ] ==> R" 

78 
(fn prems=> 

79 
[ (REPEAT (resolve_tac prems 1 

80 
ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN 

81 
resolve_tac prems 1))) ]); 

82 

83 
val impE = prove_goal IFOL.thy 

84 
"[ P>Q; P; Q ==> R ] ==> R" 

85 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); 

86 

87 
val allE = prove_goal IFOL.thy 

88 
"[ ALL x.P(x); P(x) ==> R ] ==> R" 

89 
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); 

90 

91 
(*Duplicates the quantifier; for use with eresolve_tac*) 

92 
val all_dupE = prove_goal IFOL.thy 

93 
"[ ALL x.P(x); [ P(x); ALL x.P(x) ] ==> R \ 

94 
\ ] ==> R" 

95 
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); 

96 

97 

98 
(*** Negation rules, which translate between ~P and P>False ***) 

99 

100 
val notI = prove_goalw IFOL.thy [not_def] "(P ==> False) ==> ~P" 

101 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); 

102 

103 
val notE = prove_goalw IFOL.thy [not_def] "[ ~P; P ] ==> R" 

104 
(fn prems=> 

105 
[ (resolve_tac [mp RS FalseE] 1), 

106 
(REPEAT (resolve_tac prems 1)) ]); 

107 

108 
(*This is useful with the special implication rules for each kind of P. *) 

109 
val not_to_imp = prove_goal IFOL.thy 

110 
"[ ~P; (P>False) ==> Q ] ==> Q" 

111 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); 

112 

113 

114 
(* For substitution int an assumption P, reduce Q to P>Q, substitute into 

115 
this implication, then apply impI to move P back into the assumptions. 

116 
To specify P use something like 

117 
eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) 

118 
val rev_mp = prove_goal IFOL.thy "[ P; P > Q ] ==> Q" 

119 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); 

120 

121 

122 
(*Contrapositive of an inference rule*) 

123 
val contrapos = prove_goal IFOL.thy "[ ~Q; P==>Q ] ==> ~P" 

124 
(fn [major,minor]=> 

125 
[ (rtac (major RS notE RS notI) 1), 

126 
(etac minor 1) ]); 

127 

128 

129 
(*** Modus Ponens Tactics ***) 

130 

131 
(*Finds P>Q and P in the assumptions, replaces implication by Q *) 

132 
fun mp_tac i = eresolve_tac [notE,impE] i THEN assume_tac i; 

133 

134 
(*Like mp_tac but instantiates no variables*) 

135 
fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i; 

136 

137 

138 
(*** Ifandonlyif ***) 

139 

140 
val iffI = prove_goalw IFOL.thy [iff_def] 

141 
"[ P ==> Q; Q ==> P ] ==> P<>Q" 

142 
(fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); 

143 

144 

145 
(*Observe use of rewrite_rule to unfold "<>" in metaassumptions (prems) *) 

146 
val iffE = prove_goalw IFOL.thy [iff_def] 

147 
"[ P <> Q; [ P>Q; Q>P ] ==> R ] ==> R" 

148 
(fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]); 

149 

150 
(* Destruct rules for <> similar to Modus Ponens *) 

151 

152 
val iffD1 = prove_goalw IFOL.thy [iff_def] "[ P <> Q; P ] ==> Q" 

153 
(fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); 

154 

155 
val iffD2 = prove_goalw IFOL.thy [iff_def] "[ P <> Q; Q ] ==> P" 

156 
(fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); 

157 

158 
val iff_refl = prove_goal IFOL.thy "P <> P" 

159 
(fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]); 

160 

161 
val iff_sym = prove_goal IFOL.thy "Q <> P ==> P <> Q" 

162 
(fn [major] => 

163 
[ (rtac (major RS iffE) 1), 

164 
(rtac iffI 1), 

165 
(REPEAT (eresolve_tac [asm_rl,mp] 1)) ]); 

166 

167 
val iff_trans = prove_goal IFOL.thy 

168 
"!!P Q R. [ P <> Q; Q<> R ] ==> P <> R" 

169 
(fn _ => 

170 
[ (rtac iffI 1), 

171 
(REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]); 

172 

173 

174 
(*** Unique existence. NOTE THAT the following 2 quantifications 

175 
EX!x such that [EX!y such that P(x,y)] (sequential) 

176 
EX!x,y such that P(x,y) (simultaneous) 

177 
do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. 

178 
***) 

179 

180 
val ex1I = prove_goalw IFOL.thy [ex1_def] 

181 
"[ P(a); !!x. P(x) ==> x=a ] ==> EX! x. P(x)" 

182 
(fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]); 

183 

12
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

184 
(*Sometimes easier to use: the premises have no shared variables*) 
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

185 
val ex_ex1I = prove_goal IFOL.thy 
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

186 
"[ EX x.P(x); !!x y. [ P(x); P(y) ] ==> x=y ] ==> EX! x. P(x)" 
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

187 
(fn [ex,eq] => [ (rtac (ex RS exE) 1), 
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

188 
(REPEAT (ares_tac [ex1I,eq] 1)) ]); 
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

189 

0  190 
val ex1E = prove_goalw IFOL.thy [ex1_def] 
191 
"[ EX! x.P(x); !!x. [ P(x); ALL y. P(y) > y=x ] ==> R ] ==> R" 

192 
(fn prems => 

193 
[ (cut_facts_tac prems 1), 

194 
(REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]); 

195 

196 

197 
(*** <> congruence rules for simplification ***) 

198 

199 
(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) 

200 
fun iff_tac prems i = 

201 
resolve_tac (prems RL [iffE]) i THEN 

202 
REPEAT1 (eresolve_tac [asm_rl,mp] i); 

203 

204 
val conj_cong = prove_goal IFOL.thy 

205 
"[ P <> P'; P' ==> Q <> Q' ] ==> (P&Q) <> (P'&Q')" 

206 
(fn prems => 

207 
[ (cut_facts_tac prems 1), 

208 
(REPEAT (ares_tac [iffI,conjI] 1 

209 
ORELSE eresolve_tac [iffE,conjE,mp] 1 

210 
ORELSE iff_tac prems 1)) ]); 

211 

212 
val disj_cong = prove_goal IFOL.thy 

213 
"[ P <> P'; Q <> Q' ] ==> (PQ) <> (P'Q')" 

214 
(fn prems => 

215 
[ (cut_facts_tac prems 1), 

216 
(REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 

217 
ORELSE ares_tac [iffI] 1 

218 
ORELSE mp_tac 1)) ]); 

219 

220 
val imp_cong = prove_goal IFOL.thy 

221 
"[ P <> P'; P' ==> Q <> Q' ] ==> (P>Q) <> (P'>Q')" 

222 
(fn prems => 

223 
[ (cut_facts_tac prems 1), 

224 
(REPEAT (ares_tac [iffI,impI] 1 

225 
ORELSE eresolve_tac [iffE] 1 

226 
ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); 

227 

228 
val iff_cong = prove_goal IFOL.thy 

229 
"[ P <> P'; Q <> Q' ] ==> (P<>Q) <> (P'<>Q')" 

230 
(fn prems => 

231 
[ (cut_facts_tac prems 1), 

232 
(REPEAT (eresolve_tac [iffE] 1 

233 
ORELSE ares_tac [iffI] 1 

234 
ORELSE mp_tac 1)) ]); 

235 

236 
val not_cong = prove_goal IFOL.thy 

237 
"P <> P' ==> ~P <> ~P'" 

238 
(fn prems => 

239 
[ (cut_facts_tac prems 1), 

240 
(REPEAT (ares_tac [iffI,notI] 1 

241 
ORELSE mp_tac 1 

242 
ORELSE eresolve_tac [iffE,notE] 1)) ]); 

243 

244 
val all_cong = prove_goal IFOL.thy 

245 
"(!!x.P(x) <> Q(x)) ==> (ALL x.P(x)) <> (ALL x.Q(x))" 

246 
(fn prems => 

247 
[ (REPEAT (ares_tac [iffI,allI] 1 

248 
ORELSE mp_tac 1 

249 
ORELSE eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]); 

250 

251 
val ex_cong = prove_goal IFOL.thy 

252 
"(!!x.P(x) <> Q(x)) ==> (EX x.P(x)) <> (EX x.Q(x))" 

253 
(fn prems => 

254 
[ (REPEAT (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1 

255 
ORELSE mp_tac 1 

256 
ORELSE iff_tac prems 1)) ]); 

257 

258 
val ex1_cong = prove_goal IFOL.thy 

259 
"(!!x.P(x) <> Q(x)) ==> (EX! x.P(x)) <> (EX! x.Q(x))" 

260 
(fn prems => 

261 
[ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 

262 
ORELSE mp_tac 1 

263 
ORELSE iff_tac prems 1)) ]); 

264 

265 
(*** Equality rules ***) 

266 

267 
val sym = prove_goal IFOL.thy "a=b ==> b=a" 

268 
(fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]); 

269 

270 
val trans = prove_goal IFOL.thy "[ a=b; b=c ] ==> a=c" 

271 
(fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]); 

272 

273 
(** ~ b=a ==> ~ a=b **) 

274 
val [not_sym] = compose(sym,2,contrapos); 

275 

276 
(*calling "standard" reduces maxidx to 0*) 

277 
val ssubst = standard (sym RS subst); 

278 

279 
(*A special case of ex1E that would otherwise need quantifier expansion*) 

280 
val ex1_equalsE = prove_goal IFOL.thy 

281 
"[ EX! x.P(x); P(a); P(b) ] ==> a=b" 

282 
(fn prems => 

283 
[ (cut_facts_tac prems 1), 

284 
(etac ex1E 1), 

285 
(rtac trans 1), 

286 
(rtac sym 2), 

287 
(REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]); 

288 

289 
(** Polymorphic congruence rules **) 

290 

291 
val subst_context = prove_goal IFOL.thy 

292 
"[ a=b ] ==> t(a)=t(b)" 

293 
(fn prems=> 

294 
[ (resolve_tac (prems RL [ssubst]) 1), 

295 
(resolve_tac [refl] 1) ]); 

296 

297 
val subst_context2 = prove_goal IFOL.thy 

298 
"[ a=b; c=d ] ==> t(a,c)=t(b,d)" 

299 
(fn prems=> 

300 
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); 

301 

302 
val subst_context3 = prove_goal IFOL.thy 

303 
"[ a=b; c=d; e=f ] ==> t(a,c,e)=t(b,d,f)" 

304 
(fn prems=> 

305 
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); 

306 

307 
(*Useful with eresolve_tac for proving equalties from known equalities. 

308 
a = b 

309 
  

310 
c = d *) 

311 
val box_equals = prove_goal IFOL.thy 

312 
"[ a=b; a=c; b=d ] ==> c=d" 

313 
(fn prems=> 

314 
[ (resolve_tac [trans] 1), 

315 
(resolve_tac [trans] 1), 

316 
(resolve_tac [sym] 1), 

317 
(REPEAT (resolve_tac prems 1)) ]); 

318 

319 
(*Dual of box_equals: for proving equalities backwards*) 

320 
val simp_equals = prove_goal IFOL.thy 

321 
"[ a=c; b=d; c=d ] ==> a=b" 

322 
(fn prems=> 

323 
[ (resolve_tac [trans] 1), 

324 
(resolve_tac [trans] 1), 

325 
(REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]); 

326 

327 
(** Congruence rules for predicate letters **) 

328 

329 
val pred1_cong = prove_goal IFOL.thy 

330 
"a=a' ==> P(a) <> P(a')" 

331 
(fn prems => 

332 
[ (cut_facts_tac prems 1), 

333 
(rtac iffI 1), 

334 
(DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); 

335 

336 
val pred2_cong = prove_goal IFOL.thy 

337 
"[ a=a'; b=b' ] ==> P(a,b) <> P(a',b')" 

338 
(fn prems => 

339 
[ (cut_facts_tac prems 1), 

340 
(rtac iffI 1), 

341 
(DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); 

342 

343 
val pred3_cong = prove_goal IFOL.thy 

344 
"[ a=a'; b=b'; c=c' ] ==> P(a,b,c) <> P(a',b',c')" 

345 
(fn prems => 

346 
[ (cut_facts_tac prems 1), 

347 
(rtac iffI 1), 

348 
(DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); 

349 

350 
(*special cases for free variables P, Q, R, S  up to 3 arguments*) 

351 

352 
val pred_congs = 

353 
flat (map (fn c => 

354 
map (fn th => read_instantiate [("P",c)] th) 

355 
[pred1_cong,pred2_cong,pred3_cong]) 

356 
(explode"PQRS")); 

357 

358 
(*special case for the equality predicate!*) 

359 
val eq_cong = read_instantiate [("P","op =")] pred2_cong; 

360 

361 

362 
(*** Simplifications of assumed implications. 

363 
Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE 

364 
used with mp_tac (restricted to atomic formulae) is COMPLETE for 

365 
intuitionistic propositional logic. See 

366 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

367 
(preprint, University of St Andrews, 1991) ***) 

368 

369 
val conj_impE = prove_goal IFOL.thy 

370 
"[ (P&Q)>S; P>(Q>S) ==> R ] ==> R" 

371 
(fn major::prems=> 

372 
[ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]); 

373 

374 
val disj_impE = prove_goal IFOL.thy 

375 
"[ (PQ)>S; [ P>S; Q>S ] ==> R ] ==> R" 

376 
(fn major::prems=> 

377 
[ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]); 

378 

379 
(*Simplifies the implication. Classical version is stronger. 

380 
Still UNSAFE since Q must be provable  backtracking needed. *) 

381 
val imp_impE = prove_goal IFOL.thy 

382 
"[ (P>Q)>S; [ P; Q>S ] ==> Q; S ==> R ] ==> R" 

383 
(fn major::prems=> 

384 
[ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]); 

385 

386 
(*Simplifies the implication. Classical version is stronger. 

387 
Still UNSAFE since ~P must be provable  backtracking needed. *) 

388 
val not_impE = prove_goal IFOL.thy 

389 
"[ ~P > S; P ==> False; S ==> R ] ==> R" 

390 
(fn major::prems=> 

391 
[ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]); 

392 

393 
(*Simplifies the implication. UNSAFE. *) 

394 
val iff_impE = prove_goal IFOL.thy 

395 
"[ (P<>Q)>S; [ P; Q>S ] ==> Q; [ Q; P>S ] ==> P; \ 

396 
\ S ==> R ] ==> R" 

397 
(fn major::prems=> 

398 
[ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]); 

399 

400 
(*What if (ALL x.~~P(x)) > ~~(ALL x.P(x)) is an assumption? UNSAFE*) 

401 
val all_impE = prove_goal IFOL.thy 

402 
"[ (ALL x.P(x))>S; !!x.P(x); S ==> R ] ==> R" 

403 
(fn major::prems=> 

404 
[ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]); 

405 

406 
(*Unsafe: (EX x.P(x))>S is equivalent to ALL x.P(x)>S. *) 

407 
val ex_impE = prove_goal IFOL.thy 

408 
"[ (EX x.P(x))>S; P(x)>S ==> R ] ==> R" 

409 
(fn major::prems=> 

410 
[ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]); 

411 

412 
end; 

413 

414 
open IFOL_Lemmas; 

415 