author  wenzelm 
Fri, 16 Mar 2012 22:22:05 +0100  
changeset 46972  ef6fc1a0884d 
parent 44121  44adaa6db327 
child 48891  c0eafbd55de3 
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 

23155  9 
uses 
44121  10 
"~~/src/Tools/misc_legacy.ML" 
23155  11 
"~~/src/Provers/splitter.ML" 
12 
"~~/src/Provers/hypsubst.ML" 

23171  13 
"~~/src/Tools/IsaPlanner/zipper.ML" 
14 
"~~/src/Tools/IsaPlanner/isand.ML" 

15 
"~~/src/Tools/IsaPlanner/rw_tools.ML" 

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

30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
28856
diff
changeset

17 
"~~/src/Tools/eqsubst.ML" 
23155  18 
"~~/src/Provers/quantifier1.ML" 
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

19 
"~~/src/Tools/intuitionistic.ML" 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
28856
diff
changeset

20 
"~~/src/Tools/project_rule.ML" 
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

21 
"~~/src/Tools/atomize_elim.ML" 
23155  22 
("fologic.ML") 
23 
("intprover.ML") 

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

25 

0  26 

11677  27 
subsection {* Syntax and axiomatic basis *} 
28 

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

29 
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

30 

14854  31 
classes "term" 
36452  32 
default_sort "term" 
0  33 

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

34 
typedecl o 
79  35 

11747  36 
judgment 
37 
Trueprop :: "o => prop" ("(_)" 5) 

0  38 

79  39 

46972  40 
subsubsection {* Equality *} 
35  41 

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

44 
where 

45 
refl: "a=a" and 

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

79  47 

0  48 

46972  49 
subsubsection {* Propositional logic *} 
50 

51 
axiomatization 

52 
False :: o and 

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

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

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

56 
where 

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

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

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

60 

61 
disjI1: "P ==> PQ" and 

62 
disjI2: "Q ==> PQ" and 

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

64 

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

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

67 

68 
FalseE: "False ==> P" 

69 

70 

71 
subsubsection {* Quantifiers *} 

72 

73 
axiomatization 

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

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

76 
where 

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

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

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

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

81 

82 

83 
subsubsection {* Definitions *} 

84 

85 
definition "True == False>False" 

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

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

88 

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

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

91 

92 
axiomatization where  {* Reflection, admissible *} 

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

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

95 

96 

97 
subsubsection {* Additional notation *} 

98 

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

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

79  101 

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

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

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

106 
not_equal (infixl "\<noteq>" 50) 
19363  107 

21524  108 
notation (xsymbols) 
46972  109 
Not ("\<not> _" [40] 40) and 
110 
conj (infixr "\<and>" 35) and 

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

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

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

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

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

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

35  117 

21524  118 
notation (HTML output) 
46972  119 
Not ("\<not> _" [40] 40) and 
120 
conj (infixr "\<and>" 35) and 

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

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

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

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

14236  125 

13779  126 

11677  127 
subsection {* Lemmas and proof tools *} 
128 

46972  129 
lemmas strip = impI allI 
130 

21539  131 
lemma TrueI: True 
132 
unfolding True_def by (rule impI) 

133 

134 

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

136 

137 
lemma conjE: 

138 
assumes major: "P & Q" 

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

140 
shows R 

141 
apply (rule r) 

142 
apply (rule major [THEN conjunct1]) 

143 
apply (rule major [THEN conjunct2]) 

144 
done 

145 

146 
lemma impE: 

147 
assumes major: "P > Q" 

148 
and P 

149 
and r: "Q ==> R" 

150 
shows R 

151 
apply (rule r) 

152 
apply (rule major [THEN mp]) 

153 
apply (rule `P`) 

154 
done 

155 

156 
lemma allE: 

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

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

159 
shows R 

160 
apply (rule r) 

161 
apply (rule major [THEN spec]) 

162 
done 

163 

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

165 
lemma all_dupE: 

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

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

168 
shows R 

169 
apply (rule r) 

170 
apply (rule major [THEN spec]) 

171 
apply (rule major) 

172 
done 

173 

174 

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

176 

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

178 
unfolding not_def by (erule impI) 

179 

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

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

182 

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

184 
by (erule notE) 

185 

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

187 
lemma not_to_imp: 

188 
assumes "~P" 

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

190 
shows Q 

191 
apply (rule r) 

