author  wenzelm 
Sat, 15 Mar 2008 22:07:25 +0100  
changeset 26286  3ff5d257f175 
parent 24830  a7b3ab44d993 
child 26580  c3e597a476fd 
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/quantifier1.ML" 

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

20 
("fologic.ML") 

21 
("hypsubstdata.ML") 

22 
("intprover.ML") 

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

24 

0  25 

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

3906  28 
global 
29 

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

31 
defaultsort "term" 
0  32 

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

33 
typedecl o 
79  34 

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

0  37 

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

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

40 
False :: o 
79  41 

42 
(* Connectives *) 

43 

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

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

46 
Not :: "o => o" ("~ _" [40] 40) 
17276  47 
"op &" :: "[o, o] => o" (infixr "&" 35) 
48 
"op " :: "[o, o] => o" (infixr "" 30) 

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

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

79  51 

52 
(* Quantifiers *) 

53 

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

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

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

56 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 
79  57 

0  58 

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

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

61 
"x ~= y == ~ (x = y)" 
79  62 

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

64 
not_equal (infixl "\<noteq>" 50) 
19363  65 

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

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

21524  69 
notation (xsymbols) 
21539  70 
Not ("\<not> _" [40] 40) and 
71 
"op &" (infixr "\<and>" 35) and 

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

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

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

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

21524  76 
"op >" (infixr "\<longrightarrow>" 25) and 
77 
"op <>" (infixr "\<longleftrightarrow>" 25) 

35  78 

21524  79 
notation (HTML output) 
21539  80 
Not ("\<not> _" [40] 40) and 
81 
"op &" (infixr "\<and>" 35) and 

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

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

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

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

6340  86 

3932  87 
local 
3906  88 

14236  89 
finalconsts 
90 
False All Ex 

91 
"op =" 

92 
"op &" 

93 
"op " 

94 
"op >" 

95 

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

96 
axioms 
0  97 

79  98 
(* Equality *) 
0  99 

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

100 
refl: "a=a" 
0  101 

79  102 
(* Propositional logic *) 
0  103 

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

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

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

106 
conjunct2: "P&Q ==> Q" 
0  107 

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

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

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

110 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  111 

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

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

113 
mp: "[ P>Q; P ] ==> Q" 
0  114 

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

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

116 

79  117 
(* Quantifiers *) 
0  118 

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

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

120 
spec: "(ALL x. P(x)) ==> P(x)" 
0  121 

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

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

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

125 
(* Reflection *) 

126 

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

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

128 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  129 

4092  130 

19756  131 
lemmas strip = impI allI 
132 

133 

15377  134 
text{*Thanks to Stephan Merz*} 
135 
theorem subst: 

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

137 
shows "P(b)" 

138 
proof  

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

140 
by (rule eq_reflection) 

141 
from p show ?thesis 

142 
by (unfold meta) 

143 
qed 

144 

145 

14236  146 
defs 
147 
(* Definitions *) 

148 

149 
True_def: "True == False>False" 

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

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

152 

153 
(* Unique existence *) 

154 

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

156 

13779  157 

11677  158 
subsection {* Lemmas and proof tools *} 
159 

21539  160 
lemma TrueI: True 
161 
unfolding True_def by (rule impI) 

162 

163 

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

165 

166 
lemma conjE: 

167 
assumes major: "P & Q" 

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

169 
shows R 

170 
apply (rule r) 

171 
apply (rule major [THEN conjunct1]) 

172 
apply (rule major [THEN conjunct2]) 

173 
done 

174 

175 
lemma impE: 

176 
assumes major: "P > Q" 

177 
and P 

178 
and r: "Q ==> R" 

179 
shows R 

180 
apply (rule r) 

181 
apply (rule major [THEN mp]) 

182 
apply (rule `P`) 

183 
done 

184 

185 
lemma allE: 

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

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

188 
shows R 

189 
apply (rule r) 

