author nipkow Fri, 04 May 2018 15:59:21 +0200 changeset 68078 48e188cb1591 parent 68077 ee8c13ae81e9 child 68079 9c2088adff8b child 68080 17f79ae49401
tuned
```--- 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 @@
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)"

@@ -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"