author  paulson 
Tue, 14 Jul 1998 13:29:39 +0200  
changeset 5139  013ea0f023e3 
parent 4527  4878fb3d0ac5 
child 5154  40fd46f3d3a1 
permissions  rwrr 
1465  1 
(* Title: HOL/HOL.ML 
923  2 
ID: $Id$ 
1465  3 
Author: Tobias Nipkow 
923  4 
Copyright 1991 University of Cambridge 
5 

1465  6 
For HOL.thy 
923  7 
Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68 
8 
*) 

9 

10 
open HOL; 

11 

12 

13 
(** Equality **) 

1660  14 
section "="; 
923  15 

16 
qed_goal "sym" HOL.thy "s=t ==> t=s" 

17 
(fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]); 

18 

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

20 
bind_thm ("ssubst", (sym RS subst)); 

21 

22 
qed_goal "trans" HOL.thy "[ r=s; s=t ] ==> r=t" 

23 
(fn prems => 

1465  24 
[rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]); 
923  25 

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

1465  27 
a = b 
28 
  

29 
c = d *) 

923  30 
qed_goal "box_equals" HOL.thy 
31 
"[ a=b; a=c; b=d ] ==> c=d" 

32 
(fn prems=> 

33 
[ (rtac trans 1), 

34 
(rtac trans 1), 

35 
(rtac sym 1), 

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

37 

1660  38 

923  39 
(** Congruence rules for metaapplication **) 
1660  40 
section "Congruence"; 
923  41 

42 
(*similar to AP_THM in Gordon's HOL*) 

43 
qed_goal "fun_cong" HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)" 

44 
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); 

45 

46 
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) 

47 
qed_goal "arg_cong" HOL.thy "x=y ==> f(x)=f(y)" 

48 
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); 

49 

50 
qed_goal "cong" HOL.thy 

51 
"[ f = g; (x::'a) = y ] ==> f(x) = g(y)" 

52 
(fn [prem1,prem2] => 

53 
[rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]); 

54 

1660  55 

923  56 
(** Equality of booleans  iff **) 
1660  57 
section "iff"; 
923  58 

59 
qed_goal "iffI" HOL.thy 

60 
"[ P ==> Q; Q ==> P ] ==> P=Q" 

61 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1)) ]); 

62 

63 
qed_goal "iffD2" HOL.thy "[ P=Q; Q ] ==> P" 

64 
(fn prems => 

1465  65 
[rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]); 
923  66 

4467  67 
qed_goal "rev_iffD2" HOL.thy "!!P. [ Q; P=Q ] ==> P" 
68 
(fn _ => [etac iffD2 1, assume_tac 1]); 

69 

70 
bind_thm ("iffD1", sym RS iffD2); 

71 
bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2)); 

923  72 

73 
qed_goal "iffE" HOL.thy 

74 
"[ P=Q; [ P > Q; Q > P ] ==> R ] ==> R" 

75 
(fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]); 

76 

1660  77 

923  78 
(** True **) 
1660  79 
section "True"; 
923  80 

81 
qed_goalw "TrueI" HOL.thy [True_def] "True" 

82 
(fn _ => [rtac refl 1]); 

83 

4025  84 
qed_goal "eqTrueI" HOL.thy "P ==> P=True" 
923  85 
(fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]); 
86 

87 
qed_goal "eqTrueE" HOL.thy "P=True ==> P" 

88 
(fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]); 

89 

1660  90 

923  91 
(** Universal quantifier **) 
1660  92 
section "!"; 
923  93 

94 
qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)" 

95 
(fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]); 

96 

3842  97 
qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)" 
923  98 
(fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]); 
99 

3842  100 
qed_goal "allE" HOL.thy "[ !x. P(x); P(x) ==> R ] ==> R" 
923  101 
(fn major::prems=> 
102 
[ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]); 

103 

104 
qed_goal "all_dupE" HOL.thy 

3842  105 
"[ ! x. P(x); [ P(x); ! x. P(x) ] ==> R ] ==> R" 
923  106 
(fn prems => 
107 
[ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]); 

108 

109 

110 
(** False ** Depends upon spec; it is impossible to do propositional logic 

111 
before quantifiers! **) 

1660  112 
section "False"; 
923  113 

114 
qed_goalw "FalseE" HOL.thy [False_def] "False ==> P" 

115 
(fn [major] => [rtac (major RS spec) 1]); 

116 

117 
qed_goal "False_neq_True" HOL.thy "False=True ==> P" 

