Commit 82e362d1 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

theories vont maintenant dans theories/

parent e0d8224f
theory Assoc
type t
logic op(t, t) : t
axiom Assoc : forall x,y,z:t. op(op(x,y),z)=op(x,op(y,z))
end
theory Comm
type t
logic op(t, t) : t
axiom Comm : forall x,y:t. op(x,y) = op(y,x)
end
theory AC
type t
logic op(t, t) : t
clone Assoc with type t = t, logic op = op
clone Comm with type t = t, logic op = op
end
theory Group
type t
logic unit : t
logic op(t,t) : t
logic inv(t) : t
axiom Unit_def : forall x:t. op(x, unit) = x
clone Assoc with type t = t, logic op = op
axiom Inv_def : forall x:t. op(x,inv(x)) = unit
end
theory CommutativeGroup
clone export Group
clone Comm with type t = t, logic op = op
end
theory Ring
type t
logic zero : t
logic (+) (t, t) : t
logic (-_) (t) : t
logic (*) (t, t) : t
clone CommutativeGroup with type t = t,
logic unit = zero,
logic op = (+),
logic inv = (-_)
clone Assoc with type t = t, logic op = (*)
axiom Mul_distr: forall x,y,z:t. x * (y + z) = x * y + x * z
logic (-) (x:t, y:t) : t = x + -y
end
theory CommutativeRing
clone export Ring
clone Comm with type t = t, logic op = (*)
end
theory UnitaryCommutativeRing
clone export CommutativeRing
logic one : t
axiom Unitary : forall x:t. one * x = x
end
theory Field
clone export UnitaryCommutativeRing
logic inv(t) : t
axiom Inverse : forall x:t. x * inv(x) = one
logic (/) (x:t, y:t) : t = x * inv(y)
end
theory Array
type ('a,'b) t
logic select (('a,'b) t, 'a) : 'b
logic store (('a,'b) t, 'a, 'b) : ('a,'b) t
axiom Select_eq :
forall m : ('a,'b) t. forall a1,a2 : 'a. forall b : 'b.
a1 = a2 -> select(store(m,a1,b),a2) = b
axiom Select_neq :
forall m : ('a,'b) t. forall a1,a2 : 'a. forall b : 'b.
a1 <> a2 -> select(store(m,a1,b),a2) = select(m,a2)
logic const('b) : ('a,'b) t
axiom Const : forall b:'b. forall a:'a. select(const(b),a) = b
end
theory Base
type bool = True | False
logic andb(x:bool, y:bool) : bool =
match x, y with
| True, True -> True
| _ , _ -> False
end
logic orb(x:bool, y:bool) : bool =
match x, y with
| False, False -> False
| _ , _ -> True
end
logic xorb(x:bool, y:bool) : bool =
match x, y with
| True, False -> True
| False, True -> True
| _ , _ -> False
end
logic notb(x:bool) : bool =
match x with
| False -> True
| True -> False
end
end
theory Ite
use import Base
logic ite(b:bool, x:'a, y:'a) : 'a =
match b with
| True -> x
| False -> y
end
end
(* graph theory *)
theory Path
use import list.Mem
type vertex
logic edge(vertex, vertex)
inductive simple_path(vertex, vertex list, vertex) =
| Path_empty :
forall v:vertex. simple_path(v, Nil : vertex list, v)
| Path_cons :
forall src, v, dst : vertex, l : vertex list.
simple_path(v, l, dst) -> edge(src, v) -> not mem(v, l) ->
simple_path(src, Cons(v, l), dst)
logic simple_cycle(v : vertex) =
exists l : vertex list. l <> Nil and simple_path(v, l, v)
end
theory Int
logic (< ) (int, int)
logic (<=) (int, int)
logic (> ) (int, int)
logic (>=) (int, int)
(* TODO : < is a total order relation *)
logic zero : int = 0
logic one : int = 1
clone export algebra.UnitaryCommutativeRing with
type t = int, logic zero = zero, logic one = one
end
theory Abs
use import Int
logic abs(int) : int
axiom Pos: forall x:int. x >= 0 -> abs(x) = x
axiom Neg: forall x:int. x <= 0 -> abs(x) = -x
end
theory MinMax
use import Int
logic min(int,int) : int
logic max(int,int) : int
axiom Max_is_ge : forall x,y:int. max(x,y) >= x and max(x,y) >= y
axiom Max_is_some : forall x,y:int. max(x,y) = x or max(x,y) = y
axiom Min_is_le : forall x,y:int. min(x,y) <= x and min(x,y) <= y
axiom Min_is_some : forall x,y:int. min(x,y) = x or min(x,y) = y
end
theory EuclideanDivision
(* TODO *)
end
theory ComputerDivision
(* TODO *)
end
theory List
type 'a list = Nil | Cons('a, 'a list)
end
theory Length
use import int.Int
use import List
logic length(l : 'a list) : int =
match l with
| Nil -> 0
| Cons(_, r) -> 1 + length(r)
end
lemma Length_nonnegative : forall l:'a list. length(l) >= 0
end
theory Mem
use export List
logic mem(x: 'a, l : 'a list) = match l with
| Nil -> false
| Cons(y, r) -> x = y or mem(x, r)
end
end
theory Permut
(* TODO *)
end
theory Induction
use import List
logic p ('a list)
axiom Induction :
p(Nil : 'a list) ->
(forall x:'a. forall l:'a list. p(l) -> p(Cons(x,l))) ->
forall l:'a list. p(l)
end
theory Map
use import List
type a
type b
logic f (a) : b
logic map(l : a list) : b list =
match l with
| Nil -> Nil
| Cons(x, r) -> Cons(f(x), map(r))
end
end
theory Fold
(* TODO (a la Map) *)
end
theory Real
logic (< ) (real, real)
logic (<=)(real, real)
logic (> ) (real, real)
logic (>=)(real, real)
(* TODO : < is a total order relation *)
logic zero : real = 0.0
logic one : real = 1.0
clone export algebra.Field with
type t = real, logic zero = zero, logic one = one
end
theory Abs
use import Real
logic abs(real) : real
axiom Pos: forall x:real. x >= 0.0 -> abs(x) = x
axiom Neg: forall x:real. x <= 0.0 -> abs(x) = -x
end
theory MinMax
use import Real
logic min(real,real) : real
logic max(real,real) : real
axiom Max_is_ge : forall x,y:real. max(x,y) >= x and max(x,y) >= y
axiom Max_is_some : forall x,y:real. max(x,y) = x or max(x,y) = y
axiom Min_is_le : forall x,y:real. min(x,y) <= x and min(x,y) <= y
axiom Min_is_some : forall x,y:real. min(x,y) = x or min(x,y) = y
end
theory FromInt
use int.Int
use import Real
logic from_int(int) : real
axiom Zero: from_int(0) = 0.0
axiom One: from_int(1) = 1.0
axiom Add:
forall x,y:int. from_int(Int.(+)(x,y)) = from_int(x) + from_int(y)
axiom Sub:
forall x,y:int. from_int(Int.(-)(x,y)) = from_int(x) - from_int(y)
axiom Mul:
forall x,y:int. from_int(Int.(*)(x,y)) = from_int(x) * from_int(y)
axiom Neg:
forall x,y:int. from_int(Int.(-_)(x)) = - from_int(x)
end
theory Truncate
(* TODO: truncate, floor, ceil *)
end
theory Sqrt
end
theory ExpLog
(* exp, log *)
end
theory Power
end
theory Trigonometry
(* sin, cos, tan, atan *)
end
theory Hyperbolic
(* cosh, sinh, tanh *)
end
theory Polar
(* atan2, hypot *)
end
theory Base
type 'a t
logic mem('a, 'a t)
logic empty : 'a t
axiom Empty_def1 : forall x : 'a. not mem(x, empty)
logic add('a, 'a t) : 'a t
axiom Add_def1 :
forall x, y : 'a. forall s : 'a t.
mem(x, add(y, s)) <-> (x = y or mem(x, s))
logic add'(x:'a, s:'a t) : 'a t =
epsilon res:'a t. forall y:'a. mem(y, res) <-> (y = x or mem(y, s))
logic union('a t, 'a t) : 'a t
axiom Union_def1 :
forall s1, s2 : 'a t. forall x : 'a.
mem(x, union(s1, s2)) <-> (mem(x, s1) or mem(x, s2))
logic inter('a t, 'a t) : 'a t
axiom Inter_def1 :
forall s1, s2 : 'a t. forall x : 'a.
mem(x, inter(s1, s2)) <-> (mem(x, s1) and mem(x, s2))
logic diff('a t, 'a t) : 'a t
axiom Diff_def1 :
forall s1, s2 : 'a t. forall x : 'a.
mem(x, diff(s1, s2)) <-> (mem(x, s1) and not mem(x, s2))
logic equal(s1 : 'a t, s2 : 'a t) = forall x : 'a. mem(x, s1) <-> mem(x, s2)
logic subset(s1 : 'a t, s2 : 'a t) = forall x : 'a. mem(x, s1) -> mem(x, s2)
end
(* finite sets *)
theory Fset
use import int.Int
clone export Base
logic cardinal('a t) : int
axiom Cardinal_empty : cardinal(empty : 'a t) = 0
(* TODO other axioms for cardinal *)
end
theory Set
clone export Base
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