Theory "toto"

Signature

Definitions

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

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

toto_TY_DEF

⊢ ∃rep. TYPE_DEFINITION TotOrd rep

to_bij

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

WeakLinearOrder_of_TO

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

StrongLinearOrder_of_TO

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

toto_of_LinearOrder

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

TO_inv

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

toto_inv

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

lexTO

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

lextoto

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

numOrd

⊢ numOrd = TO_of_LinearOrder $<

numto

⊢ numto = TO numOrd

num_dt_TY_DEF

⊢ ∃rep.
      TYPE_DEFINITION
        (λa0.
             ∀'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 ∧
                           'num_dt' a) ∨
                      (∃a.
                           a0 =
                           (λa.
                                ind_type$CONSTR (SUC (SUC 0)) ARB
                                  (ind_type$FCONS a (λn. ind_type$BOTTOM))) a ∧
                           'num_dt' a) ⇒
                      'num_dt' a0) ⇒
                 'num_dt' a0) rep

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

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

qk_numOrd_def

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

qk_numto

⊢ qk_numto = TO qk_numOrd

charOrd

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

charto

⊢ charto = TO charOrd

ListOrd

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

listoto

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

stringto

⊢ stringto = listoto charto

imageOrd

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

Theorems

StrongLinearOrderExists

⊢ ∃R. StrongLinearOrder R

trichotomous_ALT

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

TotOrd_TO_of_LO

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

SPLIT_PAIRS

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

all_cpn_distinct

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

TO_exists

⊢ ∃x. TotOrd x

TO_apto_ID

⊢ ∀a. TO (apto a) = a

TO_apto_TO_ID

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

TO_11

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

onto_apto

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

TO_onto

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

TotOrd_apto

⊢ ∀c. TotOrd (apto c)

TO_apto_TO_IMP

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

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

TO_equal_eq

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

toto_equal_eq

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

toto_equal_imp_eq

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

TO_refl

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

toto_refl

⊢ ∀c x. apto c x x = Equal

toto_equal_sym

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

TO_antisym

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

toto_antisym

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

toto_not_less_refl

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

toto_swap_cases

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

toto_glneq

⊢ (∀c x y. apto c x y = Less ⇒ x ≠ y) ∧ ∀c x y. apto c x y = Greater ⇒ 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

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

NOT_EQ_LESS_IMP

⊢ ∀cmp x y. apto cmp x y ≠ Less ⇒ x = y ∨ apto cmp y x = 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)

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

totoGGtrans

⊢ ∀c x y z. apto c y x = Greater ∧ apto c z y = Greater ⇒ 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

totoLEtrans

⊢ ∀c x y z. apto c x y = Less ∧ apto c y z = Equal ⇒ 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

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

Weak_Weak_of

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

STRORD_SLO

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

Strongof_toto_STRORD

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

Strong_Strong_of

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

Strong_Strong_of_TO

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

TotOrd_TO_of_Weak

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

TotOrd_TO_of_Strong

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

toto_Weak_thm

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

toto_Strong_thm

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

Weak_toto_thm

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

Strong_toto_thm

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

TotOrd_inv

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

inv_TO

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

apto_inv

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

Weak_toto_inv

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

Strong_toto_inv

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

TO_inv_TO_inv

⊢ ∀c. TO_inv (TO_inv c) = c

toto_inv_toto_inv

⊢ ∀c. toto_inv (toto_inv c) = c

TO_inv_Ord

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

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

toto_equal_imp

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

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

StrongOrder_ALT

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

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)

SLO_LEX

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

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

TO_lexTO

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

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

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

StrongLinearOrder_LESS

⊢ StrongLinearOrder $<

TO_numOrd

⊢ TotOrd numOrd

apnumto_thm

⊢ apto numto = numOrd

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

datatype_num_dt

⊢ DATATYPE (num_dt zer bit1 bit2)

num_dt_11

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

num_dt_distinct

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

num_dt_nchotomy

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

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_induction

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

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

TO_qk_numOrd

⊢ TotOrd qk_numOrd

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

ap_qk_numto_thm

⊢ apto qk_numto = qk_numOrd

TO_charOrd

⊢ TotOrd charOrd

apcharto_thm

⊢ apto charto = charOrd

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

charOrd_thm

⊢ charOrd = TO_of_LinearOrder $<

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

SLO_listorder

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

TO_ListOrd

⊢ ∀c. TotOrd (ListOrd c)

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

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

TO_injection

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

StrongLinearOrder_of_TO_TO_of_LinearOrder

⊢ ∀R. irreflexive R ⇒ StrongLinearOrder_of_TO (TO_of_LinearOrder R) = 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