author  blanchet 
Tue, 15 Nov 2011 22:13:39 +0100  
changeset 45509  624872fc47bf 
parent 44121  44adaa6db327 
child 46972  ef6fc1a0884d 
permissions  rwrr 
1268  1 
(* Title: FOL/IFOL.thy 
11677  2 
Author: Lawrence C Paulson and Markus Wenzel 
3 
*) 

35  4 

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

15481  7 
theory IFOL 
8 
imports Pure 

23155  9 
uses 
44121  10 
"~~/src/Tools/misc_legacy.ML" 
23155  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" 

30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
28856
diff
changeset

17 
"~~/src/Tools/eqsubst.ML" 
23155  18 
"~~/src/Provers/quantifier1.ML" 
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

19 
"~~/src/Tools/intuitionistic.ML" 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
28856
diff
changeset

20 
"~~/src/Tools/project_rule.ML" 
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

21 
"~~/src/Tools/atomize_elim.ML" 
23155  22 
("fologic.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 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

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

30 

14854  31 
classes "term" 
36452  32 
default_sort "term" 
0  33 

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

34 
typedecl o 
79  35 

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

0  38 

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

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

41 
False :: o 
79  42 

43 
(* Connectives *) 

44 

41310  45 
eq :: "['a, 'a] => o" (infixl "=" 50) 
35  46 

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

47 
Not :: "o => o" ("~ _" [40] 40) 
41310  48 
conj :: "[o, o] => o" (infixr "&" 35) 
49 
disj :: "[o, o] => o" (infixr "" 30) 

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

51 
iff :: "[o, o] => o" (infixr "<>" 25) 

79  52 

53 
(* Quantifiers *) 

54 

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

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

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

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

0  59 

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

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

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

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

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

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

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

21524  70 
notation (xsymbols) 
21539  71 
Not ("\<not> _" [40] 40) and 
41310  72 
conj (infixr "\<and>" 35) and 
73 
disj (infixr "\<or>" 30) and 

21539  74 
All (binder "\<forall>" 10) and 
75 
Ex (binder "\<exists>" 10) and 

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

41310  77 
imp (infixr "\<longrightarrow>" 25) and 
78 
iff (infixr "\<longleftrightarrow>" 25) 

35  79 

21524  80 
notation (HTML output) 
21539  81 
Not ("\<not> _" [40] 40) and 
41310  82 
conj (infixr "\<and>" 35) and 
83 
disj (infixr "\<or>" 30) and 

21539  84 
All (binder "\<forall>" 10) and 
85 
Ex (binder "\<exists>" 10) and 

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

6340  87 

14236  88 
finalconsts 
41310  89 
False All Ex eq conj disj imp 
14236  90 

41779  91 
axiomatization where 
79  92 
(* Equality *) 
41779  93 
refl: "a=a" and 
28681  94 
subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" 
0  95 

41779  96 

97 
axiomatization where 

79  98 
(* Propositional logic *) 
41779  99 
conjI: "[ P; Q ] ==> P&Q" and 
100 
conjunct1: "P&Q ==> P" and 

101 
conjunct2: "P&Q ==> Q" and 

0  102 

41779  103 
disjI1: "P ==> PQ" and 
104 
disjI2: "Q ==> PQ" and 

105 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" and 

0  106 

41779  107 
impI: "(P ==> Q) ==> P>Q" and 
108 
mp: "[ P>Q; P ] ==> Q" and 

0  109 

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

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

111 

41779  112 
axiomatization where 
79  113 
(* Quantifiers *) 
41779  114 
allI: "(!!x. P(x)) ==> (ALL x. P(x))" and 
115 
spec: "(ALL x. P(x)) ==> P(x)" and 

0  116 

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

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

28681  120 

41779  121 
axiomatization where 
28681  122 
(* Reflection, admissible *) 
41779  123 
eq_reflection: "(x=y) ==> (x==y)" and 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

124 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  125 

4092  126 

19756  127 
lemmas strip = impI allI 
128 

129 

14236  130 
defs 
131 
(* Definitions *) 

132 

133 
True_def: "True == False>False" 

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

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

136 

137 
(* Unique existence *) 

138 

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

140 

13779  141 

11677  142 
subsection {* Lemmas and proof tools *} 
143 

21539  144 
lemma TrueI: True 
145 
unfolding True_def by (rule impI) 

146 

147 

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

149 

150 
lemma conjE: 

151 
assumes major: "P & Q" 

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

153 
shows R 

154 
apply (rule r) 

155 
apply (rule major [THEN conjunct1]) 

156 
apply (rule major [THEN conjunct2]) 

157 
done 

158 

159 
lemma impE: 

160 
assumes major: "P > Q" 

161 
and P 

162 
and r: "Q ==> R" 

163 
shows R 

164 
apply (rule r) 

165 
apply (rule major [THEN mp]) 

166 
apply (rule `P`) 

167 
done 

168 

169 
lemma allE: 

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

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

172 
shows R 

173 
apply (rule r) 

174 
apply (rule major [THEN spec]) 

175 
done 

176 

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

178 
lemma all_dupE: 

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

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

181 
shows R 

182 
apply (rule r) 

183 
apply (rule major [THEN spec]) 

184 
apply (rule major) 

185 
done 

186 

187 

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

189 

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

191 
unfolding not_def by (erule impI) 

192 

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

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

195 

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

197 
by (erule notE) 

198 

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

200 
lemma not_to_imp: 

201 
assumes "~P" 

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

203 
shows Q 

204 
apply (rule r) 

205 
apply (rule impI) 

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

207 
done 

208 

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

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

213 

214 
(*Contrapositive of an inference rule*) 

215 
lemma contrapos: 

216 
assumes major: "~Q" 

217 
and minor: "P ==> Q" 

218 
shows "~P" 

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

220 
apply (erule minor) 

221 
done 

222 

223 

224 
(*** Modus Ponens Tactics ***) 

225 

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

227 
ML {* 

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

21539  230 
*} 
231 

232 

233 
(*** Ifandonlyif ***) 

234 

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

236 
apply (unfold iff_def) 

237 
apply (rule conjI) 

238 
apply (erule impI) 

239 
apply (erule impI) 

240 
done 

241 

242 

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

244 
lemma iffE: 

245 
assumes major: "P <> Q" 

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

247 
shows R 

248 
apply (insert major, unfold iff_def) 

249 
apply (erule conjE) 

250 
apply (erule r) 

251 
apply assumption 

252 
done 

253 

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

255 

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

257 
apply (unfold iff_def) 

258 
apply (erule conjunct1 [THEN mp]) 

259 
apply assumption 

260 
done 

261 

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

263 
apply (unfold iff_def) 

264 
apply (erule conjunct2 [THEN mp]) 

265 
apply assumption 

266 
done 

267 

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

269 
apply (erule iffD1) 

270 
apply assumption 

271 
done 

272 

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

274 
apply (erule iffD2) 

275 
apply assumption 

276 
done 

277 

278 
lemma iff_refl: "P <> P" 

279 
by (rule iffI) 

280 

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

282 
apply (erule iffE) 

283 
apply (rule iffI) 

284 
apply (assumption  erule mp)+ 

285 
done 

286 

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

288 
apply (rule iffI) 

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

290 
done 

291 

292 

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

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

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

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

297 
***) 

