author  wenzelm 
Sat, 14 May 2011 11:42:43 +0200  
changeset 42799  4e33894aec6d 
parent 42303  5786aa4a9840 
child 44121  44adaa6db327 
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 
10 
"~~/src/Provers/splitter.ML" 

11 
"~~/src/Provers/hypsubst.ML" 

23171  12 
"~~/src/Tools/IsaPlanner/zipper.ML" 
13 
"~~/src/Tools/IsaPlanner/isand.ML" 

14 
"~~/src/Tools/IsaPlanner/rw_tools.ML" 

15 
"~~/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

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

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

19 
"~~/src/Tools/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 
("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 

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

28 
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

29 

14854  30 
classes "term" 
36452  31 
default_sort "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 

41310  44 
eq :: "['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) 
41310  47 
conj :: "[o, o] => o" (infixr "&" 35) 
48 
disj :: "[o, o] => o" (infixr "" 30) 

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

50 
iff :: "[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 
41310  71 
conj (infixr "\<and>" 35) and 
72 
disj (infixr "\<or>" 30) and 

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

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

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

35  78 

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

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

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

6340  86 

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

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

41779  95 

96 
axiomatization where 

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

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

0  101 

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

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

0  105 

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

0  108 

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

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

110 

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

0  115 

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

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

28681  119 

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

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

4092  125 

19756  126 
lemmas strip = impI allI 
127 

128 

14236  129 
defs 
130 
(* Definitions *) 

131 

132 
True_def: "True == False>False" 

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

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

135 

136 
(* Unique existence *) 

137 

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

139 

13779  140 

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

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

145 

146 

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

148 

149 
lemma conjE: 

150 
assumes major: "P & Q" 

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

152 
shows R 

153 
apply (rule r) 

154 
apply (rule major [THEN conjunct1]) 

155 
apply (rule major [THEN conjunct2]) 

156 
done 

157 

158 
lemma impE: 

159 
assumes major: "P > Q" 

160 
and P 

161 
and r: "Q ==> R" 

162 
shows R 

163 
apply (rule r) 

164 
apply (rule major [THEN mp]) 

165 
apply (rule `P`) 

166 
done 

167 

168 
lemma allE: 

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

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

171 
shows R 

172 
apply (rule r) 

173 
apply (rule major [THEN spec]) 

174 
done 

175 

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

177 
lemma all_dupE: 

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

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

180 
shows R 

181 
apply (rule r) 

182 
apply (rule major [THEN spec]) 

183 
apply (rule major) 

184 
done 

185 

186 

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

188 

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

190 
unfolding not_def by (erule impI) 

191 

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

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

194 

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

196 
by (erule notE) 

197 

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

199 
lemma not_to_imp: 

200 
assumes "~P" 

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

202 
shows Q 

203 
apply (rule r) 

204 
apply (rule impI) 

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

206 
done 

207 

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

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

212 

213 
(*Contrapositive of an inference rule*) 

214 
lemma contrapos: 

215 
assumes major: "~Q" 

216 
and minor: "P ==> Q" 

217 
shows "~P" 

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

219 
apply (erule minor) 

220 
done 

221 

222 

223 
(*** Modus Ponens Tactics ***) 

224 

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

226 
ML {* 

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

21539  229 
*} 
230 

231 

232 
(*** Ifandonlyif ***) 

233 

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

235 
apply (unfold iff_def) 

236 
apply (rule conjI) 

237 
apply (erule impI) 

238 
apply (erule impI) 

239 
done 

240 

241 

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

243 
lemma iffE: 

244 
assumes major: "P <> Q" 

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

246 
shows R 

247 
apply (insert major, unfold iff_def) 

248 
apply (erule conjE) 

249 
apply (erule r) 

250 
apply assumption 

251 
done 

252 

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

254 

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

256 
apply (unfold iff_def) 

257 
apply (erule conjunct1 [THEN mp]) 

258 
apply assumption 

259 
done 

260 

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

262 
apply (unfold iff_def) 

263 
apply (erule conjunct2 [THEN mp]) 

264 
apply assumption 

265 
done 

266 

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

268 
apply (erule iffD1) 

269 
apply assumption 

270 
done 

271 

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

273 
apply (erule iffD2) 

274 
apply assumption 

275 
done 

276 

277 
lemma iff_refl: "P <> P" 

278 
by (rule iffI) 

279 

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

281 
apply (erule iffE) 

282 
apply (rule iffI) 

283 
apply (assumption  erule mp)+ 

284 
done 

285 

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

287 
apply (rule iffI) 

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

289 
done 

290 

291 

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

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

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

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

296 
***) 

