interp-function-lookup

Included Books

hons-sets bstar mv-nth rulesets untranslate-patterns ev-theoremp meta-extract-user def-functional-instance

other

(in-package "ACL2")

include-book

(include-book "hons-sets")

include-book

(include-book "std/util/bstar" :dir :system)

include-book

(include-book "tools/mv-nth" :dir :system)

include-book

(include-book "tools/rulesets" :dir :system)

include-book

(include-book "misc/untranslate-patterns" :dir :system)

include-book

(include-book "clause-processors/ev-theoremp" :dir :system)

include-book

(include-book "clause-processors/meta-extract-user" :dir :system)

other

(set-inhibit-warnings "theory")

nonnil-symbol-listpfunction

(defun nonnil-symbol-listp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (eq x nil)
    (and (symbolp (car x))
      (car x)
      (nonnil-symbol-listp (cdr x)))))

eqlable-listp-when-nonnil-symbol-listptheorem

(defthm eqlable-listp-when-nonnil-symbol-listp
  (implies (nonnil-symbol-listp x) (eqlable-listp x))
  :rule-classes :forward-chaining)

interp-defs-alistpfunction

(defun interp-defs-alistp
  (defs)
  (declare (xargs :guard t))
  (or (atom defs)
    (and (let ((entry (car defs)))
        (case-match entry
          ((fn formals body . &) (and (symbolp fn)
              (not (eq fn 'quote))
              (pseudo-termp body)
              (nonnil-symbol-listp formals)
              (no-duplicatesp formals)))))
      (interp-defs-alistp (cdr defs)))))

hons-assoc-equal-interp-defs-alistptheorem

(defthmd hons-assoc-equal-interp-defs-alistp
  (implies (and (hons-assoc-equal x obligs)
      (interp-defs-alistp obligs))
    (let ((entry (hons-assoc-equal x obligs)))
      (case-match entry
        ((& formals body . &) (and (pseudo-termp body)
            (nonnil-symbol-listp formals)
            (no-duplicatesp-equal formals))))))
  :hints (("goal" :induct (hons-assoc-equal x obligs))))

in-theory

(in-theory (disable interp-defs-alistp))

other

(defevaluator ifl-ev
  ifl-ev-lst
  ((if a
     b
     c) (equal a b)
    (not x)
    (iff a b)
    (implies a b)
    (typespec-check ts x)
    (use-by-hint x)))

other

(def-meta-extract ifl-ev ifl-ev-lst)

local

(local (in-theory (disable w)))

meta-extract-function-formals/bodyfunction

(defund meta-extract-function-formals/body
  (fn world)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp world))))
  (b* ((formula (meta-extract-formula-w fn world)))
    (case-match formula
      (('equal (!fn . formals) body . &) (b* (((unless (and (nonnil-symbol-listp formals) (no-duplicatesp formals))) (mv (msg "Function ~x0 has ill-formed formals in definitional formula ~x1"
                 fn
                 formula)
               nil
               nil)) ((unless (pseudo-termp body)) (mv (msg "Function ~x0 has non-pseudo-term body in formula: ~x1"
                  fn
                  formula)
                nil
                nil)))
          (mv nil formals body)))
      (& (mv (if (equal formula *t*)
            (msg "Function ~x0 has no associated formula" fn)
            (msg "The formula of function ~x0 is not a simple EQUAL-based ~
                     definition: ~x1"
              fn
              formula))
          nil
          nil)))))

ifl-ev-meta-extract-function-formals/bodytheorem

