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,416 +1,416 @@
 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 \<Rightarrow> 'a tree \<Rightarrow> real" where
 "A_splay a t = T_splay a t + \<Phi>(splay a t) - \<Phi> t"
 
 text\<open>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.\<close>
 
 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 \<noteq> \<langle>\<rangle>" and IH: "T_splay x lb + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb \<le> 2 * \<phi> lb - 3 * \<phi> X + 1" and
  prems: "size lb = size lb1 + size lb2 + 1" "X \<in> subtrees lb"
 shows "T_splay x lb + \<Phi> t' - \<Phi> t \<le> 3 * (\<phi> t - \<phi> X)"
 proof -
   define B' where [simp]: "B' = Node lb2 b A'"
   have "T_splay x lb + \<Phi> t' - \<Phi> t = T_splay x lb + \<Phi> lb1 + \<Phi> lb2 - \<Phi> lb + \<phi> B' + \<phi> A' - \<phi> B"
     using prems
     by(auto simp: A_splay_def size_if_splay algebra_simps in_set_tree_if split: tree.split)
   also have "\<dots> \<le> 2 * \<phi> lb + \<phi> B' + \<phi> A' - \<phi> B - 3 * \<phi> X + 1"
     using IH prems(2) by(auto simp: algebra_simps)
   also have "\<dots> \<le> \<phi> lb + \<phi> B' + \<phi> A' - 3 * \<phi> X + 1" by(simp)
   also have "\<dots> \<le> \<phi> B' + 2 * \<phi> t - 3 * \<phi> X "
     using prems ld_ld_1_less[of "size1 lb" "size1 A'"]
     by(simp add: size_if_splay)
   also have "\<dots> \<le> 3 * \<phi> t - 3 * \<phi> X"
     using prems by(simp add: size_if_splay)
   finally show ?thesis by simp
 qed
 
 lemma A_splay_ub: "\<lbrakk> bst t; Node l x r : subtrees t \<rbrakk>
   \<Longrightarrow> A_splay x t \<le> 3 * (\<phi> t - \<phi>(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 simp: A_splay_def)
 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 CD)
   (* A readable proof *)
   let ?t = "\<langle>\<langle>A, x, B\<rangle>, b, CD\<rangle>"
   let ?t' = "\<langle>A, x, \<langle>B, b, CD\<rangle>\<rangle>"
   have *: "l = A \<and> r = B" using "3.prems" by(fastforce dest: in_set_tree_if)
   have "A_splay x ?t = 1 + \<Phi> ?t' - \<Phi> ?t" using "3.hyps" by (simp add: A_splay_def)
   also have "\<dots> = 1 + \<phi> ?t' + \<phi> \<langle>B, b, CD\<rangle>  - \<phi> ?t - \<phi> \<langle>A, x, B\<rangle>" by(simp)
   also have "\<dots> = 1 + \<phi> \<langle>B, b, CD\<rangle> - \<phi> \<langle>A, x, B\<rangle>" by(simp)
   also have "\<dots> \<le>  1 + \<phi> ?t - \<phi>(Node A x B)"
     using log_le_cancel_iff[of 2 "size1(Node B b CD)" "size1 ?t"] by (simp)
   also have "\<dots> \<le> 1 + 3 * (\<phi> ?t - \<phi>(Node A x B))"
     using log_le_cancel_iff[of 2 "size1(Node A x B)" "size1 ?t"] by (simp)
   finally show ?case using * by simp
 next
   case (9 b x AB C D)
   (* An automatic proof *)
   let ?A = "\<langle>AB, b, \<langle>C, x, D\<rangle>\<rangle>"
   have "x \<notin> set_tree AB" using "9.prems"(1) by auto
   with 9 show ?case using
     log_le_cancel_iff[of 2 "size1(Node AB b C)" "size1 ?A"]
     log_le_cancel_iff[of 2 "size1(Node C x D)" "size1 ?A"]
     by (auto simp: A_splay_def algebra_simps simp del:log_le_cancel_iff)
 next
   case (6 x a b A B C)
   hence *: "\<langle>l, x, r\<rangle> \<in> subtrees A" by(fastforce dest: in_set_tree_if)
   obtain A1 a' A2 where sp: "splay x A = Node A1 a' A2"
     using splay_not_Leaf[OF \<open>A \<noteq> Leaf\<close>] by blast
   let ?X = "Node l x r" let ?AB = "Node A a B"  let ?ABC = "Node ?AB b C"
   let ?A' = "Node A1 a' A2"
   let ?BC = "Node B b C"  let ?A2BC = "Node A2 a ?BC"
   have "A_splay x ?ABC = A_splay x A + \<phi> ?A2BC + \<phi> ?BC - \<phi> ?AB - \<phi> ?A' + 1"
     using "6.hyps" sp
     by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
   also have "\<dots> \<le> 3 * \<phi> A + \<phi> ?A2BC + \<phi> ?BC - \<phi> ?AB - \<phi> ?A' - 3 * \<phi> ?X + 2"
     using "6.IH" "6.prems"(1) * by(auto simp: algebra_simps)
   also have "\<dots> = 2 * \<phi> A + \<phi> ?A2BC + \<phi> ?BC - \<phi> ?AB - 3 * \<phi> ?X + 2"
     using sp by(simp add: size_if_splay)
   also have "\<dots> < \<phi> A + \<phi> ?A2BC + \<phi> ?BC - 3 * \<phi> ?X + 2" by(simp)
   also have "\<dots> < \<phi> ?A2BC + 2 * \<phi> ?ABC - 3 * \<phi> ?X + 1"
     using sp ld_ld_1_less[of "size1 A" "size1 ?BC"]
     by(simp add: size_if_splay)
   also have "\<dots> < 3 * \<phi> ?ABC - 3 * \<phi> ?X + 1"
     using sp by(simp add: size_if_splay)
   finally show ?case by simp
 next
   case (8 a x b B A C)
   hence *: "\<langle>l, x, r\<rangle> \<in> subtrees B" by(fastforce dest: in_set_tree_if)
   obtain B1 b' B2 where sp: "splay x B = Node B1 b' B2"
      using splay_not_Leaf[OF \<open>B \<noteq> Leaf\<close>] by blast
   let ?X = "Node l x r" let ?AB = "Node A a B"  let ?ABC = "Node ?AB b C"
   let ?B' = "Node B1 b' B2"
   let ?AB1 = "Node A a B1"  let ?B2C = "Node B2 b C"
   have "A_splay x ?ABC = A_splay x B + \<phi> ?AB1 + \<phi> ?B2C - \<phi> ?AB - \<phi> ?B' + 1"
     using "8.hyps" sp
     by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
   also have "\<dots> \<le> 3 * \<phi> B + \<phi> ?AB1 + \<phi> ?B2C - \<phi> ?AB - \<phi> ?B' - 3 * \<phi> ?X + 2"
     using "8.IH" "8.prems"(1) * by(auto simp: algebra_simps)
   also have "\<dots> = 2 * \<phi> B + \<phi> ?AB1 + \<phi> ?B2C - \<phi> ?AB - 3 * \<phi> ?X + 2"
     using sp by(simp add: size_if_splay)
   also have "\<dots> < \<phi> B + \<phi> ?AB1 + \<phi> ?B2C - 3 * \<phi> ?X + 2" by(simp)
   also have "\<dots> < \<phi> B + 2 * \<phi> ?ABC - 3 * \<phi> ?X + 1"
     using sp ld_ld_1_less[of "size1 ?AB1" "size1 ?B2C"]
     by(simp add: size_if_splay)
   also have "\<dots> < 3 * \<phi> ?ABC - 3 * \<phi> ?X + 1" by(simp)
   finally show ?case by simp
 next
   case (11 b x c C A D)
   hence *: "\<langle>l, x, r\<rangle> \<in> subtrees C" by(fastforce dest: in_set_tree_if)
   obtain C1 c' C2 where sp: "splay x C = Node C1 c' C2"
     using splay_not_Leaf[OF \<open>C \<noteq> Leaf\<close>] by blast
   let ?X = "Node l x r" let ?CD = "Node C c D"  let ?ACD = "Node A b ?CD"
   let ?C' = "Node C1 c' C2"
   let ?C2D = "Node C2 c D"  let ?AC1 = "Node A b C1"
   have "A_splay x ?ACD = A_splay x C + \<phi> ?C2D + \<phi> ?AC1 - \<phi> ?CD - \<phi> ?C' + 1"
     using "11.hyps" sp
     by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
   also have "\<dots> \<le> 3 * \<phi> C + \<phi> ?C2D + \<phi> ?AC1 - \<phi> ?CD - \<phi> ?C' - 3 * \<phi> ?X + 2"
     using "11.IH" "11.prems"(1) * by(auto simp: algebra_simps)
   also have "\<dots> = 2 * \<phi> C + \<phi> ?C2D + \<phi> ?AC1 - \<phi> ?CD - 3 * \<phi> ?X + 2"
     using sp by(simp add: size_if_splay)
   also have "\<dots> \<le> \<phi> C + \<phi> ?C2D + \<phi> ?AC1 - 3 * \<phi> ?X + 2" by(simp)
   also have "\<dots> \<le> \<phi> C + 2 * \<phi> ?ACD - 3 * \<phi> ?X + 1"
     using sp ld_ld_1_less[of "size1 ?C2D" "size1 ?AC1"]
     by(simp add: size_if_splay algebra_simps)
   also have "\<dots> \<le> 3 * \<phi> ?ACD - 3 * \<phi> ?X + 1" by(simp)
   finally show ?case by simp
 next
   case (14 a x b CD A B)
   hence 0: "x \<notin> set_tree B \<and> x \<notin> set_tree A"
     using "14.prems"(1) \<open>b<x\<close> by(auto)
   hence 1: "x \<in> set_tree CD" using "14.prems" \<open>b<x\<close> \<open>a<x\<close> by (auto)
   obtain C c D where sp: "splay x CD = Node C c D"
     using splay_not_Leaf[OF \<open>CD \<noteq> Leaf\<close>] 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 + \<phi> ?B' + \<phi> ?A' - \<phi> ?B - \<phi> ?R' + 1"
     using "14.prems" 1 sp
     by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
   also have "\<dots> \<le> 3 * \<phi> ?R + \<phi> ?B' + \<phi> ?A' - \<phi> ?B - \<phi> ?R' - 3 * \<phi> ?X + 2"
     using 14 0 by(auto simp: algebra_simps)
   also have "\<dots> = 2 * \<phi> rb + \<phi> ?B' + \<phi> ?A' - \<phi> ?B - 3 * \<phi> ?X + 2"
     using sp by(simp add: size_if_splay)
   also have "\<dots> \<le> \<phi> ?R + \<phi> ?B' + \<phi> ?A' - 3 * \<phi> ?X + 2" by(simp)
   also have "\<dots> \<le> \<phi> ?B' + 2 * \<phi> ?A - 3 * \<phi> ?X + 1"
     using sp ld_ld_1_less[of "size1 ?R" "size1 ?A'"]
     by(simp add: size_if_splay algebra_simps)
   also have "\<dots> \<le> 3 * \<phi> ?A - 3 * \<phi> ?X + 1"
     using sp by(simp add: size_if_splay)
   finally show ?case by simp
 *)
 qed
 
 lemma A_splay_ub2: assumes "bst t" "x : set_tree t"
 shows "A_splay x t \<le> 3 * (\<phi> t - 1) + 1"
 proof -
   from assms(2) obtain l r where N: "Node l x r : subtrees t"
     by (metis set_treeE)
   have "A_splay x t \<le> 3 * (\<phi> t - \<phi>(Node l x r)) + 1" by(rule A_splay_ub[OF assms(1) N])
   also have "\<dots> \<le> 3 * (\<phi> t - 1) + 1" by(simp add: field_simps)
   finally show ?thesis .
 qed
 
 lemma A_splay_ub3: assumes "bst t" shows "A_splay x t \<le> 3 * \<phi> t + 1"
 proof cases
   assume "t = Leaf" thus ?thesis by(simp add: A_splay_def)
 next
   assume "t \<noteq> Leaf"
   from ex_in_set_tree[OF this assms] obtain x' where
     a': "x' \<in> set_tree t"  "splay x' t = splay x t"  "T_splay x' t = T_splay x t"
     by blast
   show ?thesis using A_splay_ub2[OF assms a'(1)] by(simp add: A_splay_def a')
 qed
 
 
 subsubsection "Analysis of insert"
 
 lemma amor_insert: assumes "bst t"
