author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 23635  e31a814c080a 
child 25685  c36e10812ae4 
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 topthm: unit > thm 

18 
val result: unit > thm 

19 
val uresult: unit > thm 

20 
val getgoal: int > term 

21 
val gethyps: int > thm list 

22 
val prlev: int > unit 

23 
val pr: unit > unit 

24 
val prlim: int > unit 

25 
val goal: theory > string > thm list 

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

27 
val Goal: string > thm list 

28 
val Goalw: thm list > string > thm list 

29 
val by: tactic > unit 

30 
val back: unit > unit 

31 
val choplev: int > unit 

32 
val undo: unit > unit 

33 
val bind_thm: string * thm > unit 

34 
val bind_thms: string * thm list > unit 

35 
val qed: string > unit 

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

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

38 
> (thm list > tactic list) > unit 

39 
val qed_spec_mp: string > unit 

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

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

42 
> (thm list > tactic list) > unit 

43 
val no_qed: unit > unit 

22109  44 
val inst: string > string > thm > thm 
18120  45 
end; 
46 

47 
signature OLD_GOALS = 

48 
sig 

49 
include GOALS 

50 
type proof 

19053  51 
val chop: unit > unit 
18120  52 
val reset_goals: unit > unit 
53 
val result_error_fn: (thm > string > thm) ref 

54 
val print_sign_exn: theory > exn > 'a 

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

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

57 
val quick_and_dirty_prove_goalw_cterm: theory > thm list > cterm 

58 
> (thm list > tactic list) > thm 

59 
val print_exn: exn > 'a 

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

61 
val goalw_cterm: thm list > cterm > thm list 

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

63 
val byev: tactic list > unit 

64 
val save_proof: unit > proof 

65 
val restore_proof: proof > thm list 

66 
val push_proof: unit > unit 

67 
val pop_proof: unit > thm list 

68 
val rotate_proof: unit > thm list 

69 
val bws: thm list > unit 

70 
val bw: thm > unit 

71 
val brs: thm list > int > unit 

72 
val br: thm > int > unit 

73 
val bes: thm list > int > unit 

74 
val be: thm > int > unit 

75 
val bds: thm list > int > unit 

76 
val bd: thm > int > unit 

77 
val ba: int > unit 

78 
val ren: string > int > unit 

79 
val frs: thm list > unit 

80 
val fr: thm > unit 

81 
val fes: thm list > unit 

82 
val fe: thm > unit 

83 
val fds: thm list > unit 

84 
val fd: thm > unit 

85 
val fa: unit > unit 

86 
end; 

87 

88 
structure OldGoals: OLD_GOALS = 

89 
struct 

90 

91 
(*** Goal package ***) 

92 

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

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

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

96 

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

98 

99 

100 
(*** References ***) 

101 

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

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

104 

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

106 
fun premises() = !curr_prems; 

107 

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

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

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

111 

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

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

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

115 
A list of lists!*) 

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

117 

118 
(* Stack of proof attempts *) 

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

120 

121 
(*reset all refs*) 

122 
fun reset_goals () = 

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

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

125 

126 

127 
(*** Setting up goaldirected proof ***) 

128 

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

130 
fun thy_error (thy,thy') = 

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

132 
in case names of 

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

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

135 
end; 

136 

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

138 
special applications.*) 

139 
fun result_error_default state msg : thm = 

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

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

142 

143 
val result_error_fn = ref result_error_default; 

144 

145 

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

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

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

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

150 
*) 

151 
fun prepare_proof atomic rths chorn = 

152 
let 

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

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

157 
val atoms = atomic andalso 

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

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

162 
val cB = cterm_of thy B; 

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

164 
in rewrite_goals_rule rths st end 

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

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

167 
fun mkresult (check,state) = 

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

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

170 
val ngoals = nprems_of state 

171 
val ath = implies_intr_list cAs state 

172 
val th = Goal.conclude ath 

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

174 
val final_th = standard th 

175 
in if not check then final_th 

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

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

178 
thy_error (thy,thy')) 

179 
else if ngoals>0 then !result_error_fn state 

180 
(string_of_int ngoals ^ " unsolved goals!") 

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

182 
("Additional hypotheses:\n" ^ 

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

184 
else if Pattern.matches thy 

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

186 
then final_th 

187 
else !result_error_fn state "proved a different theorem" 

188 
end 

189 
in 

190 
if eq_thy(thy, Thm.theory_of_thm st0) 

191 
then (prems, st0, mkresult) 

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

193 
thy_error (thy, Thm.theory_of_thm st0)) 

194 
end 

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

196 

197 
(*Prints exceptions readably to users*) 

198 
fun print_sign_exn_unit thy e = 

199 
case e of 

200 
THM (msg,i,thms) => 

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

202 
List.app print_thm thms) 

203 
 THEORY (msg,thys) => 

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

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

206 
 TERM (msg,ts) => 

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

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

209 
 TYPE (msg,Ts,ts) => 

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

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

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

213 
 e => raise e; 

214 

215 
(*Prints an exception, then fails*) 

18678  216 
fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR ""); 
18120  217 

218 
(** the prove_goal.... commands 

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

220 
Augment theory with all type assignments of goal. 

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

222 

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

224 
fun prove_goalw_cterm_general check rths chorn tacsf = 

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

226 
val tac = EVERY (tacsf prems) 

227 
fun statef() = 

228 
(case Seq.pull (tac st0) of 

229 
SOME(st,_) => st 

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

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

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

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

234 
Display.string_of_cterm chorn); raise e); 

235 

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

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

238 
fun prove_goalw_cterm rths chorn = 

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

240 
and prove_goalw_cterm_nocheck rths chorn = 

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

