author  paulson 
Thu, 20 Aug 1998 09:25:59 +0200  
changeset 5346  bc9748ad8491 
parent 5309  01c2b317da88 
child 5447  df03d330aeab 
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 

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

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

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

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

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

30 

923  31 
(*Useful with eresolve_tac for proving equalties from known equalities. 
1465  32 
a = b 
33 
  

34 
c = d *) 

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

37 
(fn prems=> 

38 
[ (rtac trans 1), 

39 
(rtac trans 1), 

40 
(rtac sym 1), 

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

42 

1660  43 

923  44 
(** Congruence rules for metaapplication **) 
1660  45 
section "Congruence"; 
923  46 

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

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

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

50 

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

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

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

54 

55 
qed_goal "cong" HOL.thy 

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

57 
(fn [prem1,prem2] => 

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

59 

1660  60 

923  61 
(** Equality of booleans  iff **) 
1660  62 
section "iff"; 
923  63 

64 
qed_goal "iffI" HOL.thy 

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

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

67 

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

69 
(fn prems => 

1465  70 
[rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]); 
923  71 

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

74 

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

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

923  77 

78 
qed_goal "iffE" HOL.thy 

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

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

81 

1660  82 

923  83 
(** True **) 
1660  84 
section "True"; 
923  85 

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

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

88 

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

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

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

94 

1660  95 

923  96 
(** Universal quantifier **) 
1660  97 
section "!"; 
923  98 

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

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

101 

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

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

108 

109 
qed_goal "all_dupE" HOL.thy 

3842  110 
"[ ! x. P(x); [ P(x); ! x. P(x) ] ==> R ] ==> R" 
923  111 
(fn prems => 
112 
[ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]); 

113 

114 

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

116 
before quantifiers! **) 

1660  117 
section "False"; 
923  118 

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

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

121 

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

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

124 

125 

126 
(** Negation **) 

1660  127 
section "~"; 
923  128 

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

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

131 

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

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

134 

2442  135 
bind_thm ("classical2", notE RS notI); 
136 

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

139 

1660  140 

923  141 
(** Implication **) 
1660  142 
section ">"; 
923  143 

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

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

146 

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

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

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

150 

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

152 
(fn [major,minor]=> 

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

154 
(etac minor 1) ]); 

155 

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

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

159 

923  160 
(* ~(?t = ?s) ==> ~(?s = ?t) *) 
1334  161 
bind_thm("not_sym", sym COMP rev_contrapos); 
923  162 

163 

164 
(** Existential quantifier **) 

1660  165 
section "?"; 
923  166 

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

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

170 
qed_goalw "exE" HOL.thy [Ex_def] 

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

174 

175 
(** Conjunction **) 

1660  176 
section "&"; 
923  177 

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

179 
(fn prems => 

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

181 

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

183 
(fn prems => 

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

185 

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

187 
(fn prems => 

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

189 

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

191 
(fn prems => 

1465  192 
[cut_facts_tac prems 1, resolve_tac prems 1, 
193 
etac conjunct1 1, etac conjunct2 1]); 

923  194 

1660  195 

923  196 
(** Disjunction *) 
1660  197 
section ""; 
923  198 

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

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

201 

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

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

204 

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

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

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

923  209 

1660  210 

923  211 
(** CCONTR  classical logic **) 
1660  212 
section "classical logic"; 
923  213 

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

215 
(fn [prem] => 

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

217 
rtac (impI RS prem RS eqTrueI) 1, 

218 
etac subst 1, assume_tac 1]); 

219 

220 
val ccontr = FalseE RS classical; 

221 

222 
(*Double negation law*) 

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

224 
(fn [major]=> 

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

226 

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

230 
etac notE 1, 

231 
rtac p1 1]); 

1660  232 

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

2031  234 
rtac notI 1, 
235 
dtac p2 1, 

236 
etac notE 1, 

237 
rtac p1 1]); 

923  238 

239 
(** Unique existence **) 

1660  240 
section "?!"; 
923  241 

242 
qed_goalw "ex1I" HOL.thy [Ex1_def] 

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

246 

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

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

252 

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

257 

5185  258 
Goal "?! x. P x ==> ? x. P x"; 
5228  259 
by (etac ex1E 1); 
260 
by (rtac exI 1); 

261 
by (assume_tac 1); 

5185  262 
qed "ex1_implies_ex"; 
263 

923  264 

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

1660  266 
section "@"; 
923  267 

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

269 
qed_goal "selectI2" 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 ==> Q x ] ==> Q (@x. P x)" 
923  271 
(fn prems => [ resolve_tac prems 1, 
1465  272 
rtac selectI 1, 
273 
resolve_tac prems 1 ]); 

923  274 

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

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

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

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

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

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

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

290 
etac impE 1, atac 1, etac ssubst 1, 

291 
etac allE 1, etac impE 1, atac 1, etac ssubst 1, 

292 
rtac refl 1]); 

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

293 

4131  294 
qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) = (? x. P x)" (K [ 
1660  295 
rtac iffI 1, 
296 
etac exI 1, 

297 
etac exE 1, 

298 
etac selectI 1]); 

299 

5299  300 
qed_goal "Eps_eq" HOL.thy "(Eps (op = x)) = x" (K [ 
301 
rtac select_equality 1, 

302 
rtac refl 1, 

303 
etac sym 1]); 

923  304 

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

1660  306 
section "classical intro rules"; 
923  307 

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

309 
(fn prems=> 

310 
[ (rtac classical 1), 

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

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

313 

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

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

316 

317 
(*For disjunctive case analysis*) 

318 
fun excluded_middle_tac sP = 

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

320 

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

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

323 
(fn major::prems=> 

324 
[ rtac (excluded_middle RS disjE) 1, 

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

326 

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

329 
default: would break old proofs.*) 

330 
qed_goal "impCE'" thy 

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

332 
(fn major::prems=> 

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

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

335 

923  336 
(*Classical <> elimination. *) 
337 
qed_goal "iffCE" HOL.thy 

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

339 
(fn major::prems => 

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

341 
(REPEAT (DEPTH_SOLVE_1 

1465  342 
(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]); 
923  343 

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

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

348 

349 

350 
(* case distinction *) 

351 

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

5154  353 
(fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, 
923  354 
etac p2 1, etac p1 1]); 
355 

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

357 

1660  358 

923  359 
(** Standard abbreviations **) 
360 

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

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

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

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

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

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

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

367 

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

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

370 

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

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

372 

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

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

374 

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

376 
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

377 
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

378 
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

379 
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

380 

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

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

382 

1515  383 
fun RSspec th = 
384 
(case concl_of th of 

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

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

387 
in th RS forall_elim ca aspec end 

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

389 

390 
fun RSmp th = 

391 
(case concl_of th of 

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

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

394 

395 
fun normalize_thm funs = 

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

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

397 
 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

398 
in zero_var_indexes o trans funs end; 
1515  399 

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

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

401 
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

402 
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

403 

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

404 
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

405 
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

406 

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

407 
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

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

3621  410 
end; 