test-jcf.why 635 Bytes
 Jean-Christophe Filliâtre committed May 30, 2011 1 `````` `````` Jean-Christophe committed Jun 16, 2011 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 `````` Jean-Christophe Filliâtre committed May 31, 2011 10 `````` `````` Jean-Christophe committed Jun 16, 2011 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 `````` Jean-Christophe Filliâtre committed May 31, 2011 15 16 ``````end `````` Jean-Christophe Filliâtre committed May 09, 2011 17 18 19 ``````theory Order type t logic (<=) t t `````` Jean-Christophe Filliâtre committed Feb 09, 2010 20 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 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 `````` Jean-Christophe Filliâtre committed Apr 18, 2011 25 `````` `````` Jean-Christophe Filliâtre committed Feb 26, 2010 26 27 ``````(* Local Variables: `````` Jean-Christophe Filliâtre committed Feb 18, 2011 28 ``````compile-command: "make -C .. tests/test-jcf.gui" `````` Jean-Christophe Filliâtre committed Feb 26, 2010 29 30 ``````End: *) `````` 31