-shows "T_splay x t + \<Phi>(Splay_Tree.insert x t) - \<Phi> t \<le> 4 * log 2 (size1 t) + 2" (is "?l \<le> ?r")
+shows "T_insert x t + \<Phi>(Splay_Tree.insert x t) - \<Phi> t \<le> 4 * log 2 (size1 t) + 3" (is "?l \<le> ?r")
 proof cases
-  assume "t = Leaf" thus ?thesis by(simp)
+  assume "t = Leaf" thus ?thesis by(simp add: T_insert_def)
 next
   assume "t \<noteq> Leaf"
   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 x t)"
   let ?Plr = "\<Phi> l + \<Phi> r"  let ?Ps = "\<Phi> t"
   let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)"
   have opt: "?t + \<Phi> (splay x t) - ?Ps  \<le> 3 * log 2 (real (size1 t)) + 1"
     using A_splay_ub3[OF \<open>bst t\<close>, simplified A_splay_def, of x] by (simp)
   from less_linear[of e x]
   show ?thesis
   proof (elim disjE)
     assume "e=x"
     have nneg: "log 2 (1 + real (size t)) \<ge> 0" by simp
     thus ?thesis using \<open>t \<noteq> Leaf\<close> opt \<open>e=x\<close>
-      apply(simp add: algebra_simps) using nneg by arith
+      apply(simp add: T_insert_def algebra_simps) using nneg by arith
   next
     let ?L = "log 2 (real(size1 l) + 1)"
     assume "e < x" hence "e \<noteq> x" by simp
