Mentions légales du service

Skip to content
Snippets Groups Projects
Commit d15da6d4 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

more lemmas on absolute value and subtraction

parent c74f2024
No related branches found
No related tags found
No related merge requests found
...@@ -32,6 +32,9 @@ theory Group ...@@ -32,6 +32,9 @@ theory Group
clone Assoc with type t = t, function op = op clone Assoc with type t = t, function op = op
axiom Inv_def : forall x:t. op x (inv x) = unit 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 end
theory CommutativeGroup theory CommutativeGroup
......
...@@ -19,8 +19,12 @@ theory Abs ...@@ -19,8 +19,12 @@ theory Abs
function abs (x:int) : int = if x >= 0 then x else -x 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_pos: forall x:int. abs x >= 0
lemma Abs_zero: forall x:int. abs x = 0 -> x = 0
end end
theory MinMax theory MinMax
......
...@@ -11,6 +11,8 @@ theory Real ...@@ -11,6 +11,8 @@ theory Real
clone export algebra.OrderedField with type t = real, clone export algebra.OrderedField with type t = real,
function zero = zero, function one = one, predicate (<=) = (<=) function zero = zero, function one = one, predicate (<=) = (<=)
lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y
end end
theory RealInfix theory RealInfix
...@@ -40,6 +42,8 @@ theory Abs ...@@ -40,6 +42,8 @@ theory Abs
lemma Abs_pos: forall x:real. abs x >= 0.0 lemma Abs_pos: forall x:real. abs x >= 0.0
lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0
end end
theory MinMax theory MinMax
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment