author  wenzelm 
Sun, 11 Jan 2009 21:49:59 +0100  
changeset 29450  ac7f67be7f1f 
parent 28856  5e009a80fe6d 
child 30160  5f7b17941730 
child 30240  5b25fee0362c 
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" 

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

20 
"~~/src/Tools/atomize_elim.ML" 
23155  21 
("fologic.ML") 
22 
("hypsubstdata.ML") 

23 
("intprover.ML") 

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

25 

0  26 

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

26956
1309a6a0a29f
setup PureThy.old_appl_syntax_setup  theory Pure provides regular application syntax by default;
wenzelm
parents:
26580
diff
changeset

29 
setup PureThy.old_appl_syntax_setup 
1309a6a0a29f
setup PureThy.old_appl_syntax_setup  theory Pure provides regular application syntax by default;
wenzelm
parents:
26580
diff
changeset

30 

3906  31 
global 
32 

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

34 
defaultsort "term" 
0  35 

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

36 
typedecl o 
79  37 

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

0  40 

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

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

43 
False :: o 
79  44 

45 
(* Connectives *) 

46 

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

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

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

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

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

79  54 

55 
(* Quantifiers *) 

56 

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

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

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

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

0  61 

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

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

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

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

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

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

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

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

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

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

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

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

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

35  81 

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

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

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

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

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

6340  89 

3932  90 
local 
3906  91 

14236  92 
finalconsts 
93 
False All Ex 

94 
"op =" 

95 
"op &" 

96 
"op " 

97 
"op >" 

98 

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

99 
axioms 
0  100 

79  101 
(* Equality *) 
0  102 

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

103 
refl: "a=a" 
28681  104 
subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" 
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 

28681  129 

130 
axioms 

131 

132 
(* Reflection, admissible *) 

0  133 

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

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

135 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  136 

4092  137 

19756  138 
lemmas strip = impI allI 
139 

140 

14236  141 
defs 
142 
(* Definitions *) 

143 

144 
True_def: "True == False>False" 

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

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

147 

148 
(* Unique existence *) 

149 

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

151 

13779  152 

11677  153 
subsection {* Lemmas and proof tools *} 
154 

21539  155 
lemma TrueI: True 
156 
unfolding True_def by (rule impI) 

157 

158 

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

160 

161 
lemma conjE: 

162 
assumes major: "P & Q" 

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

164 
shows R 

165 
apply (rule r) 

166 
apply (rule major [THEN conjunct1]) 

167 
apply (rule major [THEN conjunct2]) 

168 
done 

169 

170 
lemma impE: 

171 
assumes major: "P > Q" 

172 
and P 

173 
and r: "Q ==> R" 

174 
shows R 

175 
apply (rule r) 

176 
apply (rule major [THEN mp]) 

177 
apply (rule `P`) 

178 
done 

179 

180 
lemma allE: 

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

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

183 
shows R 

184 
apply (rule r) 

185 
apply (rule major [THEN spec]) 

186 
done 

187 

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

189 
lemma all_dupE: 

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

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

192 
shows R 

193 
apply (rule r) 

194 
apply (rule major [THEN spec]) 

195 
apply (rule major) 

196 
done 

197 

198 

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

200 

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

202 
unfolding not_def by (erule impI) 

203 

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

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

206 

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

208 
by (erule notE) 

209 

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

211 
lemma not_to_imp: 

212 
assumes "~P" 

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

214 
shows Q 

215 
apply (rule r) 

216 
apply (rule impI) 

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

218 
done 

219 

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

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

224 

225 
(*Contrapositive of an inference rule*) 

226 
lemma contrapos: 

227 
assumes major: "~Q" 

228 
and minor: "P ==> Q" 

229 
shows "~P" 

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

231 
apply (erule minor) 

232 
done 

233 

234 

235 
(*** Modus Ponens Tactics ***) 

236 

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

238 
ML {* 

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

21539  241 
*} 
242 

243 

244 
(*** Ifandonlyif ***) 

245 

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

247 
apply (unfold iff_def) 

248 
apply (rule conjI) 

249 
apply (erule impI) 

250 
apply (erule impI) 

251 
done 

252 

253 

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

255 
lemma iffE: 

256 
assumes major: "P <> Q" 

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

258 
shows R 

259 
apply (insert major, unfold iff_def) 

260 
apply (erule conjE) 

261 
apply (erule r) 

262 
apply assumption 

263 
done 

264 

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

266 

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

268 
apply (unfold iff_def) 

269 
apply (erule conjunct1 [THEN mp]) 

270 
apply assumption 

271 
done 

272 

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

274 
apply (unfold iff_def) 

