# HG changeset patch # User nipkow # Date 1585770519 -7200 # Node ID 9d8fb1dbc3689b23469aec52bf7dea8edfe93afc # Parent b36f07d288675ce5f015e6699096314a74b4224f simplified code and proofs diff -r b36f07d28867 -r 9d8fb1dbc368 src/HOL/Data_Structures/AVL_Map.thy --- 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 \ ('a*'b) avl_tree \ ('a*'b) avl_tree" where "delete _ Leaf = Leaf" | "delete x (Node l ((a,b), h) r) = (case cmp x a of - EQ \ del_root (Node l ((a,b), h) r) | + EQ \ if l = Leaf then r + else let (l', ab') = split_max l in balR l' ab' r | LT \ balR (delete x l) (a,b) r | GT \ balL l (a,b) (delete x r))" @@ -34,7 +35,7 @@ "sorted1(inorder t) \ 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 \AVL invariants\ @@ -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)) - \ 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 diff -r b36f07d28867 -r 9d8fb1dbc368 src/HOL/Data_Structures/AVL_Set.thy --- 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 \ '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 \ 'a avl_tree \ 'a avl_tree" where "delete _ Leaf = Leaf" | "delete x (Node l (a, n) r) = (case cmp x a of - EQ \ del_root (Node l (a, n) r) | + EQ \ if l = Leaf then r + else let (l', a') = split_max l in balR l' a' r | LT \ balR (delete x l) a r | GT \ 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) \ 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 \AVL invariants\ @@ -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 \ 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 \avl t\ and Node_Node have "avl ?r" by simp - from \avl t\ and Node_Node have "avl ?l" by simp - hence "avl(?l')" "height ?l = height(?l') \ - height ?l = height(?l') + 1" by (rule avl_split_max,simp)+ - with \avl t\ Node_Node have "height ?l' = height ?r \ height ?l' = height ?r + 1 - \ height ?r = height ?l' + 1 \ height ?r = height ?l' + 2" by fastforce - with \avl ?l'\ \avl ?r\ 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 \ Leaf" - shows "height t = height(del_root t) \ 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 \avl t\ and Node_Node have "avl ?r" by simp - from \avl t\ and Node_Node have "avl ?l" by simp - hence "avl(?l')" by (rule avl_split_max,simp) - have l'_height: "height ?l = height ?l' \ height ?l = height ?l' + 1" using \avl ?l\ by (intro avl_split_max) auto - have t_height: "height t = 1 + max (height ?l) (height ?r)" using \avl t\ Node_Node by simp - have "height t = height ?t' \ height t = height ?t' + 1" using \avl t\ Node_Node - proof(cases "height ?r = height ?l' + 2") - case False - show ?thesis using l'_height t_height False - by (subst height_balR2[OF \avl ?l'\ \avl ?r\ False])+ arith - next - case True - show ?thesis - proof(cases rule: disjE[OF height_balR[OF True \avl ?l'\ \avl ?r\, 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\Deletion maintains the AVL property:\ 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)) - \ 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