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

author | nipkow |

Sun, 09 Sep 2018 17:56:13 +0200 | |

changeset 68964 | ff6b594e4230 |

parent 68962 | 50676b0ab970 (current diff) |

parent 68963 | ed6511997d2b (diff) |

child 68965 | 1254f3e57fed |

merged

--- a/src/HOL/Data_Structures/Sorting.thy Sun Sep 09 17:49:15 2018 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Sun Sep 09 17:56:13 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)" by(simp add: msort_bu_def sorted_merge_all) -lemma mset_msort: "mset (msort_bu xs) = mset xs" +lemma mset_msort_bu: "mset (msort_bu xs) = mset xs" by(simp add: msort_bu_def msec_merge_all comp_def)