author  wenzelm 
Tue, 27 Apr 1999 10:43:52 +0200  
changeset 6513  e0a9459e99fc 
parent 6433  228237ec56e5 
child 6968  7f2977e96a5c 
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 

6 
Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68 

7 
*) 

8 

9 

10 
(** Equality **) 

1660  11 
section "="; 
923  12 

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

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

15 

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

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

18 

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

20 
(fn prems => 

1465  21 
[rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]); 
923  22 

5309
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

23 
val prems = goal thy "(A == B) ==> A = B"; 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

24 
by (rewrite_goals_tac prems); 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

25 
by (rtac refl 1); 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

26 
qed "def_imp_eq"; 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

27 

923  28 
(*Useful with eresolve_tac for proving equalties from known equalities. 
1465  29 
a = b 
30 
  

31 
c = d *) 

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

34 
(fn prems=> 

35 
[ (rtac trans 1), 

36 
(rtac trans 1), 

37 
(rtac sym 1), 

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

39 

1660  40 

923  41 
(** Congruence rules for metaapplication **) 
1660  42 
section "Congruence"; 
923  43 

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

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

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

47 

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

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

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

51 

52 
qed_goal "cong" HOL.thy 

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

54 
(fn [prem1,prem2] => 

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

56 

1660  57 

923  58 
(** Equality of booleans  iff **) 
1660  59 
section "iff"; 
923  60 

61 
qed_goal "iffI" HOL.thy 

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

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

64 

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

66 
(fn prems => 

1465  67 
[rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]); 
923  68 

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

71 

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

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

923  74 

75 
qed_goal "iffE" HOL.thy 

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

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

78 

1660  79 

923  80 
(** True **) 
1660  81 
section "True"; 
923  82 

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

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

85 

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

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

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

91 

1660  92 

923  93 
(** Universal quantifier **) 
1660  94 
section "!"; 
923  95 

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

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

98 

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

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

105 

106 
qed_goal "all_dupE" HOL.thy 

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

110 

111 

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

113 
before quantifiers! **) 

1660  114 
section "False"; 
923  115 

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

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

118 

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

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

121 

122 

123 
(** Negation **) 

1660  124 
section "~"; 
923  125 

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

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

128 

5760  129 
qed_goal "False_not_True" HOL.thy "False ~= True" 
130 
(K [rtac notI 1, etac False_neq_True 1]); 

131 

132 
qed_goal "True_not_False" HOL.thy "True ~= False" 

133 
(K [rtac notI 1, dtac sym 1, etac False_neq_True 1]); 

134 

923  135 
qed_goalw "notE" HOL.thy [not_def] "[ ~P; P ] ==> R" 
136 
(fn prems => [rtac (prems MRS mp RS FalseE) 1]); 

137 

2442  138 
bind_thm ("classical2", notE RS notI); 
139 

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

142 

1660  143 

923  144 
(** Implication **) 
1660  145 
section ">"; 
923  146 

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

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

149 

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

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

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

153 

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

155 
(fn [major,minor]=> 

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

157 
(etac minor 1) ]); 

158 

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

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

162 

923  163 
(* ~(?t = ?s) ==> ~(?s = ?t) *) 
1334  164 
bind_thm("not_sym", sym COMP rev_contrapos); 
923  165 

166 

167 
(** Existential quantifier **) 

1660  168 
section "?"; 
923  169 

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

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

173 
qed_goalw "exE" HOL.thy [Ex_def] 

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

177 

178 
(** Conjunction **) 

1660  179 
section "&"; 
923  180 

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

182 
(fn prems => 

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

184 

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

186 
(fn prems => 

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

188 

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

190 
(fn prems => 

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

192 

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

194 
(fn prems => 

1465  195 
[cut_facts_tac prems 1, resolve_tac prems 1, 
196 
etac conjunct1 1, etac conjunct2 1]); 

923  197 

6433  198 
qed_goal "context_conjI" HOL.thy "[ P; P ==> Q ] ==> P & Q" 
199 
(fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]); 

200 

1660  201 

923  202 
(** Disjunction *) 
1660  203 
section ""; 
923  204 

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

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

207 

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

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

210 

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

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

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

923  215 

1660  216 

923  217 
(** CCONTR  classical logic **) 
1660  218 
section "classical logic"; 
923  219 

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

221 
(fn [prem] => 

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

223 
rtac (impI RS prem RS eqTrueI) 1, 

224 
etac subst 1, assume_tac 1]); 

225 

226 
val ccontr = FalseE RS classical; 

227 

228 
(*Double negation law*) 

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

230 
(fn [major]=> 

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

232 

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

236 
etac notE 1, 

237 
rtac p1 1]); 

1660  238 

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

2031  240 
rtac notI 1, 
241 
dtac p2 1, 

242 
etac notE 1, 

243 
rtac p1 1]); 

923  244 

245 
(** Unique existence **) 

1660  246 
section "?!"; 
923  247 

248 
qed_goalw "ex1I" HOL.thy [Ex1_def] 

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

252 

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

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

258 

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

263 

5185  264 
Goal "?! x. P x ==> ? x. P x"; 
5228  265 
by (etac ex1E 1); 
266 
by (rtac exI 1); 

267 
by (assume_tac 1); 

5185  268 
qed "ex1_implies_ex"; 
269 

