author  clasohm 
Fri, 13 Oct 1995 11:48:40 +0100  
changeset 1280  909079af97b7 
parent 1002  280ec187f8e1 
child 1459  d12da312eff4 
permissions  rwrr 
1280  1 
(* Title: FOL/IFOL.ML 
0  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

1280  6 
Tactics and lemmas for IFOL.thy (intuitionistic firstorder logic) 
0  7 
*) 
8 

9 
open IFOL; 

10 

11 

779  12 
qed_goalw "TrueI" IFOL.thy [True_def] "True" 
0  13 
(fn _ => [ (REPEAT (ares_tac [impI] 1)) ]); 
14 

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

16 

779  17 
qed_goal "conjE" IFOL.thy 
0  18 
"[ P&Q; [ P; Q ] ==> R ] ==> R" 
19 
(fn prems=> 

20 
[ (REPEAT (resolve_tac prems 1 

21 
ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN 

22 
resolve_tac prems 1))) ]); 

23 

779  24 
qed_goal "impE" IFOL.thy 
0  25 
"[ P>Q; P; Q ==> R ] ==> R" 
26 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); 

27 

779  28 
qed_goal "allE" IFOL.thy 
0  29 
"[ ALL x.P(x); P(x) ==> R ] ==> R" 
30 
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); 

31 

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

779  33 
qed_goal "all_dupE" IFOL.thy 
0  34 
"[ ALL x.P(x); [ P(x); ALL x.P(x) ] ==> R \ 
35 
\ ] ==> R" 

36 
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); 

37 

38 

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

40 

779  41 
qed_goalw "notI" IFOL.thy [not_def] "(P ==> False) ==> ~P" 
0  42 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); 
43 

779  44 
qed_goalw "notE" IFOL.thy [not_def] "[ ~P; P ] ==> R" 
0  45 
(fn prems=> 
46 
[ (resolve_tac [mp RS FalseE] 1), 

47 
(REPEAT (resolve_tac prems 1)) ]); 

48 

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

779  50 
qed_goal "not_to_imp" IFOL.thy 
0  51 
"[ ~P; (P>False) ==> Q ] ==> Q" 
52 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); 

53 

1002  54 
(* For substitution into an assumption P, reduce Q to P>Q, substitute into 
0  55 
this implication, then apply impI to move P back into the assumptions. 
56 
To specify P use something like 

57 
eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) 

779  58 
qed_goal "rev_mp" IFOL.thy "[ P; P > Q ] ==> Q" 
0  59 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); 
60 

61 

62 
(*Contrapositive of an inference rule*) 

779  63 
qed_goal "contrapos" IFOL.thy "[ ~Q; P==>Q ] ==> ~P" 
0  64 
(fn [major,minor]=> 
65 
[ (rtac (major RS notE RS notI) 1), 

66 
(etac minor 1) ]); 

67 

68 

69 
(*** Modus Ponens Tactics ***) 

70 

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

72 
fun mp_tac i = eresolve_tac [notE,impE] i THEN assume_tac i; 

73 

74 
(*Like mp_tac but instantiates no variables*) 

75 
fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i; 

76 

77 

78 
(*** Ifandonlyif ***) 

79 

779  80 
qed_goalw "iffI" IFOL.thy [iff_def] 
0  81 
"[ P ==> Q; Q ==> P ] ==> P<>Q" 
82 
(fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); 

83 

84 

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

779  86 
qed_goalw "iffE" IFOL.thy [iff_def] 
0  87 
"[ P <> Q; [ P>Q; Q>P ] ==> R ] ==> R" 
88 
(fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]); 

89 

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

91 

779  92 
qed_goalw "iffD1" IFOL.thy [iff_def] "[ P <> Q; P ] ==> Q" 
0  93 
(fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); 
94 

779  95 
qed_goalw "iffD2" IFOL.thy [iff_def] "[ P <> Q; Q ] ==> P" 
0  96 
(fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); 
97 

