(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2015 - IMDEA Software Institute
 * Copyright (c) - 2012--2015 - Inria
 * 
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
require import Ring StdRing Int Real.
require (*--*) Number.

(* -------------------------------------------------------------------- *)
theory IntOrder.
clone include Number.RealDomain
  with type t <- int,

  pred Domain.unit (z : int) <- (z = 1 \/ z = -1),
  op   Domain.zeror  <- 0,
  op   Domain.oner   <- 1,
  op   Domain.( + )  <- Int.( + ),
  op   Domain.([-])  <- Int.([-]),
  op   Domain.( * )  <- Int.( * ),
  op   Domain.( / )  <- Int.( * ),
  op   Domain.invr   <- (fun (z : int) => z),
  op   Domain.intmul <- IntID.intmul,
  op   Domain.ofint  <- IntID.ofint,
  op   Domain.exp    <- IntID.exp,

  op   "`|_|" <- Int."`|_|",
  op   ( <= ) <- Int.(<=),
  op   ( <  ) <- Int.(< )

  proof Domain.* by smt, Axioms.* by smt

  remove abbrev Domain.(-).
end IntOrder.
  
(* -------------------------------------------------------------------- *)
clone Number.RealField as RealOrder
  with type t <- real,

  op   Field.zeror  <- 0%r,
  op   Field.oner   <- 1%r,
  op   Field.( + )  <- Real.( + ),
  op   Field.([-])  <- Real.([-]),
  op   Field.( * )  <- Real.( * ),
  op   Field.( / )  <- Real.( / ),
  op   Field.invr   <- Real.inv,
  op   Field.intmul <- RField.intmul,
  op   Field.ofint  <- RField.ofint,
  op   Field.exp    <- RField.exp,

  op   "`|_|" <- Real.Abs."`|_|",
  op   ( <= ) <- Real.(<=),
  op   ( <  ) <- Real.(< )

  proof Field.* by smt, Axioms.* by smt full

  remove abbrev Field.(-).