Theory: toto

Definitions

ListOrd

|- !c. ListOrd c =
       TO_of_LinearOrder (listorder (StrongLinearOrder_of_TO (apto c)))

StrongLinearOrder_of_TO

|- !c x y.
     StrongLinearOrder_of_TO c x y <=>
     case c x y of LESS => T | EQUAL => F | GREATER => F

TO_inv

|- !c x y. TO_inv c x y = c y x

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

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)

WeakLinearOrder_of_TO

|- !c x y.
     WeakLinearOrder_of_TO c x y <=>
     case c x y of LESS => T | EQUAL => T | GREATER => F

charOrd

|- !a b. charOrd a b = numOrd (ORD a) (ORD b)

charto

|- charto = TO charOrd

imageOrd

|- !f cp a b. imageOrd f cp a b = cp (f a) (f b)

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)

listoto

|- !c. listoto c = TO (ListOrd c)

numOrd

|- numOrd = TO_of_LinearOrder $<

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

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

numto

|- numto = TO numOrd

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

stringto

|- stringto = listoto charto

to_bij

|- (!a. TO (apto a) = a) /\ !r. TotOrd r <=> (apto (TO r) = r)

toto_TY_DEF

|- ?rep. TYPE_DEFINITION TotOrd rep

toto_inv

|- !c. toto_inv c = TO (TO_inv (apto c))

toto_of_LinearOrder

|- !r. toto_of_LinearOrder r = TO (TO_of_LinearOrder r)

Theorems

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)

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

NOT_EQ_LESS_IMP

|- !cmp x y. apto cmp x y <> LESS ==> (x = y) \/ (apto cmp y x = LESS)

SLO_LEX

|- !R V.
     StrongLinearOrder R /\ StrongLinearOrder V ==>
     StrongLinearOrder (R LEX V)

SLO_listorder

|- !V. StrongLinearOrder V ==> StrongLinearOrder (listorder V)

SPLIT_PAIRS

|- !x y. (x = y) <=> (FST x = FST y) /\ (SND x = SND y)

STRORD_SLO

|- !R. WeakLinearOrder R ==> StrongLinearOrder (STRORD R)

StrongLinearOrderExists

|- ?R. StrongLinearOrder R

StrongLinearOrder_LESS

|- StrongLinearOrder $<

StrongLinearOrder_of_TO_TO_of_LinearOrder

|- !R. irreflexive R ==>
       (StrongLinearOrder_of_TO (TO_of_LinearOrder R) = R)

StrongOrder_ALT

|- !Z. StrongOrder Z <=> irreflexive Z /\ transitive Z

Strong_Strong_of

|- !c. StrongLinearOrder (StrongLinearOrder_of_TO (apto c))

Strong_Strong_of_TO

|- !c. TotOrd c ==> StrongLinearOrder (StrongLinearOrder_of_TO c)

Strong_toto_inv

|- !c. StrongLinearOrder_of_TO (apto (toto_inv c)) =
       relinv (StrongLinearOrder_of_TO (apto c))

Strong_toto_thm

|- !r. StrongLinearOrder r ==>
       (StrongLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)

Strongof_toto_STRORD

|- !c. StrongLinearOrder_of_TO (apto c) =
       STRORD (WeakLinearOrder_of_TO (apto c))

TO_11

|- !r r'. TotOrd r ==> TotOrd r' ==> ((TO r = TO r') <=> (r = r'))

TO_ListOrd

|- !c. TotOrd (ListOrd c)

TO_antisym

|- !c. TotOrd c ==> !x y. (c x y = GREATER) <=> (c y x = LESS)

TO_apto_ID

|- !a. TO (apto a) = a

TO_apto_TO_ID

|- !r. TotOrd r <=> (apto (TO r) = r)

TO_apto_TO_IMP

|- !r. TotOrd r ==> (apto (TO r) = r)

TO_charOrd

|- TotOrd charOrd

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_equal_eq

|- !c. TotOrd c ==> !x y. (c x y = EQUAL) <=> (x = y)

TO_exists

|- ?x. TotOrd x

TO_injection

|- !cp. TotOrd cp ==> !f. ONE_ONE f ==> TotOrd (imageOrd f cp)

TO_inv_Ord

|- !r. TO_of_LinearOrder (relinv r) = TO_inv (TO_of_LinearOrder r)

TO_inv_TO_inv

|- !c. TO_inv (TO_inv c) = c

TO_lexTO

|- !R V. TotOrd R /\ TotOrd V ==> TotOrd (R lexTO V)

TO_numOrd

|- TotOrd numOrd

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_greater_ler

|- !r. StrongLinearOrder r ==>
       !x y. (TO_of_LinearOrder r x y = GREATER) <=> r y x

TO_of_less_rel

|- !r. StrongLinearOrder r ==>
       !x y. (TO_of_LinearOrder r x y = LESS) <=> r x y

