Commit aff6a806 authored by Clément Fumex's avatar Clément Fumex

add Monotonic axiom to FromInt theory

parent 7908605b
......@@ -53,3 +53,8 @@ Lemma Neg : forall (x:Z),
exact opp_IZR.
Qed.
(* Why3 goal *)
Lemma Monotonic : forall (x:Z) (y:Z), (x <= y)%Z ->
((Reals.Raxioms.IZR x) <= (Reals.Raxioms.IZR y))%R.
exact (IZR_le).
Qed.
......@@ -142,6 +142,8 @@ why3_vc Sub by auto
why3_vc Zero by auto
why3_vc Monotonic using assms by auto
why3_end
section {* Various truncation functions *}
......
......@@ -110,6 +110,9 @@ theory FromInt
axiom Neg:
forall x:int. from_int (Int.(-_) (x)) = - from_int x
axiom Monotonic:
forall x y:int. Int.(<=) x y -> from_int x <= from_int y
end
(** {2 Various truncation functions} *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment