test.why 1007 Bytes
Newer Older
1 2 3

(* test file *)

4 5 6 7 8 9
theory A
  type t
  logic c:t
end

theory B
10
  use import A
11 12
  logic d : t
  logic p : t -> prop
13 14 15
end

theory C
16 17
  use B
  use T : B.A 
18
  logic e : T.t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
19
  axiom test : B.p(T.c)
20 21
end

22
theory Int
23 24 25
  type int
end

26
theory List
27

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28
  type 'a list
29

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
30
  logic nil  : 'a list
31

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
32
  logic cons : 'a, 'a list -> 'a list
33

34
  logic is_nil : 'a list -> prop
35

36
  use import Int 
37 38
  
  logic length : 'a list -> int
39

40
end
41

42
theory Eq 
43

44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
  logic eq : 'a, 'a -> prop 

  (* This part is just a definition of the equality *)

  (* This theory define eq but of course these axioms should not be send
   to provers *)
 
  axiom refl : forall x:'a. eq(x,x) 
  axiom sym  : forall x,y:'a. eq(x,y) -> eq(y,x)
  axiom trans : forall x,y,z:'a. eq(x,y) -> eq(y,z) -> eq(x,z)
  (* This one can't be written in first order logic. *)
  type t
  type u
  logic f : t -> u
  axiom congru : forall x,y:t. eq(x,y) -> eq(f(x),f(y))
59

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
60
end
61

62
theory Test
63

64 65
  use Eq
  use import L : List
66
  axiom a : forall x : 'a. not Eq.eq(nil, cons(nil, nil))
67

68
end