		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-expr-cond

Transform a conditional expression.

Signature
(simpadd0-expr-cond test test-new test-events test-thm-name test-vartys test-diffp then then-new then-events then-thm-name then-vartys then-diffp else else-new else-events else-thm-name else-vartys else-diffp gin) → (mv expr gou)
Arguments: test — Guard (exprp test).; test-new — Guard (exprp test-new).; test-events — Guard (pseudo-event-form-listp test-events).; test-thm-name — Guard (symbolp test-thm-name).; test-vartys — Guard (ident-type-mapp test-vartys).; test-diffp — Guard (booleanp test-diffp).; then — Guard (expr-optionp then).; then-new — Guard (expr-optionp then-new).; then-events — Guard (pseudo-event-form-listp then-events).; then-thm-name — Guard (symbolp then-thm-name).; then-vartys — Guard (ident-type-mapp then-vartys).; then-diffp — Guard (booleanp then-diffp).; else — Guard (exprp else).; else-new — Guard (exprp else-new).; else-events — Guard (pseudo-event-form-listp else-events).; else-thm-name — Guard (symbolp else-thm-name).; else-vartys — Guard (ident-type-mapp else-vartys).; else-diffp — Guard (booleanp else-diffp).; gin — Guard (simpadd0-ginp gin).
Returns: expr — Type (exprp expr).; gou — Type (simpadd0-goutp gou).

The resulting expression is obtained by combining the possibly transformed argument expression.

We generate a theorem iff a theorem was generated for the argument expressions. The theorem is proved via a few general ones that we prove below. These are a bit more complicated than for strict expressions, because conditional expressions are non-strict: the branch not taken could return an error while the conditional expression does not.

Definitions and Theorems

Function: simpadd0-expr-cond

