apply - ACL2 Book

Included Books

lexicographic-ordering-without-arithmetic flag

other

(in-package "ACL2")

local

(local (in-theory (enable apply$-primp
      badge-prim
      badge
      (:executable-counterpart badge)
      (:executable-counterpart tamep)
      (:executable-counterpart tamep-functionp)
      (:executable-counterpart suitably-tamep-listp)
      ev$
      ev$-list
      apply$
      (:executable-counterpart apply$))))

badgefunction

(defun badge
  (fn)
  (declare (xargs :guard t))
  (cond ((apply$-primp fn) (badge-prim fn))
    ((eq fn 'badge) *generic-tame-badge-1*)
    ((eq fn 'tamep) *generic-tame-badge-1*)
    ((eq fn 'tamep-functionp) *generic-tame-badge-1*)
    ((eq fn 'suitably-tamep-listp) *generic-tame-badge-3*)
    ((eq fn 'apply$) *apply$-badge*)
    ((eq fn 'ev$) *ev$-badge*)
    (t (badge-userfn fn))))

in-theory

(in-theory (disable apply$-primp badge-prim))

badge-typetheorem

(defthm badge-type
  (or (null (badge fn)) (apply$-badgep (badge fn)))
  :rule-classes ((:forward-chaining :corollary (implies (badge fn) (apply$-badgep (badge fn))))))

in-theory

(in-theory (disable badge))

tamepmutual-recursion

(mutual-recursion (defun tamep
    (x)
    (declare (xargs :measure (acl2-count x) :guard t :verify-guards nil))
    (cond ((atom x) (symbolp x))
      ((eq (car x) 'quote) (and (consp (cdr x)) (null (cddr x))))
      ((symbolp (car x)) (let ((bdg (badge (car x))))
          (cond ((null bdg) nil)
            ((eq (access apply$-badge bdg :ilks) t) (suitably-tamep-listp (access apply$-badge bdg :arity)
                nil
                (cdr x)))
            (t (suitably-tamep-listp (access apply$-badge bdg :arity)
                (access apply$-badge bdg :ilks)
                (cdr x))))))
      ((consp (car x)) (let ((fn (car x)))
          (and (tamep-lambdap fn)
            (suitably-tamep-listp (length (cadr fn)) nil (cdr x)))))
      (t nil)))
  (defun tamep-functionp
    (fn)
    (declare (xargs :measure (acl2-count fn) :guard t))
    (if (symbolp fn)
      (let ((bdg (badge fn)))
        (and bdg (eq (access apply$-badge bdg :ilks) t)))
      (and (consp fn) (tamep-lambdap fn))))
  (defun suitably-tamep-listp
    (n flags args)
    (declare (xargs :measure (acl2-count args)
        :guard (and (natp n) (true-listp flags))))
    (cond ((zp n) (null args))
      ((atom args) nil)
      (t (and (let ((arg (car args)))
            (case (car flags)
              (:fn (and (consp arg)
                  (eq (car arg) 'quote)
                  (consp (cdr arg))
                  (null (cddr arg))
                  (tamep-functionp (cadr arg))))
              (:expr (and (consp arg)
                  (eq (car arg) 'quote)
                  (consp (cdr arg))
                  (null (cddr arg))
                  (tamep (cadr arg))))
              (otherwise (tamep arg))))
          (suitably-tamep-listp (- n 1) (cdr flags) (cdr args)))))))

other

(verify-guards tamep
  :hints (("Goal" :use ((:instance badge-type (fn fn)) (:instance badge-type (fn (car x)))))))

local

(local (defun suitably-tamep-listp-induction
    (n flags args)
    (cond ((zp n) (list flags args))
      (t (suitably-tamep-listp-induction (- n 1)
          (cdr flags)
          (cdr args))))))

local

(local (defthm suitably-tamep-listp-implicant-1
    (implies (and (suitably-tamep-listp n flags args) (natp n))
      (and (true-listp args) (equal (len args) n)))
    :hints (("Goal" :induct (suitably-tamep-listp-induction n flags args)))
    :rule-classes :forward-chaining))

local

(local (defthm tamep-implicant-1
    (implies (and (tamep x) (consp x)) (true-listp x))
    :hints (("Goal" :expand (tamep x)
       :use ((:instance badge-type (fn (car x))))))))

in-theory

(in-theory (disable (:executable-counterpart tamep)
    (:executable-counterpart tamep-functionp)
    (:executable-counterpart suitably-tamep-listp)))

include-book

(include-book "ordinals/lexicographic-ordering-without-arithmetic" :dir :system)

ev$-measurefunction

(defun ev$-measure
  (x a)
  (declare (ignore a))
  (llist (acl2-count x) 0))

ev$-list-measurefunction

(defun ev$-list-measure
  (x a)
  (declare (ignore a))
  (llist (acl2-count x) 0))

apply$-measurefunction

(defun apply$-measure
  (fn args)
  (cond ((consp fn) (llist (acl2-count fn) 0))
    ((eq fn 'apply$) (llist (+ 1 (acl2-count (car args))) 0))
    ((eq fn 'ev$) (llist (+ 1 (acl2-count (car args))) 0))
    (t (llist 0 0))))

apply$-lambda-measurefunction

(defun apply$-lambda-measure
  (fn args)
  (declare (ignore args))
  (llist (acl2-count (lambda-object-body fn)) 1))

len-ev$-listtheorem

(defthm len-ev$-list (equal (len (ev$-list x a)) (len x)))

in-theory

(in-theory (disable ev$
    ev$-list
    badge
    (:executable-counterpart badge)
    apply$
    (:executable-counterpart apply$)))

local

(local (include-book "tools/flag" :dir :system))

local

(local (encapsulate nil
    (progn (defun count-to-nil
        (x)
        (if (atom x)
          (if (null x)
            0
            1)
          (+ 1 (count-to-nil (car x)) (count-to-nil (cdr x)))))
      (verify-termination executable-badge)
      (verify-termination (executable-tamep (declare (xargs :measure (acl2-count x))))
        (executable-tamep-functionp (declare (xargs :measure (acl2-count fn))))
        (executable-suitably-tamep-listp (declare (xargs :measure (acl2-count args)))))
      (verify-termination weak-well-formed-lambda-objectp)
      (verify-termination changed-functional-or-expressional-formalp)
      (verify-termination accumulate-ilk)
      (verify-termination (guess-ilks-alist (declare (xargs :measure (acl2-count term))))
        (guess-ilks-alist-list (declare (xargs :measure (acl2-count terms))))))
    (defun find-badge-ilk
      (var formals ilks)
      (cond ((endp formals) nil)
        ((eq var (car formals)) (car ilks))
        (t (find-badge-ilk var (cdr formals) (cdr ilks)))))
    (mutual-recursion (defun check-ilks
        (fn new-formals new-badge term ilk wrld)
        (declare (xargs :measure (acl2-count term)))
        (cond ((variablep term) (eq (find-badge-ilk term
                new-formals
                (access apply$-badge new-badge :ilks))
              ilk))
          ((fquotep term) (cond ((eq ilk :fn) (or (and (symbolp (cadr term))
                    (or (not (equal fn (cadr term))) (executable-badge fn wrld))
                    (executable-tamep-functionp (cadr term) wrld))
                  (and (consp (cadr term))
                    (and (weak-well-formed-lambda-objectp (cadr term) wrld)
                      (or (not (ffnnamep fn (lambda-object-body (cadr term))))
                        (executable-badge fn wrld))
                      (executable-tamep-lambdap (cadr term) wrld)))))
              ((eq ilk :expr) (and (termp (cadr term) wrld)
                  (not (ffnnamep fn (cadr term)))
                  (executable-tamep (cadr term) wrld)))
              (t t)))
          ((flambdap (ffn-symb term)) nil)
          ((or (eq ilk :fn) (eq ilk :expr)) nil)
          ((eq fn (ffn-symb term)) (and (check-ilks-list fn
                new-formals
                new-badge
                (fargs term)
                (access apply$-badge new-badge :ilks)
                wrld)
              (or (eq (access apply$-badge new-badge :ilks) t)
                (not (changed-functional-or-expressional-formalp (formals fn wrld)
                    (access apply$-badge new-badge :ilks)
                    (fargs term))))))
          (t (let ((bdg (executable-badge (ffn-symb term) wrld)))
              (and bdg
                (check-ilks-list fn
                  new-formals
                  new-badge
                  (fargs term)
                  (access apply$-badge bdg :ilks)
                  wrld))))))
      (defun check-ilks-list
        (fn new-formals new-badge terms ilks wrld)
        (declare (xargs :measure (acl2-count terms)))
        (cond ((endp terms) t)
          (t (and (check-ilks fn
                new-formals
                new-badge
                (car terms)
                (cond ((eq ilks t) nil) (t (car ilks)))
                wrld)
              (check-ilks-list fn
                new-formals
                new-badge
                (cdr terms)
                (cond ((eq ilks t) t) (t (cdr ilks)))
                wrld))))))
    (in-theory (disable executable-badge
        executable-tamep
        executable-tamep-functionp
        weak-well-formed-lambda-objectp
        changed-functional-or-expressional-formalp))
    (make-flag checker guess-ilks-alist)
    (mutual-recursion (defun alist-okp
        (term formals badge alist wrld)
        (cond ((variablep term) (and (member term formals)
              (assoc term alist)
              (member (cdr (assoc term alist)) '(nil :fn :expr))
              (equal (find-badge-ilk term
                  formals
                  (access apply$-badge badge :ilks))
                (cdr (assoc term alist)))))
          ((fquotep term) t)
          (t (and (symbolp (car term))
              (true-listp (fgetprop (car term) 'formals t wrld))
              (alist-okp-list (fargs term) formals badge alist wrld)))))
      (defun alist-okp-list
        (terms formals badge alist wrld)
        (cond ((endp terms) t)
          (t (and (alist-okp (car terms) formals badge alist wrld)
              (alist-okp-list (cdr terms) formals badge alist wrld))))))
    (defthm-checker (defthm guess-ilks-alist-lemma
        (implies (and (alist-okp term formals new-badge alist wrld)
            (null (mv-nth 0
                (guess-ilks-alist fn new-badge term ilk wrld alist)))
            new-badge)
          (equal (mv-nth 1
              (guess-ilks-alist fn new-badge term ilk wrld alist))
            alist))
        :flag guess-ilks-alist)
      (defthm guess-ilks-alist-list-lemma
        (implies (and (alist-okp-list terms formals new-badge alist wrld)
            (null (mv-nth 0
                (guess-ilks-alist-list fn new-badge terms ilks wrld alist)))
            new-badge)
          (equal (mv-nth 1
              (guess-ilks-alist-list fn new-badge terms ilks wrld alist))
            alist))
        :flag guess-ilks-alist-list)
      :hints (("Goal" :in-theory (enable accumulate-ilk))))
    (defun badge-alistp
      (alist)
      (cond ((atom alist) (eq alist nil))
        (t (and (consp (car alist))
            (symbolp (caar alist))
            (apply$-badgep (cdar alist))
            (badge-alistp (cdr alist))))))
    (defun badge-userfn-structure-okp
      (alist)
      (cond ((atom alist) (eq alist nil))
        (t (and (weak-badge-userfn-structure-tuplep (car alist))
            (symbolp (car (car alist)))
            (booleanp (access-badge-userfn-structure-tuple-warrantp (car alist)))
            (apply$-badgep (access-badge-userfn-structure-tuple-badge (car alist)))
            (badge-userfn-structure-okp (cdr alist))))))
    (defthm apply$-badgep-hons-get-lemma
      (implies (and (badge-alistp alist) (hons-get fn alist))
        (apply$-badgep (cdr (hons-get fn alist))))
      :hints (("Goal" :in-theory (enable hons-assoc-equal))))
    (defthm apply$-badgep-executable-badge-lemma
      (implies (and (badge-userfn-structure-okp alist) (assoc fn alist))
        (apply$-badgep (access-badge-userfn-structure-tuple-badge (assoc-equal fn alist)))))
    (defthm apply$-badgep-executable-badge
      (implies (and (badge-alistp (unquote (getpropc '*badge-prim-falist* 'const nil wrld)))
          (badge-userfn-structure-okp (cdr (assoc-equal :badge-userfn-structure (table-alist 'badge-table wrld))))
          (executable-badge fn wrld))
        (apply$-badgep (executable-badge fn wrld)))
      :hints (("Goal" :in-theory (e/d (executable-badge) (hons-get apply$-badgep))))
      :rule-classes nil)
    (defthm-checker (defthm guess-ilks-alist-correct
        (implies (and (null (mv-nth 0
                (guess-ilks-alist fn new-badge term ilk wrld alist)))
            (alist-okp term formals new-badge alist wrld)
            (badge-alistp (unquote (getpropc '*badge-prim-falist* 'const nil wrld)))
            (badge-userfn-structure-okp (cdr (assoc-equal :badge-userfn-structure (table-alist 'badge-table wrld))))
            (apply$-badgep new-badge)
            (member ilk '(nil :fn :expr))
            (termp term wrld))
          (check-ilks fn formals new-badge term ilk wrld))
        :flag guess-ilks-alist)
      (defthm guess-ilks-alist-list-correct
        (implies (and (null (mv-nth 0
                (guess-ilks-alist-list fn new-badge terms ilks wrld alist)))
            (alist-okp-list terms formals new-badge alist wrld)
            (badge-alistp (unquote (getpropc '*badge-prim-falist* 'const nil wrld)))
            (badge-userfn-structure-okp (cdr (assoc-equal :badge-userfn-structure (table-alist 'badge-table wrld))))
            (apply$-badgep new-badge)
            (or (eq ilks t)
              (and (true-listp ilks) (subsetp ilks '(nil :fn :expr))))
            (term-listp terms wrld))
          (check-ilks-list fn formals new-badge terms ilks wrld))
        :flag guess-ilks-alist-list)
      :hints (("Subgoal *1/28" :use ((:instance apply$-badgep-executable-badge (fn (car term)))))))))

apply$-equivalencefunction

(defun-sk apply$-equivalence
  (fn1 fn2)
  (declare (xargs :guard t))
  (forall (args)
    (equal (ec-call (apply$ fn1 args))
      (ec-call (apply$ fn2 args)))))

fn-equalfunction

(defun fn-equal
  (fn1 fn2)
  (declare (xargs :guard t))
  (if (equal fn1 fn2)
    t
    (and (tamep-functionp fn1)
      (tamep-functionp fn2)
      (apply$-equivalence fn1 fn2))))

local

(local (defthm apply$-equivalence-necc-rewriter
    (implies (equal (apply$ fn1 (apply$-equivalence-witness fn1 fn2))
        (apply$ fn2 (apply$-equivalence-witness fn1 fn2)))
      (equal (apply$ fn1 args) (apply$ fn2 args)))
    :hints (("Goal" :in-theory (disable apply$-equivalence-necc)
       :use apply$-equivalence-necc))))

other

(defequiv fn-equal :package :legacy)

other

(defcong fn-equal equal (apply$ fn args) 1 :package :legacy)

in-theory

(in-theory (disable fn-equal))

defcong-fn-equal-equal-eventsfunction

(defun defcong-fn-equal-equal-events
  (term i c1-cn)
  (declare (xargs :guard (and (natp i) (true-listp c1-cn))))
  (cond ((endp c1-cn) nil)
    ((eq (car c1-cn) :fn) (cons `(defcong fn-equal
          equal
          ,TERM
          ,I
          :package :legacy :hints (("Goal" :in-theory (disable (:executable-counterpart force)))))
        (defcong-fn-equal-equal-events term (+ 1 i) (cdr c1-cn))))
    (t (defcong-fn-equal-equal-events term (+ 1 i) (cdr c1-cn)))))