base

(in-package "ACL2")

(local (include-book "system/apply/apply" :dir :system))

(defthm apply$-badgep-properties
  (implies (apply$-badgep x)
    (and (consp x)
      (natp (access apply$-badge x :arity))
      (natp (access apply$-badge x :out-arity))
      (or (eq (access apply$-badge x :ilks) t)
        (and (true-listp (access apply$-badge x :ilks))
          (equal (len (access apply$-badge x :ilks))
            (access apply$-badge x :arity))))))
  :rule-classes ((:compound-recognizer :corollary (implies (apply$-badgep x) (consp x))) (:linear :corollary (implies (apply$-badgep x) (<= 0 (car (cdr x)))))
    (:rewrite :corollary (implies (apply$-badgep x) (integerp (car (cdr x)))))
    (:linear :corollary (implies (apply$-badgep x) (<= 0 (car (cdr (cdr x))))))
    (:rewrite :corollary (implies (apply$-badgep x) (integerp (car (cdr (cdr x))))))
    (:rewrite :corollary (implies (and (apply$-badgep x) (not (eq (cdr (cdr (cdr x))) t)))
        (and (true-listp (cdr (cdr (cdr x))))
          (equal (len (cdr (cdr (cdr x)))) (car (cdr x))))))))

(defthm badge-prim-type
  (implies (apply$-primp fn)
    (and (apply$-badgep (badge-prim fn))
      (eq (cdr (cdr (cdr (badge-prim fn)))) t)))
  :hints (("Goal" :use (:instance check-it!-works (alist *badge-prim-falist*))
     :in-theory (disable check-it! hons-get)))
  :rule-classes ((:rewrite :corollary (implies (apply$-primp fn)
       (and (apply$-badgep (badge-prim fn))
         (eq (cdr (cdr (cdr (badge-prim fn)))) t)))) (:forward-chaining :corollary (implies (apply$-primp fn) (apply$-badgep (badge-prim fn))))))

(set-rewrite-stack-limit 4000)

