# HG changeset patch
# User nipkow
# Date 1442903905 -7200
# Node ID 759b5299a9f2c271168cf353b34dd1726bc9525f
# Parent  dfccf6c06201c5d7e1b7d9cdb63784340b1023f6
added red black trees

diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/Data_Structures/AList_Upd_Del.thy
--- a/src/HOL/Data_Structures/AList_Upd_Del.thy	Mon Sep 21 23:22:11 2015 +0200
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Tue Sep 22 08:38:25 2015 +0200
@@ -77,7 +77,7 @@
   upd_list a b (ps @ (x,y) # qs) = ps @ upd_list a b ((x,y)#qs)"
 by(induction ps) (auto simp: sorted_lems)
 
-lemmas upd_list_sorteds = upd_list_sorted1 upd_list_sorted2
+lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2
 
 (*
 lemma set_ins_list[simp]: "set (ins_list x xs) = insert x (set xs)"
diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/Data_Structures/Isin2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Isin2.thy	Tue Sep 22 08:38:25 2015 +0200
@@ -0,0 +1,21 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Function \textit{isin} for Tree2\<close>
+
+theory Isin2
+imports
+  Tree2
+  Set_by_Ordered
+begin
+
+fun isin :: "('a,'b) tree \<Rightarrow> ('a::order) \<Rightarrow> bool" where
+"isin Leaf x = False" |
+"isin (Node _ l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)"
+
+lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
+by (induction t) (auto simp: elems_simps)
+
+lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
+by (induction t) (auto simp: elems_simps dest: sortedD)
+
+end
\ No newline at end of file
diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/Data_Structures/RBT.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/RBT.thy	Tue Sep 22 08:38:25 2015 +0200
@@ -0,0 +1,53 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Red-Black Trees\<close>
+
+theory RBT
+imports Tree2
+begin
+
+datatype color = Red | Black
+
+type_synonym 'a rbt = "('a,color)tree"
+
+abbreviation R where "R l a r \<equiv> Node Red l a r"
+abbreviation B where "B l a r \<equiv> Node Black l a r"
+
+fun bal :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+(* The first line is superfluous; it merely speeds up pattern compilation *)
+"bal (R t1 a1 t2) a2 (R t3 a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"bal (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"bal (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"bal t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"bal t1 a t2 = B t1 a t2"
+
+fun red :: "'a rbt \<Rightarrow> 'a rbt" where
+"red Leaf = Leaf" |
+"red (Node _ l a r) = R l a r"
+
+fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"balL (R t1 x t2) s t3 = R (B t1 x t2) s t3" |
+"balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" |
+"balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (red t3))" |
+"balL t1 x t2 = R t1 x t2"
+
+fun balR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
+"balR (B t1 x t2) y bl = bal (R t1 x t2) y bl" |
+"balR (R t1 x (B t2 y t3)) z bl = R (bal (red t1) x t2) y (B t3 z bl)" |
+"balR t1 x t2 = R t1 x t2"
+
+fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"combine Leaf t = t" |
+"combine t Leaf = t" |
+"combine (R a x b) (R c y d) = (case combine b c of
+    R b2 z c2 \<Rightarrow> (R (R a x b2) z (R c2 y d)) |
+    bc \<Rightarrow> R a x (R bc y d))" |
+"combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of
+    R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
+    t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
+"combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
+"combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" 
+
+end
diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/Data_Structures/RBT_Map.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/RBT_Map.thy	Tue Sep 22 08:38:25 2015 +0200
@@ -0,0 +1,79 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Red-Black Tree Implementation of Maps\<close>
+
+theory RBT_Map
+imports
+  RBT_Set
+  Map_by_Ordered
+begin
+
+fun lookup :: "('a::linorder * 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b option" where
+"lookup Leaf x = None" |
+"lookup (Node _ l (a,b) r) x =
+  (if x < a then lookup l x else
+   if x > a then lookup r x else Some b)"
+
+fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
+"update x y Leaf = R Leaf (x,y) Leaf" |
+"update x y (B l (a,b) r) =
+  (if x < a then bal (update x y l) (a,b) r else
+   if x > a then bal l (a,b) (update x y r)
+   else B l (x,y) r)" |
+"update x y (R l (a,b) r) =
+  (if x < a then R (update x y l) (a,b) r else
+   if x > a then R l (a,b) (update x y r)
+   else R l (x,y) r)"
+
+fun delete :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
+and deleteL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
+and deleteR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
+where
+"delete x Leaf = Leaf" |
+"delete x (Node c t1 (a,b) t2) = 
+  (if x < a then deleteL x t1 (a,b) t2 else
+   if x > a then deleteR x t1 (a,b) t2 else combine t1 t2)" |
+"deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
+"deleteL x t1 a t2 = R (delete x t1) a t2" |
+"deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | 
+"deleteR x t1 a t2 = R t1 a (delete x t2)"
+
+
+subsection "Functional Correctness Proofs"
+
+lemma lookup_eq:
+  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
+by(induction t)
+  (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
+
+
+lemma inorder_update:
+  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
+by(induction x y t rule: update.induct)
+  (auto simp: upd_list_simps inorder_bal)
+
+
+lemma inorder_delete:
+ "sorted1(inorder t1) \<Longrightarrow>  inorder(delete x t1) = del_list x (inorder t1)" and
+ "sorted1(inorder t1) \<Longrightarrow>  inorder(deleteL x t1 a t2) =
+    del_list x (inorder t1) @ a # inorder t2" and
+ "sorted1(inorder t2) \<Longrightarrow>  inorder(deleteR x t1 a t2) =
+    inorder t1 @ a # del_list x (inorder t2)"
+by(induction x t1 and x t1 a t2 and x t1 a t2 rule: delete_deleteL_deleteR.induct)
+  (auto simp: del_list_sorted sorted_lems inorder_combine inorder_balL inorder_balR)
+
+
+interpretation Map_by_Ordered
+where empty = Leaf and lookup = lookup and update = update and delete = delete
+and inorder = inorder and wf = "\<lambda>_. True"
+proof (standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case 2 thus ?case by(simp add: lookup_eq)
+next
+  case 3 thus ?case by(simp add: inorder_update)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+qed (rule TrueI)+
+
+end
diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/Data_Structures/RBT_Set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Tue Sep 22 08:38:25 2015 +0200
@@ -0,0 +1,86 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Red-Black Tree Implementation of Sets\<close>
+
+theory RBT_Set
+imports
+  RBT
+  Isin2
+begin
+
+fun insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"insert x Leaf = R Leaf x Leaf" |
+"insert x (B l a r) =
+  (if x < a then bal (insert x l) a r else
+   if x > a then bal l a (insert x r) else B l a r)" |
+"insert x (R l a r) =
+  (if x < a then R (insert x l) a r
+   else if x > a then R l a (insert x r) else R l a r)"
+
+fun delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
+and deleteL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
+and deleteR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
+where
+"delete x Leaf = Leaf" |
+"delete x (Node _ l a r) = 
+  (if x < a then deleteL x l a r 
+   else if x > a then deleteR x l a r else combine l r)" |
+"deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
+"deleteL x l a r = R (delete x l) a r" |
+"deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | 
+"deleteR x l a r = R l a (delete x r)"
+
+
+subsection "Functional Correctness Proofs"
+
+lemma inorder_bal:
+  "inorder(bal l a r) = inorder l @ a # inorder r"
+by(induction l a r rule: bal.induct) (auto simp: sorted_lems)
+
+lemma inorder_insert:
+  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
+by(induction a t rule: insert.induct) (auto simp: ins_simps inorder_bal)
+
+lemma inorder_red: "inorder(red t) = inorder t"
+by(induction t) (auto simp: sorted_lems)
+
+lemma inorder_balL:
+  "inorder(balL l a r) = inorder l @ a # inorder r"
+by(induction l a r rule: balL.induct)
+  (auto simp: sorted_lems inorder_bal inorder_red)
+
+lemma inorder_balR:
+  "inorder(balR l a r) = inorder l @ a # inorder r"
+by(induction l a r rule: balR.induct)
+  (auto simp: sorted_lems inorder_bal inorder_red)
+
+lemma inorder_combine:
+  "inorder(combine l r) = inorder l @ inorder r"
+by(induction l r rule: combine.induct)
+  (auto simp: sorted_lems inorder_balL inorder_balR split: tree.split color.split)
+
+lemma inorder_delete:
+ "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)" and
+ "sorted(inorder l) \<Longrightarrow>  inorder(deleteL x l a r) =
+    del_list x (inorder l) @ a # inorder r" and
+ "sorted(inorder r) \<Longrightarrow>  inorder(deleteR x l a r) =
+    inorder l @ a # del_list x (inorder r)"
+by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
+  (auto simp: del_simps inorder_combine inorder_balL inorder_balR)
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete
+and inorder = inorder and wf = "\<lambda>_. True"
+proof (standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case 2 thus ?case by(simp add: isin_set)
+next
+  case 3 thus ?case by(simp add: inorder_insert)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+next
+  case 5 thus ?case ..
+qed
+
+end
diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/Data_Structures/Tree2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Tree2.thy	Tue Sep 22 08:38:25 2015 +0200
@@ -0,0 +1,17 @@
+theory Tree2
+imports Main
+begin
+
+datatype ('a,'b) tree =
+  Leaf ("\<langle>\<rangle>") |
+  Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("\<langle>_, _, _, _\<rangle>")
+
+fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
+"inorder Leaf = []" |
+"inorder (Node _ l a r) = inorder l @ a # inorder r"
+
+fun height :: "('a,'b) tree \<Rightarrow> nat" where
+"height Leaf = 0" |
+"height (Node _ l a r) = max (height l) (height r) + 1"
+
+end
\ No newline at end of file
diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/Data_Structures/Tree_Map.thy
--- a/src/HOL/Data_Structures/Tree_Map.thy	Mon Sep 21 23:22:11 2015 +0200
+++ b/src/HOL/Data_Structures/Tree_Map.thy	Tue Sep 22 08:38:25 2015 +0200
@@ -33,7 +33,8 @@
 
 subsection "Functional Correctness Proofs"
 
-lemma lookup_eq: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
+lemma lookup_eq:
+  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
 apply (induction t)
 apply (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
 done
@@ -41,7 +42,7 @@
 
 lemma inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
-by(induction t) (auto simp: upd_list_sorteds sorted_lems)
+by(induction t) (auto simp: upd_list_simps)
 
 
 lemma del_minD:
diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/Data_Structures/document/root.bib
--- a/src/HOL/Data_Structures/document/root.bib	Mon Sep 21 23:22:11 2015 +0200
+++ b/src/HOL/Data_Structures/document/root.bib	Tue Sep 22 08:38:25 2015 +0200
@@ -1,20 +1,12 @@
-@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
-@string{MIT="MIT Press"}
-@string{Springer="Springer-Verlag"}
-
-@book{Nielson,author={Hanne Riis Nielson and Flemming Nielson},
-title={Semantics with Applications},publisher={Wiley},year=1992}
+@article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
+journal={J. Functional Programming},volume=11,number=4,pages={425-432},year=2001}
 
-@book{Winskel,author={Glynn Winskel},
-title={The Formal Semantics of Programming Languages},publisher=MIT,year=1993}
+@misc{Kahrs-html,author={Stefan Kahrs},title={Red Black Trees},
+note={\url{http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html}}}
 
-@inproceedings{Nipkow,author={Tobias Nipkow},
-title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
-booktitle=
-{Foundations of Software Technology and Theoretical Computer Science},
-editor={V. Chandru and V. Vinay},
-publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
+@book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
+publisher="Cambridge University Press",year=1998}
 
 @book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
-title={Concrete Semantics. A Proof Assistant Approach},publisher=Springer,
-note={To appear}}
+title={Concrete Semantics with Isabelle/HOL},publisher=Springer,
+year=2014}
diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/Data_Structures/document/root.tex
--- a/src/HOL/Data_Structures/document/root.tex	Mon Sep 21 23:22:11 2015 +0200
+++ b/src/HOL/Data_Structures/document/root.tex	Tue Sep 22 08:38:25 2015 +0200
@@ -29,14 +29,19 @@
 of a textbook than a library of efficient algorithms.
 \end{abstract}
 
-\setcounter{tocdepth}{2}
+\setcounter{tocdepth}{1}
 \tableofcontents
 \newpage
 
-% generated text of all theories
 \input{session}
 
-%\bibliographystyle{abbrv}
-%\bibliography{root}
+\section{Bibliographic Notes}
+
+\paragraph{Red-Black trees}
+The insert function follows Okasaki \cite{Okasaki}, the delete function
+Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
+
+\bibliographystyle{abbrv}
+\bibliography{root}
 
 \end{document}
diff -r dfccf6c06201 -r 759b5299a9f2 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Sep 21 23:22:11 2015 +0200
+++ b/src/HOL/ROOT	Tue Sep 22 08:38:25 2015 +0200
@@ -176,7 +176,8 @@
   theories
     Tree_Set
     Tree_Map
-  document_files "root.tex"
+    RBT_Map
+  document_files "root.tex" "root.bib"
 
 session "HOL-Import" in Import = HOL +
   theories HOL_Light_Maps