Theory "comparison"

Signature

Definitions

good_cmp_def

|- ∀cmp.
     good_cmp cmp ⇔
     (∀x. cmp x x = Equal) ∧ (∀x y. (cmp x y = Equal) ⇒ (cmp y x = Equal)) ∧
     (∀x y. (cmp x y = Greater) ⇔ (cmp y x = Less)) ∧
     (∀x y z. (cmp x y = Equal) ∧ (cmp y z = Less) ⇒ (cmp x z = Less)) ∧
     (∀x y z. (cmp x y = Less) ∧ (cmp y z = Equal) ⇒ (cmp x z = Less)) ∧
     (∀x y z. (cmp x y = Equal) ∧ (cmp y z = Equal) ⇒ (cmp x z = Equal)) ∧
     ∀x y z. (cmp x y = Less) ∧ (cmp y z = Less) ⇒ (cmp x z = Less)

option_cmp_tupled_primitive_def

|- option_cmp_tupled =
   WFREC (@R. WF R)
     (λoption_cmp_tupled a.
        case a of
          (cmp,NONE,NONE) => I Equal
        | (cmp,NONE,SOME x) => I Less
        | (cmp,SOME x',NONE) => I Greater
        | (cmp,SOME x',SOME y) => I (cmp x' y))

option_cmp_curried_def

|- ∀x x1 x2. option_cmp x x1 x2 = option_cmp_tupled (x,x1,x2)

option_cmp2_tupled_primitive_def

|- option_cmp2_tupled =
   WFREC (@R. WF R)
     (λoption_cmp2_tupled a.
        case a of
          (cmp,NONE,NONE) => I Equal
        | (cmp,NONE,SOME x) => I Greater
        | (cmp,SOME x',NONE) => I Less
        | (cmp,SOME x',SOME y) => I (cmp x' y))

option_cmp2_curried_def

|- ∀x x1 x2. option_cmp2 x x1 x2 = option_cmp2_tupled (x,x1,x2)

list_cmp_tupled_primitive_def

|- list_cmp_tupled =
   WFREC
     (@R.
        WF R ∧
        ∀y2 y1 x2 x1 cmp.
          (cmp x1 x2 = Equal) ⇒ R (cmp,y1,y2) (cmp,x1::y1,x2::y2))
     (λlist_cmp_tupled a.
        case a of
          (cmp,[],[]) => I Equal
        | (cmp,[],x::y) => I Less
        | (cmp,x'::y',[]) => I Greater
        | (cmp,x'::y',x2::y2) =>
            I
              (case cmp x' x2 of
                 Less => Less
               | Equal => list_cmp_tupled (cmp,y',y2)
               | Greater => Greater))

list_cmp_curried_def

|- ∀x x1 x2. list_cmp x x1 x2 = list_cmp_tupled (x,x1,x2)

pair_cmp_def

|- ∀cmp1 cmp2 x y.
     pair_cmp cmp1 cmp2 x y =
     case cmp1 (FST x) (FST y) of
       Less => Less
     | Equal => cmp2 (SND x) (SND y)
     | Greater => Greater

bool_cmp_tupled_primitive_def

|- bool_cmp_tupled =
   WFREC (@R. WF R)
     (λbool_cmp_tupled a.
        case a of
          (T,T) => I Equal
        | (T,F) => I Greater
        | (F,T) => I Less
        | (F,F) => I Equal)

bool_cmp_curried_def

|- ∀x x1. bool_cmp x x1 = bool_cmp_tupled (x,x1)

num_cmp_def

|- ∀n1 n2.
     num_cmp n1 n2 =
     if n1 = n2 then Equal else if n1 < n2 then Less else Greater

char_cmp_def

|- ∀c1 c2. char_cmp c1 c2 = num_cmp (ORD c1) (ORD c2)

string_cmp_def

|- string_cmp = list_cmp char_cmp

invert_def

|- (invert Greater = Less) ∧ (invert Less = Greater) ∧ (invert Equal = Equal)

resp_equiv_def

|- ∀cmp f.
     resp_equiv cmp f ⇔ ∀k1 k2 v. (cmp k1 k2 = Equal) ⇒ (f k1 v = f k2 v)

resp_equiv2_def

|- ∀cmp cmp2 f.
     resp_equiv2 cmp cmp2 f ⇔
     ∀k1 k2. (cmp k1 k2 = Equal) ⇒ (cmp2 (f k1) (f k2) = Equal)

equiv_inj_def

|- ∀cmp cmp2 f.
     equiv_inj cmp cmp2 f ⇔
     ∀k1 k2. (cmp2 (f k1) (f k2) = Equal) ⇒ (cmp k1 k2 = Equal)

Theorems

comparison_distinct

|- Less ≠ Equal ∧ Less ≠ Greater ∧ Equal ≠ Greater

comparison_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

comparison_nchotomy

|- ∀a. (a = Less) ∨ (a = Equal) ∨ (a = Greater)

good_cmp_thm

|- ∀cmp.
     good_cmp cmp ⇔
     (∀x. cmp x x = Equal) ∧
     ∀x y z.
       ((cmp x y = Greater) ⇔ (cmp y x = Less)) ∧
       ((cmp x y = Less) ∧ (cmp y z = Equal) ⇒ (cmp x z = Less)) ∧
       ((cmp x y = Less) ∧ (cmp y z = Less) ⇒ (cmp x z = Less))

cmp_thms

|- (Less ≠ Equal ∧ Less ≠ Greater ∧ Equal ≠ Greater) ∧
   ((∀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) ∧
   (∀a. (a = Less) ∨ (a = Equal) ∨ (a = Greater)) ∧
   ∀cmp.
     good_cmp cmp ⇔
     (∀x. cmp x x = Equal) ∧ (∀x y. (cmp x y = Equal) ⇒ (cmp y x = Equal)) ∧
     (∀x y. (cmp x y = Greater) ⇔ (cmp y x = Less)) ∧
     (∀x y z. (cmp x y = Equal) ∧ (cmp y z = Less) ⇒ (cmp x z = Less)) ∧
     (∀x y z. (cmp x y = Less) ∧ (cmp y z = Equal) ⇒ (cmp x z = Less)) ∧
     (∀x y z. (cmp x y = Equal) ∧ (cmp y z = Equal) ⇒ (cmp x z = Equal)) ∧
     ∀x y z. (cmp x y = Less) ∧ (cmp y z = Less) ⇒ (cmp x z = Less)

option_cmp_ind

|- ∀P.
     (∀cmp. P cmp NONE NONE) ∧ (∀cmp x. P cmp NONE (SOME x)) ∧
     (∀cmp x. P cmp (SOME x) NONE) ∧ (∀cmp x y. P cmp (SOME x) (SOME y)) ⇒
     ∀v v1 v2. P v v1 v2

option_cmp_def

|- (option_cmp cmp NONE NONE = Equal) ∧
   (option_cmp cmp NONE (SOME x') = Less) ∧
   (option_cmp cmp (SOME x) NONE = Greater) ∧
   (option_cmp cmp (SOME x) (SOME y) = cmp x y)

option_cmp2_ind

|- ∀P.
     (∀cmp. P cmp NONE NONE) ∧ (∀cmp x. P cmp NONE (SOME x)) ∧
     (∀cmp x. P cmp (SOME x) NONE) ∧ (∀cmp x y. P cmp (SOME x) (SOME y)) ⇒
     ∀v v1 v2. P v v1 v2

option_cmp2_def

|- (option_cmp2 cmp NONE NONE = Equal) ∧
   (option_cmp2 cmp NONE (SOME x') = Greater) ∧
   (option_cmp2 cmp (SOME x) NONE = Less) ∧
   (option_cmp2 cmp (SOME x) (SOME y) = cmp x y)

list_cmp_ind

|- ∀P.
     (∀cmp. P cmp [] []) ∧ (∀cmp x y. P cmp [] (x::y)) ∧
     (∀cmp x y. P cmp (x::y) []) ∧
     (∀cmp x1 y1 x2 y2.
        ((cmp x1 x2 = Equal) ⇒ P cmp y1 y2) ⇒ P cmp (x1::y1) (x2::y2)) ⇒
     ∀v v1 v2. P v v1 v2

list_cmp_def

|- (∀cmp. list_cmp cmp [] [] = Equal) ∧
   (∀y x cmp. list_cmp cmp [] (x::y) = Less) ∧
   (∀y x cmp. list_cmp cmp (x::y) [] = Greater) ∧
   ∀y2 y1 x2 x1 cmp.
     list_cmp cmp (x1::y1) (x2::y2) =
     case cmp x1 x2 of
       Less => Less
     | Equal => list_cmp cmp y1 y2
     | Greater => Greater

bool_cmp_ind

|- ∀P. P T T ∧ P F F ∧ P T F ∧ P F T ⇒ ∀v v1. P v v1

bool_cmp_def

|- (bool_cmp T T = Equal) ∧ (bool_cmp F F = Equal) ∧
   (bool_cmp T F = Greater) ∧ (bool_cmp F T = Less)

TotOrder_imp_good_cmp

|- ∀cmp. TotOrd cmp ⇒ good_cmp cmp

invert_eq_EQUAL

|- ∀x. (invert x = Equal) ⇔ (x = Equal)

TO_inv_invert

|- ∀c. TotOrd c ⇒ (TO_inv c = CURRY (invert o UNCURRY c))

option_cmp2_TO_inv

|- ∀c. option_cmp2 c = TO_inv (option_cmp (TO_inv c))

list_cmp_ListOrd

|- ∀c. TotOrd c ⇒ (list_cmp c = ListOrd (TO c))

pair_cmp_lexTO

|- ∀R V. TotOrd R ∧ TotOrd V ⇒ (pair_cmp R V = R lexTO V)

num_cmp_numOrd

|- num_cmp = numOrd

char_cmp_charOrd

|- char_cmp = charOrd

string_cmp_stringto

|- string_cmp = apto stringto

option_cmp_good

|- ∀cmp. good_cmp cmp ⇒ good_cmp (option_cmp cmp)

option_cmp2_good

|- ∀cmp. good_cmp cmp ⇒ good_cmp (option_cmp2 cmp)

list_cmp_good

|- ∀cmp. good_cmp cmp ⇒ good_cmp (list_cmp cmp)

pair_cmp_good

|- ∀cmp1 cmp2. good_cmp cmp1 ∧ good_cmp cmp2 ⇒ good_cmp (pair_cmp cmp1 cmp2)

bool_cmp_good

|- good_cmp bool_cmp

num_cmp_good

|- good_cmp num_cmp

char_cmp_good

|- good_cmp char_cmp

string_cmp_good

|- good_cmp string_cmp

list_cmp_cong

|- ∀cmp l1 l2 cmp' l1' l2'.
     (l1 = l1') ∧ (l2 = l2') ∧
     (∀x x'. MEM x l1' ∧ MEM x' l2' ⇒ (cmp x x' = cmp' x x')) ⇒
     (list_cmp cmp l1 l2 = list_cmp cmp' l1' l2')

option_cmp_cong

|- ∀cmp v1 v2 cmp' v1' v2'.
     (v1 = v1') ∧ (v2 = v2') ∧
     (∀x x'. (v1' = SOME x) ∧ (v2' = SOME x') ⇒ (cmp x x' = cmp' x x')) ⇒
     (option_cmp cmp v1 v2 = option_cmp cmp' v1' v2')

option_cmp2_cong

|- ∀cmp v1 v2 cmp' v1' v2'.
     (v1 = v1') ∧ (v2 = v2') ∧
     (∀x x'. (v1' = SOME x) ∧ (v2' = SOME x') ⇒ (cmp x x' = cmp' x x')) ⇒
     (option_cmp2 cmp v1 v2 = option_cmp2 cmp' v1' v2')

pair_cmp_cong

|- ∀cmp1 cmp2 v1 v2 cmp1' cmp2' v1' v2'.
     (v1 = v1') ∧ (v2 = v2') ∧
     (∀a b c d. (v1' = (a,b)) ∧ (v2' = (c,d)) ⇒ (cmp1 a c = cmp1' a c)) ∧
     (∀a b c d. (v1' = (a,b)) ∧ (v2' = (c,d)) ⇒ (cmp2 b d = cmp2' b d)) ⇒
     (pair_cmp cmp1 cmp2 v1 v2 = pair_cmp cmp1' cmp2' v1' v2')

good_cmp_trans

|- ∀cmp. good_cmp cmp ⇒ transitive (λ(k,v) (k',v'). cmp k k' = Less)

bool_cmp_antisym

|- ∀x y. (bool_cmp x y = Equal) ⇔ (x ⇔ y)

num_cmp_antisym

|- ∀x y. (num_cmp x y = Equal) ⇔ (x = y)

char_cmp_antisym

|- ∀x y. (char_cmp x y = Equal) ⇔ (x = y)

list_cmp_antisym

|- ∀cmp x y.
     (∀x y. (cmp x y = Equal) ⇔ (x = y)) ⇒
     ((list_cmp cmp x y = Equal) ⇔ (x = y))

string_cmp_antisym

|- ∀x y. (string_cmp x y = Equal) ⇔ (x = y)

pair_cmp_antisym

|- ∀cmp1 cmp2 x y.
     (∀x y. (cmp1 x y = Equal) ⇔ (x = y)) ∧
     (∀x y. (cmp2 x y = Equal) ⇔ (x = y)) ⇒
     ((pair_cmp cmp1 cmp2 x y = Equal) ⇔ (x = y))

option_cmp_antisym

|- ∀cmp x y.
     (∀x y. (cmp x y = Equal) ⇔ (x = y)) ⇒
     ((option_cmp cmp x y = Equal) ⇔ (x = y))

option_cmp2_antisym

|- ∀cmp x y.
     (∀x y. (cmp x y = Equal) ⇔ (x = y)) ⇒
     ((option_cmp2 cmp x y = Equal) ⇔ (x = y))

antisym_resp_equiv

|- ∀cmp f.
     (∀x y. (cmp x y = Equal) ⇒ (x = y)) ⇒
     resp_equiv cmp f ∧ ∀cmp2. good_cmp cmp2 ⇒ resp_equiv2 cmp cmp2 f

list_cmp_equal_list_rel

|- ∀cmp l1 l2.
     (list_cmp cmp l1 l2 = Equal) ⇔ LIST_REL (λx y. cmp x y = Equal) l1 l2