# HG changeset patch
# User nipkow
# Date 1604313950 -3600
# Node ID 8eabaf951e6b8549c2cb3a4a5b0958008d01b09b
# Parent  97f12d2c8bf2c735c02f63728855c63e8d12b9ee
use min_height as in (much of?) the literature

diff -r 97f12d2c8bf2 -r 8eabaf951e6b src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Sun Nov 01 18:24:10 2020 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Mon Nov 02 11:45:50 2020 +0100
@@ -16,32 +16,28 @@
 
 type_synonym 'a lheap = "('a*nat)tree"
 
-fun rank :: "'a lheap \<Rightarrow> nat" where
-"rank Leaf = 0" |
-"rank (Node _ _ r) = rank r + 1"
-
-fun rk :: "'a lheap \<Rightarrow> nat" where
-"rk Leaf = 0" |
-"rk (Node _ (_, n) _) = n"
+fun mht :: "'a lheap \<Rightarrow> nat" where
+"mht Leaf = 0" |
+"mht (Node _ (_, n) _) = n"
 
 text\<open>The invariants:\<close>
 
 fun (in linorder) heap :: "('a*'b) tree \<Rightarrow> bool" where
 "heap Leaf = True" |
 "heap (Node l (m, _) r) =
-  (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
+  ((\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x) \<and> heap l \<and> heap r)"
 
 fun ltree :: "'a lheap \<Rightarrow> bool" where
 "ltree Leaf = True" |
 "ltree (Node l (a, n) r) =
- (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
+ (min_height l \<ge> min_height r \<and> n = min_height r + 1 \<and> ltree l & ltree r)"
 
 definition empty :: "'a lheap" where
 "empty = Leaf"
 
 definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
 "node l a r =
- (let rl = rk l; rr = rk r
+ (let rl = mht l; rr = mht r
   in if rl \<ge> rr then Node l (a,rr+1) r else Node r (a,rl+1) l)"
 
 fun get_min :: "'a lheap \<Rightarrow> 'a" where
@@ -82,11 +78,11 @@
 lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
-lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
+lemma mht_eq_min_height: "ltree t \<Longrightarrow> mht t = min_height t"
 by(cases t) auto
 
 lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r"
-by(auto simp add: node_def)
+by(auto simp add: node_def mht_eq_min_height)
 
 lemma heap_node: "heap (node l a r) \<longleftrightarrow>
   heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. a \<le> x)"
@@ -162,51 +158,36 @@
 
 subsection "Complexity"
 
-lemma pow2_rank_size1: "ltree t \<Longrightarrow> 2 ^ rank t \<le> size1 t"
-proof(induction t rule: tree2_induct)
-  case Leaf show ?case by simp
-next
-  case (Node l a n r)
-  hence "rank r \<le> rank l" by simp
-  hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp
-  have "(2::nat) ^ rank \<langle>l, (a, n), r\<rangle> = 2 ^ rank r + 2 ^ rank r"
-    by(simp add: mult_2)
-  also have "\<dots> \<le> size1 l + size1 r"
-    using Node * by (simp del: power_increasing_iff)
-  also have "\<dots> = size1 \<langle>l, (a, n), r\<rangle>" by simp
-  finally show ?case .
-qed
-
 text\<open>Explicit termination argument: sum of sizes\<close>
 
-fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
-"t_merge Leaf t = 1" |
-"t_merge t Leaf = 1" |
-"t_merge (Node l1 (a1, n1) r1 =: t1) (Node l2 (a2, n2) r2 =: t2) =
-  (if a1 \<le> a2 then 1 + t_merge r1 t2
-   else 1 + t_merge t1 r2)"
+fun T_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
+"T_merge Leaf t = 1" |
+"T_merge t Leaf = 1" |
+"T_merge (Node l1 (a1, n1) r1 =: t1) (Node l2 (a2, n2) r2 =: t2) =
+  (if a1 \<le> a2 then T_merge r1 t2
+   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"
+definition T_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
+"T_insert x t = T_merge (Node Leaf (x, 1) Leaf) t + 1"
 
-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"
+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"
 
-lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
+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)
-  case 3 thus ?case by(simp)
+  case 3 thus ?case by(auto)
 qed simp_all
 
-corollary t_merge_log: assumes "ltree l" "ltree r"
-  shows "t_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
-using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]]
-  le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_merge_rank[of l r]
+corollary T_merge_log: assumes "ltree l" "ltree r"
+  shows "T_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
+using le_log2_of_power[OF min_height_size1[of l]]
+  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) + 2"
-using t_merge_log[of "Node Leaf (x, 1) Leaf" t]
-by(simp add: t_insert_def split: tree.split)
+corollary T_insert_log: "ltree t \<Longrightarrow> T_insert x t \<le> log 2 (size1 t) + 3"
+using T_merge_log[of "Node Leaf (x, 1) Leaf" t]
+by(simp add: T_insert_def split: tree.split)
 
 (* FIXME mv ? *)
 lemma ld_ld_1_less:
@@ -221,17 +202,17 @@
   finally show ?thesis by simp
 qed
 
-corollary t_del_min_log: assumes "ltree t"
-  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
+corollary T_del_min_log: assumes "ltree t"
+  shows "T_del_min t \<le> 2 * log 2 (size1 t) + 1"
 proof(cases t rule: tree2_cases)
   case Leaf thus ?thesis using assms by simp
 next
-  case [simp]: (Node t1 _ _ t2)
-  have "t_del_min t = t_merge t1 t2" by simp
-  also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
-    using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)
+  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"
+    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"
-    using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp)
+    using ld_ld_1_less[of "size1 l" "size1 r"] by (simp)
   finally show ?thesis .
 qed