ACL2-PC::=

(atomic macro) attempt an equality (or equivalence) substitution 

Parent topic:  PROOF-CHECKER
Home


Examples:
=     -- replace the current subterm by a term equated to it in
         one of the hypotheses (if such a term exists)
(= x) -- replace the current subterm by x, assuming that the prover
         can show that they are equal
(= (+ x y) z)
      -- replace the term (+ x y) by the term z inside the current
         subterm, assuming that the prover can prove
         (equal (+ x y) z) from the current top-level hypotheses
         or that this term or (equal z (+ x y)) is among the
         current top-level hypotheses or the current governors
(= & z)
      -- exactly the same as above, if (+ x y) is the current
         subterm
(= (+ x y) z :hints :none)
      -- same as (= (+ x y) z), except that a new subgoal is
         created with the current goal's hypotheses and governors
         as its top-level hypotheses and (equal (+ x y) z) as its
         conclusion
(= (+ x y) z 0)
      -- exactly the same as immediately above
(= (p x)
   (p y)
   :equiv iff
   :otf-flg t
   :hints (("Subgoal 2" :BY FOO) ("Subgoal 1" :use bar)))
      -- same as (= (+ x y) z), except that the prover uses
         the indicated values for otf-flg and hints, and only
         propositional (iff) equivalence is used (however, it
         must be that only propositional equivalence matters at
         the current subterm)


General Form:
(= &optional x y &rest keyword-args)
If terms x and y are supplied, then replace x by y inside the current subterm if they are ``known'' to be ``equal''. Here ``known'' means the following: the prover is called as in the prove command (using keyword-args) to prove (equal x y), except that a keyword argument :equiv is allowed, in which case (equiv x y) is proved instead, where equiv is that argument. (See below for how governors are handled.)

Actually, keyword-args is either a single non-keyword or is a list of the form ((kw-1 x-1) ... (kw-n x-n)), where each kw-i is one of the keywords :equiv, :otf-flg, :hints. Here :equiv defaults to equal if the argument is not supplied or is nil, and otherwise should be the name of an ACL2 equivalence relation. :Otf-flg and :hints give directives to the prover, as explained above and in the documentation for the prove command; however, no prover call is made if :hints is a non-nil atom or if keyword-args is a single non-keyword (more on this below).

Remarks on defaults

(1) If there is only one argument, say a, then x defaults to the current subterm, in the sense that x is taken to be the current subterm and y is taken to be a.

(2) If there are at least two arguments, then x may be the symbol &, which then represents the current subterm. Thus, (= a) is equivalent to (= & a). (Obscure point: actually, & can be in any package, except the keyword package.)

(3) If there are no arguments, then we look for a top-level hypothesis or a governor of the form (equal c u) or (equal u c), where c is the current subterm. In that case we replace the current subterm by u.

As with the prove command, we allow goals to be given ``bye''s in the proof, which may be generated by a :hints keyword argument in keyword-args. These result in the creation of new subgoals.

A proof is attempted unless the :hints argument is a non-nil atom other than :none, or unless there is one element of keyword-args and it is not a keyword. In that case, if there are any hypotheses in the current goal, then what is attempted is a proof of the implication whose antecedent is the conjunction of the current hypotheses and governors and whose conclusion is the appropriate equal term.

Notes: (1) It is allowed to use abbreviations in the hints. (2) The keyword :none has the special role as a value of :hints that is shown clearly in an example above. (3) If there are governors, then the new subgoal has as additional hypotheses the current governors.

ACL2-PC::ACL2-WRAP

(macro) same as (lisp x) 

Parent topic:  PROOF-CHECKER
Home


Example:
(acl2-wrap (pe :here))


General Form:
(acl2-wrap form)
Same as (lisp form). This is provided for interface tools that want to be able to execute the same form in raw Lisp, in the proof-checker, or in the ACL2 top-level loop (lp).

ACL2-PC::ADD-ABBREVIATION

(primitive) add an abbreviation 

Parent topic:  PROOF-CHECKER
Home

