author  wenzelm 
Wed, 03 Nov 2010 21:53:56 +0100  
changeset 40335  3e4bb6e7c3ca 
parent 39557  fe5722fce758 
child 41229  d797baa3d57c 
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 

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 

17276  45 
"op =" :: "['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) 
17276  48 
"op &" :: "[o, o] => o" (infixr "&" 35) 
49 
"op " :: "[o, o] => o" (infixr "" 30) 

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

51 
"op <>" :: "[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 
72 
"op &" (infixr "\<and>" 35) and 

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

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

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

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

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

35  79 

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

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

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

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

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

6340  87 

14236  88 
finalconsts 
89 
False All Ex 

90 
"op =" 

91 
"op &" 

92 
"op " 

93 
"op >" 

94 

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

95 
axioms 
0  96 

79  97 
(* Equality *) 
0  98 

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

99 
refl: "a=a" 
28681  100 
subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" 
0  101 

79  102 
(* Propositional logic *) 
0  103 

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

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

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

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

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

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

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

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

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

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

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

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

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

116 

79  117 
(* Quantifiers *) 
0  118 

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

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

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

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

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

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

28681  125 

126 
axioms 

127 

128 
(* Reflection, admissible *) 

0  129 

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

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

131 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  132 

4092  133 

19756  134 
lemmas strip = impI allI 
135 

136 

14236  137 
defs 
138 
(* Definitions *) 

139 

140 
True_def: "True == False>False" 

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

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

143 

144 
(* Unique existence *) 

145 

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

147 

13779  148 

11677  149 
subsection {* Lemmas and proof tools *} 
150 

21539  151 
lemma TrueI: True 
152 
unfolding True_def by (rule impI) 

153 

154 

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

156 

157 
lemma conjE: 

158 
assumes major: "P & Q" 

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

160 
shows R 

161 
apply (rule r) 

162 
apply (rule major [THEN conjunct1]) 

163 
apply (rule major [THEN conjunct2]) 

164 
done 

165 

166 
lemma impE: 

167 
assumes major: "P > Q" 

168 
and P 

169 
and r: "Q ==> R" 

170 
shows R 

171 
apply (rule r) 

172 
apply (rule major [THEN mp]) 

173 
apply (rule `P`) 

174 
done 

175 

176 
lemma allE: 

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

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

179 
shows R 

180 
apply (rule r) 

181 
apply (rule major [THEN spec]) 

182 
done 

183 

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

185 
lemma all_dupE: 

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

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

188 
shows R 

189 
apply (rule r) 

190 
apply (rule major [THEN spec]) 

191 
apply (rule major) 

192 
done 

193 

194 

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

196 

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

198 
unfolding not_def by (erule impI) 

199 

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

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

202 

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

204 
by (erule notE) 

205 

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

207 
lemma not_to_imp: 

208 
assumes "~P" 

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

210 
shows Q 

211 
apply (rule r) 

212 
apply (rule impI) 

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

214 
done 

215 

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

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

220 

221 
(*Contrapositive of an inference rule*) 

222 
lemma contrapos: 

223 
assumes major: "~Q" 

224 
and minor: "P ==> Q" 

225 
shows "~P" 

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

227 
apply (erule minor) 

228 
done 

229 

230 

231 
(*** Modus Ponens Tactics ***) 

232 

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

234 
ML {* 

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

21539  237 
*} 
238 

239 

240 
(*** Ifandonlyif ***) 

241 

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

243 
apply (unfold iff_def) 

244 
apply (rule conjI) 

245 
apply (erule impI) 

246 
apply (erule impI) 

247 
done 

248 

249 

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

251 
lemma iffE: 

252 
assumes major: "P <> Q" 

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

254 
shows R 

255 
apply (insert major, unfold iff_def) 

256 
apply (erule conjE) 

257 
apply (erule r) 

258 
apply assumption 

259 
done 

260 

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

262 

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

264 
apply (unfold iff_def) 

265 
apply (erule conjunct1 [THEN mp]) 

266 
apply assumption 

267 
done 

268 

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

270 
apply (unfold iff_def) 

271 
apply (erule conjunct2 [THEN mp]) 

272 
apply assumption 

273 
done 

274 

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

276 
apply (erule iffD1) 

277 
apply assumption 

278 
done 

279 

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

281 
apply (erule iffD2) 

282 
apply assumption 

283 
done 

284 

285 
lemma iff_refl: "P <> P" 

286 
by (rule iffI) 

287 

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

289 
apply (erule iffE) 

290 
apply (rule iffI) 

291 
apply (assumption  erule mp)+ 

292 
done 

293 

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

295 
apply (rule iffI) 

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

297 
done 

298 

299 

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

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

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

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

304 
***) 

305 

306 
lemma ex1I: 

23393  307 
"P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)" 
21539  308 
apply (unfold ex1_def) 
23393  309 
apply (assumption  rule exI conjI allI impI)+ 
21539  310 
done 
311 

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

313 
lemma ex_ex1I: 

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

