Commit c671ad6b authored by Andrei Paskevich's avatar Andrei Paskevich

remove excessive commas from quantifiers

parent 5c138ad7
theory Test
axiom A : forall x,x:int. x=x
axiom A : forall x x : int. x=x
end
......@@ -31,7 +31,7 @@ logic invariant(x:int, y:int, e:int) =
e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
2 * (y2 - x2) <= e <= 2 * y2
lemma Invariant_is_ok : forall x,y,e:int. invariant x y e -> best x y
lemma Invariant_is_ok : forall x y e:int. invariant x y e -> best x y
}
let bresenham () =
......
......@@ -31,7 +31,7 @@ axiom G_succ_sound :
logic weight(vertex, vertex) : int (* edge weight, if there is an edge *)
axiom Weight_nonneg : forall x,y:vertex. weight x y >= 0
axiom Weight_nonneg : forall x y:vertex. weight x y >= 0
}
parameter eq_vertex :
......@@ -104,27 +104,27 @@ inductive path(vertex,vertex,int) =
| Path_nil :
forall x:vertex. path x x 0
| Path_cons :
forall x,y,z:vertex. forall d:int.
forall x y z:vertex. forall d:int.
path x y d -> S.mem z (g_succ y) -> path x z (d+weight y z)
lemma Length_nonneg : forall x,y:vertex. forall d:int. path x y d -> d >= 0
lemma Length_nonneg : forall x y:vertex. forall d:int. path x y d -> d >= 0
logic shortest_path(x:vertex, y:vertex, d:int) =
path x y d and forall d':int. path x y d' -> d <= d'
lemma Path_inversion :
forall src,v:vertex. forall d:int. path src v d ->
forall src v:vertex. forall d:int. path src v d ->
(v = src and d = 0) or
(exists v':vertex. path src v' (d - weight v' v) and S.mem v (g_succ v'))
lemma Path_shortest_path :
forall src,v:vertex. forall d:int. path src v d ->
forall src v:vertex. forall d:int. path src v d ->
exists d':int. shortest_path src v d' and d' <= d
(* lemmas (those requiring induction) *)
lemma Main_lemma :
forall src,v:vertex. forall d:int.
forall src v:vertex. forall d:int.
path src v d -> not shortest_path src v d ->
exists v':vertex. exists d':int.
shortest_path src v' d' and S.mem v (g_succ v') and d' + weight v' v < d
......
......@@ -11,7 +11,7 @@
axiom OneClass :
forall u:uf. num u = 1 ->
forall x,y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
forall x y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
}
......@@ -36,7 +36,7 @@ parameter union :
unit writes u
{ same !u a b and
size !u = size (old !u) and num !u = num (old !u) - 1 and
forall x,y:int. 0 <= x < size !u -> 0 <= y < size !u ->
forall x y:int. 0 <= x < size !u -> 0 <= y < size !u ->
same !u x y <->
same (old !u) x y or
same (old !u) x a and same (old !u) b y or
......@@ -49,7 +49,7 @@ parameter rand : s:int -> {} int { 0 <= result < s }
{
axiom Ineq1 :
forall n,x,y:int. 0 <= n -> 0 <= x < n -> 0 <= y < n -> 0 <= x*n+y < n*n
forall n x y:int. 0 <= n -> 0 <= x < n -> 0 <= y < n -> 0 <= x*n+y < n*n
}
{
......@@ -59,9 +59,9 @@ parameter rand : s:int -> {} int { 0 <= result < s }
logic path(graph,int,int)
axiom Path_refl : forall g:graph, x:int. path g x x
axiom Path_sym : forall g:graph, x,y:int. path g x y -> path g y x
axiom Path_sym : forall g:graph, x y:int. path g x y -> path g y x
axiom Path_trans:
forall g:graph, x,y,z:int. path g x y -> path g y z -> path g x z
forall g:graph, x y z:int. path g x y -> path g y z -> path g x z
logic select(d:int, x:'a, y:'a) : 'a = if d = 0 then x else y
}
......@@ -75,7 +75,7 @@ parameter add_edge :
{ not path !graph a b }
unit writes num_edges, graph
{ !num_edges = old !num_edges + 1 and
(forall x,y:int.
(forall x y:int.
path !graph x y <->
path (old !graph) x y or
path (old !graph) x a and path (old !graph) b y or
......@@ -85,7 +85,7 @@ parameter add_edge :
let add_edge_and_union (u:uf ref) (a:int) (b:int) =
{ 0 <= a < size !u and 0 <= b < size !u and
not same !u a b and not path !graph a b and
forall x,y:int.
forall x y:int.
0 <= x < size !u -> 0 <= y < size !u ->
same !u x y <-> path !graph x y
}
......@@ -94,7 +94,7 @@ let add_edge_and_union (u:uf ref) (a:int) (b:int) =
{ !num_edges = old !num_edges + 1 and
same !u a b and
size !u = size (old !u) and num !u = num (old !u) - 1 and
(forall x,y:int.
(forall x y:int.
0 <= x < size !u -> 0 <= y < size !u ->
same !u x y <-> path !graph x y)
}
......@@ -102,13 +102,13 @@ let add_edge_and_union (u:uf ref) (a:int) (b:int) =
let build_maze (n:int) =
{ 1 <= n and
!num_edges = 0 and
forall x,y:int. x<>y -> not path !graph x y
forall x y:int. x<>y -> not path !graph x y
}
let u = create (n*n) in
while get_num_classes u > 1 do
invariant
{ 1 <= num !u and num !u + !num_edges = size !u = n*n and
forall x,y:int. 0 <= x < n*n -> 0 <= y < n*n ->
forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
same !u x y <-> path !graph x y
}
let x = rand n in
......@@ -126,7 +126,7 @@ let build_maze (n:int) =
end
done
{ !num_edges = n*n-1 and
forall x,y:int. 0 <= x < n*n -> 0 <= y < n*n ->
forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
path !graph x y }
(*
......
......@@ -66,7 +66,7 @@ back +-+-+-+-------------------+
logic permutation (n : int, a : int array) =
(forall i : int. 0 <= i < n -> 0 <= a#i < n) and
(forall i,j : int. 0 <= i < j < n -> a#i <> a#j)
(forall i j : int. 0 <= i < j < n -> a#i <> a#j)
logic dirichlet (n : int, a : int array, i : int) : int
......
......@@ -32,7 +32,7 @@
axiom OneClass :
forall u:uf. num u = 1 ->
forall x,y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
forall x y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
}
......@@ -104,7 +104,7 @@ let union (u:uf ref) (a:int) (b:int) =
{ inv !u and
same !u a b and
size !u = size (old !u) and num !u = num (old !u) - 1 and
forall x,y:int. 0 <= x < size !u -> 0 <= y < size !u ->
forall x y:int. 0 <= x < size !u -> 0 <= y < size !u ->
same !u x y <->
same (old !u) x y or
same (old !u) x a and same (old !u) b y or
......
......@@ -459,7 +459,7 @@ list1_uquant_sep_comma:
| uquant COMMA list1_uquant_sep_comma { $1::$3 }
uquant:
| list1_lident_sep_comma COLON primitive_type { $1,$3 }
| list1_lident COLON primitive_type { $1,$3 }
match_cases:
| match_case { [$1] }
......@@ -526,9 +526,9 @@ bar_:
| BAR { () }
;
list1_lident_sep_comma:
| lident { [$1] }
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
list1_lident:
| lident { [$1] }
| lident list1_lident { $1 :: $2 }
;
use:
......
......@@ -2,13 +2,13 @@
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)
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
axiom Comm : forall x y : t. op x y = op y x
end
theory AC
......@@ -52,7 +52,7 @@ theory Ring
clone Assoc with type t = t, logic op = (*)
axiom Mul_distr: forall x,y,z:t. x * (y + z) = x * y + x * z
axiom Mul_distr: forall x y z : t. x * (y + z) = x * y + x * z
logic (-) (x:t, y:t) : t = x + -y
end
......
......@@ -7,12 +7,12 @@ theory Array
logic store (('a,'b) t, 'a, 'b) : ('a,'b) t
axiom Select_eq :
forall m : ('a,'b) t. forall a1,a2 : 'a.
forall m : ('a,'b) t. forall a1 a2 : 'a.
forall b : 'b [select (store m a1 b) a2].
a1 = a2 -> select (store m a1 b) a2 = b
axiom Select_neq :
forall m : ('a,'b) t. forall a1,a2 : 'a.
forall m : ('a,'b) t. forall a1 a2 : 'a.
forall b : 'b [select (store m a1 b) a2].
a1 <> a2 -> select (store m a1 b) a2 = select m a2
......@@ -32,12 +32,12 @@ theory ArrayKey
logic store ('a t, key, 'a) : 'a t
axiom Select_eq :
forall m : 'a t. forall a1,a2 : key.
forall m : 'a t. forall a1 a2 : key.
forall b : 'a [select (store m a1 b) a2].
a1 = a2 -> select (store m a1 b) a2 = b
axiom Select_neq :
forall m : 'a t. forall a1,a2 : key.
forall m : 'a t. forall a1 a2 : key.
forall b : 'a [select (store m a1 b) a2].
a1 <> a2 -> select (store m a1 b) a2 = select m a2
......@@ -56,7 +56,7 @@ theory ArrayLength
logic const_length('a, int) : 'a t
axiom Const_contents :
forall b:'a. forall n,i:int. select (const_length b n) i = b
forall b:'a. forall n i:int. select (const_length b n) i = b
axiom Length_const :
forall a : 'a. forall n : int. length (const_length a n) = n
......@@ -91,35 +91,35 @@ theory BitVector
logic bw_and(v1:bv,v2:bv) : bv
axiom Nth_bw_and:
forall v1,v2:bv,n:int. 0 <= n < size ->
forall v1 v2:bv, n:int. 0 <= n < size ->
nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n)
(* logical shift right *)
logic lsr(bv,int) : bv
axiom Lsr_nth_low:
forall b:bv,n,s:int. 0 <= n+s < size -> nth (lsr b s) n = nth b (n+s)
forall b:bv,n s:int. 0 <= n+s < size -> nth (lsr b s) n = nth b (n+s)
axiom Lsr_nth_high:
forall b:bv,n,s:int. n+s >= size -> nth (lsr b s) n = False
forall b:bv,n s:int. n+s >= size -> nth (lsr b s) n = False
(* arithmetic shift left *)
logic asr(bv,int) : bv
axiom Asr_nth_low:
forall b:bv,n,s:int. 0 <= n+s < size -> nth (asr b s) n = nth b (n+s)
forall b:bv,n s:int. 0 <= n+s < size -> nth (asr b s) n = nth b (n+s)
axiom Asr_nth_high:
forall b:bv,n,s:int. n+s >= size -> nth (asr b s) n = nth b (size-1)
forall b:bv,n s:int. n+s >= size -> nth (asr b s) n = nth b (size-1)
(* logical shift left *)
logic lsl(bv,int) : bv
axiom Lsl_nth_high:
forall b:bv,n,s:int. 0 <= n-s < size -> nth (lsl b s) n = nth b (n-s)
forall b:bv,n s:int. 0 <= n-s < size -> nth (lsl b s) n = nth b (n-s)
axiom Lsl_nth_low:
forall b:bv,n,s:int. n-s < 0 -> nth (lsl b s) n = False
forall b:bv,n s:int. n-s < 0 -> nth (lsl b s) n = False
end
......
......@@ -26,16 +26,16 @@ theory MinMax
logic min(t,t) : t
logic max(t,t) : t
axiom Max_is_ge : forall x,y:t. ge (max x y) x and ge (max x y) y
axiom Max_is_some : forall x,y:t. max x y = x or max x y = y
axiom Min_is_le : forall x,y:t. ge x (min x y) and ge y (min x y)
axiom Min_is_some : forall x,y:t. min x y = x or min x y = y
axiom Max_is_ge : forall x y:t. ge (max x y) x and ge (max x y) y
axiom Max_is_some : forall x y:t. max x y = x or max x y = y
axiom Min_is_le : forall x y:t. ge x (min x y) and ge y (min x y)
axiom Min_is_some : forall x y:t. min x y = x or min x y = y
(*
axiom Max_x : forall x,y:t. ge x y -> max x y = x
axiom Max_y : forall x,y:t. ge y x -> max x y = y
axiom Min_y : forall x,y:t. ge x y -> min x y = y
axiom Min_x : forall x,y:t. ge y x -> min x y = x
axiom Max_x : forall x y:t. ge x y -> max x y = x
axiom Max_y : forall x y:t. ge y x -> max x y = y
axiom Min_y : forall x y:t. ge x y -> min x y = y
axiom Min_x : forall x y:t. ge y x -> min x y = x
*)
......
......@@ -52,7 +52,7 @@ theory GenFloat
forall m:mode, x:real. abs x <= max -> no_overflow m x
axiom Round_monotonic :
forall m:mode,x,y:real. x <= y -> round m x <= round m y
forall m:mode, x y:real. x <= y -> round m x <= round m y
logic max_representable_integer : int
......
......@@ -14,7 +14,7 @@ theory Path
| Path_empty :
forall g : graph, v : vertex. path g v v
| Path_append:
forall g : graph, v1,v2,src,dst : vertex.
forall g : graph, v1 v2 src dst : vertex.
path g src v1 -> edge g v1 v2 -> path g v2 dst ->
path g src dst
......@@ -25,7 +25,7 @@ end
| Path_empty :
forall g:graph, v:vertex. simple_path g v (Nil : vertex list) v
| Path_cons :
forall g:graph, src, v, dst : vertex, l : vertex list.
forall g:graph, src v dst : vertex, l : vertex list.
simple_path g v l dst -> edge g src v -> not mem v l ->
simple_path g src (Cons v l) dst
......
......@@ -36,10 +36,10 @@ theory MinMax
logic min(x:int,y:int) : int = if x <= y then x else y
logic max(x:int,y:int) : int = if x <= y then y else x
lemma Max_is_ge : forall x,y:int. max x y >= x and max x y >= y
lemma Max_is_some : forall x,y:int. max x y = x or max x y = y
lemma Min_is_le : forall x,y:int. min x y <= x and min x y <= y
lemma Min_is_some : forall x,y:int. min x y = x or min x y = y
lemma Max_is_ge : forall x y:int. max x y >= x and max x y >= y
lemma Max_is_some : forall x y:int. max x y = x or max x y = y
lemma Min_is_le : forall x y:int. min x y <= x and min x y <= y
lemma Min_is_some : forall x y:int. min x y = x or min x y = y
end
*)
......@@ -54,10 +54,10 @@ theory EuclideanDivision
logic mod(int,int) : int
axiom Div_mod:
forall x,y:int. y <> 0 -> x = y * div x y + mod x y
forall x y:int. y <> 0 -> x = y * div x y + mod x y
axiom Mod_bound:
forall x,y:int. y <> 0 -> 0 <= mod x y < abs y
forall x y:int. y <> 0 -> 0 <= mod x y < abs y
lemma Mod_1: forall x:int. mod x 1 = 0
......@@ -74,10 +74,10 @@ theory ComputerDivision
logic mod(int,int) : int
axiom Div_mod:
forall x,y:int. y <> 0 -> x = y * div x y + mod x y
forall x y:int. y <> 0 -> x = y * div x y + mod x y
axiom Mod_bound:
forall x,y:int. y <> 0 -> -abs y < mod x y < abs y
forall x y:int. y <> 0 -> -abs y < mod x y < abs y
lemma Mod_1: forall x:int. mod x 1 = 0
......
......@@ -10,12 +10,12 @@ theory Prelude
logic ge_bool('a, 'a) : bool
logic gt_bool('a, 'a) : bool
axiom Eq_bool_def : forall x,y:'a. eq_bool x y = True <-> x= y
axiom Ne_bool_def : forall x,y:'a. ne_bool x y = True <-> x<>y
axiom Le_bool_def : forall x,y:int. le_bool x y = True <-> x<=y
axiom Lt_bool_def : forall x,y:int. lt_bool x y = True <-> x< y
axiom Ge_bool_def : forall x,y:int. ge_bool x y = True <-> x>=y
axiom Gt_bool_def : forall x,y:int. gt_bool x y = True <-> x> y
axiom Eq_bool_def : forall x y:'a. eq_bool x y = True <-> x= y
axiom Ne_bool_def : forall x y:'a. ne_bool x y = True <-> x<>y
axiom Le_bool_def : forall x y:int. le_bool x y = True <-> x<=y
axiom Lt_bool_def : forall x y:int. lt_bool x y = True <-> x< y
axiom Ge_bool_def : forall x y:int. ge_bool x y = True <-> x>=y
axiom Gt_bool_def : forall x y:int. gt_bool x y = True <-> x> y
use export unit.Unit
logic ignore('a) : unit
......
......@@ -23,7 +23,7 @@ theory Abs
logic abs(x : real) : real = if x >= 0.0 then x else -x
lemma Abs_le: forall x,y:real. abs x <= y <-> -y <= x <= y
lemma Abs_le: forall x y:real. abs x <= y <-> -y <= x <= y
lemma Abs_pos: forall x:real. abs x >= 0.0
......@@ -36,10 +36,10 @@ theory MinMax
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
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
......@@ -54,13 +54,13 @@ theory FromInt
axiom One: from_int 1 = 1.0
axiom Add:
forall x,y:int. from_int (Int.(+) x y) = from_int x + from_int y
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
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
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
forall x y:int. from_int (Int.(-_) (x)) = - from_int x
end
......@@ -96,7 +96,7 @@ theory Truncate
forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0
axiom Truncate_monotonic:
forall x,y:real. x <= y -> Int.(<=) (truncate x) (truncate y)
forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y)
axiom Truncate_monotonic_int1:
forall x:real, i:int. x <= from_int i -> Int.(<=) (truncate x) i
......@@ -122,10 +122,10 @@ theory Truncate
forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x)
axiom Floor_monotonic:
forall x,y:real. x <= y -> Int.(<=) (floor x) (floor y)
forall x y:real. x <= y -> Int.(<=) (floor x) (floor y)
axiom Ceil_monotonic:
forall x,y:real. x <= y -> Int.(<=) (ceil x) (ceil y)
forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y)
end
......@@ -165,14 +165,14 @@ theory ExpLog
logic exp(real) : real
axiom Exp_zero : exp(0.0) = 1.0
axiom Exp_sum : forall x,y:real. exp (x+y) = exp x * exp y
axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
logic e : real = exp 1.0
logic log(real) : real
axiom Log_one : log 1.0 = 0.0
axiom Log_mul :
forall x,y:real. x > 0.0 and y > 0.0 -> log (x*y) = log x + log y
forall x y:real. x > 0.0 and y > 0.0 -> log (x*y) = log x + log y
axiom Log_exp: forall x:real. log (exp x) = x
......@@ -219,7 +219,7 @@ theory Power
forall x:real. x >= 0.0 -> pow x 0.5 = sqrt x
axiom Pow_exp_log:
forall x,y:real. x > 0.0 -> pow x y = exp (y * log x)
forall x y:real. x > 0.0 -> pow x y = exp (y * log x)
end
......@@ -279,9 +279,9 @@ theory Trigonometry
forall x:real. sin (-x) = - sin x
axiom Cos_sum:
forall x,y:real. cos (x+y) = cos x * cos y - sin x * sin y
forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y
axiom Sin_sum:
forall x,y:real. sin (x+y) = sin x * cos y + cos x * sin y
forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y
logic tan(x:real) : real = sin x / cos x
logic atan(real) : real
......@@ -339,9 +339,9 @@ theory Polar
logic atan2(real,real) : real
axiom X_from_polar:
forall x,y:real. x = hypot x y * cos (atan2 y x)
forall x y:real. x = hypot x y * cos (atan2 y x)
axiom Y_from_polar:
forall x,y:real. y = hypot x y * sin (atan2 y x)
forall x y:real. y = hypot x y * sin (atan2 y x)
end
......@@ -15,27 +15,27 @@ end
theory Transitive
clone export EndoRelation
axiom Trans : forall x,y,z:t. rel x y -> rel y z -> rel x z
axiom Trans : forall x y z:t. rel x y -> rel y z -> rel x z
end
theory Symmetric
clone export EndoRelation
axiom Symm : forall x,y:t. rel x y -> rel y x
axiom Symm : forall x y:t. rel x y -> rel y x
end
theory Asymmetric
clone export EndoRelation
axiom Asymm : forall x,y:t. rel x y -> not rel y x
axiom Asymm : forall x y:t. rel x y -> not rel y x
end
theory Antisymmetric
clone export EndoRelation
axiom Antisymm : forall x,y:t. rel x y -> rel y x -> x = y
axiom Antisymm : forall x y:t. rel x y -> rel y x -> x = y
end
theory Total
clone export EndoRelation
axiom Total : forall x,y:t. rel x y or rel y x
axiom Total : forall x y:t. rel x y or rel y x
end
theory PreOrder
......@@ -70,7 +70,7 @@ end
theory TotalStrictOrder
clone export PartialStrictOrder
axiom Trichotomy : forall x,y:t. rel x y or rel y x or x = y
axiom Trichotomy : forall x y:t. rel x y or rel y x or x = y
end
theory Inverse
......@@ -84,15 +84,15 @@ theory ReflClosure
inductive relR(t,t) =
| BaseRefl : forall x:t. relR x x
| StepRefl : forall x,y:t. rel x y -> relR x y
| StepRefl : forall x y:t. rel x y -> relR x y
end
theory TransClosure
clone export EndoRelation
inductive relT(t,t) =
| BaseTrans : forall x,y:t. rel x y -> relT x y
| StepTrans : forall x,y,z:t. relT x y -> rel y z -> relT x z
| BaseTrans : forall x y:t. rel x y -> relT x y
| StepTrans : forall x y z:t. relT x y -> rel y z -> relT x z
end
theory ReflTransClosure
......@@ -100,7 +100,7 @@ theory ReflTransClosure
inductive relTR(t,t) =
| BaseTransRefl : forall x:t. relTR x x
| StepTransRefl : forall x,y,z:t. relTR x y -> rel y z -> relTR x z
| StepTransRefl : forall x y z:t. relTR x y -> rel y z -> relTR x z
end
(*
......@@ -109,7 +109,7 @@ theory PreOrder
type t
logic le(t,t)
axiom Refl : forall x:t. le(x,x)
axiom Trans : forall x,y,z:t. le x y and le y z -> le x z
axiom Trans : forall x y z:t. le x y and le y z -> le x z
end
......@@ -121,7 +121,7 @@ theory Equiv
clone PreOrder with type t = t, logic le = eq
axiom Symm : forall x,y:t. eq x y -> eq y x
axiom Symm : forall x y:t. eq x y -> eq y x
end
......@@ -132,7 +132,7 @@ theory TotalPreOrder
clone export PreOrder with type t = t, logic le = le
axiom Totality: forall x,y:t. le x y or le y x
axiom Totality: forall x y:t. le x y or le y x
end
*)
......@@ -150,14 +150,14 @@ theory TotalOrder
clone PreOrder with type t = t, logic le = le
axiom Totality: forall x,y:t. eq x y or le x y or le y x
axiom Totality: forall x y:t. eq x y or le x y or le y x
logic lt(x:t,y:t) = le x y and not eq x y
lemma Lt_antirefl: forall x:t. not lt x x
lemma Lt_trans: forall x,y,z:t. lt x y and lt y z -> lt x z
lemma Le_lt_trans: forall x,y,z:t. le x y and lt y z -> lt x z
lemma Lt_le_trans: forall x,y,z:t. lt x y and le y z -> lt x z
lemma Lt_trans: forall x y z:t. lt x y and lt y z -> lt x z
lemma Le_lt_trans: forall x y z:t. le x y and lt y z -> lt x z
lemma Lt_le_trans: forall x y z:t. lt x y and le y z -> lt x z
end
*)
......
......@@ -14,31 +14,31 @@ theory Set
logic add('a, 'a t) : 'a t
axiom Add_def1 :
forall x, y : 'a. forall s : 'a t.
forall x y : 'a. forall s : 'a t.
mem x (add y s) <-> x = y or mem x s
logic remove('a, 'a t) : 'a t
axiom Remove_def1 :
forall x, y : 'a. forall s : 'a t.
forall x y : 'a. forall s : 'a t.
mem x (remove y s) <-> x <> y and mem x s
logic union('a t, 'a t) : 'a t
axiom Union_def1 :
forall s1, s2 : 'a t. forall x : 'a.
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.
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.
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
......@@ -67,7 +67,7 @@ theory Fset
mem x s -> cardinal s = 1 + cardinal (remove x s)
axiom Cardinal_subset :
forall s1, s2 : 'a t. subset s1 s2 -> cardinal s1 <= cardinal s2
forall s1 s2 : 'a t. subset s1 s2 -> cardinal s1 <= cardinal s2
end
Markdown is supported
0% or
<