Example: (add-abbreviation v (* x y)) causes future occurrences of (* x y) to be printed as (? v), until (unless) a corresponding invocation of remove-abbreviations occurs. In this case we say that v ``abbreviates'' (* x y). 

General Form:
(add-abbreviation var &optional raw-term)
Let var be an abbreviation for raw-term, if raw-term is supplied, else for the current subterm. Note that var must be a variable that does not already abbreviate some term.

A way to think of abbreviations is as follows. Imagine that whenever an abbreviation is added, say v abbreviates expr, an entry associating v to expr is made in an association list, which we will call ``*abbreviations-alist*''. Then simply imagine that ? is a function defined by something like: 

(defun ? (v)
  (let ((pair (assoc v *abbreviations-alist*)))
    (if pair (cdr pair)
      (error ...))))
Of course the implementation isn't exactly like that, since the ``constant'' *abbreviations-alist* actually changes each time an add-abbreviation instruction is successfully invoked. Nevertheless, if one imagines an appropriate redefinition of the ``constant'' *abbreviations-alist* each time an add-abbreviation is invoked, then one will have a clear model of the meaning of such an instruction.

The effect of abbreviations on output is that before printing a term, each subterm that is abbreviated by a variable v is first replaced by (? v).

The effect of abbreviations on input is that every built-in proof-checker command accepts abbreviations wherever a term is expected as an argument, i.e., accepts the syntax (? v) whenever v abbreviates a term. For example, the second argument of add-abbreviation may itself use abbreviations that have been defined by previous add-abbreviation instructions.

See also remove-abbreviations and show-abbreviations.

ACL2-PC::BASH

(atomic macro) call the ACL2 theorem prover's simplifier 

Parent topic:  PROOF-CHECKER
Home


