author  paulson 
Wed, 26 Nov 1997 17:23:18 +0100  
changeset 4302  2c99775d953f 
parent 4131  916641b59219 
child 4467  bd05e2a28602 
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 

67 
val iffD1 = sym RS iffD2; 

68 

69 
qed_goal "iffE" HOL.thy 

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

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

72 

1660  73 

923  74 
(** True **) 
1660  75 
section "True"; 
923  76 

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

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

79 

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

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

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

85 

1660  86 

923  87 
(** Universal quantifier **) 
1660  88 
section "!"; 
923  89 

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

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

92 

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

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

99 

100 
qed_goal "all_dupE" HOL.thy 

3842  101 
"[ ! x. P(x); [ P(x); ! x. P(x) ] ==> R ] ==> R" 
923  102 
(fn prems => 
103 
[ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]); 

104 

105 

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

107 
before quantifiers! **) 

1660  108 
section "False"; 
923  109 

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

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

112 

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

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

115 

116 

117 
(** Negation **) 

1660  118 
section "~"; 
923  119 

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

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

122 

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

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

125 

2442  126 
bind_thm ("classical2", notE RS notI); 
127 

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

130 

1660  131 

923  132 
(** Implication **) 
1660  133 
section ">"; 
923  134 

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

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

137 

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

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

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

141 

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

143 
(fn [major,minor]=> 

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

145 
(etac minor 1) ]); 

146 

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

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

150 

923  151 
(* ~(?t = ?s) ==> ~(?s = ?t) *) 
1334  152 
bind_thm("not_sym", sym COMP rev_contrapos); 
923  153 

154 

155 
(** Existential quantifier **) 

1660  156 
section "?"; 
923  157 

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

161 
qed_goalw "exE" HOL.thy [Ex_def] 

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

165 

166 
(** Conjunction **) 

1660  167 
section "&"; 
923  168 

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

170 
(fn prems => 

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

172 

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

174 
(fn prems => 

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

176 

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

178 
(fn prems => 

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

180 

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

182 
(fn prems => 

1465  183 
[cut_facts_tac prems 1, resolve_tac prems 1, 
184 
etac conjunct1 1, etac conjunct2 1]); 

923  185 

1660  186 

923  187 
(** Disjunction *) 
1660  188 
section ""; 
923  189 

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

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

192 

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

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

195 

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

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

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

923  200 

1660  201 

923  202 
(** CCONTR  classical logic **) 
1660  203 
section "classical logic"; 
923  204 

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

206 
(fn [prem] => 

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

208 
rtac (impI RS prem RS eqTrueI) 1, 

209 
etac subst 1, assume_tac 1]); 

210 

211 
val ccontr = FalseE RS classical; 

212 

213 
(*Double negation law*) 

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

215 
(fn [major]=> 

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

217 

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

221 
etac notE 1, 

222 
rtac p1 1]); 

1660  223 

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

2031  225 
rtac notI 1, 
226 
dtac p2 1, 

227 
etac notE 1, 

228 
rtac p1 1]); 

923  229 

230 
(** Unique existence **) 

1660  231 
section "?!"; 
923  232 

233 
qed_goalw "ex1I" HOL.thy [Ex1_def] 

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

237 

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

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

243 

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

248 

249 

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

1660  251 
section "@"; 
923  252 

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

254 
qed_goal "selectI2" HOL.thy 

3842  255 
"[ P(a); !!x. P(x) ==> Q(x) ] ==> Q(@x. P(x))" 
923  256 
(fn prems => [ resolve_tac prems 1, 
1465  257 
rtac selectI 1, 
258 
resolve_tac prems 1 ]); 

923  259 

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

3842  262 
"[ ? a. P a; !!x. P x ==> Q x ] ==> Q(Eps P)" 
3646  263 
(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]); 
264 

923  265 
qed_goal "select_equality" HOL.thy 
3842  266 
"[ P(a); !!x. P(x) ==> x=a ] ==> (@x. P(x)) = a" 
923  267 
(fn prems => [ rtac selectI2 1, 
1465  268 
REPEAT (ares_tac prems 1) ]); 
923  269 

3646  270 
qed_goalw "select1_equality" HOL.thy [Ex1_def] 
4131  271 
"!!P. [ ?!x. P(x); P(a) ] ==> (@x. P(x)) = a" (K [ 
272 
rtac select_equality 1, atac 1, 

3646  273 
etac exE 1, etac conjE 1, 
274 
rtac allE 1, atac 1, 

275 
etac impE 1, atac 1, etac ssubst 1, 

276 
etac allE 1, etac impE 1, atac 1, etac ssubst 1, 

277 
rtac refl 1]); 

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

278 

4131  279 
qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) = (? x. P x)" (K [ 
1660  280 
rtac iffI 1, 
281 
etac exI 1, 

282 
etac exE 1, 

283 
etac selectI 1]); 

284 

4131  285 
val Eps_eq = prove_goal HOL.thy "Eps (op = x) = x" (K [ 
286 
rtac select_equality 1, rtac refl 1, etac sym 1]); 

287 

288 
val ex1_Eps_eq = prove_goal HOL.thy "!!X. [?!x. P x; P y] ==> Eps P = y" (K [ 

289 
rtac select_equality 1, 

290 
atac 1, 

291 
etac ex1E 1, 

292 
etac all_dupE 1, 

293 
etac impE 1, 

294 
atac 1, 

295 
rtac trans 1, 

296 
etac sym 2, 

297 
dtac spec 1, 

298 
etac impE 1, 

299 
ALLGOALS atac]); 

300 

923  301 

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

1660  303 
section "classical intro rules"; 
923  304 

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

306 
(fn prems=> 

307 
[ (rtac classical 1), 

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

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

310 

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

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

313 

314 
(*For disjunctive case analysis*) 

315 
fun excluded_middle_tac sP = 

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

317 

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

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

320 
(fn major::prems=> 

321 
[ rtac (excluded_middle RS disjE) 1, 

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

323 

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

326 
default: would break old proofs.*) 

327 
qed_goal "impCE'" thy 

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

329 
(fn major::prems=> 

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

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

332 

923  333 
(*Classical <> elimination. *) 
334 
qed_goal "iffCE" HOL.thy 

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

336 
(fn major::prems => 

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

338 
(REPEAT (DEPTH_SOLVE_1 

1465  339 
(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]); 
923  340 

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

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

345 

346 

347 
(* case distinction *) 

348 

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

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

351 
etac p2 1, etac p1 1]); 

352 

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

354 

1660  355 

923  356 
(** Standard abbreviations **) 
357 

1672
2c109cd2fdd0
repaired critical proofs depending on the order inside nonconfluent SimpSets,
oheimb
parents:
1668
diff
changeset

358 
fun stac th = CHANGED o rtac (th RS ssubst); 
923  359 
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
1338  360 

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

361 

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

362 
(** 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

363 

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

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

365 

1515  366 
(* 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

367 
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

368 
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

369 
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

370 
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

371 

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

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

373 

1515  374 
fun RSspec th = 
375 
(case concl_of th of 

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

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

378 
in th RS forall_elim ca aspec end 

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

380 

381 
fun RSmp th = 

382 
(case concl_of th of 

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

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

385 

386 
fun normalize_thm funs = 

387 
let fun trans [] th = th 

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

389 
in trans funs end; 

390 

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

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

392 
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

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

394 

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

395 
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

396 
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

397 

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

398 
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

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

3621  401 
end; 