		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Make-subproof-obligations

Create the obligations for a chain of subtypes.

Signature
(make-subproof-obligations variables hypotheses restrictions expr) → obligs
Arguments: variables — Guard (typed-variable-listp variables).; hypotheses — Guard (obligation-hyp-listp hypotheses).; restrictions — Guard (expression-listp restrictions).; expr — Guard (expressionp expr).
Returns: obligs — Type (proof-obligation-listp obligs).

This is used by match-type: see the documentation of that function for background.

This function takes as inputs (i) the typed variables in context, (ii) the hypotheses in context, and (iii) the sequence of expressions that define the restrictions of each subtype in the chain, from the supremum of match-type's source and destination types down to the destination type, in the same order. This function returns as output a list of proof obligations, one for each of the expression in (iii) above: the obligation has that expression as conclusion, and as hypotheses has the ones in (ii) above, augmented by all the preceding type restriction expressions.

Definitions and Theorems

Function: make-subproof-obligations

(defun make-subproof-obligations
       (variables hypotheses restrictions expr)
 (declare (xargs :guard (and (typed-variable-listp variables)
                             (obligation-hyp-listp hypotheses)
                             (expression-listp restrictions)
                             (expressionp expr))))
 (let ((__function__ 'make-subproof-obligations))
  (declare (ignorable __function__))
  (cond
   ((endp restrictions) nil)
   (t
    (let
     ((oblig? (non-trivial-proof-obligation
                   variables hypotheses (car restrictions)
                   expr))
      (r-obligs
       (make-subproof-obligations
          variables
          (append
               (obligation-hyp-list-fix hypotheses)
               (list (obligation-hyp-condition (car restrictions))))
          (cdr restrictions)
          expr)))
     (append oblig? r-obligs))))))

Theorem: proof-obligation-listp-of-make-subproof-obligations

(defthm proof-obligation-listp-of-make-subproof-obligations
  (b*
    ((obligs
          (make-subproof-obligations variables
                                     hypotheses restrictions expr)))
    (proof-obligation-listp obligs))
  :rule-classes :rewrite)

Theorem: make-subproof-obligations-of-typed-variable-list-fix-variables

(defthm
     make-subproof-obligations-of-typed-variable-list-fix-variables
 (equal
      (make-subproof-obligations (typed-variable-list-fix variables)
                                 hypotheses restrictions expr)
      (make-subproof-obligations variables
                                 hypotheses restrictions expr)))

Theorem: make-subproof-obligations-typed-variable-list-equiv-congruence-on-variables

(defthm
 make-subproof-obligations-typed-variable-list-equiv-congruence-on-variables
 (implies
   (typed-variable-list-equiv variables variables-equiv)
   (equal (make-subproof-obligations
               variables hypotheses restrictions expr)
          (make-subproof-obligations variables-equiv
                                     hypotheses restrictions expr)))
 :rule-classes :congruence)

Theorem: make-subproof-obligations-of-obligation-hyp-list-fix-hypotheses

(defthm
    make-subproof-obligations-of-obligation-hyp-list-fix-hypotheses
 (equal
     (make-subproof-obligations variables
                                (obligation-hyp-list-fix hypotheses)
                                restrictions expr)
     (make-subproof-obligations variables
                                hypotheses restrictions expr)))

Theorem: make-subproof-obligations-obligation-hyp-list-equiv-congruence-on-hypotheses

(defthm
 make-subproof-obligations-obligation-hyp-list-equiv-congruence-on-hypotheses
 (implies
  (obligation-hyp-list-equiv hypotheses hypotheses-equiv)
  (equal
    (make-subproof-obligations
         variables hypotheses restrictions expr)
    (make-subproof-obligations variables
                               hypotheses-equiv restrictions expr)))
 :rule-classes :congruence)

Theorem: make-subproof-obligations-of-expression-list-fix-restrictions

(defthm
      make-subproof-obligations-of-expression-list-fix-restrictions
  (equal
       (make-subproof-obligations variables hypotheses
                                  (expression-list-fix restrictions)
                                  expr)
       (make-subproof-obligations variables
                                  hypotheses restrictions expr)))

Theorem: make-subproof-obligations-expression-list-equiv-congruence-on-restrictions

(defthm
 make-subproof-obligations-expression-list-equiv-congruence-on-restrictions
 (implies
  (expression-list-equiv restrictions restrictions-equiv)
  (equal
    (make-subproof-obligations
         variables hypotheses restrictions expr)
    (make-subproof-obligations variables
                               hypotheses restrictions-equiv expr)))
 :rule-classes :congruence)

Theorem: make-subproof-obligations-of-expression-fix-expr

(defthm make-subproof-obligations-of-expression-fix-expr
 (equal
      (make-subproof-obligations variables hypotheses
                                 restrictions (expression-fix expr))
      (make-subproof-obligations variables
                                 hypotheses restrictions expr)))

Theorem: make-subproof-obligations-expression-equiv-congruence-on-expr

(defthm
      make-subproof-obligations-expression-equiv-congruence-on-expr
 (implies
  (expression-equiv expr expr-equiv)
  (equal
    (make-subproof-obligations
         variables hypotheses restrictions expr)
    (make-subproof-obligations variables
                               hypotheses restrictions expr-equiv)))
 :rule-classes :congruence)