author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45602  2a858377c3d2 
child 48891  c0eafbd55de3 
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 

44121  10 
uses "~~/src/Tools/misc_legacy.ML" ("hypsubst.ML") ("intprover.ML") 
17480  11 
begin 
0  12 

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

13 
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:
26480
diff
changeset

14 

17480  15 
classes "term" 
36452  16 
default_sort "term" 
0  17 

17480  18 
typedecl p 
19 
typedecl o 

0  20 

17480  21 
consts 
0  22 
(*** Judgements ***) 
1477  23 
Proof :: "[o,p]=>prop" 
0  24 
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5) 
17480  25 

0  26 
(*** Logical Connectives  Type Formers ***) 
41310  27 
eq :: "['a,'a] => o" (infixl "=" 50) 
17480  28 
True :: "o" 
29 
False :: "o" 

2714  30 
Not :: "o => o" ("~ _" [40] 40) 
41310  31 
conj :: "[o,o] => o" (infixr "&" 35) 
32 
disj :: "[o,o] => o" (infixr "" 30) 

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

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

0  35 
(*Quantifiers*) 
1477  36 
All :: "('a => o) => o" (binder "ALL " 10) 
37 
Ex :: "('a => o) => o" (binder "EX " 10) 

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

0  39 
(*Rewriting gadgets*) 
1477  40 
NORM :: "o => o" 
41 
norm :: "'a => 'a" 

0  42 

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

43 
(*** Proof Term Formers: precedence must exceed 50 ***) 
1477  44 
tt :: "p" 
45 
contr :: "p=>p" 

17480  46 
fst :: "p=>p" 
47 
snd :: "p=>p" 

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

17480  50 
inl :: "p=>p" 
51 
inr :: "p=>p" 

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

41310  54 
App :: "[p,p]=>p" (infixl "`" 60) 
648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset

55 
alll :: "['a=>p]=>p" (binder "all " 55) 
41310  56 
app :: "[p,'a]=>p" (infixl "^" 55) 
1477  57 
exists :: "['a,p]=>p" ("(1[_,/_])") 
0  58 
xsplit :: "[p,['a,p]=>p]=>p" 
59 
ideq :: "'a=>p" 

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

17480  61 
nrm :: p 
62 
NRM :: p 

0  63 

35113  64 
syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5) 
65 

38800  66 
parse_translation {* 
67 
let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p 

68 
in [(@{syntax_const "_Proof"}, proof_tr)] end 

17480  69 
*} 
70 

38800  71 
(*show_proofs = true displays the proof terms  they are ENORMOUS*) 
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
41310
diff
changeset

72 
ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *} 
38800  73 

