diff --git a/thys/Amortized_Complexity/Splay_Tree_Analysis.thy b/thys/Amortized_Complexity/Splay_Tree_Analysis.thy --- a/thys/Amortized_Complexity/Splay_Tree_Analysis.thy +++ b/thys/Amortized_Complexity/Splay_Tree_Analysis.thy @@ -1,421 +1,421 @@ subsection "Splay Tree Analysis" theory Splay_Tree_Analysis imports Splay_Tree_Analysis_Base Amortized_Framework begin subsubsection "Analysis of splay" definition a_splay :: "'a::linorder \ 'a tree \ real" where "a_splay a t = t_splay a t + \(splay a t) - \ t" -lemma a_splay_simps[simp]: "a_splay a (Node l a r) = 1" - "a a_splay a (Node (Node ll a lr) b r) = \ (Node lr b r) - \ (Node ll a lr) + 1" - "b a_splay a (Node l b (Node rl a rr)) = \ (Node rl b l) - \ (Node rl a rr) + 1" +lemma a_splay_simps[simp]: "a_splay a (Node AB a CD) = 1" + "a a_splay a (Node (Node A a B) b CD) = \ (Node B b CD) - \ (Node A a B) + 1" + "b a_splay c (Node AB b (Node C c D)) = \ (Node C b AB) - \ (Node C c D) + 1" by(auto simp add: a_splay_def algebra_simps) text\The following lemma is an attempt to prove a generic lemma that covers both zig-zig cases. However, the lemma is not as nice as one would like. Hence it is used only once, as a demo. Ideally the lemma would involve function @{const a_splay}, but that is impossible because this involves @{const splay} and thus depends on the ordering. We would need a truly symmetric version of @{const splay} that takes the ordering as an explicit argument. Then we could define all the symmetric cases by one final equation @{term"splay2 less t = splay2 (not o less) (mirror t)"}. This would simplify the code and the proofs.\ lemma zig_zig: fixes lx x rx lb b rb a ra u lb1 lb2 defines [simp]: "X == Node lx (x) rx" defines[simp]: "B == Node lb b rb" defines [simp]: "t == Node B a ra" defines [simp]: "A' == Node rb a ra" defines [simp]: "t' == Node lb1 u (Node lb2 b A')" assumes hyps: "lb \ \\" and IH: "t_splay x lb + \ lb1 + \ lb2 - \ lb \ 2 * \ lb - 3 * \ X + 1" and prems: "size lb = size lb1 + size lb2 + 1" "X \ subtrees lb" shows "t_splay x lb + \ t' - \ t \ 3 * (\ t - \ X)" proof - define B' where [simp]: "B' = Node lb2 b A'" have "t_splay x lb + \ t' - \ t = t_splay x lb + \ lb1 + \ lb2 - \ lb + \ B' + \ A' - \ B" using prems by(auto simp: a_splay_def size_if_splay algebra_simps in_set_tree_if split: tree.split) also have "\ \ 2 * \ lb + \ B' + \ A' - \ B - 3 * \ X + 1" using IH prems(2) by(auto simp: algebra_simps) also have "\ \ \ lb + \ B' + \ A' - 3 * \ X + 1" by(simp) also have "\ \ \ B' + 2 * \ t - 3 * \ X " using prems ld_ld_1_less[of "size1 lb" "size1 A'"] by(simp add: size_if_splay) also have "\ \ 3 * \ t - 3 * \ X" using prems by(simp add: size_if_splay) finally show ?thesis by simp qed lemma a_splay_ub: "\ bst t; Node l x r : subtrees t \ \ a_splay x t \ 3 * (\ t - \(Node l x r)) + 1" proof(induction x t rule: splay.induct) case 1 thus ?case by simp next case 2 thus ?case by auto next case 4 hence False by(fastforce dest: in_set_tree_if) thus ?case .. next case 5 hence False by(fastforce dest: in_set_tree_if) thus ?case .. next case 7 hence False by(fastforce dest: in_set_tree_if) thus ?case .. next case 10 hence False by(fastforce dest: in_set_tree_if) thus ?case .. next case 12 hence False by(fastforce dest: in_set_tree_if) thus ?case .. next case 13 hence False by(fastforce dest: in_set_tree_if) thus ?case .. next case (3 x b A B C) let ?A = "Node (Node A x B) b C" have "x \ set_tree C" using "3.prems"(1) by auto with 3 show ?case using log_le_cancel_iff[of 2 "size1(Node B b C)" "size1 ?A"] log_le_cancel_iff[of 2 "size1(Node A x B)" "size1 ?A"] by (auto simp: algebra_simps simp del:log_le_cancel_iff) next case (9 a x A B C) let ?A = "\A, a, \B, x, C\\" have "x \ set_tree A" using "9.prems"(1) by auto with 9 show ?case using log_le_cancel_iff[of 2 "size1(Node A a B)" "size1 ?A"] log_le_cancel_iff[of 2 "size1(Node B x C)" "size1 ?A"] by (auto simp: algebra_simps simp del:log_le_cancel_iff) next case (6 x b c AB C D) hence 0: "x \ set_tree C \ x \ set_tree D" using "6.prems"(1) by auto hence 1: "x \ set_tree AB" using "6.prems" \x by (auto) obtain A a B where sp: "splay x AB = Node A a B" using splay_not_Leaf[OF \AB \ Leaf\] by blast let ?X = "Node l x r" let ?ABC = "Node AB b C" let ?ABCD = "Node ?ABC c D" let ?AB = "Node A a B" let ?CD = "Node C c D" let ?BCD = "Node B b ?CD" have "a_splay x ?ABCD = a_splay x AB + \ ?BCD + \ ?CD - \ ?ABC - \ ?AB + 1" using "6.prems" 1 sp by(auto simp: a_splay_def size_if_splay algebra_simps split: tree.split) also have "\ \ 3 * \ AB + \ ?BCD + \ ?CD - \ ?ABC - \ ?AB - 3 * \ ?X + 2" using 6 0 by(auto simp: algebra_simps) also have "\ = 2 * \ AB + \ ?BCD + \ ?CD - \ ?ABC - 3 * \ ?X + 2" using sp by(simp add: size_if_splay) also have "\ \ \ AB + \ ?BCD + \ ?CD - 3 * \ ?X + 2" by(simp) also have "\ \ \ ?BCD + 2 * \ ?ABCD - 3 * \ ?X + 1" using sp ld_ld_1_less[of "size1 AB" "size1 ?CD"] by(simp add: size_if_splay) also have "\ \ 3 * \ ?ABCD - 3 * \ ?X + 1" using sp by(simp add: size_if_splay) finally show ?case by simp next case (8 a x c BC A D) hence 0: "x \ set_tree A \ x \ set_tree D" using "8.prems"(1) \x < c\ by(auto) hence 1: "x \ set_tree BC" using "8.prems" \a \x by (auto) obtain B b C where sp: "splay x BC = Node B b C" using splay_not_Leaf[OF \BC \ Leaf\] by blast let ?X = "Node l x r" let ?ABC = "Node A a BC" let ?ABCD = "Node ?ABC c D" let ?BC = "Node B b C" let ?AB = "Node A a B" let ?CD = "Node C c D" have "a_splay x ?ABCD = a_splay x BC + \ ?AB + \ ?CD - \ ?ABC - \ ?BC + 1" using "8.prems" 1 sp by(auto simp: a_splay_def size_if_splay algebra_simps split: tree.split) also have "\ \ 3 * \ BC + \ ?AB + \ ?CD - \ ?ABC - \ ?BC - 3 * \ ?X + 2" using 8 0 by(auto simp: algebra_simps) also have "\ = 2 * \ BC + \ ?AB + \ ?CD - \ ?ABC - 3 * \ ?X + 2" using sp by(simp add: size_if_splay) also have "\ \ \ BC + \ ?AB + \ ?CD - 3 * \ ?X + 2" by(simp) also have "\ \ \ BC + 2 * \ ?ABCD - 3 * \ ?X + 1" using sp ld_ld_1_less[of "size1 ?AB" "size1 ?CD"] by(simp add: size_if_splay) also have "\ \ 3 * \ ?ABCD - 3 * \ ?X + 1" by(simp) finally show ?case by simp next case (11 a x c BC A D) hence 0: "x \ set_tree D \ x \ set_tree A" using "11.prems"(1) \a by (auto) hence 1: "x \ set_tree BC" using "11.prems" \a \x by (auto) obtain B b C where sp: "splay x BC = Node B b C" using splay_not_Leaf[OF \BC \ Leaf\] by blast let ?X = "Node l x r" let ?BCD = "Node BC c D" let ?ABCD = "Node A a ?BCD" let ?BC = "Node B b C" let ?CD = "Node C c D" let ?AB = "Node A a B" have "a_splay x ?ABCD = a_splay x BC + \ ?CD + \ ?AB - \ ?BCD - \ ?BC + 1" using "11.prems" 1 sp by(auto simp: a_splay_def size_if_splay algebra_simps split: tree.split) also have "\ \ 3 * \ BC + \ ?CD + \ ?AB - \ ?BCD - \ ?BC - 3 * \ ?X + 2" using 11 0 by(auto simp: algebra_simps) also have "\ = 2 * \ BC + \ ?CD + \ ?AB - \ ?BCD - 3 * \ ?X + 2" using sp by(simp add: size_if_splay) also have "\ \ \ BC + \ ?CD + \ ?AB - 3 * \ ?X + 2" by(simp) also have "\ \ \ BC + 2 * \ ?ABCD - 3 * \ ?X + 1" using sp ld_ld_1_less[of "size1 ?CD" "size1 ?AB"] by(simp add: size_if_splay algebra_simps) also have "\ \ 3 * \ ?ABCD - 3 * \ ?X + 1" by(simp) finally show ?case by simp next case (14 a x b CD A B) hence 0: "x \ set_tree B \ x \ set_tree A" using "14.prems"(1) \b by(auto) hence 1: "x \ set_tree CD" using "14.prems" \b \a by (auto) obtain C c D where sp: "splay x CD = Node C c D" using splay_not_Leaf[OF \CD \ Leaf\] by blast from zig_zig[of CD x D C l r _ b B a A] 14 sp 0 show ?case by(auto simp: a_splay_def size_if_splay algebra_simps) (* The explicit version: have "a_splay x ?A = a_splay x ?R + \ ?B' + \ ?A' - \ ?B - \ ?R' + 1" using "14.prems" 1 sp by(auto simp: a_splay_def size_if_splay algebra_simps split: tree.split) also have "\ \ 3 * \ ?R + \ ?B' + \ ?A' - \ ?B - \ ?R' - 3 * \ ?X + 2" using 14 0 by(auto simp: algebra_simps) also have "\ = 2 * \ rb + \ ?B' + \ ?A' - \ ?B - 3 * \ ?X + 2" using sp by(simp add: size_if_splay) also have "\ \ \ ?R + \ ?B' + \ ?A' - 3 * \ ?X + 2" by(simp) also have "\ \ \ ?B' + 2 * \ ?A - 3 * \ ?X + 1" using sp ld_ld_1_less[of "size1 ?R" "size1 ?A'"] by(simp add: size_if_splay algebra_simps) also have "\ \ 3 * \ ?A - 3 * \ ?X + 1" using sp by(simp add: size_if_splay) finally show ?case by simp *) qed -lemma a_splay_ub2: assumes "bst t" "a : set_tree t" -shows "a_splay a t \ 3 * (\ t - 1) + 1" +lemma a_splay_ub2: assumes "bst t" "x : set_tree t" +shows "a_splay x t \ 3 * (\ t - 1) + 1" proof - - from assms(2) obtain la ra where N: "Node la a ra : subtrees t" + from assms(2) obtain l r where N: "Node l x r : subtrees t" by (metis set_treeE) - have "a_splay a t \ 3 * (\ t - \(Node la a ra)) + 1" by(rule a_splay_ub[OF assms(1) N]) + have "a_splay x t \ 3 * (\ t - \(Node l x r)) + 1" by(rule a_splay_ub[OF assms(1) N]) also have "\ \ 3 * (\ t - 1) + 1" by(simp add: field_simps) finally show ?thesis . qed -lemma a_splay_ub3: assumes "bst t" shows "a_splay a t \ 3 * \ t + 1" +lemma a_splay_ub3: assumes "bst t" shows "a_splay x t \ 3 * \ t + 1" proof cases assume "t = Leaf" thus ?thesis by(simp add: a_splay_def) next assume "t \ Leaf" - from ex_in_set_tree[OF this assms] obtain a' where - a': "a' \ set_tree t" "splay a' t = splay a t" "t_splay a' t = t_splay a t" + from ex_in_set_tree[OF this assms] obtain x' where + a': "x' \ set_tree t" "splay x' t = splay x t" "t_splay x' t = t_splay x t" by blast have [arith]: "log 2 2 > 0" by simp show ?thesis using a_splay_ub2[OF assms a'(1)] by(simp add: a_splay_def a' log_divide) qed subsubsection "Analysis of insert" lemma amor_insert: assumes "bst t" -shows "t_splay a t + \(Splay_Tree.insert a t) - \ t \ 4 * log 2 (size1 t) + 2" (is "?l \ ?r") +shows "t_splay x t + \(Splay_Tree.insert x t) - \ t \ 4 * log 2 (size1 t) + 2" (is "?l \ ?r") proof cases assume "t = Leaf" thus ?thesis by(simp) next assume "t \ Leaf" - then obtain l e r where [simp]: "splay a t = Node l e r" + then obtain l e r where [simp]: "splay x t = Node l e r" by (metis tree.exhaust splay_Leaf_iff) - let ?t = "real(t_splay a t)" + let ?t = "real(t_splay x t)" let ?Plr = "\ l + \ r" let ?Ps = "\ t" let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)" - have opt: "?t + \ (splay a t) - ?Ps \ 3 * log 2 (real (size1 t)) + 1" - using a_splay_ub3[OF \bst t\, simplified a_splay_def, of a] by (simp) - from less_linear[of e a] + have opt: "?t + \ (splay x t) - ?Ps \ 3 * log 2 (real (size1 t)) + 1" + using a_splay_ub3[OF \bst t\, simplified a_splay_def, of x] by (simp) + from less_linear[of e x] show ?thesis proof (elim disjE) - assume "e=a" + assume "e=x" have nneg: "log 2 (1 + real (size t)) \ 0" by simp - thus ?thesis using \t \ Leaf\ opt \e=a\ + thus ?thesis using \t \ Leaf\ opt \e=x\ apply(simp add: algebra_simps) using nneg by arith next let ?L = "log 2 (real(size1 l) + 1)" - assume "e a" by simp + assume "e < x" hence "e \ x" by simp hence "?l = (?t + ?Plr - ?Ps) + ?L + ?LR" - using \t \ Leaf\ \e by(simp) + using \t \ Leaf\ \e by(simp) also have "?t + ?Plr - ?Ps \ 2 * log 2 ?slr + 1" - using opt size_splay[of a t,symmetric] by(simp) + using opt size_splay[of x t,symmetric] by(simp) also have "?L \ log 2 ?slr" by(simp) also have "?LR \ log 2 ?slr + 1" proof - have "?LR \ log 2 (2 * ?slr)" by (simp add:) also have "\ \ log 2 ?slr + 1" by (simp add: log_mult del:distrib_left_numeral) finally show ?thesis . qed - finally show ?thesis using size_splay[of a t,symmetric] by (simp) + finally show ?thesis using size_splay[of x t,symmetric] by (simp) next let ?R = "log 2 (2 + real(size r))" - assume "a a" by simp + assume "x < e" hence "e \ x" by simp hence "?l = (?t + ?Plr - ?Ps) + ?R + ?LR" - using \t \ Leaf\ \a by(simp) + using \t \ Leaf\ \x < e\ by(simp) also have "?t + ?Plr - ?Ps \ 2 * log 2 ?slr + 1" - using opt size_splay[of a t,symmetric] by(simp) + using opt size_splay[of x t,symmetric] by(simp) also have "?R \ log 2 ?slr" by(simp) also have "?LR \ log 2 ?slr + 1" proof - have "?LR \ log 2 (2 * ?slr)" by (simp add:) also have "\ \ log 2 ?slr + 1" by (simp add: log_mult del:distrib_left_numeral) finally show ?thesis . qed - finally show ?thesis using size_splay[of a t, symmetric] by simp + finally show ?thesis using size_splay[of x t, symmetric] by simp qed qed subsubsection "Analysis of delete" definition a_splay_max :: "'a::linorder tree \ real" where "a_splay_max t = t_splay_max t + \(splay_max t) - \ t" lemma a_splay_max_ub: "t \ Leaf \ a_splay_max t \ 3 * (\ t - 1) + 1" proof(induction t rule: splay_max.induct) case 1 thus ?case by (simp) next - case (2 l b) - thus ?case using one_le_log_cancel_iff[of 2 "size1 l + 1"] + case (2 A) + thus ?case using one_le_log_cancel_iff[of 2 "size1 A + 1"] by (simp add: a_splay_max_def del: one_le_log_cancel_iff) next case (3 l b rl c rr) show ?case proof cases assume "rr = Leaf" thus ?thesis using one_le_log_cancel_iff[of 2 "1 + size1 rl"] one_le_log_cancel_iff[of 2 "1 + size1 l + size1 rl"] log_le_cancel_iff[of 2 "size1 l + size1 rl" "1 + size1 l + size1 rl"] by (auto simp: a_splay_max_def field_simps simp del: log_le_cancel_iff one_le_log_cancel_iff) next assume "rr \ Leaf" then obtain l' u r' where sp: "splay_max rr = Node l' u r'" using splay_max_Leaf_iff tree.exhaust by blast hence 1: "size rr = size l' + size r' + 1" using size_splay_max[of rr,symmetric] by(simp) let ?C = "Node rl c rr" let ?B = "Node l b ?C" let ?B' = "Node l b rl" let ?C' = "Node ?B' c l'" have "a_splay_max ?B = a_splay_max rr + \ ?B' + \ ?C' - \ rr - \ ?C + 1" using "3.prems" sp 1 by(auto simp add: a_splay_max_def) also have "\ \ 3 * (\ rr - 1) + \ ?B' + \ ?C' - \ rr - \ ?C + 2" using 3 \rr \ Leaf\ by auto also have "\ = 2 * \ rr + \ ?B' + \ ?C' - \ ?C - 1" by simp also have "\ \ \ rr + \ ?B' + \ ?C' - 1" by simp also have "\ \ 2 * \ ?B + \ ?C' - 2" using ld_ld_1_less[of "size1 ?B'" "size1 rr"] by(simp add:) also have "\ \ 3 * \ ?B - 2" using 1 by simp finally show ?case by simp qed qed lemma a_splay_max_ub3: "a_splay_max t \ 3 * \ t + 1" proof cases assume "t = Leaf" thus ?thesis by(simp add: a_splay_max_def) next assume "t \ Leaf" have [arith]: "log 2 2 > 0" by simp show ?thesis using a_splay_max_ub[OF \t \ Leaf\] by(simp add: a_splay_max_def) qed lemma amor_delete: assumes "bst t" shows "t_delete a t + \(Splay_Tree.delete a t) - \ t \ 6 * log 2 (size1 t) + 2" proof (cases t) case Leaf thus ?thesis by(simp add: Splay_Tree.delete_def t_delete_def) next case [simp]: (Node ls x rs) then obtain l e r where sp[simp]: "splay a (Node ls x rs) = Node l e r" by (metis tree.exhaust splay_Leaf_iff) let ?t = "real(t_splay a t)" let ?Plr = "\ l + \ r" let ?Ps = "\ t" let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)" let ?lslr = "log 2 (real (size ls) + (real (size rs) + 2))" have "?lslr \ 0" by simp have opt: "?t + \ (splay a t) - ?Ps \ 3 * log 2 (real (size1 t)) + 1" using a_splay_ub3[OF \bst t\, simplified a_splay_def, of a] by (simp add: field_simps) show ?thesis proof (cases "e=a") case False thus ?thesis using opt apply(simp add: Splay_Tree.delete_def t_delete_def field_simps) using \?lslr \ 0\ by arith next case [simp]: True show ?thesis proof (cases l) case Leaf have 1: "log 2 (real (size r) + 2) \ 0" by(simp) show ?thesis using Leaf opt apply(simp add: Splay_Tree.delete_def t_delete_def field_simps) using 1 \?lslr \ 0\ by arith next case (Node ll y lr) then obtain l' y' r' where [simp]: "splay_max (Node ll y lr) = Node l' y' r'" using splay_max_Leaf_iff tree.exhaust by blast have "bst l" using bst_splay[OF \bst t\, of a] by simp have "\ r' \ 0" apply (induction r') by (auto) have optm: "real(t_splay_max l) + \ (splay_max l) - \ l \ 3 * \ l + 1" using a_splay_max_ub3[of l, simplified a_splay_max_def] by (simp add: field_simps Node) have 1: "log 2 (2+(real(size l')+real(size r))) \ log 2 (2+(real(size l)+real(size r)))" using size_splay_max[of l] Node by simp have 2: "log 2 (2 + (real (size l') + real (size r'))) \ 0" by simp have 3: "log 2 (size1 l' + size1 r) \ log 2 (size1 l' + size1 r') + log 2 ?slr" apply simp using 1 2 by arith have 4: "log 2 (real(size ll) + (real(size lr) + 2)) \ ?lslr" using size_if_splay[OF sp] Node by simp show ?thesis using add_mono[OF opt optm] Node 3 apply(simp add: Splay_Tree.delete_def t_delete_def field_simps) using 4 \\ r' \ 0\ by arith qed qed qed subsubsection "Overall analysis" fun U where "U Empty [] = 1" | "U (Splay _) [t] = 3 * log 2 (size1 t) + 1" | "U (Insert _) [t] = 4 * log 2 (size1 t) + 2" | "U (Delete _) [t] = 6 * log 2 (size1 t) + 2" interpretation Amortized where arity = arity and exec = exec and inv = bst and cost = cost and \ = \ and U = U proof (standard, goal_cases) case (1 ss f) show ?case proof (cases f) case Empty thus ?thesis using 1 by auto next case (Splay a) then obtain t where "ss = [t]" "bst t" using 1 by auto with Splay bst_splay[OF \bst t\, of a] show ?thesis by (auto split: tree.split) next case (Insert a) then obtain t where "ss = [t]" "bst t" using 1 by auto with bst_splay[OF \bst t\, of a] Insert show ?thesis by (auto simp: splay_bstL[OF \bst t\] splay_bstR[OF \bst t\] split: tree.split) next case (Delete a) then obtain t where "ss = [t]" "bst t" using 1 by auto with 1 Delete show ?thesis by(simp add: bst_delete) qed next case (2 t) thus ?case by (induction t) auto next case (3 ss f) show ?case (is "?l \ ?r") proof(cases f) case Empty thus ?thesis using 3(2) by(simp add: a_splay_def) next case (Splay a) then obtain t where "ss = [t]" "bst t" using 3 by auto thus ?thesis using Splay a_splay_ub3[OF \bst t\] by(simp add: a_splay_def) next case [simp]: (Insert a) then obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto thus ?thesis using amor_insert[of t a] by auto next case [simp]: (Delete a) then obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto thus ?thesis using amor_delete[of t a] by auto qed qed end diff --git a/thys/Amortized_Complexity/Splay_Tree_Analysis_Base.thy b/thys/Amortized_Complexity/Splay_Tree_Analysis_Base.thy --- a/thys/Amortized_Complexity/Splay_Tree_Analysis_Base.thy +++ b/thys/Amortized_Complexity/Splay_Tree_Analysis_Base.thy @@ -1,135 +1,136 @@ section "Splay Tree" subsection "Basics" theory Splay_Tree_Analysis_Base imports Lemmas_log Splay_Tree.Splay_Tree begin declare size1_size[simp] abbreviation "\ t == log 2 (size1 t)" fun \ :: "'a tree \ real" where "\ Leaf = 0" | -"\ (Node l a r) = \ l + \ r + \ (Node l a r)" +"\ (Node l a r) = \ (Node l a r) + \ l + \ r" fun t_splay :: "'a::linorder \ 'a tree \ nat" where "t_splay x Leaf = 1" | "t_splay x (Node AB b CD) = (case cmp x b of EQ \ 1 | LT \ (case AB of Leaf \ 1 | Node A a B \ (case cmp x a of EQ \ 1 | LT \ if A = Leaf then 1 else t_splay x A + 1 | GT \ if B = Leaf then 1 else t_splay x B + 1)) | GT \ (case CD of Leaf \ 1 | Node C c D \ (case cmp x c of EQ \ 1 | LT \ if C = Leaf then 1 else t_splay x C + 1 | GT \ if D = Leaf then 1 else t_splay x D + 1)))" lemma t_splay_simps[simp]: "t_splay a (Node l a r) = 1" - "a t_splay a (Node Leaf b r) = 1" - "a t_splay a (Node (Node ll a lr) b r) = 1" - "a a t_splay a (Node (Node ll c lr) b r) = - (if ll = Leaf then 1 else t_splay a ll + 1)" - "a c t_splay a (Node (Node ll c lr) b r) = - (if lr = Leaf then 1 else t_splay a lr + 1)" - "b t_splay a (Node l b Leaf) = 1" - "b t_splay a (Node l b (Node rl a rr)) = 1" - "b a t_splay a (Node l b (Node rl c rr)) = - (if rl=Leaf then 1 else t_splay a rl + 1)" - "b c t_splay a (Node l b (Node rl c rr)) = - (if rr=Leaf then 1 else t_splay a rr + 1)" + "x t_splay x (Node Leaf b CD) = 1" + "a t_splay a (Node (Node A a B) b CD) = 1" + "x x t_splay x (Node (Node A a B) b CD) = + (if A = Leaf then 1 else t_splay x A + 1)" + "x a t_splay x (Node (Node A a B) b CD) = + (if B = Leaf then 1 else t_splay x B + 1)" + "b t_splay x (Node AB b Leaf) = 1" + "b t_splay a (Node AB b (Node C a D)) = 1" + "b x t_splay x (Node AB b (Node C c D)) = + (if C=Leaf then 1 else t_splay x C + 1)" + "b c t_splay x (Node AB b (Node C c D)) = + (if D=Leaf then 1 else t_splay x D + 1)" by auto declare t_splay.simps(2)[simp del] fun t_splay_max :: "'a::linorder tree \ nat" where "t_splay_max Leaf = 1" | -"t_splay_max (Node l b Leaf) = 1" | -"t_splay_max (Node l b (Node rl c rr)) = (if rr=Leaf then 1 else t_splay_max rr + 1)" +"t_splay_max (Node A a Leaf) = 1" | +"t_splay_max (Node A a (Node B b C)) = (if C=Leaf then 1 else t_splay_max C + 1)" definition t_delete :: "'a::linorder \ 'a tree \ nat" where -"t_delete a t = (if t = Leaf then 0 else t_splay a t + (case splay a t of - Node l x r \ - if x=a then case l of Leaf \ 0 | _ \ t_splay_max l - else 0))" +"t_delete x t = + (if t = Leaf then 0 + else t_splay x t + + (case splay x t of + Node l a r \ if x=a then case l of Leaf \ 0 | _ \ t_splay_max l else 0))" lemma ex_in_set_tree: "t \ Leaf \ bst t \ - \a' \ set_tree t. splay a' t = splay a t \ t_splay a' t = t_splay a t" -proof(induction a t rule: splay.induct) - case (6 a b c ll) - hence "splay a ll \ Leaf" by simp - then obtain lll u llr where [simp]: "splay a ll = Node lll u llr" + \x' \ set_tree t. splay x' t = splay x t \ t_splay x' t = t_splay x t" +proof(induction x t rule: splay.induct) + case (6 x b c A) + hence "splay x A \ Leaf" by simp + then obtain A1 u A2 where [simp]: "splay x A = Node A1 u A2" by (metis tree.exhaust) - have "b < c" "bst ll" using "6.prems" by auto - from "6.IH"[OF \ll \ Leaf\ \bst ll\] - obtain e where "e \ set_tree ll" "splay e ll = splay a ll" "t_splay e ll = t_splay a ll" - by blast - moreover hence "ea \a \b \bst ll\ by force -next - case (8 b a c lr) - hence "splay a lr \ Leaf" by simp - then obtain lrl u lrr where [simp]: "splay a lr = Node lrl u lrr" - by (metis tree.exhaust) - have "b < c" "bst lr" using "8.prems" by auto - from "8.IH"[OF \lr \ Leaf\ \bst lr\] - obtain e where "e \ set_tree lr" "splay e lr = splay a lr" "t_splay e lr = t_splay a lr" + have "b < c" "bst A" using "6.prems" by auto + from "6.IH"[OF \A \ Leaf\ \bst A\] + obtain x' where "x' \ set_tree A" "splay x' A = splay x A" "t_splay x' A = t_splay x A" by blast - moreover hence "ba \b \b \bst lr\ by force + moreover hence "x'x \x \b \bst A\ by force next - case (11 c a b rl) - hence "splay a rl \ Leaf" by simp - then obtain rll u rlr where [simp]: "splay a rl = Node rll u rlr" + case (8 a x c B) + hence "splay x B \ Leaf" by simp + then obtain B1 u B2 where [simp]: "splay x B = Node B1 u B2" by (metis tree.exhaust) - have "c < b" "bst rl" using "11.prems" by auto - from "11.IH"[OF \rl \ Leaf\ \bst rl\] - obtain e where "e \ set_tree rl" "splay e rl = splay a rl" "t_splay e rl = t_splay a rl" + have "a < c" "bst B" using "8.prems" by auto + from "8.IH"[OF \B \ Leaf\ \bst B\] + obtain x' where "x' \ set_tree B" "splay x' B = splay x B" "t_splay x' B = t_splay x B" by blast - moreover hence "cc \a \c \bst rl\ by force + moreover hence "ax \a \a \bst B\ by force next - case (14 c a b rr) - hence "splay a rr \ Leaf" by simp - then obtain rrl u rrr where [simp]: "splay a rr = Node rrl u rrr" + case (11 b x c C) + hence "splay x C \ Leaf" by simp + then obtain C1 u C2 where [simp]: "splay x C = Node C1 u C2" by (metis tree.exhaust) - have "c < b" "bst rr" using "14.prems" by auto - from "14.IH"[OF \rr \ Leaf\ \bst rr\] - obtain e where "e \ set_tree rr" "splay e rr = splay a rr" "t_splay e rr = t_splay a rr" + have "b < c" "bst C" using "11.prems" by auto + from "11.IH"[OF \C \ Leaf\ \bst C\] + obtain x' where "x' \ set_tree C" "splay x' C = splay x C" "t_splay x' C = t_splay x C" by blast - moreover hence "bc \b \c \bst rr\ by force + moreover hence "bb \x \b \bst C\ by force +next + case (14 a x c D) + hence "splay x D \ Leaf" by simp + then obtain D1 u D2 where [simp]: "splay x D = Node D1 u D2" + by (metis tree.exhaust) + have "a < c" "bst D" using "14.prems" by auto + from "14.IH"[OF \D \ Leaf\ \bst D\] + obtain x' where "x' \ set_tree D" "splay x' D = splay x D" "t_splay x' D = t_splay x D" + by blast + moreover hence "ca \c \a \bst D\ by force qed (auto simp: le_less) datatype 'a op = Empty | Splay 'a | Insert 'a | Delete 'a fun arity :: "'a::linorder op \ nat" where "arity Empty = 0" | -"arity (Splay a) = 1" | -"arity (Insert a) = 1" | -"arity (Delete a) = 1" +"arity (Splay x) = 1" | +"arity (Insert x) = 1" | +"arity (Delete x) = 1" fun exec :: "'a::linorder op \ 'a tree list \ 'a tree" where "exec Empty [] = Leaf" | -"exec (Splay a) [t] = splay a t" | -"exec (Insert a) [t] = Splay_Tree.insert a t" | -"exec (Delete a) [t] = Splay_Tree.delete a t" +"exec (Splay x) [t] = splay x t" | +"exec (Insert x) [t] = Splay_Tree.insert x t" | +"exec (Delete x) [t] = Splay_Tree.delete x t" fun cost :: "'a::linorder op \ 'a tree list \ nat" where "cost Empty [] = 1" | -"cost (Splay a) [t] = t_splay a t" | -"cost (Insert a) [t] = t_splay a t" | -"cost (Delete a) [t] = t_delete a t" +"cost (Splay x) [t] = t_splay x t" | +"cost (Insert x) [t] = t_splay x t" | +"cost (Delete x) [t] = t_delete x t" end diff --git a/thys/Splay_Tree/Splay_Tree.thy b/thys/Splay_Tree/Splay_Tree.thy --- a/thys/Splay_Tree/Splay_Tree.thy +++ b/thys/Splay_Tree/Splay_Tree.thy @@ -1,426 +1,447 @@ section "Splay Tree" theory Splay_Tree imports "HOL-Library.Tree" "HOL-Data_Structures.Set_Specs" "HOL-Data_Structures.Cmp" begin declare sorted_wrt.simps(2)[simp del] text\Splay trees were invented by Sleator and Tarjan~\cite{SleatorT-JACM85}.\ subsection "Function \splay\" function splay :: "'a::linorder \ 'a tree \ 'a tree" where "splay x Leaf = Leaf" | -"splay x (Node A x B) = Node A x B" | -"x splay x (Node (Node A x B) b C) = Node A x (Node B b C)" | -"x splay x (Node Leaf b A) = Node Leaf b A" | -"x x splay x (Node (Node Leaf a A) b B) = Node Leaf a (Node A b B)" | -"x x AB \ Leaf \ - splay x (Node (Node AB b C) c D) = - (case splay x AB of Node A a B \ Node A a (Node B b (Node C c D)))" | -"a x splay x (Node (Node A a Leaf) b B) = Node A a (Node Leaf b B)" | -"a x BC \ Leaf \ - splay x (Node (Node A a BC) c D) = - (case splay x BC of Node B b C \ Node (Node A a B) b (Node C c D))" | -"a splay x (Node A a (Node B x C)) = Node (Node A a B) x C" | -"a splay x (Node A a Leaf) = Node A a Leaf" | -"a x BC \ Leaf \ - splay x (Node A a (Node BC c D)) = - (case splay x BC of Node B b C \ Node (Node A a B) b (Node C c D))" | -"a x splay x (Node A a (Node Leaf b C)) = Node (Node A a Leaf) b C" | -"a b splay x (Node A a (Node B b Leaf)) = Node (Node A a B) b Leaf" | -"a b CD \ Leaf \ - splay x (Node A a (Node B b CD)) = - (case splay x CD of Node C c D \ Node (Node (Node A a B) b C) c D)" +"splay x (Node AB x CD) = Node AB x CD" | +"x splay x (Node (Node A x B) b CD) = Node A x (Node B b CD)" | +"x splay x (Node Leaf b CD) = Node Leaf b CD" | +"x x splay x (Node (Node Leaf a B) b CD) = Node Leaf a (Node B b CD)" | +"x x A \ Leaf \ + splay x (Node (Node A a B) b CD) = + (case splay x A of Node A1 a' A2 \ Node A1 a' (Node A2 a (Node B b CD)))" | +"a x splay x (Node (Node A a Leaf) b CD) = Node A a (Node Leaf b CD)" | +"a x B \ Leaf \ + splay x (Node (Node A a B) b CD) = + (case splay x B of Node B1 b' B2 \ Node (Node A a B1) b' (Node B2 b CD))" | +"b splay x (Node AB b (Node C x D)) = Node (Node AB b C) x D" | +"b splay x (Node AB b Leaf) = Node AB b Leaf" | +"b x C \ Leaf \ + splay x (Node AB b (Node C c D)) = + (case splay x C of Node C1 c' C \ Node (Node AB b C1) c' (Node C c D))" | +"b x splay x (Node AB b (Node Leaf c D)) = Node (Node AB b Leaf) c D" | +"b c splay x (Node AB b (Node C c Leaf)) = Node (Node AB b C) c Leaf" | +"a c D \ Leaf \ + splay x (Node AB a (Node C c D)) = + (case splay x D of Node D1 d' D2 \ Node (Node (Node AB a C) c D1) d' D2)" apply(atomize_elim) apply(auto) (* 1 subgoal *) apply (subst (asm) neq_Leaf_iff) apply(auto) apply (metis tree.exhaust le_less_linear less_linear)+ done termination splay by lexicographic_order lemma splay_code: "splay x (Node AB b CD) = (case cmp x b of EQ \ Node AB b CD | LT \ (case AB of Leaf \ Node AB b CD | Node A a B \ (case cmp x a of EQ \ Node A a (Node B b CD) | LT \ if A = Leaf then Node A a (Node B b CD) else case splay x A of Node A\<^sub>1 a' A\<^sub>2 \ Node A\<^sub>1 a' (Node A\<^sub>2 a (Node B b CD)) | GT \ if B = Leaf then Node A a (Node B b CD) else case splay x B of Node B\<^sub>1 b' B\<^sub>2 \ Node (Node A a B\<^sub>1) b' (Node B\<^sub>2 b CD))) | GT \ (case CD of Leaf \ Node AB b CD | Node C c D \ (case cmp x c of EQ \ Node (Node AB b C) c D | LT \ if C = Leaf then Node (Node AB b C) c D else case splay x C of Node C\<^sub>1 c' C\<^sub>2 \ Node (Node AB b C\<^sub>1) c' (Node C\<^sub>2 c D) | GT \ if D=Leaf then Node (Node AB b C) c D else case splay x D of Node D\<^sub>1 d D\<^sub>2 \ Node (Node (Node AB b C) c D\<^sub>1) d D\<^sub>2)))" by(auto split!: tree.split) definition is_root :: "'a \ 'a tree \ bool" where "is_root x t = (case t of Leaf \ False | Node l a r \ x = a)" definition "isin t x = is_root x (splay x t)" definition empty :: "'a tree" where "empty = Leaf" hide_const (open) insert fun insert :: "'a::linorder \ 'a tree \ 'a tree" where "insert x t = (if t = Leaf then Node Leaf x Leaf else case splay x t of Node l a r \ case cmp x a of EQ \ Node l a r | LT \ Node l x (Node Leaf a r) | GT \ Node (Node l a Leaf) x r)" fun splay_max :: "'a tree \ 'a tree" where "splay_max Leaf = Leaf" | "splay_max (Node A a Leaf) = Node A a Leaf" | "splay_max (Node A a (Node B b CD)) = (if CD = Leaf then Node (Node A a B) b Leaf else case splay_max CD of Node C c D \ Node (Node (Node A a B) b C) c D)" lemma splay_max_code: "splay_max t = (case t of Leaf \ t | Node la a ra \ (case ra of Leaf \ t | Node lb b rb \ (if rb=Leaf then Node (Node la a lb) b rb else case splay_max rb of Node lc c rc \ Node (Node (Node la a lb) b lc) c rc)))" by(auto simp: neq_Leaf_iff split: tree.split) definition delete :: "'a::linorder \ 'a tree \ 'a tree" where "delete x t = (if t = Leaf then Leaf else case splay x t of Node l a r \ if x \ a then Node l a r else if l = Leaf then r else case splay_max l of Node l' m r' \ Node l' m r)" subsection "Functional Correctness Proofs I" text \This subsection follows the automated method by Nipkow \cite{Nipkow-ITP16}.\ lemma splay_Leaf_iff[simp]: "(splay a t = Leaf) = (t = Leaf)" by(induction a t rule: splay.induct) (auto split: tree.splits) lemma splay_max_Leaf_iff[simp]: "(splay_max t = Leaf) = (t = Leaf)" by(induction t rule: splay_max.induct)(auto split: tree.splits) subsubsection "Verification of @{const isin}" lemma splay_elemsD: "splay x t = Node l a r \ sorted(inorder t) \ x \ set (inorder t) \ x=a" by(induction x t arbitrary: l a r rule: splay.induct) (auto simp: isin_simps ball_Un split: tree.splits) lemma isin_set: "sorted(inorder t) \ isin t x = (x \ set (inorder t))" by (auto simp: isin_def is_root_def dest: splay_elemsD split: tree.splits) subsubsection "Verification of @{const insert}" lemma inorder_splay: "inorder(splay x t) = inorder t" by(induction x t rule: splay.induct) (auto simp: neq_Leaf_iff split: tree.split) lemma sorted_splay: "sorted(inorder t) \ splay x t = Node l a r \ sorted(inorder l @ x # inorder r)" unfolding inorder_splay[of x t, symmetric] by(induction x t arbitrary: l a r rule: splay.induct) (auto simp: sorted_lems sorted_Cons_le sorted_snoc_le split: tree.splits) lemma inorder_insert: "sorted(inorder t) \ inorder(insert x t) = ins_list x (inorder t)" using inorder_splay[of x t, symmetric] sorted_splay[of t x] by(auto simp: ins_list_simps ins_list_Cons ins_list_snoc neq_Leaf_iff split: tree.split) subsubsection "Verification of @{const delete}" lemma inorder_splay_maxD: "splay_max t = Node l a r \ sorted(inorder t) \ inorder l @ [a] = inorder t \ r = Leaf" by(induction t arbitrary: l a r rule: splay_max.induct) (auto simp: sorted_lems split: tree.splits if_splits) lemma inorder_delete: "sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" using inorder_splay[of x t, symmetric] sorted_splay[of t x] by (auto simp: del_list_simps del_list_sorted_app delete_def del_list_notin_Cons inorder_splay_maxD split: tree.splits) subsubsection "Overall Correctness" interpretation splay: Set_by_Ordered where empty = empty and isin = isin and insert = insert and delete = delete and inorder = inorder and inv = "\_. True" proof (standard, goal_cases) case 2 thus ?case by(simp add: isin_set) next case 3 thus ?case by(simp add: inorder_insert del: insert.simps) next case 4 thus ?case by(simp add: inorder_delete) qed (auto simp: empty_def) +text \Corollaries:\ -subsection "Functional Correctness Proofs II" +lemma bst_splay: "bst t \ bst (splay x t)" +by (simp add: bst_iff_sorted_wrt_less inorder_splay) -text \This subsection follows the traditional approach, is less automated -and is retained more for historic reasons.\ +lemma bst_insert: "bst t \ bst(insert x t)" +using splay.invar_insert[of t x] by (simp add: bst_iff_sorted_wrt_less splay.invar_def) + +lemma bst_delete: "bst t \ bst(delete x t)" +using splay.invar_delete[of t x] by (simp add: bst_iff_sorted_wrt_less splay.invar_def) + +lemma splay_bstL: "bst t \ splay a t = Node l e r \ x \ set_tree l \ x < a" +by (metis bst_iff_sorted_wrt_less list.set_intros(1) set_inorder sorted_splay sorted_wrt_append) + +lemma splay_bstR: "bst t \ splay a t = Node l e r \ x \ set_tree r \ a < x" +by (metis bst_iff_sorted_wrt_less sorted_Cons_iff set_inorder sorted_splay sorted_wrt_append) + + +subsubsection "Size lemmas" lemma size_splay[simp]: "size (splay a t) = size t" apply(induction a t rule: splay.induct) apply auto apply(force split: tree.split)+ done lemma size_if_splay: "splay a t = Node l u r \ size t = size l + size r + 1" by (metis One_nat_def size_splay tree.size(4)) lemma splay_not_Leaf: "t \ Leaf \ \l x r. splay a t = Node l x r" by (metis neq_Leaf_iff splay_Leaf_iff) +lemma size_splay_max: "size(splay_max t) = size t" +apply(induction t rule: splay_max.induct) + apply(simp) + apply(simp) +apply(clarsimp split: tree.split) +done + +lemma size_if_splay_max: "splay_max t = Node l u r \ size t = size l + size r + 1" +by (metis One_nat_def size_splay_max tree.size(4)) + +(* +subsection "Functional Correctness Proofs II" + +text \This subsection follows the traditional approach, is less automated +and is retained more for historic reasons.\ + lemma set_splay: "set_tree(splay a t) = set_tree t" proof(induction a t rule: splay.induct) case (6 a) with splay_not_Leaf[OF 6(3), of a] show ?case by(fastforce) next case (8 _ a) with splay_not_Leaf[OF 8(3), of a] show ?case by(fastforce) next case (11 _ a) with splay_not_Leaf[OF 11(3), of a] show ?case by(fastforce) next case (14 _ a) with splay_not_Leaf[OF 14(3), of a] show ?case by(fastforce) qed auto lemma splay_bstL: "bst t \ splay a t = Node l e r \ x \ set_tree l \ x < a" apply(induction a t arbitrary: l x r rule: splay.induct) apply (auto split: tree.splits) apply auto done lemma splay_bstR: "bst t \ splay a t = Node l e r \ x \ set_tree r \ a < x" apply(induction a t arbitrary: l e x r rule: splay.induct) apply auto apply (fastforce split!: tree.splits)+ done lemma bst_splay: "bst t \ bst(splay a t)" proof(induction a t rule: splay.induct) case (6 a _ _ ll) with splay_not_Leaf[OF 6(3), of a] set_splay[of a ll,symmetric] show ?case by (fastforce) next case (8 _ a _ t) with splay_not_Leaf[OF 8(3), of a] set_splay[of a t,symmetric] show ?case by fastforce next case (11 _ a _ t) with splay_not_Leaf[OF 11(3), of a] set_splay[of a t,symmetric] show ?case by fastforce next case (14 _ a _ t) with splay_not_Leaf[OF 14(3), of a] set_splay[of a t,symmetric] show ?case by fastforce qed auto lemma splay_to_root: "\ bst t; splay a t = t' \ \ a \ set_tree t \ (\l r. t' = Node l a r)" proof(induction a t arbitrary: t' rule: splay.induct) case (6 a) with splay_not_Leaf[OF 6(3), of a] show ?case by auto next case (8 _ a) with splay_not_Leaf[OF 8(3), of a] show ?case by auto next case (11 _ a) with splay_not_Leaf[OF 11(3), of a] show ?case by auto next case (14 _ a) with splay_not_Leaf[OF 14(3), of a] show ?case by auto qed fastforce+ subsubsection "Verification of Is-in Test" text\To test if an element \a\ is in \t\, first perform @{term"splay a t"}, then check if the root is \a\. One could put this into one function that returns both a new tree and the test result.\ lemma is_root_splay: "bst t \ is_root a (splay a t) \ a \ set_tree t" by(auto simp add: is_root_def splay_to_root split: tree.split) subsubsection "Verification of @{const insert}" lemma set_insert: "set_tree(insert a t) = Set.insert a (set_tree t)" apply(cases t) apply simp using set_splay[of a t] by(simp split: tree.split) fastforce lemma bst_insert: "bst t \ bst(insert a t)" apply(cases t) apply simp using bst_splay[of t a] splay_bstL[of t a] splay_bstR[of t a] by(auto simp: ball_Un split: tree.split) subsubsection "Verification of \splay_max\" -lemma size_splay_max: "size(splay_max t) = size t" -apply(induction t rule: splay_max.induct) - apply(simp) - apply(simp) -apply(clarsimp split: tree.split) -done - -lemma size_if_splay_max: "splay_max t = Node l u r \ size t = size l + size r + 1" -by (metis One_nat_def size_splay_max tree.size(4)) - lemma set_splay_max: "set_tree(splay_max t) = set_tree t" apply(induction t rule: splay_max.induct) apply(simp) apply(simp) apply(force split: tree.split) done lemma bst_splay_max: "bst t \ bst (splay_max t)" proof(induction t rule: splay_max.induct) case (3 l b rl c rr) { fix rrl' d' rrr' have "splay_max rr = Node rrl' d' rrr' \ \x \ set_tree(Node rrl' d' rrr'). c < x" using "3.prems" set_splay_max[of rr] by (clarsimp split: tree.split simp: ball_Un) } with 3 show ?case by (fastforce split: tree.split simp: ball_Un) qed auto lemma splay_max_Leaf: "splay_max t = Node l a r \ r = Leaf" by(induction t arbitrary: l rule: splay_max.induct) (auto split: tree.splits if_splits) text\For sanity purposes only:\ lemma splay_max_eq_splay: "bst t \ \x \ set_tree t. x \ a \ splay_max t = splay a t" proof(induction a t rule: splay.induct) case (2 a l r) show ?case proof (cases r) case Leaf with 2 show ?thesis by simp next case Node with 2 show ?thesis by(auto) qed qed (auto simp: neq_Leaf_iff) lemma splay_max_eq_splay_ex: assumes "bst t" shows "\a. splay_max t = splay a t" proof(cases t) case Leaf thus ?thesis by simp next case Node hence "splay_max t = splay (Max(set_tree t)) t" using assms by (auto simp: splay_max_eq_splay) thus ?thesis by auto qed subsubsection "Verification of @{const delete}" lemma set_delete: assumes "bst t" shows "set_tree (delete a t) = set_tree t - {a}" proof(cases t) case Leaf thus ?thesis by(simp add: delete_def) next case (Node l x r) obtain l' x' r' where sp[simp]: "splay a (Node l x r) = Node l' x' r'" by (metis neq_Leaf_iff splay_Leaf_iff) show ?thesis proof cases assume [simp]: "x' = a" show ?thesis proof cases assume "l' = Leaf" thus ?thesis using Node assms set_splay[of a "Node l x r"] bst_splay[of "Node l x r" a] by(simp add: delete_def split: tree.split prod.split)(fastforce) next assume "l' \ Leaf" moreover then obtain l'' m r'' where "splay_max l' = Node l'' m r''" using splay_max_Leaf_iff tree.exhaust by blast moreover have "a \ set_tree l'" by (metis (no_types) Node assms less_irrefl sp splay_bstL) ultimately show ?thesis using Node assms set_splay[of a "Node l x r"] bst_splay[of "Node l x r" a] splay_max_Leaf[of l' l'' m r''] set_splay_max[of l'] by(clarsimp simp: delete_def split: tree.split) auto qed next assume "x' \ a" thus ?thesis using Node assms set_splay[of a "Node l x r"] splay_to_root[OF _ sp] by (simp add: delete_def) qed qed lemma bst_delete: assumes "bst t" shows "bst (delete a t)" proof(cases t) case Leaf thus ?thesis by(simp add: delete_def) next case (Node l x r) obtain l' x' r' where sp[simp]: "splay a (Node l x r) = Node l' x' r'" by (metis neq_Leaf_iff splay_Leaf_iff) show ?thesis proof cases assume [simp]: "x' = a" show ?thesis proof cases assume "l' = Leaf" thus ?thesis using Node assms bst_splay[of "Node l x r" a] by(simp add: delete_def split: tree.split prod.split) next assume "l' \ Leaf" thus ?thesis using Node assms set_splay[of a "Node l x r"] bst_splay[of "Node l x r" a] bst_splay_max[of l'] set_splay_max[of l'] by(clarsimp simp: delete_def split: tree.split) (metis (no_types) insertI1 less_trans) qed next assume "x' \ a" thus ?thesis using Node assms bst_splay[of "Node l x r" a] by(auto simp: delete_def split: tree.split prod.split) qed qed +*) end