src/HOL/Library/RBT_Impl.thy
changeset 61225 1a690dce8cfc
parent 61121 efe8b18306b7
child 61433 a4c0de1df3d8
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Sep 22 08:38:25 2015 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Sep 22 14:31:22 2015 +0200
     1.3 @@ -331,6 +331,8 @@
     1.4  
     1.5  subsection \<open>Insertion\<close>
     1.6  
     1.7 +text \<open>The function definitions are based on the book by Okasaki.\<close>
     1.8 +
     1.9  fun (* slow, due to massive case splitting *)
    1.10    balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
    1.11  where
    1.12 @@ -554,6 +556,9 @@
    1.13  lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
    1.14  by (cases t rule: rbt_cases) auto
    1.15  
    1.16 +text \<open>The function definitions are based on the Haskell code by Stefan Kahrs
    1.17 +at @{url "http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html"} .\<close>
    1.18 +
    1.19  fun
    1.20    balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
    1.21  where