316 
apply (rule ex1I) 

317 
apply assumption 

318 
apply assumption 

21539  319 
done 
320 

321 
lemma ex1E: 

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

21539  324 
apply (assumption  erule exE conjE)+ 
325 
done 

326 

327 

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

329 

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

331 
ML {* 

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

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

21539  335 
*} 
336 

337 
lemma conj_cong: 

338 
assumes "P <> P'" 

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

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

341 
apply (insert assms) 

342 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  343 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  344 
done 
345 

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

347 
lemma conj_cong2: 

348 
assumes "P <> P'" 

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

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

351 
apply (insert assms) 

352 
apply (assumption  rule iffI conjI  erule iffE conjE mp  

39159  353 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  354 
done 
355 

356 
lemma disj_cong: 

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

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

359 
apply (insert assms) 

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

361 
done 

362 

363 
lemma imp_cong: 

364 
assumes "P <> P'" 

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

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

367 
apply (insert assms) 

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

39159  369 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  370 
done 
371 

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

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

374 
done 

375 

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

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

378 
done 

379 

380 
lemma all_cong: 

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

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

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

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

387 
lemma ex_cong: 

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

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

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

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

394 
lemma ex1_cong: 

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

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

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

39159  398 
tactic {* iff_tac @{thms assms} 1 *})+ 
21539  399 
done 
400 

401 
(*** Equality rules ***) 

402 

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

404 
apply (erule subst) 

405 
apply (rule refl) 

406 
done 

407 

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

409 
apply (erule subst, assumption) 

410 
done 

411 

412 
(** **) 

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

414 
apply (erule contrapos) 

415 
apply (erule sym) 

416 
done 

417 

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

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

420 

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

422 
apply unfold 

423 
apply (rule iff_refl) 

424 
done 

425 

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

427 
apply unfold 

428 
apply (rule refl) 

429 
done 

430 

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

432 
by unfold (rule iff_refl) 

433 

434 
(*substitution*) 

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

436 
apply (drule sym) 

437 
apply (erule (1) subst) 

438 
done 

439 

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

441 
lemma ex1_equalsE: 

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

443 
apply (erule ex1E) 

444 
apply (rule trans) 

445 
apply (rule_tac [2] sym) 

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

447 
done 

448 

449 
(** Polymorphic congruence rules **) 

450 

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

452 
apply (erule ssubst) 

453 
apply (rule refl) 

454 
done 

455 

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

457 
apply (erule ssubst)+ 

458 
apply (rule refl) 

459 
done 

460 

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

462 
apply (erule ssubst)+ 

463 
apply (rule refl) 

464 
done 

465 

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

467 
a = b 

468 
  

469 
c = d *) 

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

471 
apply (rule trans) 

472 
apply (rule trans) 

473 
apply (rule sym) 

474 
apply assumption+ 

475 
done 

476 

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

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

479 
apply (rule trans) 

480 
apply (rule trans) 

481 
apply assumption+ 

482 
apply (erule sym) 

483 
done 

484 

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

486 

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

488 
apply (rule iffI) 

489 
apply (erule (1) subst) 

490 
apply (erule (1) ssubst) 

491 
done 

492 

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

494 
apply (rule iffI) 

495 
apply (erule subst)+ 

496 
apply assumption 

497 
apply (erule ssubst)+ 

498 
apply assumption 

499 
done 

500 

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

502 
apply (rule iffI) 

503 
apply (erule subst)+ 

504 
apply assumption 

505 
apply (erule ssubst)+ 

506 
apply assumption 

507 
done 

508 

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

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

511 
apply (erule (1) pred2_cong) 

512 
done 

513 

514 

