Revision 7ae3d64f7211fdb2ca0cfa738fddad52399571fb authored by François Dupressoir on 26 June 2015, 09:46:35 UTC, committed by Pierre-Yves Strub on 26 June 2015, 14:11:43 UTC
Some remain in newth/NewIntCore.ec and newth/NewRealCore.ec. smt full and smt all currently fail for different reasons.
1 parent 966282e
RealExtra.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012-2015 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B licence.
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require export Real.
pragma +implicits.
(* -------------------------------------------------------------------- *)
op lub (E : real -> bool) : real.
pred nonempty (E : real -> bool) =
exists x, E x.
pred ub (E : real -> bool) (z : real) =
forall y, E y => y <= z.
pred has_ub (E : real -> bool) = nonempty (ub E).
pred has_lub (E : real -> bool) = nonempty E /\ has_ub E.
axiom lub_upper_bound (E : real -> bool): has_lub E =>
forall x, E x => x <= lub E.
axiom lub_adherent (E : real -> bool): has_lub E =>
forall eps, 0%r < eps =>
exists e, E e /\ (lub E - eps) < e.
Computing file changes ...