74 
print_translation (advanced) {* 

75 
let 

76 
fun proof_tr' ctxt [P, p] = 

77 
if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P 

78 
else P 

79 
in [(@{const_syntax Proof}, proof_tr')] end 

80 
*} 

17480  81 

82 
axioms 

0  83 

84 
(**** Propositional logic ****) 

85 

86 
(*Equality*) 

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

88 

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

0  91 

92 
(* Truth and Falsity *) 

93 

17480  94 
TrueI: "tt : True" 
95 
FalseE: "a:False ==> contr(a):P" 

0  96 

97 
(* Conjunction *) 

98 

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

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

0  102 

103 
(* Disjunction *) 

104 

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

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

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

0  109 

110 
(* Implication *) 

111 

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

0  114 

115 
(*Quantifiers*) 

116 

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

0  119 

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

0  122 

123 
(**** Equality between proofs ****) 

124 

17480  125 
prefl: "a : P ==> a = a : P" 
126 
psym: "a = b : P ==> b = a : P" 

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

0  128 

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

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

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

0  134 

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

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

0  138 

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

0  141 

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

144 

145 
(**** Definitions ****) 

146 

17480  147 
not_def: "~P == P>False" 
148 
iff_def: "P<>Q == (P>Q) & (Q>P)" 

0  149 

150 
(*Unique existence*) 

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

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

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

156 

26322  157 
(*** Sequentstyle elimination rules for & > and ALL ***) 
158 

36319  159 
schematic_lemma conjE: 
26322  160 
assumes "p:P&Q" 
161 
and "!!x y.[ x:P; y:Q ] ==> f(x,y):R" 

162 
shows "?a:R" 

163 
apply (rule assms(2)) 

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

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

166 
done 

167 

36319  168 
schematic_lemma impE: 
26322  169 
assumes "p:P>Q" 
170 
and "q:P" 

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

172 
shows "?p:R" 

173 
apply (rule assms mp)+ 

174 
done 

175 

36319  176 
schematic_lemma allE: 
26322  177 
assumes "p:ALL x. P(x)" 
178 
and "!!y. y:P(x) ==> q(y):R" 

179 
shows "?p:R" 

180 
apply (rule assms spec)+ 

181 
done 

182 

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

36319  184 
schematic_lemma all_dupE: 
26322  185 
assumes "p:ALL x. P(x)" 
186 
and "!!y z.[ y:P(x); z:ALL x. P(x) ] ==> q(y,z):R" 

187 
shows "?p:R" 

188 
apply (rule assms spec)+ 

189 
done 

190 

191 

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

193 

36319  194 
schematic_lemma notI: 
26322  195 
assumes "!!x. x:P ==> q(x):False" 
196 
shows "?p:~P" 

197 
unfolding not_def 

198 
apply (assumption  rule assms impI)+ 

199 
done 

200 

36319  201 
schematic_lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R" 
26322  202 
unfolding not_def 
203 
apply (drule (1) mp) 

204 
apply (erule FalseE) 

205 
done 

206 

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

36319  208 
schematic_lemma not_to_imp: 
26322  209 
assumes "p:~P" 
210 
and "!!x. x:(P>False) ==> q(x):Q" 

211 
shows "?p:Q" 

212 
apply (assumption  rule assms impI notE)+ 

213 
done 

214 

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

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

220 

221 

222 
(*Contrapositive of an inference rule*) 

36319  223 
schematic_lemma contrapos: 
26322  224 
assumes major: "p:~Q" 
225 
and minor: "!!y. y:P==>q(y):Q" 

226 
shows "?a:~P" 

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

228 
apply (erule minor) 

229 
done 

230 

231 
(** Unique assumption tactic. 

232 
Ignores proof objects. 

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

234 
**) 

235 

236 
ML {* 

237 
local 

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

239 
in 

240 
val uniq_assume_tac = 

241 
SUBGOAL 

242 
(fn (prem,i) => 

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

244 
and concl = discard_proof (Logic.strip_assums_concl prem) 

245 
in 

246 
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

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

250 
else no_tac 

251 
end); 

252 
end; 

253 
*} 

254 

255 

256 
(*** Modus Ponens Tactics ***) 

257 

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

259 
ML {* 

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

261 
*} 

262 

263 
(*Like mp_tac but instantiates no variables*) 

264 
ML {* 

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

266 
*} 

267 

268 

269 
(*** Ifandonlyif ***) 

270 

36319  271 
schematic_lemma iffI: 
26322  272 
assumes "!!x. x:P ==> q(x):Q" 
273 
and "!!x. x:Q ==> r(x):P" 

274 
shows "?p:P<>Q" 

275 
unfolding iff_def 

276 
apply (assumption  rule assms conjI impI)+ 

277 
done 

278 

279 

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

281 

36319  282 
schematic_lemma iffE: 
26322  283 
assumes "p:P <> Q" 
284 
and "!!x y.[ x:P>Q; y:Q>P ] ==> q(x,y):R" 

285 
shows "?p:R" 

286 
apply (rule conjE) 

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

288 
apply (rule assms(2)) 

289 
apply assumption+ 

290 
done 

291 

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

293 

36319  294 
schematic_lemma iffD1: "[ p:P <> Q; q:P ] ==> ?p:Q" 
26322  295 
unfolding iff_def 
296 
apply (rule conjunct1 [THEN mp], assumption+) 

297 
done 

298 

36319  299 
schematic_lemma iffD2: "[ p:P <> Q; q:Q ] ==> ?p:P" 
26322  300 
unfolding iff_def 
301 
apply (rule conjunct2 [THEN mp], assumption+) 

302 
done 

303 

36319  304 
schematic_lemma iff_refl: "?p:P <> P" 
26322  305 
apply (rule iffI) 
306 
apply assumption+ 

307 
done 

308 

36319  309 
schematic_lemma iff_sym: "p:Q <> P ==> ?p:P <> Q" 
26322  310 
apply (erule iffE) 
311 
apply (rule iffI) 

312 
apply (erule (1) mp)+ 

313 
done 

314 

36319  315 
schematic_lemma iff_trans: "[ p:P <> Q; q:Q<> R ] ==> ?p:P <> R" 
26322  316 
apply (rule iffI) 
317 
apply (assumption  erule iffE  erule (1) impE)+ 

318 
done 

319 

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

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

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

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

324 
***) 

325 

36319  326 
schematic_lemma ex1I: 
26322  327 
assumes "p:P(a)" 
328 
and "!!x u. u:P(x) ==> f(u) : x=a" 

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

330 
unfolding ex1_def 

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

332 
done 

333 

36319  334 
schematic_lemma ex1E: 
26322  335 
assumes "p:EX! x. P(x)" 
336 
and "!!x u v. [ u:P(x); v:ALL y. P(y) > y=x ] ==> f(x,u,v):R" 

337 
shows "?a : R" 

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

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

29305  340 
apply (erule assms(2), assumption) 
26322  341 
done 
342 

343 

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

345 

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

347 
ML {* 

348 
fun iff_tac prems i = 

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

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

351 
*} 

352 

36319  353 
schematic_lemma conj_cong: 
26322  354 
assumes "p:P <> P'" 
355 
and "!!x. x:P' ==> q(x):Q <> Q'" 

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

357 
apply (insert assms(1)) 

358 
apply (assumption  rule iffI conjI  

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

360 
done 

361 

36319  362 
schematic_lemma disj_cong: 
26322  363 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(PQ) <> (P'Q')" 
364 
apply (erule iffE disjE disjI1 disjI2  assumption  rule iffI  tactic {* mp_tac 1 *})+ 

365 
done 

366 

36319  367 
schematic_lemma imp_cong: 
26322  368 
assumes "p:P <> P'" 
369 
and "!!x. x:P' ==> q(x):Q <> Q'" 

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

371 
apply (insert assms(1)) 

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

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

374 
done 

375 

36319  376 
schematic_lemma iff_cong: 
26322  377 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(P<>Q) <> (P'<>Q')" 
378 
apply (erule iffE  assumption  rule iffI  tactic {* mp_tac 1 *})+ 

379 
done 

380 

36319  381 
schematic_lemma not_cong: 
26322  382 
"p:P <> P' ==> ?p:~P <> ~P'" 
383 
apply (assumption  rule iffI notI  tactic {* mp_tac 1 *}  erule iffE notE)+ 

384 
done 

385 

36319  386 
schematic_lemma all_cong: 
26322  387 
assumes "!!x. f(x):P(x) <> Q(x)" 
388 
shows "?p:(ALL x. P(x)) <> (ALL x. Q(x))" 

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

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

391 
done 

392 

36319  393 
schematic_lemma ex_cong: 
26322  394 
assumes "!!x. f(x):P(x) <> Q(x)" 
395 
shows "?p:(EX x. P(x)) <> (EX x. Q(x))" 

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

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

398 
done 

399 

400 
(*NOT PROVED 

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

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

403 
(fn prems => 

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

405 
ORELSE mp_tac 1 

406 
ORELSE iff_tac prems 1)) ])) 

