author  wenzelm 
Sun, 26 Nov 2006 23:43:53 +0100  
changeset 21539  c5cf9243ad62 
parent 21524  7843e2fd14a9 
child 22139  539a63b98f76 
permissions  rwrr 
1268  1 
(* Title: FOL/IFOL.thy 
35  2 
ID: $Id$ 
11677  3 
Author: Lawrence C Paulson and Markus Wenzel 
4 
*) 

35  5 

11677  6 
header {* Intuitionistic firstorder logic *} 
35  7 

15481  8 
theory IFOL 
9 
imports Pure 

21539  10 
uses ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML") 
15481  11 
begin 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

12 

0  13 

11677  14 
subsection {* Syntax and axiomatic basis *} 
15 

3906  16 
global 
17 

14854  18 
classes "term" 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

19 
defaultsort "term" 
0  20 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

21 
typedecl o 
79  22 

11747  23 
judgment 
24 
Trueprop :: "o => prop" ("(_)" 5) 

0  25 

11747  26 
consts 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

27 
True :: o 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

28 
False :: o 
79  29 

30 
(* Connectives *) 

31 

17276  32 
"op =" :: "['a, 'a] => o" (infixl "=" 50) 
35  33 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

34 
Not :: "o => o" ("~ _" [40] 40) 
17276  35 
"op &" :: "[o, o] => o" (infixr "&" 35) 
36 
"op " :: "[o, o] => o" (infixr "" 30) 

37 
"op >" :: "[o, o] => o" (infixr ">" 25) 

38 
"op <>" :: "[o, o] => o" (infixr "<>" 25) 

79  39 

40 
(* Quantifiers *) 

41 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

42 
All :: "('a => o) => o" (binder "ALL " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

43 
Ex :: "('a => o) => o" (binder "EX " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

44 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 
79  45 

0  46 

19363  47 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

48 
not_equal :: "['a, 'a] => o" (infixl "~=" 50) where 
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

49 
"x ~= y == ~ (x = y)" 
79  50 

21210  51 
notation (xsymbols) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset

52 
not_equal (infixl "\<noteq>" 50) 
19363  53 

21210  54 
notation (HTML output) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset

55 
not_equal (infixl "\<noteq>" 50) 
19363  56 

21524  57 
notation (xsymbols) 
21539  58 
Not ("\<not> _" [40] 40) and 
59 
"op &" (infixr "\<and>" 35) and 

60 
"op " (infixr "\<or>" 30) and 

61 
All (binder "\<forall>" 10) and 

62 
Ex (binder "\<exists>" 10) and 

63 
Ex1 (binder "\<exists>!" 10) and 

21524  64 
"op >" (infixr "\<longrightarrow>" 25) and 
65 
"op <>" (infixr "\<longleftrightarrow>" 25) 

35  66 

21524  67 
notation (HTML output) 
21539  68 
Not ("\<not> _" [40] 40) and 
69 
"op &" (infixr "\<and>" 35) and 

70 
"op " (infixr "\<or>" 30) and 

71 
All (binder "\<forall>" 10) and 

72 
Ex (binder "\<exists>" 10) and 

73 
Ex1 (binder "\<exists>!" 10) 

6340  74 

3932  75 
local 
3906  76 

14236  77 
finalconsts 
78 
False All Ex 

79 
"op =" 

80 
"op &" 

81 
"op " 

82 
"op >" 

83 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

84 
axioms 
0  85 

79  86 
(* Equality *) 
0  87 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

88 
refl: "a=a" 
0  89 

79  90 
(* Propositional logic *) 
0  91 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

92 
conjI: "[ P; Q ] ==> P&Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

93 
conjunct1: "P&Q ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

94 
conjunct2: "P&Q ==> Q" 
0  95 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

96 
disjI1: "P ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

97 
disjI2: "Q ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

98 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  99 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

100 
impI: "(P ==> Q) ==> P>Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

101 
mp: "[ P>Q; P ] ==> Q" 
0  102 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

103 
FalseE: "False ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

104 

79  105 
(* Quantifiers *) 
0  106 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

107 
allI: "(!!x. P(x)) ==> (ALL x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

108 
spec: "(ALL x. P(x)) ==> P(x)" 
0  109 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

110 
exI: "P(x) ==> (EX x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

111 
exE: "[ EX x. P(x); !!x. P(x) ==> R ] ==> R" 
0  112 

113 
(* Reflection *) 

114 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

115 
eq_reflection: "(x=y) ==> (x==y)" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

116 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  117 

4092  118 

19756  119 
lemmas strip = impI allI 
120 

121 

15377  122 
text{*Thanks to Stephan Merz*} 
123 
theorem subst: 

124 
assumes eq: "a = b" and p: "P(a)" 

125 
shows "P(b)" 

126 
proof  

127 
from eq have meta: "a \<equiv> b" 

128 
by (rule eq_reflection) 

129 
from p show ?thesis 

130 
by (unfold meta) 

131 
qed 

132 

133 

14236  134 
defs 
135 
(* Definitions *) 

136 

137 
True_def: "True == False>False" 

138 
not_def: "~P == P>False" 

139 
iff_def: "P<>Q == (P>Q) & (Q>P)" 

140 

141 
(* Unique existence *) 

142 

143 
ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) > y=x)" 

