# HG changeset patch # User nipkow # Date 1446231665 -3600 # Node ID 87244a9cfe40decfd701772eb0db0efd3179e968 # Parent f2e51e704a962fbdb3f62b28a11c73eabc62d97f added splay trees diff -r f2e51e704a96 -r 87244a9cfe40 src/HOL/Data_Structures/Splay_Map.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Data_Structures/Splay_Map.thy Fri Oct 30 20:01:05 2015 +0100 @@ -0,0 +1,180 @@ +(* Author: Tobias Nipkow *) + +section "Splay Tree Implementation of Maps" + +theory Splay_Map +imports + Splay_Set + Map_by_Ordered +begin + +function splay :: "'a::linorder \ ('a*'b) tree \ ('a*'b) tree" where +"splay x Leaf = Leaf" | +"x = fst a \ splay x (Node t1 a t2) = Node t1 a t2" | +"x = fst a \ x < fst b \ splay x (Node (Node t1 a t2) b t3) = Node t1 a (Node t2 b t3)" | +"x < fst a \ splay x (Node Leaf a t) = Node Leaf a t" | +"x < fst a \ x < fst b \ splay x (Node (Node Leaf a t1) b t2) = Node Leaf a (Node t1 b t2)" | +"x < fst a \ x < fst b \ t1 \ Leaf \ + splay x (Node (Node t1 a t2) b t3) = + (case splay x t1 of Node t11 y t12 \ Node t11 y (Node t12 a (Node t2 b t3)))" | +"fst a < x \ x < fst b \ splay x (Node (Node t1 a Leaf) b t2) = Node t1 a (Node Leaf b t2)" | +"fst a < x \ x < fst b \ t2 \ Leaf \ + splay x (Node (Node t1 a t2) b t3) = + (case splay x t2 of Node t21 y t22 \ Node (Node t1 a t21) y (Node t22 b t3))" | +"fst a < x \ x = fst b \ splay x (Node t1 a (Node t2 b t3)) = Node (Node t1 a t2) b t3" | +"fst a < x \ splay x (Node t a Leaf) = Node t a Leaf" | +"fst a < x \ x < fst b \ t2 \ Leaf \ + splay x (Node t1 a (Node t2 b t3)) = + (case splay x t2 of Node t21 y t22 \ Node (Node t1 a t21) y (Node t22 b t3))" | +"fst a < x \ x < fst b \ splay x (Node t1 a (Node Leaf b t2)) = Node (Node t1 a Leaf) b t2" | +"fst a < x \ fst b < x \ splay x (Node t1 a (Node t2 b Leaf)) = Node (Node t1 a t2) b Leaf" | +"fst a < x \ fst b < x \ t3 \ Leaf \ + splay x (Node t1 a (Node t2 b t3)) = + (case splay x t3 of Node t31 y t32 \ Node (Node (Node t1 a t2) b t31) y t32)" +apply(atomize_elim) +apply(auto) +(* 1 subgoal *) +apply (subst (asm) neq_Leaf_iff) +apply(auto) +apply (metis tree.exhaust surj_pair less_linear)+ +done + +termination splay +by lexicographic_order + +lemma splay_code: "splay x t = (case t of Leaf \ Leaf | + Node al a ar \ + (if x = fst a then t else + if x < fst a then + case al of + Leaf \ t | + Node bl b br \ + (if x = fst b then Node bl b (Node br a ar) else + if x < fst b then + if bl = Leaf then Node bl b (Node br a ar) + else case splay x bl of + Node bll y blr \ Node bll y (Node blr b (Node br a ar)) + else + if br = Leaf then Node bl b (Node br a ar) + else case splay x br of + Node brl y brr \ Node (Node bl b brl) y (Node brr a ar)) + else + case ar of + Leaf \ t | + Node bl b br \ + (if x = fst b then Node (Node al a bl) b br else + if x < fst b then + if bl = Leaf then Node (Node al a bl) b br + else case splay x bl of + Node bll y blr \ Node (Node al a bll) y (Node blr b br) + else if br=Leaf then Node (Node al a bl) b br + else case splay x br of + Node bll y blr \ Node (Node (Node al a bl) b bll) y blr)))" +by(auto split: tree.split) + +definition lookup :: "('a*'b)tree \ 'a::linorder \ 'b option" where "lookup t x = + (case splay x t of Leaf \ None | Node _ (a,b) _ \ if x=a then Some b else None)" + +hide_const (open) insert + +fun update :: "'a::linorder \ 'b \ ('a*'b) tree \ ('a*'b) tree" where +"update x y t = (if t = Leaf then Node Leaf (x,y) Leaf + else case splay x t of + Node l a r \ if x = fst a then Node l (x,y) r + else if x < fst a then Node l (x,y) (Node Leaf a r) else Node (Node l a Leaf) (x,y) r)" + +definition delete :: "'a::linorder \ ('a*'b) tree \ ('a*'b) tree" where +"delete x t = (if t = Leaf then Leaf + else case splay x t of Node l a r \ + if x = fst 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" + +lemma splay_Leaf_iff: "(splay x t = Leaf) = (t = Leaf)" +by(induction x t rule: splay.induct) (auto split: tree.splits) + + +subsubsection "Proofs for lookup" + +lemma splay_map_of_inorder: + "splay x t = Node l a r \ sorted1(inorder t) \ + map_of (inorder t) x = (if x = fst a then Some(snd a) else None)" +by(induction x t arbitrary: l a r rule: splay.induct) + (auto simp: map_of_simps splay_Leaf_iff split: tree.splits) + +lemma lookup_eq: + "sorted1(inorder t) \ lookup t x = map_of (inorder t) x" +by(auto simp: lookup_def splay_Leaf_iff splay_map_of_inorder split: tree.split) + + +subsubsection "Proofs for update" + +lemma inorder_splay: "inorder(splay x t) = inorder t" +by(induction x t rule: splay.induct) + (auto simp: neq_Leaf_iff split: tree.split) + +lemma sorted_splay: + "sorted1(inorder t) \ splay x t = Node l a r \ + sorted(map fst (inorder l) @ x # map fst (inorder r))" +unfolding inorder_splay[of x t, symmetric] +by(induction x t arbitrary: l a r rule: splay.induct) + (auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits) + +(* more upd_list lemmas; unify with basic set? *) + +lemma upd_list_Cons: + "sorted1 ((x,y) # xs) \ upd_list x y xs = (x,y) # xs" +by (induction xs) auto + +lemma upd_list_snoc: + "sorted1 (xs @ [(x,y)]) \ upd_list x y xs = xs @ [(x,y)]" +by(induction xs) (auto simp add: sorted_mid_iff2) + +lemma inorder_update: + "sorted1(inorder t) \ inorder(update x y t) = upd_list x y (inorder t)" +using inorder_splay[of x t, symmetric] sorted_splay[of t x] +by(auto simp: upd_list_simps upd_list_Cons upd_list_snoc neq_Leaf_iff split: tree.split) + + +subsubsection "Proofs for delete" + +(* more del_simp lemmas; unify with basic set? *) + +lemma del_list_notin_Cons: "sorted (x # map fst xs) \ del_list x xs = xs" +by(induction xs)(auto simp: sorted_Cons_iff) + +lemma del_list_sorted_app: + "sorted(map fst xs @ [x]) \ del_list x (xs @ ys) = xs @ del_list x ys" +by (induction xs) (auto simp: sorted_mid_iff2) + +lemma inorder_splay_maxD: + "splay_max t = Node l a r \ sorted1(inorder t) \ + inorder l @ [a] = inorder t \ r = Leaf" +by(induction t arbitrary: l a r rule: splay_max.induct) + (auto simp: sorted_lems splay_max_Leaf_iff split: tree.splits if_splits) + +lemma inorder_delete: + "sorted1(inorder t) \ inorder(delete x t) = del_list x (inorder t)" +using inorder_splay[of x t, symmetric] sorted_splay[of t x] +by (auto simp: del_list_simps del_list_sorted_app delete_def + del_list_notin_Cons inorder_splay_maxD splay_Leaf_iff splay_max_Leaf_iff + split: tree.splits) + + +subsubsection "Overall Correctness" + +interpretation Map_by_Ordered +where empty = Leaf and lookup = lookup and update = update +and delete = delete and inorder = inorder and wf = "\_. True" +proof (standard, goal_cases) + case 2 thus ?case by(simp add: lookup_eq) +next + case 3 thus ?case by(simp add: inorder_update del: update.simps) +next + case 4 thus ?case by(simp add: inorder_delete) +qed auto + +end diff -r f2e51e704a96 -r 87244a9cfe40 src/HOL/Data_Structures/Splay_Set.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Data_Structures/Splay_Set.thy Fri Oct 30 20:01:05 2015 +0100 @@ -0,0 +1,209 @@ +(* +Author: Tobias Nipkow +Function defs follows AFP entry Splay_Tree, proofs are new. +*) + +section "Splay Tree Implementation of Sets" + +theory Splay_Set +imports + "~~/src/HOL/Library/Tree" + Set_by_Ordered +begin + +function splay :: "'a::linorder \ 'a tree \ 'a tree" where +"splay a Leaf = Leaf" | +"splay a (Node t1 a t2) = Node t1 a t2" | +"a splay a (Node (Node t1 a t2) b t3) = Node t1 a (Node t2 b t3)" | +"x splay x (Node Leaf a t) = Node Leaf a t" | +"x x splay x (Node (Node Leaf a t1) b t2) = Node Leaf a (Node t1 b t2)" | +"x x t1 \ Leaf \ + splay x (Node (Node t1 a t2) b t3) = + (case splay x t1 of Node t11 y t12 \ Node t11 y (Node t12 a (Node t2 b t3)))" | +"a x splay x (Node (Node t1 a Leaf) b t2) = Node t1 a (Node Leaf b t2)" | +"a x t2 \ Leaf \ + splay x (Node (Node t1 a t2) b t3) = + (case splay x t2 of Node t21 y t22 \ Node (Node t1 a t21) y (Node t22 b t3))" | +"a splay b (Node t1 a (Node t2 b t3)) = Node (Node t1 a t2) b t3" | +"a splay x (Node t a Leaf) = Node t a Leaf" | +"a x t2 \ Leaf \ + splay x (Node t1 a (Node t2 b t3)) = + (case splay x t2 of Node t21 y t22 \ Node (Node t1 a t21) y (Node t22 b t3))" | +"a x splay x (Node t1 a (Node Leaf b t2)) = Node (Node t1 a Leaf) b t2" | +"a b splay x (Node t1 a (Node t2 b Leaf)) = Node (Node t1 a t2) b Leaf" | +"a b t3 \ Leaf \ + splay x (Node t1 a (Node t2 b t3)) = + (case splay x t3 of Node t31 y t32 \ Node (Node (Node t1 a t2) b t31) y t32)" +apply(atomize_elim) +apply(auto) +(* 1 subgoal *) +apply (subst (asm) neq_Leaf_iff) +apply(auto) +apply (metis tree.exhaust less_linear)+ +done + +termination splay +by lexicographic_order + +lemma splay_code: "splay x t = (case t of Leaf \ Leaf | + Node al a ar \ + (if x=a then t else + if x < a then + case al of + Leaf \ t | + Node bl b br \ + (if x=b then Node bl b (Node br a ar) else + if x < b then + if bl = Leaf then Node bl b (Node br a ar) + else case splay x bl of + Node bll y blr \ Node bll y (Node blr b (Node br a ar)) + else + if br = Leaf then Node bl b (Node br a ar) + else case splay x br of + Node brl y brr \ Node (Node bl b brl) y (Node brr a ar)) + else + case ar of + Leaf \ t | + Node bl b br \ + (if x=b then Node (Node al a bl) b br else + if x < b then + if bl = Leaf then Node (Node al a bl) b br + else case splay x bl of + Node bll y blr \ Node (Node al a bll) y (Node blr b br) + else if br=Leaf then Node (Node al a bl) b br + else case splay x br of + Node bll y blr \ Node (Node (Node al a bl) b bll) y blr)))" +by(auto split: tree.split) + +definition is_root :: "'a \ 'a tree \ bool" where +"is_root a t = (case t of Leaf \ False | Node _ x _ \ x = a)" + +definition "isin t x = is_root x (splay x t)" + +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 splay_max :: "'a tree \ 'a tree" where +"splay_max Leaf = Leaf" | +"splay_max (Node l b Leaf) = Node l b Leaf" | +"splay_max (Node l b (Node rl c rr)) = + (if rr = Leaf then Node (Node l b rl) c Leaf + else case splay_max rr of + Node rrl m rrr \ Node (Node (Node l b rl) c rrl) m rrr)" + + +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)" + + +subsection "Functional Correctness Proofs" + +lemma splay_Leaf_iff: "(splay a t = Leaf) = (t = Leaf)" +by(induction a t rule: splay.induct) (auto split: tree.splits) + +lemma splay_max_Leaf_iff: "(splay_max t = Leaf) = (t = Leaf)" +by(induction t rule: splay_max.induct)(auto split: tree.splits) + + +subsubsection "Proofs for isin" + +lemma + "splay x t = Node l a r \ sorted(inorder t) \ + x \ elems (inorder t) \ x=a" +by(induction x t arbitrary: l a r rule: splay.induct) + (auto simp: elems_simps1 splay_Leaf_iff ball_Un split: tree.splits) + +lemma splay_elemsD: + "splay x t = Node l a r \ sorted(inorder t) \ + x \ elems (inorder t) \ x=a" +by(induction x t arbitrary: l a r rule: splay.induct) + (auto simp: elems_simps2 splay_Leaf_iff split: tree.splits) + +lemma isin_set: "sorted(inorder t) \ isin t x = (x \ elems (inorder t))" +by (auto simp: isin_def is_root_def splay_elemsD splay_Leaf_iff split: tree.splits) + + +subsubsection "Proofs for insert" + +(* more sorted lemmas; unify with basic set? *) + +lemma sorted_snoc_le: + "ASSUMPTION(sorted(xs @ [x])) \ x \ y \ sorted (xs @ [y])" +by (auto simp add: Sorted_Less.sorted_snoc_iff ASSUMPTION_def) + +lemma sorted_Cons_le: + "ASSUMPTION(sorted(x # xs)) \ y \ x \ sorted (y # xs)" +by (auto simp add: Sorted_Less.sorted_Cons_iff ASSUMPTION_def) + +lemma inorder_splay: "inorder(splay x t) = inorder t" +by(induction x t rule: splay.induct) + (auto simp: neq_Leaf_iff split: tree.split) + +lemma sorted_splay: + "sorted(inorder t) \ splay x t = Node l a r \ + sorted(inorder l @ x # inorder r)" +unfolding inorder_splay[of x t, symmetric] +by(induction x t arbitrary: l a r rule: splay.induct) + (auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits) + +lemma ins_list_Cons: "sorted (x # xs) \ ins_list x xs = x # xs" +by (induction xs) auto + +lemma ins_list_snoc: "sorted (xs @ [x]) \ ins_list x xs = xs @ [x]" +by(induction xs) (auto simp add: sorted_mid_iff2) + +lemma inorder_insert: + "sorted(inorder t) \ inorder(insert x t) = ins_list x (inorder t)" +using inorder_splay[of x t, symmetric] sorted_splay[of t x] +by(auto simp: ins_list_simps ins_list_Cons ins_list_snoc neq_Leaf_iff split: tree.split) + + +subsubsection "Proofs for delete" + +(* more del_simp lemmas; unify with basic set? *) + +lemma del_list_notin_Cons: "sorted (x # xs) \ del_list x xs = xs" +by(induction xs)(auto simp: sorted_Cons_iff) + +lemma del_list_sorted_app: + "sorted(xs @ [x]) \ del_list x (xs @ ys) = xs @ del_list x ys" +by (induction xs) (auto simp: sorted_mid_iff2) + +lemma inorder_splay_maxD: + "splay_max t = Node l a r \ sorted(inorder t) \ + inorder l @ [a] = inorder t \ r = Leaf" +by(induction t arbitrary: l a r rule: splay_max.induct) + (auto simp: sorted_lems splay_max_Leaf_iff split: tree.splits if_splits) + +lemma inorder_delete: + "sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" +using inorder_splay[of x t, symmetric] sorted_splay[of t x] +by (auto simp: del_list_simps del_list_sorted_app delete_def + del_list_notin_Cons inorder_splay_maxD splay_Leaf_iff splay_max_Leaf_iff + split: tree.splits) + + +subsubsection "Overall Correctness" + +interpretation Set_by_Ordered +where empty = Leaf and isin = isin and insert = insert +and delete = delete and inorder = inorder and wf = "\_. True" +proof (standard, goal_cases) + case 2 thus ?case by(simp add: isin_set) +next + case 3 thus ?case by(simp add: inorder_insert del: insert.simps) +next + case 4 thus ?case by(simp add: inorder_delete) +qed auto + +end diff -r f2e51e704a96 -r 87244a9cfe40 src/HOL/Data_Structures/document/root.bib --- a/src/HOL/Data_Structures/document/root.bib Thu Oct 29 15:40:52 2015 +0100 +++ b/src/HOL/Data_Structures/document/root.bib Fri Oct 30 20:01:05 2015 +0100 @@ -6,3 +6,10 @@ @book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures", publisher="Cambridge University Press",year=1998} + +@article{Schoenmakers-IPL93,author="Berry Schoenmakers", +title="A Systematic Analysis of Splaying",journal={Information Processing Letters},volume=45,pages={41-50},year=1993} + +@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} diff -r f2e51e704a96 -r 87244a9cfe40 src/HOL/Data_Structures/document/root.tex --- a/src/HOL/Data_Structures/document/root.tex Thu Oct 29 15:40:52 2015 +0100 +++ b/src/HOL/Data_Structures/document/root.tex Fri Oct 30 20:01:05 2015 +0100 @@ -44,6 +44,10 @@ \paragraph{2-3 trees} The function definitions are based on the teaching material by Franklyn Turbak. +\paragraph{Splay trees} +They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}. +Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}. + \bibliographystyle{abbrv} \bibliography{root} diff -r f2e51e704a96 -r 87244a9cfe40 src/HOL/ROOT --- a/src/HOL/ROOT Thu Oct 29 15:40:52 2015 +0100 +++ b/src/HOL/ROOT Fri Oct 30 20:01:05 2015 +0100 @@ -174,12 +174,12 @@ theories [document = false] "Less_False" theories - Tree_Set Tree_Map AVL_Map RBT_Map Tree23_Map Tree234_Map + Splay_Map document_files "root.tex" "root.bib" session "HOL-Import" in Import = HOL +