author  paulson 
Mon, 19 Jul 1999 15:19:11 +0200  
changeset 7030  53934985426a 
parent 6968  7f2977e96a5c 
child 7357  d0e16da40ea2 
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 *) 

7030  32 
Goal "[ a=b; a=c; b=d ] ==> c=d"; 
33 
by (rtac trans 1); 

34 
by (rtac trans 1); 

35 
by (rtac sym 1); 

36 
by (REPEAT (assume_tac 1)) ; 

37 
qed "box_equals"; 

923  38 

1660  39 

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

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

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

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

46 

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

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

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

50 

51 
qed_goal "cong" HOL.thy 

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

53 
(fn [prem1,prem2] => 

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

55 

1660  56 

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

7030  60 
val prems = Goal 
61 
"[ P ==> Q; Q ==> P ] ==> P=Q"; 

62 
by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1)); 

63 
qed "iffI"; 

923  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" 

7030  84 
(fn _ => [(rtac refl 1)]); 
923  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)" 

7030  97 
(fn prems => [(resolve_tac (prems RL [eqTrueI RS ext]) 1)]); 
923  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 

7030  102 
val major::prems= goal HOL.thy "[ !x. P(x); P(x) ==> R ] ==> R"; 
103 
by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ; 

104 
qed "allE"; 

923  105 

7030  106 
val prems = goal HOL.thy 
107 
"[ ! x. P(x); [ P(x); ! x. P(x) ] ==> R ] ==> R"; 

108 
by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ; 

109 
qed "all_dupE"; 

923  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" 
7030  130 
(fn _ => [rtac notI 1, etac False_neq_True 1]); 
5760  131 

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

7030  133 
(fn _ => [rtac notI 1, dtac sym 1, etac False_neq_True 1]); 
5760  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 

7030  147 
val prems = Goal "[ P>Q; P; Q ==> R ] ==> R"; 
148 
by (REPEAT (resolve_tac (prems@[mp]) 1)); 

149 
qed "impE"; 

923  150 

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

7030  152 
Goal "[ P; P > Q ] ==> Q"; 
153 
by (REPEAT (ares_tac [mp] 1)) ; 

154 
qed "rev_mp"; 

923  155 

7030  156 
val [major,minor] = Goal "[ ~Q; P==>Q ] ==> ~P"; 
157 
by (rtac (major RS notE RS notI) 1); 

158 
by (etac minor 1) ; 

159 
qed "contrapos"; 

923  160 

7030  161 
val [major,minor] = Goal "[ P==>Q; ~Q ] ==> ~P"; 
162 
by (rtac (minor RS contrapos) 1); 

163 
by (etac major 1) ; 

164 
qed "rev_contrapos"; 

1334  165 

923  166 
(* ~(?t = ?s) ==> ~(?s = ?t) *) 
1334  167 
bind_thm("not_sym", sym COMP rev_contrapos); 
923  168 

169 

170 
(** Existential quantifier **) 

1660  171 
section "?"; 
923  172 

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

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

176 
qed_goalw "exE" HOL.thy [Ex_def] 

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

180 

181 
(** Conjunction **) 

1660  182 
section "&"; 
923  183 

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

