I agree 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.

Download Files
### Definitions File

### Template File

### Check 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

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

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" by(rule c_quickselect_quad) end

Terms and Conditions