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