923  270 

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

1660  272 
section "@"; 
923  273 

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

275 
qed_goal "selectI2" HOL.thy 

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

276 
"[ P a; !!x. P x ==> Q x ] ==> Q (@x. P x)" 
923  277 
(fn prems => [ resolve_tac prems 1, 
1465  278 
rtac selectI 1, 
279 
resolve_tac prems 1 ]); 

923  280 

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

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

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

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

287 
"[ P a; !!x. P x ==> x=a ] ==> (@x. P x) = a" 
923  288 
(fn prems => [ rtac selectI2 1, 
1465  289 
REPEAT (ares_tac prems 1) ]); 
923  290 

3646  291 
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

292 
"!!P. [ ?!x. P x; P a ] ==> (@x. P x) = a" (K [ 
4131  293 
rtac select_equality 1, atac 1, 
3646  294 
etac exE 1, etac conjE 1, 
295 
rtac allE 1, atac 1, 

296 
etac impE 1, atac 1, etac ssubst 1, 

297 
etac allE 1, etac impE 1, atac 1, etac ssubst 1, 

298 
rtac refl 1]); 

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

299 

4131  300 
qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) = (? x. P x)" (K [ 
1660  301 
rtac iffI 1, 
302 
etac exI 1, 

303 
etac exE 1, 

304 
etac selectI 1]); 

305 

5447
df03d330aeab
Proved and added rewrite rule (@x. x=y) = y to simpset.
nipkow
parents:
5346
diff
changeset

306 
qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [ 
df03d330aeab
Proved and added rewrite rule (@x. x=y) = y to simpset.
nipkow
parents:
5346
diff
changeset

307 
rtac select_equality 1, 
df03d330aeab
Proved and added rewrite rule (@x. x=y) = y to simpset.
nipkow
parents:
5346
diff
changeset

308 
rtac refl 1, 
df03d330aeab
Proved and added rewrite rule (@x. x=y) = y to simpset.
nipkow
parents:
5346
diff
changeset

309 
atac 1]); 
df03d330aeab
Proved and added rewrite rule (@x. x=y) = y to simpset.
nipkow
parents:
5346
diff
changeset

310 

df03d330aeab
Proved and added rewrite rule (@x. x=y) = y to simpset.
nipkow
parents:
5346
diff
changeset

311 
qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [ 
5299  312 
rtac select_equality 1, 
313 
rtac refl 1, 

314 
etac sym 1]); 

923  315 

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

1660  317 
section "classical intro rules"; 
923  318 

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

320 
(fn prems=> 

321 
[ (rtac classical 1), 

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

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

324 

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

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

327 

328 
(*For disjunctive case analysis*) 

329 
fun excluded_middle_tac sP = 

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

331 

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

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

334 
(fn major::prems=> 

335 
[ rtac (excluded_middle RS disjE) 1, 

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

337 

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

340 
default: would break old proofs.*) 

341 
qed_goal "impCE'" thy 

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

343 
(fn major::prems=> 

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

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

346 

923  347 
(*Classical <> elimination. *) 
348 
qed_goal "iffCE" HOL.thy 

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

350 
(fn major::prems => 

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

352 
(REPEAT (DEPTH_SOLVE_1 

1465  353 
(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]); 
923  354 

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

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

359 

360 

361 
(* case distinction *) 

362 

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

5154  364 
(fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, 
923  365 
etac p2 1, etac p1 1]); 
366 

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

368 

1660  369 

923  370 
(** Standard abbreviations **) 
371 

5309
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

372 
(*Apply an equality or definition ONCE. 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

373 
Fails unless the substitution has an effect*) 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

374 
fun stac th = 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

375 
let val th' = th RS def_imp_eq handle _ => th 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

376 
in CHANGED_GOAL (rtac (th' RS ssubst)) 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

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

378 

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

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

381 

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

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

383 

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

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

385 

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

387 
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

388 
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

389 
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

390 
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

391 

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

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

393 

1515  394 
fun RSspec th = 
395 
(case concl_of th of 

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

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

398 
in th RS forall_elim ca aspec end 

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

400 

401 
fun RSmp th = 

402 
(case concl_of th of 

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

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

405 

406 
fun normalize_thm funs = 

5346
bc9748ad8491
Now qed_spec_mp respects locales, by calling ml_store_thm
paulson
parents:
5309
diff
changeset

407 
let fun trans [] th = th 
bc9748ad8491
Now qed_spec_mp respects locales, by calling ml_store_thm
paulson
parents:
5309
diff
changeset

408 
 trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th 
bc9748ad8491
Now qed_spec_mp respects locales, by calling ml_store_thm
paulson
parents:
5309
diff
changeset

409 
in zero_var_indexes o trans funs end; 
1515  410 

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

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

412 
let val thm = normalize_thm [RSspec,RSmp] (result()) 
6214  413 
in ThmDatabase.ml_store_thm(name, thm) end; 
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3436
diff
changeset

414 

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

415 
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

416 
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

417 

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

418 
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

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

3621  421 
end; 
5888  422 

423 

424 
(* attributes *) 

425 

426 
local 

427 

6092  428 
fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x; 
5888  429 

430 
in 

431 

6513  432 
val hol_setup = 
5888  433 
[Attrib.add_attributes 
434 
[("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]]; 

435 

436 
end; 