author  wenzelm 
Mon, 16 Nov 1998 11:11:58 +0100  
changeset 5888  d8e51792ca85 
parent 5809  bacf85370ce0 
child 6092  d9db67970c73 
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 

1660  198 

923  199 
(** Disjunction *) 
1660  200 
section ""; 
923  201 

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

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

204 

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

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

207 

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

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

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

923  212 

1660  213 

923  214 
(** CCONTR  classical logic **) 
1660  215 
section "classical logic"; 
923  216 

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

218 
(fn [prem] => 

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

220 
rtac (impI RS prem RS eqTrueI) 1, 

221 
etac subst 1, assume_tac 1]); 

222 

223 
val ccontr = FalseE RS classical; 

224 

225 
(*Double negation law*) 

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

227 
(fn [major]=> 

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

229 

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

233 
etac notE 1, 

234 
rtac p1 1]); 

1660  235 

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

2031  237 
rtac notI 1, 
238 
dtac p2 1, 

239 
etac notE 1, 

240 
rtac p1 1]); 

923  241 

242 
(** Unique existence **) 

1660  243 
section "?!"; 
923  244 

245 
qed_goalw "ex1I" HOL.thy [Ex1_def] 

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

249 

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

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

255 

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

260 

5185  261 
Goal "?! x. P x ==> ? x. P x"; 
5228  262 
by (etac ex1E 1); 
263 
by (rtac exI 1); 

264 
by (assume_tac 1); 

5185  265 
qed "ex1_implies_ex"; 
266 

923  267 

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

1660  269 
section "@"; 
923  270 

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

272 
qed_goal "selectI2" HOL.thy 

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

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

923  277 

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

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

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

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

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

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

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

293 
etac impE 1, atac 1, etac ssubst 1, 

294 
etac allE 1, etac impE 1, atac 1, etac ssubst 1, 

295 
rtac refl 1]); 

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

296 

4131  297 
qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) = (? x. P x)" (K [ 
1660  298 
rtac iffI 1, 
299 
etac exI 1, 

300 
etac exE 1, 

301 
etac selectI 1]); 

302 

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

303 
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

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

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

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

307 

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

308 
qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [ 
5299  309 
rtac select_equality 1, 
310 
rtac refl 1, 

311 
etac sym 1]); 

923  312 

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

1660  314 
section "classical intro rules"; 
923  315 

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

317 
(fn prems=> 

318 
[ (rtac classical 1), 

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

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

321 

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

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

324 

325 
(*For disjunctive case analysis*) 

326 
fun excluded_middle_tac sP = 

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

328 

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

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

331 
(fn major::prems=> 

332 
[ rtac (excluded_middle RS disjE) 1, 

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

334 

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

337 
default: would break old proofs.*) 

338 
qed_goal "impCE'" thy 

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

340 
(fn major::prems=> 

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

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

343 

923  344 
(*Classical <> elimination. *) 
345 
qed_goal "iffCE" HOL.thy 

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

347 
(fn major::prems => 

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

349 
(REPEAT (DEPTH_SOLVE_1 

1465  350 
(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]); 
923  351 

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

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

356 

357 

358 
(* case distinction *) 

359 

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

5154  361 
(fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, 
923  362 
etac p2 1, etac p1 1]); 
363 

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

365 

1660  366 

923  367 
(** Standard abbreviations **) 
368 

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

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

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

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

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

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

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

375 

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

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

378 

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

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

380 

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

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

382 

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

384 
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

385 
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

386 
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

387 
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

388 

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

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

390 

1515  391 
fun RSspec th = 
392 
(case concl_of th of 

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

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

395 
in th RS forall_elim ca aspec end 

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

397 

398 
fun RSmp th = 

399 
(case concl_of th of 

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

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

402 

403 
fun normalize_thm funs = 

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

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

405 
 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

406 
in zero_var_indexes o trans funs end; 
1515  407 

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

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

409 
let val thm = normalize_thm [RSspec,RSmp] (result()) 
5346
bc9748ad8491
Now qed_spec_mp respects locales, by calling ml_store_thm
paulson
parents:
5309
diff
changeset

410 
in 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

411 

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

412 
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

413 
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

414 

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

415 
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

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

3621  418 
end; 
5888  419 

420 

421 
(* attributes *) 

422 

423 
local 

424 

425 
fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x; 

426 

427 
in 

428 

429 
val attrib_setup = 

430 
[Attrib.add_attributes 

431 
[("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]]; 

432 

433 
end; 