author  blanchet 
Mon, 26 Nov 2012 13:35:05 +0100  
changeset 50222  40e3c3be6bca 
parent 49339  d1fcb4de8349 
child 51798  ad3a241def73 
permissions  rwrr 
1268  1 
(* Title: FOL/IFOL.thy 
11677  2 
Author: Lawrence C Paulson and Markus Wenzel 
3 
*) 

35  4 

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

15481  7 
theory IFOL 
8 
imports Pure 

9 
begin 

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

10 

48891  11 
ML_file "~~/src/Tools/misc_legacy.ML" 
12 
ML_file "~~/src/Provers/splitter.ML" 

13 
ML_file "~~/src/Provers/hypsubst.ML" 

14 
ML_file "~~/src/Tools/IsaPlanner/zipper.ML" 

15 
ML_file "~~/src/Tools/IsaPlanner/isand.ML" 

16 
ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" 

17 
ML_file "~~/src/Tools/eqsubst.ML" 

18 
ML_file "~~/src/Provers/quantifier1.ML" 

19 
ML_file "~~/src/Tools/intuitionistic.ML" 

20 
ML_file "~~/src/Tools/project_rule.ML" 

21 
ML_file "~~/src/Tools/atomize_elim.ML" 

22 

0  23 

11677  24 
subsection {* Syntax and axiomatic basis *} 
25 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

26 
setup Pure_Thy.old_appl_syntax_setup 
26956
1309a6a0a29f
setup PureThy.old_appl_syntax_setup  theory Pure provides regular application syntax by default;
wenzelm
parents:
26580
diff
changeset

27 

14854  28 
classes "term" 
36452  29 
default_sort "term" 
0  30 

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

31 
typedecl o 
79  32 

11747  33 
judgment 
34 
Trueprop :: "o => prop" ("(_)" 5) 

0  35 

79  36 

46972  37 
subsubsection {* Equality *} 
35  38 

46972  39 
axiomatization 
40 
eq :: "['a, 'a] => o" (infixl "=" 50) 

41 
where 

42 
refl: "a=a" and 

43 
subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" 

79  44 

0  45 

46972  46 
subsubsection {* Propositional logic *} 
47 

48 
axiomatization 

49 
False :: o and 

50 
conj :: "[o, o] => o" (infixr "&" 35) and 

51 
disj :: "[o, o] => o" (infixr "" 30) and 

52 
imp :: "[o, o] => o" (infixr ">" 25) 

53 
where 

54 
conjI: "[ P; Q ] ==> P&Q" and 

55 
conjunct1: "P&Q ==> P" and 

56 
conjunct2: "P&Q ==> Q" and 

57 

58 
disjI1: "P ==> PQ" and 

59 
disjI2: "Q ==> PQ" and 

60 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" and 

61 

62 
impI: "(P ==> Q) ==> P>Q" and 

63 
mp: "[ P>Q; P ] ==> Q" and 

64 

65 
FalseE: "False ==> P" 

66 

67 

68 
subsubsection {* Quantifiers *} 

69 

70 
axiomatization 

71 
All :: "('a => o) => o" (binder "ALL " 10) and 

72 
Ex :: "('a => o) => o" (binder "EX " 10) 

73 
where 

74 
allI: "(!!x. P(x)) ==> (ALL x. P(x))" and 

75 
spec: "(ALL x. P(x)) ==> P(x)" and 

76 
exI: "P(x) ==> (EX x. P(x))" and 

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

78 

79 

80 
subsubsection {* Definitions *} 

81 

82 
definition "True == False>False" 

83 
definition Not ("~ _" [40] 40) where not_def: "~P == P>False" 

84 
definition iff (infixr "<>" 25) where "P<>Q == (P>Q) & (Q>P)" 

85 

86 
definition Ex1 :: "('a => o) => o" (binder "EX! " 10) 

87 
where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)" 

88 

89 
axiomatization where  {* Reflection, admissible *} 

90 
eq_reflection: "(x=y) ==> (x==y)" and 

91 
iff_reflection: "(P<>Q) ==> (P==Q)" 

92 

93 

94 
subsubsection {* Additional notation *} 