407 
*) 

408 

409 
(*** Equality rules ***) 

410 

411 
lemmas refl = ieqI 

412 

36319  413 
schematic_lemma subst: 
26322  414 
assumes prem1: "p:a=b" 
415 
and prem2: "q:P(a)" 

416 
shows "?p : P(b)" 

417 
apply (rule prem2 [THEN rev_mp]) 

418 
apply (rule prem1 [THEN ieqE]) 

419 
apply (rule impI) 

420 
apply assumption 

421 
done 

422 

36319  423 
schematic_lemma sym: "q:a=b ==> ?c:b=a" 
26322  424 
apply (erule subst) 
425 
apply (rule refl) 

426 
done 

427 

36319  428 
schematic_lemma trans: "[ p:a=b; q:b=c ] ==> ?d:a=c" 
26322  429 
apply (erule (1) subst) 
430 
done 

431 

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

36319  433 
schematic_lemma not_sym: "p:~ b=a ==> ?q:~ a=b" 
26322  434 
apply (erule contrapos) 
435 
apply (erule sym) 

436 
done 

437 

45594  438 
schematic_lemma ssubst: "p:b=a \<Longrightarrow> q:P(a) \<Longrightarrow> ?p:P(b)" 
439 
apply (drule sym) 

440 
apply (erule subst) 

