author  wenzelm 
Thu, 06 Mar 2014 19:55:08 +0100  
changeset 55960  beef468837b1 
parent 55380  4de48353034e 
child 57948  75724d71013c 
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/Provers/quantifier1.ML" 

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

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

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

21 

0  22 

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

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

25 
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

26 

55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
52241
diff
changeset

27 
class "term" 
36452  28 
default_sort "term" 
0  29 

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

30 
typedecl o 
79  31 

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

0  34 

79  35 

46972  36 
subsubsection {* Equality *} 
35  37 

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

40 
where 

41 
refl: "a=a" and 

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

79  43 

0  44 

46972  45 
subsubsection {* Propositional logic *} 
46 

47 
axiomatization 

48 
False :: o and 

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

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

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

52 
where 

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

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

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

56 

57 
disjI1: "P ==> PQ" and 

58 
disjI2: "Q ==> PQ" and 

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

60 

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

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

63 

64 
FalseE: "False ==> P" 

65 

66 

67 
subsubsection {* Quantifiers *} 

68 

69 
axiomatization 

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

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

72 
where 

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

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

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

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

77 

78 

79 
subsubsection {* Definitions *} 

80 

81 
definition "True == False>False" 

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

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

84 

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

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

87 

88 
axiomatization where  {* Reflection, admissible *} 

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

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

91 

92 

93 
subsubsection {* Additional notation *} 

94 

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

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

79  97 

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

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

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

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

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

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

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

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

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

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

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

35  113 

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

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

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

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

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

14236  121 

13779  122 

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

46972  125 
lemmas strip = impI allI 
126 

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

129 

130 

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

132 

133 
lemma conjE: 

134 
assumes major: "P & Q" 

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

136 
shows R 

137 
apply (rule r) 

138 
apply (rule major [THEN conjunct1]) 

139 
apply (rule major [THEN conjunct2]) 

140 
done 

141 

142 
lemma impE: 

143 
assumes major: "P > Q" 

144 
and P 

145 
and r: "Q ==> R" 

146 
shows R 

147 
apply (rule r) 

148 
apply (rule major [THEN mp]) 

149 
apply (rule `P`) 

150 
done 

151 

152 
lemma allE: 

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

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

155 
shows R 

156 
apply (rule r) 

157 
apply (rule major [THEN spec]) 

158 
done 

159 

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

161 
lemma all_dupE: 

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

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

164 
shows R 

165 
apply (rule r) 

166 
apply (rule major [THEN spec]) 

167 
apply (rule major) 

168 
done 

169 

170 

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

172 

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

174 
unfolding not_def by (erule impI) 

175 

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

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

178 

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

180 
by (erule notE) 

181 

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

183 
lemma not_to_imp: 

184 
assumes "~P" 

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

186 
shows Q 

187 
apply (rule r) 

188 
apply (rule impI) 

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

190 
done 

191 

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

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

196 

197 
(*Contrapositive of an inference rule*) 

198 
lemma contrapos: 

199 
assumes major: "~Q" 

200 
and minor: "P ==> Q" 

201 
shows "~P" 

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

203 
apply (erule minor) 

204 
done 

205 

206 

207 
(*** Modus Ponens Tactics ***) 

208 

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

210 
ML {* 

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

21539  213 
*} 
214 

215 

216 
(*** Ifandonlyif ***) 

217 

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

219 
apply (unfold iff_def) 

220 
apply (rule conjI) 

221 
apply (erule impI) 

222 
apply (erule impI) 

223 
done 

224 

225 

226 
lemma iffE: 

227 
assumes major: "P <> Q" 

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

229 
shows R 

230 
apply (insert major, unfold iff_def) 

231 
apply (erule conjE) 

232 
apply (erule r) 

233 
apply assumption 

234 
done 

235 

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

237 

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

239 
apply (unfold iff_def) 

240 
apply (erule conjunct1 [THEN mp]) 

241 
apply assumption 

242 
done 

243 

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

245 
apply (unfold iff_def) 

246 
apply (erule conjunct2 [THEN mp]) 

247 
apply assumption 

248 
done 

249 

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

251 
apply (erule iffD1) 

252 
apply assumption 

253 
done 

254 

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

256 
apply (erule iffD2) 

257 
apply assumption 

258 
done 

259 

260 
lemma iff_refl: "P <> P" 

261 
by (rule iffI) 

262 

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

264 
apply (erule iffE) 

265 
apply (rule iffI) 

266 
apply (assumption  erule mp)+ 

267 
done 

268 

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

270 
apply (rule iffI) 

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

272 
done 

273 

274 

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

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

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

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

279 
***) 

280 

281 
lemma ex1I: 

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

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

288 
lemma ex_ex1I: 

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

291 
apply (rule ex1I) 

292 
apply assumption 

293 
apply assumption 

21539  294 
done 
295 

296 
lemma ex1E: 

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

21539  299 
apply (assumption  erule exE conjE)+ 
300 
done 

301 

302 

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

304 

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

306 
ML {* 

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

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

21539  310 
*} 
311 

312 
lemma conj_cong: 