-    hence "?l = (?t + ?Plr - ?Ps) + ?L + ?LR"
-      using  \<open>t \<noteq> Leaf\<close> \<open>e<x\<close> by(simp)
+    hence "?l = (?t + ?Plr - ?Ps) + ?L + ?LR + 1"
+      using  \<open>t \<noteq> Leaf\<close> \<open>e<x\<close> by(simp add: T_insert_def)
     also have "?t + ?Plr - ?Ps \<le> 2 * log 2 ?slr + 1"
       using opt size_splay[of x t,symmetric] by(simp)
     also have "?L \<le> log 2 ?slr" by(simp)
     also have "?LR \<le> log 2 ?slr + 1"
     proof -
       have "?LR \<le> log 2 (2 * ?slr)" by (simp add:)
       also have "\<dots> \<le> log 2 ?slr + 1"
         by (simp add: log_mult del:distrib_left_numeral)
       finally show ?thesis .
     qed
     finally show ?thesis using size_splay[of x t,symmetric] by (simp)
   next
     let ?R = "log 2 (2 + real(size r))"
     assume "x < e" hence "e \<noteq> x" by simp
-    hence "?l = (?t + ?Plr - ?Ps) + ?R + ?LR"
-      using \<open>t \<noteq> Leaf\<close> \<open>x < e\<close> by(simp)
+    hence "?l = (?t + ?Plr - ?Ps) + ?R + ?LR + 1"
+      using \<open>t \<noteq> Leaf\<close> \<open>x < e\<close> by(simp add: T_insert_def)
     also have "?t + ?Plr - ?Ps \<le> 2 * log 2 ?slr + 1"
       using opt size_splay[of x t,symmetric] by(simp)
     also have "?R \<le> log 2 ?slr" by(simp)
     also have "?LR \<le> log 2 ?slr + 1"
     proof -
       have "?LR \<le> log 2 (2 * ?slr)" by (simp add:)
       also have "\<dots> \<le> log 2 ?slr + 1"
         by (simp add: log_mult del:distrib_left_numeral)
       finally show ?thesis .
     qed
     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 \<Rightarrow> real" where
 "A_splay_max t = T_splay_max t + \<Phi>(splay_max t) - \<Phi> t"
 
 lemma A_splay_max_ub: "t \<noteq> Leaf \<Longrightarrow> A_splay_max t \<le> 3 * (\<phi> t - 1) + 1"
 proof(induction t rule: splay_max.induct)
   case 1 thus ?case by (simp)
 next
   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 \<noteq> 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 + \<phi> ?B' + \<phi> ?C' - \<phi> rr - \<phi> ?C + 1" using "3.prems" sp 1
       by(auto simp add: A_splay_max_def)
     also have "\<dots> \<le> 3 * (\<phi> rr - 1) + \<phi> ?B' + \<phi> ?C' - \<phi> rr - \<phi> ?C + 2"
       using 3 \<open>rr \<noteq> Leaf\<close> by auto
     also have "\<dots> = 2 * \<phi> rr + \<phi> ?B' + \<phi> ?C' - \<phi> ?C - 1" by simp
     also have "\<dots> \<le> \<phi> rr + \<phi> ?B' + \<phi> ?C' - 1" by simp
     also have "\<dots> \<le> 2 * \<phi> ?B + \<phi> ?C' - 2"
       using ld_ld_1_less[of "size1 ?B'" "size1 rr"] by(simp add:)
     also have "\<dots> \<le> 3 * \<phi> ?B - 2" using 1 by simp
     finally show ?case by simp
   qed
 qed
 
 lemma A_splay_max_ub3: "A_splay_max t \<le> 3 * \<phi> t + 1"
 proof cases
   assume "t = Leaf" thus ?thesis by(simp add: A_splay_max_def)
 next
   assume "t \<noteq> Leaf"
   show ?thesis using A_splay_max_ub[OF \<open>t \<noteq> Leaf\<close>] by(simp)
 qed
 
 lemma amor_delete: assumes "bst t"
-shows "T_delete a t + \<Phi>(Splay_Tree.delete a t) - \<Phi> t \<le> 6 * log 2 (size1 t) + 2"
+shows "T_delete a t + \<Phi>(Splay_Tree.delete a t) - \<Phi> t \<le> 6 * log 2 (size1 t) + 3"
 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 = "\<Phi> l + \<Phi> r"  let ?Ps = "\<Phi> 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 \<ge> 0" by simp
   have opt: "?t + \<Phi> (splay a t) - ?Ps  \<le> 3 * log 2 (real (size1 t)) + 1"
     using A_splay_ub3[OF \<open>bst t\<close>, 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 \<open>?lslr \<ge> 0\<close> by arith
   next
     case [simp]: True
     show ?thesis
     proof (cases l)
       case Leaf
       have 1: "log 2 (real (size r) + 2) \<ge> 0" by(simp)
       show ?thesis
         using Leaf opt apply(simp add: Splay_Tree.delete_def T_delete_def field_simps)
         using 1 \<open>?lslr \<ge> 0\<close> 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 \<open>bst t\<close>, of a] by simp
       have "\<Phi> r' \<ge> 0" apply (induction r') by (auto)
       have optm: "real(T_splay_max l) + \<Phi> (splay_max l) - \<Phi> l  \<le> 3 * \<phi> 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))) \<le> 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'))) \<ge> 0" by simp
       have 3: "log 2 (size1 l' + size1 r) \<le> 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)) \<le> ?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 \<open>\<Phi> r' \<ge> 0\<close> 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"
+"U (Insert _) [t] = 4 * log 2 (size1 t) + 3" |
+"U (Delete _) [t] = 6 * log 2 (size1 t) + 3"
 
 interpretation Amortized
 where arity = arity and exec = exec and inv = bst
 and cost = cost and \<Phi> = \<Phi> 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 \<open>bst t\<close>, 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 \<open>bst t\<close>, of a] Insert show ?thesis
       by (auto simp: splay_bstL[OF \<open>bst t\<close>] splay_bstR[OF \<open>bst t\<close>] 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 \<le> ?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 \<open>bst t\<close>] 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,136 +1,139 @@
 section "Splay Tree"
 
 subsection "Basics"
 
 theory Splay_Tree_Analysis_Base
 imports
   Lemmas_log
   Splay_Tree.Splay_Tree
 begin
 
 declare size1_size[simp]
 
 abbreviation "\<phi> t == log 2 (size1 t)"
 
 fun \<Phi> :: "'a tree \<Rightarrow> real" where
 "\<Phi> Leaf = 0" |
 "\<Phi> (Node l a r) = \<phi> (Node l a r) + \<Phi> l + \<Phi> r"
 
 fun T_splay :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> nat" where
 "T_splay x Leaf = 1" |
 "T_splay x (Node AB b CD) =
   (case cmp x b of
    EQ \<Rightarrow> 1 |
    LT \<Rightarrow> (case AB of
           Leaf \<Rightarrow> 1 |
           Node A a B \<Rightarrow>
             (case cmp x a of EQ \<Rightarrow> 1 |
              LT \<Rightarrow> if A = Leaf then 1 else T_splay x A + 1 |
              GT \<Rightarrow> if B = Leaf then 1 else T_splay x B + 1)) |
    GT \<Rightarrow> (case CD of
           Leaf \<Rightarrow> 1 |
           Node C c D \<Rightarrow>
             (case cmp x c of EQ \<Rightarrow> 1 |
              LT \<Rightarrow> if C = Leaf then 1 else T_splay x C + 1 |
              GT \<Rightarrow> if D = Leaf then 1 else T_splay x D + 1)))"
 
 lemma T_splay_simps[simp]:
   "T_splay a (Node l a r) = 1"
   "x<b \<Longrightarrow> T_splay x (Node Leaf b CD) = 1"
   "a<b \<Longrightarrow> T_splay a (Node (Node A a B) b CD) = 1"
   "x<a \<Longrightarrow> x<b \<Longrightarrow> T_splay x (Node (Node A a B) b CD) =
    (if A = Leaf then 1 else T_splay x A + 1)"
   "x<b \<Longrightarrow> a<x \<Longrightarrow> T_splay x (Node (Node A a B) b CD) =
    (if B = Leaf then 1 else T_splay x B + 1)"
   "b<x \<Longrightarrow> T_splay x (Node AB b Leaf) = 1"
   "b<a \<Longrightarrow> T_splay a (Node AB b (Node C a D)) = 1"
   "b<x \<Longrightarrow> x<c \<Longrightarrow> T_splay x (Node AB b (Node C c D)) =
   (if C=Leaf then 1 else T_splay x C + 1)"
   "b<x \<Longrightarrow> c<x \<Longrightarrow> 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]
 
