(* polymorphic lists *)

type 'a list

logic nil : 'a list
logic cons : 'a, 'a list -> 'a list

(* hd and tl *)

logic hd : 'a list -> 'a
logic tl : 'a list -> 'a list

axiom hd_cons : forall x:'a. forall l:'a list. hd (cons(x,l)) = x
axiom tl_cons : forall x:'a. forall l:'a list. tl (cons(x,l)) = l


goal hd_tl_1 : forall x,y:int. hd(tl(cons(x, cons(y, nil)))) = y

  (* forall x,y:'a. hd(tl(cons(x, cons(y, nil)))) = y *)


(* length *)

logic length : 'a list -> int

axiom length_def_1 : length(nil) = 0

axiom length_def_2 : 
  forall x:'a. forall l:'a list. 
  length(cons(x,l)) = 1 + length(l)

goal length_1 : length(cons(1,cons(2,cons(3,nil)))) = 3

(* nth *)



logic nth : 'a list, int -> 'a

axiom nth_def_1 : 
  forall x:'a. forall l:'a list. nth(cons(x,l),0) = x

axiom nth_def_2 : 
  forall x:'a. forall l:'a list. forall n:int.
  n > 0 -> nth(cons(x,l),n) = nth(l,n-1)

goal nth_1 : nth(cons(1,cons(2,cons(3,nil))), 1) = 2


(* mem *)


logic mem : 'a, 'a list -> prop


axiom mem_def_1 : 
  forall x:'a. not mem(x,nil)


axiom mem_def_2 : 
  forall x:'a. forall y:'a. forall l:'a list.
  mem(x, cons(y,l)) <-> (x = y or mem(x,l))


goal mem_1 : mem(2, cons(1,cons(2,cons(3,nil))))


(* append *)

logic append : 'a list, 'a list -> 'a list

axiom append_def_1 : 
  forall l:'a list. append(nil,l) = l

axiom append_def_2 : 
  forall x:'a. forall l1,l2:'a list.
  append(cons(x,l1),l2) = cons(x,append(l1,l2))

goal append_1 : 
  append(cons(1,cons(2,nil)), cons(3,cons(4,nil))) = 
  cons(1, cons(2, cons(3, cons(4, nil))))

(* rev *)

logic rev : 'a list -> 'a list

axiom rev_def_1 : rev(nil) = nil

axiom rev_def_2 : 
  forall x:'a. forall l:'a list.
  rev(cons(x,l)) = append(rev(l), cons(x,nil))

goal rev_1 : rev(cons(1,cons(2,nil))) = cons(2,cons(1,nil))

(* flatten *)

logic flatten : 'a list list -> 'a list

axiom flatten_def_1 : 
  flatten(nil) = nil

axiom flatten_def_2 : 
  forall x:'a list. forall l:'a list list. 
  flatten(cons(x,l)) = append(x,flatten(l))

goal flatten_1 : flatten(cons(cons(1,nil), 
                              cons(cons(2,cons(3,nil)), 
	                           nil))) = cons(1,cons(2,cons(3,nil)))