# HG changeset patch
# User nipkow
# Date 1447837957 -3600
# Node ID 0753dd4c9144b514a3066feef6e26a6ba8e511a5
# Parent  ce6320b9ef9bbaf992d3477c37131fe09cdf07de
converted to cmp

diff -r ce6320b9ef9b -r 0753dd4c9144 src/HOL/Data_Structures/Splay_Set.thy
--- 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"
diff -r ce6320b9ef9b -r 0753dd4c9144 src/HOL/Data_Structures/document/root.bib
--- 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}}}
diff -r ce6320b9ef9b -r 0753dd4c9144 src/HOL/Data_Structures/document/root.tex
--- 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}.