author  wenzelm 
Fri, 11 May 2007 00:43:45 +0200  
changeset 22931  11cc1ccad58e 
parent 22139  539a63b98f76 
child 23155  4b04f9d859af 
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 {* 

22139  234 
fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN assume_tac i 
235 
fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN eq_assume_tac i 

21539  236 
*} 
237 

238 

239 
(*** Ifandonlyif ***) 

240 

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

242 
apply (unfold iff_def) 

243 
apply (rule conjI) 

244 
apply (erule impI) 

245 
apply (erule impI) 

246 
done 

247 

248 

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

250 
lemma iffE: 

251 
assumes major: "P <> Q" 

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

253 
shows R 

254 
apply (insert major, unfold iff_def) 

255 
apply (erule conjE) 

256 
apply (erule r) 

257 
apply assumption 

258 
done 

259 

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

261 

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

263 
apply (unfold iff_def) 

264 
apply (erule conjunct1 [THEN mp]) 

265 
apply assumption 

266 
done 

267 

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

269 
apply (unfold iff_def) 

270 
apply (erule conjunct2 [THEN mp]) 

271 
apply assumption 

272 
done 

273 

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

275 
apply (erule iffD1) 

276 
apply assumption 

277 
done 

278 

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

280 
apply (erule iffD2) 

281 
apply assumption 

282 
done 

283 

284 
lemma iff_refl: "P <> P" 

285 
by (rule iffI) 

286 

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

288 
apply (erule iffE) 

289 
apply (rule iffI) 

290 
apply (assumption  erule mp)+ 

291 
done 

292 

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

294 
apply (rule iffI) 

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

296 
done 

297 

298 

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

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

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

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

303 
***) 

304 

305 
lemma ex1I: 

306 
assumes "P(a)" 

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

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

309 
apply (unfold ex1_def) 

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

311 
done 

312 

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

314 
lemma ex_ex1I: 

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

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

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

318 
apply (rule ex [THEN exE]) 

319 
apply (assumption  rule ex1I eq)+ 

320 
done 

321 

322 
lemma ex1E: 

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

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

325 
shows R 

326 
apply (insert ex1, unfold ex1_def) 

327 
apply (assumption  erule exE conjE)+ 

328 
done 

329 

330 

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

332 

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

334 
ML {* 

22139  335 
fun iff_tac prems i = 
336 
resolve_tac (prems RL @{thms iffE}) i THEN 

337 
REPEAT1 (eresolve_tac [@{thm asm_rl}, @{thm mp}] i) 

21539  338 
*} 
339 

340 
lemma conj_cong: 

341 
assumes "P <> P'" 

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

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

344 
apply (insert assms) 

345 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

347 
done 

348 

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

350 
lemma conj_cong2: 

351 
assumes "P <> P'" 

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

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

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 
lemma disj_cong: 

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

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

362 
apply (insert assms) 

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

364 
done 

365 

366 
lemma imp_cong: 

367 
assumes "P <> P'" 

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

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

370 
apply (insert assms) 

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

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

373 
done 

374 

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

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

377 
done 

378 

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

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

381 
done 

382 

383 
lemma all_cong: 

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

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

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

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

388 
done 

389 

390 
lemma ex_cong: 

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

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

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

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

395 
done 

396 

397 
lemma ex1_cong: 

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

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

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

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

402 
done 

403 

404 
(*** Equality rules ***) 

405 

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

407 
apply (erule subst) 

408 
apply (rule refl) 

409 
done 

410 

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

412 
apply (erule subst, assumption) 

413 
done 

414 

415 
(** **) 

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

417 
apply (erule contrapos) 

418 
apply (erule sym) 

419 
done 

420 

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

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

423 

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

425 
apply unfold 

426 
apply (rule iff_refl) 

427 
done 

428 

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

430 
apply unfold 

431 
apply (rule refl) 

432 
done 

433 

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

435 
by unfold (rule iff_refl) 

436 

437 
(*substitution*) 

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

439 
apply (drule sym) 

440 
apply (erule (1) subst) 

441 
done 

442 

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

444 
lemma ex1_equalsE: 

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

446 
apply (erule ex1E) 

447 
apply (rule trans) 

448 
apply (rule_tac [2] sym) 

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

450 
done 

451 

452 
(** Polymorphic congruence rules **) 

453 

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