779  98 
qed_goal "iff_refl" IFOL.thy "P <> P" 
0  99 
(fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]); 
100 

779  101 
qed_goal "iff_sym" IFOL.thy "Q <> P ==> P <> Q" 
0  102 
(fn [major] => 
103 
[ (rtac (major RS iffE) 1), 

104 
(rtac iffI 1), 

105 
(REPEAT (eresolve_tac [asm_rl,mp] 1)) ]); 

106 

779  107 
qed_goal "iff_trans" IFOL.thy 
0  108 
"!!P Q R. [ P <> Q; Q<> R ] ==> P <> R" 
109 
(fn _ => 

110 
[ (rtac iffI 1), 

111 
(REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]); 

112 

113 

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

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

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

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

118 
***) 

119 

779  120 
qed_goalw "ex1I" IFOL.thy [ex1_def] 
0  121 
"[ P(a); !!x. P(x) ==> x=a ] ==> EX! x. P(x)" 
122 
(fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]); 

123 

12
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

124 
(*Sometimes easier to use: the premises have no shared variables*) 
779  125 
qed_goal "ex_ex1I" IFOL.thy 
12
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

126 
"[ EX x.P(x); !!x y. [ P(x); P(y) ] ==> x=y ] ==> EX! x. P(x)" 
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

127 
(fn [ex,eq] => [ (rtac (ex RS exE) 1), 
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

128 
(REPEAT (ares_tac [ex1I,eq] 1)) ]); 
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

129 

779  130 
qed_goalw "ex1E" IFOL.thy [ex1_def] 
0  131 
"[ EX! x.P(x); !!x. [ P(x); ALL y. P(y) > y=x ] ==> R ] ==> R" 
132 
(fn prems => 

133 
[ (cut_facts_tac prems 1), 

134 
(REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]); 

135 

136 

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

138 

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

140 
fun iff_tac prems i = 

141 
resolve_tac (prems RL [iffE]) i THEN 

142 
REPEAT1 (eresolve_tac [asm_rl,mp] i); 

143 

779  144 
qed_goal "conj_cong" IFOL.thy 
0  145 
"[ P <> P'; P' ==> Q <> Q' ] ==> (P&Q) <> (P'&Q')" 
146 
(fn prems => 

147 
[ (cut_facts_tac prems 1), 

148 
(REPEAT (ares_tac [iffI,conjI] 1 

149 
ORELSE eresolve_tac [iffE,conjE,mp] 1 

150 
ORELSE iff_tac prems 1)) ]); 

151 

793  152 
(*Reversed congruence rule! Used in ZF/Order*) 
153 
qed_goal "conj_cong2" IFOL.thy 

154 
"[ P <> P'; P' ==> Q <> Q' ] ==> (Q&P) <> (Q'&P')" 

155 
(fn prems => 

156 
[ (cut_facts_tac prems 1), 

157 
(REPEAT (ares_tac [iffI,conjI] 1 

158 
ORELSE eresolve_tac [iffE,conjE,mp] 1 

159 
ORELSE iff_tac prems 1)) ]); 

160 

779  161 
qed_goal "disj_cong" IFOL.thy 
0  162 
"[ P <> P'; Q <> Q' ] ==> (PQ) <> (P'Q')" 
163 
(fn prems => 

164 
[ (cut_facts_tac prems 1), 

165 
(REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 

166 
ORELSE ares_tac [iffI] 1 

167 
ORELSE mp_tac 1)) ]); 

168 