144 

13779  145 

11677  146 
subsection {* Lemmas and proof tools *} 
147 

21539  148 
lemma TrueI: True 
149 
unfolding True_def by (rule impI) 

150 

151 

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

153 

154 
lemma conjE: 

155 
assumes major: "P & Q" 

156 
and r: "[ P; Q ] ==> R" 

157 
shows R 

158 
apply (rule r) 

159 
apply (rule major [THEN conjunct1]) 

160 
apply (rule major [THEN conjunct2]) 

161 
done 

162 

163 
lemma impE: 

164 
assumes major: "P > Q" 

165 
and P 

166 
and r: "Q ==> R" 

167 
shows R 

168 
apply (rule r) 

169 
apply (rule major [THEN mp]) 

170 
apply (rule `P`) 

171 
done 

172 

173 
lemma allE: 

174 
assumes major: "ALL x. P(x)" 

175 
and r: "P(x) ==> R" 

176 
shows R 

177 
apply (rule r) 

178 
apply (rule major [THEN spec]) 

179 
done 

180 

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

182 
lemma all_dupE: 

183 
assumes major: "ALL x. P(x)" 

184 
and r: "[ P(x); ALL x. P(x) ] ==> R" 

185 
shows R 

186 
apply (rule r) 

187 
apply (rule major [THEN spec]) 

188 
apply (rule major) 

189 
done 

190 

191 

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

193 

194 
lemma notI: "(P ==> False) ==> ~P" 

195 
unfolding not_def by (erule impI) 

196 

197 
lemma notE: "[ ~P; P ] ==> R" 

198 
unfolding not_def by (erule mp [THEN FalseE]) 

199 

200 
lemma rev_notE: "[ P; ~P ] ==> R" 

201 
by (erule notE) 

202 

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

204 
lemma not_to_imp: 

205 
assumes "~P" 

206 
and r: "P > False ==> Q" 

207 
shows Q 

208 
apply (rule r) 

209 
apply (rule impI) 

210 
apply (erule notE [OF `~P`]) 

211 
done 

212 

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

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

215 
To specify P use something like 

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

217 
lemma rev_mp: "[ P; P > Q ] ==> Q" 

218 
by (erule mp) 

219 

220 
(*Contrapositive of an inference rule*) 

221 
lemma contrapos: 

222 
assumes major: "~Q" 

223 
and minor: "P ==> Q" 

224 
shows "~P" 

225 
apply (rule major [THEN notE, THEN notI]) 

226 
apply (erule minor) 

227 
done 

228 

229 

230 
(*** Modus Ponens Tactics ***) 

231 

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

233 
ML {* 

234 
local 

235 
val notE = thm "notE" 

236 
val impE = thm "impE" 

237 
in 

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

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

240 
end 

241 
*} 

242 

243 

244 
(*** Ifandonlyif ***) 

245 

246 
lemma iffI: "[ P ==> Q; Q ==> P ] ==> P<>Q" 

