glcp-geval-thms

(in-package "GL")

(include-book "glcp-geval")

(include-book "gtype-thms")

(include-book "gtests")

(include-book "general-object-thms")

(local (defthmd gl-eval-of-atom
    (implies (atom x)
      (equal (generic-geval x env) x))
    :hints (("goal" :in-theory (enable tag)
       :expand ((generic-geval x env))))
    :rule-classes ((:rewrite :backchain-limit-lst 0))))

(defmacro def-glcp-generic-geval-thm-instance
  (new-name orig-name
    &key
    (rule-classes 'nil rule-classes-p))
  `(def-functional-instance ,GL::NEW-NAME
    ,GL::ORIG-NAME
    ((generic-geval-ev glcp-generic-geval-ev) (generic-geval-ev-lst glcp-generic-geval-ev-lst)
      (generic-geval glcp-generic-geval)
      (generic-geval-list glcp-generic-geval-list))
    :hints ('(:in-theory (e/d* (glcp-generic-geval-ev-of-fncall-args glcp-generic-geval-apply-agrees-with-glcp-generic-geval-ev)
         (glcp-generic-geval-apply))
       :expand ((:with glcp-generic-geval
          (glcp-generic-geval x env)) (glcp-generic-geval-list x env)))) . ,(AND GL::RULE-CLASSES-P `(:RULE-CLASSES ,GL::RULE-CLASSES))))

(defsection glcp-generic-geval
  (local (in-theory (enable glcp-generic-geval)))
  (defthm glcp-generic-geval-atom
    (implies (atom x)
      (equal (glcp-generic-geval x env) x))
    :hints (("Goal" :in-theory (enable gl-eval-of-atom)))
    :rule-classes ((:rewrite :backchain-limit-lst 0)))
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-mk-g-boolean-correct
    mk-g-boolean-correct)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-mk-g-integer-correct
    mk-g-integer-correct)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-cons
    generic-geval-cons)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-g-apply-p
    generic-geval-g-apply-p)
  (in-theory (disable glcp-generic-geval-g-apply-p))
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-mk-g-ite-correct
    mk-g-ite-correct)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-mk-g-concrete-correct
    mk-g-concrete-correct)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-g-concrete-quote-correct
    g-concrete-quote-correct)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-general-concrete-obj-correct
    general-concrete-obj-correct)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-of-gl-cons
    generic-geval-gl-cons)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-g-apply
    generic-geval-g-apply)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-alt-def
    generic-geval-alt-def
    :rule-classes ((:definition :clique (glcp-generic-geval))))
  (in-theory (disable glcp-generic-geval-alt-def))
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-general-consp-car-correct
    general-consp-car-correct)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-general-consp-correct
    general-consp-correct)
  (in-theory (disable glcp-generic-geval-general-consp-correct))
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-general-consp-cdr-correct
    general-consp-cdr-correct)
  (def-glcp-generic-geval-thm-instance glcp-generic-geval-consp-general-consp
    consp-general-consp)
  (in-theory (disable glcp-generic-geval-general-consp-cdr-correct
      glcp-generic-geval-general-consp-car-correct
      glcp-generic-geval-consp-general-consp))
  (def-glcp-generic-geval-thm-instance bfr-assume-of-gtests-possibly-true-for-glcp-generic-geval
    bfr-assume-of-gtests-possibly-true)
  (def-glcp-generic-geval-thm-instance bfr-assume-of-gtests-possibly-false-for-glcp-generic-geval
    bfr-assume-of-gtests-possibly-false))

(defsection glcp-generic-geval-list
  (local (in-theory (enable glcp-generic-geval-list)))
  (defthm glcp-generic-geval-list-of-cons
    (equal (glcp-generic-geval-list (cons a b) env)
      (cons (glcp-generic-geval a env)
        (glcp-generic-geval-list b env))))
  (defthm glcp-generic-geval-list-of-atom
    (implies (not (consp x))
      (equal (glcp-generic-geval-list x env) nil))
    :rule-classes ((:rewrite :backchain-limit-lst 0)))
  (defthm glcp-generic-geval-list-of-gl-cons
    (equal (glcp-generic-geval-list (gl-cons x y)
        env)
      (cons (glcp-generic-geval x env)
        (glcp-generic-geval-list y env)))
    :hints (("Goal" :in-theory (e/d (gl-cons)
         (glcp-generic-geval-alt-def glcp-generic-geval-general-concrete-obj-correct))
       :expand ((:with glcp-generic-geval
          (glcp-generic-geval x env)) (:with glcp-generic-geval
           (glcp-generic-geval (g-concrete x) env))))))
  (defthm len-of-glcp-generic-geval-list
    (equal (len (glcp-generic-geval-list x env))
      (len x))))