+definition T_insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> nat" where
+"T_insert x t = 1 + (if t = Leaf then 0 else T_splay x t)"
+
 fun T_splay_max :: "'a::linorder tree \<Rightarrow> nat" where
 "T_splay_max Leaf = 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 \<Rightarrow> 'a tree \<Rightarrow> nat" where
 "T_delete x t =
-  (if t = Leaf then 0
+  1 + (if t = Leaf then 0
    else T_splay x t +
      (case splay x t of
-        Node l a r \<Rightarrow> if x=a then case l of Leaf \<Rightarrow> 0 | _ \<Rightarrow> T_splay_max l else 0))"
+        Node l a r \<Rightarrow> if x \<noteq> a then 0 else if l = Leaf then 0 else T_splay_max l))"
 
 lemma ex_in_set_tree: "t \<noteq> Leaf \<Longrightarrow> bst t \<Longrightarrow>
   \<exists>x' \<in> set_tree t. splay x' t = splay x t \<and> 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 \<noteq> 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 A" using "6.prems" by auto
   from "6.IH"[OF \<open>A \<noteq> Leaf\<close> \<open>bst A\<close>]
   obtain x' where "x' \<in> set_tree A" "splay x' A = splay x A" "T_splay x' A = T_splay x A"
     by blast
   moreover hence "x'<b" using "6.prems"(2) by auto
   ultimately show ?case using \<open>x<c\<close> \<open>x<b\<close> \<open>b<c\<close> \<open>bst A\<close> by force
 next
   case (8 a x c B)
   hence "splay x B \<noteq> Leaf" by simp
   then obtain B1 u B2 where [simp]: "splay x B = Node B1 u B2"
     by (metis tree.exhaust)
   have "a < c" "bst B" using "8.prems" by auto
   from "8.IH"[OF \<open>B \<noteq> Leaf\<close> \<open>bst B\<close>]
   obtain x' where "x' \<in> set_tree B" "splay x' B = splay x B" "T_splay x' B = T_splay x B"
     by blast
   moreover hence "a<x' & x'<c" using "8.prems"(2) by simp
   ultimately show ?case using \<open>x<c\<close> \<open>a<x\<close> \<open>a<c\<close> \<open>bst B\<close> by force
 next
   case (11 b x c C)
   hence "splay x C \<noteq> Leaf" by simp
   then obtain C1 u C2 where [simp]: "splay x C = Node C1 u C2"
     by (metis tree.exhaust)
   have "b < c" "bst C" using "11.prems" by auto
   from "11.IH"[OF \<open>C \<noteq> Leaf\<close> \<open>bst C\<close>]
   obtain x' where "x' \<in> set_tree C" "splay x' C = splay x C" "T_splay x' C = T_splay x C"
     by blast
   moreover hence "b<x' & x'<c" using "11.prems" by simp
   ultimately show ?case using \<open>b<x\<close> \<open>x<c\<close> \<open>b<c\<close> \<open>bst C\<close> by force
 next
   case (14 a x c D)
   hence "splay x D \<noteq> 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 \<open>D \<noteq> Leaf\<close> \<open>bst D\<close>]
   obtain x' where "x' \<in> set_tree D" "splay x' D = splay x D" "T_splay x' D = T_splay x D"
     by blast
   moreover hence "c<x'" using "14.prems"(2) by simp
   ultimately show ?case using \<open>a<x\<close> \<open>c<x\<close> \<open>a<c\<close> \<open>bst D\<close> by force
 qed (auto simp: le_less)
 
 
 datatype 'a op = Empty | Splay 'a | Insert 'a | Delete 'a
 
 fun arity :: "'a::linorder op \<Rightarrow> nat" where
 "arity Empty = 0" |
 "arity (Splay x) = 1" |
 "arity (Insert x) = 1" |
 "arity (Delete x) = 1"
 
 fun exec :: "'a::linorder op \<Rightarrow> 'a tree list \<Rightarrow> 'a tree" where
 "exec Empty [] = Leaf" |
 "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 \<Rightarrow> 'a tree list \<Rightarrow> nat" where
 "cost Empty [] = 1" |
 "cost (Splay x) [t] = T_splay x t" |
-"cost (Insert x) [t] = T_splay x t" |
+"cost (Insert x) [t] = T_insert x t" |
 "cost (Delete x) [t] = T_delete x t"
 
 end