298 

299 
lemma ex1I: 

23393  300 
"P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)" 
21539  301 
apply (unfold ex1_def) 
23393  302 
apply (assumption  rule exI conjI allI impI)+ 
21539  303 
done 
304 

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

306 
lemma ex_ex1I: 

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

309 
apply (rule ex1I) 

310 
apply assumption 

311 
apply assumption 

21539  312 
done 
313 

314 
lemma ex1E: 

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

21539  317 
apply (assumption  erule exE conjE)+ 
318 
done 

319 

320 

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

322 

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

324 
ML {* 

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

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

21539  328 
*} 
329 

330 
lemma conj_cong: 

331 
assumes "P <> P'" 

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

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

334 
apply (insert assms) 

335 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  336 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  337 
done 
338 

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

340 
lemma conj_cong2: 

341 
assumes "P <> P'" 

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

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

344 
apply (insert assms) 

345 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  346 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  347 
done 
348 

349 
lemma disj_cong: 

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

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

352 
apply (insert assms) 

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

354 
done 

355 

356 
lemma imp_cong: 

357 
assumes "P <> P'" 

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

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

360 
apply (insert assms) 

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

39159  362 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  363 
done 
364 

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

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

367 
done 

368 

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

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

371 
done 

372 

373 
lemma all_cong: 

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

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

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

39159  377 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  378 
done 
379 

380 
lemma ex_cong: 

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

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

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

39159  384 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  385 
done 
386 

387 
lemma ex1_cong: 

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

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

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

39159  391 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  392 
done 
393 

394 
(*** Equality rules ***) 

395 

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

397 
apply (erule subst) 

398 
apply (rule refl) 

399 
done 

400 

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

402 
apply (erule subst, assumption) 

403 
done 

404 

405 
(** **) 

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

407 
apply (erule contrapos) 

408 
apply (erule sym) 

409 
done 

410 

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

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

413 

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

415 
apply unfold 

416 
apply (rule iff_refl) 

417 
done 

418 

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

420 
apply unfold 

421 
apply (rule refl) 

422 
done 

423 

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

425 
by unfold (rule iff_refl) 

426 