192 
apply (rule impI) 

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

194 
done 

195 

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

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

200 

201 
(*Contrapositive of an inference rule*) 

202 
lemma contrapos: 

203 
assumes major: "~Q" 

204 
and minor: "P ==> Q" 

205 
shows "~P" 

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

207 
apply (erule minor) 

208 
done 

209 

210 

211 
(*** Modus Ponens Tactics ***) 

212 

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

214 
ML {* 

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

21539  217 
*} 
218 

219 

220 
(*** Ifandonlyif ***) 

221 

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

223 
apply (unfold iff_def) 

224 
apply (rule conjI) 

225 
apply (erule impI) 

226 
apply (erule impI) 

227 
done 

228 

229 

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

231 
lemma iffE: 

232 
assumes major: "P <> Q" 

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

234 
shows R 

235 
apply (insert major, unfold iff_def) 

236 
apply (erule conjE) 

237 
apply (erule r) 

238 
apply assumption 

239 
done 

240 

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

242 

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

244 
apply (unfold iff_def) 

245 
apply (erule conjunct1 [THEN mp]) 

246 
apply assumption 

247 
done 

248 

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

250 
apply (unfold iff_def) 

251 
apply (erule conjunct2 [THEN mp]) 

252 
apply assumption 

253 
done 

254 

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

256 
apply (erule iffD1) 

257 
apply assumption 

258 
done 

259 

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

261 
apply (erule iffD2) 

262 
apply assumption 

263 
done 

264 

265 
lemma iff_refl: "P <> P" 

266 
by (rule iffI) 

267 

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

269 
apply (erule iffE) 

270 
apply (rule iffI) 

271 
apply (assumption  erule mp)+ 

272 
done 

273 

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

275 
apply (rule iffI) 

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

277 
done 

278 

279 

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

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

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

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

284 
***) 

285 

286 
lemma ex1I: 

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

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

293 
lemma ex_ex1I: 

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

296 
apply (rule ex1I) 

297 
apply assumption 

298 
apply assumption 

21539  299 
done 
300 

301 
lemma ex1E: 

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

21539  304 
apply (assumption  erule exE conjE)+ 
305 
done 

306 

307 

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

309 

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

311 
ML {* 

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

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

21539  315 
*} 
316 

317 
lemma conj_cong: 

318 
assumes "P <> P'" 

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

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

321 
apply (insert assms) 

322 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  323 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  324 
done 
325 

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

327 
lemma conj_cong2: 

328 
assumes "P <> P'" 

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

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

331 
apply (insert assms) 

332 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  333 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  334 
done 
335 

336 
lemma disj_cong: 

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

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

339 
apply (insert assms) 

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

341 
done 

342 

343 
lemma imp_cong: 

344 
assumes "P <> P'" 

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

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

347 
apply (insert assms) 

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

39159  349 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  350 
done 
351 

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

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

354 
done 

355 

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

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

358 
done 

359 

360 
lemma all_cong: 

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

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

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

39159  364 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  365 
done 
366 

367 
lemma ex_cong: 

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

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

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

39159  371 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  372 
done 
373 

374 
lemma ex1_cong: 

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

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

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

39159  378 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  379 
done 
380 

381 
(*** Equality rules ***) 

382 

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

384 
apply (erule subst) 

385 
apply (rule refl) 

386 
done 

387 

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

389 
apply (erule subst, assumption) 

390 
done 

391 

392 
(** **) 

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

394 
apply (erule contrapos) 

395 
apply (erule sym) 

396 
done 

397 

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

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

400 

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

402 
apply unfold 

403 
apply (rule iff_refl) 

404 
done 

405 

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

407 
apply unfold 

408 
apply (rule refl) 

409 
done 

410 

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

412 
by unfold (rule iff_refl) 

413 

414 
(*substitution*) 

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

416 
apply (drule sym) 

417 
apply (erule (1) subst) 

418 
done 

419 

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

421 
lemma ex1_equalsE: 

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

423 
apply (erule ex1E) 

424 
apply (rule trans) 

425 
apply (rule_tac [2] sym) 

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

427 
done 

428 

429 
(** Polymorphic congruence rules **) 

430 

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

432 
apply (erule ssubst) 

433 
apply (rule refl) 

434 
done 

435 

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

437 
apply (erule ssubst)+ 

438 
apply (rule refl) 

439 
done 

440 

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

