Theory "toto"

Signature

Definitions

WeakLinearOrder_of_TO

⊢ ∀c x y.
      WeakLinearOrder_of_TO c x y ⇔
      case c x y of Less => T | Equal => T | Greater => F

TotOrd

⊢ ∀c.
      TotOrd c ⇔
      (∀x y. (c x y = Equal) ⇔ (x = y)) ∧
      (∀x y. (c x y = Greater) ⇔ (c y x = Less)) ∧
      ∀x y z. (c x y = Less) ∧ (c y z = Less) ⇒ (c x z = Less)

toto_TY_DEF

⊢ ∃rep. TYPE_DEFINITION TotOrd rep

toto_of_LinearOrder

⊢ ∀r. toto_of_LinearOrder r = TO (TO_of_LinearOrder r)

toto_inv

⊢ ∀c. toto_inv c = TO (TO_inv (apto c))

TO_of_LinearOrder

⊢ ∀r x y.
      TO_of_LinearOrder r x y =
      if x = y then Equal else if r x y then Less else Greater

TO_inv

⊢ ∀c x y. TO_inv c x y = c y x

to_bij

⊢ (∀a. TO (apto a) = a) ∧ ∀r. TotOrd r ⇔ (apto (TO r) = r)

StrongLinearOrder_of_TO

⊢ ∀c x y.
      StrongLinearOrder_of_TO c x y ⇔
      case c x y of Less => T | Equal => F | Greater => F

stringto

⊢ stringto = listoto charto

qk_numto

⊢ qk_numto = TO qk_numOrd

qk_numOrd_def

⊢ ∀m n. qk_numOrd m n = num_dtOrd (num_to_dt m) (num_to_dt n)

numto

⊢ numto = TO numOrd

numOrd

⊢ numOrd = TO_of_LinearOrder $<

num_to_dt_primitive

⊢ num_to_dt =
  WFREC
    (@R.
         WF R ∧ (∀n. n ≠ 0 ∧ ODD n ⇒ R (DIV2 (n − 1)) n) ∧
         ∀n. n ≠ 0 ∧ ¬ODD n ⇒ R (DIV2 (n − 2)) n)
    (λnum_to_dt a.
         I
           (if a = 0 then zer
            else if ODD a then bit1 (num_to_dt (DIV2 (a − 1)))
            else bit2 (num_to_dt (DIV2 (a − 2)))))

num_dt_TY_DEF

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

num_dt_size_def

⊢ (num_dt_size zer = 0) ∧ (∀a. num_dt_size (bit1 a) = 1 + num_dt_size a) ∧
  ∀a. num_dt_size (bit2 a) = 1 + num_dt_size a

num_dt_case_def

⊢ (∀v f f1. num_dt_CASE zer v f f1 = v) ∧
  (∀a v f f1. num_dt_CASE (bit1 a) v f f1 = f a) ∧
  ∀a v f f1. num_dt_CASE (bit2 a) v f f1 = f1 a

listoto

⊢ ∀c. listoto c = TO (ListOrd c)

ListOrd

⊢ ∀c.
      ListOrd c =
      TO_of_LinearOrder (listorder (StrongLinearOrder_of_TO (apto c)))

lextoto

⊢ ∀c v. c lextoto v = TO (apto c lexTO apto v)

lexTO

⊢ ∀R V.
      R lexTO V =
      TO_of_LinearOrder
        (StrongLinearOrder_of_TO R LEX StrongLinearOrder_of_TO V)

imageOrd

⊢ ∀f cp a b. imageOrd f cp a b = cp (f a) (f b)

charto

⊢ charto = TO charOrd

charOrd

⊢ ∀a b. charOrd a b = numOrd (ORD a) (ORD b)

Theorems

Weak_Weak_of

⊢ ∀c. WeakLinearOrder (WeakLinearOrder_of_TO (apto c))

Weak_toto_thm

⊢ ∀r.
      WeakLinearOrder r ⇒
      (WeakLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)

Weak_toto_inv

⊢ ∀c.
      WeakLinearOrder_of_TO (apto (toto_inv c)) =
      (WeakLinearOrder_of_TO (apto c))ᵀ

trichotomous_ALT

⊢ ∀R. trichotomous R ⇔ ∀x y. ¬R x y ∧ ¬R y x ⇒ (x = y)

TotOrd_TO_of_Weak

⊢ ∀r. WeakLinearOrder r ⇒ TotOrd (TO_of_LinearOrder r)

TotOrd_TO_of_Strong

