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 \ 'a tree \ real" where
"A_splay a t = T_splay a t + \(splay a t) - \ t"
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 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 = "\\A, x, B\, b, CD\"
let ?t' = "\A, x, \B, b, CD\\"
have *: "l = A \ r = B" using "3.prems" by(fastforce dest: in_set_tree_if)
have "A_splay x ?t = 1 + \ ?t' - \ ?t" using "3.hyps" by (simp add: A_splay_def)
also have "\ = 1 + \ ?t' + \ \B, b, CD\ - \ ?t - \ \A, x, B\" by(simp)
also have "\ = 1 + \ \B, b, CD\ - \ \A, x, B\" by(simp)
also have "\ \ 1 + \ ?t - \(Node A x B)"
using log_le_cancel_iff[of 2 "size1(Node B b CD)" "size1 ?t"] by (simp)
also have "\ \ 1 + 3 * (\ ?t - \(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 = "\AB, b, \C, x, D\\"
have "x \ 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 *: "\l, x, r\ \ 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 \A \ Leaf\] 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 + \ ?A2BC + \ ?BC - \ ?AB - \ ?A' + 1"
using "6.hyps" sp
by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
also have "\ \ 3 * \ A + \ ?A2BC + \ ?BC - \ ?AB - \ ?A' - 3 * \ ?X + 2"
using "6.IH" "6.prems"(1) * by(auto simp: algebra_simps)
also have "\ = 2 * \ A + \ ?A2BC + \ ?BC - \ ?AB - 3 * \ ?X + 2"
using sp by(simp add: size_if_splay)
also have "\ < \ A + \ ?A2BC + \ ?BC - 3 * \ ?X + 2" by(simp)
also have "\ < \ ?A2BC + 2 * \ ?ABC - 3 * \ ?X + 1"
using sp ld_ld_1_less[of "size1 A" "size1 ?BC"]
by(simp add: size_if_splay)
also have "\ < 3 * \ ?ABC - 3 * \ ?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 *: "\l, x, r\ \ 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 \B \ Leaf\] 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 + \ ?AB1 + \ ?B2C - \ ?AB - \ ?B' + 1"
using "8.hyps" sp
by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
also have "\ \ 3 * \ B + \ ?AB1 + \ ?B2C - \ ?AB - \ ?B' - 3 * \ ?X + 2"
using "8.IH" "8.prems"(1) * by(auto simp: algebra_simps)
also have "\ = 2 * \ B + \ ?AB1 + \ ?B2C - \ ?AB - 3 * \ ?X + 2"
using sp by(simp add: size_if_splay)
also have "\ < \ B + \ ?AB1 + \ ?B2C - 3 * \ ?X + 2" by(simp)
also have "\ < \ B + 2 * \ ?ABC - 3 * \ ?X + 1"
using sp ld_ld_1_less[of "size1 ?AB1" "size1 ?B2C"]
by(simp add: size_if_splay)
also have "\ < 3 * \ ?ABC - 3 * \ ?X + 1" by(simp)
finally show ?case by simp
next
case (11 b x c C A D)
hence *: "\l, x, r\ \ 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 \C \ Leaf\] 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 + \ ?C2D + \ ?AC1 - \ ?CD - \ ?C' + 1"
using "11.hyps" sp
by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
also have "\ \ 3 * \ C + \ ?C2D + \ ?AC1 - \ ?CD - \ ?C' - 3 * \ ?X + 2"
using "11.IH" "11.prems"(1) * by(auto simp: algebra_simps)
also have "\ = 2 * \ C + \ ?C2D + \ ?AC1 - \ ?CD - 3 * \ ?X + 2"
using sp by(simp add: size_if_splay)
also have "\ \ \ C + \ ?C2D + \ ?AC1 - 3 * \ ?X + 2" by(simp)
also have "\ \ \ C + 2 * \ ?ACD - 3 * \ ?X + 1"
using sp ld_ld_1_less[of "size1 ?C2D" "size1 ?AC1"]
by(simp add: size_if_splay algebra_simps)
also have "\ \ 3 * \ ?ACD - 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" "x : set_tree t"
shows "A_splay x t \ 3 * (\