Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# FDS Week 6 homework

Week 6 homework

## Resources

### 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')
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"

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```

Terms and Conditions