defmax-nat-template

(in-package "ACL2")

(include-book "std/basic/defs" :dir :system)

(encapsulate (((xp *) => *)) (local (defun xp (x) x)))

(encapsulate (((elementp * *) =>
     *
     :formals (x y)
     :guard (and (xp x) (natp y))))
  (local (defun elementp (x y) (cons x y))))

(defun-sk uboundp
  (x y)
  (declare (xargs :guard (and (xp x) (natp y))))
  (forall (y1)
    (impliez (and (natp y1) (elementp x y1)) (>= (nfix y) y1)))
  :rewrite (implies (and (uboundp x y) (natp y1) (elementp x y1))
    (>= (nfix y) y1)))

(defthm booleanp-of-uboundp (booleanp (uboundp x y)))

(in-theory (disable uboundp uboundp-necc))

(defun-sk existsp
  (x)
  (declare (xargs :guard (xp x)))
  (exists (y) (and (natp y) (elementp x y) (uboundp x y)))
  :skolem-name existsp-witness)

(defthm booleanp-of-existsp (booleanp (existsp x)))

(in-theory (disable existsp existsp-suff))

(defun f
  (x)
  (declare (xargs :guard (xp x)))
  (if (existsp x)
    (existsp-witness x)
    nil))

(defthm maybe-natp-of-f
  (maybe-natp (f x))
  :hints (("Goal" :in-theory (enable maybe-natp existsp))))

(defthm natp-of-f-equal-existsp
  (equal (natp (f x)) (existsp x))
  :hints (("Goal" :in-theory (enable existsp))))

(defthm natp-of-f-when-existsp
  (implies (existsp x) (natp (f x)))
  :rule-classes :type-prescription)

(defthm f-iff-existsp
  (iff (f x) (existsp x))
  :hints (("Goal" :in-theory (enable existsp))))

(defthm not-f-when-not-existsp
  (implies (not (existsp x)) (not (f x)))
  :rule-classes :type-prescription)

(defthm elementp-of-f-when-existsp
  (implies (existsp x) (elementp x (f x)))
  :hints (("Goal" :in-theory (enable existsp))))

(defthm uboundp-of-f-when-existsp
  (implies (existsp x) (uboundp x (f x)))
  :hints (("Goal" :in-theory (enable existsp))))

(defthm f-geq-when-existsp-linear
  (implies (and (existsp x) (elementp x y1) (natp y1))
    (>= (f x) y1))
  :rule-classes :linear :hints (("Goal" :use (uboundp-of-f-when-existsp (:instance uboundp-necc (y (f x)))))))

(defthm f-geq-when-existsp-rewrite
  (implies (and (existsp x) (elementp x y1) (natp y1))
    (>= (f x) y1))
  :hints (("Goal" :by f-geq-when-existsp-linear)))

(defthm f-leq-when-existsp-linear
  (implies (and (existsp x) (uboundp x y1) (natp y1))
    (<= (f x) y1))
  :rule-classes :linear :hints (("Goal" :in-theory (disable f)
     :use (:instance uboundp-necc (y1 (f x)) (y y1)))))

(defthm f-leq-when-existsp-rewrite
  (implies (and (existsp x) (uboundp x y1) (natp y1))
    (<= (f x) y1))
  :hints (("Goal" :by f-leq-when-existsp-linear)))

(in-theory (disable f))

(defthm ubound-geq-member
  (implies (and (natp y0) (elementp x y0) (natp y1) (uboundp x y1))
    (>= y1 y0))
  :rule-classes nil
  :hints (("Goal" :use (:instance uboundp-necc (y y1) (y1 y0)))))

(defthm ubound-nonmember-gt-member
  (implies (and (natp y0)
      (elementp x y0)
      (natp y1)
      (uboundp x y1)
      (not (elementp x y1)))
    (> y1 y0))
  :rule-classes nil
  :hints (("Goal" :use ubound-geq-member)))

(defun find-max
  (x y1 y0)
  (declare (xargs :hints (("Goal" :use ubound-nonmember-gt-member))))
  (if (and (natp y0) (elementp x y0) (natp y1) (uboundp x y1))
    (if (elementp x y1)
      y1
      (find-max x (1- y1) y0))
    0))

(defthm find-max-uboundp-preservation
  (implies (and (natp y0)
      (elementp x y0)
      (natp y1)
      (uboundp x y1)
      (not (elementp x y1)))
    (uboundp x (1- y1)))
  :hints (("Goal" :expand ((uboundp x (1- y1)))
     :use (:instance uboundp-necc
       (y y1)
       (y1 (uboundp-witness x (1- y1)))))))

(defthm elementp-of-find-max
  (implies (and (natp y0) (elementp x y0) (natp y1) (uboundp x y1))
    (elementp x (find-max x y1 y0)))
  :hints ('(:use (:instance uboundp-necc (y y1) (y1 0))) '(:use (:instance uboundp-necc (y 0) (y1 y0)))))

(defthm uboundp-of-find-max
  (implies (and (natp y0) (elementp x y0) (natp y1) (uboundp x y1))
    (uboundp x (find-max x y1 y0)))
  :hints ('(:use (:instance uboundp-necc (y y1) (y1 0))) '(:use (:instance uboundp-necc (y 0) (y1 y0)))))

(defthm existsp-when-nonempty-and-bounded
  (implies (and (natp y0) (elementp x y0) (natp y1) (uboundp x y1))
    (existsp x))
  :rule-classes nil
  :hints (("Goal" :use (:instance existsp-suff (y (find-max x y1 y0))))))

(defthm equal-when-member-and-ubound
  (implies (and (natp y) (elementp x y) (uboundp x y))
    (equal (f x) y))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable f-geq-when-existsp-rewrite)
     :use ((:instance existsp-when-nonempty-and-bounded (y0 y) (y1 y)) (:instance f-geq-when-existsp-rewrite (y1 y))
       (:instance uboundp-necc (y1 (f x)))))))