The abstract types of **goalstack** and
**proofs** are the focus of backwards proof operations. The
type of proofs can be regarded as a list of independent goalstacks, each
with its own state. (Strictly speaking, it is misleading to call these
things *proofs*, but we are using the term in the informal sense
of "working on some proofs".) Most operations act on the head of the
list of goalstacks, and there are operations so that the focus can
change to other goalstacks. A new feature is that the prettyprinting of
goals can be changed interactively, thus giving users some control over
the "look-and-feel" of the goalstack interface.

- Starting a goalstack proof
- Applying a tactic to a goal
- Undo
- Viewing the state of the proof manager
- Switch focus to a different subgoal or proof attempt
- Prettyprinting

val set_goal :goal -> proofs val g : term frag list -> proofsRecall that the type

x<y |- (y - x) + x = xthen we would invoke

- set_goal([--`x < y`--], --`(y - x) + x = x`--); val it = Status: 1 proof. 1. Incomplete: Initial goal: `(y - x) + x = x` ____________________________ `x < y` : proofsTo understand the response from hol90, we should look again at the type of

term_pp_prefix := ""; term_pp_suffix := "";A shorthand for

- g`!x y. x < y ==> ((y - x) + x = x)`; val it = Status: 2 proofs. 2. Incomplete: Initial goal: `(y - x) + x = x` ____________________________ `x < y` 1. Incomplete: Initial goal: `!x y. x < y ==> ((y - x) + x = x)` : proofsCalling

val expandf : tactic -> goalstack val expand : tactic -> goalstack val e : tactic -> goalstackHow does one actually do a goalstack proof then? In most cases, the application of tactics to the current goal is done with the function

- expand INDUCT_TAC; OK.. 2 subgoals: val it = `!y. SUC x < y ==> ((y - SUC x) + SUC x = SUC x)` ____________________________ `!y. x < y ==> ((y - x) + x = x)` `!y. 0 < y ==> ((y - 0) + 0 = 0)` : goalstack - e (INDUCT_TAC THEN REWRITE_TAC (map (theorem "arithmetic") ["ADD_CLAUSES","SUB_0"])); = OK.. 1 subgoal: val it = `0 < SUC y ==> (SUC y = 0)` ____________________________ `0 < y ==> ((y - 0) + 0 = 0)` : goalstackNotice that the second tactic expansion has silently solved the base case of the second induction.