diff --git a/thys/Amortized_Complexity/Splay_Tree_Analysis_Optimal.thy b/thys/Amortized_Complexity/Splay_Tree_Analysis_Optimal.thy
--- a/thys/Amortized_Complexity/Splay_Tree_Analysis_Optimal.thy
+++ b/thys/Amortized_Complexity/Splay_Tree_Analysis_Optimal.thy
@@ -1,495 +1,495 @@
 subsection "Splay Tree Analysis (Optimal)"
 
 theory Splay_Tree_Analysis_Optimal
 imports
   Splay_Tree_Analysis_Base
   Amortized_Framework
   "HOL-Library.Sum_of_Squares"
 begin
 
 text\<open>This analysis follows Schoenmakers~\cite{Schoenmakers-IPL93}.\<close>
 
 subsubsection "Analysis of splay"
 
 locale Splay_Analysis =
 fixes \<alpha> :: real and \<beta> :: real
 assumes a1[arith]: "\<alpha> > 1"
 assumes A1: "\<lbrakk>1 \<le> x; 1 \<le> y; 1 \<le> z\<rbrakk> \<Longrightarrow>
  (x+y) * (y+z) powr \<beta> \<le> (x+y) powr \<beta> * (x+y+z)"
 assumes A2: "\<lbrakk>1 \<le> l'; 1 \<le> r'; 1 \<le> lr; 1 \<le> r\<rbrakk> \<Longrightarrow>
    \<alpha> * (l'+r') * (lr+r) powr \<beta> * (lr+r'+r) powr \<beta>
     \<le> (l'+r') powr \<beta> * (l'+lr+r') powr \<beta> * (l'+lr+r'+r)"
 assumes A3: "\<lbrakk>1 \<le> l'; 1 \<le> r'; 1 \<le> ll; 1 \<le> r\<rbrakk> \<Longrightarrow>
   \<alpha> * (l'+r') * (l'+ll) powr \<beta> * (r'+r) powr \<beta>
   \<le> (l'+r') powr \<beta> * (l'+ll+r') powr \<beta> * (l'+ll+r'+r)"
 begin
 
 lemma nl2: "\<lbrakk> ll \<ge> 1; lr \<ge> 1; r \<ge> 1 \<rbrakk> \<Longrightarrow>
   log \<alpha> (ll + lr) + \<beta> * log \<alpha> (lr + r)
   \<le> \<beta> * log \<alpha> (ll + lr) + log \<alpha> (ll + lr + r)"
 apply(rule powr_le_cancel_iff[THEN iffD1, OF a1])
 apply(simp add: powr_add mult.commute[of \<beta>] powr_powr[symmetric] A1)
 done
 
 
 definition \<phi> :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> real" where
 "\<phi> t1 t2 = \<beta> * log \<alpha> (size1 t1 + size1 t2)"
 
 fun \<Phi> :: "'a tree \<Rightarrow> real" where
 "\<Phi> Leaf = 0" |
 "\<Phi> (Node l _ r) = \<Phi> l + \<Phi> r + \<phi> l r"
 
 definition A :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> real" where
 "A a t = T_splay a t + \<Phi>(splay a t) - \<Phi> t"
 
 lemma A_simps[simp]: "A a (Node l a r) = 1"
  "a<b \<Longrightarrow> A a (Node (Node ll a lr) b r) = \<phi> lr r - \<phi> lr ll + 1"
  "b<a \<Longrightarrow> A a (Node l b (Node rl a rr)) = \<phi> rl l - \<phi> rr rl + 1"
 by(auto simp add: A_def \<phi>_def algebra_simps)
 
 
 lemma A_ub: "\<lbrakk> bst t; Node la a ra : subtrees t \<rbrakk>
   \<Longrightarrow> A a t \<le> log \<alpha> ((size1 t)/(size1 la + size1 ra)) + 1"
 proof(induction a 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 b a lb rb ra)
   have "b \<notin> set_tree ra" using "3.prems"(1) by auto
   thus ?case using "3.prems"(1,2) nl2[of "size1 lb" "size1 rb" "size1 ra"]
     by (auto simp: \<phi>_def log_divide algebra_simps)
 next
   case (9 a b la lb rb)
   have "b \<notin> set_tree la" using "9.prems"(1) by auto
   thus ?case using "9.prems"(1,2) nl2[of "size1 rb" "size1 lb" "size1 la"]
     by (auto simp add: \<phi>_def log_divide algebra_simps)
 next
   case (6 x b a lb rb ra)
   hence 0: "x \<notin> set_tree rb \<and> x \<notin> set_tree ra" using "6.prems"(1) by auto
   hence 1: "x \<in> set_tree lb" using "6.prems" \<open>x<b\<close> by (auto)
   then obtain lu u ru where sp: "splay x lb = Node lu u ru"
     using "6.prems"(1,2) by(cases "splay x lb") auto
   have "b < a" using "6.prems"(1,2) by (auto)
   let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
   let ?rb = "real(size1 rb)"  let ?r = "real(size1 ra)"
   have "1 + log \<alpha> (?lu + ?ru) + \<beta> * log \<alpha> (?rb + ?r) + \<beta> * log \<alpha> (?rb + ?ru + ?r) \<le>
         \<beta> * log \<alpha> (?lu + ?ru) + \<beta> * log \<alpha> (?lu + ?rb + ?ru) + log \<alpha> (?lu + ?rb + ?ru + ?r)" (is "?L\<le>?R")
   proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
     show "\<alpha> powr ?L \<le> \<alpha> powr ?R" using A2[of ?lu ?ru ?rb ?r]
       by(simp add: powr_add add_ac mult.commute[of \<beta>] powr_powr[symmetric])
   qed
   thus ?case using 6 0 1 sp
     by(auto simp: A_def \<phi>_def size_if_splay algebra_simps log_divide)
 next
   case (8 b x a rb lb ra)
   hence 0: "x \<notin> set_tree lb \<and> x \<notin> set_tree ra" using "8.prems"(1) by(auto)
   hence 1: "x \<in> set_tree rb" using "8.prems" \<open>b<x\<close> \<open>x<a\<close> by (auto)
   then obtain lu u ru where sp: "splay x rb = Node lu u ru"
     using "8.prems"(1,2) by(cases "splay x rb") auto
   let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
   let ?lb = "real(size1 lb)" let ?r = "real(size1 ra)"
   have "1 + log \<alpha> (?lu + ?ru) + \<beta> * log \<alpha> (?lu + ?lb) + \<beta> * log \<alpha> (?ru + ?r) \<le>
         \<beta> * log \<alpha> (?lu + ?ru) + \<beta> * log \<alpha> (?lu + ?lb + ?ru) + log \<alpha> (?lu + ?lb + ?ru + ?r)" (is "?L\<le>?R")
   proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
      show "\<alpha> powr ?L \<le> \<alpha> powr ?R" using A3[of ?lu ?ru ?lb ?r]
        by(simp add: powr_add mult.commute[of \<beta>] powr_powr[symmetric])
   qed
   thus ?case using 8 0 1 sp
     by(auto simp add: A_def size_if_splay \<phi>_def log_divide algebra_simps)
 next
   case (11 a x b lb la rb)
   hence 0: "x \<notin> set_tree rb \<and> x \<notin> set_tree la" using "11.prems"(1) by (auto)
   hence 1: "x \<in> set_tree lb" using "11.prems" \<open>a<x\<close> \<open>x<b\<close> by (auto)
   then obtain lu u ru where sp: "splay x lb = Node lu u ru"
     using "11.prems"(1,2) by(cases "splay x lb") auto
   let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
   let ?l = "real(size1 la)"  let ?rb = "real(size1 rb)"
   have "1 + log \<alpha> (?lu + ?ru) + \<beta> * log \<alpha> (?lu + ?l) + \<beta> * log \<alpha> (?ru + ?rb) \<le>
         \<beta> * log \<alpha> (?lu + ?ru) + \<beta> * log \<alpha> (?lu + ?ru + ?rb) + log \<alpha> (?lu + ?l + ?ru + ?rb)" (is "?L\<le>?R")
   proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
     show "\<alpha> powr ?L \<le> \<alpha> powr ?R" using A3[of ?ru ?lu ?rb ?l]
       by(simp add: powr_add mult.commute[of \<beta>] powr_powr[symmetric])
         (simp add: algebra_simps)
   qed
   thus ?case using 11 0 1 sp
     by(auto simp add: A_def size_if_splay \<phi>_def log_divide algebra_simps)
 next
   case (14 a x b rb la lb)
   hence 0: "x \<notin> set_tree lb \<and> x \<notin> set_tree la" using "14.prems"(1) by(auto)
   hence 1: "x \<in> set_tree rb" using "14.prems" \<open>a<x\<close> \<open>b<x\<close> by (auto)
   then obtain lu u ru where sp: "splay x rb = Node lu u ru"
     using "14.prems"(1,2) by(cases "splay x rb") auto
   let ?la = "real(size1 la)"  let ?lb = "real(size1 lb)"
   let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
   have "1 + log \<alpha> (?lu + ?ru) + \<beta> * log \<alpha> (?la + ?lb) + \<beta> * log \<alpha> (?lu + ?la + ?lb) \<le>
         \<beta> * log \<alpha> (?lu + ?ru) + \<beta> * log \<alpha> (?lu + ?lb + ?ru) + log \<alpha> (?lu + ?lb + ?ru + ?la)" (is "?L\<le>?R")
   proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
      show "\<alpha> powr ?L \<le> \<alpha> powr ?R" using A2[of ?ru ?lu ?lb ?la]
        by(simp add: powr_add add_ac mult.commute[of \<beta>] powr_powr[symmetric])
   qed
   thus ?case using 14 0 1 sp
     by(auto simp add: A_def size_if_splay \<phi>_def log_divide algebra_simps)
 qed
 
 lemma A_ub2: assumes "bst t" "a : set_tree t"
 shows "A a t \<le> log \<alpha> ((size1 t)/2) + 1"
 proof -
   from assms(2) obtain la ra where N: "Node la a ra : subtrees t"
     by (metis set_treeE)
   have "A a t \<le> log \<alpha> ((size1 t)/(size1 la + size1 ra)) + 1"
     by(rule A_ub[OF assms(1) N])
   also have "\<dots> \<le> log \<alpha> ((size1 t)/2) + 1" by(simp add: field_simps)
   finally show ?thesis by simp
 qed
 
 lemma A_ub3: assumes "bst t" shows "A a t \<le> log \<alpha> (size1 t) + 1"
 proof cases
   assume "t = Leaf" thus ?thesis by(simp add: A_def)
 next
   assume "t \<noteq> Leaf"
   from ex_in_set_tree[OF this assms] obtain a' where
     a': "a' \<in> set_tree t"  "splay a' t = splay a t"  "T_splay a' t = T_splay a t"
     by blast
   have [arith]: "log \<alpha> 2 > 0" by simp
   show ?thesis using A_ub2[OF assms a'(1)] by(simp add: A_def a' log_divide)
 qed
 
 
 definition Am :: "'a::linorder tree \<Rightarrow> real" where
 "Am t = T_splay_max t + \<Phi>(splay_max t) - \<Phi> t"
 
 lemma Am_simp3': "\<lbrakk> c<b; bst rr; rr \<noteq> Leaf\<rbrakk> \<Longrightarrow>
   Am (Node l c (Node rl b rr)) =
   (case splay_max rr of Node rrl _ rrr \<Rightarrow>
    Am rr + \<phi> rrl (Node l c rl) + \<phi> l rl - \<phi> rl rr - \<phi> rrl rrr + 1)"
 by(auto simp: Am_def \<phi>_def size_if_splay_max algebra_simps neq_Leaf_iff split: tree.split)
 
 lemma Am_ub: "\<lbrakk> bst t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> Am t \<le> log \<alpha> ((size1 t)/2) + 1"
 proof(induction t rule: splay_max.induct)
   case 1 thus ?case by (simp)
 next
   case 2 thus ?case by (simp add: Am_def)
 next
   case (3 l b rl c rr)
   show ?case
   proof cases
     assume "rr = Leaf"
     thus ?thesis
       using nl2[of 1 "size1 rl" "size1 l"] log_le_cancel_iff[of \<alpha> 2 "2 + real(size rl)"]
       by(auto simp: Am_def \<phi>_def log_divide field_simps
            simp del: log_le_cancel_iff)
   next
     assume "rr \<noteq> 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] by(simp)
     let ?l = "real (size1 l)" let ?rl = "real (size1 rl)"
     let ?l' = "real (size1 l')" let ?r' = "real (size1 r')"
     have "1 + log \<alpha> (?l' + ?r') + \<beta> * log \<alpha> (?l + ?rl) + \<beta> * log \<alpha> (?l' + ?l + ?rl) \<le>
       \<beta> * log \<alpha> (?l' + ?r') + \<beta> * log \<alpha> (?l' + ?rl + ?r') + log \<alpha> (?l' + ?rl + ?r' + ?l)" (is "?L\<le>?R")
     proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
       show "\<alpha> powr ?L \<le> \<alpha> powr ?R" using A2[of ?r' ?l' ?rl ?l]
         by(simp add: powr_add add.commute add.left_commute mult.commute[of \<beta>] powr_powr[symmetric])
     qed
     thus ?case using 3 sp 1 \<open>rr \<noteq> Leaf\<close>
       by(auto simp add: Am_simp3' \<phi>_def log_divide algebra_simps)
   qed
 qed
 
 lemma Am_ub3: assumes "bst t" shows "Am t \<le> log \<alpha> (size1 t) + 1"
 proof cases
   assume "t = Leaf" thus ?thesis by(simp add: Am_def)
 next
   assume "t \<noteq> Leaf"
   have [arith]: "log \<alpha> 2 > 0" by simp
   show ?thesis using Am_ub[OF assms \<open>t \<noteq> Leaf\<close>] by(simp add: Am_def log_divide)
 qed
 
 end
 
 
 subsubsection "Optimal Interpretation"
 
 lemma mult_root_eq_root:
   "n>0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> root n x * y = root n (x * (y ^ n))"
 by(simp add: real_root_mult real_root_pos2)
 
 lemma mult_root_eq_root2:
   "n>0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> y * root n x = root n ((y ^ n) * x)"
 by(simp add: real_root_mult real_root_pos2)
 
 lemma powr_inverse_numeral:
   "0 < x \<Longrightarrow> x powr (1 / numeral n) = root (numeral n) x"
 by (simp add: root_powr_inverse)
 
 lemmas root_simps = mult_root_eq_root mult_root_eq_root2 powr_inverse_numeral
 
 
 lemma nl31: "\<lbrakk> (l'::real) \<ge> 1; r' \<ge> 1; lr \<ge> 1; r \<ge> 1 \<rbrakk> \<Longrightarrow>
   4 * (l' + r') * (lr + r) \<le> (l' + lr + r' + r)^2"
 by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [r + ~1*l' + lr + ~1*r']^2))))")
 
 lemma nl32: assumes "(l'::real) \<ge> 1" "r' \<ge> 1" "lr \<ge> 1" "r \<ge> 1"
 shows "4 * (l' + r') * (lr + r) * (lr + r' + r) \<le> (l' + lr + r' + r)^3"
 proof -
   have 1: "lr + r' + r \<le> l' + lr + r' + r" using assms by arith
   have 2: "0 \<le> (l' + lr + r' + r)^2" by (rule zero_le_power2)
   have 3: "0 \<le> lr + r' + r" using assms by arith
   from mult_mono[OF nl31[OF assms] 1 2 3] show ?thesis
     by(simp add: ac_simps numeral_eq_Suc)
 qed
 
 lemma nl3: assumes "(l'::real) \<ge> 1" "r' \<ge> 1" "lr \<ge> 1" "r \<ge> 1"
 shows "4 * (l' + r')^2 * (lr + r) * (lr + r' + r)
        \<le> (l' + lr + r') * (l' + lr + r' + r)^3"
 proof-
   have 1: "l' + r' \<le> l' + lr + r'" using assms by arith
   have 2: "0 \<le> (l' + lr + r' + r)^3" using assms by simp
   have 3: "0 \<le> l' + r'" using assms by arith
   from mult_mono[OF nl32[OF assms] 1 2 3] show ?thesis
     unfolding power2_eq_square by (simp only: ac_simps)
 qed
 
 
 lemma nl41: assumes "(l'::real) \<ge> 1" "r' \<ge> 1" "ll \<ge> 1" "r \<ge> 1"
 shows "4 * (l' + ll) * (r' + r) \<le> (l' + ll + r' + r)^2"
 using assms by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [r + ~1*l' + ~1*ll + r']^2))))")
 
 lemma nl42: assumes "(l'::real) \<ge> 1" "r' \<ge> 1" "ll \<ge> 1" "r \<ge> 1"
 shows "4 * (l' + r') * (l' + ll) * (r' + r) \<le> (l' + ll + r' + r)^3"
 proof -
   have 1: "l' + r' \<le> l' + ll + r' + r" using assms by arith
   have 2: "0 \<le> (l' + ll + r' + r)^2" by (rule zero_le_power2)
   have 3: "0 \<le> l' + r'" using assms by arith
   from mult_mono[OF nl41[OF assms] 1 2 3] show ?thesis
     by(simp add: ac_simps numeral_eq_Suc del: distrib_right_numeral)
 qed
 
 lemma nl4: assumes "(l'::real) \<ge> 1" "r' \<ge> 1" "ll \<ge> 1" "r \<ge> 1"
 shows "4 * (l' + r')^2 * (l' + ll) * (r' + r)
     \<le> (l' + ll + r') * (l' + ll + r' + r)^3"
 proof-
   have 1: "l' + r' \<le> l' + ll + r'" using assms by arith
   have 2: "0 \<le> (l' + ll + r' + r)^3" using assms by simp
   have 3: "0 \<le> l' + r'" using assms by arith
   from mult_mono[OF nl42[OF assms] 1 2 3] show ?thesis
     unfolding power2_eq_square by (simp only: ac_simps)
 qed
 
 lemma cancel: "x>(0::real) \<Longrightarrow> c * x ^ 2 * y * z \<le> u * v \<Longrightarrow> c * x ^ 3 * y * z \<le> x * u * v"
 by(simp add: power2_eq_square power3_eq_cube)
 
 interpretation S34: Splay_Analysis "root 3 4" "1/3"
 proof (standard, goal_cases)
   case 2 thus ?case
     by(simp add: root_simps)
       (auto simp: numeral_eq_Suc split_mult_pos_le intro!: mult_mono)
 next
   case 3 thus ?case by(simp add: root_simps cancel nl3)
 next
   case 4 thus ?case by(simp add: root_simps cancel nl4)
 qed simp
 
 
 lemma log4_log2: "log 4 x = log 2 x / 2"
 proof -
   have "log 4 x = log (2^2) x" by simp
   also have "\<dots> = log 2 x / 2" by(simp only: log_base_pow)
   finally show ?thesis .
 qed
 
 declare log_base_root[simp]
 
 lemma A34_ub: assumes "bst t"
 shows "S34.A a t \<le> (3/2) * log 2 (size1 t) + 1"
 proof -
   have "S34.A a t \<le> log (root 3 4) (size1 t) + 1" by(rule S34.A_ub3[OF assms])
   also have "\<dots> = (3/2) * log 2 (size t + 1) + 1" by(simp add: log4_log2)
   finally show ?thesis by simp
 qed
 
 lemma Am34_ub: assumes "bst t"
 shows "S34.Am t \<le> (3/2) * log 2 (size1 t) + 1"
 proof -
   have "S34.Am t \<le> log (root 3 4) (size1 t) + 1" by(rule S34.Am_ub3[OF assms])
   also have "\<dots> = (3/2) * log 2 (size1 t) + 1" by(simp add: log4_log2)
   finally show ?thesis by simp
 qed
 
 subsubsection "Overall analysis"
 
 fun U where
 "U Empty [] = 1" |
 "U (Splay _) [t] = (3/2) * log 2 (size1 t) + 1" |