247 
apply (unfold iff_def) 

248 
apply (rule conjI) 

249 
apply (erule impI) 

250 
apply (erule impI) 

251 
done 

252 

253 

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

255 
lemma iffE: 

256 
assumes major: "P <> Q" 

257 
and r: "P>Q ==> Q>P ==> R" 

258 
shows R 

259 
apply (insert major, unfold iff_def) 

260 
apply (erule conjE) 

261 
apply (erule r) 

262 
apply assumption 

263 
done 

264 

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

266 

267 
lemma iffD1: "[ P <> Q; P ] ==> Q" 

268 
apply (unfold iff_def) 

269 
apply (erule conjunct1 [THEN mp]) 

270 
apply assumption 

271 
done 

272 

273 
lemma iffD2: "[ P <> Q; Q ] ==> P" 

274 
apply (unfold iff_def) 

275 
apply (erule conjunct2 [THEN mp]) 

276 
apply assumption 

277 
done 

278 

279 
lemma rev_iffD1: "[ P; P <> Q ] ==> Q" 

280 
apply (erule iffD1) 

281 
apply assumption 

282 
done 

283 

284 
lemma rev_iffD2: "[ Q; P <> Q ] ==> P" 

285 
apply (erule iffD2) 

286 
apply assumption 

287 
done 

288 

289 
lemma iff_refl: "P <> P" 

290 
by (rule iffI) 

291 

292 
lemma iff_sym: "Q <> P ==> P <> Q" 

293 
apply (erule iffE) 

294 
apply (rule iffI) 

295 
apply (assumption  erule mp)+ 

296 
done 

297 

298 
lemma iff_trans: "[ P <> Q; Q<> R ] ==> P <> R" 

299 
apply (rule iffI) 

300 
apply (assumption  erule iffE  erule (1) notE impE)+ 

301 
done 

302 

303 

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

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

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

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

308 
***) 

309 

310 
lemma ex1I: 

311 
assumes "P(a)" 

312 
and "!!x. P(x) ==> x=a" 

313 
shows "EX! x. P(x)" 

314 
apply (unfold ex1_def) 

315 
apply (assumption  rule assms exI conjI allI impI)+ 

316 
done 

317 

318 
(*Sometimes easier to use: the premises have no shared variables. Safe!*) 

319 
lemma ex_ex1I: 

320 
assumes ex: "EX x. P(x)" 

321 
and eq: "!!x y. [ P(x); P(y) ] ==> x=y" 

322 
shows "EX! x. P(x)" 

323 
apply (rule ex [THEN exE]) 

324 
apply (assumption  rule ex1I eq)+ 

325 
done 

326 

327 
lemma ex1E: 

328 
assumes ex1: "EX! x. P(x)" 

329 
and r: "!!x. [ P(x); ALL y. P(y) > y=x ] ==> R" 

330 
shows R 

331 
apply (insert ex1, unfold ex1_def) 

332 
apply (assumption  erule exE conjE)+ 

333 
done 

334 

335 

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

337 

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

339 
ML {* 

340 
local 

341 
val iffE = thm "iffE" 

342 
val mp = thm "mp" 

343 
in 

344 
fun iff_tac prems i = 

345 
resolve_tac (prems RL [iffE]) i THEN 

346 
REPEAT1 (eresolve_tac [asm_rl, mp] i) 

347 
end 

348 
*} 

349 

350 
lemma conj_cong: 

351 
assumes "P <> P'" 

352 
and "P' ==> Q <> Q'" 

353 
shows "(P&Q) <> (P'&Q')" 

354 
apply (insert assms) 

355 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

356 
tactic {* iff_tac (thms "assms") 1 *})+ 

357 
done 

358 

359 
(*Reversed congruence rule! Used in ZF/Order*) 

360 
lemma conj_cong2: 

361 
assumes "P <> P'" 

362 
and "P' ==> Q <> Q'" 

363 
shows "(Q&P) <> (Q'&P')" 

364 
apply (insert assms) 

365 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

366 
tactic {* iff_tac (thms "assms") 1 *})+ 

