stdlib/tptp.mlw

   1 module Univ
   2   type iType
   3 end
   4
   5 module Ghost
   6   type gh 'a
   7
   8   constant gh : gh 'a
   9 end
  10
  11 module Int
  12   use export int.Int
  13 end
  14
  15 module IntTrunc
  16   function floor (x : int) : int = x
  17   function ceiling (x : int) : int = x
  18   function truncate (x : int) : int = x
  19   function round (x : int) : int = x
  20
  21   function to_int (x : int) : int = x
  22
  23   predicate is_int int = true
  24   predicate is_rat int = true
  25 end
  26
  27 module IntDivE
  28   use export int.EuclideanDivision
  29 end
  30
  31 module IntDivT
  32   (* TODO: divide and truncate *)
  33   function div_t (x y : int) : int
  34   function mod_t (x y : int) : int
  35 end
  36
  37 module IntDivF
  38   (* TODO: divide and floor *)
  39   function div_f (x y : int) : int
  40   function mod_f (x y : int) : int
  41 end
  42
  43 module Rat
  44   use int.Int as Int
  45
  46   type rat
  47
  48   predicate (< ) (x y : rat)
  49   predicate (> ) (x y : rat) = y < x
  50   predicate (<=) (x y : rat) = x < y \/ x = y
  51   predicate (>=) (x y : rat) = y <= x
  52
  53   clone export algebra.OrderedField
  54     with type t = rat, predicate (<=) = (<=)
  55
  56   function frac (n d : int) : rat
  57
  58   function numerator rat : int
  59   function denominator rat : int
  60
  61   axiom inversion : forall r : rat. r = frac (numerator r) (denominator r)
  62   axiom dpositive : forall r : rat. Int.(>) (denominator r) 0
  63
  64   axiom frac_zero : forall d : int. d <> 0 -> frac 0 d = zero
  65   axiom frac_unit : forall d : int. d <> 0 -> frac d d = one
  66
  67   axiom nume_zero : numerator zero = 0
  68   axiom deno_zero : denominator zero = 1
  69
  70   axiom nume_unit : numerator one = 1
  71   axiom deno_unit : denominator one = 1
  72
  73   axiom proportion : forall n1 n2 d1 d2 : int. d1 <> 0 -> d2 <> 0 ->
  74     (frac n1 d1 = frac n2 d2 <-> Int.(*) n1 d2 = Int.(*) n2 d1)
  75
  76   function to_rat (x : rat) : rat = x
  77
  78   predicate is_int (r : rat) = denominator r = 1
  79   predicate is_rat rat = true
  80 end
  81
  82 module RatTrunc
  83   use Rat
  84
  85   (* TODO: axiomatize *)
  86   function floor (x : rat) : rat
  87   function ceiling (x : rat) : rat
  88   function truncate (x : rat) : rat
  89   function round (x : rat) : rat
  90
  91   function to_int (x : rat) : int = numerator (floor x)
  92 end
  93
  94 module RatDivE
  95   use Rat
  96
  97   (* TODO: euclidean division *)
  98   function div (x y : rat) : rat
  99   function mod (x y : rat) : rat
 100 end
 101
 102 module RatDivT
 103   use Rat
 104
 105   (* TODO: divide and truncate *)
 106   function div_t (x y : rat) : rat
 107   function mod_t (x y : rat) : rat
 108 end
 109
 110 module RatDivF
 111   use Rat
 112
 113   (* TODO: divide and floor *)
 114   function div_f (x y : rat) : rat
 115   function mod_f (x y : rat) : rat
 116 end
 117
 118 module Real
 119   use export real.Real
 120   function to_real (x : real) : real = x
 121 end
 122
 123 module RealTrunc
 124   use Real
 125   use real.FromInt as FromInt
 126   use real.Truncate as Truncate
 127
 128   function floor (x : real) : real = FromInt.from_int (Truncate.floor x)
 129   function ceiling (x : real) : real = FromInt.from_int (Truncate.ceil x)
 130   function truncate (x : real) : real = FromInt.from_int (Truncate.truncate x)
 131
 132   (* TODO : axiomatize *)
 133   function round (x : real) : real
 134
 135   function to_int (x : real) : int = Truncate.floor x
 136
 137   predicate is_int (r : real) = r = FromInt.from_int (Truncate.truncate r)
 138   predicate is_rat (r : real) =
 139     exists n d : int. d <> 0 /\ r * FromInt.from_int d = FromInt.from_int n
 140 end
 141
 142 module RealDivE
 143   (* TODO: euclidean division *)
 144   function div (x y : real) : real
 145   function mod (x y : real) : real
 146 end
 147
 148 module RealDivT
 149   (* TODO: divide and truncate *)
 150   function div_t (x y : real) : real
 151   function mod_t (x y : real) : real
 152 end
 153
 154 module RealDivF
 155   (* TODO: divide and floor *)
 156   function div_f (x y : real) : real
 157   function mod_f (x y : real) : real
 158 end
 159
 160 module IntToRat
 161   use Rat
 162
 163   function to_rat (x : int) : rat = frac x 1
 164 end
 165
 166 module IntToReal
 167   use real.FromInt as FromInt
 168
 169   function to_real (x : int) : real = FromInt.from_int x
 170 end
 171
 172 module RealToRat
 173   use Rat
 174
 175   (* TODO: axiomatize *)
 176   function to_rat (x : real) : rat
 177 end
 178
 179 module RatToReal
 180   use Rat
 181   use real.Real
 182   use real.FromInt as FromInt
 183
 184   function to_real (x : rat) : real =
 185     FromInt.from_int (numerator x) / FromInt.from_int (denominator x)
 186 end