author  wenzelm 
Sun, 11 Jan 2009 21:49:59 +0100  
changeset 29450  ac7f67be7f1f 
parent 29305  76af2a3c9d28 
child 32740  9dd0a2f83429 
permissions  rwrr 
1477  1 
(* Title: FOLP/IFOLP.thy 
2 
Author: Martin D Coen, Cambridge University Computer Laboratory 

1142  3 
Copyright 1992 University of Cambridge 
4 
*) 

5 

17480  6 
header {* Intuitionistic FirstOrder Logic with Proofs *} 
7 

8 
theory IFOLP 

9 
imports Pure 

26322  10 
uses ("hypsubst.ML") ("intprover.ML") 
17480  11 
begin 
0  12 

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

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

14 

3942  15 
global 
16 

17480  17 
classes "term" 
18 
defaultsort "term" 

0  19 

17480  20 
typedecl p 
21 
typedecl o 

0  22 

17480  23 
consts 
0  24 
(*** Judgements ***) 
1477  25 
"@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5) 
26 
Proof :: "[o,p]=>prop" 

0  27 
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5) 
17480  28 

0  29 
(*** Logical Connectives  Type Formers ***) 
1477  30 
"=" :: "['a,'a] => o" (infixl 50) 
17480  31 
True :: "o" 
32 
False :: "o" 

2714  33 
Not :: "o => o" ("~ _" [40] 40) 
1477  34 
"&" :: "[o,o] => o" (infixr 35) 
35 
"" :: "[o,o] => o" (infixr 30) 

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

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

0  38 
(*Quantifiers*) 
1477  39 
All :: "('a => o) => o" (binder "ALL " 10) 
40 
Ex :: "('a => o) => o" (binder "EX " 10) 

41 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 

0  42 
(*Rewriting gadgets*) 
1477  43 
NORM :: "o => o" 
44 
norm :: "'a => 'a" 

0  45 

648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset

46 
(*** Proof Term Formers: precedence must exceed 50 ***) 
1477  47 
tt :: "p" 
48 
contr :: "p=>p" 

17480  49 
fst :: "p=>p" 
50 
snd :: "p=>p" 

1477  51 
pair :: "[p,p]=>p" ("(1<_,/_>)") 
52 
split :: "[p, [p,p]=>p] =>p" 

17480  53 
inl :: "p=>p" 
54 
inr :: "p=>p" 

1477  55 
when :: "[p, p=>p, p=>p]=>p" 
56 
lambda :: "(p => p) => p" (binder "lam " 55) 

57 
"`" :: "[p,p]=>p" (infixl 60) 

648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset

58 
alll :: "['a=>p]=>p" (binder "all " 55) 
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset

59 
"^" :: "[p,'a]=>p" (infixl 55) 
1477  60 
exists :: "['a,p]=>p" ("(1[_,/_])") 
0  61 
xsplit :: "[p,['a,p]=>p]=>p" 
62 
ideq :: "'a=>p" 

63 
idpeel :: "[p,'a=>p]=>p" 

17480  64 
nrm :: p 
65 
NRM :: p 

0  66 

3942  67 
local 
68 

17480  69 
ML {* 
70 

71 
(*show_proofs:=true displays the proof terms  they are ENORMOUS*) 

72 
val show_proofs = ref false; 

73 

26322  74 
fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p; 
17480  75 

76 
fun proof_tr' [P,p] = 

77 
if !show_proofs then Const("@Proof",dummyT) $ p $ P 

78 
else P (*this case discards the proof term*); 

79 
*} 

80 

81 
parse_translation {* [("@Proof", proof_tr)] *} 

