author nipkow Wed, 01 Apr 2020 21:48:39 +0200 changeset 71636 9d8fb1dbc368 parent 71635 b36f07d28867 child 71654 0aef1812ae3a
simplified code and proofs
```--- a/src/HOL/Data_Structures/AVL_Map.thy	Wed Apr 01 18:05:02 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Map.thy	Wed Apr 01 21:48:39 2020 +0200
@@ -18,7 +18,8 @@
fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
"delete _ Leaf = Leaf" |
"delete x (Node l ((a,b), h) r) = (case cmp x a of
-   EQ \<Rightarrow> del_root (Node l ((a,b), h) r) |
+   EQ \<Rightarrow> if l = Leaf then r
+         else let (l', ab') = split_max l in balR l' ab' r |
LT \<Rightarrow> balR (delete x l) (a,b) r |
GT \<Rightarrow> balL l (a,b) (delete x r))"

@@ -34,7 +35,7 @@
"sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
by(induction t)
(auto simp: del_list_simps inorder_balL inorder_balR
-     inorder_del_root inorder_split_maxD split: prod.splits)
+      inorder_split_maxD split: prod.splits)

subsection \<open>AVL invariants\<close>
@@ -120,7 +121,8 @@
case 1
show ?case
proof(cases "x = a")
-    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
+    case True with Node 1 show ?thesis
+      using avl_split_max[of l] by (auto simp: avl_balR split: prod.split)
next
case False
show ?thesis
@@ -133,11 +135,8 @@
case 2
show ?case
proof(cases "x = a")
-    case True
-    with 1 have "height (Node l (n, h) r) = height(del_root (Node l (n, h) r))
-      \<or> height (Node l (n, h) r) = height(del_root (Node l (n, h) r)) + 1"
-      by (subst height_del_root,simp_all)
-    with True show ?thesis by simp
+    case True then show ?thesis using 1 avl_split_max[of l]
+      by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split)
next
case False
show ?thesis ```
```--- a/src/HOL/Data_Structures/AVL_Set.thy	Wed Apr 01 18:05:02 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Wed Apr 01 21:48:39 2020 +0200
@@ -67,18 +67,12 @@

lemmas split_max_induct = split_max.induct[case_names Node Leaf]

-fun del_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
-"del_root (Node Leaf (a,_) r) = r" |
-"del_root (Node l (a,_) Leaf) = l" |
-"del_root (Node l (a,_) r) = (let (l', a') = split_max l in balR l' a' r)"
-
-lemmas del_root_cases = del_root.cases[split_format(complete), case_names Leaf_t Node_Leaf Node_Node]
-
fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
"delete _ Leaf = Leaf" |
"delete x (Node l (a, n) r) =
(case cmp x a of
-     EQ \<Rightarrow> del_root (Node l (a, n) r) |
+     EQ \<Rightarrow> if l = Leaf then r
+           else let (l', a') = split_max l in balR l' a' r |
LT \<Rightarrow> balR (delete x l) a r |
GT \<Rightarrow> balL l a (delete x r))"

@@ -112,16 +106,10 @@
by(induction t arbitrary: t' rule: split_max.induct)
(auto simp: inorder_balL split: if_splits prod.splits tree.split)

-lemma inorder_del_root:
-  "inorder (del_root (Node l ah r)) = inorder l @ inorder r"
-by(cases "Node l ah r" rule: del_root.cases)
-  (auto simp: inorder_balL inorder_balR inorder_split_maxD split: if_splits prod.splits)
-
theorem inorder_delete:
"sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
by(induction t)
-  (auto simp: del_list_simps inorder_balL inorder_balR
-    inorder_del_root inorder_split_maxD split: prod.splits)
+  (auto simp: del_list_simps inorder_balL inorder_balR inorder_split_maxD split: prod.splits)

subsection \<open>AVL invariants\<close>
@@ -307,58 +295,6 @@
apply (auto split:prod.splits simp del:avl.simps) by arith+
qed auto

-lemma avl_del_root:
-  assumes "avl t" and "t \<noteq> Leaf"
-  shows "avl(del_root t)"
-using assms
-proof (cases t rule:del_root_cases)
-  case (Node_Node ll ln lh lr n h rl rn rh rr)
-  let ?l = "Node ll (ln, lh) lr"
-  let ?r = "Node rl (rn, rh) rr"
-  let ?l' = "fst (split_max ?l)"
-  from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
-  from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
-  hence "avl(?l')" "height ?l = height(?l') \<or>
-         height ?l = height(?l') + 1" by (rule avl_split_max,simp)+
-  with \<open>avl t\<close> Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
-            \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
-  with \<open>avl ?l'\<close> \<open>avl ?r\<close> have "avl(balR ?l' (snd(split_max ?l)) ?r)"
-    by (rule avl_balR)
-  with Node_Node show ?thesis by (auto split:prod.splits)
-qed simp_all
-
-lemma height_del_root:
-  assumes "avl t" and "t \<noteq> Leaf"
-  shows "height t = height(del_root t) \<or> height t = height(del_root t) + 1"
-using assms
-proof (cases t rule: del_root_cases)
-  case (Node_Node ll lx lh lr x h rl rx rh rr)
-  let ?l = "Node ll (lx, lh) lr"
-  let ?r = "Node rl (rx, rh) rr"
-  let ?l' = "fst (split_max ?l)"
-  let ?t' = "balR ?l' (snd(split_max ?l)) ?r"
-  from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
-  from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
-  hence "avl(?l')"  by (rule avl_split_max,simp)
-  have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using \<open>avl ?l\<close> by (intro avl_split_max) auto
-  have t_height: "height t = 1 + max (height ?l) (height ?r)" using \<open>avl t\<close> Node_Node by simp
-  have "height t = height ?t' \<or> height t = height ?t' + 1" using  \<open>avl t\<close> Node_Node
-  proof(cases "height ?r = height ?l' + 2")
-    case False
-    show ?thesis using l'_height t_height False
-      by (subst height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
-  next
-    case True
-    show ?thesis
-    proof(cases rule: disjE[OF height_balR[OF True \<open>avl ?l'\<close> \<open>avl ?r\<close>, of "snd (split_max ?l)"]])
-      case 1 thus ?thesis using l'_height t_height True by arith
-    next
-      case 2 thus ?thesis using l'_height t_height True by arith
-    qed
-  qed
-  thus ?thesis using Node_Node by (auto split:prod.splits)
-qed simp_all
-
text\<open>Deletion maintains the AVL property:\<close>

theorem avl_delete:
@@ -370,7 +306,8 @@
case 1
show ?case
proof(cases "x = a")
-    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
+    case True with Node 1 show ?thesis
+      using avl_split_max[of l] by (auto simp: avl_balR split: prod.split)
next
case False
show ?thesis
@@ -383,11 +320,8 @@
case 2
show ?case
proof(cases "x = a")
-    case True
-    with 1 have "height (Node l (a,n) r) = height(del_root (Node l (a,n) r))
-      \<or> height (Node l (a,n) r) = height(del_root (Node l (a,n) r)) + 1"
-      by (subst height_del_root,simp_all)
-    with True show ?thesis by simp
+    case True then show ?thesis using 1 avl_split_max[of l]
+      by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split)
next
case False
show ?thesis ```