author  wenzelm 
Thu, 23 Jul 2015 14:25:05 +0200  
changeset 60770  240563fbf41d 
parent 59529  d881f5288d5a 
child 61378  3e04c9ca001a 
permissions  rwrr 
1268  1 
(* Title: FOL/IFOL.thy 
11677  2 
Author: Lawrence C Paulson and Markus Wenzel 
3 
*) 

35  4 

60770  5 
section \<open>Intuitionistic firstorder logic\<close> 
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 

60770  23 
subsection \<open>Syntax and axiomatic basis\<close> 
11677  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 

60770  36 
subsubsection \<open>Equality\<close> 
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 

60770  45 
subsubsection \<open>Propositional logic\<close> 
46972  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 

60770  67 
subsubsection \<open>Quantifiers\<close> 
46972  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 

60770  79 
subsubsection \<open>Definitions\<close> 
46972  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 

60770  88 
axiomatization where  \<open>Reflection, admissible\<close> 
46972  89 
eq_reflection: "(x=y) ==> (x==y)" and 
90 
iff_reflection: "(P<>Q) ==> (P==Q)" 

91 

92 

60770  93 
subsubsection \<open>Additional notation\<close> 
46972  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 

60770  123 
subsection \<open>Lemmas and proof tools\<close> 
11677  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]) 

60770  149 
apply (rule \<open>P\<close>) 
21539  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) 

60770  189 
apply (erule notE [OF \<open>~P\<close>]) 
21539  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 *) 

60770  210 
ML \<open> 
59529  211 
fun mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i 
212 
fun eq_mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i 

60770  213 
\<close> 
21539  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*) 

60770  306 
ML \<open> 
59529  307 
fun iff_tac ctxt prems i = 
308 
resolve_tac ctxt (prems RL @{thms iffE}) i THEN 

309 
REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i) 

60770  310 
\<close> 
21539  311 

59529  312 
method_setup iff = 
313 
\<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close> 

314 

21539  315 
lemma conj_cong: 
316 
assumes "P <> P'" 

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

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

319 
apply (insert assms) 

59529  320 
apply (assumption  rule iffI conjI  erule iffE conjE mp  iff assms)+ 
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) 

59529  329 
apply (assumption  rule iffI conjI  erule iffE conjE mp  iff assms)+ 
21539  330 
done 
331 

332 
lemma disj_cong: 

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

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

335 
apply (insert assms) 

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

337 
done 

338 

339 
lemma imp_cong: 

340 
assumes "P <> P'" 

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

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

343 
apply (insert assms) 

59529  344 
apply (assumption  rule iffI impI  erule iffE  erule (1) notE impE  iff assms)+ 
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))" 

59529  358 
apply (assumption  rule iffI allI  erule (1) notE impE  erule allE  iff assms)+ 
21539  359 
done 
360 

361 
lemma ex_cong: 

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

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

59529  364 
apply (erule exE  assumption  rule iffI exI  erule (1) notE impE  iff assms)+ 
21539  365 
done 
366 

367 
lemma ex1_cong: 

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

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

59529  370 
apply (erule ex1E spec [THEN mp]  assumption  rule iffI ex1I  erule (1) notE impE  iff assms)+ 
21539  371 
done 
372 

373 
(*** Equality rules ***) 

374 

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

376 
apply (erule subst) 

377 
apply (rule refl) 

378 
done 

379 

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

381 
apply (erule subst, assumption) 

382 
done 

383 

384 
(** **) 

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

386 
apply (erule contrapos) 

387 
apply (erule sym) 

388 
done 

389 

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

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

392 

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

394 
apply unfold 

395 
apply (rule iff_refl) 

396 
done 

397 

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

399 
apply unfold 

400 
apply (rule refl) 

401 
done 

402 

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

404 
by unfold (rule iff_refl) 

405 

406 
(*substitution*) 

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

408 
apply (drule sym) 

409 
apply (erule (1) subst) 

410 
done 

411 

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

413 
lemma ex1_equalsE: 

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

415 
apply (erule ex1E) 

416 
apply (rule trans) 

417 
apply (rule_tac [2] sym) 

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

419 
done 

420 

421 
(** Polymorphic congruence rules **) 

422 

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

424 
apply (erule ssubst) 

425 
apply (rule refl) 

426 
done 

427 

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

429 
apply (erule ssubst)+ 

430 
apply (rule refl) 

431 
done 

432 

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

434 
apply (erule ssubst)+ 

435 
apply (rule refl) 

436 
done 

437 

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

439 
a = b 

440 
  

441 
c = d *) 

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

443 
apply (rule trans) 

444 
apply (rule trans) 

445 
apply (rule sym) 

446 
apply assumption+ 

447 
done 

448 

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

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

451 
apply (rule trans) 

452 
apply (rule trans) 