Examples:
bash -- attempt to prove the current goal by simplification alone
(bash ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
     -- attempt to prove the current goal by simplification alone,
        with the indicated hints


General Form:
(bash &rest hints)
Call the theorem prover's simplifier, creating a subgoal for each resulting goal.

Notice that unlike prove, the arguments to bash are spread out, and are all hints.

Note: All forcing rounds will be skipped (unless there are more than 15 subgoals generated in the first forcing round, an injustice that should be rectified by the next release).

ACL2-PC::BDD

(atomic macro) prove the current goal using bdds 

Parent topic:  PROOF-CHECKER
Home


Examples:
bdd
(bdd :vars nil :bdd-constructors (cons) :prove t :literal :all)

The general form is as shown in the latter example above, but with any keyword-value pairs omitted and with values as described for the :bdd hint; see hints.

This command simply calls the theorem prover with the indicated bdd hint for the top-level goal. Note that if :prove is t (the default), then the proof will succeed entirely using bdds or else it will fail immediately. See bdd.

ACL2-PC::BK

(atomic macro) move backward one argument in the enclosing term 

Parent topic:  PROOF-CHECKER
Home


Example and General Form:
bk
For example, if the conclusion is (= x (* (- y) z)) and the current subterm is (* (- y) z), then after executing bk, the current subterm will be x.

Move to the previous argument of the enclosing term.

This is the same as up followed by (dive n-1), where n is the position of the current subterm in its parent term in the conclusion. Thus in particular, the nx command fails if one is already at the top of the conclusion.

See also up, dive, top, and bk.

ACL2-PC::BOOKMARK

(macro) insert matching ``bookends'' comments 

Parent topic:  PROOF-CHECKER
Home


Example:
(bookmark final-goal)


General Form:
(bookmark name &rest instruction-list)
Run the instructions in instruction-list (as though this were a call of do-all; see the documentation for do-all), but first insert a begin bookend with the given name and then, when the instructions have been completed, insert an end bookend with that same name. See the documentation of comm for an explanation of bookends and how they can affect the display of instructions.

ACL2-PC::CASESPLIT

(primitive) split into two cases 

Parent topic:  PROOF-CHECKER
Home


Example:
(casesplit (< x y)) -- assuming that we are at the top of the
                       conclusion, add (< x y) as a new top-level
                       hypothesis in the current goal, and create a
                       subgoal identical to the current goal except
                       that it has (not (< x y)) as a new top-level
                       hypothesis


General Form:
(casesplit expr &optional use-hyps-flag do-not-flatten-flag)
When the current subterm is the entire conclusion, this instruction adds expr as a new top-level hypothesis, and create a subgoal identical to the existing current goal except that it has the negation of expr as a new top-level hypothesis. See also claim. The optional arguments control the use of governors and the ``flattening'' of new hypotheses, as we now explain.

The argument use-hyps-flag is only of interest when there are governors. (To read about governors, see the documentation for the command hyps). In that case, if use-hyps-flag is not supplied or is nil, then the description above is correct; but otherwise, it is not expr but rather it is (implies govs expr) that is added as a new top-level hypothesis (and whose negation is added as a top-level hypothesis for the new goal), where govs is the conjunction of the governors.

If do-not-flatten-flag is supplied and not nil, then that is all there is to this command. Otherwise (thus this is the default), when the claimed term (first argument) is a conjunction (and) of terms and the claim instruction succeeds, then each (nested) conjunct of the claimed term is added as a separate new top-level hypothesis. Consider the following example, assuming there are no governors. 

(casesplit (and (and (< x y) (integerp a)) (equal r s)) t)
Three new top-level hypotheses are added to the current goal, namely (< x y), (integerp a), and (equal r s). In that case, only one hypothesis is added to create the new goal, namely the negation of (and (< x y) (integerp a) (equal r s)). If the negation of this term had been claimed, then it would be the other way around: the current goal would get a single new hypothesis while the new goal would be created by adding three hypotheses.

Note: It is allowed to use abbreviations in the hints.

ACL2-PC::CG

(macro) change to another goal. 

Parent topic:  PROOF-CHECKER
Home


Examples:
(cg (main . 1)) -- change to the goal (main . 1)
cg              -- change to the next-to-top goal


General Form:
(CG &OPTIONAL goal-name)
Same as (change-goal goal-name t), i.e. change to the indicated and move the current goal to the end of the goal stack.

ACL2-PC::CHANGE-GOAL

(primitive) change to another goal. 

Parent topic:  PROOF-CHECKER
Home


Examples:
(change-goal (main . 1)) -- change to the goal (main . 1)
change-goal              -- change to the next-to-top goal


General Form:
(change-goal &optional goal-name end-flg)
Change to the goal with the name goal-name, i.e. make it the current goal. However, if goal-name is nil or is not supplied, then it defaults to the next-to-top goal, i.e., the second goal in the stack of goals. If end-flg is supplied and not nil, then move the current goal to the end of the goal stack; else merely swap it with the next-to-top goal. Also see documentation for cg.

ACL2-PC::CLAIM

(atomic macro) add a new hypothesis 

Parent topic:  PROOF-CHECKER
Home


Examples:
(claim (< x y))   -- attempt to prove (< x y) from the current
                     top-level hypotheses and if successful, then
                     add (< x y) as a new top-level hypothesis in
                     the current goal
(claim (< x y)
       :otf-flg t
       :hints (("Goal" :induct t)))
                  -- as above, but call the prover using the
                     indicated values for the otf-flg and hints
(claim (< x y) 0) -- as above, except instead of attempting to
                     prove (< x y), create a new subgoal with the
                     same top-level hypotheses as the current goal
                     that has (< x y) as its conclusion
(claim (< x y) :hints :none)
                  -- same as immediately above


General Form:
(claim expr &rest rest-args)
This command creates a new subgoal with the same top-level hypotheses as the current goal but with a conclusion of expr. If rest-args is a non-empty list headed by a non-keyword, then there will be no proof attempted for the new subgoal. With that possible exception, rest-args should consist of keyword arguments. The keyword argument :do-not-flatten controls the ``flattening'' of new hypotheses, just as with the casesplit command (as described in its documentation). The remaining rest-args are used with a call the prove command on the new subgoal, except that if :hints is a non-nil atom, then the prover is not called -- rather, this is the same as the situation described above, where rest-args is a non-empty list headed by a non-keyword.

Notes: (1) Unlike the casesplit command, the claim command is completely insensitive to governors. (2) It is allowed to use abbreviations in the hints. (3) The keyword :none has the special role as a value of :hints that is shown clearly in an example above.

ACL2-PC::COMM

(macro) display instructions from the current interactive session 

Parent topic:  PROOF-CHECKER
Home


Examples:
comm
(comm 10)


General Form:
(comm &optional n)
Prints out instructions in reverse order. This is actually the same as (commands n t) -- or, (commands nil t) if n is not supplied. As explained in the documentation for commands, the final argument of t causes suppression of instructions occurring between so-called ``matching bookends,'' which we now explain.

A ``begin bookend'' is an instruction of the form 

(COMMENT :BEGIN x . y).
Similarly, an ``end bookend'' is an instruction of the form 
(COMMENT :END x' . y').
The ``name'' of the first bookend is x and the ``name'' of the second bookend is x'. When such a pair of instructions occurs in the current state-stack, we call them ``matching bookends'' provided that they have the same name (i.e. x equals x') and if no other begin or end bookend with name x occurs between them. The idea now is that comm hides matching bookends together with the instructions they enclose. Here is a more precise explanation of this ``hiding''; probably there is no value in reading on!