95 

96 
abbreviation not_equal :: "['a, 'a] => o" (infixl "~=" 50) 

97 
where "x ~= y == ~ (x = y)" 

79  98 

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

100 
not_equal (infixl "\<noteq>" 50) 
19363  101 

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

103 
not_equal (infixl "\<noteq>" 50) 
19363  104 

21524  105 
notation (xsymbols) 
46972  106 
Not ("\<not> _" [40] 40) and 
107 
conj (infixr "\<and>" 35) and 

108 
disj (infixr "\<or>" 30) and 

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

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

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

112 
imp (infixr "\<longrightarrow>" 25) and 

113 
iff (infixr "\<longleftrightarrow>" 25) 

35  114 

21524  115 
notation (HTML output) 
46972  116 
Not ("\<not> _" [40] 40) and 
117 
conj (infixr "\<and>" 35) and 

118 
disj (infixr "\<or>" 30) and 

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

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

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

14236  122 

13779  123 

11677  124 
subsection {* Lemmas and proof tools *} 
125 

46972  126 
lemmas strip = impI allI 
127 

21539  128 
lemma TrueI: True 
129 
unfolding True_def by (rule impI) 

130 

131 

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

133 

134 
lemma conjE: 

135 
assumes major: "P & Q" 

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

137 
shows R 

138 
apply (rule r) 

139 
apply (rule major [THEN conjunct1]) 

140 
apply (rule major [THEN conjunct2]) 

141 
done 

142 

143 
lemma impE: 

144 
assumes major: "P > Q" 

145 
and P 

146 
and r: "Q ==> R" 

147 
shows R 

148 
apply (rule r) 

149 
apply (rule major [THEN mp]) 

150 
apply (rule `P`) 

151 
done 

152 

153 
lemma allE: 

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

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

156 
shows R 

157 
apply (rule r) 

158 
apply (rule major [THEN spec]) 

159 
done 

160 

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

162 
lemma all_dupE: 

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

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

165 
shows R 

166 
apply (rule r) 

167 
apply (rule major [THEN spec]) 

168 
apply (rule major) 

169 
done 

170 

171 

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

173 

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

175 
unfolding not_def by (erule impI) 

176 

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

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

179 

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

181 
by (erule notE) 

182 

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

184 
lemma not_to_imp: 

185 
assumes "~P" 

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

187 
shows Q 

188 
apply (rule r) 

189 
apply (rule impI) 

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

191 
done 

192 

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

27150  194 
this implication, then apply impI to move P back into the assumptions.*) 
21539  195 
lemma rev_mp: "[ P; P > Q ] ==> Q" 
196 
by (erule mp) 

197 

198 
(*Contrapositive of an inference rule*) 

199 
lemma contrapos: 

200 
assumes major: "~Q" 

201 
and minor: "P ==> Q" 

202 
shows "~P" 

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

204 
apply (erule minor) 

205 
done 

206 

207 

208 
(*** Modus Ponens Tactics ***) 

209 

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

211 
ML {* 

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

21539  214 
*} 
215 

216 

217 
(*** Ifandonlyif ***) 

218 

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

220 
apply (unfold iff_def) 

221 
apply (rule conjI) 

222 
apply (erule impI) 

223 
apply (erule impI) 

224 
done 

225 

226 

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

228 
lemma iffE: 

229 
assumes major: "P <> Q" 

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

231 
shows R 

232 
apply (insert major, unfold iff_def) 

233 
apply (erule conjE) 

234 
apply (erule r) 

235 
apply assumption 

236 
done 

237 

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

239 

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

241 
apply (unfold iff_def) 

242 
apply (erule conjunct1 [THEN mp]) 

243 
apply assumption 

244 
done 

245 

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

247 
apply (unfold iff_def) 

248 
apply (erule conjunct2 [THEN mp]) 

249 
apply assumption 

250 
done 

251 

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

253 
apply (erule iffD1) 

254 
apply assumption 

255 
done 

256 

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

258 
apply (erule iffD2) 

259 
apply assumption 

260 
done 

261 

262 
lemma iff_refl: "P <> P" 

263 
by (rule iffI) 

264 

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