442 
apply (erule ssubst)+ 

443 
apply (rule refl) 

444 
done 

445 

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

447 
a = b 

448 
  

449 
c = d *) 

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

451 
apply (rule trans) 

452 
apply (rule trans) 

453 
apply (rule sym) 

454 
apply assumption+ 

455 
done 

456 

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

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

459 
apply (rule trans) 

460 
apply (rule trans) 

461 
apply assumption+ 

462 
apply (erule sym) 

463 
done 

464 

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

466 

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

468 
apply (rule iffI) 

469 
apply (erule (1) subst) 

470 
apply (erule (1) ssubst) 

471 
done 

472 

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

474 
apply (rule iffI) 

475 
apply (erule subst)+ 

476 
apply assumption 

477 
apply (erule ssubst)+ 

478 
apply assumption 

479 
done 

480 

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

482 
apply (rule iffI) 

483 
apply (erule subst)+ 

484 
apply assumption 

485 
apply (erule ssubst)+ 

486 
apply assumption 

487 
done 

488 

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

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

491 
apply (erule (1) pred2_cong) 

492 
done 

493 

494 

495 
(*** Simplifications of assumed implications. 

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

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

498 
intuitionistic propositional logic. See 

499 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

501 

502 
lemma conj_impE: 

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

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

505 
shows R 

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

507 

508 
lemma disj_impE: 

509 
assumes major: "(PQ)>S" 

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

511 
shows R 

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

513 

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

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

516 
lemma imp_impE: 

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

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

519 
and r2: "S ==> R" 

520 
shows R 

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

522 

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

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

525 
lemma not_impE: 

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

528 
apply (rule notI) 

529 
apply assumption 

530 
apply assumption 

21539  531 
done 
532 

533 
(*Simplifies the implication. UNSAFE. *) 

534 
lemma iff_impE: 

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

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

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

538 
and r3: "S ==> R" 

539 
shows R 

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

541 
done 

542 

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

544 
lemma all_impE: 

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

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

547 
and r2: "S ==> R" 

548 
shows R 

23393  549 
apply (rule allI impI major [THEN mp] r1 r2)+ 
21539  550 
done 
551 

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

553 
lemma ex_impE: 

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

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

556 
shows R 

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

558 
done 

559 

560 
(*** Courtesy of Krzysztof Grabczewski ***) 

561 

562 
lemma disj_imp_disj: 

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

21539  565 
apply (rule disjI1) apply assumption 
566 
apply (rule disjI2) apply assumption 

567 
done 

11734  568 

18481  569 
ML {* 
32172  570 
structure Project_Rule = Project_Rule 
571 
( 

22139  572 
val conjunct1 = @{thm conjunct1} 
573 
val conjunct2 = @{thm conjunct2} 

574 
val mp = @{thm mp} 

32172  575 
) 
18481  576 
*} 
577 

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

578 
use "fologic.ML" 
21539  579 

42303  580 
lemma thin_refl: "[x=x; PROP W] ==> PROP W" . 
21539  581 

42799  582 
ML {* 
583 
structure Hypsubst = Hypsubst 

584 
( 

585 
val dest_eq = FOLogic.dest_eq 

586 
val dest_Trueprop = FOLogic.dest_Trueprop 

587 
val dest_imp = FOLogic.dest_imp 

588 
val eq_reflection = @{thm eq_reflection} 

589 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

590 
val imp_intr = @{thm impI} 

591 
val rev_mp = @{thm rev_mp} 

592 
val subst = @{thm subst} 

593 
val sym = @{thm sym} 

594 
val thin_refl = @{thm thin_refl} 

595 
); 

596 
open Hypsubst; 

597 
*} 

598 

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

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

601 

4092  602 

12875  603 
subsection {* Intuitionistic Reasoning *} 
12368  604 

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

606 

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

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

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

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

611 
shows R 
12349  612 
proof  
613 
from 3 and 1 have P . 

12368  614 
with 1 have Q by (rule impE) 
12349  615 
with 2 show R . 
616 
qed 

617 

618 
lemma allE': 

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

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

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

621 
shows Q 
12349  622 
proof  
623 
from 1 have "P(x)" by (rule spec) 

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

625 
qed 

626 

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

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

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

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

630 
shows R 
12349  631 
proof  
632 
from 2 and 1 have P . 

633 
with 1 show R by (rule notE) 

634 
qed 

635 

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

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

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

639 
and [Pure.intro] = exI disjI2 disjI1 

640 

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

643 

12368  644 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  645 
by iprover 
12368  646 

647 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

649 

650 

13435  651 
lemma eq_commute: "a=b <> b=a" 
652 
apply (rule iffI) 

653 
apply (erule sym)+ 

654 
done 

655 

656 

11677  657 
subsection {* Atomizing metalevel rules *} 
658 

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

22931  665 
then show "!!x. P(x)" .. 
11677  666 
qed 
667 

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

22931  674 
then show B by (rule mp) 
11677  675 
qed 
676 

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

22931  683 
then show "x == y" by (rule eq_reflection) 
11677  684 
qed 
685 

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

688 
assume "A == B" 

22931  689 
show "A <> B" unfolding `A == B` by (rule iff_refl) 
18813  690 
next 
691 
assume "A <> B" 

22931  692 
then show "A == B" by (rule iff_reflection) 
18813  693 
qed 
694 

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

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

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

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

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

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

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

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

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

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

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

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

708 
from conj show B .. 
11953  709 
qed 
710 
qed 

711 

12368  712 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  713 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  714 

11848  715 

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

716 
subsection {* Atomizing elimination rules *} 
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 
setup AtomizeElim.setup 
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_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

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_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

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_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

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

728 

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

729 
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

730 

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

731 

11848  732 
subsection {* Calculational rules *} 
733 

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

735 
by (rule ssubst) 

736 

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

738 
by (rule subst) 

739 

740 
text {* 

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

742 
*} 

743 

12019  744 
lemmas basic_trans_rules [trans] = 
11848  745 
forw_subst 
746 
back_subst 

747 
rev_mp 

748 
mp 

749 
trans 

750 

13779  751 
subsection {* ``Let'' declarations *} 
752 

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

753 
nonterminal letbinds and letbind 
13779  754 

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

755 
definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where 
13779  756 
"Let(s, f) == f(s)" 
757 

758 
syntax 

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

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

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

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

763 

764 
translations 

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

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

768 

769 
lemma LetI: 

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

772 
apply (unfold Let_def) 

773 
apply (rule refl [THEN assms]) 

774 
done 

775 

776 

26286  777 
subsection {* Intuitionistic simplification rules *} 
778 

779 
lemma conj_simps: 

780 
"P & True <> P" 

781 
"True & P <> P" 

782 
"P & False <> False" 

783 
"False & P <> False" 

784 
"P & P <> P" 

785 
"P & P & Q <> P & Q" 

786 
"P & ~P <> False" 

787 
"~P & P <> False" 

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

789 
by iprover+ 

790 

791 
lemma disj_simps: 

792 
"P  True <> True" 

793 
"True  P <> True" 

794 
"P  False <> P" 

795 
"False  P <> P" 

796 
"P  P <> P" 

797 
"P  P  Q <> P  Q" 

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

799 
by iprover+ 

800 

801 
lemma not_simps: 

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

803 
"~ False <> True" 

804 
"~ True <> False" 

805 
by iprover+ 

806 

807 
lemma imp_simps: 

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

809 
"(P > True) <> True" 

810 
"(False > P) <> True" 

811 
"(True > P) <> P" 

812 
"(P > P) <> True" 

813 
"(P > ~P) <> ~P" 

814 
by iprover+ 

815 

816 
lemma iff_simps: 

817 
"(True <> P) <> P" 

818 
"(P <> True) <> P" 

819 
"(P <> P) <> True" 

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

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

822 
by iprover+ 

823 

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

825 
lemma quant_simps: 

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

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

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

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

830 
"EX x. x=t" 

831 
"EX x. t=x" 

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

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

834 
by iprover+ 

835 

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

837 
lemma distrib_simps: 

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

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

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

841 
by iprover+ 

842 

843 

844 
text {* Conversion into rewrite rules *} 

845 

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

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

848 

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

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

851 

852 

853 
text {* More rewrite rules *} 

854 

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

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

857 
lemmas conj_comms = conj_commute conj_left_commute 

858 

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

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

861 
lemmas disj_comms = disj_commute disj_left_commute 

862 

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

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

865 

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

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

868 

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

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

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

872 

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

874 

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

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

877 

878 
lemma ex_disj_distrib: 

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

880 

881 
lemma all_conj_distrib: 

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

883 

4854  884 
end 