nat.timl

(* Operations for indexed natural numbers *)

structure Nat = struct

datatype cmp_result {a b : Nat} =
         Equal {a = b} of cmp_result {a} {b} 
       | Less {a < b} of cmp_result {a} {b}
       | Greater {a > b} of cmp_result {a} {b} 

fun cmp {x y : Nat} (x : nat {x}, y : nat {y}) return cmp_result {x} {y} using 0.0 =
    builtin

datatype le_result : {Nat} {Nat} =
         Le {a b : Nat} {a <= b} of le_result {a} {b} 
       | Gt {a b : Nat} {a > b} of le_result {a} {b} 

fun le {x : Nat} {y : Nat} (x : nat {x}, y : nat {y}) return le_result {x} {y} using 7.0 =
    case cmp (x, y) of
        Equal => Le
      | Less => Le
      | Greater => Gt

datatype min_max_result : {Nat} {Nat} =
         MinMaxResult {a b a' b' : Nat} {(a <= b -> a' = a /\ b' = b) /\ (a > b -> a' = b /\ b' = a)} of nat {a'} * nat {b'} --> min_max_result {a} {b} 

fun min_max {m : Time} {x y : Nat} (le : nat {x} * nat {y} -- m --> le_result {x} {y}) (x : nat {x}, y : nat {y}) return min_max_result {x} {y} =
    case le (x, y) of
        Le => MinMaxResult (x, y)
      | Gt => MinMaxResult (y, x)

datatype eq_dec {a b : Nat} =
         Eq {a = b} of eq_dec {a} {b}
       | Neq {a <> b} of eq_dec {a} {b}

fun eq_dec {x y : Nat} (x : nat {x}, y : nat {y}) return eq_dec {x} {y} using 1.0 =
    case cmp (x, y) of
        Equal => Eq
      | Less => Neq
      | Greater => Neq

datatype lt_dec {a b : Nat} =
         Lt {a < b} of lt_dec {a} {b}
       | Ge {a >= b} of lt_dec {a} {b}

fun lt_dec {x y : Nat} (x : nat {x}, y : nat {y}) return lt_dec {x} {y} using 1.0 =
    case cmp (x, y) of
        Equal => Ge
      | Less => Lt
      | Greater => Ge

val nat_1 : nat {1} = #1
val nat_2 : nat {2} = #2
val nat_4 : nat {4} = #4

fun nat_plus {a b : Nat} (a : nat {a}, b : nat {b}) return nat {a + b} using 1.0 =
    builtin

fun nat_minus {a b : Nat} {a >= b} (a : nat {a}, b : nat {b}) return nat {a - b} using 1.0 =
    builtin

fun nat_mult {a b : Nat} (a : nat {a}, b : nat {b}) return nat {a * b} using 1.0 =
    builtin

fun nat_max {a b : Nat} (a : nat {a}, b : nat {b}) return nat {a max b} using 1.0 =
    builtin

fun floor_half {n : Nat} (n : nat {n}) return nat {floor ($n / 2)} =
    builtin

fun ceil_half {n : Nat} (n : nat {n}) return nat {ceil ($n / 2)} =
    builtin

datatype nat_less_than {m : Nat} =
         NatLT {n : Nat} {n < m} of nat {n} --> nat_less_than {m}

end