266 
apply (erule iffE) 

267 
apply (rule iffI) 

268 
apply (assumption  erule mp)+ 

269 
done 

270 

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

272 
apply (rule iffI) 

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

274 
done 

275 

276 

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

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

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

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

281 
***) 

282 

283 
lemma ex1I: 

23393  284 
"P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)" 
21539  285 
apply (unfold ex1_def) 
23393  286 
apply (assumption  rule exI conjI allI impI)+ 
21539  287 
done 
288 

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

290 
lemma ex_ex1I: 

23393  291 
"EX x. P(x) \<Longrightarrow> (!!x y. [ P(x); P(y) ] ==> x=y) \<Longrightarrow> EX! x. P(x)" 
292 
apply (erule exE) 

293 
apply (rule ex1I) 

294 
apply assumption 

295 
apply assumption 

21539  296 
done 
297 

298 
lemma ex1E: 

23393  299 
"EX! x. P(x) \<Longrightarrow> (!!x. [ P(x); ALL y. P(y) > y=x ] ==> R) \<Longrightarrow> R" 
300 
apply (unfold ex1_def) 

21539  301 
apply (assumption  erule exE conjE)+ 
302 
done 

303 

304 

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

306 

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

308 
ML {* 

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

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

21539  312 
*} 
313 

314 
lemma conj_cong: 

315 
assumes "P <> P'" 

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

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

318 
apply (insert assms) 

319 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  320 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  321 
done 
322 

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

324 
lemma conj_cong2: 

325 
assumes "P <> P'" 

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

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

328 
apply (insert assms) 

329 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  330 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  331 
done 
332 

333 
lemma disj_cong: 

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

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

336 
apply (insert assms) 

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

338 
done 

339 

340 
lemma imp_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 impI  erule iffE  erule (1) notE impE  

39159  346 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  347 
done 
348 

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

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

351 
done 

352 

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

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

355 
done 

356 

357 
lemma all_cong: 

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

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

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

39159  361 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  362 
done 
363 

364 
lemma ex_cong: 

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

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

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

39159  368 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  369 
done 
370 

371 
lemma ex1_cong: 

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

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

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

39159  375 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  376 
done 
377 

378 
(*** Equality rules ***) 

379 

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

381 
apply (erule subst) 

382 
apply (rule refl) 

383 
done 

384 

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

386 
apply (erule subst, assumption) 

387 
done 

388 

389 
(** **) 

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

391 
apply (erule contrapos) 

392 
apply (erule sym) 

393 
done 

394 

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

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

397 

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

399 
apply unfold 

400 
apply (rule iff_refl) 

401 
done 

402 

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

404 
apply unfold 

405 
apply (rule refl) 

406 
done 

407 

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

409 
by unfold (rule iff_refl) 

410 

411 
(*substitution*) 

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

413 
apply (drule sym) 

414 
apply (erule (1) subst) 

415 
done 

416 

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

418 
lemma ex1_equalsE: 

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

420 
apply (erule ex1E) 

421 
apply (rule trans) 

422 
apply (rule_tac [2] sym) 

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

424 
done 

425 

426 
(** Polymorphic congruence rules **) 

427 

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

429 
apply (erule ssubst) 

430 
apply (rule refl) 

431 
done 

432 

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

434 
apply (erule ssubst)+ 

435 
apply (rule refl) 

436 
done 

437 

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

439 
apply (erule ssubst)+ 

440 
apply (rule refl) 

441 
done 

442 

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

444 
a = b 

445 
  

446 
c = d *) 

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

448 
apply (rule trans) 

449 
apply (rule trans) 

450 
apply (rule sym) 

451 
apply assumption+ 

452 
done 

453 

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

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

456 
apply (rule trans) 

457 
apply (rule trans) 

458 
apply assumption+ 

459 
apply (erule sym) 

460 
done 

461 

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

463 

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

465 
apply (rule iffI) 

466 
apply (erule (1) subst) 

467 
apply (erule (1) ssubst) 

468 
done 

469 

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

471 
apply (rule iffI) 

472 
apply (erule subst)+ 

473 
apply assumption 

474 
apply (erule ssubst)+ 

