Homework 6

Definitions File

theory Defs
  imports "HOL-Library.Multiset"
begin

declare Let_def [simp]
declare [[names_short]]

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

lemma find_min_len: "find_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 find_min_snd_len_decr[termination_simp]: 
  assumes "(y,ys) = find_min (x#xs)"
  shows "length ys < Suc (length xs)"
  using assms[symmetric] by (simp add: find_min_len)

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

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

abbreviation "all_n_lists\<equiv>Enum.all_n_lists"
abbreviation "n_lists\<equiv>List.n_lists"
declare in_enum[simp]


consts T_find_min :: "'a::linorder list \<Rightarrow> nat"

consts T_sel_sort :: "'a::linorder list \<Rightarrow> nat"

type_synonym comparator = "(nat \<times> nat)"
type_synonym compnet = "comparator list"

consts compnet_step :: "comparator \<Rightarrow> 'a :: linorder list \<Rightarrow> 'a list"


end

Template File

theory Submission
  imports Defs
begin

fun T_find_min :: "'a::linorder list \<Rightarrow> nat"  where
  "T_find_min _ = undefined"

fun T_sel_sort :: "'a::linorder list \<Rightarrow> nat"  where
  "T_sel_sort _ = undefined"

lemma T_find_min_cmpx: "xs \<noteq> [] \<Longrightarrow> T_find_min xs = length xs - 1"
  sorry

theorem T_sel_sort_cmpx: "T_sel_sort xs = undefined"
  sorry


definition compnet_step :: "comparator \<Rightarrow> 'a :: linorder list \<Rightarrow> 'a list"  where
  "compnet_step _ = undefined"

value "compnet_step (1,100) [1,2::nat] = [1,2]"
value "compnet_step (1,2) [1,3,2::nat] = [1,2,3]"

definition run_compnet :: "compnet \<Rightarrow> 'a :: linorder list \<Rightarrow> 'a list" where
  "run_compnet = fold compnet_step"

theorem compnet_mset[simp]: "mset (run_compnet comps xs) = mset xs"
  sorry

definition sort4 :: compnet where
  "sort4 = undefined"

value "length sort4 \<le> 5"
value "run_compnet sort4 [4,2,1,3::nat] = [1,2,3,4]"

lemma sort4_bool_exhaust: "all_n_lists (\<lambda>bs::bool list. sorted (run_compnet sort4 bs)) 4"
  \<comment>\<open>Should be provable \<open>by eval\<close> if your definition is correct!\<close>
  sorry

lemma sort4_bool: "length (bs::bool list) = 4 \<Longrightarrow> sorted (run_compnet sort4 bs)"
  using sort4_bool_exhaust[unfolded all_n_lists_def] set_n_lists by fastforce

lemma compnet_map_mono:
  assumes "mono f"
  shows "run_compnet cs (map f xs) = map f (run_compnet cs xs)"
  sorry

theorem zero_one_principle:
  assumes "\<And>bs:: bool list. length bs = length xs \<Longrightarrow> sorted (run_compnet cs bs)"
  shows "sorted (run_compnet cs xs)" (is "sorted ?rs")
  sorry

corollary "length xs = 4 \<Longrightarrow> sorted (run_compnet sort4 xs)"
  by (simp add: sort4_bool zero_one_principle)

end

Check File

theory Check
  imports Submission
begin

lemma T_find_min_cmpx: "xs \<noteq> [] \<Longrightarrow> T_find_min xs = length xs - 1"
  by (rule Submission.T_find_min_cmpx)

theorem compnet_mset: "mset (run_compnet comps xs) = mset xs"
  by (rule Submission.compnet_mset)

lemma sort4_bool_exhaust: "all_n_lists (\<lambda>bs::bool list. sorted (run_compnet sort4 bs)) 4"
  by (rule Submission.sort4_bool_exhaust)

lemma compnet_map_mono: "(mono f) \<Longrightarrow> run_compnet cs (map f xs) = map f (run_compnet cs xs)"
  by (rule Submission.compnet_map_mono)

theorem zero_one_principle: "(\<And>bs:: bool list. length bs = length xs \<Longrightarrow> sorted (run_compnet cs bs)) \<Longrightarrow> sorted (run_compnet cs xs)"
  by (rule Submission.zero_one_principle)

end