82 
print_translation {* [("Proof", proof_tr')] *} 

83 

84 
axioms 

0  85 

86 
(**** Propositional logic ****) 

87 

88 
(*Equality*) 

89 
(* Like Intensional Equality in MLTT  but proofs distinct from terms *) 

90 

17480  91 
ieqI: "ideq(a) : a=a" 
92 
ieqE: "[ p : a=b; !!x. f(x) : P(x,x) ] ==> idpeel(p,f) : P(a,b)" 

0  93 

94 
(* Truth and Falsity *) 

95 

17480  96 
TrueI: "tt : True" 
97 
FalseE: "a:False ==> contr(a):P" 

0  98 

99 
(* Conjunction *) 

100 

17480  101 
conjI: "[ a:P; b:Q ] ==> <a,b> : P&Q" 
102 
conjunct1: "p:P&Q ==> fst(p):P" 

103 
conjunct2: "p:P&Q ==> snd(p):Q" 

0  104 

105 
(* Disjunction *) 

106 

17480  107 
disjI1: "a:P ==> inl(a):PQ" 
108 
disjI2: "b:Q ==> inr(b):PQ" 

109 
disjE: "[ a:PQ; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R 

110 
] ==> when(a,f,g):R" 

0  111 

112 
(* Implication *) 

113 

17480  114 
impI: "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P>Q" 
115 
mp: "[ f:P>Q; a:P ] ==> f`a:Q" 

0  116 

117 
(*Quantifiers*) 

118 

17480  119 
allI: "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" 
120 
spec: "(f:ALL x. P(x)) ==> f^x : P(x)" 

0  121 

17480  122 
exI: "p : P(x) ==> [x,p] : EX x. P(x)" 
123 
exE: "[ p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R ] ==> xsplit(p,f):R" 

0  124 

125 
(**** Equality between proofs ****) 

126 

17480  127 
prefl: "a : P ==> a = a : P" 
128 
psym: "a = b : P ==> b = a : P" 

129 
ptrans: "[ a = b : P; b = c : P ] ==> a = c : P" 

0  130 

17480  131 
idpeelB: "[ !!x. f(x) : P(x,x) ] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" 
0  132 

17480  133 
fstB: "a:P ==> fst(<a,b>) = a : P" 
134 
sndB: "b:Q ==> snd(<a,b>) = b : Q" 

135 
pairEC: "p:P&Q ==> p = <fst(p),snd(p)> : P&Q" 

0  136 

17480  137 
whenBinl: "[ a:P; !!x. x:P ==> f(x) : Q ] ==> when(inl(a),f,g) = f(a) : Q" 
138 
whenBinr: "[ b:P; !!x. x:P ==> g(x) : Q ] ==> when(inr(b),f,g) = g(b) : Q" 

139 
plusEC: "a:PQ ==> when(a,%x. inl(x),%y. inr(y)) = a : PQ" 

0  140 

17480  141 
applyB: "[ a:P; !!x. x:P ==> b(x) : Q ] ==> (lam x. b(x)) ` a = b(a) : Q" 
142 
funEC: "f:P ==> f = lam x. f`x : P" 

0  143 

17480  144 
specB: "[ !!x. f(x) : P(x) ] ==> (all x. f(x)) ^ a = f(a) : P(a)" 
0  145 

146 

147 
(**** Definitions ****) 

148 

17480  149 
not_def: "~P == P>False" 
150 
iff_def: "P<>Q == (P>Q) & (Q>P)" 

0  151 

152 
(*Unique existence*) 

17480  153 
ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)" 
0  154 

155 
(*Rewriting  special constants to flag normalized terms and formulae*) 

17480  156 
norm_eq: "nrm : norm(x) = x" 
157 
NORM_iff: "NRM : NORM(P) <> P" 

158 

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

161 
lemma conjE: 

162 
assumes "p:P&Q" 

163 
and "!!x y.[ x:P; y:Q ] ==> f(x,y):R" 

164 
shows "?a:R" 

165 
apply (rule assms(2)) 

166 
apply (rule conjunct1 [OF assms(1)]) 

167 
apply (rule conjunct2 [OF assms(1)]) 

168 
done 

169 

170 
lemma impE: 

171 
assumes "p:P>Q" 

172 
and "q:P" 

173 
and "!!x. x:Q ==> r(x):R" 

174 
shows "?p:R" 

175 
apply (rule assms mp)+ 

176 
done 

177 

178 
lemma allE: 

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

180 
and "!!y. y:P(x) ==> q(y):R" 

181 
shows "?p:R" 

182 
apply (rule assms spec)+ 

183 
done 

184 

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

186 
lemma all_dupE: 

187 
assumes "p:ALL x. P(x)" 

188 
and "!!y z.[ y:P(x); z:ALL x. P(x) ] ==> q(y,z):R" 

189 
shows "?p:R" 

190 
apply (rule assms spec)+ 

191 
done 

192 

193 

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

195 

196 
lemma notI: 

197 
assumes "!!x. x:P ==> q(x):False" 

198 
shows "?p:~P" 

199 
unfolding not_def 

200 
apply (assumption  rule assms impI)+ 

201 
done 

202 

203 
lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R" 

204 
unfolding not_def 

205 
apply (drule (1) mp) 

206 
apply (erule FalseE) 

207 
done 

208 

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

210 
lemma not_to_imp: 

211 
assumes "p:~P" 

212 
and "!!x. x:(P>False) ==> q(x):Q" 

213 
shows "?p:Q" 

214 
apply (assumption  rule assms impI notE)+ 

215 
done 

216 

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

27150  218 
this implication, then apply impI to move P back into the assumptions.*) 
26322  219 
lemma rev_mp: "[ p:P; q:P > Q ] ==> ?p:Q" 
220 
apply (assumption  rule mp)+ 