185 
(fn prems => 

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

187 

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

189 
(fn prems => 

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

191 

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

193 
(fn prems => 

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

195 

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

197 
(fn prems => 

1465  198 
[cut_facts_tac prems 1, resolve_tac prems 1, 
199 
etac conjunct1 1, etac conjunct2 1]); 

923  200 

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

203 

1660  204 

923  205 
(** Disjunction *) 
1660  206 
section ""; 
923  207 

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

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

210 

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

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

213 

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

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

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

923  218 

1660  219 

923  220 
(** CCONTR  classical logic **) 
1660  221 
section "classical logic"; 
923  222 

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

224 
(fn [prem] => 

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

226 
rtac (impI RS prem RS eqTrueI) 1, 

227 
etac subst 1, assume_tac 1]); 

228 

229 
val ccontr = FalseE RS classical; 

230 

231 
(*Double negation law*) 

7030  232 
Goal "~~P ==> P"; 
233 
by (rtac classical 1); 

234 
by (etac notE 1); 

235 
by (assume_tac 1); 

236 
qed "notnotD"; 

923  237 

7030  238 
val [p1,p2] = Goal "[ Q; ~ P ==> ~ Q ] ==> P"; 
239 
by (rtac classical 1); 

240 
by (dtac p2 1); 

241 
by (etac notE 1); 

242 
by (rtac p1 1); 

243 
qed "contrapos2"; 

1660  244 

7030  245 
val [p1,p2] = Goal "[ P; Q ==> ~ P ] ==> ~ Q"; 
246 
by (rtac notI 1); 

247 
by (dtac p2 1); 

248 
by (etac notE 1); 

249 
by (rtac p1 1); 

250 
qed "swap2"; 

923  251 

252 
(** Unique existence **) 

1660  253 
section "?!"; 
923  254 

255 
qed_goalw "ex1I" HOL.thy [Ex1_def] 

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

259 

3003  260 
(*Sometimes easier to use: the premises have no shared variables. Safe!*) 
7030  261 
val [ex,eq] = Goal 
262 
"[ ? x. P(x); !!x y. [ P(x); P(y) ] ==> x=y ] ==> ?! x. P(x)"; 

263 
by (rtac (ex RS exE) 1); 

264 
by (REPEAT (ares_tac [ex1I,eq] 1)) ; 

265 
qed "ex_ex1I"; 

3003  266 

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

271 

5185  272 
Goal "?! x. P x ==> ? x. P x"; 
5228  273 
by (etac ex1E 1); 
274 
by (rtac exI 1); 

275 
by (assume_tac 1); 

5185  276 
qed "ex1_implies_ex"; 
277 

923  278 

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

1660  280 
section "@"; 
923  281 

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

7030  283 
val prems = Goal 
284 
"[ P a; !!x. P x ==> Q x ] ==> Q (@x. P x)"; 

285 
by (resolve_tac prems 1); 

286 
by (rtac selectI 1); 

287 
by (resolve_tac prems 1) ; 

288 
qed "selectI2"; 

923  289 

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

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

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

7030  295 
val prems = Goal 
296 
"[ P a; !!x. P x ==> x=a ] ==> (@x. P x) = a"; 

297 
by (rtac selectI2 1); 

298 
by (REPEAT (ares_tac prems 1)) ; 

299 
qed "select_equality"; 

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

300 

7030  301 
Goalw [Ex1_def] "[ ?!x. P x; P a ] ==> (@x. P x) = a"; 
302 
by (rtac select_equality 1); 

303 
by (atac 1); 

304 
by (etac exE 1); 

305 
by (etac conjE 1); 

306 
by (rtac allE 1); 

307 
by (atac 1); 

308 
by (etac impE 1); 

309 
by (atac 1); 

310 
by (etac ssubst 1); 

311 
by (etac allE 1); 

312 
by (etac mp 1); 

313 
by (atac 1); 

314 
qed "select1_equality"; 

1660  315 

7030  316 
Goal "P (@ x. P x) = (? x. P x)"; 
317 
by (rtac iffI 1); 

318 
by (etac exI 1); 

319 
by (etac exE 1); 

320 
by (etac selectI 1); 

321 
qed "select_eq_Ex"; 

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

322 

7030  323 
Goal "(@y. y=x) = x"; 
324 
by (rtac select_equality 1); 

325 
by (rtac refl 1); 

326 
by (atac 1); 

327 
qed "Eps_eq"; 

328 

329 
Goal "(Eps (op = x)) = x"; 

330 
by (rtac select_equality 1); 

331 
by (rtac refl 1); 

332 
by (etac sym 1); 

333 
qed "Eps_sym_eq"; 

923  334 

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

1660  336 
section "classical intro rules"; 
923  337 

7030  338 
val prems= Goal "(~Q ==> P) ==> PQ"; 
339 
by (rtac classical 1); 

340 
by (REPEAT (ares_tac (prems@[disjI1,notI]) 1)); 

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

342 
qed "disjCI"; 

923  343 

7030  344 
Goal "~P  P"; 
345 
by (REPEAT (ares_tac [disjCI] 1)) ; 

346 
qed "excluded_middle"; 

923  347 

348 
(*For disjunctive case analysis*) 

349 
fun excluded_middle_tac sP = 

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

351 

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

7030  353 
val major::prems = Goal "[ P>Q; ~P ==> R; Q ==> R ] ==> R"; 
354 
by (rtac (excluded_middle RS disjE) 1); 

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

356 
qed "impCE"; 

923  357 

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

360 
default: would break old proofs.*) 

7030  361 
val major::prems = Goal 
362 
"[ P>Q; Q ==> R; ~P ==> R ] ==> R"; 

363 
by (resolve_tac [excluded_middle RS disjE] 1); 

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

365 
qed "impCE'"; 

4302  366 

923  367 
(*Classical <> elimination. *) 
7030  368 
val major::prems = Goal 
369 
"[ P=Q; [ P; Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R"; 

370 
by (rtac (major RS iffE) 1); 

371 
by (REPEAT (DEPTH_SOLVE_1 

372 
(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))); 

373 
qed "iffCE"; 

923  374 

7030  375 
val prems = Goal "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"; 
376 
by (rtac ccontr 1); 

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

378 
qed "exCI"; 

923  379 

380 

381 
(* case distinction *) 

382 

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

5154  384 
(fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, 
923  385 
etac p2 1, etac p1 1]); 
386 

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

388 

1660  389 

923  390 
(** Standard abbreviations **) 
391 

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

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

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

394 
fun stac th = 
6968  395 
let val th' = th RS def_imp_eq handle THM _ => th 
5309
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5299
diff
changeset

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

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

398 

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

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

401 

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

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

403 

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

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

405 

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

407 
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

408 
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

409 
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

410 
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

411 

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

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

413 

1515  414 
fun RSspec th = 
415 
(case concl_of th of 

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

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

418 
in th RS forall_elim ca aspec end 

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

420 

421 
fun RSmp th = 

422 
(case concl_of th of 

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

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

425 

426 
fun normalize_thm funs = 

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

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

428 
 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

429 
in zero_var_indexes o trans funs end; 
1515  430 

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

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

432 
let val thm = normalize_thm [RSspec,RSmp] (result()) 
6214  433 
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

434 

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

435 
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

436 
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

437 

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

438 
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

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

3621  441 
end; 
5888  442 

443 

444 
(* attributes *) 

445 

446 
local 

447 

7030  448 
fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x; 
5888  449 

450 
in 

451 

6513  452 
val hol_setup = 
5888  453 
[Attrib.add_attributes 
454 
[("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]]; 

455 

456 
end; 