Homework 6

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