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
begin

fun quickselect :: "'a::linorder list \<Rightarrow> nat \<Rightarrow> 'a" where
"quickselect (x#xs) k = (let
xs1 = [y\<leftarrow>xs. y<x];
xs2 = [y\<leftarrow>xs. \<not>(y<x)]
in
if k<length xs1 then quickselect xs1 k
else if k=length xs1 then x
else quickselect xs2 (k-length xs1-1)
)"
| "quickselect [] _ = undefined"

fun c_quickselect :: "'a::linorder list \<Rightarrow> nat \<Rightarrow> nat" where
"c_quickselect (x#xs) k = (let
xs1 = [y\<leftarrow>xs. y<x];
xs2 = [y\<leftarrow>xs. \<not>(y<x)]
in
length xs +
(if k<length xs1 then c_quickselect xs1 k + 1
else if k=length xs1 then 2
else c_quickselect xs2 (k-length xs1-1) + 3)
)"
| "c_quickselect [] _ = 0"

end
```

### Template File

```theory Template
imports Defs
begin
lemma quickselect_works: "k<length xs \<Longrightarrow> quickselect xs k = sort xs ! k"
sorry
lemma c_quickselect_quad: "c_quickselect xs k \<le> (length xs + 1)\<^sup>2"
sorry
end
```

### Check File

```theory Check
imports Submission
begin

lemma quickselect_works: "k<length xs \<Longrightarrow> quickselect xs k = sort xs ! k"
by(rule quickselect_works)

lemma c_quickselect_quad: "c_quickselect xs k \<le> (length xs + 1)\<^sup>2"