		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands-short-list

Perhaps the most commonly used proof-builder commands

The list of subtopics below includes what are arguably the most useful, and most commonly used, proof-builder commands.

Subtopics

ACL2-pc::=: (atomic macro) attempt an equality (or equivalence) substitution
ACL2-pc::s: (primitive) simplify the current subterm
ACL2-pc::exit: (meta) exit the interactive proof-builder
ACL2-pc::in-theory: (primitive) set the current proof-builder theory
ACL2-pc::comm: (macro) display instructions from the current interactive session
ACL2-pc::dv: (atomic macro) move to the indicated subterm
ACL2-pc::x: (atomic macro) expand and (maybe) simplify function call at the current subterm
ACL2-pc::show-rewrites: (macro) display the applicable rewrite rules
ACL2-pc::claim: (atomic macro) add a new hypothesis
ACL2-pc::split: (atomic macro) split the current goal into cases
ACL2-pc::prove: (primitive) call the ACL2 theorem prover to prove the current goal
ACL2-pc::save: (macro) save the proof-builder state (state-stack)
ACL2-pc::demote: (primitive) move top-level hypotheses to the conclusion
ACL2-pc::retrieve: (macro) re-enter the proof-builder
ACL2-pc::bash: (atomic macro) call the ACL2 theorem prover's simplifier
ACL2-pc::p-top: (macro) prettyprint the conclusion, highlighting the current term
ACL2-pc::expand: (primitive) expand the current function call without simplification
ACL2-pc::bk: (atomic macro) move backward one argument in the enclosing term
ACL2-pc::induct: (atomic macro) generate subgoals using induction
ACL2-pc::undo: (meta) undo some instructions
ACL2-pc::top: (atomic macro) move to the top of the goal
ACL2-pc::restore: (meta) remove the effect of an UNDO command
ACL2-pc::replay: (macro) replay one or more instructions
ACL2-pc::p: (macro) prettyprint the current term in the usual user-level (untranslated) syntax
ACL2-pc::nx: (atomic macro) move forward one argument in the enclosing term
ACL2-pc::contrapose: (primitive) switch a hypothesis with the conclusion, negating both
ACL2-pc::up: (primitive) move to the parent (or some ancestor) of the current subterm
ACL2-pc::th: (macro) print the top-level hypotheses and the current subterm
ACL2-pc::use: (atomic macro) use a lemma instance
ACL2-pc::s-prop: (atomic macro) simplify propositionally
ACL2-pc::runes: (macro) print the runes (definitions, lemmas, ...) used
ACL2-pc::goals: (macro) list the names of goals on the stack
ACL2-pc::drop: (primitive) drop top-level hypotheses
ACL2-pc::x-dumb: (atomic macro) expand function call at the current subterm, without simplifying
ACL2-pc::cg: (macro) change to another goal.
ACL2-pc::sr: (macro) same as SHOW-REWRITES
ACL2-pc::r: (macro) same as rewrite