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.

# Homework 6

This is the task corresponding to homework 6.

## Resources

### 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]
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"