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 6

This is the task corresponding to homework 6.

## Resources

### 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)"

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

Terms and Conditions