author  wenzelm 
Fri, 29 Dec 2000 19:43:52 +0100  
changeset 10745  0f3537fad0f3 
parent 10487  97d25c125c61 
child 11554  685daff01da4 
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 

7234  15 
val reset_goals : unit > unit 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

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

17 
val atomic_goalw : theory > thm list > string > thm list 
6189  18 
val Goal : string > thm list 
19 
val Goalw : thm list > string > thm list 

1460  20 
val ba : int > unit 
21 
val back : unit > unit 

22 
val bd : thm > int > unit 

23 
val bds : thm list > int > unit 

24 
val be : thm > int > unit 

25 
val bes : thm list > int > unit 

26 
val br : thm > int > unit 

27 
val brs : thm list > int > unit 

28 
val bw : thm > unit 

29 
val bws : thm list > unit 

30 
val by : tactic > unit 

31 
val byev : tactic list > unit 

32 
val chop : unit > unit 

33 
val choplev : int > unit 

6017  34 
val export_thy : theory > thm > thm 
5246  35 
val export : thm > thm 
6189  36 
val Export : thm > thm 
1460  37 
val fa : unit > unit 
38 
val fd : thm > unit 

39 
val fds : thm list > unit 

40 
val fe : thm > unit 

41 
val fes : thm list > unit 

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

43 
val fr : thm > unit 

44 
val frs : thm list > unit 

45 
val getgoal : int > term 

46 
val gethyps : int > thm list 

47 
val goal : theory > string > thm list 

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

49 
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

50 
val current_goals_markers: (string * string * string) ref 
5246  51 
val print_current_goals_default: (int > int > thm > unit) 
3532  52 
val print_current_goals_fn : (int > int > thm > unit) ref 
1460  53 
val pop_proof : unit > thm list 
54 
val pr : unit > unit 

8884  55 
val disable_pr : unit > unit 
56 
val enable_pr : unit > unit 

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

57 
val prlev : int > unit 
2514  58 
val prlim : int > unit 
1460  59 
val premises : unit > thm list 
60 
val prin : term > unit 

61 
val printyp : typ > unit 

62 
val pprint_term : term > pprint_args > unit 

63 
val pprint_typ : typ > pprint_args > unit 

64 
val print_exn : exn > 'a 

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

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

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

69 
val prove_goalw_cterm_nocheck : thm list>cterm>(thm list>tactic list)>thm 
1460  70 
val push_proof : unit > unit 
71 
val read : string > term 

72 
val ren : string > int > unit 

73 
val restore_proof : proof > thm list 

74 
val result : unit > thm 

3532  75 
val result_error_fn : (thm > string > thm) ref 
1460  76 
val rotate_proof : unit > thm list 
77 
val uresult : unit > thm 

78 
val save_proof : unit > proof 

79 
val topthm : unit > thm 

80 
val undo : unit > unit 

0  81 
end; 
82 

1500  83 
structure Goals : GOALS = 
0  84 
struct 
85 

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

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

4270  88 
type gstack = (thm * thm Seq.seq) list; 
0  89 

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

91 

5246  92 

0  93 
(*** References ***) 
94 

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

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

97 

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

99 
fun premises() = !curr_prems; 

100 

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

7234  102 
fun init_mkresult _ = error "No goal has been supplied in subgoal module"; 
103 
val curr_mkresult = ref (init_mkresult: bool*thm>thm); 

0  104 

6390  105 
val dummy = trivial(read_cterm (Theory.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 

7234  115 
(*reset all refs*) 
116 
fun reset_goals () = 

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

7942  118 
undo_list := [[(dummy, Seq.empty)]]); 
7234  119 

0  120 

121 
(*** Setting up goaldirected proof ***) 

122 

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

124 
fun sign_error (sign,sign') = 

3974  125 
let val names = Sign.stamp_names_of sign' \\ Sign.stamp_names_of sign 
126 
in case names of 

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

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

0  129 
end; 
130 

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

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

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

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

135 
print_goals (!goals_limit) state; 
10745  136 
writeln msg; error "Proof failed"); 
1928  137 

3532  138 
val result_error_fn = ref result_error_default; 
1928  139 

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

142 
fun varify th = 

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

144 
in 

145 
th > forall_intr_frees > forall_elim_vars (maxidx + 1) 

7637  146 
> Drule.strip_shyps_warning 
5246  147 
> zero_var_indexes > Thm.varifyT > Thm.compress 
148 
end; 

149 

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

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

6189  153 
export_thy just goes one up. **) 
6017  154 

