Theory "ternaryComparisons"

Parents string

Signature

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

Definitions

ordering_TY_DEF

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

ordering_BIJ

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

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)

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

num_compare_def

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

char_compare_def

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

string_compare_def

⊢ string_cmp = list_cmp char_cmp

invert_comparison_def

⊢ invert_comparison Greater = Less ∧ invert_comparison Less = Greater ∧
  invert_comparison Equal = Equal

Theorems

num2ordering_ordering2num

⊢ ∀a. num2ordering (ordering2num a) = a

ordering2num_num2ordering

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

num2ordering_11

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

ordering2num_11

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

num2ordering_ONTO

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

ordering2num_ONTO

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

num2ordering_thm

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

ordering2num_thm

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

ordering_EQ_ordering

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

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

datatype_ordering

⊢ DATATYPE (ordering Less Equal Greater)

ordering_distinct

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

ordering_nchotomy

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

ordering_Axiom

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

ordering_induction

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

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_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_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) ∧
  ((∀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) ∧
  (Less = Equal ⇔ F) ∧ (Less = Greater ⇔ F) ∧ (Equal = Greater ⇔ F) ∧
  (Equal = Less ⇔ F) ∧ (Greater = Less ⇔ F) ∧ (Greater = Equal ⇔ F)

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

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

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

compare_equal

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

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

invert_eq_EQUAL

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