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 6

This is the task corresponding to homework 6.


Download Files

Definitions File

theory Defs
  imports "HOL-Library.Multiset"

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)

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)

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"


Template File

theory Submission
  imports Defs

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"

theorem T_sel_sort_cmpx: "T_sel_sort xs = undefined"

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"

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>

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

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

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


Check File

theory Check
  imports Submission

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)


Terms and Conditions