test-jcf.why 1.05 KB
Newer Older
1

2 3 4
theory Order
  type t
  logic (<=) t t
5

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
10

11 12
theory List
  type list 'a = Nil | Cons 'a (list 'a)
13

14 15 16
  logic mem (x: 'a) (l: list 'a) = match l with
    | Nil -> false
    | Cons y r -> x = y \/ mem x r
17 18 19
  end
end

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
36
end
37

38
theory SortedIntList
39
  use import int.Int
40 41
  use import List
  clone import SortedList with type O.t = int, logic O.(<=) = (<=)
42

43
  goal sorted123: sorted (Cons 1 (Cons 2 (Cons 3 Nil)))
44
end
45

Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
46 47
(*
Local Variables: 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
48
compile-command: "make -C .. tests/test-jcf.gui"
Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
49 50
End: 
*)
51