Theory "ordinalNotation"

Signature

Definitions

osyntax_TY_DEF

⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀'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 ∧ 'osyntax' a0 ∧ 'osyntax' a2) ⇒
                      'osyntax' a0') ⇒
                 '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))

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

finp_def

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

tail_def

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

rank_def

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

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)

ord_less_def

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

restn_def

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

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

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)

Theorems

datatype_osyntax

⊢ DATATYPE (osyntax End Plus)

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_distinct

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

osyntax_nchotomy

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

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_induction

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

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

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

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

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)

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

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

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_tail_closed

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

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

rank_expt

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

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

rank_less_imp_oless

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

oless_imp_rank_leq

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

rank_0_End

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

rank_finp

⊢ ∀x. rank x = 0 ⇔ finp x

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_positive_expt

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

oless_expt

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

oless_tail

⊢ ∀x. is_ord x ∧ ¬finp x ⇒ oless (tail x) 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

WF_ord_less

⊢ WF ord_less

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

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

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)

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

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