Homework 7

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