src/HOL/Data_Structures/RBT_Set.thy
changeset 61581 00d9682e8dd7
parent 61428 5e1938107371
child 61588 1d2907d0ed73
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Wed Nov 04 15:07:23 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Nov 05 08:27:14 2015 +0100
     1.3 @@ -5,26 +5,30 @@
     1.4  theory RBT_Set
     1.5  imports
     1.6    RBT
     1.7 +  Cmp
     1.8    Isin2
     1.9  begin
    1.10  
    1.11 -fun insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.12 +fun insert :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.13  "insert x Leaf = R Leaf x Leaf" |
    1.14 -"insert x (B l a r) =
    1.15 -  (if x < a then bal (insert x l) a r else
    1.16 -   if x > a then bal l a (insert x r) else B l a r)" |
    1.17 -"insert x (R l a r) =
    1.18 -  (if x < a then R (insert x l) a r
    1.19 -   else if x > a then R l a (insert x r) else R l a r)"
    1.20 +"insert x (B l a r) = (case cmp x a of
    1.21 +  LT \<Rightarrow> bal (insert x l) a r |
    1.22 +  GT \<Rightarrow> bal l a (insert x r) |
    1.23 +  EQ \<Rightarrow> B l a r)" |
    1.24 +"insert x (R l a r) = (case cmp x a of
    1.25 +  LT \<Rightarrow> R (insert x l) a r |
    1.26 +  GT \<Rightarrow> R l a (insert x r) |
    1.27 +  EQ \<Rightarrow> R l a r)"
    1.28  
    1.29 -fun delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.30 -and deleteL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.31 -and deleteR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.32 +fun delete :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.33 +and deleteL :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.34 +and deleteR :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.35  where
    1.36  "delete x Leaf = Leaf" |
    1.37 -"delete x (Node _ l a r) = 
    1.38 -  (if x < a then deleteL x l a r 
    1.39 -   else if x > a then deleteR x l a r else combine l r)" |
    1.40 +"delete x (Node _ l a r) = (case cmp x a of
    1.41 +  LT \<Rightarrow> deleteL x l a r |
    1.42 +  GT \<Rightarrow> deleteR x l a r |
    1.43 +  EQ \<Rightarrow> combine l r)" |
    1.44  "deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
    1.45  "deleteL x l a r = R (delete x l) a r" |
    1.46  "deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | 
    1.47 @@ -66,6 +70,7 @@
    1.48  by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
    1.49    (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
    1.50  
    1.51 +
    1.52  interpretation Set_by_Ordered
    1.53  where empty = Leaf and isin = isin and insert = insert and delete = delete
    1.54  and inorder = inorder and wf = "\<lambda>_. True"