author nipkow Wed, 29 Apr 2020 13:18:32 +0200 changeset 71812 7c25e3467cf0 parent 71811 fa4f8f3d69f2 child 71813 b11d7ffb48e0
tuned
```--- a/src/HOL/Data_Structures/Height_Balanced_Tree.thy	Tue Apr 28 22:55:51 2020 +0200
+++ b/src/HOL/Data_Structures/Height_Balanced_Tree.thy	Wed Apr 29 13:18:32 2020 +0200
@@ -17,16 +17,19 @@
definition empty :: "'a hbt" where
"empty = Leaf"

-text \<open>The maximal amount that the height of two siblings may differ.\<close>
+text \<open>The maximal amount by which the height of two siblings may differ:\<close>

-consts m :: nat
+locale HBT =
+fixes m :: nat
+assumes [arith]: "m > 0"
+begin

text \<open>Invariant:\<close>

fun hbt :: "'a hbt \<Rightarrow> bool" where
"hbt Leaf = True" |
"hbt (Node l (a,n) r) =
- (abs(int(height l) - int(height r)) \<le> int(m+1) \<and>
+ (abs(int(height l) - int(height r)) \<le> int(m) \<and>
n = max (height l) (height r) + 1 \<and> hbt l \<and> hbt r)"

fun ht :: "'a hbt \<Rightarrow> nat" where
@@ -38,7 +41,7 @@

definition balL :: "'a hbt \<Rightarrow> 'a \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
"balL AB b C =
-  (if ht AB = ht C + m + 2 then
+  (if ht AB = ht C + m + 1 then
case AB of
Node A (a, _) B \<Rightarrow>
if ht A \<ge> ht B then node A a (node B b C)
@@ -49,7 +52,7 @@

definition balR :: "'a hbt \<Rightarrow> 'a \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
"balR A a BC =
-   (if ht BC = ht A + m + 2 then
+   (if ht BC = ht A + m + 1 then
case BC of
Node B (b, _) C \<Rightarrow>
if ht B \<le> ht C then node (node A a B) b C
@@ -127,15 +130,15 @@
text \<open>First, a fast but relatively manual proof with many lemmas:\<close>

lemma height_balL:
-  "\<lbrakk> hbt l; hbt r; height l = height r + m + 2 \<rbrakk> \<Longrightarrow>
-   height (balL l a r) \<in> {height r + m + 2, height r + m + 3}"
+  "\<lbrakk> hbt l; hbt r; height l = height r + m + 1 \<rbrakk> \<Longrightarrow>
+   height (balL l a r) \<in> {height r + m + 1, height r + m + 2}"
apply (cases l)
apply (auto simp:node_def balL_def split:tree.split)
by arith+

lemma height_balR:
-  "\<lbrakk> hbt l; hbt r; height r = height l + m + 2 \<rbrakk> \<Longrightarrow>
-   height (balR l a r) \<in> {height l + m + 2, height l + m + 3}"
+  "\<lbrakk> hbt l; hbt r; height r = height l + m + 1 \<rbrakk> \<Longrightarrow>
+   height (balR l a r) \<in> {height l + m + 1, height l + m + 2}"
apply (cases r)
by arith+
@@ -144,32 +147,30 @@

lemma height_balL2:
-  "\<lbrakk> hbt l; hbt r; height l \<noteq> height r + m + 2 \<rbrakk> \<Longrightarrow>
+  "\<lbrakk> hbt l; hbt r; height l \<noteq> height r + m + 1 \<rbrakk> \<Longrightarrow>
height (balL l a r) = 1 + max (height l) (height r)"
by (cases l, cases r) (simp_all add: balL_def)

lemma height_balR2:
-  "\<lbrakk> hbt l;  hbt r;  height r \<noteq> height l + m + 2 \<rbrakk> \<Longrightarrow>
+  "\<lbrakk> hbt l;  hbt r;  height r \<noteq> height l + m + 1 \<rbrakk> \<Longrightarrow>
height (balR l a r) = 1 + max (height l) (height r)"
by (cases l, cases r) (simp_all add: balR_def)

lemma hbt_balL:
-  "\<lbrakk> hbt l; hbt r; height r - m - 1 \<le> height l \<and> height l \<le> height r + m + 2 \<rbrakk> \<Longrightarrow> hbt(balL l a r)"
+  "\<lbrakk> hbt l; hbt r; height r - m \<le> height l \<and> height l \<le> height r + m + 1 \<rbrakk> \<Longrightarrow> hbt(balL l a r)"
by(cases l, cases r)
-  (auto simp: balL_def node_def split!: if_split tree.split)
+  (auto simp: balL_def node_def max_def split!: if_splits tree.split)

lemma hbt_balR:
-  "\<lbrakk> hbt l; hbt r; height l - m - 1 \<le> height r \<and> height r \<le> height l + m + 2 \<rbrakk> \<Longrightarrow> hbt(balR l a r)"
+  "\<lbrakk> hbt l; hbt r; height l - m \<le> height r \<and> height r \<le> height l + m + 1 \<rbrakk> \<Longrightarrow> hbt(balR l a r)"
by(cases r, cases l)
-  (auto simp: balR_def node_def split!: if_split tree.split)
+  (auto simp: balR_def node_def max_def split!: if_splits tree.split)

text\<open>Insertion maintains @{const hbt}. Requires simultaneous proof.\<close>

theorem hbt_insert:
-  assumes "hbt t"
-  shows "hbt(insert x t)"
-        "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
-using assms
+  "hbt t \<Longrightarrow> hbt(insert x t)"
+  "hbt t \<Longrightarrow> height (insert x t) \<in> {height t, height t + 1}"
proof (induction t rule: tree2_induct)
case (Node l a _ r)
case 1
@@ -195,12 +196,12 @@
proof(cases "x<a")
case True
show ?thesis
-      proof(cases "height (insert x l) = height r + m + 2")
+      proof(cases "height (insert x l) = height r + m + 1")
case False with 2 Node(1,2) \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
next
case True
-        hence "(height (balL (insert x l) a r) = height r + m + 2) \<or>
-          (height (balL (insert x l) a r) = height r + m + 3)" (is "?A \<or> ?B")
+        hence "(height (balL (insert x l) a r) = height r + m + 1) \<or>
+          (height (balL (insert x l) a r) = height r + m + 2)" (is "?A \<or> ?B")
using 2 Node(1,2) height_balL[OF _ _ True] by simp
thus ?thesis
proof
@@ -212,12 +213,12 @@
next
case False
show ?thesis
-      proof(cases "height (insert x r) = height l + m + 2")
+      proof(cases "height (insert x r) = height l + m + 1")
case False with 2 Node(3,4) \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
next
case True
-        hence "(height (balR l a (insert x r)) = height l + m + 2) \<or>
-          (height (balR l a (insert x r)) = height l + m + 3)"  (is "?A \<or> ?B")
+        hence "(height (balR l a (insert x r)) = height l + m + 1) \<or>
+          (height (balR l a (insert x r)) = height l + m + 2)"  (is "?A \<or> ?B")
using Node 2 height_balR[OF _ _ True] by simp
thus ?thesis
proof
@@ -270,12 +271,12 @@
proof(cases "x<a")
case True
show ?thesis
-      proof(cases "height r = height (delete x l) + m + 2")
+      proof(cases "height r = height (delete x l) + m + 1")
case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def)
next
case True
-        hence "(height (balR (delete x l) a r) = height (delete x l) + m + 2) \<or>
-          height (balR (delete x l) a r) = height (delete x l) + m + 3" (is "?A \<or> ?B")
+        hence "(height (balR (delete x l) a r) = height (delete x l) + m + 1) \<or>
+          height (balR (delete x l) a r) = height (delete x l) + m + 2" (is "?A \<or> ?B")
using Node 2height_balR[OF _ _ True] by simp
thus ?thesis
proof
@@ -287,12 +288,12 @@
next
case False
show ?thesis
-      proof(cases "height l = height (delete x r) + m + 2")
+      proof(cases "height l = height (delete x r) + m + 1")
case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def)
next
case True
-        hence "(height (balL l a (delete x r)) = height (delete x r) + m + 2) \<or>
-          height (balL l a (delete x r)) = height (delete x r) + m + 3" (is "?A \<or> ?B")
+        hence "(height (balL l a (delete x r)) = height (delete x r) + m + 1) \<or>
+          height (balL l a (delete x r)) = height (delete x r) + m + 2" (is "?A \<or> ?B")
using Node 2 height_balL[OF _ _ True] by simp
thus ?thesis
proof
@@ -352,3 +353,5 @@
qed

end
+
+end```