441 
apply assumption 

442 
done 

26322  443 

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

36319  445 
schematic_lemma ex1_equalsE: "[ p:EX! x. P(x); q:P(a); r:P(b) ] ==> ?d:a=b" 
26322  446 
apply (erule ex1E) 
447 
apply (rule trans) 

448 
apply (rule_tac [2] sym) 

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

450 
done 

451 

452 
(** Polymorphic congruence rules **) 

453 

36319  454 
schematic_lemma subst_context: "[ p:a=b ] ==> ?d:t(a)=t(b)" 
26322  455 
apply (erule ssubst) 
456 
apply (rule refl) 

457 
done 

458 

36319  459 
schematic_lemma subst_context2: "[ p:a=b; q:c=d ] ==> ?p:t(a,c)=t(b,d)" 
26322  460 
apply (erule ssubst)+ 
461 
apply (rule refl) 

462 
done 

463 

36319  464 
schematic_lemma subst_context3: "[ p:a=b; q:c=d; r:e=f ] ==> ?p:t(a,c,e)=t(b,d,f)" 
26322  465 
apply (erule ssubst)+ 
466 
apply (rule refl) 

467 
done 

468 

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

470 
a = b 

471 
  

472 
c = d *) 

36319  473 
schematic_lemma box_equals: "[ p:a=b; q:a=c; r:b=d ] ==> ?p:c=d" 
26322  474 
apply (rule trans) 
475 
apply (rule trans) 

476 
apply (rule sym) 

477 
apply assumption+ 

478 
done 

479 

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

36319  481 
schematic_lemma simp_equals: "[ p:a=c; q:b=d; r:c=d ] ==> ?p:a=b" 
26322  482 
apply (rule trans) 
483 
apply (rule trans) 

484 
apply (assumption  rule sym)+ 

485 
done 

486 

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

488 

36319  489 
schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <> P(a')" 
26322  490 
apply (rule iffI) 
491 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) 

492 
done 

493 

36319  494 
schematic_lemma pred2_cong: "[ p:a=a'; q:b=b' ] ==> ?p:P(a,b) <> P(a',b')" 
26322  495 
apply (rule iffI) 
496 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) 

497 
done 

498 

36319  499 
schematic_lemma pred3_cong: "[ p:a=a'; q:b=b'; r:c=c' ] ==> ?p:P(a,b,c) <> P(a',b',c')" 
26322  500 
apply (rule iffI) 
501 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *}) 

502 
done 

503 

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

504 
lemmas pred_congs = pred1_cong pred2_cong pred3_cong 
26322  505 

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

45602  507 
lemmas eq_cong = pred2_cong [where P = "op ="] 
26322  508 

509 