⊢ ∀r. StrongLinearOrder r ⇒ TotOrd (TO_of_LinearOrder r)

TotOrd_TO_of_LO

⊢ ∀r. LinearOrder r ⇒ TotOrd (TO_of_LinearOrder r)

TotOrd_inv

⊢ ∀c. TotOrd c ⇒ TotOrd (TO_inv c)

TotOrd_apto

⊢ ∀c. TotOrd (apto c)

totoLLtrans

⊢ ∀c x y z. (apto c x y = Less) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

totoLGtrans

⊢ ∀c x y z. (apto c x y = Less) ∧ (apto c z y = Greater) ⇒ (apto c x z = Less)

totoLEtrans

⊢ ∀c x y z. (apto c x y = Less) ∧ (apto c y z = Equal) ⇒ (apto c x z = Less)

totoGLtrans

⊢ ∀c x y z. (apto c y x = Greater) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

totoGGtrans

⊢ ∀c x y z.
      (apto c y x = Greater) ∧ (apto c z y = Greater) ⇒ (apto c x z = Less)

totoELtrans

⊢ ∀c x y z. (apto c x y = Equal) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

totoEEtrans

⊢ ∀c x y z.
      ((apto c x y = Equal) ∧ (apto c y z = Equal) ⇒ (apto c x z = Equal)) ∧
      ((apto c x y = Equal) ∧ (apto c z y = Equal) ⇒ (apto c x z = Equal))

toto_Weak_thm

⊢ ∀c. toto_of_LinearOrder (WeakLinearOrder_of_TO (apto c)) = c

toto_unequal_imp

⊢ ∀cmp phi.
      LinearOrder phi ∧ (cmp = toto_of_LinearOrder phi) ⇒
      ∀x y.
          ((x = y) ⇔ F) ⇒
          if phi x y then apto cmp x y = Less else apto cmp x y = Greater

toto_trans_less

⊢ (∀c x y z. (apto c x y = Less) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)) ∧
  (∀c x y z.
       (apto c x y = Less) ∧ (apto c z y = Greater) ⇒ (apto c x z = Less)) ∧
  (∀c x y z.
       (apto c y x = Greater) ∧ (apto c z y = Greater) ⇒ (apto c x z = Less)) ∧
  (∀c x y z.
       (apto c y x = Greater) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)) ∧
  (∀c x y z. (apto c x y = Less) ∧ (apto c y z = Equal) ⇒ (apto c x z = Less)) ∧
  ∀c x y z. (apto c x y = Equal) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

toto_thm

⊢ ∀c.
      (∀x y. (apto c x y = Equal) ⇔ (x = y)) ∧
      (∀x y. (apto c x y = Greater) ⇔ (apto c y x = Less)) ∧
      ∀x y z. (apto c x y = Less) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

toto_swap_cases

⊢ ∀c x y.
      apto c y x =
      case apto c x y of Less => Greater | Equal => Equal | Greater => Less

toto_Strong_thm

⊢ ∀c. toto_of_LinearOrder (StrongLinearOrder_of_TO (apto c)) = c

toto_refl

⊢ ∀c x. apto c x x = Equal

toto_not_less_refl

⊢ ∀cmp h. (apto cmp h h = Less) ⇔ F

toto_inv_toto_inv

⊢ ∀c. toto_inv (toto_inv c) = c

toto_glneq

⊢ (∀c x y. (apto c x y = Less) ⇒ x ≠ y) ∧
  ∀c x y. (apto c x y = Greater) ⇒ x ≠ y

toto_equal_sym

⊢ ∀c x y. (apto c x y = Equal) ⇔ (apto c y x = Equal)

toto_equal_imp_eq

⊢ ∀c x y. (apto c x y = Equal) ⇒ (x = y)

toto_equal_imp

⊢ ∀cmp phi.
      LinearOrder phi ∧ (cmp = toto_of_LinearOrder phi) ⇒
      ∀x y. ((x = y) ⇔ T) ⇒ (apto cmp x y = Equal)

toto_equal_eq

⊢ ∀c x y. (apto c x y = Equal) ⇔ (x = y)

toto_cpn_eqn

⊢ (∀c x y. (apto c x y = Equal) ⇒ (x = y)) ∧
  (∀c x y. (apto c x y = Less) ⇒ x ≠ y) ∧
  ∀c x y. (apto c x y = Greater) ⇒ x ≠ y

toto_antisym

⊢ ∀c x y. (apto c x y = Greater) ⇔ (apto c y x = Less)