155 
fun get_top_scope_thms thy = 

6390  156 
let val sc = (Locale.get_scope_sg (Theory.sign_of thy)) 
6017  157 
in if (null sc) then (warning "No locale in theory"; []) 
158 
else map (#prop o rep_thm) (map #2 (#thms(snd(hd sc)))) 

159 
end; 

160 

161 
fun implies_intr_some_hyps thy A_set th = 

162 
let 

6390  163 
val sign = Theory.sign_of thy; 
6017  164 
val used_As = A_set inter #hyps(rep_thm(th)); 
165 
val ctl = map (cterm_of sign) used_As 

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

167 
end; 

168 

169 
fun standard_some thy A_set th = 

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

171 
in 

172 
th > implies_intr_some_hyps thy A_set 

173 
> forall_intr_frees > forall_elim_vars (maxidx + 1) 

7637  174 
> Drule.strip_shyps_warning 
6017  175 
> zero_var_indexes > Thm.varifyT > Thm.compress 
176 
end; 

177 

178 
fun export_thy thy th = 

179 
let val A_set = get_top_scope_thms thy 

180 
in 

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

182 
end; 

183 

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

6189  186 
fun Export th = export_thy (the_context ()) th; 
187 

188 

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

190 
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

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

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

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

194 
fun prepare_proof atomic rths chorn = 
230  195 
let val {sign, t=horn,...} = rep_cterm chorn; 
9533  196 
val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; 
0  197 
val (_,As,B) = Logic.strip_horn(horn); 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

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

199 
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

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

202 
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

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

204 
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

205 
in rewrite_goals_rule rths st end 
0  206 
(*discharges assumptions from state in the order they appear in goal; 
1460  207 
checks (if requested) that resulting theorem is equivalent to goal. *) 
0  208 
fun mkresult (check,state) = 
4270  209 
let val state = Seq.hd (flexflex_rule state) 
1565  210 
handle THM _ => state (*smash flexflex pairs*) 
1460  211 
val ngoals = nprems_of state 
7637  212 
val ath = implies_intr_list cAs state 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset

213 
val th = ath RS Drule.rev_triv_goal 
1240  214 
val {hyps,prop,sign=sign',...} = rep_thm th 
9573
5cadc8146573
the "nocheck" versions of goal functions now standardize their result
paulson
parents:
9533
diff
changeset

215 
val final_th = if (null(hyps)) then standard th else varify th 
5cadc8146573
the "nocheck" versions of goal functions now standardize their result
paulson
parents:
9533
diff
changeset

216 
in if not check then final_th 
3532  217 
else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state 
1460  218 
("Signature of proof state has changed!" ^ 
219 
sign_error (sign,sign')) 

3532  220 
else if ngoals>0 then !result_error_fn state 
1460  221 
(string_of_int ngoals ^ " unsolved goals!") 
5246  222 
else if (not (null hyps) andalso (not (Locale.in_locale hyps sign))) 
223 
then !result_error_fn state 

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

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

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

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

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

228 
hyps))) 
1460  229 
else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
10487  230 
(Envir.beta_norm (term_of chorn), Envir.beta_norm prop) 
9573
5cadc8146573
the "nocheck" versions of goal functions now standardize their result
paulson
parents:
9533
diff
changeset

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

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

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

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

241 

242 
(*Prints exceptions readably to users*) 

577  243 
fun print_sign_exn_unit sign e = 
0  244 
case e of 
245 
THM (msg,i,thms) => 

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

0  248 
 THEORY (msg,thys) => 
1460  249 
(writeln ("Exception THEORY raised:\n" ^ msg); 
4994  250 
seq (Pretty.writeln o Display.pretty_theory) thys) 
0  251 
 TERM (msg,ts) => 
1460  252 
(writeln ("Exception TERM raised:\n" ^ msg); 
253 
seq (writeln o Sign.string_of_term sign) ts) 

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

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

0  258 
 e => raise e; 
259 

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

262 

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

265 
Augment signature with all type assignments of goal. 

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

267 

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

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

269 
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

270 
let val (prems, st0, mkresult) = prepare_proof false rths chorn 
0  271 
val tac = EVERY (tacsf prems) 
272 
fun statef() = 

4270  273 
(case Seq.pull (tac st0) of 
1460  274 
Some(st,_) => st 
275 
 _ => error ("prove_goal: tactic failed")) 

8999  276 
in mkresult (check, cond_timeit (!Library.timing) statef) end 
914
cae574c09137
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
lcp
parents:
696
diff
changeset

277 
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e; 
6960  278 
writeln ("The exception above was raised for\n" ^ 
279 
string_of_cterm chorn); raise e); 

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

