added red black trees
authornipkow
Tue Sep 22 08:38:25 2015 +0200 (2015-09-22)
changeset 61224759b5299a9f2
parent 61223 dfccf6c06201
child 61225 1a690dce8cfc
child 61246 077b88f9ec16
added red black trees
src/HOL/Data_Structures/AList_Upd_Del.thy
src/HOL/Data_Structures/Isin2.thy
src/HOL/Data_Structures/RBT.thy
src/HOL/Data_Structures/RBT_Map.thy
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Data_Structures/Tree2.thy
src/HOL/Data_Structures/Tree_Map.thy
src/HOL/Data_Structures/document/root.bib
src/HOL/Data_Structures/document/root.tex
src/HOL/ROOT
     1.1 --- a/src/HOL/Data_Structures/AList_Upd_Del.thy	Mon Sep 21 23:22:11 2015 +0200
     1.2 +++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Tue Sep 22 08:38:25 2015 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4    upd_list a b (ps @ (x,y) # qs) = ps @ upd_list a b ((x,y)#qs)"
     1.5  by(induction ps) (auto simp: sorted_lems)
     1.6  
     1.7 -lemmas upd_list_sorteds = upd_list_sorted1 upd_list_sorted2
     1.8 +lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2
     1.9  
    1.10  (*
    1.11  lemma set_ins_list[simp]: "set (ins_list x xs) = insert x (set xs)"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Data_Structures/Isin2.thy	Tue Sep 22 08:38:25 2015 +0200
     2.3 @@ -0,0 +1,21 @@
     2.4 +(* Author: Tobias Nipkow *)
     2.5 +
     2.6 +section \<open>Function \textit{isin} for Tree2\<close>
     2.7 +
     2.8 +theory Isin2
     2.9 +imports
    2.10 +  Tree2
    2.11 +  Set_by_Ordered
    2.12 +begin
    2.13 +
    2.14 +fun isin :: "('a,'b) tree \<Rightarrow> ('a::order) \<Rightarrow> bool" where
    2.15 +"isin Leaf x = False" |
    2.16 +"isin (Node _ l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)"
    2.17 +
    2.18 +lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
    2.19 +by (induction t) (auto simp: elems_simps)
    2.20 +
    2.21 +lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
    2.22 +by (induction t) (auto simp: elems_simps dest: sortedD)
    2.23 +
    2.24 +end
    2.25 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Data_Structures/RBT.thy	Tue Sep 22 08:38:25 2015 +0200
     3.3 @@ -0,0 +1,53 @@
     3.4 +(* Author: Tobias Nipkow *)
     3.5 +
     3.6 +section \<open>Red-Black Trees\<close>
     3.7 +
     3.8 +theory RBT
     3.9 +imports Tree2
    3.10 +begin
    3.11 +
    3.12 +datatype color = Red | Black
    3.13 +
    3.14 +type_synonym 'a rbt = "('a,color)tree"
    3.15 +
    3.16 +abbreviation R where "R l a r \<equiv> Node Red l a r"
    3.17 +abbreviation B where "B l a r \<equiv> Node Black l a r"
    3.18 +
    3.19 +fun bal :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    3.20 +(* The first line is superfluous; it merely speeds up pattern compilation *)
    3.21 +"bal (R t1 a1 t2) a2 (R t3 a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    3.22 +"bal (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    3.23 +"bal (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    3.24 +"bal t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    3.25 +"bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    3.26 +"bal t1 a t2 = B t1 a t2"
    3.27 +
    3.28 +fun red :: "'a rbt \<Rightarrow> 'a rbt" where
    3.29 +"red Leaf = Leaf" |
    3.30 +"red (Node _ l a r) = R l a r"
    3.31 +
    3.32 +fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    3.33 +"balL (R t1 x t2) s t3 = R (B t1 x t2) s t3" |
    3.34 +"balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" |
    3.35 +"balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (red t3))" |
    3.36 +"balL t1 x t2 = R t1 x t2"
    3.37 +
    3.38 +fun balR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    3.39 +"balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
    3.40 +"balR (B t1 x t2) y bl = bal (R t1 x t2) y bl" |
    3.41 +"balR (R t1 x (B t2 y t3)) z bl = R (bal (red t1) x t2) y (B t3 z bl)" |
    3.42 +"balR t1 x t2 = R t1 x t2"
    3.43 +
    3.44 +fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    3.45 +"combine Leaf t = t" |
    3.46 +"combine t Leaf = t" |
    3.47 +"combine (R a x b) (R c y d) = (case combine b c of
    3.48 +    R b2 z c2 \<Rightarrow> (R (R a x b2) z (R c2 y d)) |
    3.49 +    bc \<Rightarrow> R a x (R bc y d))" |
    3.50 +"combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of
    3.51 +    R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
    3.52 +    t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
    3.53 +"combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
    3.54 +"combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" 
    3.55 +
    3.56 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Data_Structures/RBT_Map.thy	Tue Sep 22 08:38:25 2015 +0200
     4.3 @@ -0,0 +1,79 @@
     4.4 +(* Author: Tobias Nipkow *)
     4.5 +
     4.6 +section \<open>Red-Black Tree Implementation of Maps\<close>
     4.7 +
     4.8 +theory RBT_Map
     4.9 +imports
    4.10 +  RBT_Set
    4.11 +  Map_by_Ordered
    4.12 +begin
    4.13 +
    4.14 +fun lookup :: "('a::linorder * 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b option" where
    4.15 +"lookup Leaf x = None" |
    4.16 +"lookup (Node _ l (a,b) r) x =
    4.17 +  (if x < a then lookup l x else
    4.18 +   if x > a then lookup r x else Some b)"
    4.19 +
    4.20 +fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
    4.21 +"update x y Leaf = R Leaf (x,y) Leaf" |
    4.22 +"update x y (B l (a,b) r) =
    4.23 +  (if x < a then bal (update x y l) (a,b) r else
    4.24 +   if x > a then bal l (a,b) (update x y r)
    4.25 +   else B l (x,y) r)" |
    4.26 +"update x y (R l (a,b) r) =
    4.27 +  (if x < a then R (update x y l) (a,b) r else
    4.28 +   if x > a then R l (a,b) (update x y r)
    4.29 +   else R l (x,y) r)"
    4.30 +
    4.31 +fun delete :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
    4.32 +and deleteL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
    4.33 +and deleteR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
    4.34 +where
    4.35 +"delete x Leaf = Leaf" |
    4.36 +"delete x (Node c t1 (a,b) t2) = 
    4.37 +  (if x < a then deleteL x t1 (a,b) t2 else
    4.38 +   if x > a then deleteR x t1 (a,b) t2 else combine t1 t2)" |
    4.39 +"deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
    4.40 +"deleteL x t1 a t2 = R (delete x t1) a t2" |
    4.41 +"deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | 
    4.42 +"deleteR x t1 a t2 = R t1 a (delete x t2)"
    4.43 +
    4.44 +
    4.45 +subsection "Functional Correctness Proofs"
    4.46 +
    4.47 +lemma lookup_eq:
    4.48 +  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    4.49 +by(induction t)
    4.50 +  (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
    4.51 +
    4.52 +
    4.53 +lemma inorder_update:
    4.54 +  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    4.55 +by(induction x y t rule: update.induct)
    4.56 +  (auto simp: upd_list_simps inorder_bal)
    4.57 +
    4.58 +
    4.59 +lemma inorder_delete:
    4.60 + "sorted1(inorder t1) \<Longrightarrow>  inorder(delete x t1) = del_list x (inorder t1)" and
    4.61 + "sorted1(inorder t1) \<Longrightarrow>  inorder(deleteL x t1 a t2) =
    4.62 +    del_list x (inorder t1) @ a # inorder t2" and
    4.63 + "sorted1(inorder t2) \<Longrightarrow>  inorder(deleteR x t1 a t2) =
    4.64 +    inorder t1 @ a # del_list x (inorder t2)"
    4.65 +by(induction x t1 and x t1 a t2 and x t1 a t2 rule: delete_deleteL_deleteR.induct)
    4.66 +  (auto simp: del_list_sorted sorted_lems inorder_combine inorder_balL inorder_balR)
    4.67 +
    4.68 +
    4.69 +interpretation Map_by_Ordered
    4.70 +where empty = Leaf and lookup = lookup and update = update and delete = delete
    4.71 +and inorder = inorder and wf = "\<lambda>_. True"
    4.72 +proof (standard, goal_cases)
    4.73 +  case 1 show ?case by simp
    4.74 +next
    4.75 +  case 2 thus ?case by(simp add: lookup_eq)
    4.76 +next
    4.77 +  case 3 thus ?case by(simp add: inorder_update)
    4.78 +next
    4.79 +  case 4 thus ?case by(simp add: inorder_delete)
    4.80 +qed (rule TrueI)+
    4.81 +
    4.82 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Tue Sep 22 08:38:25 2015 +0200
     5.3 @@ -0,0 +1,86 @@
     5.4 +(* Author: Tobias Nipkow *)
     5.5 +
     5.6 +section \<open>Red-Black Tree Implementation of Sets\<close>
     5.7 +
     5.8 +theory RBT_Set
     5.9 +imports
    5.10 +  RBT
    5.11 +  Isin2
    5.12 +begin
    5.13 +
    5.14 +fun insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    5.15 +"insert x Leaf = R Leaf x Leaf" |
    5.16 +"insert x (B l a r) =
    5.17 +  (if x < a then bal (insert x l) a r else
    5.18 +   if x > a then bal l a (insert x r) else B l a r)" |
    5.19 +"insert x (R l a r) =
    5.20 +  (if x < a then R (insert x l) a r
    5.21 +   else if x > a then R l a (insert x r) else R l a r)"
    5.22 +
    5.23 +fun delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    5.24 +and deleteL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    5.25 +and deleteR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    5.26 +where
    5.27 +"delete x Leaf = Leaf" |
    5.28 +"delete x (Node _ l a r) = 
    5.29 +  (if x < a then deleteL x l a r 
    5.30 +   else if x > a then deleteR x l a r else combine l r)" |
    5.31 +"deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
    5.32 +"deleteL x l a r = R (delete x l) a r" |
    5.33 +"deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | 
    5.34 +"deleteR x l a r = R l a (delete x r)"
    5.35 +
    5.36 +
    5.37 +subsection "Functional Correctness Proofs"
    5.38 +
    5.39 +lemma inorder_bal:
    5.40 +  "inorder(bal l a r) = inorder l @ a # inorder r"
    5.41 +by(induction l a r rule: bal.induct) (auto simp: sorted_lems)
    5.42 +
    5.43 +lemma inorder_insert:
    5.44 +  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
    5.45 +by(induction a t rule: insert.induct) (auto simp: ins_simps inorder_bal)
    5.46 +
    5.47 +lemma inorder_red: "inorder(red t) = inorder t"
    5.48 +by(induction t) (auto simp: sorted_lems)
    5.49 +
    5.50 +lemma inorder_balL:
    5.51 +  "inorder(balL l a r) = inorder l @ a # inorder r"
    5.52 +by(induction l a r rule: balL.induct)
    5.53 +  (auto simp: sorted_lems inorder_bal inorder_red)
    5.54 +
    5.55 +lemma inorder_balR:
    5.56 +  "inorder(balR l a r) = inorder l @ a # inorder r"
    5.57 +by(induction l a r rule: balR.induct)
    5.58 +  (auto simp: sorted_lems inorder_bal inorder_red)
    5.59 +
    5.60 +lemma inorder_combine:
    5.61 +  "inorder(combine l r) = inorder l @ inorder r"
    5.62 +by(induction l r rule: combine.induct)
    5.63 +  (auto simp: sorted_lems inorder_balL inorder_balR split: tree.split color.split)
    5.64 +
    5.65 +lemma inorder_delete:
    5.66 + "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)" and
    5.67 + "sorted(inorder l) \<Longrightarrow>  inorder(deleteL x l a r) =
    5.68 +    del_list x (inorder l) @ a # inorder r" and
    5.69 + "sorted(inorder r) \<Longrightarrow>  inorder(deleteR x l a r) =
    5.70 +    inorder l @ a # del_list x (inorder r)"
    5.71 +by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
    5.72 +  (auto simp: del_simps inorder_combine inorder_balL inorder_balR)
    5.73 +
    5.74 +interpretation Set_by_Ordered
    5.75 +where empty = Leaf and isin = isin and insert = insert and delete = delete
    5.76 +and inorder = inorder and wf = "\<lambda>_. True"
    5.77 +proof (standard, goal_cases)
    5.78 +  case 1 show ?case by simp
    5.79 +next
    5.80 +  case 2 thus ?case by(simp add: isin_set)
    5.81 +next
    5.82 +  case 3 thus ?case by(simp add: inorder_insert)
    5.83 +next
    5.84 +  case 4 thus ?case by(simp add: inorder_delete)
    5.85 +next
    5.86 +  case 5 thus ?case ..
    5.87 +qed
    5.88 +
    5.89 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Data_Structures/Tree2.thy	Tue Sep 22 08:38:25 2015 +0200
     6.3 @@ -0,0 +1,17 @@
     6.4 +theory Tree2
     6.5 +imports Main
     6.6 +begin
     6.7 +
     6.8 +datatype ('a,'b) tree =
     6.9 +  Leaf ("\<langle>\<rangle>") |
    6.10 +  Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("\<langle>_, _, _, _\<rangle>")
    6.11 +
    6.12 +fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
    6.13 +"inorder Leaf = []" |
    6.14 +"inorder (Node _ l a r) = inorder l @ a # inorder r"
    6.15 +
    6.16 +fun height :: "('a,'b) tree \<Rightarrow> nat" where
    6.17 +"height Leaf = 0" |
    6.18 +"height (Node _ l a r) = max (height l) (height r) + 1"
    6.19 +
    6.20 +end
    6.21 \ No newline at end of file
     7.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Mon Sep 21 23:22:11 2015 +0200
     7.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Tue Sep 22 08:38:25 2015 +0200
     7.3 @@ -33,7 +33,8 @@
     7.4  
     7.5  subsection "Functional Correctness Proofs"
     7.6  
     7.7 -lemma lookup_eq: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
     7.8 +lemma lookup_eq:
     7.9 +  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    7.10  apply (induction t)
    7.11  apply (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
    7.12  done
    7.13 @@ -41,7 +42,7 @@
    7.14  
    7.15  lemma inorder_update:
    7.16    "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
    7.17 -by(induction t) (auto simp: upd_list_sorteds sorted_lems)
    7.18 +by(induction t) (auto simp: upd_list_simps)
    7.19  
    7.20  
    7.21  lemma del_minD:
     8.1 --- a/src/HOL/Data_Structures/document/root.bib	Mon Sep 21 23:22:11 2015 +0200
     8.2 +++ b/src/HOL/Data_Structures/document/root.bib	Tue Sep 22 08:38:25 2015 +0200
     8.3 @@ -1,20 +1,12 @@
     8.4 -@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
     8.5 -@string{MIT="MIT Press"}
     8.6 -@string{Springer="Springer-Verlag"}
     8.7 -
     8.8 -@book{Nielson,author={Hanne Riis Nielson and Flemming Nielson},
     8.9 -title={Semantics with Applications},publisher={Wiley},year=1992}
    8.10 +@article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
    8.11 +journal={J. Functional Programming},volume=11,number=4,pages={425-432},year=2001}
    8.12  
    8.13 -@book{Winskel,author={Glynn Winskel},
    8.14 -title={The Formal Semantics of Programming Languages},publisher=MIT,year=1993}
    8.15 +@misc{Kahrs-html,author={Stefan Kahrs},title={Red Black Trees},
    8.16 +note={\url{http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html}}}
    8.17  
    8.18 -@inproceedings{Nipkow,author={Tobias Nipkow},
    8.19 -title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
    8.20 -booktitle=
    8.21 -{Foundations of Software Technology and Theoretical Computer Science},
    8.22 -editor={V. Chandru and V. Vinay},
    8.23 -publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
    8.24 +@book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
    8.25 +publisher="Cambridge University Press",year=1998}
    8.26  
    8.27  @book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
    8.28 -title={Concrete Semantics. A Proof Assistant Approach},publisher=Springer,
    8.29 -note={To appear}}
    8.30 +title={Concrete Semantics with Isabelle/HOL},publisher=Springer,
    8.31 +year=2014}
     9.1 --- a/src/HOL/Data_Structures/document/root.tex	Mon Sep 21 23:22:11 2015 +0200
     9.2 +++ b/src/HOL/Data_Structures/document/root.tex	Tue Sep 22 08:38:25 2015 +0200
     9.3 @@ -29,14 +29,19 @@
     9.4  of a textbook than a library of efficient algorithms.
     9.5  \end{abstract}
     9.6  
     9.7 -\setcounter{tocdepth}{2}
     9.8 +\setcounter{tocdepth}{1}
     9.9  \tableofcontents
    9.10  \newpage
    9.11  
    9.12 -% generated text of all theories
    9.13  \input{session}
    9.14  
    9.15 -%\bibliographystyle{abbrv}
    9.16 -%\bibliography{root}
    9.17 +\section{Bibliographic Notes}
    9.18 +
    9.19 +\paragraph{Red-Black trees}
    9.20 +The insert function follows Okasaki \cite{Okasaki}, the delete function
    9.21 +Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
    9.22 +
    9.23 +\bibliographystyle{abbrv}
    9.24 +\bibliography{root}
    9.25  
    9.26  \end{document}
    10.1 --- a/src/HOL/ROOT	Mon Sep 21 23:22:11 2015 +0200
    10.2 +++ b/src/HOL/ROOT	Tue Sep 22 08:38:25 2015 +0200
    10.3 @@ -176,7 +176,8 @@
    10.4    theories
    10.5      Tree_Set
    10.6      Tree_Map
    10.7 -  document_files "root.tex"
    10.8 +    RBT_Map
    10.9 +  document_files "root.tex" "root.bib"
   10.10  
   10.11  session "HOL-Import" in Import = HOL +
   10.12    theories HOL_Light_Maps