src/HOL/Data_Structures/AVL_Set.thy
changeset 61678 b594e9277be3
parent 61647 5121b9a57cce
child 62526 347150095fd2
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Sun Nov 15 11:27:55 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Sun Nov 15 12:45:28 2015 +0100
     1.3 @@ -27,21 +27,25 @@
     1.4  "node l a r = Node (max (ht l) (ht r) + 1) l a r"
     1.5  
     1.6  definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
     1.7 -"balL l a r = (
     1.8 -  if ht l = ht r + 2 then (case l of 
     1.9 -    Node _ bl b br \<Rightarrow> (if ht bl < ht br
    1.10 -    then case br of
    1.11 -      Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
    1.12 -    else node bl b (node br a r)))
    1.13 -  else node l a r)"
    1.14 +"balL l a r =
    1.15 +  (if ht l = ht r + 2 then
    1.16 +     case l of 
    1.17 +       Node _ bl b br \<Rightarrow>
    1.18 +         if ht bl < ht br then
    1.19 +           case br of
    1.20 +             Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
    1.21 +         else node bl b (node br a r)
    1.22 +   else node l a r)"
    1.23  
    1.24  definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.25 -"balR l a r = (
    1.26 -  if ht r = ht l + 2 then (case r of
    1.27 -    Node _ bl b br \<Rightarrow> (if ht bl > ht br
    1.28 -    then case bl of
    1.29 -      Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
    1.30 -    else node (node l a bl) b br))
    1.31 +"balR l a r =
    1.32 +   (if ht r = ht l + 2 then
    1.33 +      case r of
    1.34 +        Node _ bl b br \<Rightarrow>
    1.35 +          if ht bl > ht br then
    1.36 +            case bl of
    1.37 +              Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
    1.38 +          else node (node l a bl) b br
    1.39    else node l a r)"
    1.40  
    1.41  fun insert :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.42 @@ -52,8 +56,8 @@
    1.43     GT \<Rightarrow> balR l a (insert x r))"
    1.44  
    1.45  fun del_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
    1.46 -"del_max (Node _ l a r) = (if r = Leaf then (l,a)
    1.47 -  else let (r',a') = del_max r in (balL l a r', a'))"
    1.48 +"del_max (Node _ l a r) =
    1.49 +  (if r = Leaf then (l,a) else let (r',a') = del_max r in (balL l a r', a'))"
    1.50  
    1.51  lemmas del_max_induct = del_max.induct[case_names Node Leaf]
    1.52  
    1.53 @@ -66,10 +70,11 @@
    1.54  
    1.55  fun delete :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.56  "delete _ Leaf = Leaf" |
    1.57 -"delete x (Node h l a r) = (case cmp x a of
    1.58 -   EQ \<Rightarrow> del_root (Node h l a r) |
    1.59 -   LT \<Rightarrow> balR (delete x l) a r |
    1.60 -   GT \<Rightarrow> balL l a (delete x r))"
    1.61 +"delete x (Node h l a r) =
    1.62 +  (case cmp x a of
    1.63 +     EQ \<Rightarrow> del_root (Node h l a r) |
    1.64 +     LT \<Rightarrow> balR (delete x l) a r |
    1.65 +     GT \<Rightarrow> balL l a (delete x r))"
    1.66  
    1.67  
    1.68  subsection {* Functional Correctness Proofs *}