455 
apply (erule ssubst) 

456 
apply (rule refl) 

457 
done 

458 

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

460 
apply (erule ssubst)+ 

461 
apply (rule refl) 

462 
done 

463 

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

465 
apply (erule ssubst)+ 

466 
apply (rule refl) 

467 
done 

468 

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

470 
a = b 

471 
  

472 
c = d *) 

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

474 
apply (rule trans) 

475 
apply (rule trans) 

476 
apply (rule sym) 

477 
apply assumption+ 

478 
done 

479 

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

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

482 
apply (rule trans) 

483 
apply (rule trans) 

484 
apply assumption+ 

485 
apply (erule sym) 

486 
done 

487 

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

489 

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

491 
apply (rule iffI) 

492 
apply (erule (1) subst) 

493 
apply (erule (1) ssubst) 

494 
done 

495 

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

497 
apply (rule iffI) 

498 
apply (erule subst)+ 

499 
apply assumption 

500 
apply (erule ssubst)+ 

501 
apply assumption 

502 
done 

503 

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

505 
apply (rule iffI) 

506 
apply (erule subst)+ 

507 
apply assumption 

508 
apply (erule ssubst)+ 

509 
apply assumption 

510 
done 

511 

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

513 

514 
ML {* 

515 
bind_thms ("pred_congs", 

516 
List.concat (map (fn c => 

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

22139  518 
[@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}]) 
21539  519 
(explode"PQRS"))) 
520 
*} 

521 

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

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

524 
apply (erule (1) pred2_cong) 

525 
done 

526 

527 