-"U (Insert _) [t] = 2 * log 2 (size1 t) + 3/2" |
-"U (Delete _) [t] = 3 * log 2 (size1 t) + 2"
+"U (Insert _) [t] = 2 * log 2 (size1 t) + 5/2" |
+"U (Delete _) [t] = 3 * log 2 (size1 t) + 3"
 
 interpretation Amortized
 where arity = arity and exec = exec and inv = bst
 and cost = cost and \<Phi> = S34.\<Phi> 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 \<open>bst t\<close>, 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 \<open>bst t\<close>, of a] Insert show ?thesis
       by (auto simp: splay_bstL[OF \<open>bst t\<close>] splay_bstR[OF \<open>bst t\<close>] 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) show ?case by(induction t)(simp_all add: S34.\<phi>_def)
 next
   case (3 ss f)
   show ?case (is "?l \<le> ?r")
   proof(cases f)
     case Empty thus ?thesis using 3(2) by(simp add: S34.A_def)
   next
     case (Splay a)
     then obtain t where "ss = [t]" "bst t" using 3 by auto
     thus ?thesis using S34.A_ub3[OF \<open>bst t\<close>] Splay
       by(simp add: S34.A_def log4_log2)
   next
     case [simp]: (Insert a)
     obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
     show ?thesis
     proof cases