A comm instruction hides bookends in the following manner. (So does a comment instruction when its second optional argument is supplied and non-nil.) First, if the first argument n is supplied and not nil, then we consider only the last n instructions from the state-stack; otherwise, we consider them all. Now the resulting list of instructions is replaced by the result of applying the following process to each pair of matching bookends: the pair is removed, together with everything in between the begin and end bookend of the pair, and all this is replaced by the ``instruction'' 

("***HIDING***" :COMMENT :BEGIN name ...)
where (comment begin name ...) is the begin bookend of the pair. Finally, after applying this process to each pair of matching bookends, each begin bookend of the form (comment begin name ...) that remains is replaced by 
("***UNFINISHED***" :COMMENT :BEGIN name ...) .

ACL2-PC::COMMANDS

(macro) display instructions from the current interactive session 

Parent topic:  PROOF-CHECKER
Home


Examples:
commands
(commands 10 t)


General Forms:


commands or (commands nil)
Print out all the instructions (in the current state-stack) in
reverse order, i.e. from the most recent instruction to the starting
instruction.


(commands n) [n a positive integer]
Print out the most recent n instructions (in the current
state-stack), in reverse order.


(commands x abbreviate-flag)
Same as above, but if abbreviate-flag is non-NIL, then do not
display commands between ``matching bookends''.  See documentation
for comm for an explanation of matching bookends.
Note: If there are more than n instructions in the state-stack, then (commands n) is the same as commands (and also, (commands n abb) is the same as (commands nil abb)).

ACL2-PC::COMMENT

(primitive) insert a comment 

Parent topic:  PROOF-CHECKER
Home


Example:
(comment now begin difficult final goal)


General Form:
(comment &rest x)
This instruction makes no change in the state except to insert the comment instruction.

Some comments can be used to improve the display of commands; see documentation for comm.

ACL2-PC::CONTRADICT

(macro) same as contrapose 

Parent topic:  PROOF-CHECKER
Home

see documentation for contrapose

ACL2-PC::CONTRAPOSE

(primitive) switch a hypothesis with the conclusion, negating both 

Parent topic:  PROOF-CHECKER
Home


Example:
(contrapose 3)


General Form:
(contrapose &optional n)
The (optional) argument n should be a positive integer that does not exceed the number of hypotheses. Negate the current conclusion and make it the nth hypothesis, while negating the current nth hypothesis and making it the current conclusion. If no argument is supplied then the effect is the same as for (contrapose 1).

Note: By ``negate'' we mean an operation that replaces nil by t, x by nil for any other explicit value x, (not x) by x, and any other x by (not x).

ACL2-PC::DEMOTE

(primitive) move top-level hypotheses to the conclusion 

Parent topic:  PROOF-CHECKER
Home