val backup : unit -> goalstack val b : unit -> goalstack val restart : unit -> goalstack val drop : unit -> proofs val set_backup : int -> unitOften (we are tempted to say

- b(); val it = `!y. SUC x < y ==> ((y - SUC x) + SUC x = SUC x)` ____________________________ `!y. x < y ==> ((y - x) + x = x)` `!y. 0 < y ==> ((y - 0) + 0 = 0)` : goalstackTo directly back up all the way to the original goal, the function

- drop(); OK.. val it = Status: 1 proof. 1. Incomplete: Initial goal: `(y - x) + x = x` ____________________________ `x < y` : proofs - drop(); OK.. val it = There are currently no proofs. : proofsEach proof attempt has its own

val p : unit -> goalstack val status : unit -> proofs val initial_goal : unit -> goal val top_goal : unit -> goal val top_goals : unit -> goal list val top_thm : unit -> thmTo view the state of the proof manager at any time, the functions

- g `!n. n <= FACT n`; val it = Status: 1 proof. 1. Incomplete: Initial goal: `!n. n <= FACT n` : proofs - e (INDUCT_TAC THEN REWRITE_TAC[definition "arithmetic" "FACT"]); = OK.. 2 subgoals: val it = `SUC n <= SUC n * FACT n` ____________________________ `n <= FACT n` `0 <= 1` : goalstack - status(); val it = Status: 1 proof. 1. Incomplete: Initial goal: `!n. n <= FACT n` Current goal: `0 <= 1` : proofsNow we suddenly realize that we need a lemma, so we push it on the list of proofs.

- g`!x y. 0 < x ==> y <= y*x`; val it = Status: 2 proofs. 2. Incomplete: Initial goal: `!n. n <= FACT n` Current goal: `0 <= 1` 1. Incomplete: Initial goal: `!x y. 0 < x ==> y <= y * x` : proofsTo get the top goal or goals of a proof attempt, use

- top_goal(); val it = ([],`!x y. 0 < x ==> y <= y * x`) : goalOnce a theorem has been proved, the goalstack that was used to derive it still exists (and the undo-list is still there): its only job now is to hold the theorem. This theorem can be retrieved with

REPEAT INDUCT_TAC THEN REWRITE_TAC[theorem "prim_rec" "NOT_LESS_0"] THEN REWRITE_TAC[theorem "arithmetic" "ZERO_LESS_EQ"] THEN DISCH_TAC THEN RES_TAC THEN PURE_ONCE_REWRITE_TAC[theorem "arithmetic" "MULT_SYM"] THEN MATCH_MP_TAC (REWRITE_RULE[theorem "arithmetic" "MULT_CLAUSES"] (SPEC(--`1`--) (theorem "arithmetic" "LESS_MONO_MULT"))) THEN REWRITE_TAC[PURE_ONCE_REWRITE_RULE [GSYM (theorem "arithmetic" "LESS_EQ_MONO")] (SPEC(--`x:num`--) (theorem "arithmetic" "ZERO_LESS_EQ")), num_CONV(--`1`--)]; = = = = val it = fn : tactic - e it; OK.. val it = Initial goal proved. |- !x y. 0 < x ==> y <= y * x : goalstack - top_thm(); val it = |- !x y. 0 < x ==> y <= y * x : thmWhen we check the status, we see that the attempt has been completed.

- status(); val it = Status: 2 proofs. 2. Incomplete: Initial goal: `!n. n <= FACT n` Current goal: `0 <= 1` 1. Completed: |- !x y. 0 < x ==> y <= y * x : proofs

val rotate : int -> goalstack val r : int -> goalstack val rotate_proofs : int -> proofs val R : int -> proofsOften we want to switch our attention to a different goal, or a different proof. The functions that do this are

- R 1; val it = Status: 2 proofs. 2. Completed: |- !x y. 0 < x ==> y <= y * x 1. Incomplete: Initial goal: `!n. n <= FACT n` Current goal: `0 <= 1` : proofsWhen we examine the goalstack, we see that the first subgoal is trivial, so let's defer it by rotating to the other subgoal:

- p(); val it = `SUC n <= SUC n * FACT n` ____________________________ `n <= FACT n` `0 <= 1` : goalstack - r 1; val it = `0 <= 1` `SUC n <= SUC n * FACT n` ____________________________ `n <= FACT n` : goalstackNow we find that we can use the theorem we just proved, but we have to go and get it:

- R 1; val it = Status: 2 proofs. 2. Incomplete: Initial goal: `!n. n <= FACT n` Current goal: `SUC n <= SUC n * FACT n` ____________________________ `n <= FACT n` 1. Completed: |- !x y. 0 < x ==> y <= y * x : proofs - val th = top_thm(); val th = |- !x y. 0 < x ==> y <= y * x : thmNow rotate back:

- R 1; val it = Status: 2 proofs. 2. Completed: |- !x y. 0 < x ==> y <= y * x 1. Incomplete: Initial goal: `!n. n <= FACT n` Current goal: `SUC n <= SUC n * FACT n` ____________________________ `n <= FACT n` : proofsand apply the theorem:

- e (MATCH_MP_TAC th); OK.. 1 subgoal: val it = `0 < FACT n` ____________________________ `n <= FACT n` : goalstackNow it is simple to apply a pre-proved theorem:

- e (MATCH_ACCEPT_TAC (theorem "arithmetic" "FACT_LESS")); OK.. Goal proved. |- 0 < FACT n Goal proved. |- SUC n <= SUC n * FACT n Remaining subgoals: val it = `0 <= 1` : goalstackWe are left with the trivial goal: it is quickly polished off:

- e (MATCH_ACCEPT_TAC (theorem "arithmetic" "ZERO_LESS_EQ")); OK.. Goal proved. |- 0 <= 1 val it = Initial goal proved. |- !n. n <= FACT n : goalstack - status(); val it = Status: 2 proofs. 2. Completed: |- !x y. 0 < x ==> y <= y * x 1. Completed: |- !n. n <= FACT n : proofsThe sharp-eyed reader will have seen that we have actually made no use of the inductive hypothesis in this proof. We can restart and do a proof by cases:

- restart(); val it = Initial goal: `!n. n <= FACT n` : goalstack - GEN_TAC THEN DISJ_CASES_THEN STRIP_ASSUME_TAC (SPEC(--`n:num`--) (theorem "arithmetic" "num_CASES")) THEN ASM_REWRITE_TAC[definition "arithmetic" "FACT"] THENL [MATCH_ACCEPT_TAC (theorem "arithmetic" "ZERO_LESS_EQ"), MATCH_MP_TAC th THEN MATCH_ACCEPT_TAC (theorem "arithmetic" "FACT_LESS")]; = = = = = = = val it = fn : tactic - e it; OK.. val it = Initial goal proved. |- !n. n <= FACT n : goalstack - status(); val it = Status: 2 proofs. 2. Completed: |- !x y. 0 < x ==> y <= y * x 1. Completed: |- !n. n <= FACT n : proofs

val set_goal_pp : (ppstream -> goal -> unit) -> (ppstream -> goal -> unit) val pp_goalstack : ppstream -> goalstack -> unit val pp_proofs : ppstream -> proofs -> unitIn order to support customization of the goalstack interface, we provide the function

local fun enumerate L = snd(itlist (fn x => fn (n,A) => (n+1, (n,x)::A)) L (1,[])) in fun pp_goal ppstrm (asl,w) = let val {add_string, add_break, begin_block, end_block, add_newline, ...} = PP.with_ppstream ppstrm val pr = Term_io.Hol_pp.pp_term ppstrm in begin_block PP.CONSISTENT 0; if null(asl) then add_newline() else (add_string "Hypotheses:"; add_newline(); begin_block PP.CONSISTENT 0; PP.pr_list (fn (n,tm) => (begin_block PP.INCONSISTENT 0; add_string (Lib.int_to_string n); add_string ". "; pr tm; end_block())) (fn () => ()) add_newline (rev (enumerate asl)); end_block (); add_newline()); add_string (!Globals.goal_line); add_newline (); begin_block PP.CONSISTENT 2; add_string "Goal: "; begin_block PP.CONSISTENT 0; pr w; end_block(); end_block(); add_newline (); add_newline(); end_block () end handle e => (Lib.say "\nError in attempting to print a goal!\n"; raise e) end;Note that installing a prettyprinter returns the value of the current prettyprinter.

- val old_pp = set_goal_pp pp_goal; val old_pp = fn : System.PrettyPrint.ppstream -> goal -> unit - g `(A = B) ==> (C = D) ==> (E = F) ==> (A /\ C /\ E = B /\ D /\ F)`; val it = Status: 3 proofs. 3. Completed: |- !x y. 0 < x ==> y <= y * x 2. Completed: |- !n. n <= FACT n 1. Incomplete: Initial goal: `(A = B) ==> (C = D) ==> (E = F) ==> (A /\ C /\ E = B /\ D /\ F)` : proofsThis new prettyprinter numbers the hypotheses, which can make goals more readable.

- e (REPEAT STRIP_TAC); OK.. 1 subgoal: val it = Hypotheses: 1. A = B 2. C = D 3. E = F ____________________________ Goal: A /\ C /\ E = B /\ D /\ F : goalstack - e (ASM_REWRITE_TAC[]); OK.. Goal proved. [A = B, C = D, E = F] |- A /\ C /\ E = B /\ D /\ F val it = Initial goal proved. |- (A = B) ==> (C = D) ==> (E = F) ==> (A /\ C /\ E = B /\ D /\ F) : goalstack - status(); val it = Status: 3 proofs. 3. Completed: |- !x y. 0 < x ==> y <= y * x 2. Completed: |- !n. n <= FACT n 1. Completed: |- (A = B) ==> (C = D) ==> (E = F) ==> (A /\ C /\ E = B /\ D /\ F) : proofsAnd now, we can reset the prettyprinter and see things the old way:

- b(); val it = Hypotheses: 1. A = B 2. C = D 3. E = F ____________________________ Goal: A /\ C /\ E = B /\ D /\ F : goalstack - set_goal_pp old_pp; val it = fn : System.PrettyPrint.ppstream -> goal -> unit - p(); val it = `A /\ C /\ E = B /\ D /\ F` ____________________________ `A = B` `C = D` `E = F` : goalstack

Beginning of Goal Stack

User Manual Table of Contents.

Konrad Slind, slind@informatik.tu-muenchen.de