author  paulson 
Fri, 04 Dec 1998 10:45:20 +0100  
changeset 6017  dbb33359a7ab 
parent 5955  6727d29d164f 
child 6133  4f224fd882f9 
permissions  rwrr 
1460  1 
(* Title: Pure/goals.ML 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  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 
signature GOALS = 

13 
sig 

14 
type proof 

5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

15 
val atomic_goal : theory > string > thm list 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

16 
val atomic_goalw : theory > thm list > string > thm list 
1460  17 
val ba : int > unit 
18 
val back : unit > unit 

19 
val bd : thm > int > unit 

20 
val bds : thm list > int > unit 

21 
val be : thm > int > unit 

22 
val bes : thm list > int > unit 

23 
val br : thm > int > unit 

24 
val brs : thm list > int > unit 

25 
val bw : thm > unit 

26 
val bws : thm list > unit 

27 
val by : tactic > unit 

28 
val byev : tactic list > unit 

29 
val chop : unit > unit 

30 
val choplev : int > unit 

6017  31 
val export_thy : theory > thm > thm 
5246  32 
val export : thm > thm 
1460  33 
val fa : unit > unit 
34 
val fd : thm > unit 

35 
val fds : thm list > unit 

36 
val fe : thm > unit 

37 
val fes : thm list > unit 

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

39 
val fr : thm > unit 

40 
val frs : thm list > unit 

41 
val getgoal : int > term 

42 
val gethyps : int > thm list 

43 
val goal : theory > string > thm list 

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

45 
val goalw_cterm : thm list > cterm > thm list 

5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset

46 
val current_goals_markers: (string * string * string) ref 
5246  47 
val print_current_goals_default: (int > int > thm > unit) 
3532  48 
val print_current_goals_fn : (int > int > thm > unit) ref 
1460  49 
val pop_proof : unit > thm list 
50 
val pr : unit > unit 

2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

51 
val prlev : int > unit 
2514  52 
val prlim : int > unit 
1460  53 
val premises : unit > thm list 
54 
val prin : term > unit 

55 
val printyp : typ > unit 

56 
val pprint_term : term > pprint_args > unit 

57 
val pprint_typ : typ > pprint_args > unit 

58 
val print_exn : exn > 'a 

59 
val print_sign_exn : Sign.sg > exn > 'a 

60 
val proof_timing : bool ref 

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

577  62 
val prove_goalw : theory>thm list>string>(thm list>tactic list)>thm 
1460  63 
val prove_goalw_cterm : thm list>cterm>(thm list>tactic list)>thm 
5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset

64 
val prove_goalw_cterm_nocheck : thm list>cterm>(thm list>tactic list)>thm 
1460  65 
val push_proof : unit > unit 
66 
val read : string > term 

67 
val ren : string > int > unit 

68 
val restore_proof : proof > thm list 

69 
val result : unit > thm 

3532  70 
val result_error_fn : (thm > string > thm) ref 
1460  71 
val rotate_proof : unit > thm list 
72 
val uresult : unit > thm 

73 
val save_proof : unit > proof 

74 
val topthm : unit > thm 

75 
val undo : unit > unit 

0  76 
end; 
77 

1500  78 
structure Goals : GOALS = 
0  79 
struct 
80 

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

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

4270  83 
type gstack = (thm * thm Seq.seq) list; 
0  84 

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

86 

5246  87 

0  88 
(*** References ***) 
89 

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

91 
val proof_timing = ref false; 

92 

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

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

95 

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

97 
fun premises() = !curr_prems; 

98 

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

100 
val curr_mkresult = 

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

102 
: bool*thm>thm); 

103 

5092  104 
val dummy = trivial(read_cterm (sign_of ProtoPure.thy) 
0  105 
("PROP No_goal_has_been_supplied",propT)); 
106 

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

108 
A list of lists!*) 

4270  109 
val undo_list = ref([[(dummy, Seq.empty)]] : gstack list); 
0  110 

111 
(* Stack of proof attempts *) 

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

113 

114 

115 
(*** Setting up goaldirected proof ***) 

116 

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

