src/HOL/Data_Structures/Tree_Map.thy
changeset 61581 00d9682e8dd7
parent 61534 a88e07c8d0d5
child 61640 44c9198f210c
     1.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Wed Nov 04 15:07:23 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Thu Nov 05 08:27:14 2015 +0100
     1.3 @@ -8,23 +8,24 @@
     1.4    Map_by_Ordered
     1.5  begin
     1.6  
     1.7 -fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
     1.8 +fun lookup :: "('a::cmp*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
     1.9  "lookup Leaf x = None" |
    1.10 -"lookup (Node l (a,b) r) x = (if x < a then lookup l x else
    1.11 -  if x > a then lookup r x else Some b)"
    1.12 +"lookup (Node l (a,b) r) x =
    1.13 +  (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
    1.14  
    1.15 -fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    1.16 +fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    1.17  "update x y Leaf = Node Leaf (x,y) Leaf" |
    1.18 -"update x y (Node l (a,b) r) =
    1.19 -   (if x < a then Node (update x y l) (a,b) r
    1.20 -    else if x = a then Node l (x,y) r
    1.21 -    else Node l (a,b) (update x y r))"
    1.22 +"update x y (Node l (a,b) r) = (case cmp x a of
    1.23 +   LT \<Rightarrow> Node (update x y l) (a,b) r |
    1.24 +   EQ \<Rightarrow> Node l (x,y) r |
    1.25 +   GT \<Rightarrow> Node l (a,b) (update x y r))"
    1.26  
    1.27 -fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    1.28 +fun delete :: "'a::cmp \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    1.29  "delete x Leaf = Leaf" |
    1.30 -"delete x (Node l (a,b) r) = (if x < a then Node (delete x l) (a,b) r else
    1.31 -  if x > a then Node l (a,b) (delete x r) else
    1.32 -  if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
    1.33 +"delete x (Node l (a,b) r) = (case cmp x a of
    1.34 +  LT \<Rightarrow> Node (delete x l) (a,b) r |
    1.35 +  GT \<Rightarrow> Node l (a,b) (delete x r) |
    1.36 +  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
    1.37  
    1.38  
    1.39  subsection "Functional Correctness Proofs"
    1.40 @@ -49,7 +50,6 @@
    1.41    "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    1.42  by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
    1.43  
    1.44 -
    1.45  interpretation Map_by_Ordered
    1.46  where empty = Leaf and lookup = lookup and update = update and delete = delete
    1.47  and inorder = inorder and wf = "\<lambda>_. True"