(defun meta-apply$-prim
  (term)
  (declare (xargs :guard (pseudo-termp term) :verify-guards nil))
  (cond ((and (consp term)
       (eq (ffn-symb term) 'apply$-prim)
       (quotep (fargn term 1))
       (symbolp (cadr (fargn term 1)))) (let* ((fn (cadr (fargn term 1))) (args (fargn term 2))
          (temp (hons-get fn *badge-prim-falist*)))
        (cond ((null temp) term)
          (t (if (int= (access apply$-badge (cdr temp) :out-arity) 1)
              `(,FN ,@(N-CAR-CADR-CADDR-ETC (ACCESS APPLY$-BADGE (CDR TEMP) :ARITY) ARGS))
              `(mv-list ',(ACCESS APPLY$-BADGE (CDR TEMP) :OUT-ARITY)
                (,FN ,@(N-CAR-CADR-CADDR-ETC (ACCESS APPLY$-BADGE (CDR TEMP) :ARITY) ARGS))))))))
    (t term)))

(verify-guards meta-apply$-prim)

(make-event `(encapsulate nil
    (with-output :off (prove event)
      (defevaluator apply$-prim-meta-fn-ev
        apply$-prim-meta-fn-ev-list
        ((apply$-prim fn args) ,@(STRIP-CARS *FIRST-ORDER-LIKE-TERMS-AND-OUT-ARITIES*))))
    (local (defthm n-car-cadr-caddr-etc-opener
        (implies (natp n)
          (equal (n-car-cadr-caddr-etc (+ 1 n) args)
            (cons (list 'car args)
              (n-car-cadr-caddr-etc n (list 'cdr args)))))))
    (with-output :off (prove event)
      (defthm apply$-prim-meta-fn-correct
        (equal (apply$-prim-meta-fn-ev term alist)
          (apply$-prim-meta-fn-ev (meta-apply$-prim term) alist))
        :hints (("Goal" :in-theory (disable (:executable-counterpart break$))))
        :rule-classes ((:meta :trigger-fns (apply$-prim)))))
    (defthm apply$-primp-implies-symbolp
      (implies (apply$-primp fn) (symbolp fn))
      :rule-classes :forward-chaining)))

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

(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)))))

(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)

(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))))))
  :rule-classes :forward-chaining)

(defthm apply$-lambda-opener
  (equal (apply$-lambda fn args)
    (ev$ (lambda-object-body fn)
      (pairlis$ (lambda-object-formals fn) args))))

(defequiv fn-equal)

(defcong fn-equal equal (apply$ fn args) 1)

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

(encapsulate nil
  (defthm ev$-def-fact
    (implies (tamep x)
      (equal (ev$ x a)
        (cond ((variablep x) (cdr (assoc x a)))
          ((fquotep x) (cadr x))
          ((eq (car x) 'if) (if (ev$ (cadr x) a)
              (ev$ (caddr x) a)
              (ev$ (cadddr x) a)))
          (t (apply$ (car x) (ev$-list (cdr x) a))))))
    :hints (("Goal" :expand ((ev$ x a))))
    :rule-classes nil)
  (local (defthm ev$-def
      (implies (tamep x)
        (equal (ev$ x a)
          (cond ((variablep x) (cdr (assoc x a)))
            ((fquotep x) (cadr x))
            ((eq (car x) 'if) (if (ev$ (cadr x) a)
                (ev$ (caddr x) a)
                (ev$ (cadddr x) a)))
            (t (apply$ (car x) (ev$-list (cdr x) a))))))
      :hints (("Goal" :use ev$-def-fact))
      :rule-classes (:definition)))
  (defthm ev$-opener
    (and (implies (symbolp x) (equal (ev$ x a) (cdr (assoc x a))))
      (equal (ev$ (list 'quote obj) a) obj)
      (implies (suitably-tamep-listp 3 nil args)
        (equal (ev$ (cons 'if args) a)
          (if (ev$ (car args) a)
            (ev$ (cadr args) a)
            (ev$ (caddr args) a))))
      (implies (and (not (eq fn 'quote))
          (not (eq fn 'if))
          (tamep (cons fn args)))
        (equal (ev$ (cons fn args) a) (apply$ fn (ev$-list args a)))))
    :hints (("Subgoal 1" :expand (ev$ (cons fn args) a)))))

(defthm ev$-list-def
  (equal (ev$-list x a)
    (cond ((endp x) nil)
      (t (cons (ev$ (car x) a) (ev$-list (cdr x) a)))))
  :rule-classes ((:definition)))

(in-theory (disable ev$ ev$-list))

(defthm beta-reduction
  (and (equal (apply$ (list 'lambda vars body) args)
      (ev$ body (pairlis$ vars args)))
    (equal (apply$ (list 'lambda vars dcl body) args)
      (ev$ body (pairlis$ vars args)))))

(defthm apply$-primp-badge
  (implies (apply$-primp fn)
    (equal (badge fn) (badge-prim fn)))
  :hints (("Goal" :in-theory (enable badge))))

(defthm badge-badge
  (equal (badge 'badge) *generic-tame-badge-1*))

(defthm badge-tamep
  (equal (badge 'tamep) *generic-tame-badge-1*))

(defthm badge-tamep-functionp
  (equal (badge 'tamep-functionp) *generic-tame-badge-1*))

(defthm badge-suitably-tamep-listp
  (equal (badge 'suitably-tamep-listp) *generic-tame-badge-3*))

(defthm badge-apply$ (equal (badge 'apply$) *apply$-badge*))

(defthm badge-ev$ (equal (badge 'ev$) *ev$-badge*))

(defthm apply$-primitive
  (implies (apply$-primp fn)
    (equal (apply$ fn args) (apply$-prim fn args))))

(defthm apply$-badge
  (equal (apply$ 'badge args) (badge (car args))))

(defthm apply$-tamep
  (equal (apply$ 'tamep args) (tamep (car args))))

(defthm apply$-tamep-functionp
  (equal (apply$ 'tamep-functionp args)
    (tamep-functionp (car args))))

(defthm apply$-suitably-tamep-listp
  (equal (apply$ 'suitably-tamep-listp args)
    (suitably-tamep-listp (car args) (cadr args) (caddr args))))

(defthm apply$-apply$
  (implies (tamep-functionp (car args))
    (equal (apply$ 'apply$ args)
      (apply$ (car args) (cadr args))))
  :hints (("Goal" :in-theory (enable apply$))))

(defthm apply$-ev$
  (implies (tamep (car args))
    (equal (apply$ 'ev$ args) (ev$ (car args) (cadr args))))
  :hints (("Goal" :in-theory (enable apply$))))

(encapsulate nil
  (local (defun take1
      (n args)
      (cond ((zp n) nil)
        (t (cons (car args) (take1 (- n 1) (cdr args)))))))
  (local (defthm take1-take-gen
      (equal (first-n-ac n lst ac) (revappend ac (take1 n lst)))))
  (defthm alternative-take
    (equal (take n lst)
      (if (zp n)
        nil
        (cons (car lst) (take (- n 1) (cdr lst)))))
    :rule-classes :definition)
  (in-theory (disable take))
  (defthm take-opener
    (implies (syntaxp (quotep n))
      (equal (take n lst)
        (if (zp n)
          nil
          (cons (car lst) (take (- n 1) (cdr lst))))))
    :rule-classes :rewrite))

(defthm pairlis$-takes-arity-args
  (equal (pairlis$ x (take (len x) y)) (pairlis$ x y)))

(defthm apply$-lambda-takes-arity-args
  (implies (consp fn)
    (equal (apply$-lambda fn args)
      (apply$-lambda fn (take (len (cadr fn)) args))))
  :hints (("Goal" :expand ((apply$-lambda fn args) (apply$-lambda fn (take (len (cadr fn)) args)))))
  :rule-classes nil)

(defthm apply$-lambda-arity-1
  (implies (and (consp fn) (equal (len (cadr fn)) 1))
    (equal (apply$-lambda fn (list (car args)))
      (apply$-lambda fn args)))
  :hints (("Goal" :use apply$-lambda-takes-arity-args)))

(local (defthm hide-is-identity
    (equal (hide x) x)
    :hints (("Goal" :expand ((hide x))))))

(defthm apply$-prim-takes-arity-args
  (implies (apply$-primp fn)
    (equal (apply$-prim fn args)
      (apply$-prim fn
        (take (apply$-badge-arity (badge-prim fn)) args))))
  :hints (("Goal" :in-theory '(apply$-prim apply$-primp
       badge-prim
       take-opener
       (:executable-counterpart zp)
       car-cons
       cdr-cons
       hons-get
       (:executable-counterpart hons-assoc-equal)
       hide-is-identity)))
  :rule-classes nil)

(defthm apply$-prim-arity-1
  (implies (and (apply$-primp fn)
      (equal (apply$-badge-arity (badge-prim fn)) 1))
    (equal (apply$-prim fn (list (car args)))
      (apply$-prim fn args)))
  :hints (("Goal" :use apply$-prim-takes-arity-args)))

(defthm apply$-userfn-arity-1
  (implies (and (badge-userfn fn)
      (equal (apply$-badge-arity (badge-userfn fn)) 1))
    (equal (apply$-userfn fn (list (car args)))
      (apply$-userfn fn args)))
  :hints (("Goal" :use apply$-userfn-takes-arity-args)))

(defthm apply$-symbol-arity-1
  (implies (and (symbolp fn)
      (badge fn)
      (equal (apply$-badge-arity (badge fn)) 1))
    (equal (apply$ fn (list (car args))) (apply$ fn args)))
  :hints (("Goal" :in-theory (enable apply$ badge))))

(defthm equal-len-0
  (equal (equal (len x) 0) (not (consp x))))

(defthm equal-len-1
  (equal (equal (len x) 1)
    (and (consp x) (not (consp (cdr x))))))

(defthm apply$-consp-arity-1
  (implies (and (consp fn) (equal (len (lambda-object-formals fn)) 1))
    (equal (apply$ fn (list (car args))) (apply$ fn args)))
  :hints (("Goal" :expand ((apply$ fn (list (car args)))))))

(defun$ lamb (vars body) (list 'lambda vars body))

(encapsulate nil
  (defthm consp-lamb
    (and (consp (lamb args body)) (true-listp (lamb args body)))
    :rule-classes :type-prescription)
  (defthm consp-cdr-lamb (consp (cdr (lamb args body))))
  (defthm consp-cddr-lamb (consp (cddr (lamb args body))))
  (defthm cdddr-lamb (equal (cdddr (lamb args body)) nil))
  (defthm car-lamb (equal (car (lamb args body)) 'lambda))
  (defthm lambda-formals-lamb
    (equal (lambda-formals (lamb args body)) args))
  (defthm lambda-body-lamb
    (equal (lambda-body (lamb args body)) body))
  (defthm lamb-reduction
    (equal (apply$ (lamb vars body) args)
      (ev$ body (pairlis$ vars args)))
    :hints (("Goal" :in-theory (enable apply$)))))

(in-theory (disable lamb (:executable-counterpart lamb)))

(defthm lamb-v-v-is-identity
  (implies (symbolp v) (fn-equal (lamb (list v) v) 'identity))
  :hints (("goal" :in-theory (enable fn-equal))))

(defthm lambda-v-fn-v-is-fn
  (implies (and (symbolp v)
      (equal (apply$-badge-arity (badge fn)) 1)
      (not (eq fn 'quote))
      (tamep (list fn v)))
    (fn-equal (lamb (list v) (list fn v)) fn))
  :hints (("Goal" :in-theory (e/d (fn-equal badge) (badge-type apply$-badgep-properties))
     :use ((:instance badge-type (fn fn)))
     :expand ((tamep (list fn v)) (ev$ (list fn v)
         (list (cons v
             (car (apply$-equivalence-witness (lamb (list v) (list fn v)) fn)))))))))

(defun$ ok-fnp
  (fn)
  (and (not (eq fn 'quote)) (tamep `(,FN x))))