(defun simpadd0-expr-cond
       (test test-new
             test-events test-thm-name test-vartys
             test-diffp then then-new then-events
             then-thm-name then-vartys then-diffp
             else else-new else-events else-thm-name
             else-vartys else-diffp gin)
 (declare (xargs :guard (and (exprp test)
                             (exprp test-new)
                             (pseudo-event-form-listp test-events)
                             (symbolp test-thm-name)
                             (ident-type-mapp test-vartys)
                             (booleanp test-diffp)
                             (expr-optionp then)
                             (expr-optionp then-new)
                             (pseudo-event-form-listp then-events)
                             (symbolp then-thm-name)
                             (ident-type-mapp then-vartys)
                             (booleanp then-diffp)
                             (exprp else)
                             (exprp else-new)
                             (pseudo-event-form-listp else-events)
                             (symbolp else-thm-name)
                             (ident-type-mapp else-vartys)
                             (booleanp else-diffp)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (and (expr-unambp test)
                             (expr-unambp test-new)
                             (expr-option-unambp then)
                             (expr-option-unambp then-new)
                             (expr-unambp else)
                             (expr-unambp else-new))))
 (let ((__function__ 'simpadd0-expr-cond))
  (declare (ignorable __function__))
  (b*
   (((simpadd0-gin gin) gin)
    (expr (make-expr-cond :test test
                          :then then
                          :else else))
    (expr-new (make-expr-cond :test test-new
                              :then then-new
                              :else else-new))
    (test-vartys (ident-type-map-fix test-vartys))
    (then-vartys (ident-type-map-fix then-vartys))
    (else-vartys (ident-type-map-fix else-vartys))
    ((unless (omap::compatiblep then-vartys else-vartys))
     (raise
      "Internal error: ~
                incompatible variable-type maps ~x0 and ~x1."
      then-vartys else-vartys)
     (mv (irr-expr) (irr-simpadd0-gout)))
    (vartys (omap::update* then-vartys else-vartys))
    ((unless (omap::compatiblep test-vartys vartys))
     (raise
      "Internal error: ~
                incompatible variable-type maps ~x0 and ~x1."
      test-vartys vartys)
     (mv (irr-expr) (irr-simpadd0-gout)))
    (vartys (omap::update* test-vartys vartys))
    (diffp (or test-diffp then-diffp else-diffp))
    ((unless (and test-thm-name
                  then-thm-name else-thm-name))
     (mv expr-new
         (make-simpadd0-gout
              :events (append test-events then-events else-events)
              :thm-name nil
              :thm-index gin.thm-index
              :names-to-avoid gin.names-to-avoid
              :vartys vartys
              :diffp diffp)))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e ldm-expr)
            (:e ldm-ident)
            (:e ident)
            (:e c::expr-cond)
            (:e c::type-nonchar-integerp))
         (cons
          ':use
          (cons
           (cons
            test-thm-name
            (cons
             then-thm-name
             (cons
              else-thm-name
              (cons
               (cons
                ':instance
                (cons
                 'simpadd0-expr-cond-support-lemma-1
                 (cons
                  (cons
                   'old-test
                   (cons
                    (cons
                     'mv-nth
                     (cons
                      '1
                      (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons test 'nil))
                                      'nil))
                          'nil)))
                    'nil))
                  (cons
                   (cons
                    'old-then
                    (cons
                     (cons
                      'mv-nth
                      (cons
                       '1
                       (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons then 'nil))
                                      'nil))
                          'nil)))
                     'nil))
                   (cons
                    (cons
                     'old-else
                     (cons
                      (cons
                       'mv-nth
                       (cons
                        '1
                        (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons else 'nil))
                                      'nil))
                          'nil)))
                      'nil))
                    (cons
                     (cons
                      'new-test
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons
                            'ldm-expr
                            (cons (cons 'quote (cons test-new 'nil))
                                  'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'new-then
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                            'ldm-expr
                            (cons (cons 'quote (cons then-new 'nil))
                                  'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'new-else
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                             'ldm-expr
                             (cons
                                  (cons 'quote (cons else-new 'nil))
                                  'nil))
                            'nil)))
                         'nil))
                       'nil))))))))
               (cons
                (cons
                 ':instance
                 (cons
                  'simpadd0-expr-cond-support-lemma-2
                  (cons
                   (cons
                    'old-test
                    (cons
                     (cons
                      'mv-nth
                      (cons
                       '1
                       (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons test 'nil))
                                      'nil))
                          'nil)))
                     'nil))
                   (cons
                    (cons
                     'old-then
                     (cons
                      (cons
                       'mv-nth
                       (cons
                        '1
                        (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons then 'nil))
                                      'nil))
                          'nil)))
                      'nil))
                    (cons
                     (cons
                      'old-else
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons else 'nil))
                                      'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'new-test
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                            'ldm-expr
                            (cons (cons 'quote (cons test-new 'nil))
                                  'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'new-then
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                             'ldm-expr
                             (cons
                                  (cons 'quote (cons then-new 'nil))
                                  'nil))
                            'nil)))
                         'nil))
                       (cons
                        (cons
                         'new-else
                         (cons
                          (cons
                           'mv-nth
                           (cons
                            '1
                            (cons
                             (cons
                              'ldm-expr
                              (cons
                                  (cons 'quote (cons else-new 'nil))
                                  'nil))
                             'nil)))
                          'nil))
                        'nil))))))))
                (cons
                 (cons
                  ':instance
                  (cons
                   'simpadd0-expr-cond-support-lemma-3
                   (cons
                    (cons
                     'test
                     (cons
                      (cons
                       'mv-nth
                       (cons
                        '1
                        (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons test 'nil))
                                      'nil))
                          'nil)))
                      'nil))
                    (cons
                     (cons
                      'then
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons then 'nil))
                                      'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'else
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons else 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      'nil)))))
                 (cons
                  (cons
                   ':instance
                   (cons
                    'simpadd0-expr-cond-support-lemma-4
                    (cons
                     (cons
                      'test
                      (cons
                       (cons
                        'mv-nth
                        (cons
                         '1
                         (cons
                          (cons 'ldm-expr
                                (cons (cons 'quote (cons test 'nil))
                                      'nil))
                          'nil)))
                       'nil))
                     (cons
                      (cons
                       'then
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons then 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'else
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                                'ldm-expr
                                (cons (cons 'quote (cons else 'nil))
                                      'nil))
                            'nil)))
                         'nil))
                       'nil)))))
                  (cons
                   (cons
                    ':instance
                    (cons
                     'simpadd0-expr-cond-support-lemma-5
                     (cons
                      (cons
                       'test
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons
                                'ldm-expr
                                (cons (cons 'quote (cons test 'nil))
                                      'nil))
                           'nil)))
                        'nil))
                      (cons
                       (cons
                        'then
                        (cons
                         (cons
                          'mv-nth
                          (cons
                           '1
                           (cons
                            (cons
                                'ldm-expr
                                (cons (cons 'quote (cons then 'nil))
                                      'nil))
                            'nil)))
                         'nil))
                       (cons
                        (cons
                         'else
                         (cons
                          (cons
                           'mv-nth
                           (cons
                            '1
                            (cons
                             (cons
                                'ldm-expr
                                (cons (cons 'quote (cons else 'nil))
                                      'nil))
                             'nil)))
                          'nil))
                        'nil)))))
                   'nil))))))))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (simpadd0-gen-expr-pure-thm
          expr expr-new vartys
          gin.const-new gin.thm-index hints)))
   (mv expr-new
       (make-simpadd0-gout
            :events (append test-events then-events
                            else-events (list thm-event))
            :thm-name thm-name
            :thm-index thm-index
            :names-to-avoid (cons thm-name gin.names-to-avoid)
            :vartys vartys
            :diffp diffp)))))

Theorem: exprp-of-simpadd0-expr-cond.expr

(defthm exprp-of-simpadd0-expr-cond.expr
  (b* (((mv ?expr ?gou)
        (simpadd0-expr-cond test test-new
                            test-events test-thm-name test-vartys
                            test-diffp then then-new then-events
                            then-thm-name then-vartys then-diffp
                            else else-new else-events else-thm-name
                            else-vartys else-diffp gin)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: simpadd0-goutp-of-simpadd0-expr-cond.gou

(defthm simpadd0-goutp-of-simpadd0-expr-cond.gou
  (b* (((mv ?expr ?gou)
        (simpadd0-expr-cond test test-new
                            test-events test-thm-name test-vartys
                            test-diffp then then-new then-events
                            then-thm-name then-vartys then-diffp
                            else else-new else-events else-thm-name
                            else-vartys else-diffp gin)))
    (simpadd0-goutp gou))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-simpadd0-expr-cond

(defthm expr-unambp-of-simpadd0-expr-cond
 (implies
   (and (expr-unambp test-new)
        (expr-option-unambp then-new)
        (expr-unambp else-new))
   (b* (((mv ?expr ?gou)
         (simpadd0-expr-cond test test-new
                             test-events test-thm-name test-vartys
                             test-diffp then then-new then-events
                             then-thm-name then-vartys then-diffp
                             else else-new else-events else-thm-name
                             else-vartys else-diffp gin)))
     (expr-unambp expr))))

Theorem: simpadd0-expr-cond-support-lemma-1

(defthm simpadd0-expr-cond-support-lemma-1
  (b* ((old (c::expr-cond old-test old-then old-else))
       (new (c::expr-cond new-test new-then new-else))
       (old-test-result (c::exec-expr-pure old-test compst))
       (old-then-result (c::exec-expr-pure old-then compst))
       (new-test-result (c::exec-expr-pure new-test compst))
       (new-then-result (c::exec-expr-pure new-then compst))
       (old-test-value (c::expr-value->value old-test-result))
       (old-then-value (c::expr-value->value old-then-result))
       (new-test-value (c::expr-value->value new-test-result))
       (new-then-value (c::expr-value->value new-then-result))
       (old-result (c::exec-expr-pure old compst))
       (new-result (c::exec-expr-pure new compst))
       (old-value (c::expr-value->value old-result))
       (new-value (c::expr-value->value new-result))
       (type-test (c::type-of-value old-test-value))
       (type-then (c::type-of-value old-then-value)))
    (implies (and (not (c::errorp old-result))
                  (not (c::errorp new-test-result))
                  (not (c::errorp new-then-result))
                  (equal old-test-value new-test-value)
                  (equal old-then-value new-then-value)
                  (c::type-nonchar-integerp type-test)
                  (c::type-nonchar-integerp type-then)
                  (c::test-value old-test-value))
             (and (not (c::errorp new-result))
                  (equal old-value new-value)
                  (equal (c::type-of-value old-value)
                         type-then)))))

Theorem: simpadd0-expr-cond-support-lemma-2

(defthm simpadd0-expr-cond-support-lemma-2
  (b* ((old (c::expr-cond old-test old-then old-else))
       (new (c::expr-cond new-test new-then new-else))
       (old-test-result (c::exec-expr-pure old-test compst))
       (old-else-result (c::exec-expr-pure old-else compst))
       (new-test-result (c::exec-expr-pure new-test compst))
       (new-else-result (c::exec-expr-pure new-else compst))
       (old-test-value (c::expr-value->value old-test-result))
       (old-else-value (c::expr-value->value old-else-result))
       (new-test-value (c::expr-value->value new-test-result))
       (new-else-value (c::expr-value->value new-else-result))
       (old-result (c::exec-expr-pure old compst))
       (new-result (c::exec-expr-pure new compst))
       (old-value (c::expr-value->value old-result))
       (new-value (c::expr-value->value new-result))
       (type-test (c::type-of-value old-test-value))
       (type-else (c::type-of-value old-else-value)))
    (implies (and (not (c::errorp old-result))
                  (not (c::errorp new-test-result))
                  (not (c::errorp new-else-result))
                  (equal old-test-value new-test-value)
                  (equal old-else-value new-else-value)
                  (c::type-nonchar-integerp type-test)
                  (c::type-nonchar-integerp type-else)
                  (not (c::test-value old-test-value)))
             (and (not (c::errorp new-result))
                  (equal old-value new-value)
                  (equal (c::type-of-value old-value)
                         type-else)))))

Theorem: simpadd0-expr-cond-support-lemma-3

(defthm simpadd0-expr-cond-support-lemma-3
  (implies
       (c::errorp (c::exec-expr-pure test compst))
       (c::errorp (c::exec-expr-pure (c::expr-cond test then else)
                                     compst))))

Theorem: simpadd0-expr-cond-support-lemma-4

(defthm simpadd0-expr-cond-support-lemma-4
 (implies
  (and
   (not (c::errorp (c::exec-expr-pure test compst)))
   (c::type-nonchar-integerp
       (c::type-of-value
            (c::expr-value->value (c::exec-expr-pure test compst))))
   (c::test-value
        (c::expr-value->value (c::exec-expr-pure test compst)))
   (c::errorp (c::exec-expr-pure then compst)))
  (c::errorp (c::exec-expr-pure (c::expr-cond test then else)
                                compst))))

Theorem: simpadd0-expr-cond-support-lemma-5

(defthm simpadd0-expr-cond-support-lemma-5
 (implies
  (and
   (not (c::errorp (c::exec-expr-pure test compst)))
   (c::type-nonchar-integerp
       (c::type-of-value
            (c::expr-value->value (c::exec-expr-pure test compst))))
   (not
       (c::test-value
            (c::expr-value->value (c::exec-expr-pure test compst))))
   (c::errorp (c::exec-expr-pure else compst)))
  (c::errorp (c::exec-expr-pure (c::expr-cond test then else)
                                compst))))