author  wenzelm 
Mon, 04 Jun 2007 21:04:20 +0200  
changeset 23239  3648e97da60b 
parent 22826  0f4c501a691e 
child 23635  e31a814c080a 
permissions  rwrr 
18120  1 
(* Title: Pure/old_goals.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Oldstyle goal stack package. The goal stack initially holds a dummy 

7 
proof, and can never become empty. Each goal stack consists of a list 

8 
of levels. The undo list is a list of goal stacks. Finally, there 

9 
may be a stack of pending proofs. 

10 
*) 

11 

12 
signature GOALS = 

13 
sig 

14 
val premises: unit > thm list 

15 
val prove_goal: theory > string > (thm list > tactic list) > thm 

16 
val prove_goalw: theory > thm list > string > (thm list > tactic list) > thm 

17 
val disable_pr: unit > unit 

18 
val enable_pr: unit > unit 

19 
val topthm: unit > thm 

20 
val result: unit > thm 

21 
val uresult: unit > thm 

22 
val getgoal: int > term 

23 
val gethyps: int > thm list 

24 
val prlev: int > unit 

25 
val pr: unit > unit 

26 
val prlim: int > unit 

27 
val goal: theory > string > thm list 

28 
val goalw: theory > thm list > string > thm list 

29 
val Goal: string > thm list 

30 
val Goalw: thm list > string > thm list 

31 
val by: tactic > unit 

32 
val back: unit > unit 

33 
val choplev: int > unit 

34 
val undo: unit > unit 

35 
val bind_thm: string * thm > unit 

36 
val bind_thms: string * thm list > unit 

37 
val qed: string > unit 

38 
val qed_goal: string > theory > string > (thm list > tactic list) > unit 

39 
val qed_goalw: string > theory > thm list > string 

40 
> (thm list > tactic list) > unit 

41 
val qed_spec_mp: string > unit 

42 
val qed_goal_spec_mp: string > theory > string > (thm list > tactic list) > unit 

43 
val qed_goalw_spec_mp: string > theory > thm list > string 

44 
> (thm list > tactic list) > unit 

45 
val no_qed: unit > unit 

22109  46 
val inst: string > string > thm > thm 
18120  47 
end; 
48 

49 
signature OLD_GOALS = 

50 
sig 

51 
include GOALS 

52 
type proof 

19053  53 
val chop: unit > unit 
18120  54 
val reset_goals: unit > unit 
55 
val result_error_fn: (thm > string > thm) ref 

56 
val print_sign_exn: theory > exn > 'a 

57 
val prove_goalw_cterm: thm list>cterm>(thm list>tactic list)>thm 

58 
val prove_goalw_cterm_nocheck: thm list>cterm>(thm list>tactic list)>thm 

59 
val quick_and_dirty_prove_goalw_cterm: theory > thm list > cterm 

60 
> (thm list > tactic list) > thm 

61 
val print_exn: exn > 'a 

62 
val filter_goal: (term*term>bool) > thm list > int > thm list 

63 
val goalw_cterm: thm list > cterm > thm list 

64 
val simple_prove_goal_cterm: cterm>(thm list>tactic list)>thm 

65 
val byev: tactic list > unit 

66 
val save_proof: unit > proof 

67 
val restore_proof: proof > thm list 

68 
val push_proof: unit > unit 

69 
val pop_proof: unit > thm list 

70 
val rotate_proof: unit > thm list 

71 
val bws: thm list > unit 

72 
val bw: thm > unit 

73 
val brs: thm list > int > unit 

74 
val br: thm > int > unit 

75 
val bes: thm list > int > unit 

76 
val be: thm > int > unit 

77 
val bds: thm list > int > unit 

78 
val bd: thm > int > unit 

79 
val ba: int > unit 

80 
val ren: string > int > unit 

81 
val frs: thm list > unit 

82 
val fr: thm > unit 

83 
val fes: thm list > unit 

84 
val fe: thm > unit 

85 
val fds: thm list > unit 

86 
val fd: thm > unit 

87 
val fa: unit > unit 

88 
end; 

89 

90 
structure OldGoals: OLD_GOALS = 

