ordinal-basic-thms

other

(in-package "ACL2")

include-book

(include-book "ordinal-total-order")

local

(local (include-book "top-with-meta"))

local

(local (disable-forcing))

olen-posptheorem

(defthm olen-posp (equal (posp (olen a)) (o-infp a)))

make-ord-o-first-expttheorem

(defthm make-ord-o-first-expt
  (equal (o-first-expt (make-ord a b c)) a))

make-ord-o-first-coefftheorem

(defthm make-ord-o-first-coeff
  (equal (o-first-coeff (make-ord a b c)) b))

make-ord-o-rsttheorem

(defthm make-ord-o-rst (equal (o-rst (make-ord a b c)) c))

make-ord-o-infptheorem

(defthm make-ord-o-infp (o-infp (make-ord a b c)))

make-ord-o-ptheorem

(defthm make-ord-o-p
  (equal (o-p (make-ord o-first-expt o-first-coeff o-rst))
    (and (not (equal o-first-expt 0))
      (posp o-first-coeff)
      (o-p o-first-expt)
      (o-p o-rst)
      (o< (o-first-expt o-rst) o-first-expt))))

o-first-expt-o-first-coeff-o-rst-elimtheorem

(defthm o-first-expt-o-first-coeff-o-rst-elim
  (implies (and (o-infp x) (o-p x))
    (equal (make-ord (o-first-expt x) (o-first-coeff x) (o-rst x))
      x))
  :rule-classes (:rewrite :elim))

make-ord-equal-2theorem

(defthm make-ord-equal-2
  (equal (equal (make-ord a b c) (make-ord x y z))
    (and (equal a x) (equal b y) (equal c z)))
  :hints (("goal" :in-theory (enable make-ord))))

local

(local (defthm make-ord-car
    (implies (and (o-infp a) (consp (car a)))
      (equal (cons (car a) b)
        (make-ord (o-first-expt a) (o-first-coeff a) b)))))

local

(local (defthm make-ord-def-consp
    (equal (cons (cons a b) c) (make-ord a b c))))

in-theory

(in-theory (disable make-ord))

omega-o-infptheorem

(defthm omega-o-infp (o-infp (omega)))

omega-o-ptheorem

(defthm omega-o-p (o-p (omega)))

omega-o-first-expttheorem

(defthm omega-o-first-expt (equal (o-first-expt (omega)) 1))

omega-o-first-coefftheorem

(defthm omega-o-first-coeff
  (equal (o-first-coeff (omega)) 1))

omega-o-rsttheorem

(defthm omega-o-rst (equal (o-rst (omega)) 0))

omega-limitptheorem

(defthm omega-limitp (limitp (omega)))

in-theory

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

o-finp-o-rsttheorem

(defthm o-finp-o-rst
  (implies (o-finp a) (equal (o-rst a) nil)))

acl2-count-o-rsttheorem

(defthm acl2-count-o-rst
  (implies (o-infp a)
    (o< (acl2-count (o-rst a)) (acl2-count a))))

acl2-count-o-rst-2theorem

(defthm acl2-count-o-rst-2
  (implies (o-infp a)
    (< (acl2-count (o-rst a)) (acl2-count a))))

o-first-expt-1-o-finp-o-rsttheorem

(defthm o-first-expt-1-o-finp-o-rst
  (implies (and (equal (o-first-expt a) 1) (o-p a))
    (o-finp (o-rst a)))
  :rule-classes :forward-chaining)

local

(local (defthm cdr-o-rst (equal (cdr a) (o-rst a))))

in-theory

(in-theory (disable o-rst))

o-first-expt-o-ptheorem

(defthm o-first-expt-o-p
  (implies (o-p a) (o-p (o-first-expt a)))
  :rule-classes ((:forward-chaining :trigger-terms ((o-first-expt a))) (:rewrite :backchain-limit-lst (5))))

|(o-first-expt a) < a|theorem

(defthm |(o-first-expt a) < a|
  (implies (o-p a)
    (equal (o< (o-first-expt a) a) (not (equal a 0)))))

o-first-expt-<=theorem

(defthm o-first-expt-<=
  (implies (o-p b) (<= 0 (o-first-expt b)))
  :rule-classes ((:linear)))

o-first-expt-0-natptheorem

(defthm o-first-expt-0-natp
  (implies (o-p a)
    (equal (equal (o-first-expt a) 0) (o-finp a))))

<=-o-first-expt-<=theorem

(defthm <=-o-first-expt-<=
  (implies (and (o<= a b) (o-p b))
    (o<= (o-first-expt a) (o-first-expt b)))
  :rule-classes ((:forward-chaining)))

o-first-expt-natptheorem

(defthm o-first-expt-natp
  (implies (and (equal (o-first-expt a) 0) (o-p a)) (natp a))
  :rule-classes :forward-chaining)

o-first-expt-o-infptheorem

(defthm o-first-expt-o-infp
  (implies (not (equal 0 (o-first-expt b))) (o-infp b))
  :rule-classes (:forward-chaining :rewrite))