515 
(*** Simplifications of assumed implications. 

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

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

518 
intuitionistic propositional logic. See 

519 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

521 

522 
lemma conj_impE: 

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

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

525 
shows R 

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

527 

528 
lemma disj_impE: 

529 
assumes major: "(PQ)>S" 

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

531 
shows R 

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

533 

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

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

536 
lemma imp_impE: 

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

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

539 
and r2: "S ==> R" 

540 
shows R 

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

542 

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

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

545 
lemma not_impE: 

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

548 
apply (rule notI) 

549 
apply assumption 

550 
apply assumption 

21539  551 
done 
552 

553 
(*Simplifies the implication. UNSAFE. *) 

554 
lemma iff_impE: 

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

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

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

558 
and r3: "S ==> R" 

559 
shows R 

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

561 
done 

562 

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

564 
lemma all_impE: 

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

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

567 
and r2: "S ==> R" 

568 
shows R 

23393  569 
apply (rule allI impI major [THEN mp] r1 r2)+ 
21539  570 
done 
571 

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

573 
lemma ex_impE: 

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

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

576 
shows R 

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

578 
done 

579 

580 
(*** Courtesy of Krzysztof Grabczewski ***) 

581 

582 
lemma disj_imp_disj: 

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

21539  585 
apply (rule disjI1) apply assumption 
586 
apply (rule disjI2) apply assumption 

587 
done 

11734  588 

18481  589 
ML {* 
32172  590 
structure Project_Rule = Project_Rule 
591 
( 

22139  592 
val conjunct1 = @{thm conjunct1} 
593 
val conjunct2 = @{thm conjunct2} 

594 
val mp = @{thm mp} 

32172  595 
) 
18481  596 
*} 
597 

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

598 
use "fologic.ML" 
21539  599 

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

601 

9886  602 
use "hypsubstdata.ML" 
603 
setup hypsubst_setup 

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

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

605 

4092  606 

12875  607 
subsection {* Intuitionistic Reasoning *} 
12368  608 

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

610 

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

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

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

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

615 
shows R 
12349  616 
proof  
617 
from 3 and 1 have P . 

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

621 

622 
lemma allE': 

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

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

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

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

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

629 
qed 

630 

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

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

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

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

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

637 
with 1 show R by (rule notE) 

638 
qed 

639 

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

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

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

643 
and [Pure.intro] = exI disjI2 disjI1 

644 

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

647 

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

651 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

653 

654 

13435  655 
lemma eq_commute: "a=b <> b=a" 
656 
apply (rule iffI) 

657 
apply (erule sym)+ 

658 
done 

659 

660 

11677  661 
subsection {* Atomizing metalevel rules *} 
662 

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

22931  669 
then show "!!x. P(x)" .. 
11677  670 
qed 
671 

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

22931  678 
then show B by (rule mp) 
11677  679 
qed 
680 

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

22931  687 
then show "x == y" by (rule eq_reflection) 
11677  688 
qed 
689 

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

692 
assume "A == B" 

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

22931  696 
then show "A == B" by (rule iff_reflection) 
18813  697 
qed 
698 

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

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

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

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

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

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

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

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

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

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

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

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

712 
from conj show B .. 
11953  713 
qed 
714 
qed 

715 

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

11848  719 

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

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

721 

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

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

723 

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

724 
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

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

726 

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

727 
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

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

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

734 

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

735 

11848  736 
subsection {* Calculational rules *} 
737 

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

739 
by (rule ssubst) 

740 

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

742 
by (rule subst) 

743 

744 
text {* 

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

746 
*} 

747 

12019  748 
lemmas basic_trans_rules [trans] = 
11848  749 
forw_subst 
750 
back_subst 

751 
rev_mp 

752 
mp 

753 
trans 

754 

13779  755 
subsection {* ``Let'' declarations *} 
756 

757 
nonterminals letbinds letbind 

758 

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

759 
definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where 
13779  760 
"Let(s, f) == f(s)" 
761 

762 
syntax 

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

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

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

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

767 

768 
translations 

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

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

772 

773 
lemma LetI: 

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

776 
apply (unfold Let_def) 

777 
apply (rule refl [THEN assms]) 

778 
done 

779 

780 

26286  781 
subsection {* Intuitionistic simplification rules *} 
782 

783 
lemma conj_simps: 

784 
"P & True <> P" 

785 
"True & P <> P" 

786 
"P & False <> False" 

787 
"False & P <> False" 

788 
"P & P <> P" 

789 
"P & P & Q <> P & Q" 

790 
"P & ~P <> False" 

791 
"~P & P <> False" 

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

793 
by iprover+ 

794 

795 
lemma disj_simps: 

796 
"P  True <> True" 

797 
"True  P <> True" 

798 
"P  False <> P" 

799 
"False  P <> P" 

800 
"P  P <> P" 

801 
"P  P  Q <> P  Q" 

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

803 
by iprover+ 

804 

805 
lemma not_simps: 

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

807 
"~ False <> True" 

808 
"~ True <> False" 

809 
by iprover+ 

810 

811 
lemma imp_simps: 

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

813 
"(P > True) <> True" 

814 
"(False > P) <> True" 

815 
"(True > P) <> P" 

816 
"(P > P) <> True" 

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

818 
by iprover+ 

819 

820 
lemma iff_simps: 

821 
"(True <> P) <> P" 

822 
"(P <> True) <> P" 

823 
"(P <> P) <> True" 

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

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

826 
by iprover+ 

827 

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

829 
lemma quant_simps: 

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

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

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

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

834 
"EX x. x=t" 

835 
"EX x. t=x" 

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

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

838 
by iprover+ 

839 

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

841 
lemma distrib_simps: 

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

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

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

845 
by iprover+ 

846 

847 

848 
text {* Conversion into rewrite rules *} 

849 

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

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

852 

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

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

855 

856 

857 
text {* More rewrite rules *} 

858 

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

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

861 
lemmas conj_comms = conj_commute conj_left_commute 

862 

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

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

865 
lemmas disj_comms = disj_commute disj_left_commute 

866 

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

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

869 

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

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

872 

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

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

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

876 

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

878 

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

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

881 

882 
lemma ex_disj_distrib: 

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

884 

885 
lemma all_conj_distrib: 

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

887 

4854  888 
end 