0

1 
(* Title: goals


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


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


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


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


9 
pending proofs.


10 
*)


11 


12 


13 
signature GOALS =


14 
sig


15 
structure Tactical: TACTICAL


16 
local open Tactical Tactical.Thm in


17 
type proof


18 
val ba: int > unit


19 
val back: unit > unit


20 
val bd: thm > int > unit


21 
val bds: thm list > int > unit


22 
val be: thm > int > unit


23 
val bes: thm list > int > unit


24 
val br: thm > int > unit


25 
val brs: thm list > int > unit


26 
val bw: thm > unit


27 
val bws: thm list > unit


28 
val by: tactic > unit


29 
val byev: tactic list > unit


30 
val chop: unit > unit


31 
val choplev: int > unit


32 
val fa: unit > unit


33 
val fd: thm > unit


34 
val fds: thm list > unit


35 
val fe: thm > unit


36 
val fes: thm list > unit


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


38 
val fr: thm > unit


39 
val frs: thm list > unit


40 
val getgoal: int > term


41 
val gethyps: int > thm list


42 
val goal: theory > string > thm list


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


44 
val goalw_cterm: thm list > Sign.cterm > thm list


45 
val pop_proof: unit > thm list


46 
val pr: unit > unit


47 
val premises: unit > thm list


48 
val prin: term > unit


49 
val printyp: typ > unit


50 
val pprint_term: term > pprint_args > unit


51 
val pprint_typ: typ > pprint_args > unit


52 
val print_exn: exn > 'a


53 
val prlev: int > unit


54 
val proof_timing: bool ref


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


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


57 
val prove_goalw_cterm: thm list>Sign.cterm>(thm list>tactic list)>thm


58 
val push_proof: unit > unit


59 
val read: string > term


60 
val ren: string > int > unit


61 
val restore_proof: proof > thm list


62 
val result: unit > thm


63 
val rotate_proof: unit > thm list


64 
val uresult: unit > thm


65 
val save_proof: unit > proof


66 
val topthm: unit > thm


67 
val undo: unit > unit


68 
end


69 
end;


70 


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


72 
and Pattern:PATTERN


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


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


75 
struct


76 
structure Tactical = Tactic.Tactical


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


78 
in


79 


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


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


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


83 


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


85 


86 
(*** References ***)


87 


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


89 
val proof_timing = ref false;


90 


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


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


93 


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


95 
fun premises() = !curr_prems;


96 


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


98 
val curr_mkresult =


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


100 
: bool*thm>thm);


101 


102 
val dummy = trivial(Sign.read_cterm Sign.pure


103 
("PROP No_goal_has_been_supplied",propT));


104 


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


106 
A list of lists!*)


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


108 


109 
(* Stack of proof attempts *)


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


111 


112 


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


114 


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


116 
fun sign_error (sign,sign') =


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


118 
#stamps(Sign.rep_sg sign)


119 
in case stamps of


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


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


122 
end;


123 


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


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


126 
fun prepare_proof rths chorn =


127 
let val {sign, t=horn,...} = Sign.rep_cterm chorn;


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


129 
val cAs = map (Sign.cterm_of sign) As;


130 
val p_rew = if null rths then I else rewrite_rule rths;


131 
val c_rew = if null rths then I else rewrite_goals_rule rths;


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


133 
and st0 = c_rew (trivial (Sign.cterm_of sign B))


134 
fun result_error state msg =


135 
(writeln ("Bad final proof state:");


136 
print_goals (!goals_limit) state;


137 
error msg)


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


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


140 
fun mkresult (check,state) =


141 
let val ngoals = nprems_of state


142 
val th = implies_intr_list cAs state


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


144 
in if not check then standard th


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


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


147 
sign_error (sign,sign'))


148 
else if ngoals>0 then result_error state


149 
(string_of_int ngoals ^ " unsolved goals!")


150 
else if not (null hyps) then result_error state


151 
("Additional hypotheses:\n" ^


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


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


154 
(Sign.term_of chorn, prop)


155 
then standard th


156 
else result_error state "proved a different theorem"


157 
end


158 
in


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


160 
then (prems, st0, mkresult)


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


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


163 
end


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


165 


166 
(*Prints exceptions readably to users*)


167 
fun print_sign_exn sign e =


168 
case e of


169 
THM (msg,i,thms) =>


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


171 
seq print_thm thms)


172 
 THEORY (msg,thys) =>


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


174 
seq print_theory thys)


175 
 TERM (msg,ts) =>


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


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


178 
 TYPE (msg,Ts,ts) =>


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


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


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


182 
 e => raise e;


183 


184 
(** the prove_goal.... commands


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


186 
Augment signature with all type assignments of goal.


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


188 


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


190 
fun prove_goalw_cterm rths chorn tacsf =


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


192 
val tac = EVERY (tacsf prems)


193 
fun statef() =


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


195 
Some(st,_) => st


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


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


198 


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


200 
fun prove_goalw thy rths agoal tacsf =


201 
let val sign = sign_of thy


202 
val chorn = Sign.read_cterm sign (agoal,propT)


203 
in prove_goalw_cterm rths chorn tacsf


204 
handle ERROR => error (*from type_assign, etc via prepare_proof*)


205 
("The error above occurred for " ^ agoal)


206 
 e => (print_sign_exn sign e; (*other exceptions*)


207 
error ("The exception above was raised for " ^ agoal))


208 
end;


209 


210 
(*String version with no metarewriterules*)


211 
fun prove_goal thy = prove_goalw thy [];


212 


213 


214 
(*** Commands etc ***)


215 


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


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


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


219 
 x::_ => x;


220 


221 
(*Pops the given goal stack*)


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


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


224 


225 


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


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


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


229 
print_goals (!goals_limit) th);


230 


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


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


233 
fun setstate newgoals =


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


235 


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


237 
the goal stack*)


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