o-first-expt-o-infp-2theorem

(defthm o-first-expt-o-infp-2
  (implies (and (o< (o-first-expt b) (o-first-expt a)) (o-p a) (o-p b))
    (o-infp a))
  :rule-classes :forward-chaining)

o-first-expt-def-o-finptheorem

(defthm o-first-expt-def-o-finp
  (implies (o-finp a) (equal (o-first-expt a) 0)))

o-first-expt-equal-o-finptheorem

(defthm o-first-expt-equal-o-finp
  (implies (and (equal (o-first-expt b) 0) (o-p b))
    (o-finp b))
  :rule-classes :forward-chaining)

acl2-count-o-first-expttheorem

(defthm acl2-count-o-first-expt
  (implies (o-infp a)
    (< (acl2-count (o-first-expt a)) (acl2-count a)))
  :hints (("goal" :in-theory (disable cdr-o-rst make-ord-def-consp))))

in-theory

(in-theory (disable o-first-expt))

natp-o-first-coefftheorem

(defthm natp-o-first-coeff
  (implies (o-p a) (natp (o-first-coeff a)))
  :rule-classes ((:forward-chaining :trigger-terms ((o-first-coeff a)))))

posp-o-first-coefftheorem

(defthm posp-o-first-coeff
  (implies (o-p a)
    (equal (posp (o-first-coeff a)) (not (equal a 0))))
  :rule-classes ((:rewrite :backchain-limit-lst 3) (:forward-chaining :trigger-terms ((o-first-coeff a)))))

o-first-coeff-0theorem

