Theory "ordinalNotation"

Signature

Definitions

tail_def

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

restn_def

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

rank_def

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

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)

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_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))

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

ord_less_def

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

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)

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)

finp_def

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

expt_def

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

coeff_def

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

cf2_def

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

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

Theorems

WF_ord_less

⊢ WF ord_less

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))

rank_positive_expt

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

rank_positive_exists

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

rank_positive

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

rank_less_imp_oless

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

rank_finp

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

rank_expt

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

rank_0_End

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

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

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))

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)))

osyntax_nchotomy

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

osyntax_induction

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

osyntax_distinct

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

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_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_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_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')

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

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_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_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_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_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))

oless_tail

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

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_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_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_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_imp_rank_leq

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

oless_expt

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

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_End_End

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

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_antisym

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

oless_antirefl

⊢ ∀x. is_ord x ⇒ ¬oless x x

main_lemma

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

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

is_ord_tail_closed

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

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_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_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_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_expt_closed

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

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_downclosed

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

is_ord_coeff_pos

⊢ ∀x. ¬finp x ∧ is_ord x ⇒ 0 < coeff 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

e0_RECURSION

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

e0_INDUCTION

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

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

datatype_osyntax

⊢ DATATYPE (osyntax End Plus)