# HG changeset patch
# User nipkow
# Date 1683154425 -36000
# Node ID 051b09437a6b496867dac21339ce7a80bcd61f17
# Parent  041678c7f1476a7a18d861b3f64e0595b8bfb280# Parent  8fa4e4fd852e930d3d43e93aa0c9711ab10d6db2
merged

diff -r 041678c7f147 -r 051b09437a6b src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Wed May 03 10:35:20 2023 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu May 04 08:53:45 2023 +1000
@@ -158,6 +158,8 @@
 
 subsection "Complexity"
 
+text \<open>We count only the calls of the only recursive function: @{const merge}\<close>
+
 text\<open>Explicit termination argument: sum of sizes\<close>
 
 fun T_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
@@ -168,11 +170,11 @@
    else T_merge t1 r2) + 1"
 
 definition T_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
-"T_insert x t = T_merge (Node Leaf (x, 1) Leaf) t + 1"
+"T_insert x t = T_merge (Node Leaf (x, 1) Leaf) t"
 
 fun T_del_min :: "'a::ord lheap \<Rightarrow> nat" where
-"T_del_min Leaf = 1" |
-"T_del_min (Node l _ r) = T_merge l r + 1"
+"T_del_min Leaf = 0" |
+"T_del_min (Node l _ r) = T_merge l r"
 
 lemma T_merge_min_height: "ltree l \<Longrightarrow> ltree r \<Longrightarrow> T_merge l r \<le> min_height l + min_height r + 1"
 proof(induction l r rule: merge.induct)
@@ -185,7 +187,7 @@
   le_log2_of_power[OF min_height_size1[of r]] T_merge_min_height[of l r] assms
 by linarith
 
-corollary T_insert_log: "ltree t \<Longrightarrow> T_insert x t \<le> log 2 (size1 t) + 3"
+corollary T_insert_log: "ltree t \<Longrightarrow> T_insert x t \<le> log 2 (size1 t) + 2"
 using T_merge_log[of "Node Leaf (x, 1) Leaf" t]
 by(simp add: T_insert_def split: tree.split)
 
@@ -203,15 +205,15 @@
 qed
 
 corollary T_del_min_log: assumes "ltree t"
-  shows "T_del_min t \<le> 2 * log 2 (size1 t) + 1"
+  shows "T_del_min t \<le> 2 * log 2 (size1 t)"
 proof(cases t rule: tree2_cases)
   case Leaf thus ?thesis using assms by simp
 next
   case [simp]: (Node l _ _ r)
-  have "T_del_min t = T_merge l r + 1" by simp
-  also have "\<dots> \<le> log 2 (size1 l) + log 2 (size1 r) + 2"
+  have "T_del_min t = T_merge l r" by simp
+  also have "\<dots> \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
     using \<open>ltree t\<close> T_merge_log[of l r] by (auto simp del: T_merge.simps)
-  also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
+  also have "\<dots> \<le> 2 * log 2 (size1 t)"
     using ld_ld_1_less[of "size1 l" "size1 r"] by (simp)
   finally show ?thesis .
 qed