author  lcp 
Tue, 18 Jan 1994 15:57:40 +0100  
changeset 230  ec8a2b6aa8a7 
parent 68  d8f380764934 
child 253  d7130a753ecf 
permissions  rwrr 
39
deb04a336a99
"The error/exception above ...": errorneous goal now quoted;
wenzelm
parents:
0
diff
changeset

1 
(* Title: Pure/goals.ML 
0  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Goal stack package. The goal stack initially holds a dummy proof, and can 

7 
never become empty. Each goal stack consists of a list of levels. The 

8 
undo list is a list of goal stacks. Finally, there may be a stack of 

9 
pending proofs. 

10 
*) 

11 

12 

13 
signature GOALS = 

14 
sig 

15 
structure Tactical: TACTICAL 

16 
local open Tactical Tactical.Thm in 

17 
type proof 

18 
val ba: int > unit 

19 
val back: unit > unit 

20 
val bd: thm > int > unit 

21 
val bds: thm list > int > unit 

22 
val be: thm > int > unit 

23 
val bes: thm list > int > unit 

24 
val br: thm > int > unit 

25 
val brs: thm list > int > unit 

26 
val bw: thm > unit 

27 
val bws: thm list > unit 

28 
val by: tactic > unit 

29 
val byev: tactic list > unit 

30 
val chop: unit > unit 

31 
val choplev: int > unit 

32 
val fa: unit > unit 

33 
val fd: thm > unit 

34 
val fds: thm list > unit 

35 
val fe: thm > unit 

36 
val fes: thm list > unit 

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

38 
val fr: thm > unit 

39 
val frs: thm list > unit 

40 
val getgoal: int > term 

41 
val gethyps: int > thm list 

42 
val goal: theory > string > thm list 

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

230  44 
val goalw_cterm: thm list > cterm > thm list 
0  45 
val pop_proof: unit > thm list 
46 
val pr: unit > unit 

47 
val premises: unit > thm list 

48 
val prin: term > unit 

49 
val printyp: typ > unit 

50 
val pprint_term: term > pprint_args > unit 

51 
val pprint_typ: typ > pprint_args > unit 

52 
val print_exn: exn > 'a 

53 
val prlev: int > unit 

54 
val proof_timing: bool ref 

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

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

230  57 
val prove_goalw_cterm: thm list>cterm>(thm list>tactic list)>thm 
0  58 
val push_proof: unit > unit 
59 
val read: string > term 

60 
val ren: string > int > unit 

61 
val restore_proof: proof > thm list 

62 
val result: unit > thm 

63 
val rotate_proof: unit > thm list 

64 
val uresult: unit > thm 

65 
val save_proof: unit > proof 

66 
val topthm: unit > thm 

67 
val undo: unit > unit 

68 
end 

69 
end; 

70 

71 
functor GoalsFun (structure Logic: LOGIC and Drule: DRULE and Tactic: TACTIC 

72 
and Pattern:PATTERN 

73 
sharing type Pattern.type_sig = Drule.Thm.Sign.Type.type_sig 

74 
and Drule.Thm = Tactic.Tactical.Thm) : GOALS = 

75 
struct 

76 
structure Tactical = Tactic.Tactical 

77 
local open Tactic Tactic.Tactical Tactic.Tactical.Thm Drule 

78 
in 

79 

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

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

82 
type gstack = (thm * thm Sequence.seq) list; 

83 

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

85 

86 
(*** References ***) 

87 

88 
(*Should process time be printed after proof steps?*) 

89 
val proof_timing = ref false; 

90 

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

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

93 

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

95 
fun premises() = !curr_prems; 

96 

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

98 
val curr_mkresult = 

99 
ref((fn _=> error"No goal has been supplied in subgoal module") 

100 
: bool*thm>thm); 

101 

230  102 
val dummy = trivial(read_cterm Sign.pure 
0  103 
("PROP No_goal_has_been_supplied",propT)); 
104 

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

106 
A list of lists!*) 

107 
val undo_list = ref([[(dummy, Sequence.null)]] : gstack list); 

108 

109 
(* Stack of proof attempts *) 

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

111 

112 

113 
(*** Setting up goaldirected proof ***) 

114 