475 
apply assumption 

476 
done 

477 

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

479 
apply (rule iffI) 

480 
apply (erule subst)+ 

481 
apply assumption 

482 
apply (erule ssubst)+ 

483 
apply assumption 

484 
done 

485 

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

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

488 
apply (erule (1) pred2_cong) 

489 
done 

490 

491 

492 
(*** Simplifications of assumed implications. 

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

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

495 
intuitionistic propositional logic. See 

496 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

498 

499 
lemma conj_impE: 

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

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

502 
shows R 

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

504 

505 
lemma disj_impE: 

506 
assumes major: "(PQ)>S" 

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

508 
shows R 

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

510 

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

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

513 
lemma imp_impE: 

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

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

516 
and r2: "S ==> R" 

517 
shows R 

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

519 

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

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

522 
lemma not_impE: 

23393  523 
"~P > S \<Longrightarrow> (P ==> False) \<Longrightarrow> (S ==> R) \<Longrightarrow> R" 
524 
apply (drule mp) 

525 
apply (rule notI) 

526 
apply assumption 

527 
apply assumption 

21539  528 
done 
529 

530 
(*Simplifies the implication. UNSAFE. *) 

531 
lemma iff_impE: 

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

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

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

535 
and r3: "S ==> R" 

536 
shows R 

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

538 
done 

539 

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

541 
lemma all_impE: 

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

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

544 
and r2: "S ==> R" 

545 
shows R 

23393  546 
apply (rule allI impI major [THEN mp] r1 r2)+ 
21539  547 
done 
548 

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

550 
lemma ex_impE: 

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

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

553 
shows R 

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

555 
done 

556 

557 
(*** Courtesy of Krzysztof Grabczewski ***) 

558 

559 
lemma disj_imp_disj: 

23393  560 
"PQ \<Longrightarrow> (P==>R) \<Longrightarrow> (Q==>S) \<Longrightarrow> RS" 
561 
apply (erule disjE) 

21539  562 
apply (rule disjI1) apply assumption 
563 
apply (rule disjI2) apply assumption 

564 
done 

11734  565 

18481  566 
ML {* 
32172  567 
structure Project_Rule = Project_Rule 
568 
( 

22139  569 
val conjunct1 = @{thm conjunct1} 
570 
val conjunct2 = @{thm conjunct2} 

571 
val mp = @{thm mp} 

32172  572 
) 
18481  573 
*} 
574 

48891  575 
ML_file "fologic.ML" 
21539  576 

42303  577 
lemma thin_refl: "[x=x; PROP W] ==> PROP W" . 
21539  578 

42799  579 
ML {* 
580 
structure Hypsubst = Hypsubst 

581 
( 

582 
val dest_eq = FOLogic.dest_eq 

583 
val dest_Trueprop = FOLogic.dest_Trueprop 

584 
val dest_imp = FOLogic.dest_imp 

585 
val eq_reflection = @{thm eq_reflection} 

586 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

587 
val imp_intr = @{thm impI} 

588 
val rev_mp = @{thm rev_mp} 

589 
val subst = @{thm subst} 

590 
val sym = @{thm sym} 

591 
val thin_refl = @{thm thin_refl} 

592 
); 

593 
open Hypsubst; 

594 
*} 

595 

9886  596 
setup hypsubst_setup 
48891  597 
ML_file "intprover.ML" 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

598 

4092  599 

12875  600 
subsection {* Intuitionistic Reasoning *} 
12368  601 

31299  602 
setup {* Intuitionistic.method_setup @{binding iprover} *} 
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

603 

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

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

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

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

608 
shows R 
12349  609 
proof  
610 
from 3 and 1 have P . 

12368  611 
with 1 have Q by (rule impE) 
12349  612 
with 2 show R . 
613 
qed 

614 

615 
lemma allE': 

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

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

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

618 
shows Q 
12349  619 
proof  
620 
from 1 have "P(x)" by (rule spec) 

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

622 
qed 

623 

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

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

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

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

627 
shows R 
12349  628 
proof  
629 
from 2 and 1 have P . 

630 
with 1 show R by (rule notE) 

631 
qed 

632 

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

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

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

636 
and [Pure.intro] = exI disjI2 disjI1 

637 

33369  638 
setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *} 
12349  639 

