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"