Assignment 3. Due Thursday March 13.

1. Define reverse as

     rev [] = []
     rev (h::t) = rev t ++ [h]

  and prove rev(rev x) = x.

  val rev_def = 
   Define 
     `(rev [] = []) /\
      (rev (h::t) = rev t ++ [h])`;

2. Define reverse as

    reva [] a = a
    reva (h::t) a = reva t (h::a)

    rev1 x = reva x [] 

   and prove rev1(rev1 x) = x

3. Formalize the following algorithm

      minsort [] = [] 
      minsort l =
       let m = "the smallest element in l"
       in 
         m::minsort (delete m l)`;

   Show that minsort is a sorting function, using 
   the definitions in sortingTheory. In particular,
   show that 

     !l. PERM l (minsort l)

   and

     !l. SORTED $<= (minsort l)

4. The minsort in question 3 has type

     num list -> num list

   Change minsort to take an extra parameter of type

     'a -> 'a -> bool

   which allows it to sort arbitrary lists, using essentially
   the same algorithm as in question 3. Show that the altered
   minsort is a sorting function.

5. Extra credit. Show that the function described below terminates.
   (You may need to read the description for help on termination 
    proofs and how to conduct them in HOL.)

      f(x) = if x <= 1 then 0 else 
             if x MOD 2 = 1 then f(x+1)
             else 1 + f(x DIV 2)