theory List

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

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

  lemma Length_nil : forall l:list 'a. length l = 0 <-> l = Nil

end

theory Mem
  use export List
 
  logic mem (x: 'a) (l : list 'a) = match l with
    | Nil      -> false
    | Cons y r -> x = y or mem x r
    end

end

theory Nth
  use export List
  use export option.Option
  use import int.Int
  
  logic nth (n : int) (l : list 'a) : option 'a = match l with
    | Nil -> None
    | Cons x r -> if n = 0 then Some x else nth (n - 1) r
  end

end

theory HdTl "head and tail"

  use export List
  use export option.Option

  logic hd (l : list 'a) : option 'a = match l with
    | Nil -> None
    | Cons h _ -> Some h
  end

  logic tl (l : list 'a) : option (list 'a) = match l with
    | Nil -> None
    | Cons _ t -> Some t
  end

  (* TODO: move these lemmas into another theory? *)
  use import Nth
  use import int.Int

  lemma Nth_tl :
    forall l1 l2 : list 'a. tl l1 = Some l2 -> 
    forall i : int. nth i l2 = nth (i+1) l1

  lemma Nth0_head:
    forall l : list 'a. nth 0 l = hd l

end


theory Append
  use export List

  logic append (l1 l2 : list 'a) : list 'a = match l1 with
    | Nil -> l2
    | Cons x1 r1 -> Cons x1 (append r1 l2)
  end

  lemma Append_assoc : 
    forall l1 l2 l3 : list 'a. 
    append l1 (append l2 l3) = append (append l1 l2) l3

  lemma Append_l_nil :
    forall l : list 'a. append l Nil = l

  use import Length
  use import int.Int

  lemma Append_length :
    forall l1 l2 : list 'a. length (append l1 l2) = length l1 + length l2

end

theory Reverse

  use export List
  use import Append

  logic reverse (l : list 'a) : list 'a = match l with
    | Nil -> Nil
    | Cons x r -> append (reverse r) (Cons x Nil)
  end

  use import Length
 
  lemma Reverse_length :
    forall l : list 'a. length (reverse l) = length l

end

theory Sorted

  use export 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))
 
  use import Mem

  lemma Sorted_mem :
    forall x : int, l : list int.
    (forall y : int. mem y l -> x <= y) and sorted l <-> sorted (Cons x l)

end

theory NumOcc
  
  use import int.Int
  use import List

  (* number of occurence of x in l *)
  logic num_occ (x : 'a) (l : list 'a) : int = 
    match l with
    | Nil -> 0
    | Cons y r -> (if x = y then 1 else 0) + num_occ x r
   end

  use import Mem

  lemma Mem_Num_Occ : 
    forall x:'a, l:list 'a. mem x l <-> num_occ x l > 0

end

theory Permut

  use import NumOcc
  use import List

  logic permut (l1 : list 'a) (l2 : list 'a) = 
    forall x : 'a. num_occ x l1 = num_occ x l2

  lemma Permut_refl : forall l : list 'a. permut l l

  lemma Permut_sym : forall l1 l2 : list 'a. permut l1 l2 -> permut l2 l1

  lemma Permut_trans : 
    forall l1 l2 l3 : list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3

  lemma Permut_cons : 
    forall x : 'a, l1 l2 : list 'a. 
    permut l1 l2 -> permut (Cons x l1) (Cons x l2)

  lemma Permut_swap : 
    forall x y : 'a, l : list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l))
  
  use import Mem

  lemma Permut_mem :
    forall x : 'a, l1 l2 : list 'a. permut l1 l2 -> mem x l1 -> mem x l2

  use import Length

  lemma Permut_length :
    forall l1 l2 : list 'a. permut l1 l2 -> length l1 = length l2

end

theory Induction
  use import List

  type elt

  logic p (list elt)

  axiom Induction : 
    p (Nil : list elt) ->
    (forall x:elt. forall l:list elt. p l -> p (Cons x l)) ->
    forall l:list elt. p l

end

theory Map
  use import List
 
  type a
  type b 
  logic f a : b

  logic map(l : list a) : list b = 
    match l with
    | Nil      -> Nil
    | Cons x r -> Cons (f x) (map r)
    end

end

theory Fold
  (* TODO (a la Map) *)
end