118 
(fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]); 

119 

120 

121 
(** Negation **) 

1660  122 
section "~"; 
923  123 

124 
qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P" 

125 
(fn prems=> [rtac impI 1, eresolve_tac prems 1]); 

126 

127 
qed_goalw "notE" HOL.thy [not_def] "[ ~P; P ] ==> R" 

128 
(fn prems => [rtac (prems MRS mp RS FalseE) 1]); 

129 

2442  130 
bind_thm ("classical2", notE RS notI); 
131 

1840  132 
qed_goal "rev_notE" HOL.thy "!!P R. [ P; ~P ] ==> R" 
133 
(fn _ => [REPEAT (ares_tac [notE] 1)]); 

134 

1660  135 

923  136 
(** Implication **) 
1660  137 
section ">"; 
923  138 

139 
qed_goal "impE" HOL.thy "[ P>Q; P; Q ==> R ] ==> R" 

140 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); 

141 

142 
(* Reduces Q to P>Q, allowing substitution in P. *) 

143 
qed_goal "rev_mp" HOL.thy "[ P; P > Q ] ==> Q" 

144 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); 

145 

146 
qed_goal "contrapos" HOL.thy "[ ~Q; P==>Q ] ==> ~P" 

147 
(fn [major,minor]=> 

148 
[ (rtac (major RS notE RS notI) 1), 

149 
(etac minor 1) ]); 

150 

1334  151 
qed_goal "rev_contrapos" HOL.thy "[ P==>Q; ~Q ] ==> ~P" 
152 
(fn [major,minor]=> 

153 
[ (rtac (minor RS contrapos) 1), (etac major 1) ]); 

154 

923  155 
(* ~(?t = ?s) ==> ~(?s = ?t) *) 
1334  156 
bind_thm("not_sym", sym COMP rev_contrapos); 
923  157 

158 

159 
(** Existential quantifier **) 

1660  160 
section "?"; 
923  161 

4527
4878fb3d0ac5
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
oheimb
parents:
4467
diff
changeset

162 
qed_goalw "exI" HOL.thy [Ex_def] "P x ==> ? x::'a. P x" 
923  163 
(fn prems => [rtac selectI 1, resolve_tac prems 1]); 
164 

165 
qed_goalw "exE" HOL.thy [Ex_def] 

3842  166 
"[ ? x::'a. P(x); !!x. P(x) ==> Q ] ==> Q" 
923  167 
(fn prems => [REPEAT(resolve_tac prems 1)]); 
168 

169 

170 
(** Conjunction **) 

1660  171 
section "&"; 
923  172 

173 
qed_goalw "conjI" HOL.thy [and_def] "[ P; Q ] ==> P&Q" 

174 
(fn prems => 

175 
[REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]); 

176 

177 
qed_goalw "conjunct1" HOL.thy [and_def] "[ P & Q ] ==> P" 

178 
(fn prems => 

179 
[resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]); 

180 

181 
qed_goalw "conjunct2" HOL.thy [and_def] "[ P & Q ] ==> Q" 

182 
(fn prems => 

183 
[resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]); 

184 

185 
qed_goal "conjE" HOL.thy "[ P&Q; [ P; Q ] ==> R ] ==> R" 

186 
(fn prems => 

1465  187 
[cut_facts_tac prems 1, resolve_tac prems 1, 
188 
etac conjunct1 1, etac conjunct2 1]); 

923  189 

1660  190 

923  191 
(** Disjunction *) 
1660  192 
section ""; 
923  193 

194 
qed_goalw "disjI1" HOL.thy [or_def] "P ==> PQ" 

195 
(fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]); 

196 

197 
qed_goalw "disjI2" HOL.thy [or_def] "Q ==> PQ" 

198 
(fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]); 

199 

200 
qed_goalw "disjE" HOL.thy [or_def] "[ P  Q; P ==> R; Q ==> R ] ==> R" 

201 
(fn [a1,a2,a3] => 

1465  202 
[rtac (mp RS mp) 1, rtac spec 1, rtac a1 1, 
203 
rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]); 

923  204 

1660  205 

923  206 
(** CCONTR  classical logic **) 
1660  207 
section "classical logic"; 
923  208 

209 
qed_goalw "classical" HOL.thy [not_def] "(~P ==> P) ==> P" 

210 
(fn [prem] => 

211 
[rtac (True_or_False RS (disjE RS eqTrueE)) 1, assume_tac 1, 

212 
rtac (impI RS prem RS eqTrueI) 1, 

213 
etac subst 1, assume_tac 1]); 

