author nipkow Sun, 09 Sep 2018 17:56:00 +0200 changeset 68963 ed6511997d2b parent 68961 22a3790eecae child 68964 ff6b594e4230
tuned
```--- a/src/HOL/Data_Structures/Sorting.thy	Sun Sep 09 13:48:20 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Sun Sep 09 17:56:00 2018 +0200
@@ -124,7 +124,7 @@
lemma mset_merge: "mset(merge xs ys) = mset xs + mset ys"
by(induction xs ys rule: merge.induct) auto

-lemma "mset (msort xs) = mset xs"
+lemma mset_msort: "mset (msort xs) = mset xs"
proof(induction xs rule: msort.induct)
case (1 xs)
let ?n = "length xs"
@@ -146,7 +146,12 @@
qed
qed

+text \<open>Via the previous lemma or directtly:\<close>
+
lemma set_merge: "set(merge xs ys) = set xs \<union> set ys"
+by (metis mset_merge set_mset_mset set_mset_union)
+
+lemma "set(merge xs ys) = set xs \<union> set ys"
by(induction xs ys rule: merge.induct) (auto)

lemma sorted_merge: "sorted (merge xs ys) \<longleftrightarrow> (sorted xs \<and> sorted ys)"
@@ -236,7 +241,7 @@
qed

(* Beware of conversions: *)
-lemma "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)"
+lemma c_msort_log: "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)"
using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps)
by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult)

@@ -284,7 +289,7 @@
lemma sorted_msort_bu: "sorted (msort_bu xs)"