Reading material

Pages 73-76.

Additional material

fun append([], ys) = ys
  | append(x :: xs, ys) = x :: append(xs, ys);

fun reverse([]) = []
  | reverse(x :: xs) = append(reverse(xs), [x]);

local
  fun helper([], ys) = ys
    | helper(x :: xs, ys) = helper(xs, x :: ys)
in
  fun rev(xs) = helper(xs, [])
end;
To run the above Standard ML program, first type 
  sml
On your screen you will now see something like 
  Standard ML of New Jersey, Version 110.0.6, October 31, 1999 [CM; autoload enabled]
  -
Next enter the above function definitions. This results in something like 
  val append = fn : 'a list * 'a list -> 'a list
  val reverse = fn : 'a list -> 'a list
  val rev = fn : 'a list -> 'a list
Now you can use the functions to actually reverse lists by typing 
  reverse([1, 4, 2, 3]);
which returns 
  val it = [3,2,4,1] : int list

Question

Prove that for all lists xs and ys, 
helper(xs, ys) = append(reverse(xs), ys)
by structural induction on xs. Try also to prove it using the induction tool.