Commit 796da2b5 authored by MARCHE Claude's avatar MARCHE Claude

Document the stdlib with new why3doc

parent fe25b289
(** Basic Algebra Theories *)
(** {1 Basic Algebra Theories} *)
(** {2 Associativity} *)
theory Assoc
type t
......@@ -7,12 +9,16 @@ theory Assoc
axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z)
end
(** {2 Commutativity} *)
theory Comm
type t
function op t t : t
axiom Comm : forall x y : t. op x y = op y x
end
(** {2 Associativity and Commutativity} *)
theory AC
type t
function op t t : t
......@@ -21,6 +27,8 @@ theory AC
meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)
end
(** {2 Group theory} *)
theory Group
type t
......@@ -35,18 +43,23 @@ theory Group
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
(** {2 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
(** {2 Rings} *)
theory Ring
type t
constant zero : t
......@@ -66,12 +79,16 @@ theory Ring
function (-) (x y : t) : t = x + -y
end
(** {2 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
(** {2 Commutative Rings with Unit} *)
theory UnitaryCommutativeRing
clone export CommutativeRing
constant one : t
......@@ -79,6 +96,8 @@ theory UnitaryCommutativeRing
axiom NonTrivialRing : zero <> one
end
(** {2 Ordered Commutative Rings} *)
theory OrderedUnitaryCommutativeRing
clone export UnitaryCommutativeRing
predicate (<=) t t
......@@ -93,6 +112,8 @@ theory OrderedUnitaryCommutativeRing
forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
end
(** {2 Field theory} *)
theory Field
clone export UnitaryCommutativeRing
function inv t : t
......@@ -113,6 +134,8 @@ theory Field
end
(** {2 Ordered Fields} *)
theory OrderedField
clone export Field
......@@ -127,7 +150,8 @@ theory OrderedField
forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
end
(* to be discussed: should we add the following lemmas, and where
(***
to be discussed: should we add the following lemmas, and where
lemma InvMult : forall x y : t. (-x) * y = - (x * y) = x * (-y)
lemma InvSquare : forall x : t. x * x = (-x) * (-x)
......
(** {1 Booleans} *)
(** {2 Basic theory of Booleans} *)
theory Bool
use export Bool (* built-in theory of Booleans *)
......@@ -36,6 +40,8 @@ theory Bool
end
(** {2 Operator if-then-else} *)
theory Ite
use import Bool (* this is the previously declared local theory *)
......
(** {1 Comparison Operators, Order relations} *)
(** {2 Absolute value} *)
theory Abs
type t
......@@ -11,13 +15,15 @@ theory Abs
axiom Pos: forall x:t. ge x zero -> abs x = x
axiom Neg: forall x:t. not ge x zero -> abs x = neg x
(*
(***
function abs(x : t) : t
axiom Abs_def : if ge x zero then abs x = x else abs x = neg x
*)
end
(** {2 minimum and maximum} *)
theory MinMax
type t
......@@ -39,14 +45,14 @@ theory MinMax
lemma Max_sym: forall x y:t. ge x y -> max x y = max y x
lemma Min_sym: forall x y:t. ge x y -> min x y = min y x
(*
(***
function min (x y : t) : t
axiom Min_def : if ge x y then min x y = y else min x y = x
function max (x y : t) : t
axiom Max_def : if ge x y then max x y = x else max x y = y
*)
(*
(***
function min (x y : t) : t = if ge x y then y else x
function max (x y : t) : t = if ge x y then x else y
*)
......
......@@ -36,6 +36,15 @@ theory SpecialValues
end
(** {2 Generic theory of floats}
The theory is parametrized by the real constant [max] which denotes
the maximal representable number, and the integer constant
[max_representable_integer] which is the maximal integer [n] such that
every integer between [0] and [n] are representable.
*)
theory GenFloat
use import Rounding
......@@ -95,6 +104,11 @@ theory GenFloat
end
(** {2 single precision floats}
a.k.a 32-bits floats
*)
theory Single
type single
......@@ -111,6 +125,10 @@ end
(** {2 Double precision floats}
a.k.a 64-bits floats
*)
theory Double
type double
......@@ -126,6 +144,11 @@ theory Double
end
(** {2 Generic Full theory of floats}
this theory extends the generic theory above by adding the special values
*)
theory GenFloatFull
......@@ -194,7 +217,7 @@ theory GenFloatFull
end
(** {2 Full theory of single precision floats} *)
theory SingleFull
......@@ -211,6 +234,7 @@ theory SingleFull
end
(** {2 Full theory of double precision floats} *)
theory DoubleFull
......
(** {1 Polymorphic Lists} *)
(** {2 Basic theory of polymorphic lists} *)
theory List
type list 'a = Nil | Cons 'a (list 'a)
end
(** {2 Length of a list} *)
theory Length
use import int.Int
use import List
......@@ -21,6 +27,8 @@ theory Length
end
(** {2 Membership in a list} *)
theory Mem
use export List
......@@ -31,6 +39,8 @@ theory Mem
end
(** {2 Nth element of a list} *)
theory Nth
use export List
use export option.Option
......@@ -43,7 +53,9 @@ theory Nth
end
theory HdTl "head and tail"
(** {2 Head and tail} *)
theory HdTl
use export List
use export option.Option
......@@ -60,6 +72,8 @@ theory HdTl "head and tail"
end
(** {2 Relation between head, tail and nth} *)
theory NthHdTl
use import int.Int
......@@ -75,6 +89,7 @@ theory NthHdTl
end
(** {2 Appending two lists} *)
theory Append
use export List
......@@ -109,6 +124,8 @@ theory Append
end
(** {2 Rerversing a list} *)
theory Reverse
use export List
......@@ -133,6 +150,8 @@ theory Reverse
end
(** {2 Sorted lists for some order as parameter} *)
theory Sorted
use export List
......@@ -157,6 +176,8 @@ theory Sorted
end
(** {2 Sorted lists of integers} *)
theory SortedInt
use import int.Int
......@@ -164,6 +185,8 @@ theory SortedInt
end
(** {2 Number of occurrences in a list} *)
theory NumOcc
use import int.Int
......@@ -189,6 +212,8 @@ theory NumOcc
end
(** {2 Permutation of lists} *)
theory Permut
use import NumOcc
......@@ -241,6 +266,8 @@ theory Permut
end
(** {2 List with pairwise distinct elements} *)
theory Distinct
use import List
......@@ -262,6 +289,8 @@ theory Distinct
end
(** {2 Induction on lists} *)
theory Induction
use import List
......@@ -276,6 +305,8 @@ theory Induction
end
(** {2 Maps as lists of pairs} *)
theory Map
use import List
......@@ -290,6 +321,8 @@ theory Map
end
end
(** {2 Generic recursors on lists} *)
theory FoldLeft
use import List
......@@ -318,6 +351,8 @@ theory FoldRight
end
end
(** {2 Importation of all list theories in one} *)
theory ListRich
use export List
use export Length
......@@ -332,7 +367,7 @@ theory ListRich
use export Permut
end
(*
(***
Local Variables:
compile-command: "make -C .. theories/list"
End:
......
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