640 

12368  641 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  642 
by iprover 
12368  643 

644 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

646 

647 

13435  648 
lemma eq_commute: "a=b <> b=a" 
649 
apply (rule iffI) 

650 
apply (erule sym)+ 

651 
done 

652 

653 

11677  654 
subsection {* Atomizing metalevel rules *} 
655 

11747  656 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  657 
proof 
11677  658 
assume "!!x. P(x)" 
22931  659 
then show "ALL x. P(x)" .. 
11677  660 
next 
661 
assume "ALL x. P(x)" 

22931  662 
then show "!!x. P(x)" .. 
11677  663 
qed 
664 

11747  665 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  666 
proof 
12368  667 
assume "A ==> B" 
22931  668 
then show "A > B" .. 
11677  669 
next 
670 
assume "A > B" and A 

22931  671 
then show B by (rule mp) 
11677  672 
qed 
673 

11747  674 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  675 
proof 
11677  676 
assume "x == y" 
22931  677 
show "x = y" unfolding `x == y` by (rule refl) 
11677  678 
next 
679 
assume "x = y" 

22931  680 
then show "x == y" by (rule eq_reflection) 
11677  681 
qed 
682 

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

685 
assume "A == B" 

22931  686 
show "A <> B" unfolding `A == B` by (rule iff_refl) 
18813  687 
next 
688 
assume "A <> B" 

22931  689 
then show "A == B" by (rule iff_reflection) 
18813  690 
qed 
691 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

692 
lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)" 
11976  693 
proof 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

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

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

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

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

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

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

701 
assume conj: "A & B" 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

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

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

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

705 
from conj show B .. 
11953  706 
qed 
707 
qed 

708 

12368  709 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  710 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  711 

11848  712 

26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

713 
subsection {* Atomizing elimination rules *} 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

714 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

715 
setup AtomizeElim.setup 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

716 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

717 
lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

718 
by rule iprover+ 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

719 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

720 
lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

721 
by rule iprover+ 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

722 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

723 
lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A  B ==> C) ==> C)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

724 
by rule iprover+ 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

725 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

726 
lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" .. 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

727 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

728 

11848  729 
subsection {* Calculational rules *} 
730 

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

732 
by (rule ssubst) 

733 

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

735 
by (rule subst) 

736 

737 
text {* 

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

739 
*} 

740 

12019  741 
lemmas basic_trans_rules [trans] = 
11848  742 
forw_subst 
743 
back_subst 

744 
rev_mp 

745 
mp 

746 
trans 

747 

13779  748 
subsection {* ``Let'' declarations *} 
749 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
39557
diff
changeset

750 
nonterminal letbinds and letbind 
13779  751 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

752 
definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where 
13779  753 
"Let(s, f) == f(s)" 
754 

755 
syntax 

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

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

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

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

760 

761 
translations 

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

35054  763 
"let x = a in e" == "CONST Let(a, %x. e)" 
13779  764 

765 

766 
lemma LetI: 

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

769 
apply (unfold Let_def) 

770 
apply (rule refl [THEN assms]) 

771 
done 

772 

773 

26286  774 
subsection {* Intuitionistic simplification rules *} 
775 

776 
lemma conj_simps: 

777 
"P & True <> P" 

778 
"True & P <> P" 

779 
"P & False <> False" 

780 
"False & P <> False" 

781 
"P & P <> P" 

782 
"P & P & Q <> P & Q" 

783 
"P & ~P <> False" 

784 
"~P & P <> False" 

785 
"(P & Q) & R <> P & (Q & R)" 

786 
by iprover+ 

787 

788 
lemma disj_simps: 

789 
"P  True <> True" 

790 
"True  P <> True" 

791 
"P  False <> P" 

792 
"False  P <> P" 

793 
"P  P <> P" 

794 
"P  P  Q <> P  Q" 

795 
"(P  Q)  R <> P  (Q  R)" 

796 
by iprover+ 

797 

798 
lemma not_simps: 

799 
"~(PQ) <> ~P & ~Q" 