91 
struct 

92 

93 
(*** Goal package ***) 

94 

95 
(*Each level of goal stack includes a proof state and alternative states, 

96 
the output of the tactic applied to the preceeding level. *) 

97 
type gstack = (thm * thm Seq.seq) list; 

98 

99 
datatype proof = Proof of gstack list * thm list * (bool*thm>thm); 

100 

101 

102 
(*** References ***) 

103 

104 
(*Current assumption list  set by "goal".*) 

105 
val curr_prems = ref([] : thm list); 

106 

107 
(*Return assumption list  useful if you didn't save "goal"'s result. *) 

108 
fun premises() = !curr_prems; 

109 

110 
(*Current result maker  set by "goal", used by "result". *) 

111 
fun init_mkresult _ = error "No goal has been supplied in subgoal module"; 

112 
val curr_mkresult = ref (init_mkresult: bool*thm>thm); 

113 

22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22360
diff
changeset

114 
val dummy = Thm.trivial (Thm.read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT)); 
18120  115 

116 
(*List of previous goal stacks, for the undo operation. Set by setstate. 

117 
A list of lists!*) 

118 
val undo_list = ref([[(dummy, Seq.empty)]] : gstack list); 

119 

120 
(* Stack of proof attempts *) 

121 
val proofstack = ref([]: proof list); 

122 

123 
(*reset all refs*) 

124 
fun reset_goals () = 

125 
(curr_prems := []; curr_mkresult := init_mkresult; 

126 
undo_list := [[(dummy, Seq.empty)]]); 

127 

128 

129 
(*** Setting up goaldirected proof ***) 

130 