(defthm ifl-ev-meta-extract-function-formals/body
  (b* (((mv err formals body) (meta-extract-function-formals/body fn (w state))))
    (implies (and (ifl-ev-meta-extract-global-facts) (not err))
      (equal (ifl-ev (cons fn formals) a) (ifl-ev body a))))
  :hints (("Goal" :in-theory (e/d (meta-extract-function-formals/body ifl-ev-constraint-0)
       (ifl-ev-meta-extract-formula))
     :use ((:instance ifl-ev-meta-extract-formula (name fn) (st state)))
     :cases ((eq fn 'quote))))
  :otf-flg t)

meta-extract-function-formals/body-well-formedtheorem

(defthm meta-extract-function-formals/body-well-formed
  (b* (((mv err formals body) (meta-extract-function-formals/body fn world)))
    (implies (not err)
      (and (nonnil-symbol-listp formals)
        (no-duplicatesp formals)
        (pseudo-termp body))))
  :hints (("Goal" :in-theory (enable meta-extract-function-formals/body))))

interp-function-lookupfunction

(defun interp-function-lookup
  (fn defs overrides world)
  (declare (xargs :guard (and (symbolp fn)
        (interp-defs-alistp defs)
        (interp-defs-alistp overrides)
        (plist-worldp world))
      :guard-hints (("goal" :in-theory (enable hons-assoc-equal-interp-defs-alistp)))))
  (b* ((look (hons-get fn defs)) (ov-look (or look (hons-get fn overrides)))
      ((when ov-look) (b* (((list formals body) (cdr ov-look)) (defs (if look
                defs
                (hons-acons fn (cdr ov-look) defs)))
            ((unless (mbt (and (nonnil-symbol-listp formals)
                   (no-duplicatesp-eq formals)
                   (pseudo-termp body)))) (mv (msg "Override for ~x0 ill-formed~%" fn) nil nil nil)))
          (mv nil body formals defs)))
      ((mv err formals body) (meta-extract-function-formals/body fn world))
      ((when err) (mv err nil nil nil)))
    (mv nil body formals defs)))

interp-function-lookup-defs-alistptheorem

(defthm interp-function-lookup-defs-alistp
  (b* (((mv erp & & out-defs) (interp-function-lookup fn in-defs overrides world)))
    (implies (and (not erp) (symbolp fn) (interp-defs-alistp overrides))
      (iff (interp-defs-alistp out-defs)
        (interp-defs-alistp in-defs))))
  :hints (("Goal" :in-theory (e/d (interp-defs-alistp hons-assoc-equal-interp-defs-alistp)))))

interp-function-lookup-defs-alistp-means-in-defs-alistptheorem

(defthm interp-function-lookup-defs-alistp-means-in-defs-alistp
  (b* (((mv erp & & out-defs) (interp-function-lookup fn in-defs overrides world)))
    (implies (and (not (interp-defs-alistp in-defs)) (not erp))
      (not (interp-defs-alistp out-defs))))
  :hints (("Goal" :in-theory (enable interp-defs-alistp))))

interp-function-lookup-wfptheorem

(defthm interp-function-lookup-wfp
  (b* (((mv erp body formals &) (interp-function-lookup fn in-defs overrides world)))
    (implies (not erp)
      (and (pseudo-termp body)
        (nonnil-symbol-listp formals)
        (no-duplicatesp-equal formals))))
  :hints (("Goal" :in-theory (enable hons-assoc-equal-interp-defs-alistp))))

interp-defs-alist-clausesfunction

(defun interp-defs-alist-clauses
  (defs)
  (declare (xargs :guard (interp-defs-alistp defs)
      :guard-hints (("Goal" :in-theory (enable interp-defs-alistp)))))
  (if (atom defs)
    nil
    (cons `((not (use-by-hint ',(CDDDAR DEFS))) (equal (,(CAAR DEFS) . ,(CADAR DEFS)) ,(CADDAR DEFS)))
      (interp-defs-alist-clauses (cdr defs)))))

ifl-ev-theoremp-conjunctstheorem

(defthm ifl-ev-theoremp-conjuncts
  (iff (ifl-ev-theoremp (conjoin (cons a b)))
    (and (ifl-ev-theoremp a) (ifl-ev-theoremp (conjoin b))))
  :hints (("goal" :use ((:instance ifl-ev-falsify
        (x (conjoin (cons a b)))
        (a (ifl-ev-falsify a))) (:instance ifl-ev-falsify
         (x a)
         (a (ifl-ev-falsify (conjoin (cons a b)))))
       (:instance ifl-ev-falsify
         (x (conjoin (cons a b)))
         (a (ifl-ev-falsify (conjoin b))))
       (:instance ifl-ev-falsify
         (x (conjoin b))
         (a (ifl-ev-falsify (conjoin (cons a b)))))))))

ifl-ev-theoremp-remove-first-lit-when-falsetheorem

(defthm ifl-ev-theoremp-remove-first-lit-when-false
  (implies (ifl-ev-theoremp (list 'not lit))
    (iff (ifl-ev-theoremp (disjoin (cons lit clause)))
      (ifl-ev-theoremp (disjoin clause))))
  :hints (("Goal" :use ((:instance ifl-ev-falsify
        (x (disjoin clause))
        (a (ifl-ev-falsify (disjoin (cons lit clause))))) (:instance ifl-ev-falsify
         (x (list 'not lit))
         (a (ifl-ev-falsify (disjoin clause))))
       (:instance ifl-ev-falsify
         (x (disjoin (cons lit clause)))
         (a (ifl-ev-falsify (disjoin clause)))))
     :in-theory (enable ifl-ev-disjoin-cons)))
  :otf-flg t)

ifl-ev-of-disjoin-appendtheorem

(defthm ifl-ev-of-disjoin-append
  (iff (ifl-ev (disjoin (append a b)) al)
    (or (ifl-ev (disjoin a) al) (ifl-ev (disjoin b) al))))

ifl-ev-theoremp-of-conjoin-clauses-constheorem

(defthm ifl-ev-theoremp-of-conjoin-clauses-cons
  (iff (ifl-ev-theoremp (conjoin-clauses (cons cl1 clrest)))
    (and (ifl-ev-theoremp (disjoin cl1))
      (ifl-ev-theoremp (conjoin-clauses clrest))))
  :hints (("Goal" :in-theory (enable conjoin-clauses disjoin-lst))))

ifl-ev-theoremp-of-conjoin-clauses-appendtheorem

(defthm ifl-ev-theoremp-of-conjoin-clauses-append
  (iff (ifl-ev-theoremp (conjoin-clauses (append cls1 cls2)))
    (and (ifl-ev-theoremp (conjoin-clauses cls1))
      (ifl-ev-theoremp (conjoin-clauses cls2))))
  :hints (("subgoal *1/1" :in-theory (enable conjoin-clauses))))

hons-assoc-equal-ifl-ev-defs-alist-equalitytheorem

(defthm hons-assoc-equal-ifl-ev-defs-alist-equality
  (let ((entry (hons-assoc-equal fn defs)))
    (implies (and (ifl-ev-theoremp (conjoin-clauses (interp-defs-alist-clauses defs)))
        entry)
      (equal (equal (ifl-ev (cons fn (cadr entry)) a)
          (ifl-ev (caddr entry) a))
        t)))
  :hints (("goal" :in-theory (enable interp-defs-alistp use-by-hint)) ("Subgoal *1/2" :use ((:instance ifl-ev-falsify
         (x (disjoin `((equal (,FN . ,(CADAR DEFS)) ,(CADDAR DEFS))))))))))