528 
(*** Simplifications of assumed implications. 

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

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

531 
intuitionistic propositional logic. See 

532 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

534 

535 
lemma conj_impE: 

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

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

538 
shows R 

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

540 

541 
lemma disj_impE: 

542 
assumes major: "(PQ)>S" 

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

544 
shows R 

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

546 

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

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

549 
lemma imp_impE: 

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

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

552 
and r2: "S ==> R" 

553 
shows R 

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

555 

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

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

558 
lemma not_impE: 

559 
assumes major: "~P > S" 

560 
and r1: "P ==> False" 

561 
and r2: "S ==> R" 

562 
shows R 

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

564 
done 

565 

566 
(*Simplifies the implication. UNSAFE. *) 

567 
lemma iff_impE: 

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

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

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

571 
and r3: "S ==> R" 

572 
shows R 

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

574 
done 

575 

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

577 
lemma all_impE: 

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

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

580 
and r2: "S ==> R" 

581 
shows R 

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

583 
done 

584 

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

586 
lemma ex_impE: 

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

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

589 
shows R 

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

591 
done 

592 

593 
(*** Courtesy of Krzysztof Grabczewski ***) 

594 

595 
lemma disj_imp_disj: 

596 
assumes major: "PQ" 

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

598 
shows "RS" 

599 
apply (rule disjE [OF major]) 

600 
apply (rule disjI1) apply assumption 

601 
apply (rule disjI2) apply assumption 

602 
done 

11734  603 

18481  604 
ML {* 
605 
structure ProjectRule = ProjectRuleFun 

606 
(struct 

22139  607 
val conjunct1 = @{thm conjunct1} 
608 
val conjunct2 = @{thm conjunct2} 

609 
val mp = @{thm mp} 

18481  610 
end) 
611 
*} 

612 

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

613 
use "fologic.ML" 
21539  614 

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

616 

9886  617 
use "hypsubstdata.ML" 
618 
setup hypsubst_setup 

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

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

620 

4092  621 

12875  622 
subsection {* Intuitionistic Reasoning *} 
12368  623 

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

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

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

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

628 
shows R 
12349  629 
proof  
630 
from 3 and 1 have P . 

12368  631 
with 1 have Q by (rule impE) 
12349  632 
with 2 show R . 
633 
qed 

634 

635 
lemma allE': 

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

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

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

638 
shows Q 
12349  639 
proof  
640 
from 1 have "P(x)" by (rule spec) 

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

642 
qed 

643 

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

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

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

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

647 
shows R 
12349  648 
proof  
649 
from 2 and 1 have P . 

650 
with 1 show R by (rule notE) 

651 
qed 

652 

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

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

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

656 
and [Pure.intro] = exI disjI2 disjI1 

657 

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

660 

12368  661 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  662 
by iprover 
12368  663 

664 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

666 

667 

13435  668 
lemma eq_commute: "a=b <> b=a" 
669 
apply (rule iffI) 

670 
apply (erule sym)+ 

671 
done 

672 

673 

11677  674 
subsection {* Atomizing metalevel rules *} 
675 

11747  676 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  677 
proof 
11677  678 
assume "!!x. P(x)" 
22931  679 
then show "ALL x. P(x)" .. 
11677  680 
next 
681 
assume "ALL x. P(x)" 

22931  682 
then show "!!x. P(x)" .. 
11677  683 
qed 
684 

11747  685 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  686 
proof 
12368  687 
assume "A ==> B" 
22931  688 
then show "A > B" .. 
11677  689 
next 
690 
assume "A > B" and A 

22931  691 
then show B by (rule mp) 
11677  692 
qed 
693 

11747  694 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  695 
proof 
11677  696 
assume "x == y" 
22931  697 
show "x = y" unfolding `x == y` by (rule refl) 
11677  698 
next 
699 
assume "x = y" 

22931  700 
then show "x == y" by (rule eq_reflection) 
11677  701 
qed 
702 

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

705 
assume "A == B" 

22931  706 
show "A <> B" unfolding `A == B` by (rule iff_refl) 
18813  707 
next 
708 
assume "A <> B" 

22931  709 
then show "A == B" by (rule iff_reflection) 
18813  710 
qed 
711 

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

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

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

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

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

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

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

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

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

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

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

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

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

727 
from conj show B .. 
11953  728 
qed 
729 
qed 

730 

12368  731 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  732 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  733 

11848  734 

735 
subsection {* Calculational rules *} 

736 

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

738 
by (rule ssubst) 

739 

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

741 
by (rule subst) 

742 

743 
text {* 

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

745 
*} 

746 

12019  747 
lemmas basic_trans_rules [trans] = 
11848  748 
forw_subst 
749 
back_subst 

750 
rev_mp 

751 
mp 

752 
trans 

753 

13779  754 
subsection {* ``Let'' declarations *} 
755 

756 
nonterminals letbinds letbind 

757 

758 
constdefs 

14854  759 
Let :: "['a::{}, 'a => 'b] => ('b::{})" 
13779  760 
"Let(s, f) == f(s)" 
761 

762 
syntax 

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

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

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

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

767 

768 
translations 

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

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

771 

772 

773 
lemma LetI: 

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

776 
apply (unfold Let_def) 

777 
apply (rule refl [THEN assms]) 

778 
done 

779 

780 

781 
subsection {* ML bindings *} 

13779  782 

21539  783 
ML {* 
22139  784 
val refl = @{thm refl} 
785 
val trans = @{thm trans} 

786 
val sym = @{thm sym} 

787 
val subst = @{thm subst} 

788 
val ssubst = @{thm ssubst} 

789 
val conjI = @{thm conjI} 

790 
val conjE = @{thm conjE} 

791 
val conjunct1 = @{thm conjunct1} 

792 
val conjunct2 = @{thm conjunct2} 

793 
val disjI1 = @{thm disjI1} 

794 
val disjI2 = @{thm disjI2} 

795 
val disjE = @{thm disjE} 

796 
val impI = @{thm impI} 

797 
val impE = @{thm impE} 

798 
val mp = @{thm mp} 

799 
val rev_mp = @{thm rev_mp} 

800 
val TrueI = @{thm TrueI} 

801 
val FalseE = @{thm FalseE} 

802 
val iff_refl = @{thm iff_refl} 

803 
val iff_trans = @{thm iff_trans} 

804 
val iffI = @{thm iffI} 

805 
val iffE = @{thm iffE} 

806 
val iffD1 = @{thm iffD1} 

807 
val iffD2 = @{thm iffD2} 

808 
val notI = @{thm notI} 

809 
val notE = @{thm notE} 

810 
val allI = @{thm allI} 

811 
val allE = @{thm allE} 

812 
val spec = @{thm spec} 

813 
val exI = @{thm exI} 

814 
val exE = @{thm exE} 

815 
val eq_reflection = @{thm eq_reflection} 

816 
val iff_reflection = @{thm iff_reflection} 

817 
val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} 

818 
val meta_eq_to_iff = @{thm meta_eq_to_iff} 

13779  819 
*} 
820 

4854  821 
end 