779  169 
qed_goal "imp_cong" IFOL.thy 
0  170 
"[ P <> P'; P' ==> Q <> Q' ] ==> (P>Q) <> (P'>Q')" 
171 
(fn prems => 

172 
[ (cut_facts_tac prems 1), 

173 
(REPEAT (ares_tac [iffI,impI] 1 

174 
ORELSE eresolve_tac [iffE] 1 

175 
ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); 

176 

779  177 
qed_goal "iff_cong" IFOL.thy 
0  178 
"[ P <> P'; Q <> Q' ] ==> (P<>Q) <> (P'<>Q')" 
179 
(fn prems => 

180 
[ (cut_facts_tac prems 1), 

181 
(REPEAT (eresolve_tac [iffE] 1 

182 
ORELSE ares_tac [iffI] 1 

183 
ORELSE mp_tac 1)) ]); 

184 

779  185 
qed_goal "not_cong" IFOL.thy 
0  186 
"P <> P' ==> ~P <> ~P'" 
187 
(fn prems => 

188 
[ (cut_facts_tac prems 1), 

189 
(REPEAT (ares_tac [iffI,notI] 1 

190 
ORELSE mp_tac 1 

191 
ORELSE eresolve_tac [iffE,notE] 1)) ]); 

192 

779  193 
qed_goal "all_cong" IFOL.thy 
0  194 
"(!!x.P(x) <> Q(x)) ==> (ALL x.P(x)) <> (ALL x.Q(x))" 
195 
(fn prems => 

196 
[ (REPEAT (ares_tac [iffI,allI] 1 

197 
ORELSE mp_tac 1 

198 
ORELSE eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]); 

199 

779  200 
qed_goal "ex_cong" IFOL.thy 
0  201 
"(!!x.P(x) <> Q(x)) ==> (EX x.P(x)) <> (EX x.Q(x))" 
202 
(fn prems => 

203 
[ (REPEAT (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1 

204 
ORELSE mp_tac 1 

205 
ORELSE iff_tac prems 1)) ]); 

206 

779  207 
qed_goal "ex1_cong" IFOL.thy 
0  208 
"(!!x.P(x) <> Q(x)) ==> (EX! x.P(x)) <> (EX! x.Q(x))" 
209 
(fn prems => 

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

211 
ORELSE mp_tac 1 

212 
ORELSE iff_tac prems 1)) ]); 

213 

214 
(*** Equality rules ***) 

215 

779  216 
qed_goal "sym" IFOL.thy "a=b ==> b=a" 
0  217 
(fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]); 
218 

779  219 
qed_goal "trans" IFOL.thy "[ a=b; b=c ] ==> a=c" 
0  220 
(fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]); 
221 

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

223 
val [not_sym] = compose(sym,2,contrapos); 

224 

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

779  226 
bind_thm ("ssubst", (sym RS subst)); 
0  227 

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

779  229 
qed_goal "ex1_equalsE" IFOL.thy 
0  230 
"[ EX! x.P(x); P(a); P(b) ] ==> a=b" 
231 
(fn prems => 

232 
[ (cut_facts_tac prems 1), 

233 
(etac ex1E 1), 

234 
(rtac trans 1), 

235 
(rtac sym 2), 

236 
(REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]); 

237 

238 
(** Polymorphic congruence rules **) 

239 

779  240 
qed_goal "subst_context" IFOL.thy 
0  241 
"[ a=b ] ==> t(a)=t(b)" 
242 
(fn prems=> 

243 
[ (resolve_tac (prems RL [ssubst]) 1), 

244 
(resolve_tac [refl] 1) ]); 

245 

779  246 
qed_goal "subst_context2" IFOL.thy 
0  247 
"[ a=b; c=d ] ==> t(a,c)=t(b,d)" 
248 
(fn prems=> 

249 
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); 

250 

779  251 
qed_goal "subst_context3" IFOL.thy 
0  252 
"[ a=b; c=d; e=f ] ==> t(a,c,e)=t(b,d,f)" 
253 
(fn prems=> 

254 
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); 

255 

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

257 
a = b 

258 
  

259 
c = d *) 

779  260 
qed_goal "box_equals" IFOL.thy 
0  261 
"[ a=b; a=c; b=d ] ==> c=d" 
262 
(fn prems=> 

263 
[ (resolve_tac [trans] 1), 

264 
(resolve_tac [trans] 1), 

265 
(resolve_tac [sym] 1), 

266 
(REPEAT (resolve_tac prems 1)) ]); 

