author  wenzelm 
Sun, 08 Jul 2007 19:51:58 +0200  
changeset 23655  d2d1138e0ddc 
parent 23393  31781b2de73d 
child 24097  86734ba03ca2 
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: 

23393  322 
"P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)" 
21539  323 
apply (unfold ex1_def) 
23393  324 
apply (assumption  rule exI conjI allI impI)+ 
21539  325 
done 
326 

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

328 
lemma ex_ex1I: 

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

331 
apply (rule ex1I) 

332 
apply assumption 

333 
apply assumption 

21539  334 
done 
335 

336 
lemma ex1E: 

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

21539  339 
apply (assumption  erule exE conjE)+ 
340 
done 

341 

342 

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

344 

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

346 
ML {* 

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

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

21539  350 
*} 
351 

352 
lemma conj_cong: 

353 
assumes "P <> P'" 

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

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

356 
apply (insert assms) 

357 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

359 
done 

360 

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

362 
lemma conj_cong2: 

363 
assumes "P <> P'" 

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

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

366 
apply (insert assms) 

367 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

369 
done 

370 

371 
lemma disj_cong: 

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

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

374 
apply (insert assms) 

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

376 
done 

377 

378 
lemma imp_cong: 

379 
assumes "P <> P'" 

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

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

382 
apply (insert assms) 

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

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

385 
done 

386 

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

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

389 
done 

390 

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

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

393 
done 

394 

395 
lemma all_cong: 

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

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

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

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

400 
done 

401 

402 
lemma ex_cong: 

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

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

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

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

407 
done 

408 

409 
lemma ex1_cong: 

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

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

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

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

414 
done 

415 

416 
(*** Equality rules ***) 

417 

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

419 
apply (erule subst) 

420 
apply (rule refl) 

421 
done 

422 

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

424 
apply (erule subst, assumption) 

425 
done 

426 

427 
(** **) 

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

429 
apply (erule contrapos) 

430 
apply (erule sym) 

431 
done 

432 

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

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

435 

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

437 
apply unfold 

438 
apply (rule iff_refl) 

439 
done 

440 

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

442 
apply unfold 

443 
apply (rule refl) 

444 
done 

445 

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

447 
by unfold (rule iff_refl) 

448 

449 
(*substitution*) 

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

451 
apply (drule sym) 

452 
apply (erule (1) subst) 

453 
done 

454 

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

456 
lemma ex1_equalsE: 

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

458 
apply (erule ex1E) 

459 
apply (rule trans) 

460 
apply (rule_tac [2] sym) 

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

462 
done 

463 

464 
(** Polymorphic congruence rules **) 

465 

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

467 
apply (erule ssubst) 

468 
apply (rule refl) 

469 
done 

470 

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

472 
apply (erule ssubst)+ 

473 
apply (rule refl) 

474 
done 

475 

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

477 
apply (erule ssubst)+ 

478 
apply (rule refl) 

479 
done 

480 

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

482 
a = b 

483 
  

484 
c = d *) 

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

486 
apply (rule trans) 

487 
apply (rule trans) 

488 
apply (rule sym) 

489 
apply assumption+ 

490 
done 

491 

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

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

494 
apply (rule trans) 

495 
apply (rule trans) 

496 
apply assumption+ 

497 
apply (erule sym) 

498 
done 

499 

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

501 

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

503 
apply (rule iffI) 

504 
apply (erule (1) subst) 

505 
apply (erule (1) ssubst) 

506 
done 

507 

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

509 
apply (rule iffI) 

510 
apply (erule subst)+ 

511 
apply assumption 

512 
apply (erule ssubst)+ 

513 
apply assumption 

514 
done 

515 

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

517 
apply (rule iffI) 

518 
apply (erule subst)+ 

519 
apply assumption 

520 
apply (erule ssubst)+ 

521 
apply assumption 

522 
done 

523 

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

525 

526 
ML {* 

527 
bind_thms ("pred_congs", 

528 
List.concat (map (fn c => 

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

22139  530 
[@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}]) 
21539  531 
(explode"PQRS"))) 
532 
*} 

533 

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

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

536 
apply (erule (1) pred2_cong) 

537 
done 

538 

539 

