		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-join-vartys

Join two maps from identifiers to types.

Signature
(simpadd0-join-vartys vartys1 vartys2) → vartys
Arguments: vartys1 — Guard (ident-type-mapp vartys1).; vartys2 — Guard (ident-type-mapp vartys2).
Returns: vartys — Type (ident-type-mapp vartys).

This is used on maps that must be compatible, so we throw a hard error if that is not the case.

Definitions and Theorems

Function: simpadd0-join-vartys

(defun simpadd0-join-vartys (vartys1 vartys2)
 (declare (xargs :guard (and (ident-type-mapp vartys1)
                             (ident-type-mapp vartys2))))
 (let ((__function__ 'simpadd0-join-vartys))
  (declare (ignorable __function__))
  (b* ((vartys1 (ident-type-map-fix vartys1))
       (vartys2 (ident-type-map-fix vartys2)))
   (if (omap::compatiblep vartys1 vartys2)
       (omap::update* vartys1 vartys2)
    (raise
     "Internal error: ~
              incompatible variable-type maps ~x0 and ~x1"
     vartys1 vartys2)))))

Theorem: ident-type-mapp-of-simpadd0-join-vartys

(defthm ident-type-mapp-of-simpadd0-join-vartys
  (b* ((vartys (simpadd0-join-vartys vartys1 vartys2)))
    (ident-type-mapp vartys))
  :rule-classes :rewrite)

Theorem: simpadd0-join-vartys-of-ident-type-map-fix-vartys1

(defthm simpadd0-join-vartys-of-ident-type-map-fix-vartys1
  (equal (simpadd0-join-vartys (ident-type-map-fix vartys1)
                               vartys2)
         (simpadd0-join-vartys vartys1 vartys2)))

Theorem: simpadd0-join-vartys-ident-type-map-equiv-congruence-on-vartys1

(defthm
    simpadd0-join-vartys-ident-type-map-equiv-congruence-on-vartys1
  (implies (c$::ident-type-map-equiv vartys1 vartys1-equiv)
           (equal (simpadd0-join-vartys vartys1 vartys2)
                  (simpadd0-join-vartys vartys1-equiv vartys2)))
  :rule-classes :congruence)

Theorem: simpadd0-join-vartys-of-ident-type-map-fix-vartys2

(defthm simpadd0-join-vartys-of-ident-type-map-fix-vartys2
  (equal (simpadd0-join-vartys vartys1 (ident-type-map-fix vartys2))
         (simpadd0-join-vartys vartys1 vartys2)))

Theorem: simpadd0-join-vartys-ident-type-map-equiv-congruence-on-vartys2

(defthm
    simpadd0-join-vartys-ident-type-map-equiv-congruence-on-vartys2
  (implies (c$::ident-type-map-equiv vartys2 vartys2-equiv)
           (equal (simpadd0-join-vartys vartys1 vartys2)
                  (simpadd0-join-vartys vartys1 vartys2-equiv)))
  :rule-classes :congruence)