--- a/src/HOL/Data_Structures/Sorting.thy Thu May 03 22:34:49 2018 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy Fri May 04 15:59:21 2018 +0200
@@ -35,6 +35,7 @@
"isort [] = []" |
"isort (x#xs) = insort x (isort xs)"
+
subsubsection "Functional Correctness"
lemma mset_insort: "mset (insort x xs) = add_mset x (mset xs)"
@@ -48,11 +49,6 @@
apply (simp add: mset_insort)
done
-lemma "sorted (insort a xs) = sorted xs"
-apply(induction xs)
-apply (auto)
-oops
-
lemma set_insort: "set (insort x xs) = insert x (set xs)"
by (metis mset_insort set_mset_add_mset_insert set_mset_mset)
@@ -69,7 +65,8 @@
apply(auto simp: sorted_insort)
done
-subsection "Time Complexity"
+
+subsubsection "Time Complexity"
text \<open>We count the number of function calls.\<close>
@@ -137,6 +134,7 @@
declare msort.simps [simp del]
+
subsubsection "Functional Correctness"
lemma mset_merge: "mset(merge xs ys) = mset xs + mset ys"
@@ -185,7 +183,8 @@
qed
qed
-subsection "Time Complexity"
+
+subsubsection "Time Complexity"
text \<open>We only count the number of comparisons between list elements.\<close>
@@ -278,6 +277,7 @@
definition msort_bu :: "('a::linorder) list \<Rightarrow> 'a list" where
"msort_bu xs = (if xs = [] then [] else merge_all (map (\<lambda>x. [x]) xs))"
+
subsubsection "Functional Correctness"
lemma mset_merge_adj:
@@ -303,7 +303,8 @@
lemma mset_msort: "mset (msort_bu xs) = mset xs"
by(simp add: msort_bu_def msec_merge_all comp_def)
-subsection "Time Complexity"
+
+subsubsection "Time Complexity"
fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> real" where
"c_merge_adj [] = 0" |