test-jcf.why 1.05 KB
Newer Older
1 2 3
theory Order
  type t
  logic (<=) t t
4

5 6 7 8
  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
9

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

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

19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
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
35
end
36

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

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

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