510 
(*** Simplifications of assumed implications. 

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

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

513 
intuitionistic propositional logic. See 

514 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

516 

36319  517 
schematic_lemma conj_impE: 
26322  518 
assumes major: "p:(P&Q)>S" 
519 
and minor: "!!x. x:P>(Q>S) ==> q(x):R" 

520 
shows "?p:R" 

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

522 
done 

523 

36319  524 
schematic_lemma disj_impE: 
26322  525 
assumes major: "p:(PQ)>S" 
526 
and minor: "!!x y.[ x:P>S; y:Q>S ] ==> q(x,y):R" 

527 
shows "?p:R" 

528 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE 

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

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

531 
done 

532 

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

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

36319  535 
schematic_lemma imp_impE: 
26322  536 
assumes major: "p:(P>Q)>S" 
537 
and r1: "!!x y.[ x:P; y:Q>S ] ==> q(x,y):Q" 

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

539 
shows "?p:R" 

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

541 
done 

542 

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

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

36319  545 
schematic_lemma not_impE: 
26322  546 
assumes major: "p:~P > S" 
547 
and r1: "!!y. y:P ==> q(y):False" 

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

549 
shows "?p:R" 

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

551 
done 

552 

553 
(*Simplifies the implication. UNSAFE. *) 

36319  554 
schematic_lemma iff_impE: 
26322  555 
assumes major: "p:(P<>Q)>S" 
556 
and r1: "!!x y.[ x:P; y:Q>S ] ==> q(x,y):Q" 

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

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

559 
shows "?p: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*) 

36319  564 
schematic_lemma all_impE: 
26322  565 
assumes major: "p:(ALL x. P(x))>S" 
566 
and r1: "!!x. q:P(x)" 

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

568 
shows "?p:R" 

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

570 
done 

571 

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

36319  573 
schematic_lemma ex_impE: 
26322  574 
assumes major: "p:(EX x. P(x))>S" 
575 
and r: "!!y. y:P(a)>S ==> q(y):R" 

576 
shows "?p:R" 

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

578 
done 

579 

580 

36319  581 
schematic_lemma rev_cut_eq: 
26322  582 
assumes "p:a=b" 
583 
and "!!x. x:a=b ==> f(x):R" 

584 
shows "?p:R" 

585 
apply (rule assms)+ 

586 
done 

587 

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

589 

590 
use "hypsubst.ML" 

591 

592 
ML {* 

42799  593 
structure Hypsubst = Hypsubst 
594 
( 

26322  595 
(*Take apart an equality judgement; otherwise raise Match!*) 
596 
fun dest_eq (Const (@{const_name Proof}, _) $ 

41310  597 
(Const (@{const_name eq}, _) $ t $ u) $ _) = (t, u); 
26322  598 

599 
val imp_intr = @{thm impI} 

600 

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

602 
val rev_cut_eq = @{thm rev_cut_eq} 

603 

604 
val rev_mp = @{thm rev_mp} 

605 
val subst = @{thm subst} 

606 
val sym = @{thm sym} 

607 
val thin_refl = @{thm thin_refl} 

42799  608 
); 
26322  609 
open Hypsubst; 
610 
*} 

611 

612 
use "intprover.ML" 

613 

614 

615 
(*** Rewrite rules ***) 

616 

36319  617 
schematic_lemma conj_rews: 
26322  618 
"?p1 : P & True <> P" 
619 
"?p2 : True & P <> P" 

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

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

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

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

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

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

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

627 
done 

628 

36319  629 
schematic_lemma disj_rews: 
26322  630 
"?p1 : P  True <> True" 
631 
"?p2 : True  P <> True" 

632 
"?p3 : P  False <> P" 

633 
"?p4 : False  P <> P" 

634 
"?p5 : P  P <> P" 

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

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

637 
done 

638 

36319  639 
schematic_lemma not_rews: 
26322  640 
"?p1 : ~ False <> True" 
641 
"?p2 : ~ True <> False" 

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

643 
done 

644 

36319  645 
schematic_lemma imp_rews: 
26322  646 
"?p1 : (P > False) <> ~P" 
647 
"?p2 : (P > True) <> True" 

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

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

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

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

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

653 
done 

654 

36319  655 
schematic_lemma iff_rews: 
26322  656 
"?p1 : (True <> P) <> P" 
657 
"?p2 : (P <> True) <> P" 

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

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

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

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

662 
done 

663 

36319  664 
schematic_lemma quant_rews: 
26322  665 
"?p1 : (ALL x. P) <> P" 
666 
"?p2 : (EX x. P) <> P" 

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

668 
done 

669 

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

36319  671 
schematic_lemma distrib_rews1: 
26322  672 
"?p1 : ~(PQ) <> ~P & ~Q" 
673 
"?p2 : P & (Q  R) <> P&Q  P&R" 

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

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

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

677 
done 

678 

36319  679 
schematic_lemma distrib_rews2: 
26322  680 
"?p1 : ~(EX x. NORM(P(x))) <> (ALL x. ~NORM(P(x)))" 
681 
"?p2 : ((EX x. NORM(P(x))) > Q) <> (ALL x. NORM(P(x)) > Q)" 

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

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

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

685 
done 

686 

687 
lemmas distrib_rews = distrib_rews1 distrib_rews2 

688 

36319  689 
schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <> True)" 
26322  690 
apply (tactic {* IntPr.fast_tac 1 *}) 
691 
done 

692 

36319  693 
schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <> False)" 
26322  694 
apply (tactic {* IntPr.fast_tac 1 *}) 
695 
done 

0  696 

697 
end 