TO_refl

⊢ ∀c. TotOrd c ⇒ ∀x. c x x = Equal

TO_qk_numOrd

⊢ TotOrd qk_numOrd

TO_onto

⊢ ∀a. ∃r. (a = TO r) ∧ TotOrd r

TO_of_LinearOrder_LEX

⊢ ∀R V.
      irreflexive R ∧ irreflexive V ⇒
      (TO_of_LinearOrder (R LEX V) =
       TO_of_LinearOrder R lexTO TO_of_LinearOrder V)

TO_of_less_rel

⊢ ∀r. StrongLinearOrder r ⇒ ∀x y. (TO_of_LinearOrder r x y = Less) ⇔ r x y

TO_of_greater_ler

⊢ ∀r. StrongLinearOrder r ⇒ ∀x y. (TO_of_LinearOrder r x y = Greater) ⇔ r y x

TO_numOrd

⊢ TotOrd numOrd

TO_ListOrd

⊢ ∀c. TotOrd (ListOrd c)

TO_lexTO

⊢ ∀R V. TotOrd R ∧ TotOrd V ⇒ TotOrd (R lexTO V)

TO_inv_TO_inv

⊢ ∀c. TO_inv (TO_inv c) = c

TO_inv_Ord

⊢ ∀r. TO_of_LinearOrder rᵀ = TO_inv (TO_of_LinearOrder r)

TO_injection

⊢ ∀cp. TotOrd cp ⇒ ∀f. ONE_ONE f ⇒ TotOrd (imageOrd f cp)

TO_exists

⊢ ∃x. TotOrd x

TO_equal_eq

⊢ ∀c. TotOrd c ⇒ ∀x y. (c x y = Equal) ⇔ (x = y)

TO_cpn_eqn

⊢ ∀c.
      TotOrd c ⇒
      (∀x y. (c x y = Less) ⇒ x ≠ y) ∧ (∀x y. (c x y = Greater) ⇒ x ≠ y) ∧
      ∀x y. (c x y = Equal) ⇒ (x = y)

TO_charOrd

⊢ TotOrd charOrd

TO_apto_TO_IMP

⊢ ∀r. TotOrd r ⇒ (apto (TO r) = r)

TO_apto_TO_ID

⊢ ∀r. TotOrd r ⇔ (apto (TO r) = r)

TO_apto_ID

⊢ ∀a. TO (apto a) = a

TO_antisym

⊢ ∀c. TotOrd c ⇒ ∀x y. (c x y = Greater) ⇔ (c y x = Less)

TO_11

⊢ ∀r r'. TotOrd r ⇒ TotOrd r' ⇒ ((TO r = TO r') ⇔ (r = r'))

STRORD_SLO

⊢ ∀R. WeakLinearOrder R ⇒ StrongLinearOrder (STRORD R)

StrongOrder_ALT

⊢ ∀Z. StrongOrder Z ⇔ irreflexive Z ∧ transitive Z

Strongof_toto_STRORD

⊢ ∀c.
      StrongLinearOrder_of_TO (apto c) =
      STRORD (WeakLinearOrder_of_TO (apto c))

StrongLinearOrderExists

⊢ ∃R. StrongLinearOrder R

StrongLinearOrder_of_TO_TO_of_LinearOrder

⊢ ∀R. irreflexive R ⇒ (StrongLinearOrder_of_TO (TO_of_LinearOrder R) = R)

StrongLinearOrder_LESS

⊢ StrongLinearOrder $<

Strong_toto_thm

⊢ ∀r.
      StrongLinearOrder r ⇒
      (StrongLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)

Strong_toto_inv

⊢ ∀c.
      StrongLinearOrder_of_TO (apto (toto_inv c)) =
      (StrongLinearOrder_of_TO (apto c))ᵀ

Strong_Strong_of_TO

⊢ ∀c. TotOrd c ⇒ StrongLinearOrder (StrongLinearOrder_of_TO c)

Strong_Strong_of

⊢ ∀c. StrongLinearOrder (StrongLinearOrder_of_TO (apto c))

SPLIT_PAIRS

⊢ ∀x y. (x = y) ⇔ (FST x = FST y) ∧ (SND x = SND y)

SLO_listorder

⊢ ∀V. StrongLinearOrder V ⇒ StrongLinearOrder (listorder V)

SLO_LEX

⊢ ∀R V.
      StrongLinearOrder R ∧ StrongLinearOrder V ⇒ StrongLinearOrder (R LEX V)

qk_numeralOrd