267 

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

779  269 
qed_goal "simp_equals" IFOL.thy 
0  270 
"[ a=c; b=d; c=d ] ==> a=b" 
271 
(fn prems=> 

272 
[ (resolve_tac [trans] 1), 

273 
(resolve_tac [trans] 1), 

274 
(REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]); 

275 

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

277 

779  278 
qed_goal "pred1_cong" IFOL.thy 
0  279 
"a=a' ==> P(a) <> P(a')" 
280 
(fn prems => 

281 
[ (cut_facts_tac prems 1), 

282 
(rtac iffI 1), 

283 
(DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); 

284 

779  285 
qed_goal "pred2_cong" IFOL.thy 
0  286 
"[ a=a'; b=b' ] ==> P(a,b) <> P(a',b')" 
287 
(fn prems => 

288 
[ (cut_facts_tac prems 1), 

289 
(rtac iffI 1), 

290 
(DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); 

291 

779  292 
qed_goal "pred3_cong" IFOL.thy 
0  293 
"[ a=a'; b=b'; c=c' ] ==> P(a,b,c) <> P(a',b',c')" 
294 
(fn prems => 

295 
[ (cut_facts_tac prems 1), 

296 
(rtac iffI 1), 

297 
(DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); 

298 

299 
(*special cases for free variables P, Q, R, S  up to 3 arguments*) 

300 

301 
val pred_congs = 

302 
flat (map (fn c => 

303 
map (fn th => read_instantiate [("P",c)] th) 

304 
[pred1_cong,pred2_cong,pred3_cong]) 

305 
(explode"PQRS")); 

306 

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

308 
val eq_cong = read_instantiate [("P","op =")] pred2_cong; 

309 

310 

311 
(*** Simplifications of assumed implications. 

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

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

314 
intuitionistic propositional logic. See 

315 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

317 

779  318 
qed_goal "conj_impE" IFOL.thy 
0  319 
"[ (P&Q)>S; P>(Q>S) ==> R ] ==> R" 
320 
(fn major::prems=> 

321 
[ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]); 

322 

779  323 
qed_goal "disj_impE" IFOL.thy 
0  324 
"[ (PQ)>S; [ P>S; Q>S ] ==> R ] ==> R" 
325 
(fn major::prems=> 

326 
[ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]); 

327 

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

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

779  330 
qed_goal "imp_impE" IFOL.thy 
0  331 
"[ (P>Q)>S; [ P; Q>S ] ==> Q; S ==> R ] ==> R" 
332 
(fn major::prems=> 

333 
[ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]); 

334 

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

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

779  337 
qed_goal "not_impE" IFOL.thy 
0  338 
"[ ~P > S; P ==> False; S ==> R ] ==> R" 
339 
(fn major::prems=> 

340 
[ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]); 

341 

342 
(*Simplifies the implication. UNSAFE. *) 

779  343 
qed_goal "iff_impE" IFOL.thy 
0  344 
"[ (P<>Q)>S; [ P; Q>S ] ==> Q; [ Q; P>S ] ==> P; \ 
345 
\ S ==> R ] ==> R" 

346 
(fn major::prems=> 

347 
[ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]); 

348 

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

779  350 
qed_goal "all_impE" IFOL.thy 
0  351 
"[ (ALL x.P(x))>S; !!x.P(x); S ==> R ] ==> R" 
352 
(fn major::prems=> 

353 
[ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]); 

354 

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

779  356 
qed_goal "ex_impE" IFOL.thy 
0  357 
"[ (EX x.P(x))>S; P(x)>S ==> R ] ==> R" 
358 
(fn major::prems=> 

359 
[ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]); 

821  360 

361 
(*Courtesy Krzysztof Grabczewski*) 

362 
val major::prems = goal IFOL.thy "[ PQ; P==>R; Q==>S ] ==> RS"; 

363 
br (major RS disjE) 1; 

364 
by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1)); 

365 
qed "disj_imp_disj"; 