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

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

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

Terms and Conditions