313 
assumes "P <> P'" 

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

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

316 
apply (insert assms) 

317 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  318 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  319 
done 
320 

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

322 
lemma conj_cong2: 

323 
assumes "P <> P'" 

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

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

326 
apply (insert assms) 

327 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  328 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  329 
done 
330 

331 
lemma disj_cong: 

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

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

334 
apply (insert assms) 

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

336 
done 

337 

338 
lemma imp_cong: 

339 
assumes "P <> P'" 

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

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

342 
apply (insert assms) 

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

39159  344 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  345 
done 
346 

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

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

349 
done 

350 

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

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

353 
done 

354 

355 
lemma all_cong: 

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

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

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

39159  359 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  360 
done 
361 

362 
lemma ex_cong: 

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

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

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

39159  366 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  367 
done 
368 

369 
lemma ex1_cong: 

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

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

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

39159  373 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  374 
done 
375 

376 
(*** Equality rules ***) 

377 

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

379 
apply (erule subst) 

380 
apply (rule refl) 

381 
done 

382 

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

384 
apply (erule subst, assumption) 

385 
done 

386 

387 
(** **) 

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

389 
apply (erule contrapos) 

390 
apply (erule sym) 

391 
done 

392 

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

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

395 

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

397 
apply unfold 

398 
apply (rule iff_refl) 

399 
done 

400 

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

402 
apply unfold 

403 
apply (rule refl) 

404 
done 

405 

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

407 
by unfold (rule iff_refl) 

408 

409 
(*substitution*) 

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

411 
apply (drule sym) 

412 
apply (erule (1) subst) 

413 
done 

414 

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

416 
lemma ex1_equalsE: 

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

418 
apply (erule ex1E) 

419 
apply (rule trans) 

420 
apply (rule_tac [2] sym) 

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

422 
done 

423 

424 
(** Polymorphic congruence rules **) 

425 

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

427 
apply (erule ssubst) 

428 
apply (rule refl) 

429 
done 

430 

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

432 
apply (erule ssubst)+ 

433 
apply (rule refl) 

434 
done 

435 

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

437 
apply (erule ssubst)+ 

438 
apply (rule refl) 

439 
done 

440 

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

442 
a = b 

443 
  

444 
c = d *) 

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

446 
apply (rule trans) 

447 
apply (rule trans) 

448 
apply (rule sym) 

449 
apply assumption+ 

450 
done 

451 

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

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

454 
apply (rule trans) 

455 
apply (rule trans) 

456 
apply assumption+ 

457 
apply (erule sym) 

458 
done 

459 

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

461 

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

463 
apply (rule iffI) 

464 
apply (erule (1) subst) 

465 
apply (erule (1) ssubst) 

466 
done 

467 

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

469 
apply (rule iffI) 

470 
apply (erule subst)+ 

471 
apply assumption 

472 
apply (erule ssubst)+ 

473 
apply assumption 

474 
done 

475 

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

477 
apply (rule iffI) 

478 
apply (erule subst)+ 

479 
apply assumption 

480 
apply (erule ssubst)+ 

481 
apply assumption 

482 
done 

483 

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

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

486 
apply (erule (1) pred2_cong) 

487 
done 

488 

489 

490 
(*** Simplifications of assumed implications. 

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

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

493 
intuitionistic propositional logic. See 

494 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

496 

497 
lemma conj_impE: 

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

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

500 
shows R 

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

502 

503 
lemma disj_impE: 

504 
assumes major: "(PQ)>S" 

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

506 
shows R 

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

508 

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

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

511 
lemma imp_impE: 

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

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

514 
and r2: "S ==> R" 

515 
shows R 

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

517 

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

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

520 
lemma not_impE: 

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

523 
apply (rule notI) 

524 
apply assumption 

525 
apply assumption 

21539  526 
done 
527 

528 
(*Simplifies the implication. UNSAFE. *) 

529 
lemma iff_impE: 

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

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

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

533 
and r3: "S ==> R" 

534 
shows R 

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

536 
done 

537 

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

539 
lemma all_impE: 

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

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

542 
and r2: "S ==> R" 

543 
shows R 

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

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

548 
lemma ex_impE: 

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

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

551 
shows R 

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

553 
done 

554 

555 
(*** Courtesy of Krzysztof Grabczewski ***) 

556 

557 
lemma disj_imp_disj: 

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

21539  560 
apply (rule disjI1) apply assumption 
561 
apply (rule disjI2) apply assumption 

562 
done 

11734  563 

18481  564 
ML {* 
32172  565 
structure Project_Rule = Project_Rule 
566 
( 

22139  567 
val conjunct1 = @{thm conjunct1} 
568 
val conjunct2 = @{thm conjunct2} 

569 
val mp = @{thm mp} 

32172  570 
) 
18481  571 
*} 
572 

48891  573 
ML_file "fologic.ML" 
21539  574 

42303  575 
lemma thin_refl: "[x=x; PROP W] ==> PROP W" . 
21539  576 

42799  577 
ML {* 
578 
structure Hypsubst = Hypsubst 

579 
( 

580 
val dest_eq = FOLogic.dest_eq 

581 
val dest_Trueprop = FOLogic.dest_Trueprop 

582 
val dest_imp = FOLogic.dest_imp 

583 
val eq_reflection = @{thm eq_reflection} 

584 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

585 
val imp_intr = @{thm impI} 

586 
val rev_mp = @{thm rev_mp} 

587 
val subst = @{thm subst} 

588 
val sym = @{thm sym} 

589 
val thin_refl = @{thm thin_refl} 

590 
); 

591 
open Hypsubst; 

592 
*} 

593 

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

596 

4092  597 

12875  598 
subsection {* Intuitionistic Reasoning *} 
12368  599 

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

601 

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

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

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

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

606 
shows R 
12349  607 
proof  
608 
from 3 and 1 have P . 

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

612 

613 
lemma allE': 

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

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

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

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

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

620 
qed 

621 

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

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

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

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

625 
shows R 
12349  626 
proof  
627 
from 2 and 1 have P . 

628 
with 1 show R by (rule notE) 

629 
qed 

630 

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

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

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

634 
and [Pure.intro] = exI disjI2 disjI1 

635 

51798  636 
setup {* Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) *} 
12349  637 