540 
(*** Simplifications of assumed implications. 

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

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

543 
intuitionistic propositional logic. See 

544 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

546 

547 
lemma conj_impE: 

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

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

550 
shows R 

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

552 

553 
lemma disj_impE: 

554 
assumes major: "(PQ)>S" 

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

556 
shows R 

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

558 

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

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

561 
lemma imp_impE: 

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

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

564 
and r2: "S ==> R" 

565 
shows R 

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

567 

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

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

570 
lemma not_impE: 

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

573 
apply (rule notI) 

574 
apply assumption 

575 
apply assumption 

21539  576 
done 
577 

578 
(*Simplifies the implication. UNSAFE. *) 

579 
lemma iff_impE: 

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

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

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

583 
and r3: "S ==> R" 

584 
shows R 

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

586 
done 

587 

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

589 
lemma all_impE: 

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

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

592 
and r2: "S ==> R" 

593 
shows R 

23393  594 
apply (rule allI impI major [THEN mp] r1 r2)+ 
21539  595 
done 
596 

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

598 
lemma ex_impE: 

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

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

601 
shows R 

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

603 
done 

604 

605 
(*** Courtesy of Krzysztof Grabczewski ***) 

606 

607 
lemma disj_imp_disj: 

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

21539  610 
apply (rule disjI1) apply assumption 
611 
apply (rule disjI2) apply assumption 

612 
done 

11734  613 

18481  614 
ML {* 
615 
structure ProjectRule = ProjectRuleFun 

616 
(struct 

22139  617 
val conjunct1 = @{thm conjunct1} 
618 
val conjunct2 = @{thm conjunct2} 

619 
val mp = @{thm mp} 

18481  620 
end) 
621 
*} 

622 

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

623 
use "fologic.ML" 
21539  624 

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

626 

9886  627 
use "hypsubstdata.ML" 
628 
setup hypsubst_setup 

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

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

630 

4092  631 

12875  632 
subsection {* Intuitionistic Reasoning *} 
12368  633 

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

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

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

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

638 
shows R 
12349  639 
proof  
640 
from 3 and 1 have P . 

12368  641 
with 1 have Q by (rule impE) 
12349  642 
with 2 show R . 
643 
qed 

644 

645 
lemma allE': 

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

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

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

648 
shows Q 
12349  649 
proof  
650 
from 1 have "P(x)" by (rule spec) 

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

652 
qed 

653 

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

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

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

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

657 
shows R 
12349  658 
proof  
659 
from 2 and 1 have P . 

660 
with 1 show R by (rule notE) 

661 
qed 

662 

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

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

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

666 
and [Pure.intro] = exI disjI2 disjI1 

667 

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

670 

12368  671 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  672 
by iprover 
12368  673 

674 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

676 

677 

13435  678 
lemma eq_commute: "a=b <> b=a" 
679 
apply (rule iffI) 

680 
apply (erule sym)+ 

681 
done 

682 

683 

11677  684 
subsection {* Atomizing metalevel rules *} 
685 

11747  686 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  687 
proof 
11677  688 
assume "!!x. P(x)" 
22931  689 
then show "ALL x. P(x)" .. 
11677  690 
next 
691 
assume "ALL x. P(x)" 

22931  692 
then show "!!x. P(x)" .. 
11677  693 
qed 
694 

11747  695 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  696 
proof 
12368  697 
assume "A ==> B" 
22931  698 
then show "A > B" .. 
11677  699 
next 
700 
assume "A > B" and A 

22931  701 
then show B by (rule mp) 
11677  702 
qed 
703 

11747  704 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  705 
proof 
11677  706 
assume "x == y" 
22931  707 
show "x = y" unfolding `x == y` by (rule refl) 
11677  708 
next 
709 
assume "x = y" 

22931  710 
then show "x == y" by (rule eq_reflection) 
11677  711 
qed 
712 

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

715 
assume "A == B" 

22931  716 
show "A <> B" unfolding `A == B` by (rule iff_refl) 
18813  717 
next 
718 
assume "A <> B" 

22931  719 
then show "A == B" by (rule iff_reflection) 
18813  720 
qed 
721 

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

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

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

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

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

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

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

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

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

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

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

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

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

737 
from conj show B .. 
11953  738 
qed 
739 
qed 

740 

12368  741 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  742 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  743 

11848  744 

745 
subsection {* Calculational rules *} 

746 

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

748 
by (rule ssubst) 

749 

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

751 
by (rule subst) 

752 

753 
text {* 

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

755 
*} 

756 

12019  757 
lemmas basic_trans_rules [trans] = 
11848  758 
forw_subst 
759 
back_subst 

760 
rev_mp 

761 
mp 

762 
trans 

763 

13779  764 
subsection {* ``Let'' declarations *} 
765 

766 
nonterminals letbinds letbind 

767 

768 
constdefs 

14854  769 
Let :: "['a::{}, 'a => 'b] => ('b::{})" 
13779  770 
"Let(s, f) == f(s)" 
771 

772 
syntax 

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

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

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

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

777 

778 
translations 

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

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

781 

782 

783 
lemma LetI: 

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

786 
apply (unfold Let_def) 

787 
apply (rule refl [THEN assms]) 

788 
done 

789 

790 

791 
subsection {* ML bindings *} 

13779  792 

21539  793 
ML {* 
22139  794 
val refl = @{thm refl} 
795 
val trans = @{thm trans} 

796 
val sym = @{thm sym} 

797 
val subst = @{thm subst} 

798 
val ssubst = @{thm ssubst} 

799 
val conjI = @{thm conjI} 

800 
val conjE = @{thm conjE} 

801 
val conjunct1 = @{thm conjunct1} 

802 
val conjunct2 = @{thm conjunct2} 

803 
val disjI1 = @{thm disjI1} 

804 
val disjI2 = @{thm disjI2} 

805 
val disjE = @{thm disjE} 

806 
val impI = @{thm impI} 

807 
val impE = @{thm impE} 

808 
val mp = @{thm mp} 

809 
val rev_mp = @{thm rev_mp} 

810 
val TrueI = @{thm TrueI} 

811 
val FalseE = @{thm FalseE} 

812 
val iff_refl = @{thm iff_refl} 

813 
val iff_trans = @{thm iff_trans} 

814 
val iffI = @{thm iffI} 

815 
val iffE = @{thm iffE} 

816 
val iffD1 = @{thm iffD1} 

817 
val iffD2 = @{thm iffD2} 

818 
val notI = @{thm notI} 

819 
val notE = @{thm notE} 

820 
val allI = @{thm allI} 

821 
val allE = @{thm allE} 

822 
val spec = @{thm spec} 

823 
val exI = @{thm exI} 

824 
val exE = @{thm exE} 

825 
val eq_reflection = @{thm eq_reflection} 

826 
val iff_reflection = @{thm iff_reflection} 

827 
val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} 

828 
val meta_eq_to_iff = @{thm meta_eq_to_iff} 

13779  829 
*} 
830 

4854  831 
end 