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

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

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

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

bool_cmp_def

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

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

TotOrder_imp_good_cmp

⊢ ∀cmp. TotOrd cmp ⇒ good_cmp cmp

TO_inv_invert

⊢ ∀c. TotOrd c ⇒ TO_inv c = CURRY (invert_comparison ∘ 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)

TotOrd_list_cmp

⊢ ∀c. TotOrd c ⇒ TotOrd (list_cmp 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

TO_of_LinearOrder_LLEX

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