(*
    $Id: sol.thy,v 1.2 2004/11/23 15:14:34 webertj Exp $
    Author: Farhad Mehta
*)

header {* Recursive Functions and Induction: Zip *}

(*<*) theory sol imports Main begin (*>*)

text {* 
Read the chapter about recursive definitions in the ``Tutorial on
Isabelle/HOL'' (@{text recdef}, Chapter 3.5).
*}

text {*
In this exercise you will define a function @{text Zip} that merges two lists
by interleaving.
 Examples:
@{text "Zip [a1, a2, a3]  [b1, b2, b3] = [a1, b1, a2, b2, a3, b3]"} 
 and
@{text "Zip [a1] [b1, b2, b3] = [a1, b1, b2, b3]"}.

Use three different approaches to define @{text Zip}:
\begin{enumerate}
\item by primitive recursion on the first list,
\item by primitive recursion on the second list,
\item by total recursion (using @{text recdef}).
\end{enumerate}
*}

consts zip1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
consts zip2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
consts zipr :: "('a list \<times> 'a list) \<Rightarrow> 'a list"

primrec
  "zip1 []     ys = ys"
  "zip1 (x#xs) ys = (case ys of [] \<Rightarrow> (x#xs) | z#zs \<Rightarrow> x#z#(zip1 xs zs))"

primrec
  "zip2 xs []     = xs"
  "zip2 xs (y#ys) = (case xs of [] => (y#ys) | z#zs => z # y # zip2 zs ys)"

recdef zipr "measure (\<lambda>(xs,ys). length xs + length ys)" 
  "zipr ([],ys)     = ys"
  "zipr (xs,[])     = xs"
  "zipr ((x#xs),ys) = x#zipr(ys,xs)"


text {*
Show that all three versions of @{text Zip} are equivalent.
*}

lemma "\<forall> ys. zip1 xs ys = zip2 xs ys"
  apply (induct xs)
    apply auto
    apply (case_tac ys)
    apply auto
  apply (case_tac ys)
  apply auto
done

lemma [simp]: "zipr (xs,[]) = xs"
  apply (case_tac xs)
  apply auto
done

lemma [simp]: "zipr ((x#xs),ys) = x#zipr(ys,xs)"
  apply (case_tac ys)
  apply auto
done

lemma "\<forall> xs. zip2 xs ys = zipr (xs,ys)"
  apply (induct ys)
    apply auto
  apply (case_tac xs)
    apply auto
done

lemma "\<forall> ys. zipr (xs,ys) = zip1 xs ys"
  apply (induct xs)
    apply auto
  apply (case_tac ys)
    apply auto
done


text {*
Show that @{text zipr} distributes over @{text append}.
*}

lemma zipr_append:
  "\<forall>u q v. length p = length u \<and>  length q = length v \<longrightarrow> 
  zipr(p@q,u@v) = zipr(p,u) @ zipr(q,v)"
  apply (induct p)
    apply auto
  apply (case_tac u)
    apply auto
done

lemma "\<lbrakk>length p = length u; length q = length v\<rbrakk> \<Longrightarrow> 
  zipr(p@q,u@v) = zipr(p,u) @ zipr(q,v)"
  by (simp add: zipr_append)


text {*
{\bf Note:} For @{text recdef}, the order of your equations is relevant.  If
equations overlap, they will be disambiguated before they are added to the
logic.  You can have a look at these equations using @{text "thm zipr.simps"}.
*}

(*<*) end (*>*)