367 
done 

368 

369 
lemma disj_cong: 

370 
assumes "P <> P'" and "Q <> Q'" 

371 
shows "(PQ) <> (P'Q')" 

372 
apply (insert assms) 

373 
apply (erule iffE disjE disjI1 disjI2  assumption  rule iffI  erule (1) notE impE)+ 

374 
done 

375 

376 
lemma imp_cong: 

377 
assumes "P <> P'" 

378 
and "P' ==> Q <> Q'" 

379 
shows "(P>Q) <> (P'>Q')" 

380 
apply (insert assms) 

381 
apply (assumption  rule iffI impI  erule iffE  erule (1) notE impE  

382 
tactic {* iff_tac (thms "assms") 1 *})+ 

383 
done 

384 

385 
lemma iff_cong: "[ P <> P'; Q <> Q' ] ==> (P<>Q) <> (P'<>Q')" 

386 
apply (erule iffE  assumption  rule iffI  erule (1) notE impE)+ 

387 
done 

388 

389 
lemma not_cong: "P <> P' ==> ~P <> ~P'" 

390 
apply (assumption  rule iffI notI  erule (1) notE impE  erule iffE notE)+ 

391 
done 

392 

393 
lemma all_cong: 

394 
assumes "!!x. P(x) <> Q(x)" 

395 
shows "(ALL x. P(x)) <> (ALL x. Q(x))" 

396 
apply (assumption  rule iffI allI  erule (1) notE impE  erule allE  

397 
tactic {* iff_tac (thms "assms") 1 *})+ 

398 
done 

399 

400 
lemma ex_cong: 

401 
assumes "!!x. P(x) <> Q(x)" 

402 
shows "(EX x. P(x)) <> (EX x. Q(x))" 

403 
apply (erule exE  assumption  rule iffI exI  erule (1) notE impE  

404 
tactic {* iff_tac (thms "assms") 1 *})+ 

405 
done 

406 

407 
lemma ex1_cong: 

408 
assumes "!!x. P(x) <> Q(x)" 

409 
shows "(EX! x. P(x)) <> (EX! x. Q(x))" 

410 
apply (erule ex1E spec [THEN mp]  assumption  rule iffI ex1I  erule (1) notE impE  

411 
tactic {* iff_tac (thms "assms") 1 *})+ 

412 
done 

413 

414 
(*** Equality rules ***) 

415 

416 
lemma sym: "a=b ==> b=a" 

417 
apply (erule subst) 

418 
apply (rule refl) 

419 
done 

420 

421 
lemma trans: "[ a=b; b=c ] ==> a=c" 

422 
apply (erule subst, assumption) 

423 
done 

424 

425 
(** **) 

426 
lemma not_sym: "b ~= a ==> a ~= b" 

427 
apply (erule contrapos) 

428 
apply (erule sym) 

429 
done 

430 

431 
(* Two theorms for rewriting only one instance of a definition: 

432 
the first for definitions of formulae and the second for terms *) 

433 

434 
lemma def_imp_iff: "(A == B) ==> A <> B" 

435 
apply unfold 

436 
apply (rule iff_refl) 

437 
done 

438 

439 
lemma meta_eq_to_obj_eq: "(A == B) ==> A = B" 

440 
apply unfold 

441 
apply (rule refl) 

442 
done 

443 

444 
lemma meta_eq_to_iff: "x==y ==> x<>y" 

445 
by unfold (rule iff_refl) 

446 

447 
(*substitution*) 

448 
lemma ssubst: "[ b = a; P(a) ] ==> P(b)" 

449 
apply (drule sym) 

450 
apply (erule (1) subst) 

451 
done 

452 

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

454 
lemma ex1_equalsE: 

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

456 
apply (erule ex1E) 

457 
apply (rule trans) 

458 
apply (rule_tac [2] sym) 

459 
apply (assumption  erule spec [THEN mp])+ 

460 
done 

461 

462 
(** Polymorphic congruence rules **) 

463 

464 
lemma subst_context: "[ a=b ] ==> t(a)=t(b)" 

465 
apply (erule ssubst) 

466 
apply (rule refl) 

