# HG changeset patch # User nipkow # Date 1536584936 -7200 # Node ID 2881f6cccc67bf92afe4ba85b0730ea4011b5d54 # Parent 1254f3e57fed3c7933e1b3adbf02343f87b59fd1 tuned diff -r 1254f3e57fed -r 2881f6cccc67 src/HOL/Data_Structures/Sorting.thy --- a/src/HOL/Data_Structures/Sorting.thy Sun Sep 09 17:40:12 2018 +0100 +++ b/src/HOL/Data_Structures/Sorting.thy Mon Sep 10 15:08:56 2018 +0200 @@ -128,25 +128,25 @@ proof(induction xs rule: msort.induct) case (1 xs) let ?n = "length xs" - let ?xs1 = "take (?n div 2) xs" - let ?xs2 = "drop (?n div 2) xs" + let ?ys = "take (?n div 2) xs" + let ?zs = "drop (?n div 2) xs" show ?case proof cases assume "?n \ 1" thus ?thesis by(simp add: msort.simps[of xs]) next assume "\ ?n \ 1" - hence "mset (msort xs) = mset (msort ?xs1) + mset (msort ?xs2)" + hence "mset (msort xs) = mset (msort ?ys) + mset (msort ?zs)" by(simp add: msort.simps[of xs] mset_merge) - also have "\ = mset ?xs1 + mset ?xs2" + also have "\ = mset ?ys + mset ?zs" using \\ ?n \ 1\ by(simp add: "1.IH") - also have "\ = mset (?xs1 @ ?xs2)" by (simp del: append_take_drop_id) + also have "\ = mset (?ys @ ?zs)" by (simp del: append_take_drop_id) also have "\ = mset xs" by simp finally show ?thesis . qed qed -text \Via the previous lemma or directtly:\ +text \Via the previous lemma or directly:\ lemma set_merge: "set(merge xs ys) = set xs \ set ys" by (metis mset_merge set_mset_mset set_mset_union) @@ -157,7 +157,7 @@ lemma sorted_merge: "sorted (merge xs ys) \ (sorted xs \ sorted ys)" by(induction xs ys rule: merge.induct) (auto simp: set_merge) -lemma "sorted (msort xs)" +lemma sorted_msort: "sorted (msort xs)" proof(induction xs rule: msort.induct) case (1 xs) let ?n = "length xs" @@ -168,7 +168,7 @@ next assume "\ ?n \ 1" thus ?thesis using "1.IH" - by(simp add: sorted_merge msort.simps[of xs] mset_merge) + by(simp add: sorted_merge msort.simps[of xs]) qed qed