author  wenzelm 
Thu, 31 May 2007 20:55:29 +0200  
changeset 23171  861f63a35d31 
parent 23155  4b04f9d859af 
child 23393  31781b2de73d 
permissions  rwrr 
1268  1 
(* Title: FOL/IFOL.thy 
35  2 
ID: $Id$ 
11677  3 
Author: Lawrence C Paulson and Markus Wenzel 
4 
*) 

35  5 

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

15481  8 
theory IFOL 
9 
imports Pure 

23155  10 
uses 
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" 

23155  17 
"~~/src/Provers/eqsubst.ML" 
18 
"~~/src/Provers/induct_method.ML" 

19 
"~~/src/Provers/classical.ML" 

20 
"~~/src/Provers/blast.ML" 

21 
"~~/src/Provers/clasimp.ML" 

22 
"~~/src/Provers/quantifier1.ML" 

23 
"~~/src/Provers/project_rule.ML" 

24 
("fologic.ML") 

25 
("hypsubstdata.ML") 

26 
("intprover.ML") 

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

28 

0  29 

11677  30 
subsection {* Syntax and axiomatic basis *} 
31 

3906  32 
global 
33 

14854  34 
classes "term" 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

35 
defaultsort "term" 
0  36 

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

37 
typedecl o 
79  38 

11747  39 
judgment 
40 
Trueprop :: "o => prop" ("(_)" 5) 

0  41 

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

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

44 
False :: o 
79  45 

46 
(* Connectives *) 

47 

17276  48 
"op =" :: "['a, 'a] => o" (infixl "=" 50) 
35  49 

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

50 
Not :: "o => o" ("~ _" [40] 40) 
17276  51 
"op &" :: "[o, o] => o" (infixr "&" 35) 
52 
"op " :: "[o, o] => o" (infixr "" 30) 

53 
"op >" :: "[o, o] => o" (infixr ">" 25) 

54 
"op <>" :: "[o, o] => o" (infixr "<>" 25) 

79  55 

56 
(* Quantifiers *) 

57 

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

58 
All :: "('a => o) => o" (binder "ALL " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

59 
Ex :: "('a => o) => o" (binder "EX " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

60 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 
79  61 

0  62 

19363  63 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

64 
not_equal :: "['a, 'a] => o" (infixl "~=" 50) where 
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

65 
"x ~= y == ~ (x = y)" 
79  66 

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

68 
not_equal (infixl "\<noteq>" 50) 
19363  69 

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

71 
not_equal (infixl "\<noteq>" 50) 
19363  72 

21524  73 
notation (xsymbols) 
21539  74 
Not ("\<not> _" [40] 40) and 
75 
"op &" (infixr "\<and>" 35) and 

76 
"op " (infixr "\<or>" 30) and 

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

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

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

21524  80 
"op >" (infixr "\<longrightarrow>" 25) and 
81 
"op <>" (infixr "\<longleftrightarrow>" 25) 

35  82 

21524  83 
notation (HTML output) 
21539  84 
Not ("\<not> _" [40] 40) and 
85 
"op &" (infixr "\<and>" 35) and 

86 
"op " (infixr "\<or>" 30) and 

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

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

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

6340  90 

3932  91 
local 
3906  92 

14236  93 
finalconsts 
94 
False All Ex 

95 
"op =" 

96 
"op &" 

97 
"op " 

98 
"op >" 

99 

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

100 
axioms 
0  101 

79  102 
(* Equality *) 
0  103 

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

104 
refl: "a=a" 
0  105 

79  106 
(* Propositional logic *) 
0  107 

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

108 
conjI: "[ P; Q ] ==> P&Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

109 
conjunct1: "P&Q ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

110 
conjunct2: "P&Q ==> Q" 
0  111 

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

112 
disjI1: "P ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

113 
disjI2: "Q ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

114 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  115 

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

116 
impI: "(P ==> Q) ==> P>Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

117 
mp: "[ P>Q; P ] ==> Q" 
0  118 

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

119 
FalseE: "False ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

120 

79  121 
(* Quantifiers *) 
0  122 

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

123 
allI: "(!!x. P(x)) ==> (ALL x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

124 
spec: "(ALL x. P(x)) ==> P(x)" 
0  125 

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

126 
exI: "P(x) ==> (EX x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

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

129 
(* Reflection *) 

130 

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

131 
eq_reflection: "(x=y) ==> (x==y)" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

132 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  133 

4092  134 

19756  135 
lemmas strip = impI allI 
136 

137 

15377  138 
text{*Thanks to Stephan Merz*} 
139 
theorem subst: 

140 
assumes eq: "a = b" and p: "P(a)" 

141 
shows "P(b)" 

142 
proof  

143 
from eq have meta: "a \<equiv> b" 

144 
by (rule eq_reflection) 

145 
from p show ?thesis 

146 
by (unfold meta) 

147 
qed 

148 

149 

14236  150 
defs 
151 
(* Definitions *) 

152 

153 
True_def: "True == False>False" 

154 
not_def: "~P == P>False" 

155 
iff_def: "P<>Q == (P>Q) & (Q>P)" 

156 

157 
(* Unique existence *) 

158 

159 
ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) > y=x)" 