467 
done 

468 

469 
lemma subst_context2: "[ a=b; c=d ] ==> t(a,c)=t(b,d)" 

470 
apply (erule ssubst)+ 

471 
apply (rule refl) 

472 
done 

473 

474 
lemma subst_context3: "[ a=b; c=d; e=f ] ==> t(a,c,e)=t(b,d,f)" 

475 
apply (erule ssubst)+ 

476 
apply (rule refl) 

477 
done 

478 

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

480 
a = b 

481 
  

482 
c = d *) 

483 
lemma box_equals: "[ a=b; a=c; b=d ] ==> c=d" 

484 
apply (rule trans) 

485 
apply (rule trans) 

486 
apply (rule sym) 

487 
apply assumption+ 

488 
done 

489 

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

491 
lemma simp_equals: "[ a=c; b=d; c=d ] ==> a=b" 

492 
apply (rule trans) 

493 
apply (rule trans) 

494 
apply assumption+ 

495 
apply (erule sym) 

496 
done 

497 

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

499 

500 
lemma pred1_cong: "a=a' ==> P(a) <> P(a')" 

501 
apply (rule iffI) 

502 
apply (erule (1) subst) 

503 
apply (erule (1) ssubst) 

504 
done 

505 

506 
lemma pred2_cong: "[ a=a'; b=b' ] ==> P(a,b) <> P(a',b')" 

507 
apply (rule iffI) 

508 
apply (erule subst)+ 

509 
apply assumption 

510 
apply (erule ssubst)+ 

511 
apply assumption 

512 
done 

513 

514 
lemma pred3_cong: "[ a=a'; b=b'; c=c' ] ==> P(a,b,c) <> P(a',b',c')" 

515 
apply (rule iffI) 

516 
apply (erule subst)+ 

517 
apply assumption 

518 
apply (erule ssubst)+ 

519 
apply assumption 

520 
done 

521 

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

523 

524 
ML {* 

525 
bind_thms ("pred_congs", 

526 
List.concat (map (fn c => 

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

528 
[thm "pred1_cong", thm "pred2_cong", thm "pred3_cong"]) 

529 
(explode"PQRS"))) 

530 
*} 

531 

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

533 
lemma eq_cong: "[ a = a'; b = b' ] ==> a = b <> a' = b'" 

534 
apply (erule (1) pred2_cong) 

535 
done 

536 

537 

