swh:1:snp:a009335c9ad61a15b4ffe398f445dd601942b68c
Tip revision: 6590f1e16484df765fdb915ed05e006511f40800 authored by MegiDervishi on 05 August 2019, 10:06:50 UTC
wdep
wdep
Tip revision: 6590f1e
Real.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import Int Ring AlgTactic.
op zero : real.
op one : real.
op ( + ) : real -> real -> real.
op [ - ] : real -> real.
op ( * ) : real -> real -> real.
op inv : real -> real.
op ( < ) : real -> real -> bool.
op ( <= ) = fun x y => x < y \/ x = y.
abbrev ( - ) (x y : real) = x + -y.
abbrev ( / ) (x y : real) = x * (inv y).
abbrev [-printing] ( > ) (x y : real) = y < x.
abbrev [-printing] ( >= ) (x y : real) = y <= x.
(* -------------------------------------------------------------------- *)
op from_int: int -> real.
(* -------------------------------------------------------------------- *)
abbrev b2r (b:bool) = if b then from_int 1 else from_int 0.
(* -------------------------------------------------------------------- *)
op "`|_|" x = if from_int 0 <= x then x else -x.
op ( ^ ) : real -> int -> real.
axiom powrN (x : real) (n : int) :
x^(-n) = inv (x^n).
axiom powr0 (x : real) :
x^0 = one.
axiom powrS (x : real) (n : int) :
0 <= n => x^(n+1) = x^n * x.