PROOF-CHECKER

Major Section:  ACL2 Documentation

Call this up with (verify ...).

• ACL2-PC::= -- (atomic macro)
  attempt an equality (or equivalence) substitution

• ACL2-PC::ACL2-WRAP -- (macro)
  same as (lisp x)

• ACL2-PC::ADD-ABBREVIATION -- (primitive)
  add an abbreviation

• ACL2-PC::BASH -- (atomic macro)
  call the ACL2 theorem prover's simplifier

• ACL2-PC::BDD -- (atomic macro)
  prove the current goal using bdds

• ACL2-PC::BK -- (atomic macro)
  move backward one argument in the enclosing term

• ACL2-PC::BOOKMARK -- (macro)
  insert matching ``bookends'' comments

• ACL2-PC::CASESPLIT -- (primitive)
  split into two cases

• ACL2-PC::CG -- (macro)
  change to another goal.

• ACL2-PC::CHANGE-GOAL -- (primitive)
  change to another goal.

• ACL2-PC::CLAIM -- (atomic macro)
  add a new hypothesis

• ACL2-PC::COMM -- (macro)
  display instructions from the current interactive session

• ACL2-PC::COMMANDS -- (macro)
  display instructions from the current interactive session

• ACL2-PC::COMMENT -- (primitive)
  insert a comment

• ACL2-PC::CONTRADICT -- (macro)
  same as contrapose

• ACL2-PC::CONTRAPOSE -- (primitive)
  switch a hypothesis with the conclusion, negating both

• ACL2-PC::DEMOTE -- (primitive)
  move top-level hypotheses to the conclusion

• ACL2-PC::DIVE -- (primitive)
  move to the indicated subterm

• ACL2-PC::DO-ALL -- (macro)
  run the given instructions

• ACL2-PC::DO-ALL-NO-PROMPT -- (macro)
  run the given instructions, halting once there is a ``failure''

• ACL2-PC::DO-STRICT -- (macro)
  run the given instructions, halting once there is a ``failure''

• ACL2-PC::DROP -- (primitive)
  drop top-level hypotheses

• ACL2-PC::DV -- (atomic macro)
  move to the indicated subterm

• ACL2-PC::ELIM -- (atomic macro)
  call the ACL2 theorem prover's elimination process

• ACL2-PC::EQUIV -- (primitive)
  attempt an equality (or congruence-based) substitution

• ACL2-PC::EX -- (macro)
  exit after possibly saving the state

• ACL2-PC::EXIT -- (meta)
  exit the interactive proof-checker

• ACL2-PC::EXPAND -- (primitive)
  expand the current function call without simplification

• ACL2-PC::FAIL -- (macro)
  cause a failure

• ACL2-PC::FORWARDCHAIN -- (atomic macro)
  forward chain from an implication in the hyps

• ACL2-PC::FREE -- (atomic macro)
  create a ``free variable''

• ACL2-PC::GENERALIZE -- (primitive)
  perform a generalization

• ACL2-PC::GOALS -- (macro)
  list the names of goals on the stack

• ACL2-PC::HELP -- (macro)
  proof-checker help facility

• ACL2-PC::HELP! -- (macro)
  proof-checker help facility

• ACL2-PC::HELP-LONG -- (macro)
  same as help!

• ACL2-PC::HYPS -- (macro)
  print the hypotheses

• ACL2-PC::ILLEGAL -- (macro)
  illegal instruction

• ACL2-PC::IN-THEORY -- (primitive)
  set the current proof-checker theory

• ACL2-PC::INDUCT -- (atomic macro)
  generate subgoals using induction

• ACL2-PC::LISP -- (meta)
  evaluate the given form in Lisp

• ACL2-PC::MORE -- (macro)
  proof-checker help facility

• ACL2-PC::MORE! -- (macro)
  proof-checker help facility

• ACL2-PC::NEGATE -- (macro)
  run the given instructions, and ``succeed'' if and only if they ``fail''

• ACL2-PC::NIL -- (macro)
  used for interpreting control-d

• ACL2-PC::NOISE -- (meta)
  run instructions with output

• ACL2-PC::NX -- (atomic macro)
  move forward one argument in the enclosing term

• ACL2-PC::ORELSE -- (macro)
  run the first instruction; if (and only if) it ``fails'', run the
  second

• ACL2-PC::P -- (macro)
  prettyprint the current term

• ACL2-PC::P-TOP -- (macro)
  prettyprint the conclusion, highlighting the current term

• ACL2-PC::PP -- (macro)
  prettyprint the current term

• ACL2-PC::PRINT -- (macro)
  print the result of evaluating the given form

