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.

Resources

Download Files

Definitions File

theory Defs
  imports "HOL-Library.Multiset"
begin

fun a :: "nat \<Rightarrow> int" where
"a 0 = 0" |
"a (Suc n) = a n ^ 2 + 1"

fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
  where
  "path G u [] v \<longleftrightarrow> u=v"
| "path G u (x#xs) v \<longleftrightarrow> G u x \<and> path G x xs v"

lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
  by (induction p1 arbitrary: u) auto

lemma pump_nondistinct_path:
  assumes P: "path G u p v"
  assumes ND: "\<not>distinct p"
  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
proof -
  from not_distinct_decomp[OF ND]
  obtain xs ys zs y where [simp]: "p = xs @ y # ys @ y # zs" by auto
  from P have 1: "path G u (xs@y#ys@y#ys@y#zs) v"
    by auto

  have 2: "length (xs@y#ys@y#ys@y#zs) > length p" "\<not>distinct (xs@y#ys@y#ys@y#zs)"
    by auto

  from 1 2 show ?thesis by blast
qed

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

consts compnet_step :: "(nat \<times> nat) \<Rightarrow> 'a :: linorder list \<Rightarrow> 'a list"
consts run_compnet :: "(nat \<times> nat) list \<Rightarrow> 'a :: linorder list \<Rightarrow> 'a list" 
consts sort4 :: "(nat \<times> nat) list"
end

Template File

theory Submission
  imports Defs
begin

lemma exists_simple_path:
  assumes "path G u p v"
  shows "\<exists>p'. path G u p' v \<and> distinct p'"
  sorry

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

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

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 = []"

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

lemma "length ls = 4 \<Longrightarrow> sorted (run_compnet sort4 ls)"
  oops

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)"
  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 exists_simple_path: "(path G u p v) \<Longrightarrow> \<exists>p'. path G u p' v \<and> distinct p'"
  by (rule Submission.exists_simple_path)

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