(defun$ compose (f g) (lamb '(v) `(,F (,G v))))

(defthm ok-fnp-compose
  (implies (and (ok-fnp f) (ok-fnp g)) (ok-fnp (compose f g)))
  :hints (("Goal" :in-theory (e/d (lamb) (badge))
     :expand ((tamep (cons g '(x))) (tamep (cons g '(v)))
       (tamep (list f (cons g '(v))))))))

(defthm apply$-composition
  (implies (and (ok-fnp f) (ok-fnp g))
    (equal (apply$ (compose f g) (list a))
      (apply$ f (list (apply$ g (list a))))))
  :hints (("Goal" :in-theory (e/d (lamb) (badge))
     :expand ((ev$ (list f (cons g '(v))) (list (cons 'v a))) (ev$ (cons g '(v)) (list (cons 'v a)))
       (tamep (cons g '(x)))
       (tamep (cons f '(x)))
       (tamep (list f (cons g '(v))))))))

(in-theory (disable compose))

(in-theory (disable (:definition fn-equal)
    (:definition ev$-list)
    (:definition ev$)
    (:definition apply$)
    (:definition badge)
    (:definition apply$-prim)
    (:definition badge-prim)
    (:definition apply$-primp)
    (:executable-counterpart apply$-equivalence)
    (:executable-counterpart apply$)
    (:executable-counterpart suitably-tamep-listp)
    (:executable-counterpart tamep-functionp)
    (:executable-counterpart tamep)
    (:executable-counterpart badge)))