221 
done 

222 

223 

224 
(*Contrapositive of an inference rule*) 

225 
lemma contrapos: 

226 
assumes major: "p:~Q" 

227 
and minor: "!!y. y:P==>q(y):Q" 

228 
shows "?a:~P" 

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

230 
apply (erule minor) 

231 
done 

232 

233 
(** Unique assumption tactic. 

234 
Ignores proof objects. 

235 
Fails unless one assumption is equal and exactly one is unifiable 

236 
**) 

237 

238 
ML {* 

239 
local 

240 
fun discard_proof (Const (@{const_name Proof}, _) $ P $ _) = P; 

241 
in 

242 
val uniq_assume_tac = 

243 
SUBGOAL 

244 
(fn (prem,i) => 

245 
let val hyps = map discard_proof (Logic.strip_assums_hyp prem) 

246 
and concl = discard_proof (Logic.strip_assums_concl prem) 

247 
in 

248 
if exists (fn hyp => hyp aconv concl) hyps 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27152
diff
changeset

249 
then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of 
26322  250 
[_] => assume_tac i 
251 
 _ => no_tac 

252 
else no_tac 

253 
end); 

254 
end; 

255 
*} 

256 

257 

258 
(*** Modus Ponens Tactics ***) 

259 

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

261 
ML {* 

262 
fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i THEN assume_tac i 

263 
*} 

264 

265 
(*Like mp_tac but instantiates no variables*) 

266 
ML {* 

267 
fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN uniq_assume_tac i 

268 
*} 

269 

270 

271 
(*** Ifandonlyif ***) 

272 

273 
lemma iffI: 

274 
assumes "!!x. x:P ==> q(x):Q" 

275 
and "!!x. x:Q ==> r(x):P" 

276 
shows "?p:P<>Q" 

277 
unfolding iff_def 

278 
apply (assumption  rule assms conjI impI)+ 

279 
done 

280 

281 

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

283 

284 
lemma iffE: 

285 
assumes "p:P <> Q" 

286 
and "!!x y.[ x:P>Q; y:Q>P ] ==> q(x,y):R" 

287 
shows "?p:R" 

288 
apply (rule conjE) 

289 
apply (rule assms(1) [unfolded iff_def]) 

290 
apply (rule assms(2)) 

291 
apply assumption+ 

292 
done 

293 

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

295 

296 
lemma iffD1: "[ p:P <> Q; q:P ] ==> ?p:Q" 

297 
unfolding iff_def 

298 
apply (rule conjunct1 [THEN mp], assumption+) 

299 
done 

300 

