src/HOL/Data_Structures/Tree_Map.thy
changeset 63411 e051eea34990
parent 61790 0494964bb226
child 67965 aaa31cd0caef
     1.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Thu Jul 07 09:24:03 2016 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Thu Jul 07 18:08:02 2016 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Author: Tobias Nipkow *)
     1.5  
     1.6 -section {* Unbalanced Tree as Map *}
     1.7 +section \<open>Unbalanced Tree Implementation of Map\<close>
     1.8  
     1.9  theory Tree_Map
    1.10  imports
    1.11 @@ -8,19 +8,19 @@
    1.12    Map_by_Ordered
    1.13  begin
    1.14  
    1.15 -fun lookup :: "('a::cmp*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
    1.16 +fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
    1.17  "lookup Leaf x = None" |
    1.18  "lookup (Node l (a,b) r) x =
    1.19    (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
    1.20  
    1.21 -fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    1.22 +fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    1.23  "update x y Leaf = Node Leaf (x,y) Leaf" |
    1.24  "update x y (Node l (a,b) r) = (case cmp x a of
    1.25     LT \<Rightarrow> Node (update x y l) (a,b) r |
    1.26     EQ \<Rightarrow> Node l (x,y) r |
    1.27     GT \<Rightarrow> Node l (a,b) (update x y r))"
    1.28  
    1.29 -fun delete :: "'a::cmp \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    1.30 +fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    1.31  "delete x Leaf = Leaf" |
    1.32  "delete x (Node l (a,b) r) = (case cmp x a of
    1.33    LT \<Rightarrow> Node (delete x l) (a,b) r |