297 

298 
lemma ex1I: 

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

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

305 
lemma ex_ex1I: 

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

308 
apply (rule ex1I) 

309 
apply assumption 

310 
apply assumption 

21539  311 
done 
312 

313 
lemma ex1E: 

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

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

318 

319 

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

321 

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

323 
ML {* 

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

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

21539  327 
*} 
328 

329 
lemma conj_cong: 

330 
assumes "P <> P'" 

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

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

333 
apply (insert assms) 

334 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

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

339 
lemma conj_cong2: 

340 
assumes "P <> P'" 

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

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

343 
apply (insert assms) 

344 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

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

348 
lemma disj_cong: 

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

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

351 
apply (insert assms) 

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

353 
done 

354 

355 
lemma imp_cong: 

356 
assumes "P <> P'" 

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

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

359 
apply (insert assms) 

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

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

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

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

366 
done 

367 

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

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

370 
done 

371 

372 
lemma all_cong: 

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

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

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

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

379 
lemma ex_cong: 

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

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

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

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

386 
lemma ex1_cong: 

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

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

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

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

393 
(*** Equality rules ***) 

394 

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

396 
apply (erule subst) 

397 
apply (rule refl) 

398 
done 

399 

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

401 
apply (erule subst, assumption) 

402 
done 

403 

404 
(** **) 

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

406 
apply (erule contrapos) 

407 
apply (erule sym) 

408 
done 

409 

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

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

412 

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

414 
apply unfold 

415 
apply (rule iff_refl) 

416 
done 

417 

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

419 
apply unfold 

420 
apply (rule refl) 

421 
done 

422 

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

424 
by unfold (rule iff_refl) 

425 

426 
(*substitution*) 

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

428 
apply (drule sym) 

429 
apply (erule (1) subst) 

430 
done 

431 

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

433 
lemma ex1_equalsE: 

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

435 
apply (erule ex1E) 

436 
apply (rule trans) 

437 
apply (rule_tac [2] sym) 

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

439 
done 

440 

441 
(** Polymorphic congruence rules **) 

442 

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

444 
apply (erule ssubst) 

445 
apply (rule refl) 

446 
done 

447 

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

449 
apply (erule ssubst)+ 

450 
apply (rule refl) 

451 
done 

452 

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

454 
apply (erule ssubst)+ 

455 
apply (rule refl) 

456 
done 

457 

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

459 
a = b 

460 
  

461 
c = d *) 

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

463 
apply (rule trans) 

464 
apply (rule trans) 

465 
apply (rule sym) 

466 
apply assumption+ 

467 
done 

468 

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

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

471 
apply (rule trans) 

472 
apply (rule trans) 

473 
apply assumption+ 

474 
apply (erule sym) 

475 
done 

476 

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

478 

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

480 
apply (rule iffI) 

481 
apply (erule (1) subst) 

482 
apply (erule (1) ssubst) 

483 
done 

484 

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

486 
apply (rule iffI) 

487 
apply (erule subst)+ 

488 
apply assumption 

489 
apply (erule ssubst)+ 

490 
apply assumption 

491 
done 

492 

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

494 
apply (rule iffI) 

495 
apply (erule subst)+ 

496 
apply assumption 

497 
apply (erule ssubst)+ 

498 
apply assumption 

499 
done 

500 

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

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

503 
apply (erule (1) pred2_cong) 

504 
done 

505 

506 

507 
(*** Simplifications of assumed implications. 

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

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

510 
intuitionistic propositional logic. See 

511 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

513 

514 
lemma conj_impE: 

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

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

517 
shows R 

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

519 

520 
lemma disj_impE: 

521 
assumes major: "(PQ)>S" 

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

523 
shows R 

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

525 

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

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

528 
lemma imp_impE: 

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

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

531 
and r2: "S ==> R" 

532 
shows R 

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

534 

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

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

537 
lemma not_impE: 

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

540 
apply (rule notI) 

541 
apply assumption 

542 
apply assumption 

21539  543 
done 
544 

545 
(*Simplifies the implication. UNSAFE. *) 

546 
lemma iff_impE: 

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

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

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

550 
and r3: "S ==> R" 

551 
shows R 

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

553 
done 

554 

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

556 
lemma all_impE: 

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

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

559 
and r2: "S ==> R" 

560 
shows R 

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

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

565 
lemma ex_impE: 

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

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

568 
shows R 

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

570 
done 

571 

572 
(*** Courtesy of Krzysztof Grabczewski ***) 

573 

574 
lemma disj_imp_disj: 

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

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

579 
done 

11734  580 

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

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

586 
val mp = @{thm mp} 

32172  587 
) 
18481  588 
*} 
589 

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

