merge

--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Dec 06 12:03:56 2023 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Dec 06 12:45:51 2023 +0100
@@ -476,20 +476,16 @@
   estimations of their complexity.
 \<close>
 definition T_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
-[simp]: "T_link _ _ = 1"
+[simp]: "T_link _ _ = 0"
 
-text \<open>This function is non-canonical: we omitted a \<open>+1\<close> in the \<open>else\<close>-part,
-  to keep the following analysis simpler and more to the point.
-\<close>
 fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a trees \<Rightarrow> nat" where
   "T_ins_tree t [] = 1"
-| "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = (
-    (if rank t\<^sub>1 < rank t\<^sub>2 then 1
-     else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts)
-  )"
+| "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = 1 +
+    (if rank t\<^sub>1 < rank t\<^sub>2 then 0
+     else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts)"
 
 definition T_insert :: "'a::linorder \<Rightarrow> 'a trees \<Rightarrow> nat" where
-"T_insert x ts = T_ins_tree (Node 0 x []) ts + 1"
+"T_insert x ts = T_ins_tree (Node 0 x []) ts"
 
 lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
 by (induction t ts rule: T_ins_tree.induct) auto
@@ -498,11 +494,11 @@
 
 lemma T_insert_bound:
   assumes "invar ts"
-  shows "T_insert x ts \<le> log 2 (size (mset_trees ts) + 1) + 2"
+  shows "T_insert x ts \<le> log 2 (size (mset_trees ts) + 1) + 1"
 proof -
-  have "real (T_insert x ts) \<le> real (length ts) + 2"
-    unfolding T_insert_def using T_ins_tree_simple_bound 
-    using of_nat_mono by fastforce
+  have "real (T_insert x ts) \<le> real (length ts) + 1"
+    unfolding T_insert_def using T_ins_tree_simple_bound
+    by (metis of_nat_1 of_nat_add of_nat_mono) 
   also note size_mset_trees[OF \<open>invar ts\<close>]
   finally show ?thesis by simp
 qed
@@ -605,14 +601,13 @@
 
 definition T_del_min :: "'a::linorder trees \<Rightarrow> nat" where
   "T_del_min ts = T_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
-                    \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2
-  ) + 1"
+                    \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2)"
 
 lemma T_del_min_bound:
   fixes ts
   defines "n \<equiv> size (mset_trees ts)"
   assumes "invar ts" and "ts\<noteq>[]"
-  shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
+  shows "T_del_min ts \<le> 6 * log 2 (n+1) + 2"
 proof -
   obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
     by (metis surj_pair tree.exhaust_sel)
@@ -628,7 +623,7 @@
     using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
     by (auto simp: mset_trees_def)
 
-  have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2) + 1"
+  have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2)"
     unfolding T_del_min_def GM
     by simp
   also have "T_get_min_rest ts \<le> log 2 (n+1)" 
@@ -637,7 +632,7 @@
     unfolding T_rev_def n\<^sub>1_def using size_mset_trees[OF I1] by simp
   also have "T_merge (rev ts\<^sub>1) ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1"
     unfolding n\<^sub>1_def n\<^sub>2_def using T_merge_bound[OF I1 I2] by (simp add: algebra_simps)
-  finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 3"
+  finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 2"
     by (simp add: algebra_simps)
   also note \<open>n\<^sub>1 + n\<^sub>2 \<le> n\<close>
   also note \<open>n\<^sub>1 \<le> n\<close>

--- a/src/HOL/Data_Structures/Queue_2Lists.thy	Wed Dec 06 12:03:56 2023 +0100
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy	Wed Dec 06 12:45:51 2023 +0100
@@ -60,29 +60,23 @@
 text \<open>Running times:\<close>
 
 fun T_norm :: "'a queue \<Rightarrow> nat" where
-"T_norm (fs,rs) = (if fs = [] then T_itrev rs [] else 0) + 1"
+"T_norm (fs,rs) = (if fs = [] then T_itrev rs [] else 0)"
 
 fun T_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
-"T_enq a (fs,rs) = T_norm(fs, a # rs) + 1"
+"T_enq a (fs,rs) = T_norm(fs, a # rs)"
 
 fun T_deq :: "'a queue \<Rightarrow> nat" where
-"T_deq (fs,rs) = (if fs = [] then 0 else T_norm(tl fs,rs)) + 1"
-
-fun T_first :: "'a queue \<Rightarrow> nat" where
-"T_first (a # fs,rs) = 1"
-
-fun T_is_empty :: "'a queue \<Rightarrow> nat" where
-"T_is_empty (fs,rs) = 1"
+"T_deq (fs,rs) = (if fs = [] then 0 else T_norm(tl fs,rs))"
 
 text \<open>Amortized running times:\<close>
 
 fun \<Phi> :: "'a queue \<Rightarrow> nat" where
 "\<Phi>(fs,rs) = length rs"
 
-lemma a_enq: "T_enq a (fs,rs) + \<Phi>(enq a (fs,rs)) - \<Phi>(fs,rs) \<le> 4"
+lemma a_enq: "T_enq a (fs,rs) + \<Phi>(enq a (fs,rs)) - \<Phi>(fs,rs) \<le> 2"
 by(auto simp: T_itrev)
 
-lemma a_deq: "T_deq (fs,rs) + \<Phi>(deq (fs,rs)) - \<Phi>(fs,rs) \<le> 3"
+lemma a_deq: "T_deq (fs,rs) + \<Phi>(deq (fs,rs)) - \<Phi>(fs,rs) \<le> 1"
 by(auto simp: T_itrev)
 
 end

--- a/src/HOL/Data_Structures/Tree23_of_List.thy	Wed Dec 06 12:03:56 2023 +0100
+++ b/src/HOL/Data_Structures/Tree23_of_List.thy	Wed Dec 06 12:45:51 2023 +0100
@@ -130,7 +130,7 @@
 "T_leaves (a # as) = T_leaves as + 1"
 
 definition T_tree23_of_list :: "'a list \<Rightarrow> nat" where
-"T_tree23_of_list as = T_leaves as + T_join_all(leaves as) + 1"
+"T_tree23_of_list as = T_leaves as + T_join_all(leaves as)"
 
 lemma T_join_adj: "not_T ts \<Longrightarrow> T_join_adj ts \<le> len ts div 2"
 by(induction ts rule: T_join_adj.induct) auto
@@ -162,7 +162,7 @@
 lemma len_leaves: "len(leaves as) = length as + 1"
 by(induction as) auto
 
-lemma T_tree23_of_list: "T_tree23_of_list as \<le> 3*(length as) + 4"
+lemma T_tree23_of_list: "T_tree23_of_list as \<le> 3*(length as) + 3"
 using T_join_all[of "leaves as"] by(simp add: T_tree23_of_list_def T_leaves len_leaves)
 
 end