author nipkow Mon, 02 Nov 2020 11:45:50 +0100 changeset 72540 8eabaf951e6b parent 72539 97f12d2c8bf2 child 72541 72b0490c8924
use min_height as in (much of?) the literature
```--- 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"

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"
-  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]
+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]

(* 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
```