		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-expr-pure-thm

Generate a theorem for the transformation of a pure expression.

Signature
(simpadd0-gen-expr-pure-thm old new falliblep vars const-new thm-index hints) → (mv thm-event thm-name updated-thm-index)
Arguments: old — Guard (exprp old).; new — Guard (exprp new).; falliblep — Guard (booleanp falliblep).; vars — Guard (ident-setp vars).; const-new — Guard (symbolp const-new).; thm-index — Guard (posp thm-index).; hints — Guard (true-listp hints).
Returns: thm-event — Type (pseudo-event-formp thm-event).; thm-name — Type (symbolp thm-name).; updated-thm-index — Type (posp updated-thm-index).

This function takes the old and new expressions as inputs, which must always satisfy c$::expr-pure-formalp. If the two expressions are syntactically equal, the generated theorem just says that the expressions have type int. If they are not syntactically equal, the theorem also says that the execution of the two expressions yields the same result, assuming that the old expression's result is not an error. More precisely, the theorem equates the value components of the expression values returned by expression execution; for our current purposes this is adequate, but we may generalize this in the future.

Note that the calls of c$::ldm-expr in the theorem are known to succeed (i.e. not return any error), given that c$::expr-pure-formalp holds.

This function also takes as input a set of identifiers, which are the variables in scope of type int. The theorem includes a hypothesis for each of these variables, saying that they are in the computation state and that they contain int values.

The hypothesis that the old expression does not return an error is generated only if the old expression may actually return an error, which is indicated by the boolean flag passed as input. This possbility of returning an error or not is with respect to the hypotheses about the variables in vars mentioned above.

The hints to prove the theorem are passed as input too, since the proof generally varies depending on the kind of expression.

Definitions and Theorems

Function: simpadd0-gen-expr-pure-thm