• ACL2-PC::PRINT-ALL-GOALS -- (macro)
  print all the (as yet unproved) goals

• ACL2-PC::PRINT-MAIN -- (macro)
  print the original goal

• ACL2-PC::PRO -- (atomic macro)
  repeatedly apply promote

• ACL2-PC::PROMOTE -- (primitive)
  move antecedents of conclusion's implies term to top-level
  hypotheses

• ACL2-PC::PROTECT -- (macro)
  run the given instructions, reverting to existing state upon
  failure

• ACL2-PC::PROVE -- (primitive)
  call the ACL2 theorem prover to prove the current goal

• ACL2-PC::PUT -- (macro)
  substitute for a ``free variable''

• ACL2-PC::QUIET -- (meta)
  run instructions without output

• ACL2-PC::R -- (macro)
  same as rewrite

• ACL2-PC::REDUCE -- (atomic macro)
  call the ACL2 theorem prover's simplifier

• ACL2-PC::REDUCE-BY-INDUCTION -- (macro)
  call the ACL2 prover without induction, after going into
  induction

• ACL2-PC::REMOVE-ABBREVIATIONS -- (primitive)
  remove one or more abbreviations

• ACL2-PC::REPEAT -- (macro)
  repeat the given instruction until it ``fails''

• ACL2-PC::REPEAT-REC -- (macro)
  auxiliary to repeat

• ACL2-PC::REPLAY -- (macro)
  replay one or more instructions

• ACL2-PC::RESTORE -- (meta)
  remove the effect of an UNDO command

• ACL2-PC::RETAIN -- (atomic macro)
  drop all but the indicated top-level hypotheses

• ACL2-PC::RETRIEVE -- (macro)
  re-enter the proof-checker

• ACL2-PC::REWRITE -- (primitive)
  apply a rewrite rule

• ACL2-PC::RUN-INSTR-ON-GOAL -- (macro)
  auxiliary toxae THEN

• ACL2-PC::RUN-INSTR-ON-NEW-GOALS -- (macro)
  auxiliary to then

• ACL2-PC::S -- (primitive)
  simplify the current subterm

• ACL2-PC::S-PROP -- (atomic macro)
  simplify propositionally

• ACL2-PC::SAVE -- (macro)
  save the proof-checker state (state-stack)

• ACL2-PC::SEQUENCE -- (meta)
  run the given list of instructions according to a multitude of
  options

• ACL2-PC::SHOW-ABBREVIATIONS -- (macro)
  display the current abbreviations

• ACL2-PC::SHOW-REWRITES -- (macro)
  display the applicable rewrite rules

• ACL2-PC::SKIP -- (macro)
  ``succeed'' without doing anything

• ACL2-PC::SL -- (atomic macro)
  simplify with lemmas

• ACL2-PC::SPLIT -- (atomic macro)
  split the current goal into cases

• ACL2-PC::SR -- (macro)
  same as SHOW-REWRITES

• ACL2-PC::SUCCEED -- (macro)
  run the given instructions, and ``succeed''

• ACL2-PC::TH -- (macro)
  print the top-level hypotheses and the current subterm

• ACL2-PC::THEN -- (macro)
  apply one instruction to current goal and another to new subgoals

• ACL2-PC::TOP -- (atomic macro)
  move to the top of the goal

• ACL2-PC::TYPE-ALIST -- (macro)
  display the type-alist from the current context

• ACL2-PC::UNDO -- (meta)
  undo some instructions

• ACL2-PC::UNSAVE -- (macro)
  remove a proof-checker state

• ACL2-PC::UP -- (primitive)
  move to the parent (or some ancestor) of the current subterm

• ACL2-PC::USE -- (atomic macro)
  use a lemma instance

• ACL2-PC::X -- (atomic macro)
  expand and (maybe) simplify function call at the current subterm

• ACL2-PC::X-DUMB -- (atomic macro)
  expand function call at the current subterm, without simplifying

• DEFINE-PC-HELP -- define a macro command whose purpose is to print something

• INSTRUCTIONS -- instructions to the proof checker

• MACRO-COMMAND -- compound command for the proof-checker

• RETRIEVE -- re-enter a (specified) proof-checker state

• TOGGLE-PC-MACRO -- change an ordinary macro command to an atomic macro, or vice-versa

• UNSAVE -- remove a proof-checker state

• VERIFY -- enter the interactive proof checker

Individual proof-checker commands have already been listed above. Among them are proof-checker commands help, help-long, more, and more!, which behave respectively like the ACL2 functions :doc, :doc!, :more, and :more!.