ordinal-isomorphism

Included Books

other

(in-package "ACL2")

include-book

(include-book "ordinal-addition")

local

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

local

(local (disable-forcing))

local

(local (in-theory (disable zp-open o+ o<)))

e0-ord-<function

(defun e0-ord-<
  (x y)
  "< for the old acl2 ordinals"
  (declare (xargs :guard t))
  (if (consp x)
    (if (consp y)
      (if (e0-ord-< (car x) (car y))
        t
        (if (equal (car x) (car y))
          (e0-ord-< (cdr x) (cdr y))
          nil))
      nil)
    (if (consp y)
      t
      (< (if (real/rationalp x)
          x
          0)
        (if (real/rationalp y)
          y
          0)))))

e0-ordinalpfunction

(defun e0-ordinalp
  (x)
  "The old acl2 ordinal definition"
  (declare (xargs :guard t))
  (if (consp x)
    (and (e0-ordinalp (car x))
      (not (equal (car x) 0))
      (e0-ordinalp (cdr x))
      (or (atom (cdr x)) (not (e0-ord-< (car x) (cadr x)))))
    (and (integerp x) (>= x 0))))

local

(local (defthm open-zp
    (implies (syntaxp (not (variablep x)))
      (equal (zp x) (not (posp x))))))

copynfunction

(defun copyn
  (a n)
  (declare (xargs :guard (natp n)))
  (if (zp n)
    nil
    (cons a (copyn a (1- n)))))

local

(local (defthm acl2-count-o-first-expt
    (implies (o-infp a)
      (< (acl2-count (o-first-expt a)) (acl2-count a)))
    :hints (("goal" :in-theory (enable o-first-expt)))))

ctoafunction

(defun ctoa
  (x)
  (declare (xargs :guard (o-p x)))
  (if (o-finp x)
    x
    (append (copyn (ctoa (o-first-expt x)) (o-first-coeff x))
      (ctoa (o-rst x)))))

local

(local (defthm |x a<  y  =>  ~(y a< x)|
    (implies (e0-ord-< x y) (not (e0-ord-< y x)))
    :rule-classes :forward-chaining))

local

(local (defthm car-app-copyn
    (implies (posp n) (equal (car (append (copyn x n) y)) x))
    :hints (("goal" :expand (copyn x n)))))

local

(local (defthm posp-consp
    (implies (posp x) (consp (copyn y x)))
    :hints (("goal" :expand (copyn y x)))
    :rule-classes ((:type-prescription) (:rewrite))))

local

(local (defthm consp-append
    (implies (consp a) (consp (append a b)))))

local

(local (defthm cnf-cons
    (implies (and (o-p y) (o-infp y)) (consp (ctoa y)))
    :hints (("goal" :expand (ctoa y)))
    :rule-classes ((:type-prescription) (:rewrite))))

ctoa-def-atomtheorem

(defthm ctoa-def-atom
  (implies (and (o-p a) (atom (ctoa a))) (equal (ctoa a) a))
  :hints (("goal" :expand (ctoa a) :do-not-induct t)))

local

(local (defthm ctoa-car
    (implies (and (o-infp a) (o-p a))
      (equal (car (ctoa a)) (ctoa (o-first-expt a))))))

local

(local (defthm cnf-l1
    (implies (and (o-infp x)
        (o-infp y)
        (e0-ord-< (ctoa (o-first-expt x)) (ctoa (o-first-expt y)))
        (o-p x)
        (o-p y)
        (o< (o-first-expt x) (o-first-expt y)))
      (e0-ord-< (ctoa x) (ctoa y)))
    :hints (("goal" :expand ((ctoa x) (ctoa y))))))

local

(local (defun i2
    (n1 n2)
    (if (zp n2)
      n1
      (i2 (- n1 1) (- n2 1)))))

local

(local (defthm copyn-<-2
    (implies (and (<= w v) (natp w) (natp v))
      (equal (e0-ord-< (append (copyn z w) cx) (append (copyn z v) cy))
        (e0-ord-< cx (append (copyn z (- v w)) cy))))
    :hints (("goal" :induct (i2 v w)))))

