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,
(A B C D E F).But what distinguishes ACL2 (the logic) from applicative Common Lisp (the
language) is that in ACL2 you can prove that the concatenation function
app is associative when its arguments are true-lists, whereas in Common
Lisp all you can do is test that proposition.
That is, in ACL2 it makes sense to say that the following formula is a ``theorem.''
Theorem Associativity 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.
