FDS Week 6 Homework

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

end