other
(in-package "GL")
other
(include-book "g-if")
other
(include-book "g-primitives-help")
other
(include-book "symbolic-arithmetic")
other
(include-book "eval-g-base")
other
(local (include-book "eval-g-base-help"))
other
(local (include-book "hyp-fix"))
other
(local (defthm nth-open-when-constant-idx (implies (syntaxp (quotep n)) (equal (nth n x) (if (zp n) (car x) (nth (1- n) (cdr x)))))))
other
(local (defthm eval-g-base-atom (implies (not (consp x)) (equal (eval-g-base x env) x)) :hints (("goal" :expand ((:with eval-g-base (eval-g-base x env))))) :rule-classes ((:rewrite :backchain-limit-lst 0))))
other
(program)
strip-correct-lemmasfunction
(defun strip-correct-lemmas (alist) (if (atom alist) nil (append (strip-cars (cddr (car alist))) (strip-correct-lemmas (cdr alist)))))
def-g-predicate-fnfunction
(defun def-g-predicate-fn (fn cases corr-hints guard-hints encap guard-encap corr-encap formals) (declare (xargs :mode :program)) (let* ((gfn (gl-fnsym fn)) (booleanp-thmname (incat 'foo (symbol-package-name fn) "::" (symbol-name fn) "-IS-BOOLEANP")) (x (car formals))) `(encapsulate nil (logic) (local (def-ruleset! g-correct-lemmas (strip-correct-lemmas (table-alist 'gl-function-info world)))) (def-g-fn ,GL::FN `(if (atom ,',GL::X) (gret (,',GL::FN ,',GL::X)) (pattern-match ,',GL::X ((g-concrete obj) (gret (,',GL::FN obj))) ((g-ite test then else) (if (zp clk) (gret (g-apply ',',GL::FN (list ,',GL::X))) (g-if (gret test) (,GL::GFN then . ,GL::PARAMS) (,GL::GFN else . ,GL::PARAMS)))) ((g-apply & &) (gret (g-apply ',',GL::FN (list ,',GL::X)))) ((g-var &) (gret (g-apply ',',GL::FN (list ,',GL::X)))) . ,',GL::CASES))) (local (in-theory (disable ,GL::GFN))) (local (defthm ,GL::BOOLEANP-THMNAME (booleanp (,GL::FN ,GL::X)))) (local (defthm tag-of-cons (equal (tag (cons a b)) a) :hints (("Goal" :in-theory (enable tag))))) (encapsulate nil (local (in-theory (e/d* (minimal-theory (:executable-counterpart-theory :here) bfr-and-of-nil bfr-or-of-t natp ,GL::BOOLEANP-THMNAME) ((immediate-force-modep) (force) (general-concretep) logcons eval-g-base-alt-def)))) ,@GL::ENCAP ,@GL::GUARD-ENCAP (verify-g-guards ,GL::FN :hints ',GL::GUARD-HINTS)) (def-gobj-dependency-thm ,GL::FN :hints `(("goal" :induct ,GL::GCALL :expand (,GL::GCALL) :in-theory (e/d ((:i ,GL::GFN)) ((:d ,GL::GFN)))))) (encapsulate nil (local (in-theory (e/d* (booleanp-compound-recognizer eval-g-base-g-apply (:type-prescription bfr-eval) eval-g-base-apply nth-open-when-constant-idx eval-g-base-of-gl-cons eval-g-base-atom eval-g-base-list) ((:type-prescription booleanp) bfr-eval-booleanp general-concretep-def general-boolean-value-correct booleanp-of-geval-for-eval-g-base integerp-of-geval-for-eval-g-base consp-of-geval-for-eval-g-base bool-cond-itep-eval eval-g-base-alt-def eval-concrete-gobjectp) nil))) ,@GL::ENCAP ,@GL::CORR-ENCAP (def-g-correct-thm ,GL::FN eval-g-base :hints `(("goal" :in-theory (enable (:induction ,GL::GFN)) :induct (,GL::GFN ,',GL::X . ,GL::PARAMS) :expand ((,GL::GFN ,',GL::X . ,GL::PARAMS))) (and stable-under-simplificationp '(:expand ((:with eval-g-base (eval-g-base ,',GL::X env)) (:with eval-g-base (eval-g-base nil env)) (:with eval-g-base (eval-g-base t env))))) . ,',GL::CORR-HINTS))))))
def-g-predicatemacro
(defmacro def-g-predicate (fn cases &key corr-hints guard-hints gobj-hints encap gobj-encap guard-encap corr-encap (formals '(x))) (declare (ignorable gobj-hints gobj-encap)) (def-g-predicate-fn fn cases corr-hints guard-hints encap guard-encap corr-encap formals))
other
(logic)
other
(def-g-predicate booleanp (((g-boolean &) (gret t)) (& (gret nil))))
other
(def-g-predicate not (((g-boolean bdd) (gret (mk-g-boolean (bfr-not bdd)))) (& (gret nil))) :formals (p) :corr-hints ((and stable-under-simplificationp '(:cases ((eval-g-base (g-ite->test p) env))))))
other
(def-g-predicate symbolp (((g-boolean &) (gret t)) (& (gret nil))))
other
(def-g-predicate acl2-numberp (((g-integer &) (gret t)) (& (gret nil))))
other
(def-g-predicate stringp ((& (gret nil))))
other
(def-g-predicate characterp ((& (gret nil))))
other
(def-g-predicate consp (((g-boolean &) (gret nil)) ((g-integer &) (gret nil)) (& (gret t))))
other
(def-g-predicate integerp (((g-integer &) (gret t)) (& (gret nil))))
other
(def-g-predicate rationalp (((g-integer &) (gret t)) (& (gret nil))))