ordinal-total-order

other

(in-package "ACL2")

include-book

(include-book "ordinal-definitions")

local

(local (disable-forcing))

ocmp-lttheorem

(defthm ocmp-lt (equal (equal (ocmp a b) 'lt) (o< a b)))

ocmp-gttheorem

(defthm ocmp-gt (equal (equal (ocmp a b) 'gt) (o> a b)))

o-rst-<-fctheorem

(defthm o-rst-<-fc
  (implies (and (o< (o-rst a) (o-rst b))
      (equal (o-first-coeff a) (o-first-coeff b))
      (equal (o-first-expt a) (o-first-expt b))
      (o-p a)
      (o-p b))
    (o< a b))
  :rule-classes :forward-chaining)

make-ord-o<-3theorem

(defthm make-ord-o<-3
  (equal (o< (make-ord a b c) (make-ord x y z))
    (cond ((not (equal a x)) (o< a x))
      ((not (equal b y)) (< b y))
      (t (o< c z))))
  :hints (("goal" :in-theory (enable o-rst o-first-expt o-first-coeff o< make-ord))))

o-rst-<theorem

(defthm o-rst-<
  (implies (o< rst1 rst2)
    (o< (make-ord o-first-expt o-first-coeff rst1)
      (make-ord o-first-expt o-first-coeff rst2)))
  :hints (("goal" :in-theory (enable o<))))

o-first-coeff-<-fctheorem

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

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

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

o-first-coeff-<theorem

(defthm o-first-coeff-<
  (implies (and (o-infp b)
      (< (o-first-coeff a) (o-first-coeff b))
      (equal (o-first-expt a) (o-first-expt b)))
    (o< a b))
  :rule-classes ((:rewrite :backchain-limit-lst (3 3 3)) (:forward-chaining :trigger-terms ((< (o-first-coeff a) (o-first-coeff b))))))

|~(a < a)|theorem

(defthm |~(a < a)| (not (o< a a)))

o-first-expt-<theorem

(defthm o-first-expt-<
  (implies (and (o< (o-first-expt a) (o-first-expt b)) (o-p a))
    (o< a b))
  :rule-classes ((:forward-chaining) (:rewrite :backchain-limit-lst 3)))

o-finp-crtheorem

(defthm o-finp-cr
  (equal (o-finp x) (atom x))
  :rule-classes :compound-recognizer)

o-finp-<theorem

(defthm o-finp-<
  (implies (and (o-finp a) (o-finp b) (< a b)) (o< a b))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

o-finp-<-fctheorem

(defthm o-finp-<-fc
  (implies (and (o< a b) (o-finp a) (o-finp b)) (< a b))
  :rule-classes :forward-chaining)

o<-o-finp-o-finptheorem

(defthm o<-o-finp-o-finp
  (implies (and (o< a b) (o-finp b)) (o-finp a))
  :rule-classes :forward-chaining)

ac-<theorem

(defthm ac-<
  (implies (and (o-finp a) (o-infp b)) (o< a b))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

o<=-o-finp-deftheorem

(defthm o<=-o-finp-def
  (implies (and (o-finp a) (o-finp b) (<= a b)) (o<= a b))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

local

(local (in-theory (disable o-first-coeff-< o-first-expt-< o-finp-< ac-<)))

|~(a<0)|theorem

(defthm |~(a<0)|
  (implies (o-p a) (not (o< a 0)))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

|a <= b & ~(a = b) => a < b|theorem

(defthm |a <= b & ~(a = b)  =>  a < b|
  (implies (and (not (equal a b)) (o<= a b) (o-p a) (o-p b))
    (o< a b))
  :rule-classes :forward-chaining)

|a <= b => (a ~(a = b))|theorem

(defthm |a <= b  =>  (a < b <=> ~(a = b))|
  (implies (and (o<= a b) (o-p a) (o-p b))
    (equal (o< a b) (not (equal a b))))
  :rule-classes :forward-chaining)

|a a <= b & ~(a = b)|theorem

(defthm |a < b  =>  a <= b & ~(a = b)|
  (implies (o< a b) (and (o<= a b) (not (equal a b))))
  :rule-classes :forward-chaining)

|a ~(a = b)|theorem

(defthm |a < b  =>  ~(a = b)|
  (implies (o< a b) (not (equal a b))))

|a a<=b|theorem

(defthm |a<b => a<=b|
  (implies (o< a b) (o<= a b))
  :rule-classes :forward-chaining)

o-infp-o-finp-o<=theorem

(defthm o-infp-o-finp-o<=
  (implies (and (o-infp a) (o-finp b)) (o<= b a))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

|a <= b & b <= c => a <= c|theorem

(defthm |a <= b & b <= c  =>  a <= c|
  (implies (and (o<= a b) (o<= b c) (o-p a) (o-p b))
    (o<= a c))
  :rule-classes ((:forward-chaining :trigger-terms ((o< b a) (o< c b)))))

|a a < c|theorem

(defthm |a < b & b < c  =>  a < c|
  (implies (and (o< a b) (o< b c)) (o< a c))
  :rule-classes ((:forward-chaining) (:rewrite :match-free :all :backchain-limit-lst 3)))

|a a < c|theorem

(defthm |a < b & b <= c  =>  a < c|
  (implies (and (o< a b) (o<= b c) (o-p b) (o-p c)) (o< a c))
  :hints (("goal" :use (:instance |a <= b & ~(a = b)  =>  a < b| (b b) (a c))))
  :rule-classes ((:forward-chaining :trigger-terms ((o< a b) (o< c b)))))

|a <= b & b < c => a < c|theorem

(defthm |a <= b & b < c  =>  a < c|
  (implies (and (o< b c) (o<= a b) (o-p a) (o-p c)) (o< a c))
  :rule-classes ((:forward-chaining :trigger-terms ((o< b a) (o< b c)))))

|b <= a & a <= b => a = b|theorem

(defthm |b <= a & a <= b  =>  a = b|
  (implies (and (o<= a b) (o-p a) (o-p b) (o<= b a))
    (equal a b))
  :rule-classes ((:forward-chaining)))

local

(local (defthm ocmp-aux-equal
    (implies (and (o-p a) (o-p b))
      (equal (equal (ocmp-aux a b) 'eq) (equal a b)))
    :rule-classes :forward-chaining))

local

(local (defthm ocmp-aux-lt
    (implies (and (o-p a) (o-p b))
      (equal (equal (ocmp-aux a b) 'lt) (o< a b)))
    :hints (("goal" :induct (ocmp-aux a b)))))

other

(verify-guards ocmp)

in-theory

(in-theory (disable ocmp))

|a = b => (a <= b)|theorem

(defthm |a = b  =>  (a <= b)|
  (implies (equal a b) (o<= a b))
  :rule-classes ((:forward-chaining)))

|0 < a = ~(a = 0)|theorem

(defthm |0 < a  =  ~(a = 0)|
  (implies (o-p a) (equal (o< 0 a) (not (equal a 0))))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

omega-o<theorem

(defthm omega-o<
  (implies (o-p a) (equal (o< a (omega)) (o-finp a)))
  :hints (("goal" :in-theory (enable o<)))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

in-theory

(in-theory (disable |a < b  =>  ~(a = b)|))

ordinal-total-order

Included Books