Theory "ternaryComparisons"

Parents string

Signature

Type	Arity
ordering	0
Constant	Type
EQUAL	:ordering
GREATER	:ordering
LESS	:ordering
bool_compare	:bool -> bool -> ordering
char_compare	:char -> char -> ordering
invert_comparison	:ordering -> ordering
list_compare	:(α -> β -> ordering) -> α list -> β list -> ordering
list_merge	:(α -> α -> bool) -> α list -> α list -> α list
num2ordering	:num -> ordering
num_compare	:num -> num -> ordering
option_compare	:(α -> β -> ordering) -> α option -> β option -> ordering
ordering2num	:ordering -> num
ordering_CASE	:ordering -> α -> α -> α -> α
ordering_size	:ordering -> num
pair_compare	:(α -> β -> ordering) -> (γ -> δ -> ordering) -> α # γ -> β # δ -> ordering
string_compare	:string -> string -> ordering

Definitions

string_compare_def

⊢ string_cmp = list_cmp char_cmp

pair_compare_def

⊢ ∀c1 c2 a b x y.
      pair_cmp c1 c2 (a,b) (x,y) =
      case c1 a x of Less => Less | Equal => c2 b y | Greater => Greater

ordering_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λn. n < 3) rep

ordering_size_def

⊢ ∀x. ordering_size x = 0

ordering_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) (ordering2num x)

ordering_BIJ

⊢ (∀a. num2ordering (ordering2num a) = a) ∧
  ∀r. (λn. n < 3) r ⇔ (ordering2num (num2ordering r) = r)

num_compare_def

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

invert_comparison_def

⊢ (invert_comparison Greater = Less) ∧ (invert_comparison Less = Greater) ∧
  (invert_comparison Equal = Equal)

char_compare_def

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

Theorems

ordering_nchotomy

⊢ ∀a. (a = Less) ∨ (a = Equal) ∨ (a = Greater)

ordering_induction

⊢ ∀P. P Equal ∧ P Greater ∧ P Less ⇒ ∀a. P a

ordering_EQ_ordering

⊢ ∀a a'. (a = a') ⇔ (ordering2num a = ordering2num a')

ordering_eq_dec

⊢ (∀x. (x = x) ⇔ T) ∧ ((Less = Equal) ⇔ F) ∧ ((Less = Greater) ⇔ F) ∧
  ((Equal = Greater) ⇔ F) ∧ ((Equal = Less) ⇔ F) ∧ ((Greater = Less) ⇔ F) ∧
  ((Greater = Equal) ⇔ F) ∧
  ((ordering2num Less = 0) ∧ (ordering2num Equal = 1) ∧
   (ordering2num Greater = 2)) ∧ (num2ordering 0 = Less) ∧
  (num2ordering 1 = Equal) ∧ (num2ordering 2 = Greater)

ordering_distinct

⊢ Less ≠ Equal ∧ Less ≠ Greater ∧ Equal ≠ Greater

ordering_case_eq

⊢ ((case x of Less => v0 | Equal => v1 | Greater => v2) = v) ⇔
  (x = Less) ∧ (v0 = v) ∨ (x = Equal) ∧ (v1 = v) ∨ (x = Greater) ∧ (v2 = v)

ordering_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

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

ordering_Axiom

⊢ ∀x0 x1 x2. ∃f. (f Less = x0) ∧ (f Equal = x1) ∧ (f Greater = x2)

ordering2num_thm

⊢ (ordering2num Less = 0) ∧ (ordering2num Equal = 1) ∧
  (ordering2num Greater = 2)

ordering2num_ONTO

⊢ ∀r. r < 3 ⇔ ∃a. r = ordering2num a

ordering2num_num2ordering

⊢ ∀r. r < 3 ⇔ (ordering2num (num2ordering r) = r)

ordering2num_11

⊢ ∀a a'. (ordering2num a = ordering2num a') ⇔ (a = a')

option_compare_ind

⊢ ∀P.
      (∀c. P c NONE NONE) ∧ (∀c v0. P c NONE (SOME v0)) ∧
      (∀c v3. P c (SOME v3) NONE) ∧ (∀c v1 v2. P c (SOME v1) (SOME v2)) ⇒
      ∀v v1 v2. P v v1 v2

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

num2ordering_thm

⊢ (num2ordering 0 = Less) ∧ (num2ordering 1 = Equal) ∧
  (num2ordering 2 = Greater)

num2ordering_ordering2num

⊢ ∀a. num2ordering (ordering2num a) = a

num2ordering_ONTO

⊢ ∀a. ∃r. (a = num2ordering r) ∧ r < 3

num2ordering_11

⊢ ∀r r'. r < 3 ⇒ r' < 3 ⇒ ((num2ordering r = num2ordering r') ⇔ (r = r'))

list_merge_ind

⊢ ∀P.
      (∀a_lt l1. P a_lt l1 []) ∧ (∀a_lt v4 v5. P a_lt [] (v4::v5)) ∧
      (∀a_lt x l1 y l2.
           (¬a_lt x y ⇒ P a_lt (x::l1) l2) ∧ (a_lt x y ⇒ P a_lt l1 (y::l2)) ⇒
           P a_lt (x::l1) (y::l2)) ⇒
      ∀v v1 v2. P v v1 v2

list_merge_def

⊢ (∀l1 a_lt. list_merge a_lt l1 [] = l1) ∧
  (∀v5 v4 a_lt. list_merge a_lt [] (v4::v5) = v4::v5) ∧
  ∀y x l2 l1 a_lt.
      list_merge a_lt (x::l1) (y::l2) =
      if a_lt x y then x::list_merge a_lt l1 (y::l2)
      else y::list_merge a_lt (x::l1) l2

list_compare_ind

⊢ ∀P.
      (∀cmp. P cmp [] []) ∧ (∀cmp v8 v9. P cmp [] (v8::v9)) ∧
      (∀cmp v4 v5. P cmp (v4::v5) []) ∧
      (∀cmp x l1 y l2.
           ((cmp x y = Equal) ⇒ P cmp l1 l2) ⇒ P cmp (x::l1) (y::l2)) ⇒
      ∀v v1 v2. P v v1 v2

list_compare_def

⊢ (∀cmp. list_cmp cmp [] [] = Equal) ∧
  (∀v9 v8 cmp. list_cmp cmp [] (v8::v9) = Less) ∧
  (∀v5 v4 cmp. list_cmp cmp (v4::v5) [] = Greater) ∧
  ∀y x l2 l1 cmp.
      list_cmp cmp (x::l1) (y::l2) =
      case cmp x y of
        Less => Less
      | Equal => list_cmp cmp l1 l2
      | Greater => Greater

invert_eq_EQUAL

⊢ ∀x. (invert_comparison x = Equal) ⇔ (x = Equal)

datatype_ordering

⊢ DATATYPE (ordering Less Equal Greater)

compare_equal

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

bool_compare_ind

⊢ ∀P. P T T ∧ P F F ∧ P T F ∧ P F T ⇒ ∀v v1. P v v1

bool_compare_def

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