131 
(*Generates the list of new theories when the proof state's theory changes*) 

132 
fun thy_error (thy,thy') = 

133 
let val names = Context.names_of thy' \\ Context.names_of thy 

134 
in case names of 

135 
[name] => "\nNew theory: " ^ name 

136 
 _ => "\nNew theories: " ^ space_implode ", " names 

137 
end; 

138 

139 
(*Default action is to print an error message; could be suppressed for 

140 
special applications.*) 

141 
fun result_error_default state msg : thm = 

142 
Pretty.str "Bad final proof state:" :: Display.pretty_goals (!goals_limit) state @ 

143 
[Pretty.str msg, Pretty.str "Proof failed!"] > Pretty.chunks > Pretty.string_of > error; 

144 

145 
val result_error_fn = ref result_error_default; 

146 

147 

148 
(*Common treatment of "goal" and "prove_goal": 

149 
Return assumptions, initial proof state, and function to make result. 

150 
"atomic" indicates if the goal should be wrapped up in the function 

151 
"Goal::prop=>prop" to avoid assumptions being returned separately. 

152 
*) 

153 
fun prepare_proof atomic rths chorn = 

154 
let 

22826  155 
val _ = legacy_feature "old goal command"; 
18120  156 
val {thy, t=horn,...} = rep_cterm chorn; 
157 
val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; 

158 
val (As, B) = Logic.strip_horn horn; 

159 
val atoms = atomic andalso 

23239  160 
forall (fn t => not (can Logic.dest_implies t orelse can Logic.dest_all t)) As; 
18120  161 
val (As,B) = if atoms then ([],horn) else (As,B); 
162 
val cAs = map (cterm_of thy) As; 

163 
val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs; 

164 
val cB = cterm_of thy B; 

165 
val st0 = let val st = Goal.init cB > fold Thm.weaken cAs 

166 
in rewrite_goals_rule rths st end 

167 
(*discharges assumptions from state in the order they appear in goal; 

168 
checks (if requested) that resulting theorem is equivalent to goal. *) 

169 
fun mkresult (check,state) = 

170 
let val state = Seq.hd (flexflex_rule state) 

171 
handle THM _ => state (*smash flexflex pairs*) 

172 
val ngoals = nprems_of state 

173 
val ath = implies_intr_list cAs state 

174 
val th = Goal.conclude ath 

175 
val {hyps,prop,thy=thy',...} = rep_thm th 

176 
val final_th = standard th 

177 
in if not check then final_th 

178 
else if not (eq_thy(thy,thy')) then !result_error_fn state 

179 
("Theory of proof state has changed!" ^ 

180 
thy_error (thy,thy')) 

181 
else if ngoals>0 then !result_error_fn state 

182 
(string_of_int ngoals ^ " unsolved goals!") 

183 
else if not (null hyps) then !result_error_fn state 

184 
("Additional hypotheses:\n" ^ 

185 
cat_lines (map (Sign.string_of_term thy) hyps)) 

186 
else if Pattern.matches thy 

187 
(Envir.beta_norm (term_of chorn), Envir.beta_norm prop) 

188 
then final_th 

189 
else !result_error_fn state "proved a different theorem" 

190 
end 

191 
in 

192 
if eq_thy(thy, Thm.theory_of_thm st0) 

193 
then (prems, st0, mkresult) 

194 
else error ("Definitions would change the proof state's theory" ^ 

195 
thy_error (thy, Thm.theory_of_thm st0)) 

196 
end 

197 
handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s); 

198 

199 
(*Prints exceptions readably to users*) 

200 
fun print_sign_exn_unit thy e = 

201 
case e of 

202 
THM (msg,i,thms) => 

203 
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); 

204 
List.app print_thm thms) 

205 
 THEORY (msg,thys) => 

206 
(writeln ("Exception THEORY raised:\n" ^ msg); 

207 
List.app (writeln o Context.str_of_thy) thys) 

208 
 TERM (msg,ts) => 

209 
(writeln ("Exception TERM raised:\n" ^ msg); 

210 
List.app (writeln o Sign.string_of_term thy) ts) 

211 
 TYPE (msg,Ts,ts) => 

212 
(writeln ("Exception TYPE raised:\n" ^ msg); 

213 
List.app (writeln o Sign.string_of_typ thy) Ts; 

214 
List.app (writeln o Sign.string_of_term thy) ts) 

215 
 e => raise e; 

216 

217 
(*Prints an exception, then fails*) 

18678  218 
fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR ""); 
18120  219 

220 
(** the prove_goal.... commands 

221 
Prove theorem using the listed tactics; check it has the specified form. 

222 
Augment theory with all type assignments of goal. 

223 
Syntax is similar to "goal" command for easy keyboard use. **) 

224 

225 
(*Version taking the goal as a cterm*) 

226 
fun prove_goalw_cterm_general check rths chorn tacsf = 

227 
let val (prems, st0, mkresult) = prepare_proof false rths chorn 

228 
val tac = EVERY (tacsf prems) 

229 
fun statef() = 

230 
(case Seq.pull (tac st0) of 

231 
SOME(st,_) => st 

232 
 _ => error ("prove_goal: tactic failed")) 

233 
in mkresult (check, cond_timeit (!Output.timing) statef) end 

234 
handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e; 

235 
writeln ("The exception above was raised for\n" ^ 

236 
Display.string_of_cterm chorn); raise e); 

237 

238 
(*Two variants: one checking the result, one not. 

239 
Neither prints runtime messages: they are for internal packages.*) 

240 
fun prove_goalw_cterm rths chorn = 

241 
setmp Output.timing false (prove_goalw_cterm_general true rths chorn) 

242 
and prove_goalw_cterm_nocheck rths chorn = 

243 
setmp Output.timing false (prove_goalw_cterm_general false rths chorn); 

244 

245 

246 
(*Version taking the goal as a string*) 

247 
fun prove_goalw thy rths agoal tacsf = 

22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22360
diff
changeset

248 
let val chorn = Thm.read_cterm thy (agoal, propT) 
18120  249 
in prove_goalw_cterm_general true rths chorn tacsf end 
18678  250 
handle ERROR msg => cat_error msg (*from read_cterm?*) 
18120  251 
("The error(s) above occurred for " ^ quote agoal); 
252 

253 
(*String version with no metarewriterules*) 

254 
fun prove_goal thy = prove_goalw thy []; 

255 

256 
(*quick and dirty version (conditional)*) 

257 
fun quick_and_dirty_prove_goalw_cterm thy rews ct tacs = 

258 
prove_goalw_cterm rews ct 

259 
(if ! quick_and_dirty then (K [SkipProof.cheat_tac thy]) else tacs); 

260 

261 

262 
(*** Commands etc ***) 

263 

264 
(*Return the current goal stack, if any, from undo_list*) 

265 
fun getstate() : gstack = case !undo_list of 

266 
[] => error"No current state in subgoal module" 

267 
 x::_ => x; 

268 

269 
(*Pops the given goal stack*) 

270 
fun pop [] = error"Cannot go back past the beginning of the proof!" 

271 
 pop (pair::pairs) = (pair,pairs); 

272 

273 

274 
(* Print a level of the goal stack  subject to quiet mode *) 

275 

276 
val quiet = ref false; 

277 
fun disable_pr () = quiet := true; 

278 
fun enable_pr () = quiet := false; 

279 

280 
fun print_top ((th, _), pairs) = 

281 
if ! quiet then () 

282 
else ! Display.print_current_goals_fn (length pairs) (! goals_limit) th; 

283 

284 
(*Printing can raise exceptions, so the assignment occurs last. 

285 
Can do setstate[(st,Seq.empty)] to set st as the state. *) 

286 
fun setstate newgoals = 

287 
(print_top (pop newgoals); undo_list := newgoals :: !undo_list); 

288 

289 
(*Given a proof state transformation, return a command that updates 

290 
the goal stack*) 

291 
fun make_command com = setstate (com (pop (getstate()))); 

292 

293 
(*Apply a function on proof states to the current goal stack*) 

294 
fun apply_fun f = f (pop(getstate())); 

295 

296 
(*Return the top theorem, representing the proof state*) 

297 
fun topthm () = apply_fun (fn ((th,_), _) => th); 

298 

299 
(*Return the final result. *) 

300 
fun result () = !curr_mkresult (true, topthm()); 

301 

302 
(*Return the result UNCHECKED that it equals the goal  for synthesis, 

303 
answer extraction, or other instantiation of Vars *) 

304 
fun uresult () = !curr_mkresult (false, topthm()); 

305 

306 
(*Get subgoal i from goal stack*) 

307 
fun getgoal i = Logic.get_goal (prop_of (topthm())) i; 

308 

309 
(*Return subgoal i's hypotheses as metalevel assumptions. 

310 
For debugging uses of METAHYPS*) 

311 
local exception GETHYPS of thm list 

312 
in 

313 
fun gethyps i = 

314 
(METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); []) 

315 
handle GETHYPS hyps => hyps 

316 
end; 

317 

318 
(*Prints exceptions nicely at top level; 

319 
raises the exception in order to have a polymorphic type!*) 

320 
fun print_exn e = (print_sign_exn_unit (Thm.theory_of_thm (topthm())) e; raise e); 

321 

322 
(*Which thms could apply to goal i? (debugs tactics involving filter_thms) *) 

323 
fun filter_goal could ths i = filter_thms could (999, getgoal i, ths); 

324 

325 
(*For inspecting earlier levels of the backward proof*) 

326 
fun chop_level n (pair,pairs) = 

327 
let val level = length pairs 

328 
in if n<0 andalso ~n <= level 

329 
then List.drop (pair::pairs, ~n) 

330 
else if 0<=n andalso n<= level 

331 
then List.drop (pair::pairs, level  n) 

332 
else error ("Level number must lie between 0 and " ^ 

333 
string_of_int level) 

334 
end; 

335 

336 
(*Print the given level of the proof; prlev ~1 prints previous level*) 

337 
fun prlev n = (enable_pr (); apply_fun (print_top o pop o (chop_level n))); 

338 
fun pr () = (enable_pr (); apply_fun print_top); 

339 

340 
(*Set goals_limit and print again*) 

341 
fun prlim n = (goals_limit:=n; pr()); 

342 

343 
(** the goal.... commands 

344 
Read main goal. Set global variables curr_prems, curr_mkresult. 

345 
Initial subgoal and premises are rewritten using rths. **) 

346 

347 
(*Version taking the goal as a cterm; if you have a term t and theory thy, use 

348 
goalw_cterm rths (cterm_of thy t); *) 

349 
fun agoalw_cterm atomic rths chorn = 

350 
let val (prems, st0, mkresult) = prepare_proof atomic rths chorn 

351 
in undo_list := []; 

352 
setstate [ (st0, Seq.empty) ]; 

353 
curr_prems := prems; 

354 
curr_mkresult := mkresult; 

355 
prems 

356 
end; 

357 

358 
val goalw_cterm = agoalw_cterm false; 

359 

360 
(*Version taking the goal as a string*) 

361 
fun agoalw atomic thy rths agoal = 

22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22360
diff
changeset

362 
agoalw_cterm atomic rths (Thm.read_cterm thy (agoal, propT)) 
18678  363 
handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*) 
18120  364 
("The error(s) above occurred for " ^ quote agoal); 
365 