800 
"~ False <> True" 

801 
"~ True <> False" 

802 
by iprover+ 

803 

804 
lemma imp_simps: 

805 
"(P > False) <> ~P" 

806 
"(P > True) <> True" 

807 
"(False > P) <> True" 

808 
"(True > P) <> P" 

809 
"(P > P) <> True" 

810 
"(P > ~P) <> ~P" 

811 
by iprover+ 

812 

813 
lemma iff_simps: 

814 
"(True <> P) <> P" 

815 
"(P <> True) <> P" 

816 
"(P <> P) <> True" 

817 
"(False <> P) <> ~P" 

818 
"(P <> False) <> ~P" 

819 
by iprover+ 

820 

821 
(*The x=t versions are needed for the simplification procedures*) 

822 
lemma quant_simps: 

823 
"!!P. (ALL x. P) <> P" 

824 
"(ALL x. x=t > P(x)) <> P(t)" 

825 
"(ALL x. t=x > P(x)) <> P(t)" 

826 
"!!P. (EX x. P) <> P" 

827 
"EX x. x=t" 

828 
"EX x. t=x" 

829 
"(EX x. x=t & P(x)) <> P(t)" 

830 
"(EX x. t=x & P(x)) <> P(t)" 

831 
by iprover+ 

832 

833 
(*These are NOT supplied by default!*) 

834 
lemma distrib_simps: 

835 
"P & (Q  R) <> P&Q  P&R" 

836 
"(Q  R) & P <> Q&P  R&P" 

837 
"(P  Q > R) <> (P > R) & (Q > R)" 

838 
by iprover+ 

839 

840 

841 
text {* Conversion into rewrite rules *} 

842 

843 
lemma P_iff_F: "~P ==> (P <> False)" by iprover 

844 
lemma iff_reflection_F: "~P ==> (P == False)" by (rule P_iff_F [THEN iff_reflection]) 

845 

846 
lemma P_iff_T: "P ==> (P <> True)" by iprover 

847 
lemma iff_reflection_T: "P ==> (P == True)" by (rule P_iff_T [THEN iff_reflection]) 

848 

849 

850 
text {* More rewrite rules *} 

851 

852 
lemma conj_commute: "P&Q <> Q&P" by iprover 

853 
lemma conj_left_commute: "P&(Q&R) <> Q&(P&R)" by iprover 

854 
lemmas conj_comms = conj_commute conj_left_commute 

855 

856 
lemma disj_commute: "PQ <> QP" by iprover 

857 
lemma disj_left_commute: "P(QR) <> Q(PR)" by iprover 

858 
lemmas disj_comms = disj_commute disj_left_commute 

859 

860 
lemma conj_disj_distribL: "P&(QR) <> (P&Q  P&R)" by iprover 

861 
lemma conj_disj_distribR: "(PQ)&R <> (P&R  Q&R)" by iprover 

862 

863 
lemma disj_conj_distribL: "P(Q&R) <> (PQ) & (PR)" by iprover 

864 
lemma disj_conj_distribR: "(P&Q)R <> (PR) & (QR)" by iprover 

865 

866 
lemma imp_conj_distrib: "(P > (Q&R)) <> (P>Q) & (P>R)" by iprover 

867 
lemma imp_conj: "((P&Q)>R) <> (P > (Q > R))" by iprover 

868 
lemma imp_disj: "(PQ > R) <> (P>R) & (Q>R)" by iprover 

869 

870 
lemma de_Morgan_disj: "(~(P  Q)) <> (~P & ~Q)" by iprover 

871 

872 
lemma not_ex: "(~ (EX x. P(x))) <> (ALL x.~P(x))" by iprover 

873 
lemma imp_ex: "((EX x. P(x)) > Q) <> (ALL x. P(x) > Q)" by iprover 

874 

875 
lemma ex_disj_distrib: 

876 
"(EX x. P(x)  Q(x)) <> ((EX x. P(x))  (EX x. Q(x)))" by iprover 

877 

878 
lemma all_conj_distrib: 

879 
"(ALL x. P(x) & Q(x)) <> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover 

880 

4854  881 
end 