src/HOL/Data_Structures/Tree_Set.thy
changeset 61678 b594e9277be3
parent 61651 415e816d3f37
child 63411 e051eea34990
     1.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Sun Nov 15 11:27:55 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Sun Nov 15 12:45:28 2015 +0100
     1.3 @@ -12,27 +12,32 @@
     1.4  fun isin :: "'a::cmp tree \<Rightarrow> 'a \<Rightarrow> bool" where
     1.5  "isin Leaf x = False" |
     1.6  "isin (Node l a r) x =
     1.7 -  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)"
     1.8 +  (case cmp x a of
     1.9 +     LT \<Rightarrow> isin l x |
    1.10 +     EQ \<Rightarrow> True |
    1.11 +     GT \<Rightarrow> isin r x)"
    1.12  
    1.13  hide_const (open) insert
    1.14  
    1.15  fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    1.16  "insert x Leaf = Node Leaf x Leaf" |
    1.17 -"insert x (Node l a r) = (case cmp x a of
    1.18 -      LT \<Rightarrow> Node (insert x l) a r |
    1.19 -      EQ \<Rightarrow> Node l a r |
    1.20 -      GT \<Rightarrow> Node l a (insert x r))"
    1.21 +"insert x (Node l a r) =
    1.22 +  (case cmp x a of
    1.23 +     LT \<Rightarrow> Node (insert x l) a r |
    1.24 +     EQ \<Rightarrow> Node l a r |
    1.25 +     GT \<Rightarrow> Node l a (insert x r))"
    1.26  
    1.27  fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
    1.28 -"del_min (Node l a r) = (if l = Leaf then (a,r)
    1.29 -  else let (x,l') = del_min l in (x, Node l' a r))"
    1.30 +"del_min (Node l a r) =
    1.31 +  (if l = Leaf then (a,r) else let (x,l') = del_min l in (x, Node l' a r))"
    1.32  
    1.33  fun delete :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    1.34  "delete x Leaf = Leaf" |
    1.35 -"delete x (Node l a r) = (case cmp x a of
    1.36 -  LT \<Rightarrow>  Node (delete x l) a r |
    1.37 -  GT \<Rightarrow>  Node l a (delete x r) |
    1.38 -  EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
    1.39 +"delete x (Node l a r) =
    1.40 +  (case cmp x a of
    1.41 +     LT \<Rightarrow>  Node (delete x l) a r |
    1.42 +     GT \<Rightarrow>  Node l a (delete x r) |
    1.43 +     EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
    1.44  
    1.45  
    1.46  subsection "Functional Correctness Proofs"