acl2-count-o-infptheorem

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

local

(local (defthm i1-lemma-1
    (implies (o-infp a)
      (< (acl2-count (o-first-expt (o-rst a))) (acl2-count a)))
    :instructions (promote (claim (< (acl2-count (o-rst a)) (acl2-count a)))
      (casesplit (o-finp (o-rst a)))
      bash
      (claim (< (acl2-count (o-first-expt (o-rst a)))
          (acl2-count (o-rst a))))
      bash)))

local

(local (defun i1
    (x y)
    (if (and (o-infp x) (o-infp y))
      (if (equal (o-first-expt x) (o-first-expt y))
        (if (equal (o-first-coeff x) (o-first-coeff y))
          (i1 (o-rst x) (o-rst y))
          (i1 (o-first-expt (o-rst x)) (o-first-expt y)))
        (i1 (o-first-expt x) (o-first-expt y)))
      (cons x y))))

local

(local (defthm app-copyn-1
    (implies (consp (copyn z x))
      (equal (car (append (copyn z x) y)) z))))

local

(local (encapsulate nil
    (local (defthm o<-e0-ord-<-helper2
        (implies (and (o-infp y)
            (equal (o-first-expt x) (o-first-expt y))
            (not (equal (o-first-coeff x) (o-first-coeff y)))
            (e0-ord-< (ctoa (o-first-expt (o-rst x)))
              (ctoa (o-first-expt x)))
            (o-p x)
            (o-p y)
            (< (o-first-coeff x) (o-first-coeff y)))
          (e0-ord-< (append (copyn (ctoa (o-first-expt x)) (o-first-coeff x))
              (ctoa (o-rst x)))
            (ctoa y)))
        :hints (("goal" :expand ((ctoa y) (ctoa (o-rst x)))))))
    (defthm o<-e0-ord-<
      (implies (and (o-p x) (o-p y) (o< x y))
        (e0-ord-< (ctoa x) (ctoa y)))
      :hints (("goal" :induct (i1 x y))))))

local

(local (encapsulate nil
    (local (defthm e0-ord-app-copyn-helper
        (implies (and (e0-ordinalp (append (copyn z (+ -1 x)) n))
            (posp x)
            (natp n)
            (not (equal z 0))
            (e0-ordinalp z)
            (consp (append (copyn z (+ -1 x)) n)))
          (not (e0-ord-< z (car (append (copyn z (+ -1 x)) n)))))
        :hints (("goal" :cases ((posp (+ -1 x)))))
        :rule-classes ((:rewrite :match-free :all))))
    (defthm e0-ord-app-copyn
      (implies (and (posp x) (natp n) (not (equal z 0)) (e0-ordinalp z))
        (e0-ordinalp (append (copyn z x) n))))))

local

(local (defun nat-ind
    (n)
    (if (zp n)
      1
      (cons n (nat-ind (1- n))))))

local

(local (encapsulate nil
    (local (defthm e0-ordp-app-copy-helper
        (implies (and (not (zp n))
            (e0-ordinalp (append (copyn x (+ -1 n)) y))
            (not (equal x 0))
            (e0-ordinalp x)
            (e0-ordinalp y)
            (e0-ord-< (car y) x)
            (consp (append (copyn x (+ -1 n)) y)))
          (not (e0-ord-< x (car (append (copyn x (+ -1 n)) y)))))
        :hints (("goal" :cases ((zp (+ -1 n)))))
        :rule-classes ((:rewrite :match-free :all))))
    (defthm e0-ordp-app-copy
      (implies (and (not (equal x 0))
          (e0-ordinalp x)
          (e0-ordinalp y)
          (e0-ord-< (car y) x))
        (e0-ordinalp (append (copyn x n) y)))
      :hints (("goal" :induct (nat-ind n))))))

local

(local (defthm consp-neq-0 (implies (consp a) (not (equal a 0)))))

local

(local (defthm cnf-0
    (implies (o-p x) (equal (equal (ctoa x) 0) (equal x 0)))))

|oc.x <=> oa(ctoa.x)|encapsulate