275 
apply (erule conjunct2 [THEN mp]) 

276 
apply assumption 

277 
done 

278 

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

280 
apply (erule iffD1) 

281 
apply assumption 

282 
done 

283 

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

285 
apply (erule iffD2) 

286 
apply assumption 

287 
done 

288 

289 
lemma iff_refl: "P <> P" 

290 
by (rule iffI) 

291 

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

293 
apply (erule iffE) 

294 
apply (rule iffI) 

295 
apply (assumption  erule mp)+ 

296 
done 

297 

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

299 
apply (rule iffI) 

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

301 
done 

302 

303 

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

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

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

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

308 
***) 

309 

310 
lemma ex1I: 

23393  311 
"P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)" 
21539  312 
apply (unfold ex1_def) 
23393  313 
apply (assumption  rule exI conjI allI impI)+ 
21539  314 
done 
315 

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

317 
lemma ex_ex1I: 

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

320 
apply (rule ex1I) 

321 
apply assumption 

322 
apply assumption 

21539  323 
done 
324 

325 
lemma ex1E: 

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

21539  328 
apply (assumption  erule exE conjE)+ 
329 
done 

330 

331 

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

333 

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

335 
ML {* 

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

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

21539  339 
*} 
340 

341 
lemma conj_cong: 

342 
assumes "P <> P'" 

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

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

345 
apply (insert assms) 

346 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

348 
done 

349 

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

351 
lemma conj_cong2: 

352 
assumes "P <> P'" 

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

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

355 
apply (insert assms) 

356 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

358 
done 

359 

360 
lemma disj_cong: 

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

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

363 
apply (insert assms) 

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

365 
done 

366 

367 
lemma imp_cong: 

368 
assumes "P <> P'" 

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

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

371 
apply (insert assms) 

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

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

374 
done 

375 

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

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

378 
done 

379 

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

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

382 
done 

383 

384 
lemma all_cong: 

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

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

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

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

389 
done 

390 

391 
lemma ex_cong: 

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

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

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

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

396 
done 

397 

398 
lemma ex1_cong: 

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

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

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

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

403 
done 

404 

405 
(*** Equality rules ***) 

406 

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

408 
apply (erule subst) 

409 
apply (rule refl) 

410 
done 

411 

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

413 
apply (erule subst, assumption) 

414 
done 

415 

416 
(** **) 

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

418 
apply (erule contrapos) 

419 
apply (erule sym) 

420 
done 

421 

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

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

424 

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

426 
apply unfold 

427 
apply (rule iff_refl) 

428 
done 

429 

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

431 
apply unfold 

432 
apply (rule refl) 

433 
done 

434 

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

436 
by unfold (rule iff_refl) 

437 

438 
(*substitution*) 

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

440 
apply (drule sym) 

441 
apply (erule (1) subst) 

442 
done 

443 

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

445 
lemma ex1_equalsE: 

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

447 
apply (erule ex1E) 

448 
apply (rule trans) 

449 
apply (rule_tac [2] sym) 

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

451 
done 

452 

453 
(** Polymorphic congruence rules **) 

454 

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

456 
apply (erule ssubst) 

457 
apply (rule refl) 

458 
done 

459 

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

461 
apply (erule ssubst)+ 

462 
apply (rule refl) 

463 
done 

464 

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

466 
apply (erule ssubst)+ 

467 
apply (rule refl) 

468 
done 

469 

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

471 
a = b 

472 
  

473 
c = d *) 

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

475 
apply (rule trans) 

476 
apply (rule trans) 

477 
apply (rule sym) 

478 
apply assumption+ 

479 
done 

480 

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

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

483 
apply (rule trans) 

484 
apply (rule trans) 

485 
apply assumption+ 

486 
apply (erule sym) 

487 
done 

488 

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

490 

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

492 
apply (rule iffI) 

493 
apply (erule (1) subst) 

494 
apply (erule (1) ssubst) 

495 
done 

496 

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

498 
apply (rule iffI) 

499 
apply (erule subst)+ 

500 
apply assumption 

501 
apply (erule ssubst)+ 

502 
apply assumption 

503 
done 

504 

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

506 
apply (rule iffI) 

507 
apply (erule subst)+ 

508 
apply assumption 

509 
apply (erule ssubst)+ 

510 
apply assumption 

511 
done 

512 

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

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

515 
apply (erule (1) pred2_cong) 

516 
done 

517 

518 