453 
apply assumption+ 

454 
apply (erule sym) 

455 
done 

456 

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

458 

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

460 
apply (rule iffI) 

461 
apply (erule (1) subst) 

462 
apply (erule (1) ssubst) 

463 
done 

464 

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

466 
apply (rule iffI) 

467 
apply (erule subst)+ 

468 
apply assumption 

469 
apply (erule ssubst)+ 

470 
apply assumption 

471 
done 

472 

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

474 
apply (rule iffI) 

475 
apply (erule subst)+ 

476 
apply assumption 

477 
apply (erule ssubst)+ 

478 
apply assumption 

479 
done 

480 

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

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

483 
apply (erule (1) pred2_cong) 

484 
done 

485 

486 

487 
(*** Simplifications of assumed implications. 

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

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

490 
intuitionistic propositional logic. See 

491 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

493 

494 
lemma conj_impE: 

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

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

497 
shows R 

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

499 

500 
lemma disj_impE: 

501 
assumes major: "(PQ)>S" 

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

503 
shows R 

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

505 

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

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

508 
lemma imp_impE: 

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

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

511 
and r2: "S ==> R" 

512 
shows R 

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

514 

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

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

517 
lemma not_impE: 

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

520 
apply (rule notI) 

521 
apply assumption 

522 
apply assumption 

21539  523 
done 
524 

525 
(*Simplifies the implication. UNSAFE. *) 

526 
lemma iff_impE: 

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

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

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

530 
and r3: "S ==> R" 

531 
shows R 

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

533 
done 

534 

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

536 
lemma all_impE: 

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

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

539 
and r2: "S ==> R" 

540 
shows R 

23393  541 
apply (rule allI impI major [THEN mp] r1 r2)+ 
21539  542 
done 
543 

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

545 
lemma ex_impE: 

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

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

548 
shows R 

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

550 
done 

551 

552 
(*** Courtesy of Krzysztof Grabczewski ***) 

553 

554 
lemma disj_imp_disj: 

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

21539  557 
apply (rule disjI1) apply assumption 
558 
apply (rule disjI2) apply assumption 

559 
done 

11734  560 

60770  561 
ML \<open> 
32172  562 
structure Project_Rule = Project_Rule 
563 
( 

22139  564 
val conjunct1 = @{thm conjunct1} 
565 
val conjunct2 = @{thm conjunct2} 

566 
val mp = @{thm mp} 

32172  567 
) 
60770  568 
\<close> 
18481  569 

48891  570 
ML_file "fologic.ML" 
21539  571 

42303  572 
lemma thin_refl: "[x=x; PROP W] ==> PROP W" . 
21539  573 

60770  574 
ML \<open> 
42799  575 
structure Hypsubst = Hypsubst 
576 
( 

577 
val dest_eq = FOLogic.dest_eq 

578 
val dest_Trueprop = FOLogic.dest_Trueprop 

579 
val dest_imp = FOLogic.dest_imp 

580 
val eq_reflection = @{thm eq_reflection} 

581 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

582 
val imp_intr = @{thm impI} 

583 
val rev_mp = @{thm rev_mp} 

584 
val subst = @{thm subst} 

585 
val sym = @{thm sym} 

586 
val thin_refl = @{thm thin_refl} 

587 
); 

588 
open Hypsubst; 

60770  589 
\<close> 
42799  590 

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

592 

4092  593 

60770  594 
subsection \<open>Intuitionistic Reasoning\<close> 
12368  595 

60770  596 
setup \<open>Intuitionistic.method_setup @{binding iprover}\<close> 
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

597 

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

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

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

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

602 
shows R 
12349  603 
proof  
604 
from 3 and 1 have P . 

12368  605 
with 1 have Q by (rule impE) 
12349  606 
with 2 show R . 
607 
qed 

608 

609 
lemma allE': 

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

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

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

612 
shows Q 
12349  613 
proof  
614 
from 1 have "P(x)" by (rule spec) 

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

616 
qed 

617 

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

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

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

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

621 
shows R 
12349  622 
proof  
623 
from 2 and 1 have P . 

624 
with 1 show R by (rule notE) 

625 
qed 

626 

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

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

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

630 
and [Pure.intro] = exI disjI2 disjI1 

631 

60770  632 
setup \<open>Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac)\<close> 
12349  633 

634 

12368  635 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  636 
by iprover 
12368  637 

638 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

640 

641 

13435  642 
lemma eq_commute: "a=b <> b=a" 
643 
apply (rule iffI) 

644 
apply (erule sym)+ 

645 
done 

646 

647 

60770  648 
subsection \<open>Atomizing metalevel rules\<close> 
11677  649 

11747  650 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  651 
proof 
11677  652 
assume "!!x. P(x)" 
22931  653 
then show "ALL x. P(x)" .. 
11677  654 
next 
655 
assume "ALL x. P(x)" 

