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 *}
```