Examples:
demote        -- demote all top-level hypotheses
(demote 3 5)  -- demote hypotheses 3 and 5
For example, if the top-level hypotheses are x and y and the conclusion is z, then after execution of demote, the conclusion will be (implies (and x y) z) and there will be no (top-level) hypotheses. 

General Form:
(demote &rest hyps-indices)
Eliminate the indicated (top-level) hypotheses, but replace the conclusion conc with (implies hyps conc) where hyps is the conjunction of the hypotheses that were eliminated. If no arguments are supplied, then all hypotheses are demoted, i.e. demote is the same as (demote 1 2 ... n) where n is the number of top-level hypotheses.

Note: You must be at the top of the conclusion in order to use this command. Otherwise, first invoke top. Also, demote fails if there are no top-level hypotheses or if indices are supplied that are out of range.

ACL2-PC::DIVE

(primitive) move to the indicated subterm 

Parent topic:  PROOF-CHECKER
Home


Examples:
(DIVE 1)    -- assign the new current subterm to be the first
               argument of the existing current subterm
(DIVE 1 2)  -- assign the new current subterm to be the result of
               first taking the 1st argument of the existing
               current subterm, and then the 2nd argument of that
For example, if the current subterm is 
(* (+ a b) c),
then after (dive 1) it is 
(+ a b).
If after that, then (dive 2) is invoked, the new current subterm will be 
b.
Instead of (dive 1) followed by (dive 2), the same current subterm could be obtained by instead submitting the single instruction (dive 1 2). 

General Form:
(dive &rest naturals-list)
If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers, let the new current subterm be the result of selecting the n_1-st argument of the current subterm, and then the n_2-th subterm of that, ..., finally the n_k-th subterm.

Note: Dive is related to the command pp, in that the diving is done according to raw (translated, internal form) syntax. Use the command dv if you want to dive according to the syntax displayed by the command p. Note that (dv n) can be abbreviated by simply n.

ACL2-PC::DO-ALL

(macro) run the given instructions 

Parent topic:  PROOF-CHECKER
Home


Example:
(do-all induct p prove)


General Form:
(do-all &rest instruction-list)
Run the indicated instructions until there is a hard ``failure''. The instruction ``succeeds'' if and only if each instruction in instruction-list does. (See the documentation for sequence for an explanation of ``success'' and ``failure.'') As each instruction is executed, the system will print the usual prompt followed by that instruction, unless the global state variable print-prompt-and-instr-flg is nil.

Note: If do-all ``fails'', then the failure is hard if and only if the last instruction it runs has a hard ``failure''.

Obscure point: For the record, (do-all ins_1 ins_2 ... ins_k) is the same as (sequence (ins_1 ins_2 ... ins_k)).

ACL2-PC::DO-ALL-NO-PROMPT

(macro) run the given instructions, halting once there is a ``failure'' 

Parent topic:  PROOF-CHECKER
Home


Example:
(do-all-no-prompt induct p prove)


General Form:
(do-all-no-prompt &rest instruction-list)
Do-all-no-prompt is the same as do-all, except that the prompt and instruction are not printed each time, regardless of the value of print-prompt-and-instr-flg. Also, restoring is disabled. See the documentation for do-all.

ACL2-PC::DO-STRICT

(macro) run the given instructions, halting once there is a ``failure'' 

Parent topic:  PROOF-CHECKER
Home


Example:
(do-strict induct p prove)


General Form:
(do-strict &rest instruction-list)
Run the indicated instructions until there is a (hard or soft) ``failure''. In fact do-strict is identical in effect to do-all, except that do-all only halts once there is a hard ``failure''. See the documentation for do-all.

ACL2-PC::DROP

(primitive) drop top-level hypotheses 

Parent topic:  PROOF-CHECKER
Home


Examples:
(drop 2 3) -- drop the second and third hypotheses
drop       -- drop all top-level hypotheses


General Forms:
(drop n1 n2 ...) -- Drop the hypotheses with the indicated indices.


drop             -- Drop all the top-level hypotheses.
Note: If there are no top-level hypotheses, then the instruction drop will fail. If any of the indices is out of range, i.e. is not an integer between one and the number of top-level hypotheses (inclusive), then (drop n1 n2 ...) will fail.

