Why3 Standard Library index



Basic Algebra Theories


Associativity

theory Assoc

  type t
  function op t t : t
  axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z)

end

Commutativity

theory Comm

  type t
  function op t t : t
  axiom Comm : forall x y : t. op x y = op y x

end

Associativity and Commutativity

theory AC

  clone export Assoc
  clone Comm with type t = t, function op = op
  meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)

end

Monoids

theory Monoid

  clone export Assoc
  constant unit : t
  axiom Unit_def_l : forall x:t. op unit x = x
  axiom Unit_def_r : forall x:t. op x unit = x

end

Commutative Monoids

theory CommutativeMonoid

  clone export Monoid
  clone Comm with type t = t, function op = op
  meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)

end

Groups

theory Group

  clone export Monoid
  function inv t : t
  axiom Inv_def_l : forall x:t. op (inv x) x = unit
  axiom Inv_def_r : forall x:t. op x (inv x) = unit

end

Commutative Groups

theory CommutativeGroup

  clone export Group
  clone Comm with type t = t, function op = op
  meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)

end

Rings

theory Ring

  type t
  constant zero : t
  function (+) t t : t
  function (-_) t : t
  function (*) t t : t

  clone CommutativeGroup with type t = t,
                              constant unit = zero,
                              function op = (+),
                              function inv = (-_)

  clone Assoc with type t = t, function op = (*)

  axiom Mul_distr_l : forall x y z : t. x * (y + z) = x * y + x * z
  axiom Mul_distr_r : forall x y z : t. (y + z) * x = y * x + z * x

  function (-) (x y : t) : t = x + -y

end

Commutative Rings

theory CommutativeRing

  clone export Ring
  clone Comm with type t = t, function op = (*)
  meta AC function (*) (*, prop Assoc.Assoc, prop Comm.Comm*)

end

Commutative Rings with Unit

theory UnitaryCommutativeRing

  clone export CommutativeRing
  constant one : t
  axiom Unitary : forall x:t. one * x = x
  axiom NonTrivialRing : zero <> one

end

Ordered Commutative Rings

theory OrderedUnitaryCommutativeRing

  clone export UnitaryCommutativeRing
  predicate (<=) t t
  predicate (>=) (x y : t) = y <= x
  clone export relations.TotalOrder with type t = t, predicate rel = (<=)

  axiom ZeroLessOne : zero <= one

  axiom CompatOrderAdd  :
    forall x y z : t. x <= y -> x + z <= y + z
  axiom CompatOrderMult :
    forall x y z : t. x <= y -> zero <= z -> x * z <= y * z

end

Field theory

theory Field

  clone export UnitaryCommutativeRing
  function inv t : t
  axiom Inverse : forall x:t. x <> zero -> x * inv x = one
  function (/) (x y : t) : t = x * inv y

  lemma add_div :
    forall x y z : t. z <> zero -> (x+y)/z = x/z + y/z

  lemma sub_div :
    forall x y z : t. z <> zero -> (x-y)/z = x/z - y/z

  lemma neg_div :
    forall x y : t. y <> zero -> (-x)/y = -(x/y)

  lemma assoc_mul_div: forall x y z:t.
    (* todo: discard the hypothesis ? *)
     z <> zero -> (x*y)/z = x*(y/z)

  lemma assoc_div_mul: forall x y z:t.
    (* todo: discard the hypothesis ? *)
     y <> zero /\ z <> zero -> (x/y)/z = x/(y*z)

  lemma assoc_div_div: forall x y z:t.
    (* todo: discard the hypothesis ? *)
     y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y

end

Ordered Fields

theory OrderedField

  clone export Field

  predicate (<=) t t
  predicate (>=) (x y : t) = y <= x
  clone export relations.TotalOrder with type t = t, predicate rel = (<=)

  axiom ZeroLessOne : zero <= one

  axiom CompatOrderAdd  : forall x y z : t. x <= y -> x + z <= y + z
  axiom CompatOrderMult :
    forall x y z : t. x <= y -> zero <= z -> x * z <= y * z

end


Generated by why3doc 0.87.3