427 
(*substitution*) 

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

429 
apply (drule sym) 

430 
apply (erule (1) subst) 

431 
done 

432 

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

434 
lemma ex1_equalsE: 

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

436 
apply (erule ex1E) 

437 
apply (rule trans) 

438 
apply (rule_tac [2] sym) 

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

440 
done 

441 

442 
(** Polymorphic congruence rules **) 

443 

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

445 
apply (erule ssubst) 

446 
apply (rule refl) 

447 
done 

448 

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

450 
apply (erule ssubst)+ 

451 
apply (rule refl) 

452 
done 

453 

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

455 
apply (erule ssubst)+ 

456 
apply (rule refl) 

457 
done 

458 

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

460 
a = b 

461 
  

462 
c = d *) 

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

464 
apply (rule trans) 

465 
apply (rule trans) 

466 
apply (rule sym) 

467 
apply assumption+ 

468 
done 

469 

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

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

472 
apply (rule trans) 

473 
apply (rule trans) 

474 
apply assumption+ 

475 
apply (erule sym) 

476 
done 

477 

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

479 

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

481 
apply (rule iffI) 

482 
apply (erule (1) subst) 

483 
apply (erule (1) ssubst) 

484 
done 

485 

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

487 
apply (rule iffI) 

488 
apply (erule subst)+ 

489 
apply assumption 

490 
apply (erule ssubst)+ 

491 
apply assumption 

492 
done 

493 

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

495 
apply (rule iffI) 

496 
apply (erule subst)+ 

497 
apply assumption 

498 
apply (erule ssubst)+ 

499 
apply assumption 

500 
done 

501 

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

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

504 
apply (erule (1) pred2_cong) 

505 
done 

506 

507 

508 
(*** Simplifications of assumed implications. 

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

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

511 
intuitionistic propositional logic. See 

512 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

514 

515 
lemma conj_impE: 

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

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

518 
shows R 

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

520 

521 
lemma disj_impE: 

522 
assumes major: "(PQ)>S" 

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

524 
shows R 

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

526 

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

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

529 
lemma imp_impE: 

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

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

532 
and r2: "S ==> R" 

533 
shows R 

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

535 

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

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

538 
lemma not_impE: 

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

541 
apply (rule notI) 

542 
apply assumption 

543 
apply assumption 

21539  544 
done 
545 

546 
(*Simplifies the implication. UNSAFE. *) 

547 
lemma iff_impE: 

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

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

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

551 
and r3: "S ==> R" 

552 
shows R 

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

554 
done 

555 

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

557 
lemma all_impE: 

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

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

560 
and r2: "S ==> R" 

561 
shows R 

23393  562 
apply (rule allI impI major [THEN mp] r1 r2)+ 
21539  563 
done 
564 

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

566 
lemma ex_impE: 

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

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

569 
shows R 

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

571 
done 

572 

573 
(*** Courtesy of Krzysztof Grabczewski ***) 

574 

575 
lemma disj_imp_disj: 

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

21539  578 
apply (rule disjI1) apply assumption 
579 
apply (rule disjI2) apply assumption 

580 
done 

11734  581 

18481  582 
ML {* 
32172  583 
structure Project_Rule = Project_Rule 
584 
( 

22139  585 
val conjunct1 = @{thm conjunct1} 
586 
val conjunct2 = @{thm conjunct2} 

587 
val mp = @{thm mp} 

32172  588 
) 
18481  589 
*} 
590 

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

591 
use "fologic.ML" 
21539  592 

42303  593 
lemma thin_refl: "[x=x; PROP W] ==> PROP W" . 
21539  594 

42799  595 
ML {* 
596 
structure Hypsubst = Hypsubst 

597 
( 

598 
val dest_eq = FOLogic.dest_eq 

599 
val dest_Trueprop = FOLogic.dest_Trueprop 

600 
val dest_imp = FOLogic.dest_imp 

601 
val eq_reflection = @{thm eq_reflection} 

602 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

603 
val imp_intr = @{thm impI} 

604 
val rev_mp = @{thm rev_mp} 

605 
val subst = @{thm subst} 

606 
val sym = @{thm sym} 

607 
val thin_refl = @{thm thin_refl} 

608 
); 

609 
open Hypsubst; 

610 
*} 

611 

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

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

614 

4092  615 

12875  616 
subsection {* Intuitionistic Reasoning *} 
12368  617 

31299  618 
setup {* Intuitionistic.method_setup @{binding iprover} *} 
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

619 

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

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

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

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

624 
shows R 
12349  625 
proof  
626 
from 3 and 1 have P . 

12368  627 
with 1 have Q by (rule impE) 
12349  628 
with 2 show R . 
629 
qed 

630 

631 
lemma allE': 

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

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

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

634 
shows Q 
12349  635 
proof  
636 
from 1 have "P(x)" by (rule spec) 

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

638 
qed 

639 

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

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

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

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

643 
shows R 
12349  644 
proof  
645 
from 2 and 1 have P . 

646 
with 1 show R by (rule notE) 

647 
qed 

648 

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

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

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

652 
and [Pure.intro] = exI disjI2 disjI1 

653 

33369  654 
setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *} 
12349  655 