ACL2-PC::DV

(atomic macro) move to the indicated subterm 

Parent topic:  PROOF-CHECKER
Home


Examples:
(dv 1)    -- assign the new current subterm to be the first argument
             of the existing current subterm
(dv 1 2)  -- assign the new current subterm to be the result of
             first taking the 1st argument of the existing
             current subterm, and then the 2nd argument of that
For example, if the current subterm is 
(* (+ a b) c),
then after (dv 1) it is 
(+ a b).
If after that, then (dv 2) is invoked, the new current subterm will be 
b.
Instead of (dv 1) followed by (dv 2), the same current subterm could be obtained by instead submitting the single instruction (dv 1 2). 

General Form:
(dv &rest naturals-list)
If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers, let the new current subterm be the result of selecting the n_1-st argument of the current subterm, and then the n_2-th subterm of that, ..., finally the n_k-th subterm.

Note: (dv n) may be abbreviated by simply n, so we could have typed 1 instead of (dv 1) in the first example above.

Note: See also dive, which is related to the command pp, in that the diving is done according to raw (translated, internal form) syntax. Use the command dv if you want to dive according to the syntax displayed by the command p.

ACL2-PC::ELIM

(atomic macro) call the ACL2 theorem prover's elimination process 

Parent topic:  PROOF-CHECKER
Home


Example and General Form:
elim

Upon running the elim command, the system will create a subgoal will be created for each goal that would have been pushed for proof by induction in an ordinary proof, where only elimination is used; not even simplification is used!

ACL2-PC::EQUIV

(primitive) attempt an equality (or congruence-based) substitution 

Parent topic:  PROOF-CHECKER
Home


Examples:
(equiv (* x y) 3) -- replace (* x y) by 3 everywhere inside the
                     current subterm, if their equality is among the
                     top-level hypotheses or the governors
(equiv x t iff)   -- replace x by t everywhere inside the current
                     subterm, where only propositional equivalence
                     needs to be maintained at each occurrence of x


General form:
(equiv old new &optional relation)
Substitute new for old everywhere inside the current subterm, provided that either (relation old new) or (relation new old) is among the top-level hypotheses or the governors (possibly by way of backchaining and/or refinement; see below). If relation is nil or is not supplied, then it defaults to equal. See also the command =, which is much more flexible. Note that this command fails if no substitution is actually made.

Note: No substitution takes place inside explicit values. So for example, the instruction (equiv 3 x) will cause 3 to be replaced by x if the current subterm is, say, (* 3 y), but not if the current subterm is (* 4 y) even though 4 = (1+ 3).

The following remarks are quite technical and mostly describe a certain weak form of ``backchaining'' that has been implemented for equiv in order to support the = command. In fact neither the term (relation old new) nor the term (relation new old) needs to be explicitly among the current ``assumptions'', i.e., the top-level hypothesis or the governors. Rather, there need only be such an assumption that ``tells us'' (r old new) or (r new old), for some equivalence relation r that refines relation. Here, ``tells us'' means that either one of the indicated terms is among those assumptions, or else there is an assumption that is an implication whose conclusion is one of the indicated terms and whose hypotheses (gathered up by appropriately flattening the first argument of the implies term) are all among the current assumptions.

ACL2-PC::EX

(macro) exit after possibly saving the state 

Parent topic:  PROOF-CHECKER
Home


Example and General Form:
ex

Same as exit, except that first the instruction save is executed.

If save queries the user and is answered negatively, then the exit is aborted.

ACL2-PC::EXIT

(meta) exit the interactive proof-checker 

Parent topic:  PROOF-CHECKER
Home


Examples:
exit                        -- exit the interactive proof-checker
(exit append-associativity) -- exit and create a defthm
                               event named append-associativity


General Forms:


exit --  Exit without storing an event.


(exit event-name &optional rule-classes do-it-flg)
Exit, and store an event.
The command exit returns you to the ACL2 loop. At a later time, (verify) may be executed to get back into the same proof-checker state, as long as there hasn't been an intervening use of the proof-checker (otherwise see save).

