		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Abstract-syntax-anno-additional-theroems

Additional theorems about the annotation predicates.

These are in addition to the ones generated by fty::deffold-reduce. These are needed for actual proofs involving the annotation predicates. In particular, fty::deffold-reduce does not generate theorems for constructs in the :override input; so we must supply theorems for those cases.

Definitions and Theorems

Theorem: iconst-annop-of-iconst

(defthm iconst-annop-of-iconst
  (equal (iconst-annop (iconst core suffix? info))
         (iconst-infop info)))

Theorem: expr-annop-of-expr-ident

(defthm expr-annop-of-expr-ident
  (equal (expr-annop (expr-ident ident info))
         (var-infop info)))

Theorem: expr-annop-of-expr-const

(defthm expr-annop-of-expr-const
  (equal (expr-annop (expr-const const info))
         (and (const-annop const)
              (expr-const-infop info))))

Theorem: expr-annop-of-expr-string

(defthm expr-annop-of-expr-string
  (equal (expr-annop (expr-string strings info))
         (expr-string-infop info)))

Theorem: expr-annop-of-expr-arrsub

(defthm expr-annop-of-expr-arrsub
  (equal (expr-annop (expr-arrsub arg1 arg2 info))
         (and (expr-annop arg1)
              (expr-annop arg2)
              (expr-arrsub-infop info))))

Theorem: expr-annop-of-expr-funcall

(defthm expr-annop-of-expr-funcall
  (equal (expr-annop (expr-funcall fun args info))
         (and (expr-annop fun)
              (expr-list-annop args)
              (expr-funcall-infop info))))

Theorem: expr-annop-of-expr-unary

(defthm expr-annop-of-expr-unary
  (equal (expr-annop (expr-unary op arg info))
         (and (expr-annop arg)
              (expr-unary-infop info))))

Theorem: expr-annop-of-expr-binary

(defthm expr-annop-of-expr-binary
  (equal (expr-annop (expr-binary op arg1 arg2 info))
         (and (expr-annop arg1)
              (expr-annop arg2)
              (expr-binary-infop info))))

Theorem: tyname-annop-of-tyname

(defthm tyname-annop-of-tyname
  (equal (tyname-annop (tyname specquals declor? info))
         (and (spec/qual-list-annop specquals)
              (absdeclor-option-annop declor?)
              (tyname-infop info))))

Theorem: param-declor-annop-of-param-declor-nonabstract

(defthm param-declor-annop-of-param-declor-nonabstract
  (equal (param-declor-annop (param-declor-nonabstract declor info))
         (and (declor-annop declor)
              (param-declor-nonabstract-infop info))))

Theorem: init-declor-annop-of-init-declor

(defthm init-declor-annop-of-init-declor
 (equal
  (init-declor-annop (init-declor declor asm? attribs initer? info))
  (and (declor-annop declor)
       (initer-option-annop initer?)
       (init-declor-infop info))))

Theorem: fundef-annop-of-fundef

(defthm fundef-annop-of-fundef
  (equal
       (fundef-annop (fundef extension specs
                             declor asm? attribs declons body info))
       (and (decl-spec-list-annop specs)
            (declor-annop declor)
            (declon-list-annop declons)
            (comp-stmt-annop body)
            (fundef-infop info))))

Theorem: transunit-annop-of-transunit

(defthm transunit-annop-of-transunit
  (equal (transunit-annop (transunit declons info))
         (and (ext-declon-list-annop declons)
              (transunit-infop info))))

Theorem: iconst-infop-of-iconst->info

(defthm iconst-infop-of-iconst->info
  (implies (iconst-annop iconst)
           (iconst-infop (iconst->info iconst))))

Theorem: var-infop-of-expr-ident->info

(defthm var-infop-of-expr-ident->info
  (implies (and (expr-annop expr)
                (expr-case expr :ident))
           (var-infop (expr-ident->info expr))))

Theorem: const-annop-of-expr-const->const

(defthm const-annop-of-expr-const->const
  (implies (and (expr-annop expr)
                (expr-case expr :const))
           (const-annop (expr-const->const expr))))

Theorem: expr-const-infop-of-expr-const->info

(defthm expr-const-infop-of-expr-const->info
  (implies (and (expr-annop expr)
                (expr-case expr :const))
           (expr-const-infop (expr-const->info expr))))

Theorem: expr-string-infop-of-expr-string->info

(defthm expr-string-infop-of-expr-string->info
  (implies (and (expr-annop expr)
                (expr-case expr :string))
           (expr-string-infop (expr-string->info expr))))

Theorem: expr-annop-of-expr-arrsub->arg1

(defthm expr-annop-of-expr-arrsub->arg1
  (implies (and (expr-annop expr)
                (expr-case expr :arrsub))
           (expr-annop (expr-arrsub->arg1 expr))))

Theorem: expr-annop-of-expr-arrsub->arg2

(defthm expr-annop-of-expr-arrsub->arg2
  (implies (and (expr-annop expr)
                (expr-case expr :arrsub))
           (expr-annop (expr-arrsub->arg2 expr))))

Theorem: expr-arrsub-infop-of-expr-arrsub->info

(defthm expr-arrsub-infop-of-expr-arrsub->info
  (implies (and (expr-annop expr)
                (expr-case expr :arrsub))
           (expr-arrsub-infop (expr-arrsub->info expr))))

Theorem: expr-annop-of-expr-funcall->fun

(defthm expr-annop-of-expr-funcall->fun
  (implies (and (expr-annop expr)
                (expr-case expr :funcall))
           (expr-annop (expr-funcall->fun expr))))

