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

header {* Merge Sort *}

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

subsection {* Sorting with lists *}

text {*
  For simplicity we sort natural numbers.

  Define a predicate @{term sorted} that checks if each element in the list is
  less or equal to the following ones; @{term "le n xs"} should be true iff
  @{term n} is less or equal to all elements of @{text xs}.
*}

consts 
  le     :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
  sorted :: "nat list \<Rightarrow> bool"

primrec
  "le a []     = True"
  "le a (x#xs) = (a <= x & le a xs)"

primrec
  "sorted []     = True"
  "sorted (x#xs) = (le x xs & sorted xs)"


text {*
  Define a function @{term "count xs x"} that counts how often @{term x} occurs
  in @{term xs}.
*}

consts
  count :: "nat list => nat => nat"

primrec
  "count []     y = 0"
  "count (x#xs) y = (if x=y then Suc(count xs y) else count xs y)"


subsection {* Merge sort *}

text {*
  Implement \emph{merge sort}: a list is sorted by splitting it into two lists,
  sorting them separately, and merging the results.

  With the help of @{text recdef} define two functions
*}

consts merge :: "nat list \<times> nat list \<Rightarrow> nat list"
       msort :: "nat list \<Rightarrow> nat list"

recdef merge "measure (%(xs,ys). size xs + size ys)"
  "merge (x#xs, y#ys) = (if x <= y then x # merge(xs,y#ys) else y # merge(x#xs,ys))"
  "merge (xs,   [])   = xs"
  "merge ([],   ys)   = ys"

recdef msort "measure size"
  "msort []  = []"
  "msort [x] = [x]"
  "msort xs  = merge (msort(take (size xs div 2) xs), msort(drop (size xs div 2) xs))"


text {* and show *}

theorem "sorted (msort xs)"
(*<*)oops(*>*)

theorem "count (msort xs) x = count xs x"
(*<*)oops(*>*)

lemma [simp]: "x \<le> y \<Longrightarrow> le y xs \<longrightarrow> le x xs"
  apply (induct_tac xs)
  apply auto
done

lemma [simp]: "count (merge(xs,ys)) x = count xs x + count ys x"
  apply(induct xs ys rule: merge.induct)
  apply auto
done

lemma [simp]: "le x (merge (xs,ys)) = (le x xs \<and> le x ys)"
  apply (induct xs ys rule: merge.induct)
  apply auto
done

lemma [simp]: "sorted (merge(xs,ys)) = (sorted xs \<and> sorted ys)"
  apply(induct xs ys rule: merge.induct)
  apply (auto simp add: linorder_not_le order_less_le)
done

lemma [simp]: "1 < x \<Longrightarrow> min x (x div 2::nat) < x"
  by (simp add: min_def linorder_not_le)
  
lemma [simp]: "1 < x \<Longrightarrow> x - x div (2::nat) < x"
  by arith

theorem "sorted (msort xs)"
  apply (induct_tac xs rule: msort.induct) 
  apply auto
done

lemma count_append[simp]: "count (xs @ ys) x = count xs x + count ys x"
  apply (induct xs)
  apply auto
done

theorem "count (msort xs) x = count xs x"
  apply (induct xs rule: msort.induct)
      apply simp
    apply simp
  apply simp
  apply (simp del:count_append add:count_append[symmetric])
done


text {*
  You may have to prove lemmas about @{term sorted} and @{term count}.

  Hints:
  \begin{itemize}
  \item For @{text recdef} see Section~3.5 of the Isabelle/HOL tutorial.

  \item To split a list into two halves of almost equal length you can use the
  functions \mbox{@{text "n div 2"}}, @{term take} und @{term drop}, where
  @{term "take n xs"} returns the first @{text n} elements of @{text xs} and
  @{text "drop n xs"} the remainder.

  \item Here are some potentially useful lemmas:\\
    @{text "linorder_not_le:"} @{thm linorder_not_le [no_vars]}\\
    @{text "order_less_le:"} @{thm order_less_le [no_vars]}\\
    @{text "min_def:"} @{thm min_def [no_vars]}
  \end{itemize}
*}

(*<*) end (*>*)