280 

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

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

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

283 
fun prove_goalw_cterm rths chorn = 
8999  284 
setmp Library.timing false (prove_goalw_cterm_general true rths chorn) 
5614
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset

285 
and prove_goalw_cterm_nocheck rths chorn = 
8999  286 
setmp Library.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

287 

0  288 

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

290 
fun prove_goalw thy rths agoal tacsf = 

6390  291 
let val sign = Theory.sign_of thy 
230  292 
val chorn = read_cterm sign (agoal,propT) 
5614
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset

293 
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

294 
handle ERROR => error (*from read_cterm?*) 
3536  295 
("The error(s) above occurred for " ^ quote agoal); 
0  296 

297 
(*String version with no metarewriterules*) 

298 
fun prove_goal thy = prove_goalw thy []; 

299 

300 

301 
(*** Commands etc ***) 

302 

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

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

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

306 
 x::_ => x; 

307 

308 
(*Pops the given goal stack*) 

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

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

311 

312 

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

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

315 

3532  316 
fun print_current_goals_default n max th = 
7265  317 
let 
318 
val ref (begin_state, end_state, begin_goal) = current_goals_markers; 

319 
val ngoals = nprems_of th; 

320 
in 

321 
if begin_state = "" then () else writeln begin_state; 

322 
writeln ("Level " ^ string_of_int n ^ 

7063  323 
(if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ 
324 
(if ngoals <> 1 then "s" else "") ^ ")" 

325 
else "")); 

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

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

327 
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

328 
end; 
3532  329 

330 
val print_current_goals_fn = ref print_current_goals_default; 

331 

8884  332 
(* Print a level of the goal stack  subject to quiet mode *) 
333 

334 
val quiet = ref false; 

335 
fun disable_pr () = quiet := true; 

336 
fun enable_pr () = quiet := false; 

337 

3532  338 
fun print_top ((th, _), pairs) = 
8884  339 
if ! quiet then () 
340 
else ! print_current_goals_fn (length pairs) (! goals_limit) th; 

0  341 

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

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

346 

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

348 
the goal stack*) 

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

350 

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

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

353 

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

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

356 

357 
(*Return the final result. *) 

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

359 

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

361 
answer extraction, or other instantiation of Vars *) 

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

363 

364 
(*Get subgoal i from goal stack*) 

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

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

366 
handle Subscript => error"getgoal: Goal number out of range"; 
0  367 

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

369 
For debugging uses of METAHYPS*) 

370 
local exception GETHYPS of thm list 

371 
in 

372 
fun gethyps i = 

1500  373 
(METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); []) 
0  374 
handle GETHYPS hyps => hyps 
375 
end; 

376 

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

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

379 

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

381 
fun chop_level n (pair,pairs) = 

382 
let val level = length pairs 

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

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

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

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

386 
then List.drop (pair::pairs, level  n) 
0  387 
else error ("Level number must lie between 0 and " ^ 
1460  388 
string_of_int level) 
0  389 
end; 
390 

