(* test file *) theory Test_inline_trivial type t function c : t predicate eq (x y :'a) = x=y goal G : eq c c end theory Test_ind use graph.Path goal G : true end (* theory Test_encoding use int.Int function id(x: int) : int = x function id2(x: int) : int = id(x) function succ(x:int) : int = id(x+1) type myt function f (int) : myt clone transform.encoding_decorate.Kept with type t = myt goal G : (forall x:int.f(x)=f(x)) \/ (forall x:int. x=x+1) goal G2 : forall x:int. let x = 0 + 1 in x = let y = 0 + 1 + 0 in y end *) theory Test_simplify_array use int.Int use map.Map goal G1 : forall x y:int. forall m: map int int. get (set m y x) y = x goal G2 : forall x y:int. forall m: map int int. get (set m y x) y = y goal G3 : forall x y:int. forall m: map int int. get (const x) y = x end theory Test_simplify_array2 use int.Int use map.Map type t2 'a goal G1 : forall y:int. forall x:t2 int. forall m: map int (t2 int). get (set m y x) y = x end theory Test_guard type t function f t : t function a : t function b : t goal G : forall x:t. f a = x end theory Test_conjunction use int.Int axiom Trivial : 2 * 2 = 4 /\ 4 * 2 = 8 goal G : forall x:int. x*x=4 -> ((x*x*x=8 \/ x*x*x = -8) /\ x*x*2 = 8) goal G2 : forall x:int. (x+x=4 \/ x*x=4) -> ((x*x*x=8 \/ x*x*x = -8) /\ x*x*2 = 8) end theory Split_conj predicate p(x:int) (*goal G : forall x,y,z:int. ((p(x) -> p(y)) /\ ((not p(x)) -> p(z))) -> ((p(x) /\ p(y)) \/ ((not p(x)) /\ p(z)))*) (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) /\ p(y)) \/ ((not p(x)) /\ p(z)))*) (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*) goal G : forall x y z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z)) (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) /\ (not p(x)) \/ ((p(z)) /\ (p(x))))) *) (*goal G : forall x,y,z:int. (p(x) \/ p(y)) -> p(z)*) end theory TestEnco use int.Int meta "encoding : kept" type int type mytype 'a function id(x: int) : int = x function id2(x: int) : int = id(x) function succ(x:int) : int = id(x+1) goal G : (forall x:int. x=x) \/ (forall x:int. x=x+1) function p('a ) : mytype 'a function p2(mytype 'a) : 'a type toto function f (toto) : mytype toto axiom A0 : forall x : toto. f(x) = p(x) function g (mytype int) : toto function h (int) : toto axiom A05 : forall x : int. g(p(x)) = h(x) axiom A1 : forall x : mytype 'a. p(p2(x)) = x goal G2 : forall x:mytype toto. f(p2(x)) = x end theory TestIte use int.Int use list.Length use list.Mem function abs(x:int) : int = if x >= 0 then x else -x goal G : forall x:int. abs(x) >= 0 goal G2 : forall x:int. if x>=0 then x >= 0 else -x>=0 end theory TestBuiltin_real use real.Real goal G1 : 5.5 * 10. = 55. goal G2 : 9. / 3. = 3. goal G3 : inv(5.) = 0.2 end theory TestBuiltin_bool use bool.Bool goal G : xorb True False = True goal G_false : xorb True False = False end theory TestEncodingEnumerate type t = A | B | C goal G : forall x : t. (x = A \/ x = B) -> x<>C goal G1 : forall x : t. B <> A goal G2 : forall x : t. x = A \/ x = B \/ x=C goal G3 : forall x : t. x = A \/ x = B \/ x <> C end (* Local Variables: compile-command: "make -C .. test" End: *)