preliminaries.lisp

The Common Lisp function char extracts the i^{th} character of a string. Our proofs below don't depend on the definition of char. We tell the theorem-prover to ``disable'' it, which instructs the theorem-prover not to expand the definition of char in proofs.

(in-theory (disable char))


(defthm a-cons-is-not-false
  (iff (cons x y) t))

(defmacro  memberp (x y)
  `(not (null (member ,x ,y))))


(defmacro  member-equal-p (x y)
  `(not (null (member-equal ,x ,y))))


(defmacro  true ()
  't)


(defmacro  false ()
  'nil)


(defmacro  non-nil-non-t-symbolp (x)
  `(and (symbolp ,x)
        (not (equal ,x nil))
        (not (equal ,x t))))

Facts about strings

(defthm stringp-subseq-stringp
  (implies (stringp x)
           (stringp (subseq x i j)))
  :rule-classes (:rewrite :type-prescription))

Some General Macros

Some macros to make the code more readable.

The macro non-empty is used to recognize stacks that are not empty.This definition relies on two facts: (1) that we use nil to represent an empty stack, and (2) that Common Lisp -- and hence ACL2 -- considers any value other than nil to be true. Thus the expression (not (null (foo x))) has the same truth value as (foo x), even though it may have a different non-nil value.

(defmacro  non-empty (stack)
  `(consp ,stack))


(defmacro  stack-empty-p (x)
  `(null ,x))


(defmacro  stack-top (x)
  `(car ,x))


(defmacro  observe (name term \&rest defthm-options)
  `(defthm ,name
     ,term
     :rule-classes ()
     ,@defthm-options))

Some small functions

These functions are used at various places when defining instructions. They are trivial functions and are used mainly as a ``do nothing'' place-holder where a function is required in the standard form definition of some instructions.

(defun true-2 (x y)
  (declare (ignore x y)
           (xargs :guard t))
  t)


(defun identity-2 (x y)
  (declare (ignore x)
           (xargs :guard t))
  y)

This page is URL http://www.computationallogic.com/software/djvm/html-0.5/preliminaries.html