2514  391 
(*Print the given level of the proof; prlev ~1 prints previous level*) 
8884  392 
fun prlev n = (enable_pr (); apply_fun (print_top o pop o (chop_level n))); 
393 
fun pr () = (enable_pr (); apply_fun print_top); 

0  394 

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

397 

0  398 
(** the goal.... commands 
399 
Read main goal. Set global variables curr_prems, curr_mkresult. 

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

401 

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

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

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

405 
let val (prems, st0, mkresult) = prepare_proof atomic rths chorn 
0  406 
in undo_list := []; 
4270  407 
setstate [ (st0, Seq.empty) ]; 
0  408 
curr_prems := prems; 
409 
curr_mkresult := mkresult; 

410 
prems 

411 
end; 

412 

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

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

414 

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

416 
fun agoalw atomic thy rths agoal = 
6390  417 
agoalw_cterm atomic rths (Locale.read_cterm(Theory.sign_of thy)(agoal,propT)) 
5246  418 
handle ERROR => error (*from type_assign, etc via prepare_proof*) 
419 
("The error(s) above occurred for " ^ quote agoal); 

0  420 

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

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

422 

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

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

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

426 

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

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

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

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

430 

6189  431 
(*implicit context versions*) 
432 
fun Goal s = atomic_goal (Context.the_context ()) s; 

433 
fun Goalw thms s = atomic_goalw (Context.the_context ()) thms s; 

434 

0  435 

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

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

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

441 
(if eq_thm(th,th2) 

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

442 
then warning "Warning: same as previous level" 
1460  443 
else if eq_thm_sg(th,th2) then () 
4280  444 
else warning ("Warning: signature of proof state has changed" ^ 
1460  445 
sign_error (#sign(rep_thm th), #sign(rep_thm th2))); 
0  446 
((th2,ths2)::(th,ths)::pairs))); 
447 

8999  448 
fun by tac = cond_timeit (!Library.timing) 
0  449 
(fn() => make_command (by_com tac)); 
450 

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

452 
Good for debugging proofs involving prove_goal.*) 

453 
val byev = by o EVERY; 

454 

455 

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

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

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

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

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

463 
(if eq_thm(th,th2) 

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

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

466 
else warning "Warning: signature of proof state has changed"; 
1460  467 
(th2,thstr2)::pairs)); 
0  468 

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

470 

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

472 
fun choplev n = make_command (chop_level n); 

473 

474 
(*Chopping back the goal stack*) 

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

476 

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

478 
fun undo() = case !undo_list of 

479 
[] => error"No proof state" 

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

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

482 

483 

484 
(*** Managing the proof stack ***) 

485 

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

487 

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

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

490 

491 

492 
fun top_proof() = case !proofstack of 

1460  493 
[] => error("Stack of proof attempts is empty!") 
0  494 
 p::ps => (p,ps); 
495 

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

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

498 

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

500 
fun pop_proof() = 

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

502 
val prems = restore_proof p 

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

504 

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

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

1460  507 
in proofstack := ps@[save_proof()]; 
508 
restore_proof p; 

509 
pr(); 

510 
!curr_prems 

511 
end; 

0  512 

513 

514 
(** Shortcuts for commonlyused tactics **) 

515 

516 
fun bws rls = by (rewrite_goals_tac rls); 

517 
fun bw rl = bws [rl]; 

518 

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

520 
fun br rl = brs [rl]; 

521 

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

523 
fun be rl = bes [rl]; 

524 

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

526 
fun bd rl = bds [rl]; 

527 

528 
fun ba i = by (assume_tac i); 

529 

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

531 

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

533 

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

535 
fun fr rl = frs [rl]; 

536 

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

538 
fun fe rl = fes [rl]; 

539 

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

541 
fun fd rl = fds [rl]; 

542 

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

544 

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

546 

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

548 

8086  549 
fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT)); 
0  550 

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

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

553 

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

555 

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

557 

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

559 

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

560 

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

563 
fun print_exn e = (print_sign_exn_unit (top_sg()) e; raise e); 
0  564 

565 
end; 

1500  566 

567 
open Goals; 