160 

13779  161 

11677  162 
subsection {* Lemmas and proof tools *} 
163 

21539  164 
lemma TrueI: True 
165 
unfolding True_def by (rule impI) 

166 

167 

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

169 

170 
lemma conjE: 

171 
assumes major: "P & Q" 

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

173 
shows R 

174 
apply (rule r) 

175 
apply (rule major [THEN conjunct1]) 

176 
apply (rule major [THEN conjunct2]) 

177 
done 

178 

179 
lemma impE: 

180 
assumes major: "P > Q" 

181 
and P 

182 
and r: "Q ==> R" 

183 
shows R 

184 
apply (rule r) 

185 
apply (rule major [THEN mp]) 

186 
apply (rule `P`) 

187 
done 

188 

189 
lemma allE: 

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

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

192 
shows R 

193 
apply (rule r) 

194 
apply (rule major [THEN spec]) 

195 
done 

196 

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

198 
lemma all_dupE: 

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

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

201 
shows R 

202 
apply (rule r) 

203 
apply (rule major [THEN spec]) 

204 
apply (rule major) 

205 
done 

206 

207 

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

209 

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

211 
unfolding not_def by (erule impI) 

212 

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

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

215 

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

217 
by (erule notE) 

218 

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

220 
lemma not_to_imp: 

221 
assumes "~P" 

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

223 
shows Q 

224 
apply (rule r) 

225 
apply (rule impI) 

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

227 
done 

228 

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

230 
this implication, then apply impI to move P back into the assumptions. 

231 
To specify P use something like 

232 
eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) 

233 
lemma rev_mp: "[ P; P > Q ] ==> Q" 

234 
by (erule mp) 

235 

236 
(*Contrapositive of an inference rule*) 

237 
lemma contrapos: 

238 
assumes major: "~Q" 

239 
and minor: "P ==> Q" 

240 
shows "~P" 

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

242 
apply (erule minor) 

243 
done 

244 

245 

246 
(*** Modus Ponens Tactics ***) 

247 

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

249 
ML {* 

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

21539  252 
*} 
253 

254 

255 
(*** Ifandonlyif ***) 

256 

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

258 
apply (unfold iff_def) 

259 
apply (rule conjI) 

260 
apply (erule impI) 

261 
apply (erule impI) 

262 
done 

263 

264 

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

266 
lemma iffE: 

267 
assumes major: "P <> Q" 

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

269 
shows R 

270 
apply (insert major, unfold iff_def) 

271 
apply (erule conjE) 

272 
apply (erule r) 

273 
apply assumption 

274 
done 

275 

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

277 

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

279 
apply (unfold iff_def) 

280 
apply (erule conjunct1 [THEN mp]) 

281 
apply assumption 

