Cookies disclaimer

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.

Homework 7

This is the task corresponding to homework 7.

Resources

Download Files

Definitions File

theory Defs
  imports "HOL-Library.Multiset" "HOL-Data_Structures.Define_Time_Function"
begin

declare Let_def [simp]
declare [[names_short]]

fun split_min :: "'a::linorder list \<Rightarrow> 'a \<times> 'a list" where
  "split_min [x] = (x,[])"
| "split_min (x#xs) = (
    let (y,ys) = split_min xs in
      if (x<y) then (x,xs)
      else (y,x#ys)
    )"

lemma split_min_len: "split_min(x#xs) = (y,ys) \<Longrightarrow> length ys = length xs"
  apply (induction xs arbitrary: x y ys)
   apply (auto split: prod.splits if_splits)
  done

lemma split_min_snd_len_decr[termination_simp]: 
  assumes "(y,ys) = split_min (x#xs)"
  shows "length ys < Suc (length xs)"
  using assms[symmetric] by (simp add: split_min_len)

fun sel_sort where
  "sel_sort [] = []"
| "sel_sort xs = (let (y,ys) = split_min xs in y#sel_sort ys)"

lemma split_min_mset: 
  assumes "split_min (x#xs) = (y,ys)"
  shows "mset (x#xs) = add_mset y (mset ys)"  
  using assms  
  apply (induction xs arbitrary: y ys rule: split_min.induct)
    apply (auto split: prod.splits if_splits)
  done

time_fun split_min
time_fun sel_sort

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"

(* Might be helpful *)
fun index :: "('a::linorder) list \<Rightarrow> 'a \<Rightarrow> nat" where
  "index [] x = 0"
| "index (x#xs) y = (if x=y then 0 else Suc (index xs y))"

consts rev_pre :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"

consts place_max_correct :: "('a::linorder) list \<Rightarrow> 'a list"

consts psort :: "('a::linorder) list \<Rightarrow> 'a list"



end

Template File

theory Submission
  imports Defs
begin

lemma T_split_min_cmpx: "xs \<noteq> [] \<Longrightarrow> T_split_min xs = length xs"
  sorry

theorem T_sel_sort_cmpx: "T_sel_sort xs = undefined" \<comment> \<open>Replace with your closed form\<close>
  sorry

lemma C_qsort_bound: "C_qsort xs \<le> (length xs)\<^sup>2"
  sorry

fun rev_pre :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
  "rev_pre _ _ = []"

lemma mset_rev_pre[simp]: "mset (rev_pre n xs) = mset xs"
  sorry

definition place_max_correct :: "('a::linorder) list \<Rightarrow> 'a list"  where
  "place_max_correct _ = []"

lemma mset_place_max_correct[simp]: "mset (place_max_correct (x#xs)) = mset (x#xs)"
  sorry

lemma last_place_max_correct: "xs \<noteq> [] \<Longrightarrow> last (place_max_correct xs) = Max (set xs)"
  sorry

lemma length_place_max_correct[simp]: "length (place_max_correct (x#xs)) = length (x#xs)"
  sorry

fun psort :: "('a::linorder) list \<Rightarrow> 'a list"  where
  "psort _ = []"

lemma psort_mset[simp]: "mset (psort xs) = mset xs"
  sorry

lemma sorted_psort: "sorted (psort xs)"
  sorry


(* Bonus exercise starts here: *)

fun rev_pre_chain :: "nat list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "rev_pre_chain [] xs = xs"
| "rev_pre_chain (r#rs) xs = rev_pre_chain rs (rev_pre r xs)"

definition "psortable_in xs k \<equiv> \<exists>rs . length rs \<le> k \<and> (let ys = rev_pre_chain rs xs in mset ys = mset xs \<and> sorted ys)"

fun psort_revs :: "('a :: linorder) list \<Rightarrow> nat list"  where
  "psort_revs _ = []"

lemma length_psort_revs: "length (psort_revs xs) \<le> undefined" \<comment> \<open>Replace with your bound\<close>
  sorry

lemma mset_rev_pre_chain_psort_revs: "mset (rev_pre_chain (psort_revs xs) xs) = mset xs"
  sorry

lemma sorted_psort_revs: "sorted (rev_pre_chain (psort_revs xs) xs)"
  sorry

theorem psortable_in_linear: "psortable_in xs undefined" \<comment> \<open>Replace with your bound\<close>
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma T_split_min_cmpx: "xs \<noteq> [] \<Longrightarrow> T_split_min xs = length xs"
  by (rule Submission.T_split_min_cmpx)

lemma C_qsort_bound: "C_qsort xs \<le> (length xs)\<^sup>2"
  by (rule Submission.C_qsort_bound)

lemma mset_rev_pre: "mset (rev_pre n xs) = mset xs"
  by (rule Submission.mset_rev_pre)

lemma mset_place_max_correct: "mset (place_max_correct (x#xs)) = mset (x#xs)"
  by (rule Submission.mset_place_max_correct)

lemma last_place_max_correct: "xs \<noteq> [] \<Longrightarrow> last (place_max_correct xs) = Max (set xs)"
  by (rule Submission.last_place_max_correct)

lemma length_place_max_correct: "length (place_max_correct (x#xs)) = length (x#xs)"
  by (rule Submission.length_place_max_correct)

lemma psort_mset: "mset (psort xs) = mset xs"
  by (rule Submission.psort_mset)

lemma sorted_psort: "sorted (psort xs)"
  by (rule Submission.sorted_psort)

lemma mset_rev_pre_chain_psort_revs: "mset (rev_pre_chain (psort_revs xs) xs) = mset xs"
  by (rule Submission.mset_rev_pre_chain_psort_revs)

lemma sorted_psort_revs: "sorted (rev_pre_chain (psort_revs xs) xs)"
  by (rule Submission.sorted_psort_revs)

end

Terms and Conditions