Theory "comparison"

Signature

Definitions

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)

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)

equiv_inj_def

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

Theorems

TotOrder_imp_good_cmp

⊢ ∀cmp. TotOrd cmp ⇒ good_cmp cmp

TotOrd_list_cmp

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

TO_of_LinearOrder_LLEX

⊢ ∀R.
      irreflexive R ⇒
      (TO_of_LinearOrder (LLEX R) = list_cmp (TO_of_LinearOrder R))

TO_inv_invert

⊢ ∀c. TotOrd c ⇒ (TO_inv c = CURRY (invert_comparison ∘ UNCURRY c))

string_cmp_stringto

⊢ string_cmp = apto stringto

string_cmp_good

⊢ good_cmp string_cmp

string_cmp_def

⊢ string_cmp = list_cmp char_cmp

string_cmp_antisym

⊢ ∀x y. (string_cmp x y = Equal) ⇔ (x = y)

pair_cmp_lexTO

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

pair_cmp_good

⊢ ∀cmp1 cmp2. good_cmp cmp1 ∧ good_cmp cmp2 ⇒ good_cmp (pair_cmp cmp1 cmp2)

pair_cmp_def

⊢ pair_cmp c1 c2 x y =
  case c1 (FST x) (FST y) of
    Less => Less
  | Equal => c2 (SND x) (SND y)
  | Greater => Greater

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

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_good

⊢ ∀cmp. good_cmp cmp ⇒ good_cmp (option_cmp cmp)

option_cmp_def

⊢ (option_cmp c NONE NONE = Equal) ∧ (option_cmp c NONE (SOME v0) = Less) ∧
  (option_cmp c (SOME v3) NONE = Greater) ∧
  (option_cmp c (SOME v1) (SOME v2) = c v1 v2)

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_cmp_antisym

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

option_cmp2_TO_inv

⊢ ∀c. option_cmp2 c = TO_inv (option_cmp (TO_inv c))

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_good

⊢ ∀cmp. good_cmp cmp ⇒ good_cmp (option_cmp2 cmp)

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)

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

option_cmp2_antisym

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

num_cmp_numOrd

⊢ num_cmp = numOrd

num_cmp_good

⊢ good_cmp num_cmp

num_cmp_def

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

num_cmp_antisym

⊢ ∀x y. (num_cmp x y = Equal) ⇔ (x = y)

list_cmp_ListOrd

⊢ ∀c. TotOrd c ⇒ (list_cmp c = ListOrd (TO c))

list_cmp_good

⊢ ∀cmp. good_cmp cmp ⇒ good_cmp (list_cmp cmp)

list_cmp_equal_list_rel

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

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

list_cmp_antisym

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

good_cmp_trans

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

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

good_cmp_Less_trans

⊢ ∀cmp. good_cmp cmp ⇒ transitive (λk k'. cmp k k' = Less)

good_cmp_Less_irrefl_trans

⊢ ∀cmp.
      good_cmp cmp ⇒
      irreflexive (λk k'. cmp k k' = Less) ∧
      transitive (λk k'. cmp k k' = 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)

char_cmp_good

⊢ good_cmp char_cmp

char_cmp_def

⊢ ∀c1 c2. char_cmp c1 c2 = num_cmp (ORD c1) (ORD c2)

char_cmp_charOrd

⊢ char_cmp = charOrd

char_cmp_antisym

⊢ ∀x y. (char_cmp x y = Equal) ⇔ (x = y)

bool_cmp_good

⊢ good_cmp bool_cmp

bool_cmp_def

⊢ (bool_cmp T T = Equal) ∧ (bool_cmp F F = Equal) ∧ (bool_cmp T F = Greater) ∧
  (bool_cmp F T = Less)

bool_cmp_antisym

⊢ ∀x y. (bool_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