214 

215 
val ccontr = FalseE RS classical; 

216 

217 
(*Double negation law*) 

218 
qed_goal "notnotD" HOL.thy "~~P ==> P" 

219 
(fn [major]=> 

220 
[ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); 

221 

1660  222 
qed_goal "contrapos2" HOL.thy "[ Q; ~ P ==> ~ Q ] ==> P" (fn [p1,p2] => [ 
2031  223 
rtac classical 1, 
224 
dtac p2 1, 

225 
etac notE 1, 

226 
rtac p1 1]); 

1660  227 

228 
qed_goal "swap2" HOL.thy "[ P; Q ==> ~ P ] ==> ~ Q" (fn [p1,p2] => [ 

2031  229 
rtac notI 1, 
230 
dtac p2 1, 

231 
etac notE 1, 

232 
rtac p1 1]); 

923  233 

234 
(** Unique existence **) 

1660  235 
section "?!"; 
923  236 

237 
qed_goalw "ex1I" HOL.thy [Ex1_def] 

2031  238 
"[ P(a); !!x. P(x) ==> x=a ] ==> ?! x. P(x)" 
923  239 
(fn prems => 
240 
[REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]); 

241 

3003  242 
(*Sometimes easier to use: the premises have no shared variables. Safe!*) 
243 
qed_goal "ex_ex1I" HOL.thy 

3842  244 
"[ ? x. P(x); !!x y. [ P(x); P(y) ] ==> x=y ] ==> ?! x. P(x)" 
3003  245 
(fn [ex,eq] => [ (rtac (ex RS exE) 1), 
246 
(REPEAT (ares_tac [ex1I,eq] 1)) ]); 

247 

923  248 
qed_goalw "ex1E" HOL.thy [Ex1_def] 
3842  249 
"[ ?! x. P(x); !!x. [ P(x); ! y. P(y) > y=x ] ==> R ] ==> R" 
923  250 
(fn major::prems => 
251 
[rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]); 

252 

253 

254 
(** Select: Hilbert's Epsilonoperator **) 

1660  255 
section "@"; 
923  256 

257 
(*Easier to apply than selectI: conclusion has only one occurrence of P*) 

258 
qed_goal "selectI2" HOL.thy 

4527
4878fb3d0ac5
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
oheimb
parents:
4467
diff
changeset

259 
"[ P a; !!x. P x ==> Q x ] ==> Q (@x. P x)" 
923  260 
(fn prems => [ resolve_tac prems 1, 
1465  261 
rtac selectI 1, 
262 
resolve_tac prems 1 ]); 

923  263 

3646  264 
(*Easier to apply than selectI2 if witness ?a comes from an EXformula*) 
265 
qed_goal "selectI2EX" HOL.thy 

4527
4878fb3d0ac5
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
oheimb
parents:
4467
diff
changeset

266 
"[ ? a. P a; !!x. P x ==> Q x ] ==> Q (Eps P)" 
3646  267 
(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]); 
268 

923  269 
qed_goal "select_equality" HOL.thy 
4527
4878fb3d0ac5
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
oheimb
parents:
4467
diff
changeset

270 
"[ P a; !!x. P x ==> x=a ] ==> (@x. P x) = a" 
923  271 
(fn prems => [ rtac selectI2 1, 
1465  272 
REPEAT (ares_tac prems 1) ]); 
923  273 

3646  274 
qed_goalw "select1_equality" HOL.thy [Ex1_def] 
4527
4878fb3d0ac5
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
oheimb
parents:
4467
diff
changeset

275 
"!!P. [ ?!x. P x; P a ] ==> (@x. P x) = a" (K [ 
4131  276 
rtac select_equality 1, atac 1, 
3646  277 
etac exE 1, etac conjE 1, 
278 
rtac allE 1, atac 1, 

279 
etac impE 1, atac 1, etac ssubst 1, 

280 
etac allE 1, etac impE 1, atac 1, etac ssubst 1, 

281 
rtac refl 1]); 

3436
d68dbb8f22d3
Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
nipkow
parents:
3003
diff
changeset

282 

4131  283 
qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) = (? x. P x)" (K [ 
1660  284 
rtac iffI 1, 
285 
etac exI 1, 

286 
etac exE 1, 

287 
etac selectI 1]); 

288 

923  289 

290 
(** Classical intro rules for disjunction and existential quantifiers *) 

1660  291 
section "classical intro rules"; 
923  292 