538 
(*** Simplifications of assumed implications. 

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

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

541 
intuitionistic propositional logic. See 

542 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

544 

545 
lemma conj_impE: 

546 
assumes major: "(P&Q)>S" 

547 
and r: "P>(Q>S) ==> R" 

548 
shows R 

549 
by (assumption  rule conjI impI major [THEN mp] r)+ 

550 

551 
lemma disj_impE: 

552 
assumes major: "(PQ)>S" 

553 
and r: "[ P>S; Q>S ] ==> R" 

554 
shows R 

555 
by (assumption  rule disjI1 disjI2 impI major [THEN mp] r)+ 

556 

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

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

559 
lemma imp_impE: 

560 
assumes major: "(P>Q)>S" 

561 
and r1: "[ P; Q>S ] ==> Q" 

562 
and r2: "S ==> R" 

563 
shows R 

564 
by (assumption  rule impI major [THEN mp] r1 r2)+ 

565 

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

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

568 
lemma not_impE: 

569 
assumes major: "~P > S" 

570 
and r1: "P ==> False" 

571 
and r2: "S ==> R" 

572 
shows R 

573 
apply (assumption  rule notI impI major [THEN mp] r1 r2)+ 

574 
done 

575 

576 
(*Simplifies the implication. UNSAFE. *) 

577 
lemma iff_impE: 

578 
assumes major: "(P<>Q)>S" 

579 
and r1: "[ P; Q>S ] ==> Q" 

580 
and r2: "[ Q; P>S ] ==> P" 

581 
and r3: "S ==> R" 

582 
shows R 

583 
apply (assumption  rule iffI impI major [THEN mp] r1 r2 r3)+ 

584 
done 

585 

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

587 
lemma all_impE: 

588 
assumes major: "(ALL x. P(x))>S" 

589 
and r1: "!!x. P(x)" 

590 
and r2: "S ==> R" 

591 
shows R 

592 
apply (assumption  rule allI impI major [THEN mp] r1 r2)+ 

593 
done 

594 

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

596 
lemma ex_impE: 

597 
assumes major: "(EX x. P(x))>S" 

598 
and r: "P(x)>S ==> R" 

599 
shows R 

600 
apply (assumption  rule exI impI major [THEN mp] r)+ 

601 
done 

602 

603 
(*** Courtesy of Krzysztof Grabczewski ***) 

604 

605 
lemma disj_imp_disj: 

606 
assumes major: "PQ" 

607 
and "P==>R" and "Q==>S" 

608 
shows "RS" 

609 
apply (rule disjE [OF major]) 

610 
apply (rule disjI1) apply assumption 

611 
apply (rule disjI2) apply assumption 

612 
done 

11734  613 

18481  614 
ML {* 
615 
structure ProjectRule = ProjectRuleFun 

616 
(struct 

617 
val conjunct1 = thm "conjunct1"; 

618 
val conjunct2 = thm "conjunct2"; 

619 
val mp = thm "mp"; 

620 
end) 

621 
*} 

622 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

623 
use "fologic.ML" 
21539  624 

625 
lemma thin_refl: "!!X. [x=x; PROP W] ==> PROP W" . 

626 

9886  627 
use "hypsubstdata.ML" 
628 
setup hypsubst_setup 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

629 
use "intprover.ML" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

630 

4092  631 

12875  632 
subsection {* Intuitionistic Reasoning *} 
12368  633 

12349  634 
lemma impE': 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

635 
assumes 1: "P > Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

636 
and 2: "Q ==> R" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

637 
and 3: "P > Q ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

638 
shows R 
12349  639 
proof  
640 
from 3 and 1 have P . 

12368  641 
with 1 have Q by (rule impE) 
12349  642 
with 2 show R . 
643 
qed 

644 

645 
lemma allE': 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

646 
assumes 1: "ALL x. P(x)" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

647 
and 2: "P(x) ==> ALL x. P(x) ==> Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

648 
shows Q 
12349  649 
proof  
650 
from 1 have "P(x)" by (rule spec) 

651 
from this and 1 show Q by (rule 2) 

652 
qed 

653 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

654 
lemma notE': 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

655 
assumes 1: "~ P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

656 
and 2: "~ P ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

657 
shows R 
12349  658 
proof  
659 
from 2 and 1 have P . 

660 
with 1 show R by (rule notE) 

661 
qed 

662 

663 
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE 

664 
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl 

665 
and [Pure.elim 2] = allE notE' impE' 

666 
and [Pure.intro] = exI disjI2 disjI1 

667 

18708  668 
setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *} 
12349  669 

670 

12368  671 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  672 
by iprover 
12368  673 

674 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

675 
and [Pure.elim?] = iffD1 iffD2 impE 

676 

677 

13435  678 
lemma eq_commute: "a=b <> b=a" 
679 
apply (rule iffI) 

680 
apply (erule sym)+ 

681 
done 

682 

683 

11677  684 
subsection {* Atomizing metalevel rules *} 
685 

11747  686 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  687 
proof 
11677  688 
assume "!!x. P(x)" 
12368  689 
show "ALL x. P(x)" .. 
11677  690 
next 
691 
assume "ALL x. P(x)" 

12368  692 
thus "!!x. P(x)" .. 
11677  693 
qed 
694 

11747  695 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  696 
proof 
12368  697 
assume "A ==> B" 
698 
thus "A > B" .. 

11677  699 
next 
700 
assume "A > B" and A 

701 
thus B by (rule mp) 

702 
qed 

703 

11747  704 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  705 
proof 
11677  706 
assume "x == y" 
707 
show "x = y" by (unfold prems) (rule refl) 

708 
next 

709 
assume "x = y" 

710 
thus "x == y" by (rule eq_reflection) 

711 
qed 

712 

18813  713 
lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <> B)" 
714 
proof 

