author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 5775  cbd439ed350d 
child 5955  6727d29d164f 
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 

5246  31 
val export : thm > thm 
1460  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 

44 
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

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

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

50 
val prlev : int > unit 
2514  51 
val prlim : int > unit 
1628
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

52 
val pr_latex : unit > unit 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

53 
val printgoal_latex : int > unit 
1460  54 
val premises : unit > thm list 
55 
val prin : term > unit 

56 
val printyp : typ > unit 

57 
val pprint_term : term > pprint_args > unit 

58 
val pprint_typ : typ > pprint_args > unit 

59 
val print_exn : exn > 'a 

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

61 
val proof_timing : bool ref 

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

577  63 
val prove_goalw : theory>thm list>string>(thm list>tactic list)>thm 
1460  64 
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

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

68 
val ren : string > int > unit 

69 
val restore_proof : proof > thm list 

70 
val result : unit > thm 

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

74 
val save_proof : unit > proof 

75 
val topthm : unit > thm 

76 
val undo : unit > unit 

0  77 
end; 
78 

1500  79 
structure Goals : GOALS = 
0  80 
struct 
81 

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

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

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

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

87 

5246  88 

0  89 
(*** References ***) 
90 

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

92 
val proof_timing = ref false; 

93 

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

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

96 

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

98 
fun premises() = !curr_prems; 

99 

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

101 
val curr_mkresult = 

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

103 
: bool*thm>thm); 

104 

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

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

109 
A list of lists!*) 

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

112 
(* Stack of proof attempts *) 

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

114 

115 

116 
(*** Setting up goaldirected proof ***) 

117 

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

119 
fun sign_error (sign,sign') = 

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

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

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

0  124 
end; 
125 

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

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

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

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

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

131 
writeln msg; raise ERROR); 
1928  132 

3532  133 
val result_error_fn = ref result_error_default; 
1928  134 

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

137 
fun varify th = 

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

139 
in 

140 
th > forall_intr_frees > forall_elim_vars (maxidx + 1) 

141 
> Thm.strip_shyps > Thm.implies_intr_shyps 

142 
> zero_var_indexes > Thm.varifyT > Thm.compress 

143 
end; 

144 

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

146 
and expand and cancel the locale definitions. It's relatively easy, because 

147 
a definiendum is a locale const, hence Free, hence Var, after standard **) 

148 
val export = standard o Seq.hd o (REPEAT (FIRSTGOAL (rtac reflexive_thm))) o standard; 

149 

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

151 
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

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

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

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

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

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

159 
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

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

162 
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

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

164 
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

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

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

173 
val th = ath RS Drule.rev_triv_goal 
1240  174 
val {hyps,prop,sign=sign',...} = rep_thm th 
175 
val xshyps = extra_shyps th; 

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

176 
in if not check then th 
3532  177 
else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state 
1460  178 
("Signature of proof state has changed!" ^ 
179 
sign_error (sign,sign')) 

3532  180 
else if ngoals>0 then !result_error_fn state 
1460  181 
(string_of_int ngoals ^ " unsolved goals!") 
5246  182 
else if (not (null hyps) andalso (not (Locale.in_locale hyps sign))) 
183 
then !result_error_fn state 

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

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

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

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

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

188 
hyps))) 
3532  189 
else if not (null xshyps) then !result_error_fn state 
1240  190 
("Extra sort hypotheses: " ^ 
3853  191 
commas (map (Sign.str_of_sort sign) xshyps)) 
1460  192 
else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
193 
(term_of chorn, prop) 

5246  194 
then (if (null(hyps)) then standard th 
195 
else varify th) 

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

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

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

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

205 

206 
(*Prints exceptions readably to users*) 

577  207 
fun print_sign_exn_unit sign e = 
0  208 
case e of 
209 
THM (msg,i,thms) => 

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

0  212 
 THEORY (msg,thys) => 
1460  213 
(writeln ("Exception THEORY raised:\n" ^ msg); 
4994  214 
seq (Pretty.writeln o Display.pretty_theory) thys) 
0  215 
 TERM (msg,ts) => 
1460  216 
(writeln ("Exception TERM raised:\n" ^ msg); 
217 
seq (writeln o Sign.string_of_term sign) ts) 

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

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

0  222 
 e => raise e; 
223 

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

226 

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

229 
Augment signature with all type assignments of goal. 

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

231 

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

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

233 
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

234 
let val (prems, st0, mkresult) = prepare_proof false rths chorn 
0  235 
val tac = EVERY (tacsf prems) 
236 
fun statef() = 

4270  237 
(case Seq.pull (tac st0) of 
1460  238 
Some(st,_) => st 
239 
 _ => error ("prove_goal: tactic failed")) 

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

240 
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

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

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

244 

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

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

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

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

248 
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

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

250 
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

251 

0  252 

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

254 
fun prove_goalw thy rths agoal tacsf = 

255 
let val sign = sign_of thy 

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

257 
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

258 
handle ERROR => error (*from read_cterm?*) 
3536  259 
("The error(s) above occurred for " ^ quote agoal); 
0  260 

261 
(*String version with no metarewriterules*) 

262 
fun prove_goal thy = prove_goalw thy []; 

263 

264 

265 
(*** Commands etc ***) 

266 

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

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

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

270 
 x::_ => x; 

271 

272 
(*Pops the given goal stack*) 

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

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

275 

276 

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

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

279 

3532  280 
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

281 
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

282 
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

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

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

285 
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

286 
end; 
3532  287 

