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

theories vont maintenant dans theories/

parent ade3c20a
theory AC
type t
logic op(t,t) : t
axiom Comm : forall x,y:t. op(x,y) = op(y,x)
axiom Assoc : forall x,y,z:t. op(op(x,y),z)=op(x,op(y,z))
end
theory GroupStructure
type t
logic neutral : t
logic op(t,t) : t
logic inv(t) : t
axiom Neutral_def : forall x:t. op(x,neutral) = x
clone AC with type t = t,
logic op = op
axiom Inv_def : forall x:t. op(x,inv(x)) = neutral
end
theory RingStructure
type t
logic zero : t
logic (_+_)(t, t) : t
logic (-_)(t) : t
logic (_*_)(t, t) : t
clone GroupStructure with type t = t,
logic neutral = zero,
logic op = (_+_),
logic inv = (-_)
clone AC with type t = t,
logic op = (_*_)
axiom Mul_distr: forall x,y,z:t. x * (y + z) = x * y + x * z
end
theory IntArray
use import prelude.Int
use import prelude.Array
end
(*
Local Variables:
compile-command: "make -C ../.. test"
End:
*)
theory Prelude
type deco
type undeco
type ty
logic sort(ty,undeco) : deco
end
theory Builtin
use import Prelude
type t
logic tty : ty
logic d2t(deco) : t
logic t2u(t) : undeco
axiom Conv : forall x:t[t2u(x)]. d2t(sort(tty,t2u(x)))=x
end
(* graph theory *)
theory Path
use import prelude.List
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. forall 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
(* additional theories over lists *)
theory IntList
use import prelude.Int
use import prelude.List
logic sorted(int list)
axiom Sorted_nil :
sorted(Nil)
axiom Sorted_one :
forall x: int. sorted(Cons(x, Nil))
axiom Sorted_cons:
forall x,y: int. forall l: int list.
sorted(Cons(y, l)) -> x <= y -> sorted(Cons(x, Cons(y, l)))
end
(*
Local Variables:
compile-command: "make -C ../.. test"
End:
*)
theory RingStructure
type t
logic zero : t
logic (_+_)(t, t) : t
logic (-_)(t) : t
logic (_*_)(t, t) : t
axiom Add_assoc: forall x,y,z:t. x + (y + z) = (x + y) + z
axiom Add_comm: forall x,y:t. x + y = y + x
axiom Zero_neutral: forall x:t. x + zero = x
axiom Neg: forall x:t. x + -x = zero
axiom Mul_assoc: forall x,y,z:t. x * (y * z) = (x * y) * z
axiom Mul_distr: forall x,y,z:t. x * (y + z) = x * y + x * z
end
(* The Why prelude *)
theory Int
logic (_< _) (int, int)
logic (_<=_)(int, int)
logic (_> _) (int, int)
logic (_>=_)(int, int)
logic (_+_) (int, int) : int
logic (_-_) (int, int) : int
logic (_*_) (int, int) : int
logic (_/_) (int, int) : int
logic (_%_) (int, int) : int
logic zero : int = 0
logic (-_)(int) : int
(* ring structure *)
clone export math.RingStructure with
type t = int, logic zero = zero,
logic (_+_) = (_+_), logic (_*_) = (_*_), logic (-_) = (-_)
(* int is a unitary, commutative ring *)
axiom Mul_comm: forall x,y:int. x * y = y * x
axiom One_neutral: forall x:int. 1 * x = x
end
theory Real
logic (_< _) (real, real)
logic (_<=_)(real, real)
logic (_> _) (real, real)
logic (_>=_)(real, real)
logic (_+_) (real, real) : real
logic (_-_) (real, real) : real
logic (_*_) (real, real) : real
logic (_/_) (real, real) : real
logic (-_)(real) : real
logic inv(real) : real
(* field structure *)
axiom Add_assoc: forall x,y,z:real. x + (y + z) = (x + y) + z
axiom Add_comm: forall x,y:real. x + y = y + x
axiom Mul_comm: forall x,y:real. x * y = y * x
axiom Zero_neutral: forall x:real. x + 0. = x
axiom Neg: forall x:real. x + -x = 0.
axiom Mul_assoc: forall x,y,z:real. x * (y * z) = (x * y) * z
axiom Mul_distr: forall x,y,z:real. x * (y + z) = x * y + x * z
axiom One_neutral: forall x:real. 1. * x = x
axiom Inv: forall x:real. x * inv(x) = 1.
end
theory Bool
type bool = True | False
end
theory List
type 'a list = Nil | Cons('a, 'a list)
logic is_nil(x : 'a list) = x = Nil
logic mem(x: 'a, l : 'a list) = match l with
| Nil -> false
| Cons(y, r) -> x = y or mem(x, r)
end
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 Set
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 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
theory Programs
logic old('a) : 'a
type label
logic at('a, label) : 'a
type 'a ref
logic (!_)('a ref) : 'a
logic ref('a) : 'a ref
end
(*
Local Variables:
compile-command: "make -C ../.. test"
End:
*)
(***
theory Set_list
use import List
logic add(x:'a,s:'a t) : 'a t = Cons(x,s)
logic mem(x:'a,s:'a t) = match s with
| Nil -> false
| Cons(x2,s2) -> x=x2 or mem(x,s2)
theory Set_list : Set with t = list
empty = Nil
add = add
mem = mem
use include Set_list
end
theory Set_array
uses Array, Bool
type 'a t = ('a,Bool.t) Array.t
(*logic empty : ('a,Bool.t) Array.t
axiom empty : Eq.eq(empty,Array.const(Bool.False))*)
logic empty : ('a,Bool.t) Array.t = Array.const(Bool.False)
(*logic mem : 'a, ('a,Bool.t) Array.t -> prop
axiom mem : forall s:'a t. forall e:'a.
mem(e,s) <-> Eq.eq(select(x,y),Bool.True)
*)
logic mem(s:'a t, e:'a) = select(x,y) = Bool.True
(*logic add : 'a, ('a,Bool.t) Array.t -> ('a,Bool.t) Array.t (* add(x,s) = store(x,s,bool.True) *)
axiom add : forall x:'a. forall s: ('a,Bool.t) Array.t. add(x,s) = store(s,x,Bool.True)*)
logic add(x:'a,s: ('a,Bool.t) Array.t) : ('a,Bool.t) Array.t = store(s,x,Bool.True)
theory Set_array : Set with t = t
empty = empty
add = add
mem = mem
use include Set_array
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