author  lcp 
Fri, 16 Dec 1994 13:30:34 +0100  
changeset 793  0b5c5f568d74 
parent 779  4ab9176b45b7 
child 821  650ee089809b 
permissions  rwrr 
0  1 
(* Title: FOL/ifol.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
Tactics and lemmas for ifol.thy (intuitionistic firstorder logic) 

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 

54 

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

56 
this implication, then apply impI to move P back into the assumptions. 

57 
To specify P use something like 

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

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

62 

63 
(*Contrapositive of an inference rule*) 

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

67 
(etac minor 1) ]); 

68 

69 

70 
(*** Modus Ponens Tactics ***) 

71 

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

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

74 

75 
(*Like mp_tac but instantiates no variables*) 

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

77 

78 

79 
(*** Ifandonlyif ***) 

80 

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

84 

85 

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

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

90 

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

92 

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

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

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

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

105 
(rtac iffI 1), 

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

107 

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

111 
[ (rtac iffI 1), 

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

113 

114 

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

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

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

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

119 
***) 

120 

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

124 

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

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

127 
"[ 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

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

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

130 

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

134 
[ (cut_facts_tac prems 1), 

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

136 

137 

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

139 

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

141 
fun iff_tac prems i = 

142 
resolve_tac (prems RL [iffE]) i THEN 

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

144 

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

148 
[ (cut_facts_tac prems 1), 

149 
(REPEAT (ares_tac [iffI,conjI] 1 

150 
ORELSE eresolve_tac [iffE,conjE,mp] 1 

151 
ORELSE iff_tac prems 1)) ]); 

152 

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

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

156 
(fn prems => 

157 
[ (cut_facts_tac prems 1), 

158 
(REPEAT (ares_tac [iffI,conjI] 1 

159 
ORELSE eresolve_tac [iffE,conjE,mp] 1 

160 
ORELSE iff_tac prems 1)) ]); 

161 

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

165 
[ (cut_facts_tac prems 1), 

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

167 
ORELSE ares_tac [iffI] 1 

168 
ORELSE mp_tac 1)) ]); 

169 

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

173 
[ (cut_facts_tac prems 1), 

174 
(REPEAT (ares_tac [iffI,impI] 1 

175 
ORELSE eresolve_tac [iffE] 1 

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

177 

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

181 
[ (cut_facts_tac prems 1), 

182 
(REPEAT (eresolve_tac [iffE] 1 

183 
ORELSE ares_tac [iffI] 1 

184 
ORELSE mp_tac 1)) ]); 

185 

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

189 
[ (cut_facts_tac prems 1), 

190 
(REPEAT (ares_tac [iffI,notI] 1 

191 
ORELSE mp_tac 1 

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

193 

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

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

198 
ORELSE mp_tac 1 

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

200 

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

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

205 
ORELSE mp_tac 1 

206 
ORELSE iff_tac prems 1)) ]); 

207 

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

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

212 
ORELSE mp_tac 1 

213 
ORELSE iff_tac prems 1)) ]); 

214 

215 
(*** Equality rules ***) 

216 

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

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

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

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

225 

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

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

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

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

233 
[ (cut_facts_tac prems 1), 

234 
(etac ex1E 1), 

235 
(rtac trans 1), 

236 
(rtac sym 2), 

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

238 

239 
(** Polymorphic congruence rules **) 

240 

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

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

245 
(resolve_tac [refl] 1) ]); 

246 

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

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

251 

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

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

256 

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

258 
a = b 

259 
  

260 
c = d *) 

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

264 
[ (resolve_tac [trans] 1), 

265 
(resolve_tac [trans] 1), 

266 
(resolve_tac [sym] 1), 

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

268 

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

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

273 
[ (resolve_tac [trans] 1), 

274 
(resolve_tac [trans] 1), 

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

276 

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

278 

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

282 
[ (cut_facts_tac prems 1), 

283 
(rtac iffI 1), 

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

285 

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

289 
[ (cut_facts_tac prems 1), 

290 
(rtac iffI 1), 

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

292 

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

296 
[ (cut_facts_tac prems 1), 

297 
(rtac iffI 1), 

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

299 

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

301 

302 
val pred_congs = 

303 
flat (map (fn c => 

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

305 
[pred1_cong,pred2_cong,pred3_cong]) 

306 
(explode"PQRS")); 

307 

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

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

310 

311 

312 
(*** Simplifications of assumed implications. 

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

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

315 
intuitionistic propositional logic. See 

316 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

318 

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

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

323 

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

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

328 

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

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

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

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

335 

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

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

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

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

342 

343 
(*Simplifies the implication. UNSAFE. *) 

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

347 
(fn major::prems=> 

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

349 

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

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

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

355 

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

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

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