(* $Id: ex.thy,v 1.4 2012/01/04 14:35:44 webertj Exp$ Author: Farhad Mehta *) header {* Recursive Functions and Induction: Zip *} (*<*) theory ex imports Main begin (*>*) text {* Read the chapter about total recursive functions in the Tutorial on Isabelle/HOL'' (@{text fun}, 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 fun}). \end{enumerate} *} consts zip1 :: "'a list \ 'a list \ 'a list" consts zip2 :: "'a list \ 'a list \ 'a list" consts zipr :: "'a list \ 'a list \ 'a list" text {* Show that all three versions of @{text Zip} are equivalent. *} text {* Show that @{text zipr} distributes over @{text append}. *} lemma "\length p = length u; length q = length v\ \ zipr (p@q) (u@v) = zipr p u @ zipr q v" (*<*) oops (*>*) text {* {\bf Note:} For @{text fun}, 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 (*>*)