282 
done 

283 

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

285 
apply (unfold iff_def) 

286 
apply (erule conjunct2 [THEN mp]) 

287 
apply assumption 

288 
done 

289 

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

291 
apply (erule iffD1) 

292 
apply assumption 

293 
done 

294 

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

296 
apply (erule iffD2) 

297 
apply assumption 

298 
done 

299 

300 
lemma iff_refl: "P <> P" 

301 
by (rule iffI) 

302 

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

304 
apply (erule iffE) 

305 
apply (rule iffI) 

306 
apply (assumption  erule mp)+ 

307 
done 

308 

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

310 
apply (rule iffI) 

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

312 
done 

313 

314 

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

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

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

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

319 
***) 

320 

321 
lemma ex1I: 

322 
assumes "P(a)" 

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

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

325 
apply (unfold ex1_def) 

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

327 
done 

328 

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

330 
lemma ex_ex1I: 

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

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

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

334 
apply (rule ex [THEN exE]) 

335 
apply (assumption  rule ex1I eq)+ 

336 
done 

337 

338 
lemma ex1E: 

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

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

341 
shows R 

342 
apply (insert ex1, unfold ex1_def) 

343 
apply (assumption  erule exE conjE)+ 

344 
done 

345 

346 

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

348 

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

350 
ML {* 

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

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

21539  354 
*} 
355 

356 
lemma conj_cong: 

357 
assumes "P <> P'" 

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

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

360 
apply (insert assms) 

361 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

363 
done 

364 

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

366 
lemma conj_cong2: 

367 
assumes "P <> P'" 

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

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

370 
apply (insert assms) 

371 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

373 
done 

374 

375 
lemma disj_cong: 

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

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

378 
apply (insert assms) 

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

380 
done 

381 

382 
lemma imp_cong: 

383 
assumes "P <> P'" 

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

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

386 
apply (insert assms) 

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

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

389 
done 

390 

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

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

393 
done 

394 

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

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

397 
done 

398 

399 
lemma all_cong: 

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

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

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

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

404 
done 

405 

406 
lemma ex_cong: 

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

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

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

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

411 
done 

412 

413 
lemma ex1_cong: 

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

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

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

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

418 
done 

419 

420 
(*** Equality rules ***) 

421 

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

423 
apply (erule subst) 

424 
apply (rule refl) 

425 
done 

426 

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

428 
apply (erule subst, assumption) 

429 
done 

430 

431 
(** **) 

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

433 
apply (erule contrapos) 

434 
apply (erule sym) 

435 
done 

436 

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

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

439 

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

441 
apply unfold 

442 
apply (rule iff_refl) 

443 
done 

444 

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

446 
apply unfold 

447 
apply (rule refl) 

448 
done 

449 

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

451 
by unfold (rule iff_refl) 

452 

453 
(*substitution*) 

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

455 
apply (drule sym) 

456 
apply (erule (1) subst) 

457 
done 

458 

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

460 
lemma ex1_equalsE: 

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

462 
apply (erule ex1E) 

463 
apply (rule trans) 

464 
apply (rule_tac [2] sym) 

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

466 
done 

467 

468 
(** Polymorphic congruence rules **) 

469 

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

471 
apply (erule ssubst) 

472 
apply (rule refl) 

473 
done 

474 

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

476 
apply (erule ssubst)+ 

477 
apply (rule refl) 

478 
done 

479 

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

481 
apply (erule ssubst)+ 

482 
apply (rule refl) 

483 
done 

484 

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

486 
a = b 

487 
  

488 
c = d *) 

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

490 
apply (rule trans) 

491 
apply (rule trans) 

492 
apply (rule sym) 

493 
apply assumption+ 

494 
done 

495 

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

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

498 
apply (rule trans) 

499 
apply (rule trans) 

500 
apply assumption+ 

501 
apply (erule sym) 

502 
done 

503 

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

505 

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

507 
apply (rule iffI) 

508 
apply (erule (1) subst) 

