Filtering...

gify-thms

books/centaur/gl/gify-thms
other
(in-package "GL")
other
(include-book "std/basic/two-nats-measure" :dir :system)
other
(include-book "generic-geval")
other
(include-book "gtypes")
other
(include-book "general-objects")
other
(include-book "gl-mbe")
other
(local (include-book "gtype-thms"))
other
(local (include-book "general-object-thms"))
other
(local (include-book "hyp-fix"))
other
(defthm mk-g-ite-correct
  (equal (generic-geval (mk-g-ite c x y) b)
    (if (generic-geval c b)
      (generic-geval x b)
      (generic-geval y b))))
other
(defthm mk-g-boolean-correct
  (equal (generic-geval (mk-g-boolean x) env)
    (bfr-eval x (car env)))
  :hints (("Goal" :in-theory (enable mk-g-boolean))))
other
(defthm mk-g-concrete-correct
  (equal (generic-geval (mk-g-concrete x) b)
    x))
other
(defthm g-concrete-quote-correct
  (equal (generic-geval (g-concrete-quote x) b)
    x)
  :hints (("Goal" :in-theory (enable eval-concrete-gobjectp
       concrete-gobjectp-def
       g-concrete-quote))))
other
(defthm generic-geval-gl-cons
  (equal (generic-geval (gl-cons x y) env)
    (cons (generic-geval x env)
      (generic-geval y env))))
other
(defthm generic-geval-list-gl-cons
  (equal (generic-geval-list (gl-cons x y) env)
    (cons (generic-geval x env)
      (generic-geval-list y env)))
  :hints (("Goal" :expand ((:free (x)
        (generic-geval-list (cons x y) env))))))
other
(defthm generic-geval-list-atom
  (implies (not (consp x))
    (equal (generic-geval-list x env) nil))
  :hints (("Goal" :expand ((generic-geval-list x env))))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))
other
(defthm generic-geval-g-apply
  (implies (not (equal fn 'quote))
    (equal (generic-geval (g-apply fn args) env)
      (generic-geval-ev (cons fn
          (kwote-lst (generic-geval-list args env)))
        nil)))
  :hints (("goal" :expand ((generic-geval (g-apply fn args) env))
     :in-theory (enable generic-geval-apply))))
other
(defthm generic-geval-nil
  (equal (generic-geval nil env) nil))
other
(defthm generic-geval-non-cons
  (implies (not (consp x))
    (equal (generic-geval x env) x))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))
other
(defthmd general-concrete-obj-correct
  (implies (general-concretep x)
    (equal (generic-geval x env)
      (general-concrete-obj x))))
other
(defthm natp-of-nfix (natp (nfix x)))
other
(defthm nfix-natp
  (implies (natp n)
    (equal (nfix n) n))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))
other
(def-ruleset! generic-geval-g-correct-lemmas
  '(generic-geval-gl-cons generic-geval-nil
    generic-geval-g-apply
    generic-geval-list-gl-cons
    generic-geval-list-atom
    mk-g-ite-correct
    mk-g-boolean-correct
    mk-g-concrete-correct
    g-concrete-quote-correct
    general-concrete-obj-correct))
other
(def-ruleset! g-correct-lemmas
  '(bfr-eval-bfr-binary-and bfr-eval-bfr-binary-or
    bfr-eval-bfr-not
    gl-aside
    gl-error-is-nil
    bfr-equiv-is-an-equivalence
    bfr-equiv-implies-equal-bfr-eval-1
    bfr-and-of-nil
    bfr-or-of-t
    (g-keyword-symbolp)
    gl-aside
    gl-error-is-nil))
other
(def-ruleset! g-guard-lemmas
  '(natp-compound-recognizer natp-of-nfix
    gl-aside
    gl-error-is-nil
    bfr-and-of-nil
    bfr-or-of-t
    (g-keyword-symbolp)
    gl-aside
    gl-error-is-nil))
other
(defthmd <-asym (not (< a a)))
other
(def-ruleset! clk-measure-rules
  '((:compound-recognizer natp-compound-recognizer) (:compound-recognizer zp-compound-recognizer)
    (:definition nfix)
    (:definition not)
    (:executable-counterpart <)
    (:executable-counterpart eql)
    (:executable-counterpart equal)
    (:executable-counterpart if)
    (:executable-counterpart nfix)
    (:rewrite <-asym)
    (:rewrite nfix-natp)
    (:rewrite o-p-of-two-nats-measure)
    (:rewrite o<-of-two-nats-measure)))