638 

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

642 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

644 

645 

13435  646 
lemma eq_commute: "a=b <> b=a" 
647 
apply (rule iffI) 

648 
apply (erule sym)+ 

649 
done 

650 

651 

11677  652 
subsection {* Atomizing metalevel rules *} 
653 

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

22931  660 
then show "!!x. P(x)" .. 
11677  661 
qed 
662 

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

22931  669 
then show B by (rule mp) 
11677  670 
qed 
671 

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

22931  678 
then show "x == y" by (rule eq_reflection) 
11677  679 
qed 
680 

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

683 
assume "A == B" 

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

22931  687 
then show "A == B" by (rule iff_reflection) 
18813  688 
qed 
689 

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

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

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

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

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

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

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

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

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

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

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

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

703 
from conj show B .. 
11953  704 
qed 
705 
qed 

706 

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

11848  710 

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

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

712 

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

713 
setup AtomizeElim.setup 
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 
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

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

717 

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

718 
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

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

720 

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

721 
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

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

723 

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

724 
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

725 

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

726 

11848  727 
subsection {* Calculational rules *} 
728 

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

730 
by (rule ssubst) 

731 

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

733 
by (rule subst) 

734 

735 
text {* 

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

737 
*} 

738 

12019  739 
lemmas basic_trans_rules [trans] = 
11848  740 
forw_subst 
741 
back_subst 

742 
rev_mp 

743 
mp 

744 
trans 

745 

13779  746 
subsection {* ``Let'' declarations *} 
747 

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

748 
nonterminal letbinds and letbind 
13779  749 

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

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

753 
syntax 

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

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

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

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

758 

759 
translations 

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

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

763 

764 
lemma LetI: 

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

767 
apply (unfold Let_def) 

768 
apply (rule refl [THEN assms]) 

769 
done 

770 

771 

26286  772 
subsection {* Intuitionistic simplification rules *} 
773 

774 
lemma conj_simps: 

775 
"P & True <> P" 

776 
"True & P <> P" 

777 
"P & False <> False" 

778 
"False & P <> False" 

779 
"P & P <> P" 

780 
"P & P & Q <> P & Q" 

781 
"P & ~P <> False" 

782 
"~P & P <> False" 

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

784 
by iprover+ 

785 

786 
lemma disj_simps: 

787 
"P  True <> True" 

788 
"True  P <> True" 

789 
"P  False <> P" 

790 
"False  P <> P" 

791 
"P  P <> P" 

792 
"P  P  Q <> P  Q" 

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

794 
by iprover+ 

795 

796 
lemma not_simps: 

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

798 
"~ False <> True" 

799 
"~ True <> False" 

800 
by iprover+ 

801 

802 
lemma imp_simps: 

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

804 
"(P > True) <> True" 

805 
"(False > P) <> True" 

806 
"(True > P) <> P" 

807 
"(P > P) <> True" 

808 
"(P > ~P) <> ~P" 

809 
by iprover+ 

810 

811 
lemma iff_simps: 

812 
"(True <> P) <> P" 

813 
"(P <> True) <> P" 

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

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

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

817 
by iprover+ 

818 

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

820 
lemma quant_simps: 

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

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

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

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

825 
"EX x. x=t" 

826 
"EX x. t=x" 

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

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

829 
by iprover+ 

830 

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

832 
lemma distrib_simps: 

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

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

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

836 
by iprover+ 

837 

838 

839 
text {* Conversion into rewrite rules *} 

840 

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

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

843 

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

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

846 

847 

848 
text {* More rewrite rules *} 

849 

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

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

852 
lemmas conj_comms = conj_commute conj_left_commute 

853 

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

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

856 
lemmas disj_comms = disj_commute disj_left_commute 

857 

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

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

860 

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

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

863 

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

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

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

867 

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

869 

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

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

872 

873 
lemma ex_disj_distrib: 

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

875 

876 
lemma all_conj_distrib: 

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

878 

4854  879 
end 