115 
(*Generates the list of new theories when the proof state's signature changes*) 

116 
fun sign_error (sign,sign') = 

117 
let val stamps = #stamps(Sign.rep_sg sign') \\ 

118 
#stamps(Sign.rep_sg sign) 

119 
in case stamps of 

120 
[stamp] => "\nNew theory: " ^ !stamp 

121 
 _ => "\nNew theories: " ^ space_implode ", " (map ! stamps) 

122 
end; 

123 

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

125 
Return assumptions, initial proof state, and function to make result. *) 

126 
fun prepare_proof rths chorn = 

230  127 
let val {sign, t=horn,...} = rep_cterm chorn; 
0  128 
val (_,As,B) = Logic.strip_horn(horn); 
230  129 
val cAs = map (cterm_of sign) As; 
0  130 
val p_rew = if null rths then I else rewrite_rule rths; 
131 
val c_rew = if null rths then I else rewrite_goals_rule rths; 

132 
val prems = map (p_rew o forall_elim_vars(0) o assume) cAs 

230  133 
and st0 = c_rew (trivial (cterm_of sign B)) 
0  134 
fun result_error state msg = 
135 
(writeln ("Bad final proof state:"); 

68
d8f380764934
goals/print_top,prepare_proof: now call \!print_goals_ref
lcp
parents:
39
diff
changeset

136 
!print_goals_ref (!goals_limit) state; 
0  137 
error msg) 
138 
(*discharges assumptions from state in the order they appear in goal; 

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

140 
fun mkresult (check,state) = 

141 
let val ngoals = nprems_of state 

142 
val th = implies_intr_list cAs state 

143 
val {hyps,prop,sign=sign',...} = rep_thm th 

144 
in if not check then standard th 

145 
else if not (eq_sg(sign,sign')) then result_error state 

146 
("Signature of proof state has changed!" ^ 

147 
sign_error (sign,sign')) 

148 
else if ngoals>0 then result_error state 

149 
(string_of_int ngoals ^ " unsolved goals!") 

150 
else if not (null hyps) then result_error state 

151 
("Additional hypotheses:\n" ^ 

152 
cat_lines (map (Sign.string_of_term sign) hyps)) 

153 
else if Pattern.eta_matches (#tsig(Sign.rep_sg sign)) 

230  154 
(term_of chorn, prop) 
0  155 
then standard th 
156 
else result_error state "proved a different theorem" 

157 
end 

158 
in 

159 
if eq_sg(sign, #sign(rep_thm st0)) 

160 
then (prems, st0, mkresult) 

161 
else error ("Definitions would change the proof state's signature" ^ 

162 
sign_error (sign, #sign(rep_thm st0))) 

163 
end 

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

165 

166 
(*Prints exceptions readably to users*) 

167 
fun print_sign_exn sign e = 

168 
case e of 

169 
THM (msg,i,thms) => 

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

171 
seq print_thm thms) 

172 
 THEORY (msg,thys) => 

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

174 
seq print_theory thys) 

175 
 TERM (msg,ts) => 

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

177 
seq (writeln o Sign.string_of_term sign) ts) 

178 
 TYPE (msg,Ts,ts) => 

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

180 
seq (writeln o Sign.string_of_typ sign) Ts; 

181 
seq (writeln o Sign.string_of_term sign) ts) 

182 
 e => raise e; 

183 

184 
(** the prove_goal.... commands 

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

186 
Augment signature with all type assignments of goal. 

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

188 

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

190 
fun prove_goalw_cterm rths chorn tacsf = 

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

192 
val tac = EVERY (tacsf prems) 

193 
fun statef() = 

194 
(case Sequence.pull (tapply(tac,st0)) of 

195 
Some(st,_) => st 

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

197 
in mkresult (true, cond_timeit (!proof_timing) statef) end; 

198 

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

200 
fun prove_goalw thy rths agoal tacsf = 

201 
let val sign = sign_of thy 

230  202 
val chorn = read_cterm sign (agoal,propT) 
0  203 
in prove_goalw_cterm rths chorn tacsf 
204 
handle ERROR => error (*from type_assign, etc via prepare_proof*) 

39
deb04a336a99
"The error/exception above ...": errorneous goal now quoted;
wenzelm
parents:
0
diff
changeset

205 
("The error above occurred for " ^ quote agoal) 
0  206 
 e => (print_sign_exn sign e; (*other exceptions*) 
39
deb04a336a99
"The error/exception above ...": errorneous goal now quoted;
wenzelm
parents:
0
diff
changeset

207 
error ("The exception above was raised for " ^ quote agoal)) 
0  208 
end; 
209 

210 
(*String version with no metarewriterules*) 

211 
fun prove_goal thy = prove_goalw thy []; 

212 

213 

214 
(*** Commands etc ***) 

215 

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

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

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

219 
 x::_ => x; 

220 

221 
(*Pops the given goal stack*) 

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

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

224 

225 

226 
(*Print a level of the goal stack.*) 

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

228 
(prs("Level " ^ string_of_int(length pairs) ^ "\n"); 

68
d8f380764934
goals/print_top,prepare_proof: now call \!print_goals_ref
lcp
parents:
39
diff
changeset

229 
!print_goals_ref (!goals_limit) th); 
0  230 

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

232 
Can do setstate[(st,Sequence.null)] to set st as the state. *) 

233 
fun setstate newgoals = 

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

235 

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

237 
the goal stack*) 

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

239 

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

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

242 

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

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

245 

246 
(*Return the final result. *) 

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

248 

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

250 
answer extraction, or other instantiation of Vars *) 

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

252 

253 
(*Get subgoal i from goal stack*) 

254 
fun getgoal i = 

255 
(case drop (i1, prems_of (topthm())) of 

256 
[] => error"getgoal: Goal number out of range" 

257 
 Q::_ => Q); 

258 

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

260 
For debugging uses of METAHYPS*) 

261 
local exception GETHYPS of thm list 

262 
in 

263 
fun gethyps i = 

264 
(tapply(METAHYPS (fn hyps => raise (GETHYPS hyps)) i, topthm()); []) 

265 
handle GETHYPS hyps => hyps 

266 
end; 

267 

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

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

270 

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

272 
fun chop_level n (pair,pairs) = 

273 
let val level = length pairs 

274 
in if 0<=n andalso n<= level 

275 
then drop (level  n, pair::pairs) 

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

277 
string_of_int level) 

278 
end; 

279 

280 
(*Print the given level of the proof*) 

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

282 
fun pr () = apply_fun print_top; 

283 

284 
(** the goal.... commands 

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

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

287 

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

230  289 
goalw_cterm rths (cterm_of (sign_of thy) t); *) 
0  290 
fun goalw_cterm rths chorn = 
291 
let val (prems, st0, mkresult) = prepare_proof rths chorn 

292 
in undo_list := []; 

293 
setstate [ (st0, Sequence.null) ]; 

294 
curr_prems := prems; 

295 
curr_mkresult := mkresult; 

296 
prems 

297 
end; 

298 

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

300 
fun goalw thy rths agoal = 

230  301 
goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT)) 
0  302 
handle ERROR => error (*from type_assign, etc via prepare_proof*) 
39
deb04a336a99
"The error/exception above ...": errorneous goal now quoted;
wenzelm
parents:
0
diff
changeset

303 
("The error above occurred for " ^ quote agoal); 
0  304 

305 
(*String version with no metarewriterules*) 

306 
fun goal thy = goalw thy []; 

307 

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

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

310 
(case Sequence.pull(tapply(tac, th)) of 

311 
None => error"by: tactic failed" 

312 
 Some(th2,ths2) => 

313 
(if eq_thm(th,th2) 

314 
then writeln"Warning: same as previous level" 

315 
else if eq_thm_sg(th,th2) then () 

316 
else writeln("Warning: signature of proof state has changed" ^ 

317 
sign_error (#sign(rep_thm th), #sign(rep_thm th2))); 

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

319 

320 
fun by tac = cond_timeit (!proof_timing) 

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

322 

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

324 
Good for debugging proofs involving prove_goal.*) 

325 
val byev = by o EVERY; 

326 

327 

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

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

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

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

332 
(case Sequence.pull thstr of 

333 
None => (writeln"Going back a level..."; backtrack pairs) 

334 
 Some(th2,thstr2) => 

335 
(if eq_thm(th,th2) 

336 
then writeln"Warning: same as previous choice at this level" 

337 
else if eq_thm_sg(th,th2) then () 

338 
else writeln"Warning: signature of proof state has changed"; 

339 
(th2,thstr2)::pairs)); 

340 

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

342 

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

344 
fun choplev n = make_command (chop_level n); 

345 

346 
(*Chopping back the goal stack*) 

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

348 

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

350 
fun undo() = case !undo_list of 

351 
[] => error"No proof state" 

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

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

354 

355 

356 
(*** Managing the proof stack ***) 

357 

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

359 

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

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

362 

363 

364 
fun top_proof() = case !proofstack of 

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

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

367 

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

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

370 

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

372 
fun pop_proof() = 

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

374 
val prems = restore_proof p 

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

376 

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

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

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

380 
restore_proof p; 

381 
pr(); 

382 
!curr_prems 

383 
end; 

384 

385 

386 
(** Shortcuts for commonlyused tactics **) 

387 

388 
fun bws rls = by (rewrite_goals_tac rls); 

389 
fun bw rl = bws [rl]; 

390 

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

392 
fun br rl = brs [rl]; 

393 

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

395 
fun be rl = bes [rl]; 

396 

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

398 
fun bd rl = bds [rl]; 

399 

400 
fun ba i = by (assume_tac i); 

401 

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

403 

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

405 

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

407 
fun fr rl = frs [rl]; 

408 

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

410 
fun fe rl = fes [rl]; 

411 

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

413 
fun fd rl = fds [rl]; 

414 

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

416 

417 
(** Reading and printing terms wrt the current theory **) 

418 

419 
fun top_sg() = #sign(rep_thm(topthm())); 

420 

230  421 
fun read s = term_of (read_cterm (top_sg()) 
0  422 
(s, (TVar(("DUMMY",0),[])))); 
423 

424 
(*Print a term under the current signature of the proof state*) 

425 
fun prin t = writeln (Sign.string_of_term (top_sg()) t); 

426 

427 
fun printyp T = writeln (Sign.string_of_typ (top_sg()) T); 

428 

429 
fun pprint_term t = Sign.pprint_term (top_sg()) t; 

430 

431 
fun pprint_typ T = Sign.pprint_typ (top_sg()) T; 

432 

433 
(*Prints exceptions nicely at top level; 

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

435 
fun print_exn e = (print_sign_exn (top_sg()) e; raise e); 

436 

437 
end; 

438 
end; 