		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-theorem

Check if a theorem is statically well-formed.

Signature
(check-theorem thm ctxt) → (mv err? obligs)
Arguments: thm — Guard (theoremp thm).; ctxt — Guard (contextp ctxt).
Returns: obligs — Type (proof-obligation-listp obligs).

This is at the top level, so the context has no type names, function headers, variables, and hypotheses.

We ensure that a theorem with the same name does not already exist.

We extend the context with the variables, and we check the formula, ensuring it is a boolean.

Definitions and Theorems

Function: check-theorem

(defun check-theorem (thm ctxt)
 (declare (xargs :guard (and (theoremp thm) (contextp ctxt))))
 (declare
      (xargs :guard (and (null (context->types ctxt))
                         (null (context->functions ctxt))
                         (omap::emptyp (context->variables ctxt))
                         (null (context->obligation-vars ctxt))
                         (null (context->obligation-hyps ctxt)))))
 (let ((__function__ 'check-theorem))
   (declare (ignorable __function__))
   (b*
     (((theorem thm) thm)
      ((when (get-theorem thm.name (context->tops ctxt)))
       (mv (list :theorem-already-exists thm.name)
           nil))
      (var-ctxt (typed-variables-to-variable-context thm.variables))
      (ctxt (change-context ctxt
                            :variables var-ctxt
                            :obligation-vars thm.variables))
      (result (check-expression thm.formula ctxt)))
     (type-result-case
          result :err (mv result.info nil)
          :ok
          (if (type-list-equiv result.types (list (type-boolean)))
              (mv nil result.obligations)
            (mv (list :non-boolean-theorem-formula thm.formula)
                nil))))))

Theorem: proof-obligation-listp-of-check-theorem.obligs

(defthm proof-obligation-listp-of-check-theorem.obligs
  (b* (((mv ?err? ?obligs)
        (check-theorem thm ctxt)))
    (proof-obligation-listp obligs))
  :rule-classes :rewrite)

Theorem: check-theorem-of-theorem-fix-thm

(defthm check-theorem-of-theorem-fix-thm
  (equal (check-theorem (theorem-fix thm) ctxt)
         (check-theorem thm ctxt)))

Theorem: check-theorem-theorem-equiv-congruence-on-thm

(defthm check-theorem-theorem-equiv-congruence-on-thm
  (implies (theorem-equiv thm thm-equiv)
           (equal (check-theorem thm ctxt)
                  (check-theorem thm-equiv ctxt)))
  :rule-classes :congruence)

Theorem: check-theorem-of-context-fix-ctxt

(defthm check-theorem-of-context-fix-ctxt
  (equal (check-theorem thm (context-fix ctxt))
         (check-theorem thm ctxt)))

Theorem: check-theorem-context-equiv-congruence-on-ctxt

(defthm check-theorem-context-equiv-congruence-on-ctxt
  (implies (context-equiv ctxt ctxt-equiv)
           (equal (check-theorem thm ctxt)
                  (check-theorem thm ctxt-equiv)))
  :rule-classes :congruence)