TO_onto

|- !a. ?r. (a = TO r) /\ TotOrd r

TO_qk_numOrd

|- TotOrd qk_numOrd

TO_refl

|- !c. TotOrd c ==> !x. c x x = EQUAL

TotOrd_TO_of_LO

|- !r. LinearOrder r ==> TotOrd (TO_of_LinearOrder r)

TotOrd_TO_of_Strong

|- !r. StrongLinearOrder r ==> TotOrd (TO_of_LinearOrder r)

TotOrd_TO_of_Weak

|- !r. WeakLinearOrder r ==> TotOrd (TO_of_LinearOrder r)

TotOrd_apto

|- !c. TotOrd (apto c)

TotOrd_inv

|- !c. TotOrd c ==> TotOrd (TO_inv c)

Weak_Weak_of

|- !c. WeakLinearOrder (WeakLinearOrder_of_TO (apto c))

Weak_toto_inv

|- !c. WeakLinearOrder_of_TO (apto (toto_inv c)) =
       relinv (WeakLinearOrder_of_TO (apto c))

Weak_toto_thm

|- !r. WeakLinearOrder r ==>
       (WeakLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)

all_cpn_distinct

|- (LESS <> EQUAL /\ LESS <> GREATER /\ EQUAL <> GREATER) /\
   EQUAL <> LESS /\ GREATER <> LESS /\ GREATER <> EQUAL

ap_qk_numto_thm

|- apto qk_numto = qk_numOrd

apcharto_thm

|- apto charto = charOrd

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

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

apnumto_thm

|- apto numto = numOrd

apto_inv

|- !c. apto (toto_inv c) = TO_inv (apto c)

charOrd_eq_lem

|- !a b. (numOrd a b = EQUAL) ==> (charOrd (CHR a) (CHR b) = EQUAL)

charOrd_gt_lem

|- !a b.
     (numOrd a b = GREATER) ==>
     (a < 256 <=> T) ==>
     (charOrd (CHR a) (CHR b) = GREATER)

charOrd_lt_lem

|- !a b.
     (numOrd a b = LESS) ==>
     (b < 256 <=> T) ==>
     (charOrd (CHR a) (CHR b) = LESS)

charOrd_thm

|- charOrd = TO_of_LinearOrder char_lt

datatype_num_dt

|- DATATYPE (num_dt zer bit1 bit2)

inv_TO

|- !r. TotOrd r ==> (toto_inv (TO r) = TO (TO_inv r))

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

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

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

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

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

|- (!a a'. (bit1 a = bit1 a') <=> (a = a')) /\
   !a a'. (bit2 a = bit2 a') <=> (a = a')

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

|- (!a. zer <> bit1 a) /\ (!a. zer <> bit2 a) /\ !a' a. bit1 a <> bit2 a'

num_dt_induction

|- !P. P zer /\ (!n. P n ==> P (bit1 n)) /\ (!n. P n ==> P (bit2 n)) ==>
       !n. P n

num_dt_nchotomy

|- !nn. (nn = zer) \/ (?n. nn = bit1 n) \/ ?n. nn = bit2 n

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)

onto_apto

|- !r. TotOrd r <=> ?a. r = apto a

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

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)

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

totoELtrans

|- !c x y z.
     (apto c x y = EQUAL) /\ (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)

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)

totoLGtrans

|- !c x y z.
     (apto c x y = LESS) /\ (apto c z y = GREATER) ==> (apto c x z = LESS)

totoLLtrans

|- !c x y z.
     (apto c x y = LESS) /\ (apto c y z = LESS) ==> (apto c x z = LESS)

toto_Strong_thm

|- !c. toto_of_LinearOrder (StrongLinearOrder_of_TO (apto c)) = c

toto_Weak_thm

|- !c. toto_of_LinearOrder (WeakLinearOrder_of_TO (apto c)) = c

toto_antisym

|- !c x y. (apto c x y = GREATER) <=> (apto c y x = LESS)

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_equal_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_imp_eq

|- !c x y. (apto c x y = EQUAL) ==> (x = y)

toto_equal_sym

|- !c x y. (apto c x y = EQUAL) <=> (apto c y x = EQUAL)

toto_glneq

|- (!c x y. (apto c x y = LESS) ==> x <> y) /\
   !c x y. (apto c x y = GREATER) ==> x <> y

toto_inv_toto_inv

|- !c. toto_inv (toto_inv c) = c

toto_not_less_refl

|- !cmp h. (apto cmp h h = LESS) <=> F

toto_refl

|- !c x. apto c x x = EQUAL

toto_swap_cases

|- !c x y.
     apto c y x =
     case apto c x y of LESS => GREATER | EQUAL => EQUAL | GREATER => 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_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_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

trichotomous_ALT

|- !R. trichotomous R <=> !x y. ~R x y /\ ~R y x ==> (x = y)

Theory toto

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems