		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Non-trivial-proof-obligation

Signature
(non-trivial-proof-obligation variables hypotheses restriction expr) → oblig?
Arguments: variables — Guard (typed-variable-listp variables).; hypotheses — Guard (obligation-hyp-listp hypotheses).; restriction — Guard (expressionp restriction).; expr — Guard (expressionp expr).
Returns: oblig? — Type (proof-obligation-listp oblig?).

Definitions and Theorems

Function: non-trivial-proof-obligation

(defun non-trivial-proof-obligation
       (variables hypotheses restriction expr)
  (declare (xargs :guard (and (typed-variable-listp variables)
                              (obligation-hyp-listp hypotheses)
                              (expressionp restriction)
                              (expressionp expr))))
  (let ((__function__ 'non-trivial-proof-obligation))
    (declare (ignorable __function__))
    (if (member-equal (obligation-hyp-condition restriction)
                      (obligation-hyp-list-fix hypotheses))
        nil
      (b* ((oblig (make-proof-obligation :variables variables
                                         :hypotheses hypotheses
                                         :conclusion restriction
                                         :source-expression expr)))
        (list oblig)))))

Theorem: proof-obligation-listp-of-non-trivial-proof-obligation

(defthm proof-obligation-listp-of-non-trivial-proof-obligation
  (b* ((oblig? (non-trivial-proof-obligation
                    variables hypotheses restriction expr)))
    (proof-obligation-listp oblig?))
  :rule-classes :rewrite)

Theorem: non-trivial-proof-obligation-of-typed-variable-list-fix-variables

(defthm
  non-trivial-proof-obligation-of-typed-variable-list-fix-variables
 (equal
   (non-trivial-proof-obligation (typed-variable-list-fix variables)
                                 hypotheses restriction expr)
   (non-trivial-proof-obligation
        variables hypotheses restriction expr)))

Theorem: non-trivial-proof-obligation-typed-variable-list-equiv-congruence-on-variables

(defthm
 non-trivial-proof-obligation-typed-variable-list-equiv-congruence-on-variables
 (implies
   (typed-variable-list-equiv variables variables-equiv)
   (equal
        (non-trivial-proof-obligation
             variables hypotheses restriction expr)
        (non-trivial-proof-obligation variables-equiv
                                      hypotheses restriction expr)))
 :rule-classes :congruence)

Theorem: non-trivial-proof-obligation-of-obligation-hyp-list-fix-hypotheses

(defthm
 non-trivial-proof-obligation-of-obligation-hyp-list-fix-hypotheses
 (equal
  (non-trivial-proof-obligation variables
                                (obligation-hyp-list-fix hypotheses)
                                restriction expr)
  (non-trivial-proof-obligation
       variables hypotheses restriction expr)))

Theorem: non-trivial-proof-obligation-obligation-hyp-list-equiv-congruence-on-hypotheses

(defthm
 non-trivial-proof-obligation-obligation-hyp-list-equiv-congruence-on-hypotheses
 (implies (obligation-hyp-list-equiv hypotheses hypotheses-equiv)
          (equal (non-trivial-proof-obligation
                      variables hypotheses restriction expr)
                 (non-trivial-proof-obligation
                      variables
                      hypotheses-equiv restriction expr)))
 :rule-classes :congruence)

Theorem: non-trivial-proof-obligation-of-expression-fix-restriction

(defthm non-trivial-proof-obligation-of-expression-fix-restriction
  (equal (non-trivial-proof-obligation
              variables
              hypotheses (expression-fix restriction)
              expr)
         (non-trivial-proof-obligation
              variables hypotheses restriction expr)))

Theorem: non-trivial-proof-obligation-expression-equiv-congruence-on-restriction

(defthm
 non-trivial-proof-obligation-expression-equiv-congruence-on-restriction
 (implies (expression-equiv restriction restriction-equiv)
          (equal (non-trivial-proof-obligation
                      variables hypotheses restriction expr)
                 (non-trivial-proof-obligation
                      variables
                      hypotheses restriction-equiv expr)))
 :rule-classes :congruence)

Theorem: non-trivial-proof-obligation-of-expression-fix-expr

(defthm non-trivial-proof-obligation-of-expression-fix-expr
 (equal
    (non-trivial-proof-obligation variables hypotheses
                                  restriction (expression-fix expr))
    (non-trivial-proof-obligation
         variables hypotheses restriction expr)))

Theorem: non-trivial-proof-obligation-expression-equiv-congruence-on-expr

(defthm
   non-trivial-proof-obligation-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (non-trivial-proof-obligation
                       variables hypotheses restriction expr)
                  (non-trivial-proof-obligation
                       variables
                       hypotheses restriction expr-equiv)))
  :rule-classes :congruence)