--- a/src/HOL/Data_Structures/Binomial_Heap.thy Sat Jul 23 12:19:45 2022 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Mon Jul 25 12:19:59 2022 +0200
@@ -457,15 +457,15 @@
have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1"
by (simp add: sum_power2)
- also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1"
- using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "(^) (2::nat)"]
- using power_increasing[where a="2::nat"]
- by (auto simp: o_def)
- also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV
+ also have "\<dots> = (\<Sum>i\<leftarrow>[0..<length ts]. 2^i) + 1" (is "_ = ?S + 1")
+ by (simp add: interv_sum_list_conv_sum_set_nat)
+ also have "?S \<le> (\<Sum>t\<leftarrow>ts. 2^rank t)" (is "_ \<le> ?T")
+ using sorted_wrt_less_idx[OF ASC] by(simp add: sum_list_mono2)
+ also have "?T + 1 \<le> (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV
by (auto cong: map_cong simp: size_mset_tree)
also have "\<dots> = size (mset_trees ts) + 1"
unfolding mset_trees_def by (induction ts) auto
- finally have "2^length ts \<le> size (mset_trees ts) + 1" .
+ finally have "2^length ts \<le> size (mset_trees ts) + 1" by simp
then show ?thesis using le_log2_of_power by blast
qed
--- a/src/HOL/Groups_List.thy Sat Jul 23 12:19:45 2022 +0200
+++ b/src/HOL/Groups_List.thy Mon Jul 25 12:19:59 2022 +0200
@@ -252,6 +252,15 @@
qed
qed
+text \<open>A much more general version of this monotonicity lemma
+can be formulated with multisets and the multiset order\<close>
+
+lemma sum_list_mono2: fixes xs :: "'a ::ordered_comm_monoid_add list"
+shows "\<lbrakk> length xs = length ys; \<And>i. i < length xs \<longrightarrow> xs!i \<le> ys!i \<rbrakk>
+ \<Longrightarrow> sum_list xs \<le> sum_list ys"
+apply(induction xs ys rule: list_induct2)
+by(auto simp: nth_Cons' less_Suc_eq_0_disj imp_ex add_mono)
+
lemma (in monoid_add) sum_list_distinct_conv_sum_set:
"distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)"
by (induct xs) simp_all