242 

243 

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

245 
fun prove_goalw thy rths agoal tacsf = 

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

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

251 
(*String version with no metarewriterules*) 

252 
fun prove_goal thy = prove_goalw thy []; 

253 

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

255 
fun quick_and_dirty_prove_goalw_cterm thy rews ct tacs = 

256 
prove_goalw_cterm rews ct 

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

258 

259 

260 
(*** Commands etc ***) 

261 

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

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

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

265 
 x::_ => x; 

266 

267 
(*Pops the given goal stack*) 

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

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

270 

271 

23635  272 
(* Print a level of the goal stack *) 
18120  273 

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

23635  275 
let 
276 
val n = length pairs; 

277 
val m = (! goals_limit); 

278 
val ngoals = nprems_of th; 

279 
in 

280 
[Pretty.str ("Level " ^ string_of_int n ^ 

281 
(if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ 

282 
(if ngoals <> 1 then "s" else "") ^ ")" 

283 
else ""))] @ 

284 
Display.pretty_goals m th 

285 
end > Pretty.chunks > Pretty.writeln; 

18120  286 

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

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

289 
fun setstate newgoals = 

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

291 

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

293 
the goal stack*) 

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

295 

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

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

298 

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

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

301 

302 
(*Return the final result. *) 

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

304 

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

306 
answer extraction, or other instantiation of Vars *) 

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

308 

309 
(*Get subgoal i from goal stack*) 

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

311 

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

313 
For debugging uses of METAHYPS*) 

314 
local exception GETHYPS of thm list 

315 
in 

316 
fun gethyps i = 

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

318 
handle GETHYPS hyps => hyps 

319 
end; 

320 

321 
(*Prints exceptions nicely at top level; 

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

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

324 

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

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

327 

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

329 
fun chop_level n (pair,pairs) = 

330 
let val level = length pairs 

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

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

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

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

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

336 
string_of_int level) 

337 
end; 

338 

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

23635  340 
fun prlev n = apply_fun (print_top o pop o (chop_level n)); 
341 
fun pr () = apply_fun print_top; 

18120  342 

343 
(*Set goals_limit and print again*) 

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

345 

346 
(** the goal.... commands 

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

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

349 

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

351 
goalw_cterm rths (cterm_of thy t); *) 

352 
fun agoalw_cterm atomic rths chorn = 

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

354 
in undo_list := []; 

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

356 
curr_prems := prems; 

357 
curr_mkresult := mkresult; 

358 
prems 

359 
end; 

360 

361 
val goalw_cterm = agoalw_cterm false; 

362 

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

364 
fun agoalw atomic thy rths agoal = 

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

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

369 
val goalw = agoalw false; 

370 
fun goal thy = goalw thy []; 

371 

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

22109  373 
fun Goalw thms s = agoalw true (ML_Context.the_context ()) thms s; 
18120  374 
val Goal = Goalw []; 
375 

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

377 
fun simple_prove_goal_cterm G f = 

378 
let 

22826  379 
val _ = legacy_feature "old goal command"; 
18120  380 
val As = Drule.strip_imp_prems G; 
381 
val B = Drule.strip_imp_concl G; 

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

385 
0 => thm 

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

387 
in 

388 
standard (implies_intr_list As 

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

390 
end; 

391 

392 

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

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

395 
(case Seq.pull(tac th) of 

396 
NONE => error"by: tactic failed" 

397 
 SOME(th2,ths2) => 

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

398 
(if Thm.eq_thm(th,th2) 
18120  399 
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

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

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

404 

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

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

407 

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

409 
Good for debugging proofs involving prove_goal.*) 

410 
val byev = by o EVERY; 

411 

412 

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

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

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

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

417 
(case Seq.pull thstr of 

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

419 
 SOME(th2,thstr2) => 

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

420 
(if Thm.eq_thm(th,th2) 
18120  421 
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

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

425 

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

427 

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

429 
fun choplev n = make_command (chop_level n); 

430 

431 
(*Chopping back the goal stack*) 

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

433 

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

435 
fun undo() = case !undo_list of 

436 
[] => error"No proof state" 

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

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

439 

440 

441 
(*** Managing the proof stack ***) 

442 

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

444 

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

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

447 

448 

449 
fun top_proof() = case !proofstack of 

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

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

452 

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

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

455 

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

457 
fun pop_proof() = 

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

459 
val prems = restore_proof p 

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

461 

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

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

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

465 
restore_proof p; 

466 
pr(); 

467 
!curr_prems 

468 
end; 

469 

470 

471 
(** Shortcuts for commonlyused tactics **) 

472 

473 
fun bws rls = by (rewrite_goals_tac rls); 

474 
fun bw rl = bws [rl]; 

475 

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

477 
fun br rl = brs [rl]; 

478 

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

480 
fun be rl = bes [rl]; 

481 

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

483 
fun bd rl = bds [rl]; 

484 

485 
fun ba i = by (assume_tac i); 

486 

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

488 

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

490 

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

492 
fun fr rl = frs [rl]; 

493 

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

495 
fun fe rl = fes [rl]; 

496 

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

498 
fun fd rl = fds [rl]; 

499 

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

501 

502 

19053  503 
(** theorem database **) 
18120  504 

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

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

507 

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

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

510 
fun qed_goalw name thy rews goal tacsf = 

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

512 
fun qed_spec_mp name = 

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

514 
fun qed_goal_spec_mp name thy s p = 

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

516 
fun qed_goalw_spec_mp name thy defs s p = 

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

518 

519 
fun no_qed () = (); 

520 

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

523 

18120  524 
end; 
525 

526 
structure Goals: GOALS = OldGoals; 

527 
open Goals; 