⊢ ∀x y.
      (qk_numOrd ZERO ZERO = Equal) ∧ (qk_numOrd ZERO (BIT1 y) = Less) ∧
      (qk_numOrd ZERO (BIT2 y) = Less) ∧ (qk_numOrd (BIT1 x) ZERO = Greater) ∧
      (qk_numOrd (BIT2 x) ZERO = Greater) ∧
      (qk_numOrd (BIT1 x) (BIT1 y) = qk_numOrd x y) ∧
      (qk_numOrd (BIT2 x) (BIT2 y) = qk_numOrd x y) ∧
      (qk_numOrd (BIT1 x) (BIT2 y) = Less) ∧
      (qk_numOrd (BIT2 x) (BIT1 y) = Greater)

pre_aplextoto

⊢ ∀c v x y.
      apto (c lextoto v) x y =
      case apto c (FST x) (FST y) of
        Less => Less
      | Equal => apto v (SND x) (SND y)
      | Greater => Greater

onto_apto

⊢ ∀r. TotOrd r ⇔ ∃a. r = apto a

numeralOrd

⊢ ∀x y.
      (numOrd ZERO ZERO = Equal) ∧ (numOrd ZERO (BIT1 y) = Less) ∧
      (numOrd ZERO (BIT2 y) = Less) ∧ (numOrd (BIT1 x) ZERO = Greater) ∧
      (numOrd (BIT2 x) ZERO = Greater) ∧
      (numOrd (BIT1 x) (BIT1 y) = numOrd x y) ∧
      (numOrd (BIT2 x) (BIT2 y) = numOrd x y) ∧
      (numOrd (BIT1 x) (BIT2 y) =
       case numOrd x y of Less => Less | Equal => Less | Greater => Greater) ∧
      (numOrd (BIT2 x) (BIT1 y) =
       case numOrd x y of Less => Less | Equal => Greater | Greater => Greater)

num_dtOrd_ind

⊢ ∀P.
      P zer zer ∧ (∀x. P zer (bit1 x)) ∧ (∀x. P zer (bit2 x)) ∧
      (∀x. P (bit1 x) zer) ∧ (∀x. P (bit2 x) zer) ∧
      (∀x y. P (bit1 x) (bit2 y)) ∧ (∀x y. P (bit2 x) (bit1 y)) ∧
      (∀x y. P x y ⇒ P (bit1 x) (bit1 y)) ∧
      (∀x y. P x y ⇒ P (bit2 x) (bit2 y)) ⇒
      ∀v v1. P v v1

num_dtOrd

⊢ (num_dtOrd zer zer = Equal) ∧ (∀x. num_dtOrd zer (bit1 x) = Less) ∧
  (∀x. num_dtOrd zer (bit2 x) = Less) ∧
  (∀x. num_dtOrd (bit1 x) zer = Greater) ∧
  (∀x. num_dtOrd (bit2 x) zer = Greater) ∧
  (∀y x. num_dtOrd (bit1 x) (bit2 y) = Less) ∧
  (∀y x. num_dtOrd (bit2 x) (bit1 y) = Greater) ∧
  (∀y x. num_dtOrd (bit1 x) (bit1 y) = num_dtOrd x y) ∧
  ∀y x. num_dtOrd (bit2 x) (bit2 y) = num_dtOrd x y

num_dt_nchotomy

⊢ ∀nn. (nn = zer) ∨ (∃n. nn = bit1 n) ∨ ∃n. nn = bit2 n

num_dt_induction

⊢ ∀P. P zer ∧ (∀n. P n ⇒ P (bit1 n)) ∧ (∀n. P n ⇒ P (bit2 n)) ⇒ ∀n. P n

num_dt_distinct

⊢ (∀a. zer ≠ bit1 a) ∧ (∀a. zer ≠ bit2 a) ∧ ∀a' a. bit1 a ≠ bit2 a'

num_dt_case_eq