190 
apply (rule major [THEN spec]) 

191 
done 

192 

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

194 
lemma all_dupE: 

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

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

197 
shows R 

198 
apply (rule r) 

199 
apply (rule major [THEN spec]) 

200 
apply (rule major) 

201 
done 

202 

203 

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

205 

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

207 
unfolding not_def by (erule impI) 

208 

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

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

211 

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

213 
by (erule notE) 

214 

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

216 
lemma not_to_imp: 

217 
assumes "~P" 

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

219 
shows Q 

220 
apply (rule r) 

221 
apply (rule impI) 

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

223 
done 

224 

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

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

227 
To specify P use something like 

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

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

230 
by (erule mp) 

231 

232 
(*Contrapositive of an inference rule*) 

233 
lemma contrapos: 

234 
assumes major: "~Q" 

235 
and minor: "P ==> Q" 

236 
shows "~P" 

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

238 
apply (erule minor) 

239 
done 

240 

241 

242 
(*** Modus Ponens Tactics ***) 

243 

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

245 
ML {* 

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

21539  248 
*} 
249 

250 

251 
(*** Ifandonlyif ***) 

252 

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

254 
apply (unfold iff_def) 

255 
apply (rule conjI) 

256 
apply (erule impI) 

257 
apply (erule impI) 

258 
done 

259 

260 

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

262 
lemma iffE: 

263 
assumes major: "P <> Q" 

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

265 
shows R 

266 
apply (insert major, unfold iff_def) 

267 
apply (erule conjE) 

268 
apply (erule r) 

269 
apply assumption 

270 
done 

271 

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

273 

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

275 
apply (unfold iff_def) 

276 
apply (erule conjunct1 [THEN mp]) 

277 
apply assumption 

278 
done 

279 

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

281 
apply (unfold iff_def) 

282 
apply (erule conjunct2 [THEN mp]) 

283 
apply assumption 

284 
done 

285 

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

287 
apply (erule iffD1) 

288 
apply assumption 

289 
done 

290 

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

292 
apply (erule iffD2) 

293 
apply assumption 

294 
done 

295 

296 
lemma iff_refl: "P <> P" 

297 
by (rule iffI) 

298 

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

300 
apply (erule iffE) 

301 
apply (rule iffI) 

302 
apply (assumption  erule mp)+ 

303 
done 

304 

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

306 
apply (rule iffI) 

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

308 
done 

309 

310 

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

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

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

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

315 
***) 

316 

317 
lemma ex1I: 

23393  318 
"P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)" 
21539  319 
apply (unfold ex1_def) 
23393  320 
apply (assumption  rule exI conjI allI impI)+ 
21539  321 
done 
322 

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

324 
lemma ex_ex1I: 

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

327 
apply (rule ex1I) 

328 
apply assumption 

329 
apply assumption 

21539  330 
done 
331 

332 
lemma ex1E: 

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

21539  335 
apply (assumption  erule exE conjE)+ 
336 
done 

337 

338 

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

340 

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

342 
ML {* 

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

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

21539  346 
*} 
347 

348 
lemma conj_cong: 

349 
assumes "P <> P'" 

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

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

352 
apply (insert assms) 

353 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

355 
done 

356 

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

358 
lemma conj_cong2: 

359 
assumes "P <> P'" 

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

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

362 
apply (insert assms) 

363 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

365 
done 

366 

367 
lemma disj_cong: 

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

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

370 
apply (insert assms) 

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

372 
done 

373 

374 
lemma imp_cong: 

375 
assumes "P <> P'" 

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

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

378 
apply (insert assms) 

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

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

381 
done 

382 

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

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

385 
done 

386 

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

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

389 
done 

390 

391 
lemma all_cong: 

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

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

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

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

396 
done 

397 

398 
lemma ex_cong: 

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

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

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

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

403 
done 

404 

405 
lemma ex1_cong: 

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

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

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

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

410 
done 

411 

