test-jcf.why 1.19 KB
 Jean-Christophe Filliâtre committed May 30, 2011 1 `````` `````` Jean-Christophe Filliâtre committed May 31, 2011 2 3 4 5 6 7 8 9 10 11 12 ``````theory Test use import bool.Bool type t 'a = {| a: 'a; b: bool; c: 'a |} goal G: forall x: t bool. {| x with a = 0 |}.a = 0 end `````` Jean-Christophe Filliâtre committed May 09, 2011 13 14 15 ``````theory Order type t logic (<=) t t `````` Jean-Christophe Filliâtre committed Feb 09, 2010 16 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 17 18 19 20 `````` 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 21 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 22 23 ``````theory List type list 'a = Nil | Cons 'a (list 'a) `````` Jean-Christophe Filliâtre committed Apr 18, 2011 24 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 25 26 27 `````` 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 28 29 30 `````` end end `````` Jean-Christophe Filliâtre committed May 09, 2011 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 ``````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 47 ``````end `````` Jean-Christophe Filliâtre committed Oct 07, 2010 48 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 49 ``````theory SortedIntList `````` Jean-Christophe Filliâtre committed Dec 13, 2010 50 `````` use import int.Int `````` Jean-Christophe Filliâtre committed May 09, 2011 51 52 `````` use import List clone import SortedList with type O.t = int, logic O.(<=) = (<=) `````` Jean-Christophe Filliâtre committed Oct 26, 2010 53 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 54 `````` goal sorted123: sorted (Cons 1 (Cons 2 (Cons 3 Nil))) `````` Jean-Christophe Filliâtre committed Dec 13, 2010 55 ``````end `````` Francois Bobot committed Mar 22, 2010 56 `````` `````` Jean-Christophe Filliâtre committed Feb 26, 2010 57 58 ``````(* Local Variables: `````` Jean-Christophe Filliâtre committed Feb 18, 2011 59 ``````compile-command: "make -C .. tests/test-jcf.gui" `````` Jean-Christophe Filliâtre committed Feb 26, 2010 60 61 ``````End: *) `````` 62