		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-var-hyps

Generate variable hypotheses for certain theorems.

Signature
(simpadd0-gen-var-hyps vartys) → hyps
Arguments: vartys — Guard (ident-type-mapp vartys).
Returns: hyps — Type (true-listp hyps).

The input of this function comes from the vartys component of simpadd0-gout. For each such variable, we add a hypothesis about it saying that the variable can be read from the computation state and it contains a value of the appropriate type.

Definitions and Theorems

Function: simpadd0-gen-var-hyps

(defun simpadd0-gen-var-hyps (vartys)
 (declare (xargs :guard (ident-type-mapp vartys)))
 (let ((__function__ 'simpadd0-gen-var-hyps))
  (declare (ignorable __function__))
  (b*
   (((when (omap::emptyp (ident-type-map-fix vartys)))
     nil)
    ((mv var type) (omap::head vartys))
    ((unless (type-formalp type))
     (raise "Internal error: variable ~x0 has type ~x1."
            var type))
    ((mv & ctype) (ldm-type type))
    (hyp
     (cons
      'b*
      (cons
       (cons
        (cons
         'var
         (cons
          (cons
           'mv-nth
           (cons
            '1
            (cons (cons 'ldm-ident
                        (cons (cons 'ident
                                    (cons (ident->unwrap var) 'nil))
                              'nil))
                  'nil)))
          'nil))
        '((objdes (c::objdesign-of-var var compst))
          (val (c::read-object objdes compst))))
       (cons
        (cons
         'and
         (cons
          'objdes
          (cons
             '(c::valuep val)
             (cons (cons 'equal
                         (cons '(c::type-of-value val)
                               (cons (cons 'quote (cons ctype 'nil))
                                     'nil)))
                   'nil))))
        'nil))))
    (hyps (simpadd0-gen-var-hyps (omap::tail vartys))))
   (cons hyp hyps))))

Theorem: true-listp-of-simpadd0-gen-var-hyps

(defthm true-listp-of-simpadd0-gen-var-hyps
  (b* ((hyps (simpadd0-gen-var-hyps vartys)))
    (true-listp hyps))
  :rule-classes :rewrite)

Theorem: simpadd0-gen-var-hyps-of-ident-type-map-fix-vartys

(defthm simpadd0-gen-var-hyps-of-ident-type-map-fix-vartys
  (equal (simpadd0-gen-var-hyps (ident-type-map-fix vartys))
         (simpadd0-gen-var-hyps vartys)))

Theorem: simpadd0-gen-var-hyps-ident-type-map-equiv-congruence-on-vartys

(defthm
    simpadd0-gen-var-hyps-ident-type-map-equiv-congruence-on-vartys
  (implies (c$::ident-type-map-equiv vartys vartys-equiv)
           (equal (simpadd0-gen-var-hyps vartys)
                  (simpadd0-gen-var-hyps vartys-equiv)))
  :rule-classes :congruence)