Theory "toto"

Signature

Definitions

cpn_TY_DEF

|- ∃rep. TYPE_DEFINITION (λn. n < 3) rep

cpn_BIJ

|- (∀a. num2cpn (cpn2num a) = a) ∧
   ∀r. (λn. n < 3) r ⇔ (cpn2num (num2cpn r) = r)

cpn_size_def

|- ∀x. cpn_size x = 0

cpn_CASE

|- ∀x v0 v1 v2.
     (case x of LESS => v0 | EQUAL => v1 | GREATER => v2) =
     (λm. if m < 1 then v0 else if m = 1 then v1 else v2) (cpn2num x)

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 GREATER => F | _ => T

StrongLinearOrder_of_TO

|- ∀c x y. StrongLinearOrder_of_TO c x y ⇔ case c x y of LESS => T | _ => 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 n.
        I
          (if n = 0 then zer
           else if ODD n then bit1 (num_to_dt (DIV2 (n − 1)))
           else bit2 (num_to_dt (DIV2 (n − 2)))))

num_dtOrd_tupled_primitive

|- num_dtOrd_tupled =
   WFREC
     (@R.
        WF R ∧ (∀y x. R (x,y) (bit1 x,bit1 y)) ∧
        ∀y x. R (x,y) (bit2 x,bit2 y))
     (λnum_dtOrd_tupled a.
        case a of
          (zer,zer) => I EQUAL
        | (zer,bit1 x) => I LESS
        | (zer,bit2 x') => I LESS
        | (bit1 x'',zer) => I GREATER
        | (bit1 x'',bit1 y'') => I (num_dtOrd_tupled (x'',y''))
        | (bit1 x'',bit2 y) => I LESS
        | (bit2 x''',zer) => I GREATER
        | (bit2 x''',bit1 y') => I GREATER
        | (bit2 x''',bit2 y''') => I (num_dtOrd_tupled (x''',y''')))

num_dtOrd_curried

|- ∀x x1. num_dtOrd x x1 = num_dtOrd_tupled (x,x1)

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

listorder_tupled_primitive

|- listorder_tupled =
   WFREC (@R. WF R ∧ ∀s r m l V. R (V,l,m) (V,r::l,s::m))
     (λlistorder_tupled a.
        case a of
          (V,l,[]) => I F
        | (V,[],s::m) => I T
        | (V,r::l',s::m) => I (V r s ∨ (r = s) ∧ listorder_tupled (V,l',m)))

listorder_curried

|- ∀x x1 x2. listorder x x1 x2 ⇔ listorder_tupled (x,x1,x2)

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

num2cpn_cpn2num

|- ∀a. num2cpn (cpn2num a) = a

cpn2num_num2cpn

|- ∀r. r < 3 ⇔ (cpn2num (num2cpn r) = r)

num2cpn_11

|- ∀r r'. r < 3 ⇒ r' < 3 ⇒ ((num2cpn r = num2cpn r') ⇔ (r = r'))

cpn2num_11

|- ∀a a'. (cpn2num a = cpn2num a') ⇔ (a = a')

num2cpn_ONTO

|- ∀a. ∃r. (a = num2cpn r) ∧ r < 3

cpn2num_ONTO

|- ∀r. r < 3 ⇔ ∃a. r = cpn2num a

num2cpn_thm

|- (num2cpn 0 = LESS) ∧ (num2cpn 1 = EQUAL) ∧ (num2cpn 2 = GREATER)

cpn2num_thm

|- (cpn2num LESS = 0) ∧ (cpn2num EQUAL = 1) ∧ (cpn2num GREATER = 2)

cpn_EQ_cpn

|- ∀a a'. (a = a') ⇔ (cpn2num a = cpn2num a')

cpn_case_def

|- (∀v0 v1 v2. (case LESS of LESS => v0 | EQUAL => v1 | GREATER => v2) = v0) ∧
   (∀v0 v1 v2.
      (case EQUAL of LESS => v0 | EQUAL => v1 | GREATER => v2) = v1) ∧
   ∀v0 v1 v2. (case GREATER of LESS => v0 | EQUAL => v1 | GREATER => v2) = v2

datatype_cpn

|- DATATYPE (cpn LESS EQUAL GREATER)

cpn_distinct

|- LESS ≠ EQUAL ∧ LESS ≠ GREATER ∧ EQUAL ≠ GREATER

cpn_case_cong

|- ∀M M' v0 v1 v2.
     (M = M') ∧ ((M' = LESS) ⇒ (v0 = v0')) ∧ ((M' = EQUAL) ⇒ (v1 = v1')) ∧
     ((M' = GREATER) ⇒ (v2 = v2')) ⇒
     ((case M of LESS => v0 | EQUAL => v1 | GREATER => v2) =
      case M' of LESS => v0' | EQUAL => v1' | GREATER => v2')

cpn_nchotomy

|- ∀a. (a = LESS) ∨ (a = EQUAL) ∨ (a = GREATER)

cpn_Axiom

|- ∀x0 x1 x2. ∃f. (f LESS = x0) ∧ (f EQUAL = x1) ∧ (f GREATER = x2)

cpn_induction

|- ∀P. P EQUAL ∧ P GREATER ∧ P LESS ⇒ ∀a. P a

all_cpn_distinct

|- (LESS ≠ EQUAL ∧ LESS ≠ GREATER ∧ EQUAL ≠ GREATER) ∧ EQUAL ≠ LESS ∧
   GREATER ≠ LESS ∧ GREATER ≠ EQUAL

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

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

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)

TotOrd_TO_of_Strong

|- ∀r. StrongLinearOrder r ⇒ TotOrd (TO_of_LinearOrder r)

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

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

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 GREATER => GREATER | _ => LESS) ∧
     (numOrd (BIT2 x) (BIT1 y) =
      case numOrd x y of LESS => LESS | _ => 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_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_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_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

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)

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

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