How to start using ACL2; the ACL2 command loop
When you start up ACL2, you'll probably find yourself inside the
ACL2 command loop, as indicated by the following prompt.
If not, you should type (LP). See lp, which has a lot more
information about the ACL2 command loop.
You should now be in ACL2. The current ``default-defun-mode'' is
:logic; the other mode is :program, which would
cause the letter p to be printed in the prompt. :Logic means that any function we define is not only executable but also is
axiomatically defined in the ACL2 logic. See defun-mode and see default-defun-mode. For example we can define a function my-cons as
follows. (You may find it useful to start up ACL2 and submit this and other
commands below to the ACL2 command loop, as we won't include
ACL2 !>(defun my-cons (x y) (cons x y))
An easy theorem may then be proved: the car of (my-cons a b)
ACL2 !>(defthm car-my-cons (equal (car (my-cons a b)) a))
You can place raw Lisp forms to evaluate at start-up into file
acl2-init.lsp in your home directory, except on Windows systems. For
example, if you put the following into acl2-init.lsp, then ACL2 will
print "HI" when it starts up.
But be careful; all bets are off when you submit forms to raw Lisp, so this
capability should only be used when you are hacking or when you are setting
some Lisp parameters (e.g., (setq si::*notify-gbc* nil) to turn off
garbage collection notices in GCL).
Notice that unlike Nqthm, the theorem command is defthm
rather than prove-lemma. See defthm, which explains (among other
things) that the default is to turn theorems into rewrite rules.
Various keyword commands are available to query the ACL2 ``world'',
or database. For example, we may view the definition of my-cons by
invoking a command to print events, as follows.
ACL2 !>:pe my-cons
Also see pe. We may also view all the lemmas that rewrite
terms whose top function symbol is car by using the following
command, whose output will refer to the lemma car-my-cons proved
ACL2 !>:pl car
Also see pl. Finally, we may print all the commands back
through the initial world as follows.
ACL2 !>:pbt 0
See history for a list of commands, including these, for viewing the
current ACL2 world.
Continue with the documentation for annotated-ACL2-scripts to
see a simple but illustrative example in the use of ACL2 for reasoning about