When given one or more arguments as shown above, exit still returns you to the ACL2 loop, but first, if the interactive proof is complete, then it attempts create a defthm event with the specified event-name and rule-classes (which defaults to (:rewrite) if not supplied). The event will be printed to the terminal, and then normally the user will be queried whether an event should really be created. However, if the final optional argument do-it-flg is supplied and not nil, then an event will be made without a query.

For example, the form 

(exit top-pop-elim (:elim :rewrite) t)
causes a defthm event named top-pop-elim to be created with rule-classes (:elim :rewrite), without a query to the user (because of the argument t).

Note: it is permitted for event-name to be nil. In that case, the name of the event will be the name supplied during the original call of verify. (See the documentation for verify and commands.) Also in that case, if rule-classes is not supplied then it defaults to the rule-classes supplied in the original call of verify.

Comments on ``success'' and ``failure''. An exit instruction will always ``fail'', so for example, if it appears as an argument of a do-strict instruction then none of the later (instruction) arguments will be executed. Moreover, the ``failure'' will be ``hard'' if an event is successfully created or if the instruction is simply exit; otherwise it will be ``soft''. See the documentation for sequence for an explanation of hard and soft ``failures''. An obscure but potentially important fact is that if the ``failure'' is hard, then the error signal is a special signal that the top-level interactive loop can interpret as a request to exit. Thus for example, a sequencing command that turns an error triple (mv erp val state) into (mv t val state) would never cause an exit from the interactive loop.

If the proof is not complete, then (exit event-name ...) will not cause an exit from the interactive loop. However, in that case it will print out the original user-supplied goal (the one that was supplied with the call to verify) and the current list of instructions.

ACL2-PC::EXPAND

(primitive) expand the current function call without simplification 

Parent topic:  PROOF-CHECKER
Home


Examples:
expand -- expand and do not simplify.
For example, if the current subterm is (append a b), then after (expand t) the current subterm will be the term: 
(if (true-listp x)
    (if x
        (cons (car x) (append (cdr x) y))
      y)
  (apply 'binary-append (list x y)))
regardless of the top-level hypotheses and the governors. 

General Form:
(expand &optional
        do-not-expand-lambda-flg new-goals-flg keep-all-guards-flg)
Expand the function call at the current subterm, and do not simplify. The options have the following meanings: 
do-not-expand-lambda-flg:   default is nil; otherwise, the result
                            should be a lambda expression


new-goals-flg:       default of nil means to introduce APPLY for guards


keep-all-guards-flg: default of nil means that the system should make
                     a weak attempt to prove the guards from the
                     current context
See also x, which allows simplification.

ACL2-PC::FAIL

(macro) cause a failure 

Parent topic:  PROOF-CHECKER
Home


Examples:
fail
(fail t)


General Form:
(fail &optional hard)
This is probably only of interest to writers of macro commands. The only function of fail is to fail to ``succeed''.

The full story is that fail and (fail nil) simply return (mv nil nil state), while (fail hard) returns (mv hard nil state) if hard-flag is not nil. See also do-strict, do-all, and sequence.

ACL2-PC::FORWARDCHAIN

(atomic macro) forward chain from an implication in the hyps 

Parent topic:  PROOF-CHECKER
Home


Example:
(forwardchain 2) ; Second hypothesis should be of the form
                 ; (IMPLIES hyp concl), and the result is to replace
                 ; that hypothesis with concl.



General Forms:
(forwardchain hypothesis-number)
(forwardchain hypothesis-number hints)
(forwardchain hypothesis-number hints quiet-flg)

This command replaces the hypothesis corresponding to given index, which should be of the form (IMPLIES hyp concl), with its consequent concl. In fact, the given hypothesis is dropped, and the replacement hypothesis will appear as the final hypothesis after this command is executed.

The prover must be able to prove the indicated hypothesis from the other hypotheses, or else the command will fail. The :hints argument is used in this prover call, and should have the usual syntax of hints to the prover.

Output is suppressed if quiet-flg is supplied and not nil.