118 
fun sign_error (sign,sign') = 

3974  119 
let val names = Sign.stamp_names_of sign' \\ Sign.stamp_names_of sign 
120 
in case names of 

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

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

0  123 
end; 
124 

1928  125 
(*Default action is to print an error message; could be suppressed for 
126 
special applications.*) 

3669
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset

127 
fun result_error_default state msg : thm = 
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset

128 
(writeln "Bad final proof state:"; 
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset

129 
print_goals (!goals_limit) state; 
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset

130 
writeln msg; raise ERROR); 
1928  131 

3532  132 
val result_error_fn = ref result_error_default; 
1928  133 

5246  134 
(* alternative to standard: this function does not discharge the hypotheses 
135 
first. Is used for locales, in the following function prepare_proof *) 

136 
fun varify th = 

137 
let val {maxidx,...} = rep_thm th 

138 
in 

139 
th > forall_intr_frees > forall_elim_vars (maxidx + 1) 

140 
> Thm.strip_shyps > Thm.implies_intr_shyps 

141 
> zero_var_indexes > Thm.varifyT > Thm.compress 

142 
end; 

143 

144 
(** exporting a theorem out of a locale means turning all metahyps into assumptions 

6017  145 
and expand and cancel the locale definitions. 
146 
export goes through all levels in case of nested locales, whereas 

147 
export_thy just goes one up. (Here the version with theory parameter, the real export 

148 
resides in Thy/context.ML **) 

149 

150 
fun get_top_scope_thms thy = 

151 
let val sc = (Locale.get_scope_sg (sign_of thy)) 

152 
in if (null sc) then (warning "No locale in theory"; []) 

153 
else map (#prop o rep_thm) (map #2 (#thms(snd(hd sc)))) 

154 
end; 

155 

156 
fun implies_intr_some_hyps thy A_set th = 

157 
let 

158 
val sign = sign_of thy; 

159 
val used_As = A_set inter #hyps(rep_thm(th)); 

160 
val ctl = map (cterm_of sign) used_As 

161 
in foldl (fn (x, y) => Thm.implies_intr y x) (th, ctl) 

162 
end; 

163 

164 
fun standard_some thy A_set th = 

165 
let val {maxidx,...} = rep_thm th 

166 
in 

167 
th > implies_intr_some_hyps thy A_set 

168 
> forall_intr_frees > forall_elim_vars (maxidx + 1) 

169 
> Thm.strip_shyps > Thm.implies_intr_shyps 

170 
> zero_var_indexes > Thm.varifyT > Thm.compress 

171 
end; 

172 

173 
fun export_thy thy th = 

174 
let val A_set = get_top_scope_thms thy 

175 
in 

176 
standard_some thy [] (Seq.hd ((REPEAT (FIRSTGOAL (rtac reflexive_thm))) (standard_some thy A_set th))) 

177 
end; 

178 

5246  179 
val export = standard o Seq.hd o (REPEAT (FIRSTGOAL (rtac reflexive_thm))) o standard; 
180 

0  181 
(*Common treatment of "goal" and "prove_goal": 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

182 
Return assumptions, initial proof state, and function to make result. 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

183 
"atomic" indicates if the goal should be wrapped up in the function 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

184 
"Goal::prop=>prop" to avoid assumptions being returned separately. 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

185 
*) 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

186 
fun prepare_proof atomic rths chorn = 
230  187 
let val {sign, t=horn,...} = rep_cterm chorn; 
0  188 
val (_,As,B) = Logic.strip_horn(horn); 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

189 
val atoms = atomic andalso 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

190 
forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

191 
val (As,B) = if atoms then ([],horn) else (As,B); 
230  192 
val cAs = map (cterm_of sign) As; 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

193 
val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

194 
val cB = cterm_of sign B; 
5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset

195 
val st0 = let val st = Drule.mk_triv_goal cB 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

196 
in rewrite_goals_rule rths st end 
0  197 
(*discharges assumptions from state in the order they appear in goal; 
1460  198 
checks (if requested) that resulting theorem is equivalent to goal. *) 
0  199 
fun mkresult (check,state) = 
4270  200 
let val state = Seq.hd (flexflex_rule state) 
1565  201 
handle THM _ => state (*smash flexflex pairs*) 
1460  202 
val ngoals = nprems_of state 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

203 
val ath = strip_shyps (implies_intr_list cAs state) 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

204 
val th = ath RS Drule.rev_triv_goal 
1240  205 
val {hyps,prop,sign=sign',...} = rep_thm th 
206 
val xshyps = extra_shyps th; 

2169
31ba286f2307
Removed "standard" call from uresult, to allow specialist applications
paulson
parents:
2126
diff
changeset

207 
in if not check then th 
3532  208 
else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state 
1460  209 
("Signature of proof state has changed!" ^ 
210 
sign_error (sign,sign')) 

3532  211 
else if ngoals>0 then !result_error_fn state 
1460  212 
(string_of_int ngoals ^ " unsolved goals!") 
5246  213 
else if (not (null hyps) andalso (not (Locale.in_locale hyps sign))) 
214 
then !result_error_fn state 

5748
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset

215 
("Additional hypotheses:\n" ^ 
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset

216 
cat_lines 
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset

217 
(map (Sign.string_of_term sign) 
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset

218 
(filter (fn x => (not (Locale.in_locale [x] sign))) 
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset

219 
hyps))) 
3532  220 
else if not (null xshyps) then !result_error_fn state 
1240  221 
("Extra sort hypotheses: " ^ 
3853  222 
commas (map (Sign.str_of_sort sign) xshyps)) 
1460  223 
else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
224 
(term_of chorn, prop) 

5246  225 
then (if (null(hyps)) then standard th 
226 
else varify th) 

3532  227 
else !result_error_fn state "proved a different theorem" 
0  228 
end 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
577
diff
changeset

229 
in 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
577
diff
changeset

230 
if Sign.eq_sg(sign, #sign(rep_thm st0)) 
0  231 
then (prems, st0, mkresult) 
232 
else error ("Definitions would change the proof state's signature" ^ 

1460  233 
sign_error (sign, #sign(rep_thm st0))) 
0  234 
end 
235 
handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s); 

236 

237 
(*Prints exceptions readably to users*) 

577  238 
fun print_sign_exn_unit sign e = 
0  239 
case e of 
240 
THM (msg,i,thms) => 

1460  241 
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); 
242 
seq print_thm thms) 

0  243 
 THEORY (msg,thys) => 
1460  244 
(writeln ("Exception THEORY raised:\n" ^ msg); 
4994  245 
seq (Pretty.writeln o Display.pretty_theory) thys) 
0  246 
 TERM (msg,ts) => 
1460  247 
(writeln ("Exception TERM raised:\n" ^ msg); 
248 
seq (writeln o Sign.string_of_term sign) ts) 

0  249 
 TYPE (msg,Ts,ts) => 
1460  250 
(writeln ("Exception TYPE raised:\n" ^ msg); 
251 
seq (writeln o Sign.string_of_typ sign) Ts; 

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

0  253 
 e => raise e; 
254 

577  255 
(*Prints an exception, then fails*) 
256 
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise ERROR); 

257 

0  258 
(** the prove_goal.... commands 
259 
Prove theorem using the listed tactics; check it has the specified form. 

260 
Augment signature with all type assignments of goal. 

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

262 

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

5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset

264 
fun prove_goalw_cterm_general check rths chorn tacsf = 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

265 
let val (prems, st0, mkresult) = prepare_proof false rths chorn 
0  266 
val tac = EVERY (tacsf prems) 
267 
fun statef() = 

4270  268 
(case Seq.pull (tac st0) of 
1460  269 
Some(st,_) => st 
270 
 _ => error ("prove_goal: tactic failed")) 

5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset

271 
in mkresult (check, cond_timeit (!proof_timing) statef) end 
914
cae574c09137
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
lcp
parents:
696
diff
changeset

272 
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e; 
1460  273 
error ("The exception above was raised for\n" ^ 
274 
string_of_cterm chorn)); 

545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exceptionhandling, moved
lcp
parents:
253
diff
changeset

275 

5614
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset

276 
(*Two variants: one checking the result, one not. 
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset

277 
Neither prints runtime messages: they are for internal packages.*) 
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset

278 
fun prove_goalw_cterm rths chorn = 
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset

279 
setmp proof_timing false (prove_goalw_cterm_general true rths chorn) 
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset

280 
and prove_goalw_cterm_nocheck rths chorn = 
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset

281 
setmp proof_timing false (prove_goalw_cterm_general false rths chorn); 
5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset

282 

0  283 

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

285 
fun prove_goalw thy rths agoal tacsf = 

286 
let val sign = sign_of thy 

230  287 
val chorn = read_cterm sign (agoal,propT) 
5614
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset

288 
in prove_goalw_cterm_general true rths chorn tacsf end 
545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exceptionhandling, moved
lcp
parents:
253
diff
changeset

289 
handle ERROR => error (*from read_cterm?*) 
3536  290 
("The error(s) above occurred for " ^ quote agoal); 
0  291 

292 
(*String version with no metarewriterules*) 

293 
fun prove_goal thy = prove_goalw thy []; 

294 

295 

296 
(*** Commands etc ***) 

297 

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

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

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

301 
 x::_ => x; 

302 

303 
(*Pops the given goal stack*) 

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

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

306 

307 

3532  308 
(*Print goals of current level*) 
5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset

309 
val current_goals_markers = ref ("", "", ""); 
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset

310 

3532  311 
fun print_current_goals_default n max th = 
5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset

312 
let val ref (begin_state, end_state, begin_goal) = current_goals_markers in 
5775
cbd439ed350d
tuned current_goals_markers semantics to avoid empty lines;
wenzelm
parents:
5748
diff
changeset

313 
if begin_state = "" then () else writeln begin_state; 
5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset

314 
writeln ("Level " ^ string_of_int n); 
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset

315 
Locale.print_goals_marker begin_goal max th; 
5775
cbd439ed350d
tuned current_goals_markers semantics to avoid empty lines;
wenzelm
parents:
5748
diff
changeset

316 
if end_state = "" then () else writeln end_state 
5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset

317 
end; 
3532  318 

319 
val print_current_goals_fn = ref print_current_goals_default; 

320 

0  321 
(*Print a level of the goal stack.*) 
3532  322 
fun print_top ((th, _), pairs) = 
323 
!print_current_goals_fn (length pairs) (!goals_limit) th; 

0  324 

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

4270  326 
Can do setstate[(st,Seq.empty)] to set st as the state. *) 
0  327 
fun setstate newgoals = 
328 
(print_top (pop newgoals); undo_list := newgoals :: !undo_list); 

329 

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

331 
the goal stack*) 

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

333 

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

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

336 

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

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

339 

340 
(*Return the final result. *) 

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

342 

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

344 
answer extraction, or other instantiation of Vars *) 

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

346 

347 
(*Get subgoal i from goal stack*) 

2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

348 
fun getgoal i = List.nth (prems_of (topthm()), i1) 
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

349 
handle Subscript => error"getgoal: Goal number out of range"; 
0  350 

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

352 
For debugging uses of METAHYPS*) 

353 
local exception GETHYPS of thm list 

354 
in 

355 
fun gethyps i = 

1500  356 
(METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); []) 
0  357 
handle GETHYPS hyps => hyps 
358 
end; 

359 

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

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

362 

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

364 
fun chop_level n (pair,pairs) = 

365 
let val level = length pairs 

2126
d927beecedf8
Allowing negative levels (as offsets) in prlev and choplev
paulson
parents:
1928
diff
changeset

366 
in if n<0 andalso ~n <= level 
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

367 
then List.drop (pair::pairs, ~n) 
2126
d927beecedf8
Allowing negative levels (as offsets) in prlev and choplev
paulson
parents:
1928
diff
changeset

368 
else if 0<=n andalso n<= level 
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

369 
then List.drop (pair::pairs, level  n) 
0  370 
else error ("Level number must lie between 0 and " ^ 
1460  371 
string_of_int level) 
0  372 
end; 
373 

2514  374 
(*Print the given level of the proof; prlev ~1 prints previous level*) 
0  375 
fun prlev n = apply_fun (print_top o pop o (chop_level n)); 
376 
fun pr () = apply_fun print_top; 

377 

2514  378 
(*Set goals_limit and print again*) 
379 
fun prlim n = (goals_limit:=n; pr()); 

380 

0  381 
(** the goal.... commands 
382 
Read main goal. Set global variables curr_prems, curr_mkresult. 

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

384 

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

230  386 
goalw_cterm rths (cterm_of (sign_of thy) t); *) 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

387 
fun agoalw_cterm atomic rths chorn = 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

388 
let val (prems, st0, mkresult) = prepare_proof atomic rths chorn 
0  389 
in undo_list := []; 
4270  390 
setstate [ (st0, Seq.empty) ]; 
0  391 
curr_prems := prems; 
392 
curr_mkresult := mkresult; 

393 
prems 

394 
end; 

395 

5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

396 
val goalw_cterm = agoalw_cterm false; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

397 

0  398 
(*Version taking the goal as a string*) 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

399 
fun agoalw atomic thy rths agoal = 
5246  400 
agoalw_cterm atomic rths (Locale.read_cterm(sign_of thy)(agoal,propT)) 
401 
handle ERROR => error (*from type_assign, etc via prepare_proof*) 

402 
("The error(s) above occurred for " ^ quote agoal); 

0  403 

5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

404 
val goalw = agoalw false; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

405 

0  406 
(*String version with no metarewriterules*) 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

407 
fun agoal atomic thy = agoalw atomic thy []; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

408 
val goal = agoal false; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

409 

a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

410 
(*now the versions that wrap the goal up in `Goal' to make it atomic*) 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

411 

a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

412 
val atomic_goalw = agoalw true; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

413 
val atomic_goal = agoal true; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

414 

0  415 

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

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

4270  418 
(case Seq.pull(tac th) of 
0  419 
None => error"by: tactic failed" 
420 
 Some(th2,ths2) => 

421 
(if eq_thm(th,th2) 

3707
40856b593501
Prints warnings using the "warning" function instead of "writeln"
paulson
parents:
3669
diff
changeset

422 
then warning "Warning: same as previous level" 
1460  423 
else if eq_thm_sg(th,th2) then () 
4280  424 
else warning ("Warning: signature of proof state has changed" ^ 
1460  425 
sign_error (#sign(rep_thm th), #sign(rep_thm th2))); 
0  426 
((th2,ths2)::(th,ths)::pairs))); 
427 

428 
fun by tac = cond_timeit (!proof_timing) 

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

430 

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

432 
Good for debugging proofs involving prove_goal.*) 

433 
val byev = by o EVERY; 

434 

435 

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

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

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

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

4270  440 
(case Seq.pull thstr of 
1460  441 
None => (writeln"Going back a level..."; backtrack pairs) 
442 
 Some(th2,thstr2) => 

443 
(if eq_thm(th,th2) 

3707
40856b593501
Prints warnings using the "warning" function instead of "writeln"
paulson
parents:
3669
diff
changeset

444 
then warning "Warning: same as previous choice at this level" 
1460  445 
else if eq_thm_sg(th,th2) then () 
3707
40856b593501
Prints warnings using the "warning" function instead of "writeln"
paulson
parents:
3669
diff
changeset

446 
else warning "Warning: signature of proof state has changed"; 
1460  447 
(th2,thstr2)::pairs)); 
0  448 

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

450 

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

452 
fun choplev n = make_command (chop_level n); 

453 

454 
(*Chopping back the goal stack*) 

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

456 

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

458 
fun undo() = case !undo_list of 

459 
[] => error"No proof state" 

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

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

462 

463 

464 
(*** Managing the proof stack ***) 

465 

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

467 

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

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

470 

471 

472 
fun top_proof() = case !proofstack of 

1460  473 
[] => error("Stack of proof attempts is empty!") 
0  474 
 p::ps => (p,ps); 
475 

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

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

478 

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

480 
fun pop_proof() = 

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

482 
val prems = restore_proof p 

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

484 

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

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

1460  487 
in proofstack := ps@[save_proof()]; 
488 
restore_proof p; 

489 
pr(); 

490 
!curr_prems 

491 
end; 

0  492 

493 

494 
(** Shortcuts for commonlyused tactics **) 

495 

496 
fun bws rls = by (rewrite_goals_tac rls); 

497 
fun bw rl = bws [rl]; 

498 

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

500 
fun br rl = brs [rl]; 

501 

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

503 
fun be rl = bes [rl]; 

504 

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

506 
fun bd rl = bds [rl]; 

507 

508 
fun ba i = by (assume_tac i); 

509 

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

511 

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

513 

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

515 
fun fr rl = frs [rl]; 

516 

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

518 
fun fe rl = fes [rl]; 

519 

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

521 
fun fd rl = fds [rl]; 

522 

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

524 

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

526 

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

528 

230  529 
fun read s = term_of (read_cterm (top_sg()) 
1460  530 
(s, (TVar(("DUMMY",0),[])))); 
0  531 

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

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

534 

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

536 

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

538 

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

540 

1628
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

541 

0  542 
(*Prints exceptions nicely at top level; 
543 
raises the exception in order to have a polymorphic type!*) 

914
cae574c09137
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
lcp
parents:
696
diff
changeset

544 
fun print_exn e = (print_sign_exn_unit (top_sg()) e; raise e); 
0  545 

546 
end; 

1500  547 

548 
open Goals; 