Homework 6

Definitions File

theory Defs
  imports "HOL-Library.Multiset"
begin

text \<open>better setup of simp rules for insort\<close>

fun insort1 :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"insort1 x [] = [x]" |
"insort1 x (y#ys) =
  (if x \<le> y then x#y#ys else y#(insort1 x ys))"

fun insort :: "'a::linorder list \<Rightarrow> 'a list" where
"insort [] = []" |
"insort (x#xs) = insort1 x (insort xs)"

lemma mset_insort1[simp]: "mset (insort1 x xs) = {#x#} + mset xs"
  by(induction xs) auto

lemma mset_insort[simp]: "mset (insort xs) = mset xs"
  by(induction xs) auto

lemma set_insort1[simp]: "set (insort1 x xs) = {x} \<union> set xs"
  by(simp flip: set_mset_mset)

lemma set_insort[simp]: "set (insort xs) = set xs"
  by(simp flip: set_mset_mset)

lemma lenth_insort1[simp]: "length (insort1 x xs) = Suc (length xs)"
  by (induction xs) auto

lemma length_insort[simp]: "length (insort xs) = length xs"
  by (induction xs) auto


text \<open>Quickselect\<close>
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 Submission
  imports Defs
begin

hide_const List.insort

lemma partition_correct: "insort xs = insort [x\<leftarrow>xs. x<p] @ insort [x\<leftarrow>xs. \<not>(x<p)]"
  sorry

theorem quickselect_correct: "k<length xs \<Longrightarrow> quickselect xs k = insort xs ! k"
proof (induction xs k rule: quickselect.induct)
  case 2 then show ?case by simp
next
  case (1 x xs k)
  text \<open>Note: To make the induction hypothesis more readable,
    you can collapse the first two premises of the form \<open>?x=\<dots>\<close>
    by reflexivity:\<close>
  note IH = "1.IH"[OF refl refl]
  text \<open>Insert your proof here!\<close>
  sorry
qed

theorem quickselect_quadratic: "C_quickselect xs k \<le> (length xs + 1)\<^sup>2"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma partition_correct: "insort xs = insort [x\<leftarrow>xs. x<p] @ insort [x\<leftarrow>xs. \<not>(x<p)]"
  by (rule Submission.partition_correct)

theorem quickselect_correct: "k<length xs \<Longrightarrow> quickselect xs k = insort xs ! k"
  by (rule Submission.quickselect_correct)

theorem quickselect_quadratic: "C_quickselect xs k \<le> (length xs + 1)\<^sup>2"
  by (rule Submission.quickselect_quadratic)

end