next up previous contents
Next: All order relations Up: Order relations Previous: Propositional Relations

Boolean-valued Relations

The order relations on nat are decidable so another way to represent them is via boolean valued functions. The following file defines boolean-valued strict and non-strict inequality plus the boolean-valued equality. Most of the propositional order relation theorems have a boolean counterpart, the most useful of which are included in the library.

 ** Module lib_nat_bool_rels Imports lib_nat_suc_thms lib_bool_thms
  lt = ... : nat->nat->bool
  le = ... : nat->nat->bool
  nat_eq = ... : nat->nat->bool
  zero_lt_suc = ... : {n:nat}is_true (lt zero (suc n))
  zero_le_suc = ... : {n:nat}is_true (le zero (suc n))
  not_n_lt_zero = ... : {n:nat}is_false (lt n zero)
  lt_resp_suc = ... : {n,m:nat}Eq (lt n m) (lt (suc n) (suc m))
  le_resp_suc = ... : {n,m:nat}Eq (le n m) (le (suc n) (suc m))
  not_n_lt_n = ... : {n:nat}is_false (lt n n)
  n_lt_suc_n = ... : {n:nat}is_true (lt n (suc n))
  not_lt_suc_is_suc = ... : {m,n:nat}(is_false (lt m (suc n)))->is_suc m
  lt_weak_trans = ... :
    {m,n|nat}(is_true (lt m n))->is_true (lt m (suc n))
  lt_left_suc = ... :
    {n,m:nat}(is_true (lt (suc n) m))->is_true (lt n m)
  lt_suc_character = ... :
    {m,n:nat}(is_true (lt n (suc m)))->(Eq n m \/ is_true (lt n m))
  lt_character = ... :
    {n,m:nat}
    ((is_true (lt n m) /\ is_false (lt m n)) \/
     ((is_true (lt m n) /\ is_false (lt n m)) \/ Eq n m))
  le_character = ... :
    {n,m:nat}
    ((is_true (le n m) /\ is_false (le m n)) \/
     ((is_true (le m n) /\ is_false (le n m)) \/ Eq n m))
  le_refl = ... : {n:nat}is_true (le n n)
  le_zero_imp_zero = ... : {n:nat}iff (is_true (le n zero)) (Eq n zero)
  le_not_lt_imp_Eq = ... :
    {i,n:nat}(is_true (le i n) /\ is_false (lt i n))->Eq i n
  lt_imp_le_suc = ... :
    {x,y|nat}(is_true (lt x y))->is_true (le (suc x) y)
  nat_eq_character = ... : {m,n:nat}iff (is_true (nat_eq m n)) (Eq m n)
  nat_eq_character' = ... :
    {m,n:nat}iff (is_false (nat_eq m n)) (not (Eq m n))
  nat_eq_sym = ... : {m,n:nat}Eq (nat_eq m n) (nat_eq n m)
  nat_eq_refl = ... : {n:nat}is_true (nat_eq n n)
  odd = ... : nat->bool
  even = ... : nat->bool



Conor McBride
11/13/1998