src/HOL/Data_Structures/RBT_Set.thy
changeset 61678 b594e9277be3
parent 61588 1d2907d0ed73
child 61749 7f530d7e552d
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sun Nov 15 11:27:55 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Nov 15 12:45:28 2015 +0100
     1.3 @@ -11,24 +11,27 @@
     1.4  
     1.5  fun insert :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
     1.6  "insert x Leaf = R Leaf x Leaf" |
     1.7 -"insert x (B l a r) = (case cmp x a of
     1.8 -  LT \<Rightarrow> bal (insert x l) a r |
     1.9 -  GT \<Rightarrow> bal l a (insert x r) |
    1.10 -  EQ \<Rightarrow> B l a r)" |
    1.11 -"insert x (R l a r) = (case cmp x a of
    1.12 -  LT \<Rightarrow> R (insert x l) a r |
    1.13 -  GT \<Rightarrow> R l a (insert x r) |
    1.14 -  EQ \<Rightarrow> R l a r)"
    1.15 +"insert x (B l a r) =
    1.16 +  (case cmp x a of
    1.17 +     LT \<Rightarrow> bal (insert x l) a r |
    1.18 +     GT \<Rightarrow> bal l a (insert x r) |
    1.19 +     EQ \<Rightarrow> B l a r)" |
    1.20 +"insert x (R l a r) =
    1.21 +  (case cmp x a of
    1.22 +    LT \<Rightarrow> R (insert x l) a r |
    1.23 +    GT \<Rightarrow> R l a (insert x r) |
    1.24 +    EQ \<Rightarrow> R l a r)"
    1.25  
    1.26  fun delete :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.27  and deleteL :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.28  and deleteR :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.29  where
    1.30  "delete x Leaf = Leaf" |
    1.31 -"delete x (Node _ l a r) = (case cmp x a of
    1.32 -  LT \<Rightarrow> deleteL x l a r |
    1.33 -  GT \<Rightarrow> deleteR x l a r |
    1.34 -  EQ \<Rightarrow> combine l r)" |
    1.35 +"delete x (Node _ l a r) =
    1.36 +  (case cmp x a of
    1.37 +     LT \<Rightarrow> deleteL x l a r |
    1.38 +     GT \<Rightarrow> deleteR x l a r |
    1.39 +     EQ \<Rightarrow> combine l r)" |
    1.40  "deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
    1.41  "deleteL x l a r = R (delete x l) a r" |
    1.42  "deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | 
    1.43 @@ -62,9 +65,9 @@
    1.44    (auto simp: inorder_balL inorder_balR split: tree.split color.split)
    1.45  
    1.46  lemma inorder_delete:
    1.47 - "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)" and
    1.48 + "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)"
    1.49   "sorted(inorder l) \<Longrightarrow>  inorder(deleteL x l a r) =
    1.50 -    del_list x (inorder l) @ a # inorder r" and
    1.51 +    del_list x (inorder l) @ a # inorder r"
    1.52   "sorted(inorder r) \<Longrightarrow>  inorder(deleteR x l a r) =
    1.53      inorder l @ a # del_list x (inorder r)"
    1.54  by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
    1.55 @@ -81,7 +84,7 @@
    1.56  next
    1.57    case 3 thus ?case by(simp add: inorder_insert)
    1.58  next
    1.59 -  case 4 thus ?case by(simp add: inorder_delete)
    1.60 +  case 4 thus ?case by(simp add: inorder_delete(1))
    1.61  qed (rule TrueI)+
    1.62  
    1.63  end