author  wenzelm 
Fri, 02 Oct 2009 22:15:08 +0200  
changeset 32861  105f40051387 
parent 32172  c4e55f30d527 
child 33369  470a7b233ee5 
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 
("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 {* 
32172  594 
structure Project_Rule = Project_Rule 
595 
( 

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

598 
val mp = @{thm mp} 

32172  599 
) 
18481  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 

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

614 

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

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

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

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

619 
shows R 
12349  620 
proof  
621 
from 3 and 1 have P . 

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

625 

626 
lemma allE': 

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

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

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

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

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

633 
qed 

634 

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

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

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

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

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

641 
with 1 show R by (rule notE) 

642 
qed 

643 

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

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

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

647 
and [Pure.intro] = exI disjI2 disjI1 

648 

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

651 

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

655 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

657 

658 

13435  659 
lemma eq_commute: "a=b <> b=a" 
660 
apply (rule iffI) 

661 
apply (erule sym)+ 

662 
done 

663 

664 

11677  665 
subsection {* Atomizing metalevel rules *} 
666 

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

22931  673 
then show "!!x. P(x)" .. 
11677  674 
qed 
675 

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

22931  682 
then show B by (rule mp) 
11677  683 
qed 
684 

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

22931  691 
then show "x == y" by (rule eq_reflection) 
11677  692 
qed 
693 

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

696 
assume "A == B" 

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

22931  700 
then show "A == B" by (rule iff_reflection) 
18813  701 
qed 
702 

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

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

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

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

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

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

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

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

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

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

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

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

716 
from conj show B .. 
11953  717 
qed 
718 
qed 

719 

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

11848  723 

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

724 
subsection {* Atomizing elimination rules *} 
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 
setup AtomizeElim.setup 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset

727 

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

728 
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

729 
by rule iprover+ 
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 
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

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

733 

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

734 
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

735 
by rule iprover+ 
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 
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

738 

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

739 

11848  740 
subsection {* Calculational rules *} 
741 

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

743 
by (rule ssubst) 

744 

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

746 
by (rule subst) 

747 

748 
text {* 

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

750 
*} 

751 

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

755 
rev_mp 

756 
mp 

757 
trans 

758 

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

761 
nonterminals letbinds letbind 

762 

763 
constdefs 

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

767 
syntax 

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

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

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

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

772 

773 
translations 

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

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

776 

777 

778 
lemma LetI: 

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

781 
apply (unfold Let_def) 

782 
apply (rule refl [THEN assms]) 

783 
done 

784 

785 

26286  786 
subsection {* Intuitionistic simplification rules *} 
787 

788 
lemma conj_simps: 

789 
"P & True <> P" 

790 
"True & P <> P" 

791 
"P & False <> False" 

792 
"False & P <> False" 

793 
"P & P <> P" 

794 
"P & P & Q <> P & Q" 

795 
"P & ~P <> False" 

796 
"~P & P <> False" 

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

798 
by iprover+ 

799 

800 
lemma disj_simps: 

801 
"P  True <> True" 

802 
"True  P <> True" 

803 
"P  False <> P" 

804 
"False  P <> P" 

805 
"P  P <> P" 

806 
"P  P  Q <> P  Q" 

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

808 
by iprover+ 

809 

810 
lemma not_simps: 

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

812 
"~ False <> True" 

813 
"~ True <> False" 

814 
by iprover+ 

815 

816 
lemma imp_simps: 

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

818 
"(P > True) <> True" 

819 
"(False > P) <> True" 

820 
"(True > P) <> P" 

821 
"(P > P) <> True" 

822 
"(P > ~P) <> ~P" 

823 
by iprover+ 

824 

825 
lemma iff_simps: 

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

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

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

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

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

831 
by iprover+ 

832 

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

834 
lemma quant_simps: 

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

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

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

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

839 
"EX x. x=t" 

840 
"EX x. t=x" 

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

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

843 
by iprover+ 

844 

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

846 
lemma distrib_simps: 

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

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

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

850 
by iprover+ 

851 

852 

853 
text {* Conversion into rewrite rules *} 

854 

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

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

857 

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

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

860 

861 

862 
text {* More rewrite rules *} 

863 

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

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

866 
lemmas conj_comms = conj_commute conj_left_commute 

867 

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

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

870 
lemmas disj_comms = disj_commute disj_left_commute 

871 

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

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

874 

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

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

877 

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

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

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

881 

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

883 

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

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

886 

887 
lemma ex_disj_distrib: 

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

889 

890 
lemma all_conj_distrib: 

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

892 

893 

894 
subsection {* Legacy ML bindings *} 

13779  895 

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

899 
val sym = @{thm sym} 

900 
val subst = @{thm subst} 

901 
val ssubst = @{thm ssubst} 

902 
val conjI = @{thm conjI} 

903 
val conjE = @{thm conjE} 

904 
val conjunct1 = @{thm conjunct1} 

905 
val conjunct2 = @{thm conjunct2} 

906 
val disjI1 = @{thm disjI1} 

907 
val disjI2 = @{thm disjI2} 

908 
val disjE = @{thm disjE} 

909 
val impI = @{thm impI} 

910 
val impE = @{thm impE} 

911 
val mp = @{thm mp} 

912 
val rev_mp = @{thm rev_mp} 

913 
val TrueI = @{thm TrueI} 

914 
val FalseE = @{thm FalseE} 

915 
val iff_refl = @{thm iff_refl} 

916 
val iff_trans = @{thm iff_trans} 

917 
val iffI = @{thm iffI} 

918 
val iffE = @{thm iffE} 

919 
val iffD1 = @{thm iffD1} 

920 
val iffD2 = @{thm iffD2} 

921 
val notI = @{thm notI} 

922 
val notE = @{thm notE} 

923 
val allI = @{thm allI} 

924 
val allE = @{thm allE} 

925 
val spec = @{thm spec} 

926 
val exI = @{thm exI} 

927 
val exE = @{thm exE} 

928 
val eq_reflection = @{thm eq_reflection} 

929 
val iff_reflection = @{thm iff_reflection} 

930 
val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} 

931 
val meta_eq_to_iff = @{thm meta_eq_to_iff} 

13779  932 
*} 
933 

4854  934 
end 