⊢ (num_dt_CASE x v f f1 = v') ⇔
  (x = zer) ∧ (v = v') ∨ (∃n. (x = bit1 n) ∧ (f n = v')) ∨
  ∃n. (x = bit2 n) ∧ (f1 n = v')

num_dt_case_cong

⊢ ∀M M' v f f1.
      (M = M') ∧ ((M' = zer) ⇒ (v = v')) ∧
      (∀a. (M' = bit1 a) ⇒ (f a = f' a)) ∧
      (∀a. (M' = bit2 a) ⇒ (f1 a = f1' a)) ⇒
      (num_dt_CASE M v f f1 = num_dt_CASE M' v' f' f1')

num_dt_Axiom

⊢ ∀f0 f1 f2.
      ∃fn.
          (fn zer = f0) ∧ (∀a. fn (bit1 a) = f1 a (fn a)) ∧
          ∀a. fn (bit2 a) = f2 a (fn a)

num_dt_11

⊢ (∀a a'. (bit1 a = bit1 a') ⇔ (a = a')) ∧
  ∀a a'. (bit2 a = bit2 a') ⇔ (a = a')

NOT_EQ_LESS_IMP

⊢ ∀cmp x y. apto cmp x y ≠ Less ⇒ (x = y) ∨ (apto cmp y x = Less)

listorder_ind

⊢ ∀P.
      (∀V l. P V l []) ∧ (∀V s m. P V [] (s::m)) ∧
      (∀V r l s m. P V l m ⇒ P V (r::l) (s::m)) ⇒
      ∀v v1 v2. P v v1 v2

listorder

⊢ (∀l V. listorder V l [] ⇔ F) ∧ (∀s m V. listorder V [] (s::m) ⇔ T) ∧
  ∀s r m l V. listorder V (r::l) (s::m) ⇔ V r s ∨ (r = s) ∧ listorder V l m

ListOrd_THM

⊢ ∀c.
      (ListOrd c [] [] = Equal) ∧ (∀b y. ListOrd c [] (b::y) = Less) ∧
      (∀a x. ListOrd c (a::x) [] = Greater) ∧
      ∀a x b y.
          ListOrd c (a::x) (b::y) =
          case apto c a b of
            Less => Less
          | Equal => ListOrd c x y
          | Greater => Greater

lexTO_thm

⊢ ∀R V.
      TotOrd R ∧ TotOrd V ⇒
      ∀x y.
          (R lexTO V) x y =
          case R (FST x) (FST y) of
            Less => Less
          | Equal => V (SND x) (SND y)
          | Greater => Greater

lexTO_ALT

⊢ ∀R V.
      TotOrd R ∧ TotOrd V ⇒
      ∀(r,u) (r',u').
          (R lexTO V) (r,u) (r',u') =
          case R r r' of Less => Less | Equal => V u u' | Greater => Greater

LEX_ALT

⊢ ∀R U c d.
      (R LEX U) c d ⇔ R (FST c) (FST d) ∨ (FST c = FST d) ∧ U (SND c) (SND d)

inv_TO

⊢ ∀r. TotOrd r ⇒ (toto_inv (TO r) = TO (TO_inv r))

datatype_num_dt

⊢ DATATYPE (num_dt zer bit1 bit2)

charOrd_thm

⊢ charOrd = TO_of_LinearOrder $<

charOrd_lt_lem

⊢ ∀a b. (numOrd a b = Less) ⇒ (b < 256 ⇔ T) ⇒ (charOrd (CHR a) (CHR b) = Less)

charOrd_gt_lem

⊢ ∀a b.
      (numOrd a b = Greater) ⇒
      (a < 256 ⇔ T) ⇒
      (charOrd (CHR a) (CHR b) = Greater)

charOrd_eq_lem

⊢ ∀a b. (numOrd a b = Equal) ⇒ (charOrd (CHR a) (CHR b) = Equal)

apto_inv

⊢ ∀c. apto (toto_inv c) = TO_inv (apto c)

apnumto_thm

⊢ apto numto = numOrd

aplistoto

⊢ ∀c.
      (apto (listoto c) [] [] = Equal) ∧
      (∀b y. apto (listoto c) [] (b::y) = Less) ∧
      (∀a x. apto (listoto c) (a::x) [] = Greater) ∧
      ∀a x b y.
          apto (listoto c) (a::x) (b::y) =
          case apto c a b of
            Less => Less
          | Equal => apto (listoto c) x y
          | Greater => Greater

aplextoto

⊢ ∀c v x1 x2 y1 y2.
      apto (c lextoto v) (x1,x2) (y1,y2) =
      case apto c x1 y1 of
        Less => Less
      | Equal => apto v x2 y2
      | Greater => Greater

apcharto_thm

⊢ apto charto = charOrd

ap_qk_numto_thm

⊢ apto qk_numto = qk_numOrd

all_cpn_distinct

⊢ (Less ≠ Equal ∧ Less ≠ Greater ∧ Equal ≠ Greater) ∧ Equal ≠ Less ∧
  Greater ≠ Less ∧ Greater ≠ Equal