(encapsulate nil
  (local (defthm |oc.x  <=>  oa(ctoa.x) :helper|
      (implies (and (o-infp x)
          (e0-ordinalp (ctoa (o-first-expt x)))
          (e0-ordinalp (ctoa (o-rst x)))
          (o-p x))
        (e0-ordinalp (append (copyn (ctoa (o-first-expt x)) (o-first-coeff x))
            (ctoa (o-rst x)))))
      :hints (("goal" :cases ((o-infp (o-rst x)))))))
  (defthm |oc.x  <=>  oa(ctoa.x)|
    (implies (o-p x) (e0-ordinalp (ctoa x)))
    :rule-classes ((:forward-chaining) (:rewrite))))

atocfunction

(defun atoc
  (a)
  (declare (xargs :guard (e0-ordinalp a) :verify-guards nil))
  (if (atom a)
    a
    (o+ (omega-term (atoc (car a)) 1) (atoc (cdr a)))))

local

(local (in-theory (enable o+)))

local

(local (defthm o-infp-o-finp-o<=-2
    (implies (and (o-infp a) (o-finp b)) (o<= b a))
    :hints (("goal" :in-theory (enable o<)))))

local

(local (defthm ateo-neq-0
    (implies (and (not (equal a 0)) (e0-ordinalp a))
      (not (equal 0 (atoc a))))))

local

(local (in-theory (disable o+)))

|oa.x <=> oc(atoc.x)|theorem

(defthm |oa.x  <=>  oc(atoc.x)|
  (implies (e0-ordinalp x) (o-p (atoc x)))
  :hints (("goal" :induct (atoc x))))

other

(verify-guards atoc)

local

(local (defthm consp-atoc
    (implies (and (consp a) (e0-ordinalp a)) (o-infp (atoc a)))))

local

(local (defthm e0-total-order
    (implies (and (not (equal a b))
        (not (e0-ord-< a b))
        (e0-ordinalp a)
        (e0-ordinalp b))
      (e0-ord-< b a))
    :rule-classes :forward-chaining))

local

