# 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 \ '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 \ 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 \ '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 @@ -100,11 +104,12 @@ 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 if l = Leaf then r else case splay_max l of Node l' m r' \ 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 \ + if x = a + then if l = Leaf then r else case splay_max l of Node l' m r' \ 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}.