412 
(*** Equality rules ***) 

413 

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

415 
apply (erule subst) 

416 
apply (rule refl) 

417 
done 

418 

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

420 
apply (erule subst, assumption) 

421 
done 

422 

423 
(** **) 

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

425 
apply (erule contrapos) 

426 
apply (erule sym) 

427 
done 

428 

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

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

431 

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

433 
apply unfold 

434 
apply (rule iff_refl) 

435 
done 

436 

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

438 
apply unfold 

439 
apply (rule refl) 

440 
done 

441 

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

443 
by unfold (rule iff_refl) 

444 

445 
(*substitution*) 

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

447 
apply (drule sym) 

448 
apply (erule (1) subst) 

449 
done 

450 

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

452 
lemma ex1_equalsE: 

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

454 
apply (erule ex1E) 

455 
apply (rule trans) 

456 
apply (rule_tac [2] sym) 

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

458 
done 

459 

460 
(** Polymorphic congruence rules **) 

461 

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

463 
apply (erule ssubst) 

464 
apply (rule refl) 

465 
done 

466 

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

468 
apply (erule ssubst)+ 

469 
apply (rule refl) 

470 
done 

471 

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

473 
apply (erule ssubst)+ 

474 
apply (rule refl) 

475 
done 

476 

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

478 
a = b 

479 
  

480 
c = d *) 

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

482 
apply (rule trans) 

483 
apply (rule trans) 

484 
apply (rule sym) 

485 
apply assumption+ 

486 
done 

487 

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

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

490 
apply (rule trans) 

491 
apply (rule trans) 

492 
apply assumption+ 

493 
apply (erule sym) 

494 
done 

495 

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

497 

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

499 
apply (rule iffI) 

500 
apply (erule (1) subst) 

501 
apply (erule (1) ssubst) 

502 
done 

503 

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

505 
apply (rule iffI) 

506 
apply (erule subst)+ 

507 
apply assumption 

508 
apply (erule ssubst)+ 

509 
apply assumption 

510 
done 

511 

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

513 
apply (rule iffI) 

514 
apply (erule subst)+ 

515 
apply assumption 

516 
apply (erule ssubst)+ 

517 
apply assumption 

518 
done 

519 

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

521 

522 
ML {* 

523 
bind_thms ("pred_congs", 

524 
List.concat (map (fn c => 

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

22139  526 
[@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}]) 
21539  527 
(explode"PQRS"))) 
528 
*} 

529 

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

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

532 
apply (erule (1) pred2_cong) 

533 
done 

534 

535 