366 
val goalw = agoalw false; 

367 
fun goal thy = goalw thy []; 

368 

369 
(*now the versions that wrap the goal up in `Goal' to make it atomic*) 

22109  370 
fun Goalw thms s = agoalw true (ML_Context.the_context ()) thms s; 
18120  371 
val Goal = Goalw []; 
372 

373 
(*simple version with minimal amount of checking and postprocessing*) 

374 
fun simple_prove_goal_cterm G f = 

375 
let 

22826  376 
val _ = legacy_feature "old goal command"; 
18120  377 
val As = Drule.strip_imp_prems G; 
378 
val B = Drule.strip_imp_concl G; 

20229  379 
val asms = map Assumption.assume As; 
18120  380 
fun check NONE = error "prove_goal: tactic failed" 
381 
 check (SOME (thm, _)) = (case nprems_of thm of 

382 
0 => thm 

383 
 i => !result_error_fn thm (string_of_int i ^ " unsolved goals!")) 

384 
in 

385 
standard (implies_intr_list As 

386 
(check (Seq.pull (EVERY (f asms) (trivial B))))) 

387 
end; 

388 

389 

390 
(*Proof step "by" the given tactic  apply tactic to the proof state*) 

391 
fun by_com tac ((th,ths), pairs) : gstack = 

392 
(case Seq.pull(tac th) of 

393 
NONE => error"by: tactic failed" 

394 
 SOME(th2,ths2) => 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22109
diff
changeset

395 
(if Thm.eq_thm(th,th2) 
18120  396 
then warning "Warning: same as previous level" 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22109
diff
changeset

397 
else if Thm.eq_thm_thy(th,th2) then () 
18120  398 
else warning ("Warning: theory of proof state has changed" ^ 
399 
thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2)); 

400 
((th2,ths2)::(th,ths)::pairs))); 

401 

402 
fun by tac = cond_timeit (!Output.timing) 

403 
(fn() => make_command (by_com tac)); 

404 

405 
(* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn. 

406 
Good for debugging proofs involving prove_goal.*) 

407 
val byev = by o EVERY; 

408 

409 

410 
(*Backtracking means find an alternative result from a tactic. 

411 
If none at this level, try earlier levels*) 

412 
fun backtrack [] = error"back: no alternatives" 

413 
 backtrack ((th,thstr) :: pairs) = 

414 
(case Seq.pull thstr of 

415 
NONE => (writeln"Going back a level..."; backtrack pairs) 

416 
 SOME(th2,thstr2) => 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22109
diff
changeset

417 
(if Thm.eq_thm(th,th2) 
18120  418 
then warning "Warning: same as previous choice at this level" 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22109
diff
changeset

419 
else if Thm.eq_thm_thy(th,th2) then () 
18120  420 
else warning "Warning: theory of proof state has changed"; 
421 
(th2,thstr2)::pairs)); 

422 

423 
fun back() = setstate (backtrack (getstate())); 

424 

425 
(*Chop back to previous level of the proof*) 

426 
fun choplev n = make_command (chop_level n); 

427 

428 
(*Chopping back the goal stack*) 

429 
fun chop () = make_command (fn (_,pairs) => pairs); 

430 

431 
(*Restore the previous proof state; discard current state. *) 

432 
fun undo() = case !undo_list of 

433 
[] => error"No proof state" 

434 
 [_] => error"Already at initial state" 

435 
 _::newundo => (undo_list := newundo; pr()) ; 

436 

437 

438 
(*** Managing the proof stack ***) 

439 

440 
fun save_proof() = Proof(!undo_list, !curr_prems, !curr_mkresult); 

441 

442 
fun restore_proof(Proof(ul,prems,mk)) = 

443 
(undo_list:= ul; curr_prems:= prems; curr_mkresult := mk; prems); 

444 

445 

446 
fun top_proof() = case !proofstack of 

447 
[] => error("Stack of proof attempts is empty!") 

448 
 p::ps => (p,ps); 

449 

450 
(* push a copy of the current proof state on to the stack *) 

451 
fun push_proof() = (proofstack := (save_proof() :: !proofstack)); 

452 

453 
(* discard the top proof state of the stack *) 

454 
fun pop_proof() = 

455 
let val (p,ps) = top_proof() 

456 
val prems = restore_proof p 

457 
in proofstack := ps; pr(); prems end; 

458 

459 
(* rotate the stack so that the top element goes to the bottom *) 

460 
fun rotate_proof() = let val (p,ps) = top_proof() 

461 
in proofstack := ps@[save_proof()]; 

462 
restore_proof p; 

463 
pr(); 

464 
!curr_prems 

465 
end; 

466 

467 

468 
(** Shortcuts for commonlyused tactics **) 

469 

470 
fun bws rls = by (rewrite_goals_tac rls); 

471 
fun bw rl = bws [rl]; 

472 

473 
fun brs rls i = by (resolve_tac rls i); 

474 
fun br rl = brs [rl]; 

475 

476 
fun bes rls i = by (eresolve_tac rls i); 

477 
fun be rl = bes [rl]; 

478 

479 
fun bds rls i = by (dresolve_tac rls i); 

480 
fun bd rl = bds [rl]; 

481 

482 
fun ba i = by (assume_tac i); 

483 

484 
fun ren str i = by (rename_tac str i); 

485 

486 
(** Shortcuts to work on the first applicable subgoal **) 

487 

488 
fun frs rls = by (FIRSTGOAL (trace_goalno_tac (resolve_tac rls))); 

489 
fun fr rl = frs [rl]; 

490 

491 
fun fes rls = by (FIRSTGOAL (trace_goalno_tac (eresolve_tac rls))); 

492 
fun fe rl = fes [rl]; 

493 

494 
fun fds rls = by (FIRSTGOAL (trace_goalno_tac (dresolve_tac rls))); 

495 
fun fd rl = fds [rl]; 

496 

497 
fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac)); 

498 

499 

19053  500 
(** theorem database **) 
18120  501 

502 
fun bind_thm (name, thm) = ThmDatabase.ml_store_thm (name, standard thm); 

503 
fun bind_thms (name, thms) = ThmDatabase.ml_store_thms (name, map standard thms); 

504 

505 
fun qed name = ThmDatabase.ml_store_thm (name, result ()); 

506 
fun qed_goal name thy goal tacsf = ThmDatabase.ml_store_thm (name, prove_goal thy goal tacsf); 

507 
fun qed_goalw name thy rews goal tacsf = 

508 
ThmDatabase.ml_store_thm (name, prove_goalw thy rews goal tacsf); 

509 
fun qed_spec_mp name = 

510 
ThmDatabase.ml_store_thm (name, ObjectLogic.rulify_no_asm (result ())); 

511 
fun qed_goal_spec_mp name thy s p = 

512 
bind_thm (name, ObjectLogic.rulify_no_asm (prove_goal thy s p)); 

513 
fun qed_goalw_spec_mp name thy defs s p = 

514 
bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p)); 

515 

516 
fun no_qed () = (); 

517 

22109  518 
(*shorthand for instantiating just one variable in the current theory*) 
519 
fun inst x t = read_instantiate_sg (the_context()) [(x,t)]; 

520 

18120  521 
end; 
522 

523 
structure Goals: GOALS = OldGoals; 

524 
open Goals; 