301 
lemma iffD2: "[ p:P <> Q; q:Q ] ==> ?p:P" 

302 
unfolding iff_def 

303 
apply (rule conjunct2 [THEN mp], assumption+) 

304 
done 

305 

306 
lemma iff_refl: "?p:P <> P" 

307 
apply (rule iffI) 

308 
apply assumption+ 

309 
done 

310 

311 
lemma iff_sym: "p:Q <> P ==> ?p:P <> Q" 

312 
apply (erule iffE) 

313 
apply (rule iffI) 

314 
apply (erule (1) mp)+ 

315 
done 

316 

317 
lemma iff_trans: "[ p:P <> Q; q:Q<> R ] ==> ?p:P <> R" 

318 
apply (rule iffI) 

319 
apply (assumption  erule iffE  erule (1) impE)+ 

320 
done 

321 

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

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

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

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

326 
***) 

327 

328 
lemma ex1I: 

329 
assumes "p:P(a)" 

330 
and "!!x u. u:P(x) ==> f(u) : x=a" 

331 
shows "?p:EX! x. P(x)" 

332 
unfolding ex1_def 

333 
apply (assumption  rule assms exI conjI allI impI)+ 

334 
done 

335 

336 
lemma ex1E: 

337 
assumes "p:EX! x. P(x)" 

338 
and "!!x u v. [ u:P(x); v:ALL y. P(y) > y=x ] ==> f(x,u,v):R" 

339 
shows "?a : R" 

340 
apply (insert assms(1) [unfolded ex1_def]) 

341 
apply (erule exE conjE  assumption  rule assms(1))+ 

29305  342 
apply (erule assms(2), assumption) 
26322  343 
done 
344 

345 

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

347 

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

349 
ML {* 

350 
fun iff_tac prems i = 

351 
resolve_tac (prems RL [@{thm iffE}]) i THEN 

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

353 
*} 

354 

355 
lemma conj_cong: 

356 
assumes "p:P <> P'" 

357 
and "!!x. x:P' ==> q(x):Q <> Q'" 

358 
shows "?p:(P&Q) <> (P'&Q')" 

359 
apply (insert assms(1)) 

360 
apply (assumption  rule iffI conjI  

361 
erule iffE conjE mp  tactic {* iff_tac @{thms assms} 1 *})+ 

362 
done 

363 

364 
lemma disj_cong: 

365 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(PQ) <> (P'Q')" 

366 
apply (erule iffE disjE disjI1 disjI2  assumption  rule iffI  tactic {* mp_tac 1 *})+ 

367 
done 

368 

369 
lemma imp_cong: 

370 
assumes "p:P <> P'" 

371 
and "!!x. x:P' ==> q(x):Q <> Q'" 

372 
shows "?p:(P>Q) <> (P'>Q')" 

373 
apply (insert assms(1)) 

374 
apply (assumption  rule iffI impI  erule iffE  tactic {* mp_tac 1 *}  

375 
tactic {* iff_tac @{thms assms} 1 *})+ 

376 
done 

377 

378 
lemma iff_cong: 

379 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(P<>Q) <> (P'<>Q')" 

380 
apply (erule iffE  assumption  rule iffI  tactic {* mp_tac 1 *})+ 

381 
done 

382 

383 
lemma not_cong: 

384 
"p:P <> P' ==> ?p:~P <> ~P'" 

385 
apply (assumption  rule iffI notI  tactic {* mp_tac 1 *}  erule iffE notE)+ 

386 
done 

387 

388 
lemma all_cong: 

389 
assumes "!!x. f(x):P(x) <> Q(x)" 

390 
shows "?p:(ALL x. P(x)) <> (ALL x. Q(x))" 

391 
apply (assumption  rule iffI allI  tactic {* mp_tac 1 *}  erule allE  

392 
tactic {* iff_tac @{thms assms} 1 *})+ 

393 
done 

394 

395 
lemma ex_cong: 

396 
assumes "!!x. f(x):P(x) <> Q(x)" 

397 
shows "?p:(EX x. P(x)) <> (EX x. Q(x))" 

