# HG changeset patch
# User nipkow
# Date 1588159112 -7200
# Node ID 7c25e3467cf0ca9e78d0eecc6547b595970a26c9
# Parent  fa4f8f3d69f2a709ef1e23af99007c349644fae2
tuned

diff -r fa4f8f3d69f2 -r 7c25e3467cf0 src/HOL/Data_Structures/Height_Balanced_Tree.thy
--- 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)
  apply(auto simp add:node_def balR_def split:tree.split)
  by arith+
@@ -144,32 +147,30 @@
 by (simp add: node_def)
 
 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