summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 10 Sep 2018 15:08:56 +0200 | |

changeset 68966 | 2881f6cccc67 |

parent 68965 | 1254f3e57fed |

child 68967 | cd32e6b34b5c |

tuned

--- 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 \<le> 1" thus ?thesis by(simp add: msort.simps[of xs]) next assume "\<not> ?n \<le> 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 "\<dots> = mset ?xs1 + mset ?xs2" + also have "\<dots> = mset ?ys + mset ?zs" using \<open>\<not> ?n \<le> 1\<close> by(simp add: "1.IH") - also have "\<dots> = mset (?xs1 @ ?xs2)" by (simp del: append_take_drop_id) + also have "\<dots> = mset (?ys @ ?zs)" by (simp del: append_take_drop_id) also have "\<dots> = mset xs" by simp finally show ?thesis . qed qed -text \<open>Via the previous lemma or directtly:\<close> +text \<open>Via the previous lemma or directly:\<close> lemma set_merge: "set(merge xs ys) = set xs \<union> set ys" by (metis mset_merge set_mset_mset set_mset_union) @@ -157,7 +157,7 @@ lemma sorted_merge: "sorted (merge xs ys) \<longleftrightarrow> (sorted xs \<and> 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 "\<not> ?n \<le> 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