--- a/src/HOL/Data_Structures/Splay_Set.thy Wed Nov 18 08:54:58 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Set.thy Wed Nov 18 10:12:37 2015 +0100
@@ -83,11 +83,15 @@
hide_const (open) insert
-fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"insert x t = (if t = Leaf then Node Leaf x Leaf
- else case splay x t of
- Node l a r \<Rightarrow> if x = a then Node l a r
- else if x < a then Node l x (Node Leaf a r) else Node (Node l a Leaf) x r)"
+fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"insert x t =
+ (if t = Leaf then Node Leaf x Leaf
+ else case splay x t of
+ Node l a r \<Rightarrow>
+ case cmp x a of
+ EQ \<Rightarrow> Node l a r |
+ LT \<Rightarrow> Node l x (Node Leaf a r) |
+ GT \<Rightarrow> Node (Node l a Leaf) x r)"
fun splay_max :: "'a tree \<Rightarrow> 'a tree" where
@@ -100,11 +104,12 @@
definition delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"delete x t = (if t = Leaf then Leaf
- else case splay x t of Node l a r \<Rightarrow>
- if x = a
- then if l = Leaf then r else case splay_max l of Node l' m r' \<Rightarrow> Node l' m r
- else Node l a r)"
+"delete x t =
+ (if t = Leaf then Leaf
+ else case splay x t of Node l a r \<Rightarrow>
+ if x = a
+ then if l = Leaf then r else case splay_max l of Node l' m r' \<Rightarrow> Node l' m r
+ else Node l a r)"
subsection "Functional Correctness Proofs"
--- a/src/HOL/Data_Structures/document/root.bib Wed Nov 18 08:54:58 2015 +0100
+++ b/src/HOL/Data_Structures/document/root.bib Wed Nov 18 10:12:37 2015 +0100
@@ -13,3 +13,7 @@
@article{SleatorT-JACM85,author={Daniel D. Sleator and Robert E. Tarjan},
title={Self-adjusting Binary Search Trees},journal={J. ACM},
volume=32,number=3,pages={652-686},year=1985}
+
+@misc{Turbak230,author={Franklyn Turbak},
+title={{CS230 Handouts --- Spring 2007}},year=2007,
+note={\url{http://cs.wellesley.edu/~cs230/spring07/handouts.html}}}
--- a/src/HOL/Data_Structures/document/root.tex Wed Nov 18 08:54:58 2015 +0100
+++ b/src/HOL/Data_Structures/document/root.tex Wed Nov 18 10:12:37 2015 +0100
@@ -42,7 +42,8 @@
Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
\paragraph{2-3 trees}
-The function definitions are based on the teaching material by Franklyn Turbak.
+The function definitions are based on the teaching material by
+Turbak~\cite{Turbak230}.
\paragraph{Splay trees}
They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.