398 
apply (erule exE  assumption  rule iffI exI  tactic {* mp_tac 1 *}  

399 
tactic {* iff_tac @{thms assms} 1 *})+ 

400 
done 

401 

402 
(*NOT PROVED 

403 
bind_thm ("ex1_cong", prove_goal (the_context ()) 

404 
"(!!x.f(x):P(x) <> Q(x)) ==> ?p:(EX! x.P(x)) <> (EX! x.Q(x))" 

405 
(fn prems => 

406 
[ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 

407 
ORELSE mp_tac 1 

408 
ORELSE iff_tac prems 1)) ])) 

409 
*) 

410 

411 
(*** Equality rules ***) 

412 

413 
lemmas refl = ieqI 

414 

415 
lemma subst: 

416 
assumes prem1: "p:a=b" 

417 
and prem2: "q:P(a)" 

418 
shows "?p : P(b)" 

419 
apply (rule prem2 [THEN rev_mp]) 

420 
apply (rule prem1 [THEN ieqE]) 

421 
apply (rule impI) 

422 
apply assumption 

423 
done 

424 

425 
lemma sym: "q:a=b ==> ?c:b=a" 

426 
apply (erule subst) 

427 
apply (rule refl) 

428 
done 

429 

430 
lemma trans: "[ p:a=b; q:b=c ] ==> ?d:a=c" 

431 
apply (erule (1) subst) 

432 
done 

433 

434 
(** ~ b=a ==> ~ a=b **) 

435 
lemma not_sym: "p:~ b=a ==> ?q:~ a=b" 

436 
apply (erule contrapos) 

437 
apply (erule sym) 

438 
done 

439 

440 
(*calling "standard" reduces maxidx to 0*) 

441 
lemmas ssubst = sym [THEN subst, standard] 

442 

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

444 
lemma ex1_equalsE: "[ p:EX! x. P(x); q:P(a); r:P(b) ] ==> ?d:a=b" 

445 
apply (erule ex1E) 

446 
apply (rule trans) 

447 
apply (rule_tac [2] sym) 

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

449 
done 

450 

451 
(** Polymorphic congruence rules **) 

452 

453 
lemma subst_context: "[ p:a=b ] ==> ?d:t(a)=t(b)" 

454 
apply (erule ssubst) 

455 
apply (rule refl) 

456 
done 

457 

458 
lemma subst_context2: "[ p:a=b; q:c=d ] ==> ?p:t(a,c)=t(b,d)" 

459 
apply (erule ssubst)+ 

460 
apply (rule refl) 

461 
done 

462 

463 
lemma subst_context3: "[ p:a=b; q:c=d; r:e=f ] ==> ?p:t(a,c,e)=t(b,d,f)" 

464 
apply (erule ssubst)+ 

465 
apply (rule refl) 

466 
done 

467 

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

469 
a = b 

470 
  

471 
c = d *) 

472 
lemma box_equals: "[ p:a=b; q:a=c; r:b=d ] ==> ?p:c=d" 

473 
apply (rule trans) 

474 
apply (rule trans) 

475 
apply (rule sym) 

476 
apply assumption+ 

477 
done 

478 

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

480 
lemma simp_equals: "[ p:a=c; q:b=d; r:c=d ] ==> ?p:a=b" 

481 
apply (rule trans) 

482 
apply (rule trans) 

483 
apply (assumption  rule sym)+ 

484 
done 

485 

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

487 

488 
lemma pred1_cong: "p:a=a' ==> ?p:P(a) <> P(a')" 

489 
apply (rule iffI) 

490 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) 

491 
done 

492 

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

494 
apply (rule iffI) 

495 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) 

496 
done 

497 

498 
lemma pred3_cong: "[ p:a=a'; q:b=b'; r:c=c' ] ==> ?p:P(a,b,c) <> P(a',b',c')" 

499 
apply (rule iffI) 

500 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) 

501 
done 

502 

27152
192954a9a549
changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;
wenzelm
parents:
27150
diff
changeset