715 
assume "A == B" 

716 
show "A <> B" by (unfold prems) (rule iff_refl) 

717 
next 

718 
assume "A <> B" 

719 
thus "A == B" by (rule iff_reflection) 

720 
qed 

721 

12875  722 
lemma atomize_conj [atomize]: 
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

723 
includes meta_conjunction_syntax 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

724 
shows "(A && B) == Trueprop (A & B)" 
11976  725 
proof 
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

726 
assume conj: "A && B" 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

727 
show "A & B" 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

728 
proof (rule conjI) 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

729 
from conj show A by (rule conjunctionD1) 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

730 
from conj show B by (rule conjunctionD2) 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

731 
qed 
11953  732 
next 
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

733 
assume conj: "A & B" 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

734 
show "A && B" 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

735 
proof  
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

736 
from conj show A .. 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

737 
from conj show B .. 
11953  738 
qed 
739 
qed 

740 

12368  741 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  742 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  743 

11848  744 

745 
subsection {* Calculational rules *} 

746 

747 
lemma forw_subst: "a = b ==> P(b) ==> P(a)" 

748 
by (rule ssubst) 

749 

750 
lemma back_subst: "P(a) ==> a = b ==> P(b)" 

751 
by (rule subst) 

752 

753 
text {* 

754 
Note that this list of rules is in reverse order of priorities. 

755 
*} 

756 

12019  757 
lemmas basic_trans_rules [trans] = 
11848  758 
forw_subst 
759 
back_subst 

760 
rev_mp 

761 
mp 

762 
trans 

763 

13779  764 
subsection {* ``Let'' declarations *} 
765 

766 
nonterminals letbinds letbind 

767 

768 
constdefs 

14854  769 
Let :: "['a::{}, 'a => 'b] => ('b::{})" 
13779  770 
"Let(s, f) == f(s)" 
771 

772 
syntax 

773 
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) 

774 
"" :: "letbind => letbinds" ("_") 

775 
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") 

776 
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) 

777 

778 
translations 

779 
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" 

780 
"let x = a in e" == "Let(a, %x. e)" 

781 

782 

783 
lemma LetI: 

21539  784 
assumes "!!x. x=t ==> P(u(x))" 
785 
shows "P(let x=t in u(x))" 

786 
apply (unfold Let_def) 

787 
apply (rule refl [THEN assms]) 

788 
done 

789 

790 

791 
subsection {* ML bindings *} 

13779  792 

21539  793 
ML {* 
794 
val refl = thm "refl" 

795 
val trans = thm "trans" 

796 
val sym = thm "sym" 

797 
val subst = thm "subst" 

798 
val ssubst = thm "ssubst" 

799 
val conjI = thm "conjI" 

800 
val conjE = thm "conjE" 

801 
val conjunct1 = thm "conjunct1" 

802 
val conjunct2 = thm "conjunct2" 

803 
val disjI1 = thm "disjI1" 

804 
val disjI2 = thm "disjI2" 

805 
val disjE = thm "disjE" 

806 
val impI = thm "impI" 

807 
val impE = thm "impE" 

808 
val mp = thm "mp" 

809 
val rev_mp = thm "rev_mp" 

810 
val TrueI = thm "TrueI" 

811 
val FalseE = thm "FalseE" 

812 
val iff_refl = thm "iff_refl" 

813 
val iff_trans = thm "iff_trans" 

814 
val iffI = thm "iffI" 

815 
val iffE = thm "iffE" 

816 
val iffD1 = thm "iffD1" 

817 
val iffD2 = thm "iffD2" 

818 
val notI = thm "notI" 

819 
val notE = thm "notE" 

820 
val allI = thm "allI" 

821 
val allE = thm "allE" 

822 
val spec = thm "spec" 

823 
val exI = thm "exI" 

824 
val exE = thm "exE" 

825 
val eq_reflection = thm "eq_reflection" 

826 
val iff_reflection = thm "iff_reflection" 

827 
val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq" 

828 
val meta_eq_to_iff = thm "meta_eq_to_iff" 

13779  829 
*} 
830 

4854  831 
end 