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 Main "~~/src/HOL/Library/Multiset" begin end
theory Submission
imports Defs
begin
fun c_qsort :: "'a::linorder list \<Rightarrow> nat" where
"c_qsort [] = 0"
| "c_qsort (p#xs)
= c_qsort (filter (\<lambda>x. x < p) xs) + c_qsort (filter (\<lambda>x. x \<ge> p) xs) + 2*length xs"
lemma qsort_quad: "c_qsort xs \<le> (length xs)\<^sup>2"
proof (induction xs rule: length_induct)
case (1 xs)
show ?case proof (cases xs)
case Nil
then show ?thesis by auto
next
case [simp]: (Cons x xs')
text \<open>Insert your proof here\<close>
show ?thesis
sorry
qed
qed
fun sorted_key :: "('a \<Rightarrow> 'b::linorder) \<Rightarrow> 'a list \<Rightarrow> bool" where
"sorted_key k [] = True"
| "sorted_key k (x # xs) = ((\<forall>y\<in>set xs. k x \<le> k y) & sorted_key k xs)"
fun quicksort :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"quicksort _ _ = undefined"
lemma quicksort_preserves_mset: "mset (quicksort k xs) = mset xs"
sorry
lemma quicksort_sorts: "sorted_key k (quicksort k xs)"
sorry
lemma quicksort_stable:
"[x\<leftarrow>quicksort k xs. k x = (a::nat)] = [x\<leftarrow>xs. k x = a]"
sorry
end
theory Check imports Submission begin lemma qsort_quad: "c_qsort xs \<le> (length xs)\<^sup>2" by(rule qsort_quad) lemma quicksort_preserves_mset: "mset (quicksort k xs) = mset xs" by(rule quicksort_preserves_mset) lemma quicksort_sorts: "sorted_key k (quicksort k xs)" by(rule quicksort_sorts) lemma quicksort_stable: "[x\<leftarrow>quicksort k xs. k x = (a::nat)] = [x\<leftarrow>xs. k x = a]" by(rule quicksort_stable) end