Theorem: expr-list-annop-of-expr-funcall->args

(defthm expr-list-annop-of-expr-funcall->args
  (implies (and (expr-annop expr)
                (expr-case expr :funcall))
           (expr-list-annop (expr-funcall->args expr))))

Theorem: expr-funcall-infop-of-expr-funcall->info

(defthm expr-funcall-infop-of-expr-funcall->info
  (implies (and (expr-annop expr)
                (expr-case expr :funcall))
           (expr-funcall-infop (expr-funcall->info expr))))

Theorem: expr-annop-of-expr-unary->arg

(defthm expr-annop-of-expr-unary->arg
  (implies (and (expr-annop expr)
                (expr-case expr :unary))
           (expr-annop (expr-unary->arg expr))))

Theorem: expr-unary-infop-of-expr-unary->info

(defthm expr-unary-infop-of-expr-unary->info
  (implies (and (expr-annop expr)
                (expr-case expr :unary))
           (expr-unary-infop (expr-unary->info expr))))

Theorem: expr-annop-of-expr-binary->arg1

(defthm expr-annop-of-expr-binary->arg1
  (implies (and (expr-annop expr)
                (expr-case expr :binary))
           (expr-annop (expr-binary->arg1 expr))))

Theorem: expr-annop-of-expr-binary->arg2

(defthm expr-annop-of-expr-binary->arg2
  (implies (and (expr-annop expr)
                (expr-case expr :binary))
           (expr-annop (expr-binary->arg2 expr))))

Theorem: expr-binary-infop-of-expr-binary->info

(defthm expr-binary-infop-of-expr-binary->info
  (implies (and (expr-annop expr)
                (expr-case expr :binary))
           (expr-binary-infop (expr-binary->info expr))))

Theorem: declor-annop-of-init-declor->declor

(defthm declor-annop-of-init-declor->declor
  (implies (init-declor-annop init-declor)
           (declor-annop (init-declor->declor init-declor))))

Theorem: initer-option-annop-of-init-declor->initer?

(defthm initer-option-annop-of-init-declor->initer?
 (implies (init-declor-annop init-declor)
          (initer-option-annop (init-declor->initer? init-declor))))

Theorem: init-declor-infop-of-init-declor->info

(defthm init-declor-infop-of-init-declor->info
  (implies (init-declor-annop init-declor)
           (init-declor-infop (init-declor->info init-declor))))

Theorem: spec/qual-list-annop-of-tyname->specquals

(defthm spec/qual-list-annop-of-tyname->specquals
  (implies (tyname-annop tyname)
           (spec/qual-list-annop (tyname->specquals tyname))))

Theorem: absdeclor-option-annop-of-tyname->declor?

(defthm absdeclor-option-annop-of-tyname->declor?
  (implies (tyname-annop tyname)
           (absdeclor-option-annop (tyname->declor? tyname))))

Theorem: tyname-infop-of-tyname->info

(defthm tyname-infop-of-tyname->info
  (implies (tyname-annop tyname)
           (tyname-infop (tyname->info tyname))))

Theorem: declor-annop-of-param-declor-nonabstract->declor

(defthm declor-annop-of-param-declor-nonabstract->declor
 (implies
    (and (param-declor-annop param-declor)
         (param-declor-case param-declor :nonabstract))
    (declor-annop (param-declor-nonabstract->declor param-declor))))

Theorem: param-declor-nonabstract-infop-of-param-declor-nonabstract->info

(defthm
   param-declor-nonabstract-infop-of-param-declor-nonabstract->info
  (implies (and (param-declor-annop param-declor)
                (param-declor-case param-declor :nonabstract))
           (param-declor-nonabstract-infop
                (param-declor-nonabstract->info param-declor))))

Theorem: decl-spec-list-annop-of-fundef->specs

(defthm decl-spec-list-annop-of-fundef->specs
  (implies (fundef-annop fundef)
           (decl-spec-list-annop (fundef->specs fundef))))

Theorem: declor-annop-of-fundef->declor

(defthm declor-annop-of-fundef->declor
  (implies (fundef-annop fundef)
           (declor-annop (fundef->declor fundef))))

Theorem: declon-list-annop-of-fundef->declons

(defthm declon-list-annop-of-fundef->declons
  (implies (fundef-annop fundef)
           (declon-list-annop (fundef->declons fundef))))

Theorem: comp-stmt-annop-of-fundef->body

(defthm comp-stmt-annop-of-fundef->body
  (implies (fundef-annop fundef)
           (comp-stmt-annop (fundef->body fundef))))

Theorem: fundef-infop-of-fundef->info

(defthm fundef-infop-of-fundef->info
  (implies (fundef-annop fundef)
           (fundef-infop (fundef->info fundef))))

Theorem: ext-declon-list-annop-of-transunit->declons

(defthm ext-declon-list-annop-of-transunit->declons
  (implies (transunit-annop transunit)
           (ext-declon-list-annop (transunit->declons transunit))))

Theorem: transunit-infop-of-transunit->info

(defthm transunit-infop-of-transunit->info
  (implies (transunit-annop transunit)
           (transunit-infop (transunit->info transunit))))

Theorem: transunit-ensemble-annop-of-irr-transunit-ensemble

(defthm transunit-ensemble-annop-of-irr-transunit-ensemble
  (transunit-ensemble-annop (irr-transunit-ensemble)))

Theorem: code-ensemble-annop-of-irr-code-ensemble

(defthm code-ensemble-annop-of-irr-code-ensemble
  (code-ensemble-annop (irr-code-ensemble)))