Theory "ordinalNotation"

Signature

Definitions

cf1_def

⊢ (∀v0 b. cf1 (End v0) b = 0) ∧
  ∀e1 c1 k1 b.
    cf1 (Plus e1 c1 k1) b = if ord_less (expt b) e1 then 1 + cf1 k1 b else 0

cf2_def

⊢ ∀a b n. cf2 a b n = n + cf1 (restn a n) b

coeff_def

⊢ (∀x. coeff (End x) = x) ∧ ∀e k t. coeff (Plus e k t) = k

expt_def

⊢ (∀v0. expt (End v0) = End 0) ∧ ∀e k t. expt (Plus e k t) = e

finp_def

⊢ (∀v0. finp (End v0) ⇔ T) ∧ ∀v1 v2 v3. finp (Plus v1 v2 v3) ⇔ F

is_ord_def

⊢ is_ord =
  (λa0.
       ∀is_ord'.
         (∀a0.
            (∃k. a0 = End k) ∨
            (∃e k t.
               (a0 = Plus e k t) ∧ is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord' t ∧
               oless (expt t) e) ⇒
            is_ord' a0) ⇒
         is_ord' a0)

oless_def

⊢ oless =
  (λa0 a1.
       ∀oless'.
         (∀a0 a1.
            (∃k1 k2. (a0 = End k1) ∧ (a1 = End k2) ∧ k1 < k2) ∨
            (∃k1 e2 k2 t2. (a0 = End k1) ∧ (a1 = Plus e2 k2 t2)) ∨
            (∃e1 k1 t1 e2 k2 t2.
               (a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ oless' e1 e2) ∨
            (∃e1 k1 t1 e2 k2 t2.
               (a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ (e1 = e2) ∧
               k1 < k2) ∨
            (∃e1 k1 t1 e2 k2 t2.
               (a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ (e1 = e2) ∧
               (k1 = k2) ∧ oless' t1 t2) ⇒
            oless' a0 a1) ⇒
         oless' a0 a1)

ord_less_def

⊢ ∀x y. ord_less x y ⇔ is_ord x ∧ is_ord y ∧ oless x y

osyntax_TY_DEF

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('osyntax').
             (∀a0'.
                (∃a. a0' = (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM)) a) ∨
                (∃a0 a1 a2.
                   (a0' =
                    (λa0 a1 a2.
                         ind_type$CONSTR (SUC 0) a1
                           (ind_type$FCONS a0
                              (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))) a0
                      a1 a2) ∧ $var$('osyntax') a0 ∧ $var$('osyntax') a2) ⇒
                $var$('osyntax') a0') ⇒
             $var$('osyntax') a0') rep

osyntax_case_def

⊢ (∀a f f1. osyntax_CASE (End a) f f1 = f a) ∧
  ∀a0 a1 a2 f f1. osyntax_CASE (Plus a0 a1 a2) f f1 = f1 a0 a1 a2

osyntax_size_def

⊢ (∀a. osyntax_size (End a) = 1 + a) ∧
  ∀a0 a1 a2.
    osyntax_size (Plus a0 a1 a2) =
    1 + (osyntax_size a0 + (a1 + osyntax_size a2))

padd_def

⊢ (∀a b. padd a b 0 = ord_add a b) ∧
  ∀a b n. padd a b (SUC n) = Plus (expt a) (coeff a) (padd (tail a) b n)

rank_def

⊢ (∀v0. rank (End v0) = 0) ∧ ∀e k t. rank (Plus e k t) = 1 + rank e

restn_def

⊢ (∀a. restn a 0 = a) ∧ ∀a n. restn a (SUC n) = restn (tail a) n

tail_def

⊢ ∀e k t. tail (Plus e k t) = t

Theorems

WF_ord_less

⊢ WF ord_less

datatype_osyntax

⊢ DATATYPE (osyntax End Plus)

decompose_plus

⊢ ∀e k t.
    is_ord (Plus e k t) ⇒
    is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ oless (expt t) e

e0_INDUCTION

⊢ ∀P f. (∀x. (∀y. ord_less (f y) (f x) ⇒ P y) ⇒ P x) ⇒ ∀x. P x

e0_RECURSION

⊢ ∀f. ∃!g. ∀x. g x = M (RESTRICT g (λx y. ord_less (f x) (f y)) x) x

is_ord_cases

⊢ ∀a0.
    is_ord a0 ⇔
    (∃k. a0 = End k) ∨
    ∃e k t.
      (a0 = Plus e k t) ∧ is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧
      oless (expt t) e

is_ord_coeff_pos

⊢ ∀x. ¬finp x ∧ is_ord x ⇒ 0 < coeff x

is_ord_downclosed

⊢ is_ord (Plus w k t) ⇒ is_ord w ∧ is_ord t

is_ord_equations

⊢ (is_ord (End k) ⇔ T) ∧
  (is_ord (Plus e k t) ⇔
   is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ oless (expt t) e)

is_ord_expt_closed

⊢ ∀x. is_ord x ⇒ is_ord (expt x)

is_ord_ind

⊢ ∀is_ord'.
    (∀k. is_ord' (End k)) ∧
    (∀e k t.
       is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord' t ∧ oless (expt t) e ⇒
       is_ord' (Plus e k t)) ⇒
    ∀a0. is_ord a0 ⇒ is_ord' a0

is_ord_rules

⊢ (∀k. is_ord (End k)) ∧
  ∀e k t.
    is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ oless (expt t) e ⇒
    is_ord (Plus e k t)

is_ord_strong_ind

⊢ ∀is_ord'.
    (∀k. is_ord' (End k)) ∧
    (∀e k t.
       is_ord e ∧ is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ is_ord' t ∧
       oless (expt t) e ⇒
       is_ord' (Plus e k t)) ⇒
    ∀a0. is_ord a0 ⇒ is_ord' a0

is_ord_strongind

⊢ ∀is_ord'.
    (∀k. is_ord' (End k)) ∧
    (∀e k t.
       is_ord e ∧ is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ is_ord' t ∧
       oless (expt t) e ⇒
       is_ord' (Plus e k t)) ⇒
    ∀a0. is_ord a0 ⇒ is_ord' a0

is_ord_tail_closed

⊢ ∀x. ¬finp x ∧ is_ord x ⇒ is_ord (tail x)

lemma

⊢ ∀n P.
    (∃x. is_ord x ∧ P x ∧ rank x ≤ n) ⇒
    ∃m. is_ord m ∧ P m ∧ rank m ≤ n ∧
        ∀y. is_ord y ∧ rank y ≤ n ∧ oless y m ⇒ ¬P y

main_lemma

⊢ ∀P. (∃x. P x ∧ is_ord x) ⇒
      ∃x. P x ∧ is_ord x ∧ ∀y. is_ord y ∧ oless y x ⇒ ¬P y

oless_End_End

⊢ ∀k1 k2. oless (End k1) (End k2) ⇒ k1 < k2

oless_antirefl

⊢ ∀x. is_ord x ⇒ ¬oless x x

oless_antisym

⊢ ∀x y. is_ord x ∧ is_ord y ∧ oless x y ⇒ ¬oless y x

oless_cases

⊢ ∀a0 a1.
    oless a0 a1 ⇔
    (∃k1 k2. (a0 = End k1) ∧ (a1 = End k2) ∧ k1 < k2) ∨
    (∃k1 e2 k2 t2. (a0 = End k1) ∧ (a1 = Plus e2 k2 t2)) ∨
    (∃e1 k1 t1 e2 k2 t2.
       (a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ oless e1 e2) ∨
    (∃e1 k1 t1 e2 k2 t2.
       (a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ (e1 = e2) ∧ k1 < k2) ∨
    ∃e1 k1 t1 e2 k2 t2.
      (a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ (e1 = e2) ∧ (k1 = k2) ∧
      oless t1 t2

oless_equations

⊢ (oless (End m) (End n) ⇔ m < n) ∧ (oless (End m) (Plus e k t) ⇔ T) ∧
  (oless (Plus e k t) (End m) ⇔ F) ∧
  (oless (Plus e1 k1 t1) (Plus e2 k2 t2) ⇔
   if oless e1 e2 then T
   else if (e1 = e2) ∧ k1 < k2 then T
   else if (e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 then T
   else F)

oless_expt

⊢ ∀e k t. is_ord (Plus e k t) ⇒ oless e (Plus e k t)

oless_imp_rank_leq

⊢ ∀x y. is_ord x ∧ is_ord y ∧ oless x y ⇒ rank x ≤ rank y

oless_ind

⊢ ∀oless'.
    (∀k1 k2. k1 < k2 ⇒ oless' (End k1) (End k2)) ∧
    (∀k1 e2 k2 t2. oless' (End k1) (Plus e2 k2 t2)) ∧
    (∀e1 k1 t1 e2 k2 t2. oless' e1 e2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
    (∀e1 k1 t1 e2 k2 t2.
       (e1 = e2) ∧ k1 < k2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
    (∀e1 k1 t1 e2 k2 t2.
       (e1 = e2) ∧ (k1 = k2) ∧ oless' t1 t2 ⇒
       oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
    ∀a0 a1. oless a0 a1 ⇒ oless' a0 a1

oless_rules

⊢ (∀k1 k2. k1 < k2 ⇒ oless (End k1) (End k2)) ∧
  (∀k1 e2 k2 t2. oless (End k1) (Plus e2 k2 t2)) ∧
  (∀e1 k1 t1 e2 k2 t2. oless e1 e2 ⇒ oless (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
  (∀e1 k1 t1 e2 k2 t2.
     (e1 = e2) ∧ k1 < k2 ⇒ oless (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
  ∀e1 k1 t1 e2 k2 t2.
    (e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 ⇒
    oless (Plus e1 k1 t1) (Plus e2 k2 t2)

oless_strong_ind

⊢ ∀oless'.
    (∀k1 k2. k1 < k2 ⇒ oless' (End k1) (End k2)) ∧
    (∀k1 e2 k2 t2. oless' (End k1) (Plus e2 k2 t2)) ∧
    (∀e1 k1 t1 e2 k2 t2.
       oless e1 e2 ∧ oless' e1 e2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
    (∀e1 k1 t1 e2 k2 t2.
       (e1 = e2) ∧ k1 < k2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
    (∀e1 k1 t1 e2 k2 t2.
       (e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 ∧ oless' t1 t2 ⇒
       oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
    ∀a0 a1. oless a0 a1 ⇒ oless' a0 a1

oless_strongind

⊢ ∀oless'.
    (∀k1 k2. k1 < k2 ⇒ oless' (End k1) (End k2)) ∧
    (∀k1 e2 k2 t2. oless' (End k1) (Plus e2 k2 t2)) ∧
    (∀e1 k1 t1 e2 k2 t2.
       oless e1 e2 ∧ oless' e1 e2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
    (∀e1 k1 t1 e2 k2 t2.
       (e1 = e2) ∧ k1 < k2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
    (∀e1 k1 t1 e2 k2 t2.
       (e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 ∧ oless' t1 t2 ⇒
       oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
    ∀a0 a1. oless a0 a1 ⇒ oless' a0 a1

oless_tail

⊢ ∀x. is_ord x ∧ ¬finp x ⇒ oless (tail x) x

ord_add_def

⊢ (∀n m. ord_add (End m) (End n) = End (m + n)) ∧
  (∀t p m k. ord_add (End m) (Plus p k t) = Plus p k t) ∧
  (∀t m k e. ord_add (Plus e k t) (End m) = Plus e k (ord_add t (End m))) ∧
  ∀t2 t1 k2 k1 e2 e1.
    ord_add (Plus e1 k1 t1) (Plus e2 k2 t2) =
    if oless e1 e2 then Plus e2 k2 t2
    else if e1 = e2 then Plus e2 (k1 + k2) t2
    else Plus e1 k1 (ord_add t1 (Plus e2 k2 t2))

ord_add_ind

⊢ ∀P. (∀m n. P (End m) (End n)) ∧ (∀m p k t. P (End m) (Plus p k t)) ∧
      (∀e k t m. P t (End m) ⇒ P (Plus e k t) (End m)) ∧
      (∀e1 k1 t1 e2 k2 t2.
         (¬oless e1 e2 ∧ e1 ≠ e2 ⇒ P t1 (Plus e2 k2 t2)) ⇒
         P (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
      ∀v v1. P v v1

ord_mult_def

⊢ ∀y x.
    ord_mult x y =
    if (x = End 0) ∨ (y = End 0) then End 0
    else
      case (x,y) of
        (End m,End n) => End (m * n)
      | (End m,Plus e k t) => Plus (ord_add (End 0) e) k (ord_mult (End m) t)
      | (Plus e' k' t',End n') => Plus e' (k' * n') t'
      | (Plus e' k' t',Plus e2 k2 t2) =>
        Plus (ord_add e' e2) k2 (ord_mult (Plus e' k' t') t2)

ord_mult_ind

⊢ ∀P. (∀x y.
         (∀v v1 m e k t.
            ¬((x = End 0) ∨ (y = End 0)) ∧ ((x,y) = (v,v1)) ∧ (v = End m) ∧
            (v1 = Plus e k t) ⇒
            P (End m) t) ∧
         (∀v v1 e' k' t' e2 k2 t2.
            ¬((x = End 0) ∨ (y = End 0)) ∧ ((x,y) = (v,v1)) ∧
            (v = Plus e' k' t') ∧ (v1 = Plus e2 k2 t2) ⇒
            P (Plus e' k' t') t2) ⇒
         P x y) ⇒
      ∀v v1. P v v1

ord_sub_def

⊢ (∀n m. ord_sub (End m) (End n) = End (m − n)) ∧
  (∀t p m k. ord_sub (End m) (Plus p k t) = End 0) ∧
  (∀t m k e. ord_sub (Plus e k t) (End m) = Plus e k t) ∧
  ∀t2 t1 k2 k1 e2 e1.
    ord_sub (Plus e1 k1 t1) (Plus e2 k2 t2) =
    if oless e1 e2 then End 0
    else if e1 = e2 then
      if k1 < k2 then End 0
      else if k1 > k2 then Plus e1 (k1 − k2) t1
      else ord_sub t1 t2
    else Plus e1 k1 t1

ord_sub_ind

⊢ ∀P. (∀m n. P (End m) (End n)) ∧ (∀m p k t. P (End m) (Plus p k t)) ∧
      (∀e k t m. P (Plus e k t) (End m)) ∧
      (∀e1 k1 t1 e2 k2 t2.
         (¬oless e1 e2 ∧ (e1 = e2) ∧ ¬(k1 < k2) ∧ ¬(k1 > k2) ⇒ P t1 t2) ⇒
         P (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
      ∀v v1. P v v1

osyntax_11

⊢ (∀a a'. (End a = End a') ⇔ (a = a')) ∧
  ∀a0 a1 a2 a0' a1' a2'.
    (Plus a0 a1 a2 = Plus a0' a1' a2') ⇔ (a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')

osyntax_Axiom

⊢ ∀f0 f1. ∃fn.
    (∀a. fn (End a) = f0 a) ∧
    ∀a0 a1 a2. fn (Plus a0 a1 a2) = f1 a1 a0 a2 (fn a0) (fn a2)

osyntax_case_cong

⊢ ∀M M' f f1.
    (M = M') ∧ (∀a. (M' = End a) ⇒ (f a = f' a)) ∧
    (∀a0 a1 a2. (M' = Plus a0 a1 a2) ⇒ (f1 a0 a1 a2 = f1' a0 a1 a2)) ⇒
    (osyntax_CASE M f f1 = osyntax_CASE M' f' f1')

osyntax_case_eq

⊢ (osyntax_CASE x f f1 = v) ⇔
  (∃n. (x = End n) ∧ (f n = v)) ∨
  ∃o' n o0. (x = Plus o' n o0) ∧ (f1 o' n o0 = v)

osyntax_distinct

⊢ ∀a2 a1 a0 a. End a ≠ Plus a0 a1 a2

osyntax_induction

⊢ ∀P. (∀n. P (End n)) ∧ (∀ $o o0. P $o ∧ P o0 ⇒ ∀n. P (Plus $o n o0)) ⇒
      ∀ $o. P $o

osyntax_nchotomy

⊢ ∀oo. (∃n. oo = End n) ∨ ∃ $o n o0. oo = Plus $o n o0

padd_compute

⊢ (∀a b. padd a b 0 = ord_add a b) ∧
  (∀a b n.
     padd a b (NUMERAL (BIT1 n)) =
     Plus (expt a) (coeff a) (padd (tail a) b (NUMERAL (BIT1 n) − 1))) ∧
  ∀a b n.
    padd a b (NUMERAL (BIT2 n)) =
    Plus (expt a) (coeff a) (padd (tail a) b (NUMERAL (BIT1 n)))

pmult_def

⊢ ∀n b a.
    pmult a b n =
    if (a = End 0) ∨ (b = End 0) then End 0
    else
      case (a,b) of
        (End i,End j) => End (i * j)
      | (Plus e1 c1 k1,End j) => Plus e1 (c1 * j) k1
      | (v,Plus e2 c2 k2) =>
        (let
           m = cf2 (expt a) e2 n
         in
           Plus (padd (expt a) e2 m) c2 (pmult a k2 m))

pmult_ind

⊢ ∀P. (∀a b n.
         (∀v v1 e2 c2 k2 m.
            ¬((a = End 0) ∨ (b = End 0)) ∧ ((a,b) = (v,v1)) ∧
            (v1 = Plus e2 c2 k2) ∧ (m = cf2 (expt a) e2 n) ⇒
            P a k2 m) ⇒
         P a b n) ⇒
      ∀v v1 v2. P v v1 v2

rank_0_End

⊢ ∀x. (rank x = 0) ⇔ ∃n. x = End n

rank_expt

⊢ ∀x n. is_ord x ∧ (rank x = SUC n) ⇒ (rank (expt x) = n)

rank_finp

⊢ ∀x. (rank x = 0) ⇔ finp x

rank_less_imp_oless

⊢ ∀x y. is_ord x ∧ is_ord y ∧ rank x < rank y ⇒ oless x y

rank_positive

⊢ ∀x. 0 < rank x ⇔ (x = Plus (expt x) (coeff x) (tail x))

rank_positive_exists

⊢ ∀x. 0 < rank x ⇔ ∃e c t. x = Plus e c t

rank_positive_expt

⊢ ∀x n. (rank x = SUC n) ⇒ (rank (expt x) = n)

restn_compute

⊢ (∀a. restn a 0 = a) ∧
  (∀a n. restn a (NUMERAL (BIT1 n)) = restn (tail a) (NUMERAL (BIT1 n) − 1)) ∧
  ∀a n. restn a (NUMERAL (BIT2 n)) = restn (tail a) (NUMERAL (BIT1 n))