590 
use "fologic.ML" 
21539  591 

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

42799  594 
ML {* 
595 
structure Hypsubst = Hypsubst 

596 
( 

597 
val dest_eq = FOLogic.dest_eq 

598 
val dest_Trueprop = FOLogic.dest_Trueprop 

599 
val dest_imp = FOLogic.dest_imp 

600 
val eq_reflection = @{thm eq_reflection} 

601 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

602 
val imp_intr = @{thm impI} 

603 
val rev_mp = @{thm rev_mp} 

604 
val subst = @{thm subst} 

605 
val sym = @{thm sym} 

606 
val thin_refl = @{thm thin_refl} 

607 
); 

608 
open Hypsubst; 

609 
*} 

610 

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

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

613 

4092  614 

12875  615 
subsection {* Intuitionistic Reasoning *} 
12368  616 

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

618 

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

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

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

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

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

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

629 

630 
lemma allE': 

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

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

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

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

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

637 
qed 

638 

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

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

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

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

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

645 
with 1 show R by (rule notE) 

646 
qed 

647 

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

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

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

651 
and [Pure.intro] = exI disjI2 disjI1 

652 

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

655 

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

659 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

661 

662 

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

665 
apply (erule sym)+ 

666 
done 

667 

668 

11677  669 
subsection {* Atomizing metalevel rules *} 
670 

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

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

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

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

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

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

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

700 
assume "A == B" 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

723 

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

11848  727 

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

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

729 

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

730 
setup AtomizeElim.setup 
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_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

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_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

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

737 

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

738 
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

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

740 

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

741 
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

742 

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

743 

11848  744 
subsection {* Calculational rules *} 
745 

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

747 
by (rule ssubst) 

748 

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

750 
by (rule subst) 

751 

752 
text {* 

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

754 
*} 

755 

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

759 
rev_mp 

760 
mp 

761 
trans 

762 

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

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

765 
nonterminal letbinds and letbind 
13779  766 

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

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

770 
syntax 

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

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

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

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

775 

776 
translations 

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

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

780 

781 
lemma LetI: 

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

784 
apply (unfold Let_def) 

785 
apply (rule refl [THEN assms]) 

786 
done 

787 

788 

26286  789 
subsection {* Intuitionistic simplification rules *} 
790 

791 
lemma conj_simps: 

792 
"P & True <> P" 

793 
"True & P <> P" 

794 
"P & False <> False" 

795 
"False & P <> False" 

796 
"P & P <> P" 

797 
"P & P & Q <> P & Q" 

798 
"P & ~P <> False" 

799 
"~P & P <> False" 

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

801 
by iprover+ 

802 

803 
lemma disj_simps: 

804 
"P  True <> True" 

805 
"True  P <> True" 

806 
"P  False <> P" 

807 
"False  P <> P" 

808 
"P  P <> P" 

809 
"P  P  Q <> P  Q" 

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

811 
by iprover+ 

812 

813 
lemma not_simps: 

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

815 
"~ False <> True" 

816 
"~ True <> False" 

817 
by iprover+ 

818 

819 
lemma imp_simps: 

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

821 
"(P > True) <> True" 

822 
"(False > P) <> True" 

823 
"(True > P) <> P" 

824 
"(P > P) <> True" 

825 
"(P > ~P) <> ~P" 

826 
by iprover+ 

827 

828 
lemma iff_simps: 

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

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

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

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

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

834 
by iprover+ 

835 

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

837 
lemma quant_simps: 

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

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

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

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

842 
"EX x. x=t" 

843 
"EX x. t=x" 

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

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

846 
by iprover+ 

847 

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

849 
lemma distrib_simps: 

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

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

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

853 
by iprover+ 

854 

855 

856 
text {* Conversion into rewrite rules *} 

857 

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

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

860 

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

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

863 

864 

865 
text {* More rewrite rules *} 

866 

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

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

869 
lemmas conj_comms = conj_commute conj_left_commute 

870 

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

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

873 
lemmas disj_comms = disj_commute disj_left_commute 

874 

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

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

877 

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

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

880 

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

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

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

884 

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

886 

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

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

889 

890 
lemma ex_disj_distrib: 

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

892 

893 
lemma all_conj_distrib: 

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

895 

4854  896 
end 