From d15da6d4e4a5051a15b39c312c26500bed177029 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Sun, 4 Sep 2011 16:43:48 +0200 Subject: [PATCH] more lemmas on absolute value and subtraction --- theories/algebra.why | 3 +++ theories/int.why | 4 ++++ theories/real.why | 4 ++++ 3 files changed, 11 insertions(+) diff --git a/theories/algebra.why b/theories/algebra.why index d1d1bf979..b7171bd43 100644 --- a/theories/algebra.why +++ b/theories/algebra.why @@ -32,6 +32,9 @@ theory Group clone Assoc with type t = t, function op = op axiom Inv_def : forall x:t. op x (inv x) = unit + + lemma Inv_unit : forall x y:t. op x (inv y) = unit -> x = y + end theory CommutativeGroup diff --git a/theories/int.why b/theories/int.why index 0257c4a62..78cb5dfb5 100644 --- a/theories/int.why +++ b/theories/int.why @@ -19,8 +19,12 @@ theory Abs function abs (x:int) : int = if x >= 0 then x else -x + lemma Abs_le: forall x y:int. abs x <= y <-> -y <= x <= y + lemma Abs_pos: forall x:int. abs x >= 0 + lemma Abs_zero: forall x:int. abs x = 0 -> x = 0 + end theory MinMax diff --git a/theories/real.why b/theories/real.why index a4dfbee28..e8473c31b 100644 --- a/theories/real.why +++ b/theories/real.why @@ -11,6 +11,8 @@ theory Real clone export algebra.OrderedField with type t = real, function zero = zero, function one = one, predicate (<=) = (<=) + lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y + end theory RealInfix @@ -40,6 +42,8 @@ theory Abs lemma Abs_pos: forall x:real. abs x >= 0.0 + lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0 + end theory MinMax -- 2.26.2