519 
(*** Simplifications of assumed implications. 

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

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

522 
intuitionistic propositional logic. See 

523 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

525 

526 
lemma conj_impE: 

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

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

529 
shows R 

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

531 

532 
lemma disj_impE: 

533 
assumes major: "(PQ)>S" 

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

535 
shows R 

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

537 

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

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

540 
lemma imp_impE: 

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

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

543 
and r2: "S ==> R" 

544 
shows R 

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

546 

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

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

549 
lemma not_impE: 

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

552 
apply (rule notI) 

553 
apply assumption 

554 
apply assumption 

21539  555 
done 
556 

557 
(*Simplifies the implication. UNSAFE. *) 

558 
lemma iff_impE: 

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

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

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

562 
and r3: "S ==> R" 

563 
shows R 

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

565 
done 

566 

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

568 
lemma all_impE: 

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

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

571 
and r2: "S ==> R" 

572 
shows R 

23393  573 
apply (rule allI impI major [THEN mp] r1 r2)+ 
21539  574 
done 
575 

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

577 
lemma ex_impE: 

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

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

580 
shows R 

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

582 
done 

583 

584 
(*** Courtesy of Krzysztof Grabczewski ***) 

585 

586 
lemma disj_imp_disj: 

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

21539  589 
apply (rule disjI1) apply assumption 
590 
apply (rule disjI2) apply assumption 

591 
done 

11734  592 

18481  593 
ML {* 
594 
structure ProjectRule = ProjectRuleFun 

595 
(struct 

22139  596 
val conjunct1 = @{thm conjunct1} 
597 
val conjunct2 = @{thm conjunct2} 

598 
val mp = @{thm mp} 

18481  599 
end) 
600 
*} 

601 

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

602 
use "fologic.ML" 
21539  603 

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

605 

9886  606 
use "hypsubstdata.ML" 
607 
setup hypsubst_setup 

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

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

609 

4092  610 

12875  611 
subsection {* Intuitionistic Reasoning *} 
12368  612 

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

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

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

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

617 
shows R 
12349  618 
proof  
619 
from 3 and 1 have P . 

12368  620 
with 1 have Q by (rule impE) 
12349  621 
with 2 show R . 
622 
qed 

623 

624 
lemma allE': 

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

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

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

627 
shows Q 
12349  628 
proof  
629 
from 1 have "P(x)" by (rule spec) 

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

631 
qed 

632 

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

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

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

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

636 
shows R 
12349  637 
proof  
638 
from 2 and 1 have P . 

639 
with 1 show R by (rule notE) 

640 
qed 

641 

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

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

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

645 
and [Pure.intro] = exI disjI2 disjI1 

646 

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

649 

12368  650 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  651 
by iprover 
12368  652 

653 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

655 

656 

13435  657 
lemma eq_commute: "a=b <> b=a" 
658 
apply (rule iffI) 

659 
apply (erule sym)+ 

660 
done 

661 

662 

11677  663 
subsection {* Atomizing metalevel rules *} 
664 

11747  665 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  666 
proof 
11677  667 
assume "!!x. P(x)" 
22931  668 
then show "ALL x. P(x)" .. 
11677  669 
next 
670 
assume "ALL x. P(x)" 

22931  671 
then show "!!x. P(x)" .. 
11677  672 
qed 
673 

11747  674 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  675 
proof 
12368  676 
assume "A ==> B" 
22931  677 
then show "A > B" .. 
11677  678 
next 
679 
assume "A > B" and A 

22931  680 
then show B by (rule mp) 
11677  681 
qed 
682 

11747  683 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  684 
proof 
11677  685 
assume "x == y" 
22931  686 
show "x = y" unfolding `x == y` by (rule refl) 
11677  687 
next 
688 
assume "x = y" 

22931  689 
then show "x == y" by (rule eq_reflection) 
11677  690 
qed 
691 

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

694 
assume "A == B" 

22931  695 
show "A <> B" unfolding `A == B` by (rule iff_refl) 
18813  696 
next 
697 
assume "A <> B" 

22931  698 
then show "A == B" by (rule iff_reflection) 
18813  699 
qed 
700 

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

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

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

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

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

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

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

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

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

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

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

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

714 
from conj show B .. 
11953  715 
qed 
716 
qed 

717 

12368  718 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  719 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  720 

11848  721 

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

722 
subsection {* Atomizing elimination rules *} 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

723 

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

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

725 

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

726 
lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

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

728 

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

729 
lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

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

731 

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

732 
lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A  B ==> C) ==> C)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

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

734 

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

735 
lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" .. 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

736 

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

737 

11848  738 
subsection {* Calculational rules *} 
739 

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

741 
by (rule ssubst) 

742 

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

744 
by (rule subst) 

745 

746 
text {* 

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

748 
*} 

749 

