author nipkow Tue, 28 Apr 2020 22:55:51 +0200 changeset 72027 fa4f8f3d69f2 parent 72025 3c6586a599bb (current diff) parent 72026 7567f73ef541 (diff) child 72028 7c25e3467cf0
merged
```--- a/src/HOL/Data_Structures/Height_Balanced_Tree.thy	Tue Apr 28 22:09:20 2020 +0200
+++ b/src/HOL/Data_Structures/Height_Balanced_Tree.thy	Tue Apr 28 22:55:51 2020 +0200
@@ -1,6 +1,4 @@
-(*
-Author: Tobias Nipkow
-*)
+(* Author: Tobias Nipkow *)

section "Height-Balanced Trees"

@@ -130,16 +128,14 @@

lemma height_balL:
"\<lbrakk> hbt l; hbt r; height l = height r + m + 2 \<rbrakk> \<Longrightarrow>
-   height (balL l a r) = height r + m + 2 \<or>
-   height (balL l a r) = height r + m + 3"
+   height (balL l a r) \<in> {height r + m + 2, height r + m + 3}"
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) = height l + m + 2 \<or>
-   height (balR l a r) = height l + m + 3"
+   height (balR l a r) \<in> {height l + m + 2, height l + m + 3}"
apply (cases r)
by arith+
@@ -184,15 +180,15 @@
case False
show ?thesis
proof(cases "x<a")
-      case True with Node 1 show ?thesis by (auto intro!:hbt_balL)
+      case True with 1 Node(1,2) show ?thesis by (auto intro!: hbt_balL)
next
-      case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto intro!:hbt_balR)
+      case False with 1 Node(3,4) \<open>x\<noteq>a\<close> show ?thesis by (auto intro!: hbt_balR)
qed
qed
case 2
show ?case
proof(cases "x = a")
-    case True with Node 1 show ?thesis by simp
+    case True with 2 show ?thesis by simp
next
case False
show ?thesis
@@ -200,34 +196,34 @@
case True
show ?thesis
proof(cases "height (insert x l) = height r + m + 2")
-        case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
+        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")
-          using Node 2 by (intro height_balL) simp_all
+          using 2 Node(1,2) height_balL[OF _ _ True] by simp
thus ?thesis
proof
-          assume ?A with Node(2) 2 True \<open>x < a\<close> show ?thesis by (auto)
+          assume ?A with 2 Node(2) True \<open>x < a\<close> show ?thesis by (auto)
next
-          assume ?B with Node(2) 1 True \<open>x < a\<close> show ?thesis by (simp) arith
+          assume ?B with 2 Node(2) True \<open>x < a\<close> show ?thesis by (simp) arith
qed
qed
next
case False
show ?thesis
proof(cases "height (insert x r) = height l + m + 2")
-        case False with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
+        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")
-          using Node 2 by (intro height_balR) simp_all
+          using Node 2 height_balR[OF _ _ True] by simp
thus ?thesis
proof
-          assume ?A with Node(4) 2 True \<open>\<not>x < a\<close> show ?thesis by (auto)
+          assume ?A with 2 Node(4) True \<open>\<not>x < a\<close> show ?thesis by (auto)
next
-          assume ?B with Node(4) 1 True \<open>\<not>x < a\<close> show ?thesis by (simp) arith
+          assume ?B with 2 Node(4) True \<open>\<not>x < a\<close> show ?thesis by (simp) arith
qed
qed
qed
@@ -256,9 +252,8 @@
text\<open>Deletion maintains @{const hbt}:\<close>

theorem hbt_delete:
-  assumes "hbt t"
-  shows "hbt(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
-using assms
+  "hbt t \<Longrightarrow> hbt(delete x t)"
+  "hbt t \<Longrightarrow> height t \<in> {height (delete x t), height (delete x t) + 1}"
proof (induct t rule: tree2_induct)
case (Node l a n r)
case 1
@@ -281,7 +276,7 @@
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")
-          using Node 2 by (intro height_balR) auto
+          using Node 2height_balR[OF _ _ True] by simp
thus ?thesis
proof
assume ?A with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def split!: if_splits)
@@ -298,7 +293,7 @@
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")
-          using Node 2 by (intro height_balL) auto
+          using Node 2 height_balL[OF _ _ True] by simp
thus ?thesis
proof
assume ?A with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def split: if_splits)
@@ -314,29 +309,22 @@
Complete automation as for insertion seems hard due to resource requirements.\<close>

theorem hbt_delete_auto:
-  assumes "hbt t"
-  shows "hbt(delete x t)" and "height t \<in> {height (delete x t), height (delete x t) + 1}"
-using assms
+  "hbt t \<Longrightarrow> hbt(delete x t)"
+  "hbt t \<Longrightarrow> height t \<in> {height (delete x t), height (delete x t) + 1}"
proof (induct t rule: tree2_induct)
case (Node l a n r)
case 1
-  show ?case
-  proof(cases "x = a")
-    case True thus ?thesis
-      using 1 hbt_split_max[of l] by (auto intro!: hbt_balR split: prod.split)
-  next
-    case False thus ?thesis
-      using Node 1 by (auto intro!: hbt_balL hbt_balR)
-  qed
+  thus ?case
+    using Node hbt_split_max[of l] by (auto intro!: hbt_balL hbt_balR split: prod.split)
case 2
show ?case
proof(cases "x = a")
case True thus ?thesis
-      using 1 hbt_split_max[of l]
+      using 2 hbt_split_max[of l]
by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split)
next
case False thus ?thesis
-      using height_balL[of l "delete x r" a] height_balR[of "delete x l" r a] Node 1
+      using height_balL[of l "delete x r" a] height_balR[of "delete x l" r a] 2 Node
by(auto simp: balL_def balR_def split!: if_split)
qed
qed simp_all```