503 
lemmas pred_congs = pred1_cong pred2_cong pred3_cong 
26322  504 

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

506 
lemmas eq_cong = pred2_cong [where P = "op =", standard] 

507 

508 

509 
(*** Simplifications of assumed implications. 

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

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

512 
intuitionistic propositional logic. See 

513 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

515 

516 
lemma conj_impE: 

517 
assumes major: "p:(P&Q)>S" 

518 
and minor: "!!x. x:P>(Q>S) ==> q(x):R" 

519 
shows "?p:R" 

520 
apply (assumption  rule conjI impI major [THEN mp] minor)+ 

521 
done 

522 

523 
lemma disj_impE: 

524 
assumes major: "p:(PQ)>S" 

525 
and minor: "!!x y.[ x:P>S; y:Q>S ] ==> q(x,y):R" 

526 
shows "?p:R" 

527 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE 

528 
resolve_tac [@{thm disjI1}, @{thm disjI2}, @{thm impI}, 

529 
@{thm major} RS @{thm mp}, @{thm minor}] 1) *}) 

530 
done 

531 

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

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

534 
lemma imp_impE: 

535 
assumes major: "p:(P>Q)>S" 

536 
and r1: "!!x y.[ x:P; y:Q>S ] ==> q(x,y):Q" 

537 
and r2: "!!x. x:S ==> r(x):R" 

538 
shows "?p:R" 

539 
apply (assumption  rule impI major [THEN mp] r1 r2)+ 

540 
done 

541 

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

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

544 
lemma not_impE: 

545 
assumes major: "p:~P > S" 

546 
and r1: "!!y. y:P ==> q(y):False" 

547 
and r2: "!!y. y:S ==> r(y):R" 

548 
shows "?p:R" 

549 
apply (assumption  rule notI impI major [THEN mp] r1 r2)+ 

550 
done 

551 

552 
(*Simplifies the implication. UNSAFE. *) 

553 
lemma iff_impE: 

554 
assumes major: "p:(P<>Q)>S" 

555 
and r1: "!!x y.[ x:P; y:Q>S ] ==> q(x,y):Q" 

556 
and r2: "!!x y.[ x:Q; y:P>S ] ==> r(x,y):P" 

557 
and r3: "!!x. x:S ==> s(x):R" 

558 
shows "?p:R" 

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

560 
done 

561 

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

563 
lemma all_impE: 

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

565 
and r1: "!!x. q:P(x)" 

566 
and r2: "!!y. y:S ==> r(y):R" 

567 
shows "?p:R" 

568 
apply (assumption  rule allI impI major [THEN mp] r1 r2)+ 

569 
done 

570 

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

572 
lemma ex_impE: 

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

574 
and r: "!!y. y:P(a)>S ==> q(y):R" 

575 
shows "?p:R" 

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

577 
done 

578 

579 

580 
lemma rev_cut_eq: 

581 
assumes "p:a=b" 

582 
and "!!x. x:a=b ==> f(x):R" 

583 
shows "?p:R" 

584 
apply (rule assms)+ 

585 
done 

586 

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

588 

589 
use "hypsubst.ML" 

590 

591 
ML {* 

592 

593 
(*** Applying HypsubstFun to generate hyp_subst_tac ***) 

594 

595 
structure Hypsubst_Data = 

596 
struct 

597 
(*Take apart an equality judgement; otherwise raise Match!*) 

598 
fun dest_eq (Const (@{const_name Proof}, _) $ 

599 
(Const (@{const_name "op ="}, _) $ t $ u) $ _) = (t, u); 

600 

601 
val imp_intr = @{thm impI} 

602 

603 
(*etac rev_cut_eq moves an equality to be the last premise. *) 

604 
val rev_cut_eq = @{thm rev_cut_eq} 

605 

606 
val rev_mp = @{thm rev_mp} 

607 
val subst = @{thm subst} 

608 
val sym = @{thm sym} 

609 
val thin_refl = @{thm thin_refl} 

610 
end; 

611 

612 
structure Hypsubst = HypsubstFun(Hypsubst_Data); 

613 
open Hypsubst; 

614 
*} 

