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

Terms and Conditions