12019  750 
lemmas basic_trans_rules [trans] = 
11848  751 
forw_subst 
752 
back_subst 

753 
rev_mp 

754 
mp 

755 
trans 

756 

13779  757 
subsection {* ``Let'' declarations *} 
758 

759 
nonterminals letbinds letbind 

760 

761 
constdefs 

14854  762 
Let :: "['a::{}, 'a => 'b] => ('b::{})" 
13779  763 
"Let(s, f) == f(s)" 
764 

765 
syntax 

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

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

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

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

770 

771 
translations 

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

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

774 

775 

776 
lemma LetI: 

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

779 
apply (unfold Let_def) 

780 
apply (rule refl [THEN assms]) 

781 
done 

782 

783 

26286  784 
subsection {* Intuitionistic simplification rules *} 
785 

786 
lemma conj_simps: 

787 
"P & True <> P" 

788 
"True & P <> P" 

789 
"P & False <> False" 

790 
"False & P <> False" 

791 
"P & P <> P" 

792 
"P & P & Q <> P & Q" 

793 
"P & ~P <> False" 

794 
"~P & P <> False" 

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

796 
by iprover+ 

797 

798 
lemma disj_simps: 

799 
"P  True <> True" 

800 
"True  P <> True" 

801 
"P  False <> P" 

802 
"False  P <> P" 

803 
"P  P <> P" 

804 
"P  P  Q <> P  Q" 

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

806 
by iprover+ 

807 

808 
lemma not_simps: 

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

810 
"~ False <> True" 

811 
"~ True <> False" 

812 
by iprover+ 

813 

814 
lemma imp_simps: 

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

816 
"(P > True) <> True" 

817 
"(False > P) <> True" 

818 
"(True > P) <> P" 

819 
"(P > P) <> True" 

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

821 
by iprover+ 

822 

823 
lemma iff_simps: 

824 
"(True <> P) <> P" 

825 
"(P <> True) <> P" 

826 
"(P <> P) <> True" 

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

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

829 
by iprover+ 

830 

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

832 
lemma quant_simps: 

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

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

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

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

837 
"EX x. x=t" 

838 
"EX x. t=x" 

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

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

841 
by iprover+ 

842 

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

844 
lemma distrib_simps: 

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

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

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

848 
by iprover+ 

849 

850 

851 
text {* Conversion into rewrite rules *} 

852 

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

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

855 

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

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

858 

859 

860 
text {* More rewrite rules *} 

861 

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

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

864 
lemmas conj_comms = conj_commute conj_left_commute 

865 

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

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

868 
lemmas disj_comms = disj_commute disj_left_commute 

869 

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

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

872 

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

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

875 

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

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

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

879 

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

881 

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

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

884 

885 
lemma ex_disj_distrib: 

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

887 

888 
lemma all_conj_distrib: 

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

890 

891 

892 
subsection {* Legacy ML bindings *} 

13779  893 

21539  894 
ML {* 
22139  895 
val refl = @{thm refl} 
896 
val trans = @{thm trans} 

897 
val sym = @{thm sym} 

898 
val subst = @{thm subst} 

899 
val ssubst = @{thm ssubst} 

900 
val conjI = @{thm conjI} 

901 
val conjE = @{thm conjE} 

902 
val conjunct1 = @{thm conjunct1} 

903 
val conjunct2 = @{thm conjunct2} 

904 
val disjI1 = @{thm disjI1} 

905 
val disjI2 = @{thm disjI2} 

906 
val disjE = @{thm disjE} 

907 
val impI = @{thm impI} 

908 
val impE = @{thm impE} 

909 
val mp = @{thm mp} 

910 
val rev_mp = @{thm rev_mp} 

911 
val TrueI = @{thm TrueI} 

912 
val FalseE = @{thm FalseE} 

913 
val iff_refl = @{thm iff_refl} 

914 
val iff_trans = @{thm iff_trans} 

915 
val iffI = @{thm iffI} 

916 
val iffE = @{thm iffE} 

917 
val iffD1 = @{thm iffD1} 

918 
val iffD2 = @{thm iffD2} 

919 
val notI = @{thm notI} 

920 
val notE = @{thm notE} 

921 
val allI = @{thm allI} 

922 
val allE = @{thm allE} 

923 
val spec = @{thm spec} 

924 
val exI = @{thm exI} 

925 
val exE = @{thm exE} 

926 
val eq_reflection = @{thm eq_reflection} 

927 
val iff_reflection = @{thm iff_reflection} 

928 
val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} 

929 
val meta_eq_to_iff = @{thm meta_eq_to_iff} 

13779  930 
*} 
931 

4854  932 
end 