288 
val print_current_goals_fn = ref print_current_goals_default; 

289 

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

0  293 

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

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

298 

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

300 
the goal stack*) 

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

302 

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

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

305 

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

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

308 

309 
(*Return the final result. *) 

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

311 

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

313 
answer extraction, or other instantiation of Vars *) 

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

315 

316 
(*Get subgoal i from goal stack*) 

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

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

318 
handle Subscript => error"getgoal: Goal number out of range"; 
0  319 

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

321 
For debugging uses of METAHYPS*) 

322 
local exception GETHYPS of thm list 

323 
in 

324 
fun gethyps i = 

1500  325 
(METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); []) 
0  326 
handle GETHYPS hyps => hyps 
327 
end; 

328 

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

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

331 

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

333 
fun chop_level n (pair,pairs) = 

334 
let val level = length pairs 

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

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

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

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

338 
then List.drop (pair::pairs, level  n) 
0  339 
else error ("Level number must lie between 0 and " ^ 
1460  340 
string_of_int level) 
0  341 
end; 
342 

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

346 

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

349 

0  350 
(** the goal.... commands 
351 
Read main goal. Set global variables curr_prems, curr_mkresult. 

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

353 

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

230  355 
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

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

357 
let val (prems, st0, mkresult) = prepare_proof atomic rths chorn 
0  358 
in undo_list := []; 
4270  359 
setstate [ (st0, Seq.empty) ]; 
0  360 
curr_prems := prems; 
361 
curr_mkresult := mkresult; 

362 
prems 

363 
end; 

364 

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

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

366 

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

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

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

0  372 

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

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

374 

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

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

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

378 

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

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

380 

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

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

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

383 

0  384 

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

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

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

390 
(if eq_thm(th,th2) 

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

391 
then warning "Warning: same as previous level" 
1460  392 
else if eq_thm_sg(th,th2) then () 
4280  393 
else warning ("Warning: signature of proof state has changed" ^ 
1460  394 
sign_error (#sign(rep_thm th), #sign(rep_thm th2))); 
0  395 
((th2,ths2)::(th,ths)::pairs))); 
396 

397 
fun by tac = cond_timeit (!proof_timing) 

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

399 

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

401 
Good for debugging proofs involving prove_goal.*) 

402 
val byev = by o EVERY; 

403 

404 

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

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

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

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

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

412 
(if eq_thm(th,th2) 

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

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

415 
else warning "Warning: signature of proof state has changed"; 
1460  416 
(th2,thstr2)::pairs)); 
0  417 

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

419 

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

421 
fun choplev n = make_command (chop_level n); 

422 

423 
(*Chopping back the goal stack*) 

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

425 

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

427 
fun undo() = case !undo_list of 

428 
[] => error"No proof state" 

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

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

431 

432 

433 
(*** Managing the proof stack ***) 

434 

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

436 

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

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

439 

440 

441 
fun top_proof() = case !proofstack of 

1460  442 
[] => error("Stack of proof attempts is empty!") 
0  443 
 p::ps => (p,ps); 
444 

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

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

447 

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

449 
fun pop_proof() = 

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

451 
val prems = restore_proof p 

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

453 

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

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

1460  456 
in proofstack := ps@[save_proof()]; 
457 
restore_proof p; 

458 
pr(); 

459 
!curr_prems 

460 
end; 

0  461 

462 

463 
(** Shortcuts for commonlyused tactics **) 

464 

465 
fun bws rls = by (rewrite_goals_tac rls); 

466 
fun bw rl = bws [rl]; 

467 

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

469 
fun br rl = brs [rl]; 

470 

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

472 
fun be rl = bes [rl]; 

473 

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

475 
fun bd rl = bds [rl]; 

476 

477 
fun ba i = by (assume_tac i); 

478 

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

480 

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

482 

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

484 
fun fr rl = frs [rl]; 

485 

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

487 
fun fe rl = fes [rl]; 

488 

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

490 
fun fd rl = fds [rl]; 

491 

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

493 

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

495 

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

497 

230  498 
fun read s = term_of (read_cterm (top_sg()) 
1460  499 
(s, (TVar(("DUMMY",0),[])))); 
0  500 

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

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

503 

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

505 

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

507 

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

509 

4211  510 
(* FIXME !? *) 
511 
(* output to LaTeX / xdvi *) 

512 
fun latex s = 

513 
execute ("( cd /tmp ; echo \"" ^ s ^ 

514 
"\"  isa2latex s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &"); 

515 

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

516 
(* Redirect output of function f:unit>unit to LaTeX *) 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

517 
fun redirect_to_latex f = 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

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

519 
val s = ref "" 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

520 
val old_prs_fn = !prs_fn 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

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

522 
(prs_fn := (fn a => s := !s ^ a); 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

523 
f (); 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

524 
latex (!s); 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

525 
prs_fn := old_prs_fn) 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

526 
end; 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

527 

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

528 
(* Display current proof state in xdvi window *) 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

529 
fun pr_latex () = redirect_to_latex pr; 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

530 

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

531 
(* Display goal n of current proof state in xdvi window *) 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

532 
fun printgoal_latex n = redirect_to_latex (fn () => prin(getgoal n)); 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

533 

0  534 
(*Prints exceptions nicely at top level; 
535 
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

536 
fun print_exn e = (print_sign_exn_unit (top_sg()) e; raise e); 
0  537 

538 
end; 

1500  539 

5246  540 

541 

1500  542 
open Goals; 