# HG changeset patch
# User nipkow
# Date 1525442361 -7200
# Node ID 48e188cb1591751e925fcc9691cbbd48feb3f8c9
# Parent  ee8c13ae81e96337e63343fc7b5f3203ff33286e
tuned

diff -r ee8c13ae81e9 -r 48e188cb1591 src/HOL/Data_Structures/Sorting.thy
--- 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" |