Commit ee1880af authored by Francois Bobot's avatar Francois Bobot

ajout de quelques theory

parent e6e6070f
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 -> Eq.eq(select(store(m,a1,b),a2),b)
axiom select_eq : forall m : ('a,'b) t. forall a1,a2 : 'a. forall b : 'b.
not 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
type t = | True | False
\ No newline at end of file
type 'a list = Nil
Cons ('a,'a list)
\ No newline at end of file
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))
end
theory Set_list
use open 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
\ No newline at end of file
......@@ -28,7 +28,7 @@
(list
'("(\\*\\([^*]\\|\\*[^)]\\)*\\*)" . font-lock-comment-face)
'("{\\([^}]*\\)}" . font-lock-type-face)
`(,(why-regexp-opt '("include" "inductive" "external" "logic" "parameter" "exception" "axiom" "predicate" "function" "goal" "type")) . font-lock-builtin-face)
`(,(why-regexp-opt '("use" "open" "include" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type")) . font-lock-builtin-face)
`(,(why-regexp-opt '("let" "rec" "in" "if" "then" "else" "begin" "end" "while" "do" "done" "label" "assert" "try" "with" "theory" "uses")) . font-lock-keyword-face)
; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
)
......
......@@ -61,96 +61,10 @@ theory Eq
end
theory Set
type elt
type t
logic in_ : elt , t -> prop
logic empty : t
axiom empty_def1 : forall x:elt. not in_(x, empty)
logic add : elt, t -> t
uses Eq
axiom add_def1 : forall x,y:elt. forall s:t.
in_(x, add(y, s)) <-> (Eq.eq(x, y) or in_(x, s))
end
theory Set_poly
type 'a t
logic in_ : 'a , 'a t -> prop
logic empty : 'a t
axiom empty_def1 : forall x:'a. not in_(x, empty)
logic add : 'a, 'a t -> 'a t
uses Eq
axiom add_def1 : forall x,y:'a. forall s:'a t.
in_(x, add(y, s)) <-> (Eq.eq(x, y) or in_(x, s))
end
theory Test
uses Eq, L : List
open L
axiom a : forall x : 'a. not Eq.eq(nil, cons(nil, nil))
end
theory Array
type ('a,'b) t
logic select : ('a,'b) t,'a -> 'b
logic store : ('a,'b) t,'a,'b -> ('a,'b) t
uses Eq
axiom select_eq : forall m : ('a,'b) t. forall a1,a2 : 'a. forall b : 'b.
Eq.eq(a1,a2) -> Eq.eq(select(store(m,a1,b),a2),b)
axiom select_eq : forall m : ('a,'b) t. forall a1,a2 : 'a. forall b : 'b.
not Eq.eq(a1,a2) -> Eq.eq(select(store(m,a1,b),a2),select(m,a2))
logic const : 'b -> ('a,'b) t
axiom const : forall b:'b. forall a:'a. Eq.eq(select(const(b),a),b)
end
theory Bool
type t = | True | False
end
theory Set_array
uses Array, Bool
(*type 'a t = ('a,Bool.t) Array.t*)
uses Eq
(*logic empty : ('a,Bool.t) Array.t
axiom empty : Eq.eq(empty,Array.const(Bool.False))*)
function empty() : ('a,Bool.t) Array.t = Array.const(Bool.False)
(*logic in_ : 'a, ('a,Bool.t) Array.t -> prop
axiom in_ : forall s:'a t. forall e:'a.
in_(e,s) <-> Eq.eq(select(x,y),Bool.True)
*)
predicate in_(s:'a t, e:'a) = Eq.eq(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. Eq.eq(add(x,s),store(s,x,Bool.True))*)
function add(x:'a,s: ('a,Bool.t) Array.t) : ('a,Bool.t) Array.t = store(s,x,Bool.True)
end
\ No newline at end of file
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