656 

12368  657 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  658 
by iprover 
12368  659 

660 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

662 

663 

13435  664 
lemma eq_commute: "a=b <> b=a" 
665 
apply (rule iffI) 

666 
apply (erule sym)+ 

667 
done 

668 

669 

11677  670 
subsection {* Atomizing metalevel rules *} 
671 

11747  672 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  673 
proof 
11677  674 
assume "!!x. P(x)" 
22931  675 
then show "ALL x. P(x)" .. 
11677  676 
next 
677 
assume "ALL x. P(x)" 

22931  678 
then show "!!x. P(x)" .. 
11677  679 
qed 
680 

11747  681 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  682 
proof 
12368  683 
assume "A ==> B" 
22931  684 
then show "A > B" .. 
11677  685 
next 
686 
assume "A > B" and A 

22931  687 
then show B by (rule mp) 
11677  688 
qed 
689 

11747  690 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  691 
proof 
11677  692 
assume "x == y" 
22931  693 
show "x = y" unfolding `x == y` by (rule refl) 
11677  694 
next 
695 
assume "x = y" 

22931  696 
then show "x == y" by (rule eq_reflection) 
11677  697 
qed 
698 

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

701 
assume "A == B" 

22931  702 
show "A <> B" unfolding `A == B` by (rule iff_refl) 
18813  703 
next 
704 
assume "A <> B" 

22931  705 
then show "A == B" by (rule iff_reflection) 
18813  706 
qed 
707 

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

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

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

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

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

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

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

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

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

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

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

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

721 
from conj show B .. 
11953  722 
qed 
723 
qed 

724 

12368  725 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  726 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  727 

11848  728 

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

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

730 

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

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

732 

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

733 
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

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

735 

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

736 
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

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

738 

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

739 
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

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

741 

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

742 
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

743 

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

744 

11848  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 

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

766 
nonterminal letbinds and letbind 
13779  767 

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

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

771 
syntax 

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

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

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

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

776 

777 
translations 

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

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

781 

782 
lemma LetI: 

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

785 
apply (unfold Let_def) 

786 
apply (rule refl [THEN assms]) 

787 
done 

788 

789 

26286  790 
subsection {* Intuitionistic simplification rules *} 
791 

792 
lemma conj_simps: 

793 
"P & True <> P" 

794 
"True & P <> P" 

795 
"P & False <> False" 

796 
"False & P <> False" 

797 
"P & P <> P" 

798 
"P & P & Q <> P & Q" 

799 
"P & ~P <> False" 

800 
"~P & P <> False" 

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

802 
by iprover+ 

803 

804 
lemma disj_simps: 

805 
"P  True <> True" 

806 
"True  P <> True" 

807 
"P  False <> P" 

808 
"False  P <> P" 

809 
"P  P <> P" 

810 
"P  P  Q <> P  Q" 

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

812 
by iprover+ 

813 

814 
lemma not_simps: 

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

816 
"~ False <> True" 

817 
"~ True <> False" 

818 
by iprover+ 

819 

820 
lemma imp_simps: 

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

822 
"(P > True) <> True" 

823 
"(False > P) <> True" 

824 
"(True > P) <> P" 

825 
"(P > P) <> True" 

826 
"(P > ~P) <> ~P" 

827 
by iprover+ 

828 

829 
lemma iff_simps: 

830 
"(True <> P) <> P" 

831 
"(P <> True) <> P" 

832 
"(P <> P) <> True" 

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

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

835 
by iprover+ 

836 

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

838 
lemma quant_simps: 

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

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

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

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

843 
"EX x. x=t" 

844 
"EX x. t=x" 

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

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

847 
by iprover+ 

848 

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

850 
lemma distrib_simps: 

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

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

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

854 
by iprover+ 

855 

856 

857 
text {* Conversion into rewrite rules *} 

858 

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

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

861 

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

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

864 

865 

866 
text {* More rewrite rules *} 

867 

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

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

870 
lemmas conj_comms = conj_commute conj_left_commute 

871 

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

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

874 
lemmas disj_comms = disj_commute disj_left_commute 

875 

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

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

878 

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

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

881 

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

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

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

885 

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

887 

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

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

890 

891 
lemma ex_disj_distrib: 

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

893 

894 
lemma all_conj_distrib: 

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

896 

4854  897 
end 