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

  predicate mem (x: 'a) (l: list 'a) = match l with
    | Nil -> false
    | Cons y r -> x = y \/ mem x r
  end

  goal G1: mem 2 (Cons 1 (Cons 2 (Cons 3 Nil)))

end

theory Length

  use import List
  use import int.Int

  function length (l: list 'a) : int = match l with
    | Nil -> 0
    | Cons _ r -> length r + 1
  end

  goal G2: length (Cons 1 (Cons 2 (Cons 3 Nil))) = 3

  lemma length_nonnegative: forall l:list 'a. length(l) >= 0

  goal G3: forall x: int, l: list int. length (Cons x l) > 0

end

theory Order
  type t
  predicate (<=) 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 SortedList

  use import List
  clone export Order

  inductive sorted (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
  use import List

  clone import SortedList with type t = int, predicate (<=) = (<=),
    lemma le_refl, lemma le_asym, lemma le_trans

  goal sorted123: sorted (Cons 1 (Cons 2 (Cons 3 Nil)))

end

(*
Local Variables:
compile-command: "why3 ide demo_logic.why"
End:
*)