		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-expr-asg-thm

Generate a theorem for the transformation of an assignment expression.

Signature
(simpadd0-gen-expr-asg-thm old new vartys const-new thm-index hints) → (mv thm-event thm-name updated-thm-index)
Arguments: old — Guard (exprp old).; new — Guard (exprp new).; vartys — Guard (ident-type-mapp vartys).; 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 only applies to simple assignments whose left side is a variable expression var and whose old and new right sides are pure expressions. The caller of this function checks that that is the case; here we double-check these conditions, and throw a hard error if they are not satisfied, because that should never happen.

If the two expressions are syntactically equal, we generate a dummy theorem. At this point we do not seem to need any actual theorem for this case, but we want proof generation to proceed after this expression, so we generate a theorem for uniformity, so that code for larger constructs can uniformly check whether a theorem was generated for this construct.

If the two expressions are syntactically unequal, the theorem says that if the old assignment expression does not cause an error, neither does the new assignment expression, and the two return the same updated computation state.

Definitions and Theorems

Function: simpadd0-gen-expr-asg-thm

(defun simpadd0-gen-expr-asg-thm
       (old new vartys const-new thm-index hints)
 (declare (xargs :guard (and (exprp old)
                             (exprp new)
                             (ident-type-mapp vartys)
                             (symbolp const-new)
                             (posp thm-index)
                             (true-listp hints))))
 (declare (xargs :guard (and (expr-unambp old)
                             (expr-unambp new))))
 (let ((__function__ 'simpadd0-gen-expr-asg-thm))
  (declare (ignorable __function__))
  (b*
   ((old (expr-fix old))
    (new (expr-fix new))
    ((unless (expr-asg-formalp old))
     (raise "Internal error: ~x0 is not in the formalized subset."
            old)
     (mv '(_) nil 1))
    ((unless (expr-asg-formalp new))
     (raise "Internal error: ~x0 is not in the formalized subset."
            new)
     (mv '(_) nil 1))
    ((unless (and (expr-case old :binary)
                  (binop-case (expr-binary->op old)
                              :asg)))
     (raise "Internal error: ~x0 is not an assignment expression."
            old)
     (mv '(_) nil 1))
    (old-left (expr-binary->arg1 old))
    (old-right (expr-binary->arg2 old))
    ((unless (expr-case old-left :ident))
     (raise "Internal error: ~x0 is not a variable."
            old-left)
     (mv '(_) nil 1))
    ((unless (expr-purep old-right))
     (raise "Internal error: ~x0 is not a pure expression."
            old-right)
     (mv '(_) nil 1))
    ((unless (and (expr-case new :binary)
                  (binop-case (expr-binary->op new)
                              :asg)))
     (raise "Internal error: ~x0 is not an assignment expression."
            new)
     (mv '(_) nil 1))
    (new-left (expr-binary->arg1 new))
    (new-right (expr-binary->arg2 new))
    ((unless (equal new-left old-left))
     (raise "Internal error: ~x0 and ~x1 differ."
            old-left new-left)
     (mv '(_) nil 1))
    ((unless (expr-purep new-right))
     (raise "Internal error: ~x0 is not a pure expression."
            new-right)
     (mv '(_) nil 1))
    (hyps (simpadd0-gen-var-hyps vartys))
    (thm-name (packn-pos (list const-new '-thm- thm-index)
                         const-new))
    (thm-index (1+ (pos-fix thm-index)))
    (formula
     (cons
      'b*
      (cons
       (cons
        (cons
         'old-expr
         (cons
          (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-expr
                                 (cons (cons 'quote (cons old 'nil))
                                       'nil))
                           'nil)))
          'nil))
        (cons
         (cons
          'new-expr
          (cons
           (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-expr
                                 (cons (cons 'quote (cons new 'nil))
                                       'nil))
                           'nil)))
           'nil))
         '((old-compst
                (c::exec-expr-asg old-expr compst old-fenv limit))
           (new-compst
               (c::exec-expr-asg new-expr compst new-fenv limit)))))
       (cons
        (cons
          'implies
          (cons (cons 'and
                      (append hyps '((not (c::errorp old-compst)))))
                '((and (not (c::errorp new-compst))
                       (equal old-compst new-compst)))))
        'nil))))
    (thm-event
         (if (equal old-right new-right)
             (cons 'defthm
                   (cons thm-name '(t :rule-classes nil)))
           (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-asg-thm.thm-event

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

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

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

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

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

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

(defthm simpadd0-gen-expr-asg-thm-of-expr-fix-old
 (equal
  (simpadd0-gen-expr-asg-thm (expr-fix old)
                             new vartys const-new thm-index hints)
  (simpadd0-gen-expr-asg-thm old
                             new vartys const-new thm-index hints)))

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

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

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

(defthm simpadd0-gen-expr-asg-thm-of-expr-fix-new
 (equal
  (simpadd0-gen-expr-asg-thm old (expr-fix new)
                             vartys const-new thm-index hints)
  (simpadd0-gen-expr-asg-thm old
                             new vartys const-new thm-index hints)))

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

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