test-jcf.why 635 Bytes
Newer Older
1

Jean-Christophe's avatar
Jean-Christophe committed
2 3 4 5 6 7 8 9
theory Bijection
  use export int.Int
  logic n : int
  logic f int : int
  axiom dom_f : forall i: int. 0 <= i < n -> 0 <= f i < n
  logic g int : int
  axiom gf : forall i: int. 0 <= i < n -> g (f i) = i
end
10

Jean-Christophe's avatar
Jean-Christophe committed
11 12 13 14
theory Test1
  logic id (i: int) : int = i
  clone import Bijection with logic f = id, lemma dom_f
  goal G: n > 4 -> g (id 4) = 4
15 16
end

17 18 19
theory Order
  type t
  logic (<=) t t
20

21 22 23 24
  axiom le_refl : forall x : t. x <= x
  axiom le_asym : forall x y : t. x <= y -> y <= x -> x = y
  axiom le_trans: forall x y z : t. x <= y -> y <= z -> x <= z
end
25

Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
26 27
(*
Local Variables: 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28
compile-command: "make -C .. tests/test-jcf.gui"
Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
29 30
End: 
*)
31