22931  656 
then show "!!x. P(x)" .. 
11677  657 
qed 
658 

11747  659 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  660 
proof 
12368  661 
assume "A ==> B" 
22931  662 
then show "A > B" .. 
11677  663 
next 
664 
assume "A > B" and A 

22931  665 
then show B by (rule mp) 
11677  666 
qed 
667 

11747  668 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  669 
proof 
11677  670 
assume "x == y" 
60770  671 
show "x = y" unfolding \<open>x == y\<close> by (rule refl) 
11677  672 
next 
673 
assume "x = y" 

22931  674 
then show "x == y" by (rule eq_reflection) 
11677  675 
qed 
676 

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

679 
assume "A == B" 

60770  680 
show "A <> B" unfolding \<open>A == B\<close> by (rule iff_refl) 
18813  681 
next 
682 
assume "A <> B" 

22931  683 
then show "A == B" by (rule iff_reflection) 
18813  684 
qed 
685 

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

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

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

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

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

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

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

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

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

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

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

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

699 
from conj show B .. 
11953  700 
qed 
701 
qed 

702 

12368  703 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  704 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  705 

11848  706 

60770  707 
subsection \<open>Atomizing elimination rules\<close> 
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

708 

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

709 
lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)" 
57948  710 
by rule iprover+ 
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

711 

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

712 
lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" 
57948  713 
by rule iprover+ 
26580
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_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A  B ==> C) ==> C)" 
57948  716 
by rule iprover+ 
26580
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_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

719 

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

720 

60770  721 
subsection \<open>Calculational rules\<close> 
11848  722 

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

724 
by (rule ssubst) 

725 

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

727 
by (rule subst) 

728 

60770  729 
text \<open> 
11848  730 
Note that this list of rules is in reverse order of priorities. 
60770  731 
\<close> 
11848  732 

12019  733 
lemmas basic_trans_rules [trans] = 
11848  734 
forw_subst 
735 
back_subst 

736 
rev_mp 

737 
mp 

738 
trans 

739 

60770  740 
subsection \<open>``Let'' declarations\<close> 
13779  741 

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

742 
nonterminal letbinds and letbind 
13779  743 

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

744 
definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where 
13779  745 
"Let(s, f) == f(s)" 
746 

747 
syntax 

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

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

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

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

752 

753 
translations 

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

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

757 

758 
lemma LetI: 

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

761 
apply (unfold Let_def) 

762 
apply (rule refl [THEN assms]) 

763 
done 

764 

765 

60770  766 
subsection \<open>Intuitionistic simplification rules\<close> 
26286  767 

768 
lemma conj_simps: 

769 
"P & True <> P" 

770 
"True & P <> P" 

771 
"P & False <> False" 

772 
"False & P <> False" 

773 
"P & P <> P" 

774 
"P & P & Q <> P & Q" 

775 
"P & ~P <> False" 

776 
"~P & P <> False" 

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

778 
by iprover+ 

779 

780 
lemma disj_simps: 

781 
"P  True <> True" 

782 
"True  P <> True" 

783 
"P  False <> P" 

784 
"False  P <> P" 

785 
"P  P <> P" 

786 
"P  P  Q <> P  Q" 

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

788 
by iprover+ 

789 

790 
lemma not_simps: 

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

792 
"~ False <> True" 

793 
"~ True <> False" 

794 
by iprover+ 

795 

796 
lemma imp_simps: 

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

798 
"(P > True) <> True" 

799 
"(False > P) <> True" 

800 
"(True > P) <> P" 

801 
"(P > P) <> True" 

802 
"(P > ~P) <> ~P" 

803 
by iprover+ 

804 

805 
lemma iff_simps: 

806 
"(True <> P) <> P" 

807 
"(P <> True) <> P" 

808 
"(P <> P) <> True" 

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

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

811 
by iprover+ 

812 

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

814 
lemma quant_simps: 

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

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

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

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

819 
"EX x. x=t" 

820 
"EX x. t=x" 

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

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

823 
by iprover+ 

824 

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

826 
lemma distrib_simps: 

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

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

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

830 
by iprover+ 

831 

832 

60770  833 
text \<open>Conversion into rewrite rules\<close> 
26286  834 

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

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

837 

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

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

840 

841 

60770  842 
text \<open>More rewrite rules\<close> 
26286  843 

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

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

846 
lemmas conj_comms = conj_commute conj_left_commute 

847 

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

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

850 
lemmas disj_comms = disj_commute disj_left_commute 

851 

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

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

854 

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

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

857 

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

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

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

861 

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

863 

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

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

866 

867 
lemma ex_disj_distrib: 

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

869 

870 
lemma all_conj_distrib: 

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

872 

4854  873 
end 