-      assume "t = Leaf" thus ?thesis by(simp add: S34.\<phi>_def log4_log2)
+      assume "t = Leaf" thus ?thesis by(simp add: S34.\<phi>_def log4_log2 T_insert_def)
     next
       assume "t \<noteq> Leaf"
       then obtain l e r where [simp]: "splay a t = Node l e r"
         by (metis tree.exhaust splay_Leaf_iff)
       let ?t = "real(T_splay a t)"
       let ?Plr = "S34.\<Phi> l + S34.\<Phi> r"  let ?Ps = "S34.\<Phi> t"
       let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)"
       have opt: "?t + S34.\<Phi> (splay a t) - ?Ps  \<le> 3/2 * log 2 (real (size1 t)) + 1"
         using S34.A_ub3[OF \<open>bst t\<close>, simplified S34.A_def, of a]
         by (simp add: log4_log2)
       from less_linear[of e a]
       show ?thesis
       proof (elim disjE)
         assume "e=a"
         have nneg: "log 2 (1 + real (size t)) \<ge> 0" by simp
         thus ?thesis using \<open>t \<noteq> Leaf\<close> opt \<open>e=a\<close>
-          apply(simp add: field_simps) using nneg by arith
+          apply(simp add: field_simps T_insert_def) using nneg by arith
       next
         let ?L = "log 2 (real(size1 l) + 1)"
         assume "e<a" hence "e \<noteq> a" by simp