239 


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


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


242 


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


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


245 


246 
(*Return the final result. *)


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


248 


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


250 
answer extraction, or other instantiation of Vars *)


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


252 


253 
(*Get subgoal i from goal stack*)


254 
fun getgoal i =


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


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


257 
 Q::_ => Q);


258 


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


260 
For debugging uses of METAHYPS*)


261 
local exception GETHYPS of thm list


262 
in


263 
fun gethyps i =


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


265 
handle GETHYPS hyps => hyps


266 
end;


267 


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


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


270 


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


272 
fun chop_level n (pair,pairs) =


273 
let val level = length pairs


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


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


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


277 
string_of_int level)


278 
end;


279 


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


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


282 
fun pr () = apply_fun print_top;


283 


284 
(** the goal.... commands


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


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


287 


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


289 
goalw_cterm rths (Sign.cterm_of (sign_of thy) t); *)


290 
fun goalw_cterm rths chorn =


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


292 
in undo_list := [];


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


294 
curr_prems := prems;


295 
curr_mkresult := mkresult;


296 
prems


297 
end;


298 


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


300 
fun goalw thy rths agoal =


301 
goalw_cterm rths (Sign.read_cterm(sign_of thy)(agoal,propT))


302 
handle ERROR => error (*from type_assign, etc via prepare_proof*)


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


304 


305 
(*String version with no metarewriterules*)


306 
fun goal thy = goalw thy [];


307 


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


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


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


311 
None => error"by: tactic failed"


312 
 Some(th2,ths2) =>


313 
(if eq_thm(th,th2)


314 
then writeln"Warning: same as previous level"


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


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


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


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


319 


320 
fun by tac = cond_timeit (!proof_timing)


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


322 


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


324 
Good for debugging proofs involving prove_goal.*)


325 
val byev = by o EVERY;


326 


327 


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


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


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


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


332 
(case Sequence.pull thstr of


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


334 
 Some(th2,thstr2) =>


335 
(if eq_thm(th,th2)


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


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


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


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


340 


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


342 


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


344 
fun choplev n = make_command (chop_level n);


345 


346 
(*Chopping back the goal stack*)


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


348 


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


350 
fun undo() = case !undo_list of


351 
[] => error"No proof state"


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


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


354 


355 


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


357 


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


359 


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


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


362 


363 


364 
fun top_proof() = case !proofstack of


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


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


367 


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


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


370 


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


372 
fun pop_proof() =


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


374 
val prems = restore_proof p


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


376 


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


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


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


380 
restore_proof p;


381 
pr();


382 
!curr_prems


383 
end;


384 


385 


386 
(** Shortcuts for commonlyused tactics **)


387 


388 
fun bws rls = by (rewrite_goals_tac rls);


389 
fun bw rl = bws [rl];


390 


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


392 
fun br rl = brs [rl];


393 


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


395 
fun be rl = bes [rl];


396 


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


398 
fun bd rl = bds [rl];


399 


400 
fun ba i = by (assume_tac i);


401 


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


403 


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


405 


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


407 
fun fr rl = frs [rl];


408 


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


410 
fun fe rl = fes [rl];


411 


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


413 
fun fd rl = fds [rl];


414 


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


416 


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


418 


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


420 


421 
fun read s = Sign.term_of (Sign.read_cterm (top_sg())


422 
(s, (TVar(("DUMMY",0),[]))));


423 


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


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


426 


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


428 


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


430 


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


432 


433 
(*Prints exceptions nicely at top level;


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


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


436 


437 
end;


438 
end;