(defthm o-first-coeff-0
  (implies (o-p a)
    (equal (equal (o-first-coeff a) 0) (equal a 0)))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

posp-o-first-coeff-2theorem

(defthm posp-o-first-coeff-2
  (implies (o-p a) (or (equal a 0) (posp (o-first-coeff a))))
  :rule-classes ((:forward-chaining :trigger-terms ((o-first-coeff a)))))

o-first-coeff-def-o-finptheorem

(defthm o-first-coeff-def-o-finp
  (implies (o-finp a) (equal (o-first-coeff a) a))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

in-theory

(in-theory (disable o-first-coeff))

o-p-o-infp-cartheorem

(defthm o-p-o-infp-car
  (implies (o-p a) (equal (consp (car a)) (o-infp a)))
  :rule-classes ((:rewrite :backchain-limit-lst 3) (:forward-chaining :trigger-terms ((consp (car a))))))

o-p-o-infp-car-2theorem

(defthm o-p-o-infp-car-2
  (implies (o-p (cons a b)) (consp a))
  :rule-classes :forward-chaining)

o-p-o-first-expt-neq-0theorem

(defthm o-p-o-first-expt-neq-0
  (implies (and (o-infp a) (o-p a))
    (not (equal (o-first-expt a) 0)))
  :rule-classes ((:rewrite :backchain-limit-lst 3) (:forward-chaining :trigger-terms ((o-first-expt a)))))

o-p-o-p-o-rsttheorem

(defthm o-p-o-p-o-rst
  (implies (and (o-infp a) (o-p a)) (o-p (o-rst a)))
  :rule-classes ((:forward-chaining :trigger-terms ((o-rst a)))))

o-p-<-o-first-expt-o-first-expt-o-rsttheorem

(defthm o-p-<-o-first-expt-o-first-expt-o-rst
  (implies (and (o-infp a) (o-p a))
    (o< (o-first-expt (o-rst a)) (o-first-expt a)))
  :rule-classes ((:forward-chaining :trigger-terms ((o-rst a)))))

o-p-def-o-finp-1theorem

(defthm o-p-def-o-finp-1
  (implies (o-finp a) (equal (o-p a) (natp a)))
  :rule-classes ((:rewrite :backchain-limit-lst 3) (:forward-chaining)))

o-p-def-o-finp-2theorem

(defthm o-p-def-o-finp-2
  (implies (and (o-finp a) (o-p a)) (natp a))
  :rule-classes :forward-chaining)

in-theory

(in-theory (disable o-p))

o-infp->neq-0theorem

(defthm o-infp->neq-0
  (implies (o-infp a) (not (equal a 0)))
  :rule-classes ((:forward-chaining) (:rewrite :backchain-limit-lst 3)))

in-theory

(in-theory (disable o-finp))

limitp-o-ptheorem

(defthm limitp-o-p
  (implies (limitp a) (o-p a))
  :rule-classes :forward-chaining)

limitp-o-infptheorem

(defthm limitp-o-infp
  (implies (limitp a) (o-infp a))
  :rule-classes :forward-chaining)

limitp-natparttheorem

(defthm limitp-natpart
  (implies (limitp a) (equal (natpart a) 0))
  :rule-classes :forward-chaining)

not-limitp-natptheorem

(defthm not-limitp-natp
  (implies (and (o-infp a) (o-p a) (not (limitp a)))
    (not (equal (natpart a) 0))))

limitp-o-rsttheorem

(defthm limitp-o-rst
  (implies (limitp b)
    (or (equal (o-rst b) 0) (limitp (o-rst b))))
  :rule-classes :forward-chaining)

limitp-o-infp-o-rsttheorem

(defthm limitp-o-infp-o-rst
  (implies (limitp a)
    (equal (limitp (o-rst a)) (o-infp (o-rst a))))
  :rule-classes :forward-chaining)

limitp-deftheorem

(defthm limitp-def
  (implies (and (o-infp a) (equal (natpart a) 0) (o-p a))
    (limitp a)))

limitp-def-2theorem

(defthm limitp-def-2
  (equal (limitp (make-ord a b c))
    (and (o-p (make-ord a b c)) (equal (natpart c) 0))))

in-theory

(in-theory (disable limitp))

natpart-o-finptheorem

(defthm natpart-o-finp
  (o-finp (natpart a))
  :hints (("goal" :in-theory (enable natpart))))

natpart-natptheorem

(defthm natpart-natp
  (implies (o-p a) (natp (natpart a)))
  :rule-classes :type-prescription)

natpart-def-o-finptheorem

(defthm natpart-def-o-finp
  (implies (o-finp a) (equal (natpart a) a)))

natpart-o-rsttheorem

(defthm natpart-o-rst
  (implies (o-infp a) (equal (natpart a) (natpart (o-rst a))))
  :rule-classes ((:forward-chaining :trigger-terms ((natpart (o-rst a))))))

natpart-make-ordtheorem

(defthm natpart-make-ord
  (equal (natpart (make-ord a b c)) (natpart c)))

limitpart-o-first-expttheorem

(defthm limitpart-o-first-expt
  (equal (o-first-expt (limitpart a)) (o-first-expt a))
  :hints (("goal" :expand (limitpart a))))

limitpart-o-first-coefftheorem

(defthm limitpart-o-first-coeff
  (implies (o-infp a)
    (equal (o-first-coeff (limitpart a)) (o-first-coeff a)))
  :hints (("goal" :expand (limitpart a))))

limitpart-o-rsttheorem

(defthm limitpart-o-rst
  (implies (o-infp a)
    (equal (o-rst (limitpart a)) (limitpart (o-rst a))))
  :hints (("goal" :expand (limitpart a))))

limitpart-def-o-finptheorem

(defthm limitpart-def-o-finp
  (implies (o-finp a) (equal (limitpart a) 0)))

limitpart-olentheorem

(defthm limitpart-olen
  (equal (olen (limitpart a)) (olen a)))

limitpart-o-finptheorem

(defthm limitpart-o-finp
  (equal (o-finp (limitpart a)) (o-finp a)))

limitpart-o-ptheorem

(defthm limitpart-o-p
  (implies (o-p a) (o-p (limitpart a)))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

other

(verify-guards limitpart)

natpart-limitparttheorem

(defthm natpart-limitpart (equal (natpart (limitpart a)) 0))

limitpart-limitptheorem

(defthm limitpart-limitp
  (implies (o-p a) (equal (limitp (limitpart a)) (o-infp a))))

limitpart-limitp-tptheorem

(defthm limitpart-limitp-tp
  (implies (and (o-infp a) (o-p a)) (limitp (limitpart a))))

in-theory

(in-theory (disable limitpart natpart))

o-p-o-last-expttheorem

(defthm o-p-o-last-expt
  (implies (o-p a) (o-p (o-last-expt a)))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

o-last-expt-o-first-expt-2theorem

(defthm o-last-expt-o-first-expt-2
  (implies (o-p a) (o<= (o-last-expt a) (o-first-expt a)))
  :rule-classes ((:forward-chaining :trigger-terms ((o-last-expt a))) (:rewrite)))

o-last-expt-0theorem

(defthm o-last-expt-0
  (implies (o-p a)
    (equal (equal (o-last-expt a) 0) (o-finp a))))

o-last-expt-def-o-infp-1theorem

(defthm o-last-expt-def-o-infp-1
  (implies (o-infp (o-rst a))
    (equal (o-last-expt a) (o-last-expt (o-rst a))))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

o-last-expt-def-o-infp-2theorem

(defthm o-last-expt-def-o-infp-2
  (implies (and (o-infp a) (o-finp (o-rst a)))
    (equal (o-last-expt a) (o-first-expt a))))

in-theory

(in-theory (disable o-last-expt))

o-p-dropntheorem

(defthm o-p-dropn (implies (o-p a) (o-p (dropn n a))))

dropn-new-deftheorem

(defthm dropn-new-def
  (equal (dropn n a)
    (if (or (o-finp a) (zp n))
      a
      (dropn (1- n) (o-rst a))))
  :hints (("goal" :in-theory (enable o-finp)))
  :rule-classes :definition)

in-theory

(in-theory (disable dropn))

other

(verify-guards count2)

ordinal-basic-thms

Included Books