interp-function-lookup-theoremp-defs-historytheorem

(defthm interp-function-lookup-theoremp-defs-history
  (b* (((mv erp & & out-defs) (interp-function-lookup fn in-defs overrides world)))
    (implies (and (ifl-ev-theoremp (conjoin-clauses (interp-defs-alist-clauses out-defs)))
        (not erp))
      (ifl-ev-theoremp (conjoin-clauses (interp-defs-alist-clauses in-defs))))))

interp-function-lookup-correct-1theorem

(defthm interp-function-lookup-correct-1
  (mv-let (erp body formals out-defs)
    (interp-function-lookup fn in-defs overrides (w state))
    (implies (and (not erp)
        (ifl-ev-theoremp (conjoin-clauses (interp-defs-alist-clauses out-defs)))
        (ifl-ev-meta-extract-global-facts))
      (equal (ifl-ev body a) (ifl-ev (cons fn formals) a))))
  :hints (("goal" :in-theory (e/d (hons-assoc-equal-interp-defs-alistp use-by-hint)
       (default-car default-cdr pseudo-termp len))
     :use ((:instance ifl-ev-falsify
        (x (b* (((mv & body formals &) (interp-function-lookup fn in-defs overrides world)))
            (disjoin `((equal (,FN . ,FORMALS) ,BODY)))))
        (a a))))))

in-theory

(in-theory (disable interp-function-lookup))

ifl-ev-lst-acons-non-membertheorem

(defthm ifl-ev-lst-acons-non-member
  (implies (and (nonnil-symbol-listp vars)
      (not (member-equal key vars)))
    (equal (ifl-ev-lst vars (cons (cons key val) rest))
      (ifl-ev-lst vars rest))))

ifl-ev-lst-pairlistheorem

(defthm ifl-ev-lst-pairlis
  (implies (and (nonnil-symbol-listp vars)
      (no-duplicatesp-equal vars)
      (equal (len vars) (len vals)))
    (equal (ifl-ev-lst vars (pairlis$ vars vals))
      (list-fix vals))))

kwote-list-list-fixtheorem

(defthm kwote-list-list-fix
  (equal (kwote-lst (list-fix x)) (kwote-lst x)))

ifl-ev-cons-pairlistheorem

(defthm ifl-ev-cons-pairlis
  (implies (and (nonnil-symbol-listp vars)
      (no-duplicatesp-equal vars)
      (equal (len vars) (len vals))
      (not (eq fn 'quote)))
    (equal (ifl-ev (cons fn vars) (pairlis$ vars vals))
      (ifl-ev (cons fn (kwote-lst vals)) nil)))
  :hints (("goal" :use ((:instance ifl-ev-constraint-0
        (x (cons fn vars))
        (a (pairlis$ vars vals)))))))

interp-function-lookup-correct-2theorem

(defthm interp-function-lookup-correct-2
  (mv-let (erp body formals out-defs)
    (interp-function-lookup fn in-defs overrides (w state))
    (implies (and (not erp)
        (ifl-ev-theoremp (conjoin-clauses (interp-defs-alist-clauses out-defs)))
        (equal (len formals) (len actuals))
        (not (eq fn 'quote))
        (ifl-ev-meta-extract-global-facts))
      (equal (ifl-ev body (pairlis$ formals actuals))
        (ifl-ev (cons fn (kwote-lst actuals)) nil))))
  :hints (("goal" :do-not-induct t) (and stable-under-simplificationp
      '(:in-theory (enable ifl-ev-constraint-0)))))

len-ifl-ev-lsttheorem

(defthm len-ifl-ev-lst
  (equal (len (ifl-ev-lst x a)) (len x))
  :hints (("goal" :induct (len x))))

interp-function-lookup-correcttheorem

(defthm interp-function-lookup-correct
  (mv-let (erp body formals out-defs)
    (interp-function-lookup fn in-defs overrides (w state))
    (implies (and (not erp)
        (ifl-ev-theoremp (conjoin-clauses (interp-defs-alist-clauses out-defs)))
        (equal (len formals) (len actuals))
        (not (eq fn 'quote))
        (ifl-ev-meta-extract-global-facts))
      (equal (ifl-ev body (pairlis$ formals (ifl-ev-lst actuals a)))
        (ifl-ev (cons fn actuals) a))))
  :hints (("goal" :in-theory (e/d* (ifl-ev-constraint-0))
     :do-not-induct t)))

local

(local (progn (include-book "tools/def-functional-instance" :dir :system)
    (defevaluator foo-ev
      foo-ev-lst
      ((if a
         b
         c) (equal a b)
        (not a)
        (use-by-hint x)
        (typespec-check ts x)
        (implies a b)
        (iff a b)
        (cons a b)
        (car a)
        (cdr b)
        (consp a)
        (binary-+ a b)
        (unary-- a)
        (len x)))
    (def-meta-extract foo-ev foo-ev-lst)
    (def-functional-instance interp-function-lookup-correct-for-foo-ev
      interp-function-lookup-correct
      ((ifl-ev foo-ev) (ifl-ev-lst foo-ev-lst)
        (ifl-ev-falsify foo-ev-falsify)
        (ifl-ev-meta-extract-global-badguy foo-ev-meta-extract-global-badguy))
      :hints ((and stable-under-simplificationp
         '(:use (foo-ev-constraint-0 foo-ev-falsify
             foo-ev-meta-extract-global-badguy)))))
    (def-functional-instance interp-function-lookup-correct-2-for-foo-ev
      interp-function-lookup-correct-2
      ((ifl-ev foo-ev) (ifl-ev-lst foo-ev-lst)
        (ifl-ev-falsify foo-ev-falsify)
        (ifl-ev-meta-extract-global-badguy foo-ev-meta-extract-global-badguy)))
    (def-functional-instance interp-function-lookup-theoremp-defs-history-for-foo-ev
      interp-function-lookup-theoremp-defs-history
      ((ifl-ev foo-ev) (ifl-ev-lst foo-ev-lst)
        (ifl-ev-falsify foo-ev-falsify)
        (ifl-ev-meta-extract-global-badguy foo-ev-meta-extract-global-badguy)))
    (def-functional-instance foo-ev-theoremp-of-conjoin-clauses-cons
      ifl-ev-theoremp-of-conjoin-clauses-cons
      ((ifl-ev foo-ev) (ifl-ev-lst foo-ev-lst)
        (ifl-ev-falsify foo-ev-falsify)
        (ifl-ev-meta-extract-global-badguy foo-ev-meta-extract-global-badguy)))
    (def-functional-instance foo-ev-theoremp-of-conjoin-clauses-append
      ifl-ev-theoremp-of-conjoin-clauses-append
      ((ifl-ev foo-ev) (ifl-ev-lst foo-ev-lst)
        (ifl-ev-falsify foo-ev-falsify)
        (ifl-ev-meta-extract-global-badguy foo-ev-meta-extract-global-badguy)))))