theory List type list 'a = Nil | Cons 'a (list 'a) use import bool.Bool logic x : int = if true then 1 else 3 end theory Length use import int.Int use import List logic length (l : list 'a) : int = match l with | Nil -> 0 | Cons _ r -> 1 + length r end lemma Length_nonnegative : forall l:list 'a. length(l) >= 0 end theory Sorted use import List use import int.Int inductive sorted (l : list int) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:int. sorted (Cons x Nil) | Sorted_Two : forall x y : int, l : list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) end theory Order type t logic (<=) t t 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 theory SortedGen 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)) end theory SortedIntList use import int.Int clone SortedGen with type O.t = int, logic O.(<=) = (<=) end (* Local Variables: compile-command: "cd ..; bin/why.opt -D drivers/simplify.drv tests/test-jcf.why && bin/why.opt -P simplify tests/test-jcf.why" End: *)