Homework 6

Definitions File

theory Defs
  imports "HOL-Data_Structures.Sorting"
begin

declare [[names_short]]


consts bubble :: "'a ::linorder list \<Rightarrow> 'a list"

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

consts bsort :: "'a::linorder list \<Rightarrow> 'a list"

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

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

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


end

Template File

theory Submission
  imports Defs
begin

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

fun bsort_aux :: "nat \<Rightarrow> 'a::linorder list \<Rightarrow> 'a list" where
  "bsort_aux 0 xs =  xs" |
  "bsort_aux (Suc n) xs = bsort_aux n (bubble xs)"

definition bsort :: "'a::linorder list \<Rightarrow> 'a list" where
  "bsort xs = bsort_aux (length xs) xs"

theorem bsort_mset: "mset (bsort xs) = mset xs"
  sorry

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

definition T_bsort :: "'a::linorder list \<Rightarrow> nat"  where
  "T_bsort _ = undefined"

theorem T_bsort: "\<exists>c d. T_bsort xs \<le> c * (length xs)^2 + d"
  sorry

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

lemma measure_sorted_0: "sorted xs \<longleftrightarrow> measure xs = 0"
  sorry

lemma measure_le[simp]: "measure (bubble xs) \<le> measure xs"
  sorry

lemma measure_dec[simp]: "\<not>sorted xs \<Longrightarrow> measure (bubble xs) < measure xs"
  sorry

lemma bsort_sorted: "sorted (bsort xs)"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem bsort_mset: "mset (bsort xs) = mset xs"
  by (rule Submission.bsort_mset)

theorem T_bsort: "\<exists>c d. T_bsort xs \<le> c * (length xs)^2 + d"
  by (rule Submission.T_bsort)

lemma measure_sorted_0: "sorted xs \<longleftrightarrow> measure xs = 0"
  by (rule Submission.measure_sorted_0)

lemma measure_le: "measure (bubble xs) \<le> measure xs"
  by (rule Submission.measure_le)

lemma measure_dec: "\<not>sorted xs \<Longrightarrow> measure (bubble xs) < measure xs"
  by (rule Submission.measure_dec)

lemma bsort_sorted: "sorted (bsort xs)"
  by (rule Submission.bsort_sorted)

end