Analyzing Common Lisp Models

To analyze a model you must be able to reason about the operations and relations involved. Perhaps, for example, some aspect of the model depends upon the fact that the concatenation operation is associative.

In any Common Lisp you can confirm that

(app '(A B) (app '(C D) '(E F)))

and

(app (app '(A B) '(C D)) '(E F)))

both evaluate to the same thing,

But what distinguishes ACL2 (the logic) from applicative Common Lisp (the
language) is that in ACL2 you can **prove** that the concatenation function

That is, in ACL2 it makes sense to say that the following formula is a ``theorem.''

TheoremAssociativity of App (implies (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))))

Theorems about the properties of models are proved by symbolically manipulating the operations and relations involved. If the concatenation of sequences is involved in your model, then you may well need the theorem above in order to that your model has some particular property.