-        hence "?l = (?t + ?Plr - ?Ps) + ?L / 2 + ?LR / 2"
-          using \<open>t \<noteq> Leaf\<close> \<open>e<a\<close> by(simp add: S34.\<phi>_def log4_log2)
+        hence "?l = (?t + ?Plr - ?Ps) + ?L / 2 + ?LR / 2 + 1"
+          using \<open>t \<noteq> Leaf\<close> \<open>e<a\<close> by(simp add: S34.\<phi>_def log4_log2 T_insert_def)
         also have "?t + ?Plr - ?Ps \<le> log 2 ?slr + 1"
           using opt size_splay[of a t,symmetric]
           by(simp add: S34.\<phi>_def log4_log2)
         also have "?L/2 \<le> log 2 ?slr / 2" by(simp)
         also have "?LR/2 \<le> log 2 ?slr / 2 + 1/2"
         proof -
           have "?LR/2 \<le> log 2 (2 * ?slr) / 2" by simp
           also have "\<dots> \<le> log 2 ?slr / 2 + 1/2"
             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
       next
         let ?R = "log 2 (2 + real(size r))"
         assume "a<e" hence "e \<noteq> a" by simp
-        hence "?l = (?t + ?Plr - ?Ps) + ?R / 2 + ?LR / 2"
-          using  \<open>t \<noteq> Leaf\<close> \<open>a<e\<close> by(simp add: S34.\<phi>_def log4_log2)
+        hence "?l = (?t + ?Plr - ?Ps) + ?R / 2 + ?LR / 2 + 1"
+          using  \<open>t \<noteq> Leaf\<close> \<open>a<e\<close> by(simp add: S34.\<phi>_def log4_log2 T_insert_def)
         also have "?t + ?Plr - ?Ps \<le> log 2 ?slr + 1"
           using opt size_splay[of a t,symmetric]
           by(simp add: S34.\<phi>_def log4_log2)
         also have "?R/2 \<le> log 2 ?slr / 2" by(simp)
         also have "?LR/2 \<le> log 2 ?slr / 2 + 1/2"
         proof -
           have "?LR/2 \<le> log 2 (2 * ?slr) / 2" by simp
           also have "\<dots> \<le> log 2 ?slr / 2 + 1/2"
             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
       qed
     qed
   next
     case [simp]: (Delete a)
     obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
     show ?thesis
     proof (cases t)
       case Leaf thus ?thesis
         by(simp add: Splay_Tree.delete_def T_delete_def S34.\<phi>_def log4_log2)
     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 = "S34.\<Phi> l + S34.\<Phi> r"  let ?Ps = "S34.\<Phi> 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 \<ge> 0" by simp
       have opt: "?t + S34.\<Phi> (splay a t) - ?Ps  \<le> 3/2 * log 2 (real (size1 t)) + 1"
         using S34.A_ub3[OF \<open>bst t\<close>, simplified S34.A_def, of a]
         by (simp add: log4_log2 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 \<open>?lslr \<ge> 0\<close> by arith
       next
         case [simp]: True
         show ?thesis
         proof (cases l)
           case Leaf
           have "S34.\<phi> Leaf r \<ge> 0" by(simp add: S34.\<phi>_def)
           thus ?thesis using Leaf opt
             apply(simp add: Splay_Tree.delete_def T_delete_def field_simps)
             using \<open>?lslr \<ge> 0\<close> 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 \<open>bst t\<close>, of a] by simp
           have "S34.\<Phi> r' \<ge> 0" apply (induction r') by (auto simp add: S34.\<phi>_def)
           have optm: "real(T_splay_max l) + S34.\<Phi> (splay_max l) - S34.\<Phi> l
             \<le> 3/2 * log 2 (real (size1 l)) + 1"
             using S34.Am_ub3[OF \<open>bst l\<close>, simplified S34.Am_def]
             by (simp add: log4_log2 field_simps Node)
           have 1: "log 4 (2+(real(size l')+real(size r))) \<le>
             log 4 (2+(real(size l)+real(size r)))"
             using size_splay_max[of l] Node by simp
           have 2: "log 4 (2 + (real (size l') + real (size r'))) \<ge> 0" by simp
           have 3: "S34.\<phi> l' r \<le> S34.\<phi> l' r' + S34.\<phi> l r"
             apply(simp add: S34.\<phi>_def) using 1 2 by arith
           have 4: "log 2 (real(size ll) + (real(size lr) + 2)) \<le> ?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 \<open>S34.\<Phi> r' \<ge> 0\<close> by arith
         qed
       qed
     qed
   qed
 qed
 
 end