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.

Download Files
### Definitions File

### Template File

### Check 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

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

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