FDS Week 6 homework

Definitions File

theory Defs
  imports Main "~~/src/HOL/Library/Multiset"
begin

end

Template File

theory Submission
  imports Defs
begin

fun c_qsort :: "'a::linorder list \<Rightarrow> nat" where
  "c_qsort [] = 0"
| "c_qsort (p#xs) 
    = c_qsort (filter (\<lambda>x. x < p) xs) + c_qsort (filter (\<lambda>x. x \<ge> p) xs) + 2*length xs"

lemma qsort_quad: "c_qsort xs \<le> (length xs)\<^sup>2"
proof (induction xs rule: length_induct)
  case (1 xs)
  show ?case proof (cases xs)
    case Nil
    then show ?thesis by auto
  next
    case [simp]: (Cons x xs')
    text \<open>Insert your proof here\<close>  
    show ?thesis 
      sorry
  qed
qed

fun sorted_key :: "('a \<Rightarrow> 'b::linorder) \<Rightarrow> 'a list \<Rightarrow> bool" where
  "sorted_key k [] = True"
| "sorted_key k (x # xs) = ((\<forall>y\<in>set xs. k x \<le> k y) & sorted_key k xs)"

fun quicksort :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "quicksort _ _ = undefined"

lemma quicksort_preserves_mset: "mset (quicksort k xs) = mset xs"
  sorry

lemma quicksort_sorts: "sorted_key k (quicksort k xs)"
  sorry

lemma quicksort_stable:
  "[x\<leftarrow>quicksort k xs. k x = (a::nat)] = [x\<leftarrow>xs. k x = a]"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma qsort_quad: "c_qsort xs \<le> (length xs)\<^sup>2"
  by(rule qsort_quad)

lemma quicksort_preserves_mset: "mset (quicksort k xs) = mset xs"
  by(rule quicksort_preserves_mset)

lemma quicksort_sorts: "sorted_key k (quicksort k xs)"
  by(rule quicksort_sorts)

lemma quicksort_stable:
  "[x\<leftarrow>quicksort k xs. k x = (a::nat)] = [x\<leftarrow>xs. k x = a]"
  by(rule quicksort_stable)

end