--- 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