(defun simpadd0-gen-expr-pure-thm
       (old new falliblep
            vars const-new thm-index hints)
 (declare (xargs :guard (and (exprp old)
                             (exprp new)
                             (booleanp falliblep)
                             (ident-setp vars)
                             (symbolp const-new)
                             (posp thm-index)
                             (true-listp hints))))
 (declare (xargs :guard (and (expr-unambp old)
                             (expr-unambp new))))
 (let ((__function__ 'simpadd0-gen-expr-pure-thm))
  (declare (ignorable __function__))
  (b*
   ((old (expr-fix old))
    (new (expr-fix new))
    ((unless (c$::expr-pure-formalp old))
     (raise "Internal error: ~x0 is not in the formalized subset."
            old)
     (mv '(_) nil 1))
    (equalp (equal old new))
    ((unless (or equalp (c$::expr-pure-formalp new)))
     (raise "Internal error: ~x0 is not in the formalized subset."
            new)
     (mv '(_) nil 1))
    (hyps (simpadd0-gen-var-hyps vars))
    (formula
     (if equalp
      (cons
       'b*
       (cons
        (cons
         (cons
          'expr
          (cons
           (cons
               'mv-nth
               (cons '1
                     (cons (cons 'c$::ldm-expr
                                 (cons (cons 'quote (cons old 'nil))
                                       'nil))
                           'nil)))
           'nil))
         '((expr-result (c::exec-expr-pure expr compst))
           (expr-value (c::expr-value->value expr-result))))
        (cons
         (cons
          'implies
          (cons
              (cons 'and
                    (append hyps
                            (and falliblep
                                 '((not (c::errorp expr-result))))))
              '((equal (c::value-kind expr-value)
                       :sint))))
         'nil)))
      (cons
       'b*
       (cons
        (cons
         (cons
          'old-expr
          (cons
           (cons
               'mv-nth
               (cons '1
                     (cons (cons 'c$::ldm-expr
                                 (cons (cons 'quote (cons old 'nil))
                                       'nil))
                           'nil)))
           'nil))
         (cons
          (cons
           'new-expr
           (cons
            (cons
               'mv-nth
               (cons '1
                     (cons (cons 'c$::ldm-expr
                                 (cons (cons 'quote (cons new 'nil))
                                       'nil))
                           'nil)))
            'nil))
          '((old-result (c::exec-expr-pure old-expr compst))
            (new-result (c::exec-expr-pure new-expr compst))
            (old-value (c::expr-value->value old-result))
            (new-value (c::expr-value->value new-result)))))
        (cons
         (cons
          'implies
          (cons
               (cons 'and
                     (append hyps
                             (and falliblep
                                  '((not (c::errorp old-result))))))
               '((and (equal old-value new-value)
                      (equal (c::value-kind old-value)
                             :sint)))))
         'nil)))))
    (thm-name (packn-pos (list const-new '-thm- thm-index)
                         const-new))
    (thm-index (1+ (pos-fix thm-index)))
    (thm-event
         (cons 'defthmd
               (cons thm-name
                     (cons formula
                           (cons ':hints (cons hints 'nil)))))))
   (mv thm-event thm-name thm-index))))

Theorem: pseudo-event-formp-of-simpadd0-gen-expr-pure-thm.thm-event

(defthm pseudo-event-formp-of-simpadd0-gen-expr-pure-thm.thm-event
 (b* (((mv ?thm-event ?thm-name ?updated-thm-index)
       (simpadd0-gen-expr-pure-thm old new falliblep
                                   vars const-new thm-index hints)))
   (pseudo-event-formp thm-event))
 :rule-classes :rewrite)

Theorem: symbolp-of-simpadd0-gen-expr-pure-thm.thm-name

(defthm symbolp-of-simpadd0-gen-expr-pure-thm.thm-name
 (b* (((mv ?thm-event ?thm-name ?updated-thm-index)
       (simpadd0-gen-expr-pure-thm old new falliblep
                                   vars const-new thm-index hints)))
   (symbolp thm-name))
 :rule-classes :rewrite)

Theorem: posp-of-simpadd0-gen-expr-pure-thm.updated-thm-index

(defthm posp-of-simpadd0-gen-expr-pure-thm.updated-thm-index
 (b* (((mv ?thm-event ?thm-name ?updated-thm-index)
       (simpadd0-gen-expr-pure-thm old new falliblep
                                   vars const-new thm-index hints)))
   (posp updated-thm-index))
 :rule-classes :rewrite)

Theorem: simpadd0-gen-expr-pure-thm-of-expr-fix-old

(defthm simpadd0-gen-expr-pure-thm-of-expr-fix-old
  (equal
       (simpadd0-gen-expr-pure-thm (expr-fix old)
                                   new falliblep
                                   vars const-new thm-index hints)
       (simpadd0-gen-expr-pure-thm old new falliblep
                                   vars const-new thm-index hints)))

Theorem: simpadd0-gen-expr-pure-thm-expr-equiv-congruence-on-old

(defthm simpadd0-gen-expr-pure-thm-expr-equiv-congruence-on-old
 (implies
  (c$::expr-equiv old old-equiv)
  (equal
       (simpadd0-gen-expr-pure-thm old new falliblep
                                   vars const-new thm-index hints)
       (simpadd0-gen-expr-pure-thm old-equiv new falliblep
                                   vars const-new thm-index hints)))
 :rule-classes :congruence)

Theorem: simpadd0-gen-expr-pure-thm-of-expr-fix-new

(defthm simpadd0-gen-expr-pure-thm-of-expr-fix-new
  (equal
       (simpadd0-gen-expr-pure-thm old (expr-fix new)
                                   falliblep
                                   vars const-new thm-index hints)
       (simpadd0-gen-expr-pure-thm old new falliblep
                                   vars const-new thm-index hints)))

Theorem: simpadd0-gen-expr-pure-thm-expr-equiv-congruence-on-new

(defthm simpadd0-gen-expr-pure-thm-expr-equiv-congruence-on-new
 (implies
  (c$::expr-equiv new new-equiv)
  (equal
       (simpadd0-gen-expr-pure-thm old new falliblep
                                   vars const-new thm-index hints)
       (simpadd0-gen-expr-pure-thm old new-equiv falliblep
                                   vars const-new thm-index hints)))
 :rule-classes :congruence)