509 
apply (erule (1) ssubst) 

510 
done 

511 

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

513 
apply (rule iffI) 

514 
apply (erule subst)+ 

515 
apply assumption 

516 
apply (erule ssubst)+ 

517 
apply assumption 

518 
done 

519 

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

521 
apply (rule iffI) 

522 
apply (erule subst)+ 

523 
apply assumption 

524 
apply (erule ssubst)+ 

525 
apply assumption 

526 
done 

527 

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

529 

530 
ML {* 

531 
bind_thms ("pred_congs", 

532 
List.concat (map (fn c => 

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

22139  534 
[@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}]) 
21539  535 
(explode"PQRS"))) 
536 
*} 

537 

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

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

540 
apply (erule (1) pred2_cong) 

541 
done 

542 

543 

544 
(*** Simplifications of assumed implications. 

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

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

547 
intuitionistic propositional logic. See 

548 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

550 

551 
lemma conj_impE: 

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

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

554 
shows R 

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

556 

557 
lemma disj_impE: 

558 
assumes major: "(PQ)>S" 

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

560 
shows R 

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

562 

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

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

565 
lemma imp_impE: 

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

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

568 
and r2: "S ==> R" 

569 
shows R 

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

571 

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

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

574 
lemma not_impE: 

575 
assumes major: "~P > S" 

576 
and r1: "P ==> False" 

577 
and r2: "S ==> R" 

578 
shows R 

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

580 
done 

581 

582 
(*Simplifies the implication. UNSAFE. *) 

583 
lemma iff_impE: 

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

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

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

587 
and r3: "S ==> R" 

588 
shows R 

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

590 
done 

591 

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

593 
lemma all_impE: 

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

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

596 
and r2: "S ==> R" 

597 
shows R 

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

599 
done 

600 

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

602 
lemma ex_impE: 

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

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

605 
shows R 

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

607 
done 

608 

609 
(*** Courtesy of Krzysztof Grabczewski ***) 

610 

611 
lemma disj_imp_disj: 

612 
assumes major: "PQ" 

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

614 
shows "RS" 

615 
apply (rule disjE [OF major]) 

616 
apply (rule disjI1) apply assumption 

617 
apply (rule disjI2) apply assumption 

618 
done 

11734  619 

18481  620 
ML {* 
621 
structure ProjectRule = ProjectRuleFun 

622 
(struct 

22139  623 
val conjunct1 = @{thm conjunct1} 
624 
val conjunct2 = @{thm conjunct2} 

625 
val mp = @{thm mp} 

18481  626 
end) 
627 
*} 

628 

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

629 
use "fologic.ML" 
21539  630 

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

632 

9886  633 
use "hypsubstdata.ML" 
634 
setup hypsubst_setup 

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

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

636 

4092  637 

12875  638 
subsection {* Intuitionistic Reasoning *} 
12368  639 

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

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

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

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

644 
shows R 
12349  645 
proof  
646 
from 3 and 1 have P . 

12368  647 
with 1 have Q by (rule impE) 
12349  648 
with 2 show R . 
649 
qed 

650 

651 
lemma allE': 

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

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

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

654 
shows Q 
12349  655 
proof  
656 
from 1 have "P(x)" by (rule spec) 

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

658 
qed 

659 

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

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

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

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

663 
shows R 
12349  664 
proof  
665 
from 2 and 1 have P . 

666 
with 1 show R by (rule notE) 

667 
qed 

668 

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

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

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

672 
and [Pure.intro] = exI disjI2 disjI1 

673 

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

676 

12368  677 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  678 
by iprover 
12368  679 

680 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

682 

683 

13435  684 
lemma eq_commute: "a=b <> b=a" 
685 
apply (rule iffI) 

686 
apply (erule sym)+ 

687 
done 

688 

689 

11677  690 
subsection {* Atomizing metalevel rules *} 
691 

11747  692 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  693 
proof 
11677  694 
assume "!!x. P(x)" 
22931  695 
then show "ALL x. P(x)" .. 
11677  696 
next 
697 
assume "ALL x. P(x)" 

22931  698 
then show "!!x. P(x)" .. 
11677  699 
qed 
700 

11747  701 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  702 
proof 
12368  703 
assume "A ==> B" 
22931  704 
then show "A > B" .. 
11677  705 
next 
706 
assume "A > B" and A 

22931  707 
then show B by (rule mp) 
11677  708 
qed 
709 

11747  710 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  711 
proof 
11677  712 
assume "x == y" 
22931  713 
show "x = y" unfolding `x == y` by (rule refl) 
11677  714 
next 
715 
assume "x = y" 

22931  716 
then show "x == y" by (rule eq_reflection) 
11677  717 
qed 
718 

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

721 
assume "A == B" 

22931  722 
show "A <> B" unfolding `A == B` by (rule iff_refl) 
18813  723 
next 
724 
assume "A <> B" 

22931  725 
then show "A == B" by (rule iff_reflection) 
18813  726 
qed 
727 

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

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

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

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

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

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

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

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

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

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

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

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

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

743 
from conj show B .. 
11953  744 
qed 
745 
qed 

746 

12368  747 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  748 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  749 

11848  750 

751 
subsection {* Calculational rules *} 

752 

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

754 
by (rule ssubst) 

755 

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

757 
by (rule subst) 

758 

759 
text {* 

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

761 
*} 

762 

12019  763 
lemmas basic_trans_rules [trans] = 
11848  764 
forw_subst 
765 
back_subst 

766 
rev_mp 

767 
mp 

768 
trans 

769 

13779  770 
subsection {* ``Let'' declarations *} 
771 

772 
nonterminals letbinds letbind 

773 

774 
constdefs 

14854  775 
Let :: "['a::{}, 'a => 'b] => ('b::{})" 
13779  776 
"Let(s, f) == f(s)" 
777 

778 
syntax 

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

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

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

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

783 

784 
translations 

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

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

787 

788 

789 
lemma LetI: 

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

792 
apply (unfold Let_def) 

793 
apply (rule refl [THEN assms]) 

794 
done 

795 

796 

797 
subsection {* ML bindings *} 

13779  798 

21539  799 
ML {* 
22139  800 
val refl = @{thm refl} 
801 
val trans = @{thm trans} 

802 
val sym = @{thm sym} 

803 
val subst = @{thm subst} 

804 
val ssubst = @{thm ssubst} 

805 
val conjI = @{thm conjI} 

806 
val conjE = @{thm conjE} 

807 
val conjunct1 = @{thm conjunct1} 

808 
val conjunct2 = @{thm conjunct2} 

809 
val disjI1 = @{thm disjI1} 

810 
val disjI2 = @{thm disjI2} 

811 
val disjE = @{thm disjE} 

812 
val impI = @{thm impI} 

813 
val impE = @{thm impE} 

814 
val mp = @{thm mp} 

815 
val rev_mp = @{thm rev_mp} 

816 
val TrueI = @{thm TrueI} 

817 
val FalseE = @{thm FalseE} 

818 
val iff_refl = @{thm iff_refl} 

819 
val iff_trans = @{thm iff_trans} 

820 
val iffI = @{thm iffI} 

821 
val iffE = @{thm iffE} 

822 
val iffD1 = @{thm iffD1} 

823 
val iffD2 = @{thm iffD2} 

824 
val notI = @{thm notI} 

825 
val notE = @{thm notE} 

826 
val allI = @{thm allI} 

827 
val allE = @{thm allE} 

828 
val spec = @{thm spec} 

829 
val exI = @{thm exI} 

830 
val exE = @{thm exE} 

831 
val eq_reflection = @{thm eq_reflection} 

832 
val iff_reflection = @{thm iff_reflection} 

833 
val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} 

834 
val meta_eq_to_iff = @{thm meta_eq_to_iff} 

13779  835 
*} 
836 

4854  837 
end 