615 

616 
use "intprover.ML" 

617 

618 

619 
(*** Rewrite rules ***) 

620 

621 
lemma conj_rews: 

622 
"?p1 : P & True <> P" 

623 
"?p2 : True & P <> P" 

624 
"?p3 : P & False <> False" 

625 
"?p4 : False & P <> False" 

626 
"?p5 : P & P <> P" 

627 
"?p6 : P & ~P <> False" 

628 
"?p7 : ~P & P <> False" 

629 
"?p8 : (P & Q) & R <> P & (Q & R)" 

630 
apply (tactic {* fn st => IntPr.fast_tac 1 st *})+ 

631 
done 

632 

633 
lemma disj_rews: 

634 
"?p1 : P  True <> True" 

635 
"?p2 : True  P <> True" 

636 
"?p3 : P  False <> P" 

637 
"?p4 : False  P <> P" 

638 
"?p5 : P  P <> P" 

639 
"?p6 : (P  Q)  R <> P  (Q  R)" 

640 
apply (tactic {* IntPr.fast_tac 1 *})+ 

641 
done 

642 

643 
lemma not_rews: 

644 
"?p1 : ~ False <> True" 

645 
"?p2 : ~ True <> False" 

646 
apply (tactic {* IntPr.fast_tac 1 *})+ 

647 
done 

648 

649 
lemma imp_rews: 

650 
"?p1 : (P > False) <> ~P" 

651 
"?p2 : (P > True) <> True" 

652 
"?p3 : (False > P) <> True" 

653 
"?p4 : (True > P) <> P" 

654 
"?p5 : (P > P) <> True" 

655 
"?p6 : (P > ~P) <> ~P" 

656 
apply (tactic {* IntPr.fast_tac 1 *})+ 

657 
done 

658 

659 
lemma iff_rews: 

660 
"?p1 : (True <> P) <> P" 

661 
"?p2 : (P <> True) <> P" 

662 
"?p3 : (P <> P) <> True" 

663 
"?p4 : (False <> P) <> ~P" 

664 
"?p5 : (P <> False) <> ~P" 

665 
apply (tactic {* IntPr.fast_tac 1 *})+ 

666 
done 

667 

668 
lemma quant_rews: 

669 
"?p1 : (ALL x. P) <> P" 

670 
"?p2 : (EX x. P) <> P" 

671 
apply (tactic {* IntPr.fast_tac 1 *})+ 

672 
done 

673 

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

675 
lemma distrib_rews1: 

676 
"?p1 : ~(PQ) <> ~P & ~Q" 

677 
"?p2 : P & (Q  R) <> P&Q  P&R" 

678 
"?p3 : (Q  R) & P <> Q&P  R&P" 

679 
"?p4 : (P  Q > R) <> (P > R) & (Q > R)" 

680 
apply (tactic {* IntPr.fast_tac 1 *})+ 

681 
done 

682 

683 
lemma distrib_rews2: 

684 
"?p1 : ~(EX x. NORM(P(x))) <> (ALL x. ~NORM(P(x)))" 

685 
"?p2 : ((EX x. NORM(P(x))) > Q) <> (ALL x. NORM(P(x)) > Q)" 

686 
"?p3 : (EX x. NORM(P(x))) & NORM(Q) <> (EX x. NORM(P(x)) & NORM(Q))" 

687 
"?p4 : NORM(Q) & (EX x. NORM(P(x))) <> (EX x. NORM(Q) & NORM(P(x)))" 

688 
apply (tactic {* IntPr.fast_tac 1 *})+ 

689 
done 

690 

691 
lemmas distrib_rews = distrib_rews1 distrib_rews2 

692 

693 
lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <> True)" 

694 
apply (tactic {* IntPr.fast_tac 1 *}) 

695 
done 

696 

697 
lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <> False)" 

698 
apply (tactic {* IntPr.fast_tac 1 *}) 

699 
done 

0  700 

701 
end 