536 
(*** Simplifications of assumed implications. 

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

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

539 
intuitionistic propositional logic. See 

540 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

542 

543 
lemma conj_impE: 

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

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

546 
shows R 

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

548 

549 
lemma disj_impE: 

550 
assumes major: "(PQ)>S" 

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

552 
shows R 

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

554 

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

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

557 
lemma imp_impE: 

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

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

560 
and r2: "S ==> R" 

561 
shows R 

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

563 

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

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

566 
lemma not_impE: 

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

569 
apply (rule notI) 

570 
apply assumption 

571 
apply assumption 

21539  572 
done 
573 

574 
(*Simplifies the implication. UNSAFE. *) 

575 
lemma iff_impE: 

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

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

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

579 
and r3: "S ==> R" 

580 
shows R 

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

582 
done 

583 

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

585 
lemma all_impE: 

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

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

588 
and r2: "S ==> R" 

589 
shows R 

23393  590 
apply (rule allI impI major [THEN mp] r1 r2)+ 
21539  591 
done 
592 

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

594 
lemma ex_impE: 

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

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

597 
shows R 

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

599 
done 

600 

601 
(*** Courtesy of Krzysztof Grabczewski ***) 

602 

603 
lemma disj_imp_disj: 

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

21539  606 
apply (rule disjI1) apply assumption 
607 
apply (rule disjI2) apply assumption 

608 
done 

11734  609 

18481  610 
ML {* 
611 
structure ProjectRule = ProjectRuleFun 

612 
(struct 

22139  613 
val conjunct1 = @{thm conjunct1} 
614 
val conjunct2 = @{thm conjunct2} 

615 
val mp = @{thm mp} 

18481  616 
end) 
617 
*} 

618 

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

619 
use "fologic.ML" 
21539  620 

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

622 

9886  623 
use "hypsubstdata.ML" 
624 
setup hypsubst_setup 

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

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

626 

4092  627 

12875  628 
subsection {* Intuitionistic Reasoning *} 
12368  629 

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

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

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

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

634 
shows R 
12349  635 
proof  
636 
from 3 and 1 have P . 

12368  637 
with 1 have Q by (rule impE) 
12349  638 
with 2 show R . 
639 
qed 

640 

641 
lemma allE': 

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

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

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

644 
shows Q 
12349  645 
proof  
646 
from 1 have "P(x)" by (rule spec) 

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

648 
qed 

649 

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

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

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

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

653 
shows R 
12349  654 
proof  
655 
from 2 and 1 have P . 

656 
with 1 show R by (rule notE) 

657 
qed 

658 

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

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

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

662 
and [Pure.intro] = exI disjI2 disjI1 

663 

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

666 

12368  667 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  668 
by iprover 
12368  669 

670 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

672 

673 

13435  674 
lemma eq_commute: "a=b <> b=a" 
675 
apply (rule iffI) 

676 
apply (erule sym)+ 

677 
done 

678 

679 

11677  680 
subsection {* Atomizing metalevel rules *} 
681 

11747  682 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  683 
proof 
11677  684 
assume "!!x. P(x)" 
22931  685 
then show "ALL x. P(x)" .. 
11677  686 
next 
687 
assume "ALL x. P(x)" 

22931  688 
then show "!!x. P(x)" .. 
11677  689 
qed 
690 

11747  691 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  692 
proof 
12368  693 
assume "A ==> B" 
22931  694 
then show "A > B" .. 
11677  695 
next 
696 
assume "A > B" and A 

22931  697 
then show B by (rule mp) 
11677  698 
qed 
699 

11747  700 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  701 
proof 
11677  702 
assume "x == y" 
22931  703 
show "x = y" unfolding `x == y` by (rule refl) 
11677  704 
next 
705 
assume "x = y" 

22931  706 
then show "x == y" by (rule eq_reflection) 
11677  707 
qed 
708 

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

711 
assume "A == B" 

22931  712 
show "A <> B" unfolding `A == B` by (rule iff_refl) 
18813  713 
next 
714 
assume "A <> B" 

22931  715 
then show "A == B" by (rule iff_reflection) 
18813  716 
qed 
717 

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

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

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

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

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

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

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

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

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

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

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

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

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

733 
from conj show B .. 
11953  734 
qed 
735 
qed 

736 

12368  737 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  738 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  739 

11848  740 

741 
subsection {* Calculational rules *} 

742 

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

744 
by (rule ssubst) 

745 

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

747 
by (rule subst) 

748 

749 
text {* 

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

751 
*} 

752 

12019  753 
lemmas basic_trans_rules [trans] = 
11848  754 
forw_subst 
755 
back_subst 

756 
rev_mp 

757 
mp 

758 
trans 

759 

13779  760 
subsection {* ``Let'' declarations *} 
761 

762 
nonterminals letbinds letbind 

763 

764 
constdefs 

14854  765 
Let :: "['a::{}, 'a => 'b] => ('b::{})" 
13779  766 
"Let(s, f) == f(s)" 
767 

768 
syntax 

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

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

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

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

773 

774 
translations 

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

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

777 

778 

779 
lemma LetI: 

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

782 
apply (unfold Let_def) 

783 
apply (rule refl [THEN assms]) 

784 
done 

785 

786 

26286  787 
subsection {* Intuitionistic simplification rules *} 
788 

789 
lemma conj_simps: 

790 
"P & True <> P" 

791 
"True & P <> P" 

792 
"P & False <> False" 

793 
"False & P <> False" 

794 
"P & P <> P" 

795 
"P & P & Q <> P & Q" 

796 
"P & ~P <> False" 

797 
"~P & P <> False" 

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

799 
by iprover+ 

800 

801 
lemma disj_simps: 

802 
"P  True <> True" 

803 
"True  P <> True" 

804 
"P  False <> P" 

805 
"False  P <> P" 

806 
"P  P <> P" 

807 
"P  P  Q <> P  Q" 

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

809 
by iprover+ 

810 

811 
lemma not_simps: 

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

813 
"~ False <> True" 

814 
"~ True <> False" 

815 
by iprover+ 

816 

817 
lemma imp_simps: 

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

819 
"(P > True) <> True" 

820 
"(False > P) <> True" 

821 
"(True > P) <> P" 

822 
"(P > P) <> True" 

823 
"(P > ~P) <> ~P" 

824 
by iprover+ 

825 

826 
lemma iff_simps: 

827 
"(True <> P) <> P" 

828 
"(P <> True) <> P" 

829 
"(P <> P) <> True" 

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

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

832 
by iprover+ 

833 

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

835 
lemma quant_simps: 

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

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

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

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

840 
"EX x. x=t" 

841 
"EX x. t=x" 

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

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

844 
by iprover+ 

845 

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

847 
lemma distrib_simps: 

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

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

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

851 
by iprover+ 

852 

853 

854 
text {* Conversion into rewrite rules *} 

855 

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

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

858 

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

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

861 

862 

863 
text {* More rewrite rules *} 

864 

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

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

867 
lemmas conj_comms = conj_commute conj_left_commute 

868 

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

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

871 
lemmas disj_comms = disj_commute disj_left_commute 

872 

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

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

875 

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

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

878 

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

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

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

882 

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

884 

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

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

887 

888 
lemma ex_disj_distrib: 

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

890 

891 
lemma all_conj_distrib: 

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

893 

894 

895 
subsection {* Legacy ML bindings *} 

13779  896 

21539  897 
ML {* 
22139  898 
val refl = @{thm refl} 
899 
val trans = @{thm trans} 

900 
val sym = @{thm sym} 

901 
val subst = @{thm subst} 

902 
val ssubst = @{thm ssubst} 

903 
val conjI = @{thm conjI} 

904 
val conjE = @{thm conjE} 

905 
val conjunct1 = @{thm conjunct1} 

906 
val conjunct2 = @{thm conjunct2} 

907 
val disjI1 = @{thm disjI1} 

908 
val disjI2 = @{thm disjI2} 

909 
val disjE = @{thm disjE} 

910 
val impI = @{thm impI} 

911 
val impE = @{thm impE} 

912 
val mp = @{thm mp} 

913 
val rev_mp = @{thm rev_mp} 

914 
val TrueI = @{thm TrueI} 

915 
val FalseE = @{thm FalseE} 

916 
val iff_refl = @{thm iff_refl} 

917 
val iff_trans = @{thm iff_trans} 

918 
val iffI = @{thm iffI} 

919 
val iffE = @{thm iffE} 

920 
val iffD1 = @{thm iffD1} 

921 
val iffD2 = @{thm iffD2} 

922 
val notI = @{thm notI} 

923 
val notE = @{thm notE} 

924 
val allI = @{thm allI} 

925 
val allE = @{thm allE} 

926 
val spec = @{thm spec} 

927 
val exI = @{thm exI} 

928 
val exE = @{thm exE} 

929 
val eq_reflection = @{thm eq_reflection} 

930 
val iff_reflection = @{thm iff_reflection} 

931 
val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} 

932 
val meta_eq_to_iff = @{thm meta_eq_to_iff} 

13779  933 
*} 
934 

4854  935 
end 