(local (defun ci
    (x y)
    (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
    (if (and (consp x) (consp y))
      (list (ci (cdr x) y)
        (ci x (cdr y))
        (ci (cadr x) (car x))
        (ci (cadr y) (car y))
        (ci (car x) (car y))
        (ci (cdr x) (cdr y)))
      (list x y))))

local

(local (defthm |x a< y  =>  ~(y a< y)|
    (implies (e0-ord-< x y) (not (e0-ord-< y x)))
    :rule-classes :forward-chaining))

local

(local (encapsulate nil
    (local (encapsulate nil
        (local (defthm e0-ord-<-o<-help1a
            (implies (and (equal (o-first-expt (atoc (cdr x))) (atoc (cadr x)))
                (not (e0-ord-< (car x) (cadr x)))
                (not (e0-ord-< (cadr x) (car x)))
                (consp x)
                (consp y)
                (e0-ordinalp (car x))
                (not (equal (car x) 0))
                (e0-ordinalp (cdr x))
                (e0-ordinalp y))
              (equal (o-first-expt (o+ (make-ord (atoc (car x)) 1 0) (atoc (cdr x))))
                (atoc (car x))))
            :hints (("goal" :use ((:instance e0-total-order (a (cadr x)) (b (car x))) (:instance o+-o-first-expt-2
                   (a (make-ord (atoc (car x)) 1 0))
                   (b (atoc (cdr x)))))
               :in-theory (disable e0-total-order o+-o-first-expt-2)))
            :rule-classes ((:rewrite :match-free :all))))
        (defthm e0-ord-<-o<-help1
          (implies (and (consp x)
              (consp y)
              (e0-ordinalp x)
              (e0-ordinalp y)
              (implies (and (consp (cdr x))
                  (consp y)
                  (e0-ordinalp (cdr x))
                  (e0-ordinalp y))
                (equal (o-first-expt (atoc (cdr x))) (atoc (cadr x))))
              (implies (and (consp (cadr x))
                  (consp (car x))
                  (e0-ordinalp (cadr x))
                  (e0-ordinalp (car x)))
                (implies (e0-ord-< (cadr x) (car x))
                  (o< (atoc (cadr x)) (atoc (car x))))))
            (equal (o-first-expt (atoc x)) (atoc (car x))))
          :hints (("goal" :do-not-induct t))
          :rule-classes nil)))
    (local (defthm e0-ord-<-o<-help2a
        (implies (and (equal (o-first-expt (o+ (make-ord (atoc (car x)) 1 0) (cdr x)))
              (atoc (car x)))
            (equal (o-first-expt (o+ (make-ord (atoc (car y)) 1 0) (atoc (cdr y))))
              (atoc (car y)))
            (equal (car x) (car y))
            (not (e0-ord-< (car x) (car y)))
            (e0-ordinalp (car x))
            (not (equal (car x) 0))
            (e0-ordinalp (cdr x))
            (not (consp (cdr x)))
            (e0-ordinalp (car y))
            (not (equal (car y) 0))
            (e0-ordinalp (cdr y))
            (not (e0-ord-< (car y) (cadr y)))
            (consp (cdr y))
            (o-infp (atoc (cdr y)))
            (consp x)
            (consp y))
          (o< (o+ (make-ord (atoc (car x)) 1 0) (cdr x))
            (o+ (make-ord (atoc (car x)) 1 0) (atoc (cdr y)))))
        :hints (("goal" :use ((:instance |a < b  <=>  c+a < c+b|
              (a (cdr x))
              (b (atoc (cdr y)))
              (c (make-ord (atoc (car x)) 1 0))))))))
    (local (defthm e0-ord-<-o<-help2
        (implies (and (consp x)
            (consp y)
            (e0-ordinalp x)
            (e0-ordinalp y)
            (equal (o-first-expt (atoc x)) (atoc (car x)))
            (equal (o-first-expt (atoc y)) (atoc (car y)))
            (implies (e0-ord-< (car x) (car y))
              (o< (atoc (car x)) (atoc (car y))))
            (implies (e0-ord-< (cdr x) (cdr y))
              (o< (atoc (cdr x)) (atoc (cdr y))))
            (e0-ord-< x y))
          (o< (atoc x) (atoc y)))
        :rule-classes nil))
    (local (defthm e0-ord-<-o<-lemma
        (implies (and (e0-ordinalp x) (e0-ordinalp y) (consp x) (consp y))
          (and (equal (o-first-expt (atoc x)) (atoc (car x)))
            (equal (o-first-expt (atoc y)) (atoc (car y)))
            (implies (e0-ord-< x y) (o< (atoc x) (atoc y)))))
        :rule-classes ((:rewrite :match-free :all))
        :instructions ((induct (ci x y)) (promote)
          (claim (equal (o-first-expt (atoc x)) (atoc (car x)))
            :hints (("goal" :by e0-ord-<-o<-help1)))
          (claim (equal (o-first-expt (atoc y)) (atoc (car y)))
            :hints (("goal" :by (:instance e0-ord-<-o<-help1 (x y) (y x)))))
          (s)
          (promote)
          (use e0-ord-<-o<-help2)
          (promote)
          (drop 2 3 4 5 6 7)
          (demote 1)
          (dive 1 1)
          (s-prop)
          (top)
          (casesplit (equal (car x) (car y)))
          (bash)
          (demote 9)
          (dv 1)
          (expand)
          (s)
          (top)
          (promote)
          (dive 1 1 1)
          (s)
          (up)
          (s)
          (top)
          (casesplit (consp (car x)))
          (claim (consp (car y)))
          (bash)
          (drop 1 2)
          (bash))))
    (defthm e0-ord-<-o<
      (implies (and (e0-ordinalp x) (e0-ordinalp y) (e0-ord-< x y))
        (o< (atoc x) (atoc y)))
      :hints (("goal" :do-not-induct t :use e0-ord-<-o<-lemma)))
    (defthm o-first-expt-atoc
      (implies (and (consp x) (e0-ordinalp x))
        (equal (o-first-expt (atoc x)) (atoc (car x)))))))

local

(local (defthm atoc-not-<
    (implies (and (not (e0-ord-< a b)) (e0-ordinalp a) (e0-ordinalp b))
      (not (o< (atoc a) (atoc b))))
    :instructions (pro (casesplit (equal a b))
      (= a b)
      bash
      (claim (e0-ord-< b a) :hints (("goal" :use e0-total-order)))
      (claim (o< (atoc b) (atoc a)))
      bash)))

local

(local (defun ind
    (x y)
    (if (atom y)
      (cons x y)
      (ind x (cdr y)))))

local

(local (defthm ctoa-o+
    (implies (and (o-p a)
        (not (equal a 0))
        (o-p b)
        (not (o< a (o-first-expt b))))
      (equal (ctoa (o+ (make-ord a 1 0) b))
        (cons (ctoa a) (ctoa b))))
    :instructions (pro (claim (o-p (make-ord a 1 0)))
      (claim (not (o< (o-first-expt (make-ord a 1 0)) (o-first-expt b))))
      (induct (ind a b))
      pro
      (casesplit (equal (o-first-expt b) a))
      (claim (equal (o-first-expt (make-ord a 1 0)) (o-first-expt b)))
      (dv 1)
      x
      top
      bash
      (claim (o< (o-first-expt b) (o-first-expt (make-ord a 1 0))))
      (dv 1)
      x
      (dv 1)
      x
      top
      bash
      bash)))

|oa.x => ctoa(atoc.x) = x|theorem

(defthm |oa.x  =>  ctoa(atoc.x) = x|
  (implies (e0-ordinalp x) (equal (ctoa (atoc x)) x))
  :instructions ((induct (atoc x)) (pro)
    (claim (e0-ordinalp (car x)))
    (claim (e0-ordinalp (cdr x)))
    (dv 1 1)
    x
    up
    (rewrite ctoa-o+)
    top
    bash
    bash
    bash
    bash
    bash
    (casesplit (atom (cdr x)))
    bash
    (dive 1 2)
    (rewrite o-first-expt-atoc)
    (claim (not (e0-ord-< (car x) (cadr x))))
    (claim (e0-ordinalp (cadr x)))
    top
    bash
    bash))

ctoa-=-equivtheorem

(defthm ctoa-=-equiv
  (implies (and (o-p x) (o-p y))
    (equal (equal (ctoa x) (ctoa y)) (equal x y)))
  :hints (("goal" :do-not-induct t
     :use ((:instance o<-e0-ord-< (x y) (y x)) (:instance o<-e0-ord-<)))))

atoc-=-equivtheorem

(defthm atoc-=-equiv
  (implies (and (e0-ordinalp x) (e0-ordinalp y))
    (equal (equal (atoc x) (atoc y)) (equal x y)))
  :hints (("goal" :do-not-induct t
     :use ((:instance e0-ord-<-o< (x y) (y x)) (:instance e0-ord-<-o<)))))

|oc.x => atoc(ctoa.x) = x|theorem

(defthm |oc.x  =>  atoc(ctoa.x) = x|
  (implies (o-p x) (equal (atoc (ctoa x)) x))
  :hints (("goal" :in-theory (disable ctoa-=-equiv)
     :use ((:instance ctoa-=-equiv (x (atoc (ctoa x))) (y x))))))

ctoa-<-equivtheorem

(defthm ctoa-<-equiv
  (implies (and (o-p x) (o-p y))
    (equal (e0-ord-< (ctoa x) (ctoa y)) (o< x y)))
  :hints (("goal" :use ((:instance e0-ord-<-o< (x (ctoa x)) (y (ctoa y)))))))

atoc-<-equivtheorem

(defthm atoc-<-equiv
  (implies (and (e0-ordinalp x) (e0-ordinalp y))
    (equal (o< (atoc x) (atoc y)) (e0-ord-< x y)))
  :hints (("goal" :use ((:instance o<-e0-ord-< (x (atoc x)) (y (atoc y)))))))

e0-ordinal-well-foundedtheorem

(defthm e0-ordinal-well-founded
  (and (implies (e0-ordinalp x) (o-p (atoc x)))
    (implies (and (e0-ordinalp x) (e0-ordinalp y) (e0-ord-< x y))
      (o< (atoc x) (atoc y))))
  :rule-classes :well-founded-relation)