293 
qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> PQ" 

294 
(fn prems=> 

295 
[ (rtac classical 1), 

296 
(REPEAT (ares_tac (prems@[disjI1,notI]) 1)), 

297 
(REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]); 

298 

299 
qed_goal "excluded_middle" HOL.thy "~P  P" 

300 
(fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]); 

301 

302 
(*For disjunctive case analysis*) 

303 
fun excluded_middle_tac sP = 

304 
res_inst_tac [("Q",sP)] (excluded_middle RS disjE); 

305 

306 
(*Classical implies (>) elimination. *) 

307 
qed_goal "impCE" HOL.thy "[ P>Q; ~P ==> R; Q ==> R ] ==> R" 

308 
(fn major::prems=> 

309 
[ rtac (excluded_middle RS disjE) 1, 

310 
REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]); 

311 

4302  312 
(*This version of > elimination works on Q before P. It works best for 
313 
those cases in which P holds "almost everywhere". Can't install as 

314 
default: would break old proofs.*) 

315 
qed_goal "impCE'" thy 

316 
"[ P>Q; Q ==> R; ~P ==> R ] ==> R" 

317 
(fn major::prems=> 

318 
[ (resolve_tac [excluded_middle RS disjE] 1), 

319 
(DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); 

320 

923  321 
(*Classical <> elimination. *) 
322 
qed_goal "iffCE" HOL.thy 

323 
"[ P=Q; [ P; Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R" 

324 
(fn major::prems => 

325 
[ (rtac (major RS iffE) 1), 

326 
(REPEAT (DEPTH_SOLVE_1 

1465  327 
(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]); 
923  328 

3842  329 
qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)" 
923  330 
(fn prems=> 
331 
[ (rtac ccontr 1), 

332 
(REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1)) ]); 

333 

334 

335 
(* case distinction *) 

336 

337 
qed_goal "case_split_thm" HOL.thy "[ P ==> Q; ~P ==> Q ] ==> Q" 

338 
(fn [p1,p2] => [cut_facts_tac [excluded_middle] 1, etac disjE 1, 

339 
etac p2 1, etac p1 1]); 

340 

341 
fun case_tac a = res_inst_tac [("P",a)] case_split_thm; 

342 

1660  343 

923  344 
(** Standard abbreviations **) 
345 

5139
013ea0f023e3
stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
paulson
parents:
4527
diff
changeset

346 
(*Fails unless the substitution has an effect*) 
013ea0f023e3
stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
paulson
parents:
4527
diff
changeset

347 
fun stac th = CHANGED_GOAL (rtac (th RS ssubst)); 
013ea0f023e3
stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
paulson
parents:
4527
diff
changeset

348 

923  349 
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
1338  350 

2562
d571d6660240
Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work
paulson
parents:
2442
diff
changeset

351 

d571d6660240
Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work
paulson
parents:
2442
diff
changeset

352 
(** strip ! and > from proved goal while preserving !bound var names **) 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

353 

240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

354 
local 
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

355 

1515  356 
(* Use XXX to avoid forall_intr failing because of duplicate variable name *) 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

357 
val myspec = read_instantiate [("P","?XXX")] spec; 
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

358 
val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec; 
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

359 
val cvx = cterm_of (#sign(rep_thm myspec)) vx; 
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

360 
val aspec = forall_intr cvx myspec; 
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

361 

240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

362 
in 
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset

363 

1515  364 
fun RSspec th = 
365 
(case concl_of th of 

366 
_ $ (Const("All",_) $ Abs(a,_,_)) => 

367 
let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT)) 

368 
in th RS forall_elim ca aspec end 

369 
 _ => raise THM("RSspec",0,[th])); 

370 

371 
fun RSmp th = 

372 
(case concl_of th of 

373 
_ $ (Const("op >",_)$_$_) => th RS mp 

374 
 _ => raise THM("RSmp",0,[th])); 

375 

376 
fun normalize_thm funs = 

377 
let fun trans [] th = th 

378 
 trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th 

379 
in trans funs end; 

380 

3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

381 
fun qed_spec_mp name = 
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

382 
let val thm = normalize_thm [RSspec,RSmp] (result()) 
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

383 
in bind_thm(name, thm) end; 
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

384 

e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

385 
fun qed_goal_spec_mp name thy s p = 
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

386 
bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p)); 
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

387 

e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

388 
fun qed_goalw_spec_mp name thy defs s p = 
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

389 
bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p)); 
1660  390 

3621  391 
end; 