		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Context-add-binding

Add a binding obligation hypothesis to a context.

Signature
(context-add-binding bind ctxt) → new-ctxt
Arguments: bind — Guard (bindingp bind).; ctxt — Guard (contextp ctxt).
Returns: new-ctxt — Type (contextp new-ctxt).

The hypothesis is added at the end, because its well-formedness may depend on the preceding hypotheses.

Definitions and Theorems

Function: context-add-binding

(defun context-add-binding (bind ctxt)
 (declare (xargs :guard (and (bindingp bind) (contextp ctxt))))
 (let ((__function__ 'context-add-binding))
  (declare (ignorable __function__))
  (change-context
   ctxt
   :obligation-hyps (append (context->obligation-hyps ctxt)
                            (list (obligation-hyp-binding bind))))))

Theorem: contextp-of-context-add-binding

(defthm contextp-of-context-add-binding
  (b* ((new-ctxt (context-add-binding bind ctxt)))
    (contextp new-ctxt))
  :rule-classes :rewrite)

Theorem: context-add-binding-of-binding-fix-bind

(defthm context-add-binding-of-binding-fix-bind
  (equal (context-add-binding (binding-fix bind)
                              ctxt)
         (context-add-binding bind ctxt)))

Theorem: context-add-binding-binding-equiv-congruence-on-bind

(defthm context-add-binding-binding-equiv-congruence-on-bind
  (implies (binding-equiv bind bind-equiv)
           (equal (context-add-binding bind ctxt)
                  (context-add-binding bind-equiv ctxt)))
  :rule-classes :congruence)

Theorem: context-add-binding-of-context-fix-ctxt

(defthm context-add-binding-of-context-fix-ctxt
  (equal (context-add-binding bind (context-fix ctxt))
         (context-add-binding bind ctxt)))

Theorem: context-add-binding-context-equiv-congruence-on-ctxt

(defthm context-add-binding-context-equiv-congruence-on-ctxt
  (implies (context-equiv ctxt ctxt-equiv)
           (equal (context-add-binding bind ctxt)
                  (context-add-binding bind ctxt-equiv)))
  :rule-classes :congruence)