test-jcf.why 1.05 KB
 Jean-Christophe Filliâtre committed May 30, 2011 1 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 2 3 4 ``````theory Order type t logic (<=) t t `````` Jean-Christophe Filliâtre committed Feb 09, 2010 5 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 6 7 8 9 `````` 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 10 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 11 12 ``````theory List type list 'a = Nil | Cons 'a (list 'a) `````` Jean-Christophe Filliâtre committed Apr 18, 2011 13 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 14 15 16 `````` logic mem (x: 'a) (l: list 'a) = match l with | Nil -> false | Cons y r -> x = y \/ mem x r `````` Jean-Christophe Filliâtre committed Apr 18, 2011 17 18 19 `````` end end `````` Jean-Christophe Filliâtre committed May 09, 2011 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 ``````theory SortedList use import List clone import Order as O inductive sorted (l : list t) = | sorted_nil : sorted Nil | sorted_one : forall x:t. sorted (Cons x Nil) | sorted_two : forall x y : t, l : list t. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) lemma sorted_Cons: forall x: t, l: list t. sorted (Cons x l) -> forall y: t. mem y l -> x <= y `````` Jean-Christophe Filliâtre committed Apr 18, 2011 36 ``````end `````` Jean-Christophe Filliâtre committed Oct 07, 2010 37 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 38 ``````theory SortedIntList `````` Jean-Christophe Filliâtre committed Dec 13, 2010 39 `````` use import int.Int `````` Jean-Christophe Filliâtre committed May 09, 2011 40 41 `````` use import List clone import SortedList with type O.t = int, logic O.(<=) = (<=) `````` Jean-Christophe Filliâtre committed Oct 26, 2010 42 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 43 `````` goal sorted123: sorted (Cons 1 (Cons 2 (Cons 3 Nil))) `````` Jean-Christophe Filliâtre committed Dec 13, 2010 44 ``````end `````` Francois Bobot committed Mar 22, 2010 45 `````` `````` Jean-Christophe Filliâtre committed Feb 26, 2010 46 47 ``````(* Local Variables: `````` Jean-Christophe Filliâtre committed Feb 18, 2011 48 ``````compile-command: "make -C .. tests/test-jcf.gui" `````` Jean-Christophe Filliâtre committed Feb 26, 2010 49 50 ``````End: *) `````` 51