tuned white space
authornipkow
Sun Nov 15 12:45:28 2015 +0100 (2015-11-15)
changeset 61678b594e9277be3
parent 61677 a97232cf1981
child 61679 1335462046e8
child 61682 f2c69a221055
tuned white space
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Data_Structures/RBT.thy
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/Data_Structures/Tree_Set.thy
     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 *}
     2.1 --- a/src/HOL/Data_Structures/RBT.thy	Sun Nov 15 11:27:55 2015 +0100
     2.2 +++ b/src/HOL/Data_Structures/RBT.thy	Sun Nov 15 12:45:28 2015 +0100
     2.3 @@ -41,12 +41,14 @@
     2.4  fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
     2.5  "combine Leaf t = t" |
     2.6  "combine t Leaf = t" |
     2.7 -"combine (R t1 a t2) (R t3 c t4) = (case combine t2 t3 of
     2.8 -    R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
     2.9 -    t23 \<Rightarrow> R t1 a (R t23 c t4))" |
    2.10 -"combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of
    2.11 -    R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
    2.12 -    t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
    2.13 +"combine (R t1 a t2) (R t3 c t4) =
    2.14 +  (case combine t2 t3 of
    2.15 +     R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
    2.16 +     t23 \<Rightarrow> R t1 a (R t23 c t4))" |
    2.17 +"combine (B t1 a t2) (B t3 c t4) =
    2.18 +  (case combine t2 t3 of
    2.19 +     R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
    2.20 +     t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
    2.21  "combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
    2.22  "combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" 
    2.23  
     3.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sun Nov 15 11:27:55 2015 +0100
     3.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Nov 15 12:45:28 2015 +0100
     3.3 @@ -11,24 +11,27 @@
     3.4  
     3.5  fun insert :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
     3.6  "insert x Leaf = R Leaf x Leaf" |
     3.7 -"insert x (B l a r) = (case cmp x a of
     3.8 -  LT \<Rightarrow> bal (insert x l) a r |
     3.9 -  GT \<Rightarrow> bal l a (insert x r) |
    3.10 -  EQ \<Rightarrow> B l a r)" |
    3.11 -"insert x (R l a r) = (case cmp x a of
    3.12 -  LT \<Rightarrow> R (insert x l) a r |
    3.13 -  GT \<Rightarrow> R l a (insert x r) |
    3.14 -  EQ \<Rightarrow> R l a r)"
    3.15 +"insert x (B l a r) =
    3.16 +  (case cmp x a of
    3.17 +     LT \<Rightarrow> bal (insert x l) a r |
    3.18 +     GT \<Rightarrow> bal l a (insert x r) |
    3.19 +     EQ \<Rightarrow> B l a r)" |
    3.20 +"insert x (R l a r) =
    3.21 +  (case cmp x a of
    3.22 +    LT \<Rightarrow> R (insert x l) a r |
    3.23 +    GT \<Rightarrow> R l a (insert x r) |
    3.24 +    EQ \<Rightarrow> R l a r)"
    3.25  
    3.26  fun delete :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    3.27  and deleteL :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    3.28  and deleteR :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    3.29  where
    3.30  "delete x Leaf = Leaf" |
    3.31 -"delete x (Node _ l a r) = (case cmp x a of
    3.32 -  LT \<Rightarrow> deleteL x l a r |
    3.33 -  GT \<Rightarrow> deleteR x l a r |
    3.34 -  EQ \<Rightarrow> combine l r)" |
    3.35 +"delete x (Node _ l a r) =
    3.36 +  (case cmp x a of
    3.37 +     LT \<Rightarrow> deleteL x l a r |
    3.38 +     GT \<Rightarrow> deleteR x l a r |
    3.39 +     EQ \<Rightarrow> combine l r)" |
    3.40  "deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
    3.41  "deleteL x l a r = R (delete x l) a r" |
    3.42  "deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | 
    3.43 @@ -62,9 +65,9 @@
    3.44    (auto simp: inorder_balL inorder_balR split: tree.split color.split)
    3.45  
    3.46  lemma inorder_delete:
    3.47 - "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)" and
    3.48 + "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)"
    3.49   "sorted(inorder l) \<Longrightarrow>  inorder(deleteL x l a r) =
    3.50 -    del_list x (inorder l) @ a # inorder r" and
    3.51 +    del_list x (inorder l) @ a # inorder r"
    3.52   "sorted(inorder r) \<Longrightarrow>  inorder(deleteR x l a r) =
    3.53      inorder l @ a # del_list x (inorder r)"
    3.54  by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
    3.55 @@ -81,7 +84,7 @@
    3.56  next
    3.57    case 3 thus ?case by(simp add: inorder_insert)
    3.58  next
    3.59 -  case 4 thus ?case by(simp add: inorder_delete)
    3.60 +  case 4 thus ?case by(simp add: inorder_delete(1))
    3.61  qed (rule TrueI)+
    3.62  
    3.63  end
     4.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Sun Nov 15 11:27:55 2015 +0100
     4.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sun Nov 15 12:45:28 2015 +0100
     4.3 @@ -12,10 +12,19 @@
     4.4  fun isin :: "'a::cmp tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
     4.5  "isin Leaf x = False" |
     4.6  "isin (Node2 l a r) x =
     4.7 -  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" |
     4.8 +  (case cmp x a of
     4.9 +     LT \<Rightarrow> isin l x |
    4.10 +     EQ \<Rightarrow> True |
    4.11 +     GT \<Rightarrow> isin r x)" |
    4.12  "isin (Node3 l a m b r) x =
    4.13 -  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of
    4.14 -   LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))"
    4.15 +  (case cmp x a of
    4.16 +     LT \<Rightarrow> isin l x |
    4.17 +     EQ \<Rightarrow> True |
    4.18 +     GT \<Rightarrow>
    4.19 +       (case cmp x b of
    4.20 +          LT \<Rightarrow> isin m x |
    4.21 +          EQ \<Rightarrow> True |
    4.22 +          GT \<Rightarrow> isin r x))"
    4.23  
    4.24  datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
    4.25  
    4.26 @@ -27,27 +36,33 @@
    4.27  "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
    4.28  "ins x (Node2 l a r) =
    4.29     (case cmp x a of
    4.30 -      LT \<Rightarrow> (case ins x l of
    4.31 -              T\<^sub>i l' => T\<^sub>i (Node2 l' a r)
    4.32 -            | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
    4.33 +      LT \<Rightarrow>
    4.34 +        (case ins x l of
    4.35 +           T\<^sub>i l' => T\<^sub>i (Node2 l' a r) |
    4.36 +           Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
    4.37        EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
    4.38 -      GT \<Rightarrow> (case ins x r of
    4.39 -              T\<^sub>i r' => T\<^sub>i (Node2 l a r')
    4.40 -            | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
    4.41 +      GT \<Rightarrow>
    4.42 +        (case ins x r of
    4.43 +           T\<^sub>i r' => T\<^sub>i (Node2 l a r') |
    4.44 +           Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
    4.45  "ins x (Node3 l a m b r) =
    4.46     (case cmp x a of
    4.47 -      LT \<Rightarrow> (case ins x l of
    4.48 -              T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r)
    4.49 -            | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
    4.50 +      LT \<Rightarrow>
    4.51 +        (case ins x l of
    4.52 +           T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) |
    4.53 +           Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
    4.54        EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    4.55 -      GT \<Rightarrow> (case cmp x b of
    4.56 -               GT \<Rightarrow> (case ins x r of
    4.57 -                       T\<^sub>i r' => T\<^sub>i (Node3 l a m b r')
    4.58 -                     | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
    4.59 -               EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    4.60 -               LT \<Rightarrow> (case ins x m of
    4.61 -                       T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r)
    4.62 -                     | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))"
    4.63 +      GT \<Rightarrow>
    4.64 +        (case cmp x b of
    4.65 +           GT \<Rightarrow>
    4.66 +             (case ins x r of
    4.67 +                T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') |
    4.68 +                Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
    4.69 +           EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    4.70 +           LT \<Rightarrow>
    4.71 +             (case ins x m of
    4.72 +                T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) |
    4.73 +                Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))"
    4.74  
    4.75  hide_const insert
    4.76  
    4.77 @@ -93,20 +108,25 @@
    4.78  "del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
    4.79  "del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
    4.80  
    4.81 -fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d"
    4.82 -where
    4.83 +fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    4.84  "del x Leaf = T\<^sub>d Leaf" |
    4.85 -"del x (Node2 Leaf a Leaf) = (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
    4.86 -"del x (Node3 Leaf a Leaf b Leaf) = T\<^sub>d(if x = a then Node2 Leaf b Leaf
    4.87 -  else if x = b then Node2 Leaf a Leaf else Node3 Leaf a Leaf b Leaf)" |
    4.88 -"del x (Node2 l a r) = (case cmp x a of
    4.89 -  LT \<Rightarrow> node21 (del x l) a r |
    4.90 -  GT \<Rightarrow> node22 l a (del x r) |
    4.91 -  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
    4.92 -"del x (Node3 l a m b r) = (case cmp x a of
    4.93 -  LT \<Rightarrow> node31 (del x l) a m b r |
    4.94 -  EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
    4.95 -  GT \<Rightarrow> (case cmp x b of
    4.96 +"del x (Node2 Leaf a Leaf) =
    4.97 +  (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
    4.98 +"del x (Node3 Leaf a Leaf b Leaf) =
    4.99 +  T\<^sub>d(if x = a then Node2 Leaf b Leaf else
   4.100 +     if x = b then Node2 Leaf a Leaf
   4.101 +     else Node3 Leaf a Leaf b Leaf)" |
   4.102 +"del x (Node2 l a r) =
   4.103 +  (case cmp x a of
   4.104 +     LT \<Rightarrow> node21 (del x l) a r |
   4.105 +     GT \<Rightarrow> node22 l a (del x r) |
   4.106 +     EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
   4.107 +"del x (Node3 l a m b r) =
   4.108 +  (case cmp x a of
   4.109 +     LT \<Rightarrow> node31 (del x l) a m b r |
   4.110 +     EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
   4.111 +     GT \<Rightarrow>
   4.112 +       (case cmp x b of
   4.113            LT \<Rightarrow> node32 l a (del x m) b r |
   4.114            EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
   4.115            GT \<Rightarrow> node33 l a m b (del x r)))"
     5.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Sun Nov 15 11:27:55 2015 +0100
     5.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Sun Nov 15 12:45:28 2015 +0100
     5.3 @@ -12,27 +12,32 @@
     5.4  fun isin :: "'a::cmp tree \<Rightarrow> 'a \<Rightarrow> bool" where
     5.5  "isin Leaf x = False" |
     5.6  "isin (Node l a r) x =
     5.7 -  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)"
     5.8 +  (case cmp x a of
     5.9 +     LT \<Rightarrow> isin l x |
    5.10 +     EQ \<Rightarrow> True |
    5.11 +     GT \<Rightarrow> isin r x)"
    5.12  
    5.13  hide_const (open) insert
    5.14  
    5.15  fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    5.16  "insert x Leaf = Node Leaf x Leaf" |
    5.17 -"insert x (Node l a r) = (case cmp x a of
    5.18 -      LT \<Rightarrow> Node (insert x l) a r |
    5.19 -      EQ \<Rightarrow> Node l a r |
    5.20 -      GT \<Rightarrow> Node l a (insert x r))"
    5.21 +"insert x (Node l a r) =
    5.22 +  (case cmp x a of
    5.23 +     LT \<Rightarrow> Node (insert x l) a r |
    5.24 +     EQ \<Rightarrow> Node l a r |
    5.25 +     GT \<Rightarrow> Node l a (insert x r))"
    5.26  
    5.27  fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
    5.28 -"del_min (Node l a r) = (if l = Leaf then (a,r)
    5.29 -  else let (x,l') = del_min l in (x, Node l' a r))"
    5.30 +"del_min (Node l a r) =
    5.31 +  (if l = Leaf then (a,r) else let (x,l') = del_min l in (x, Node l' a r))"
    5.32  
    5.33  fun delete :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    5.34  "delete x Leaf = Leaf" |
    5.35 -"delete x (Node l a r) = (case cmp x a of
    5.36 -  LT \<Rightarrow>  Node (delete x l) a r |
    5.37 -  GT \<Rightarrow>  Node l a (delete x r) |
    5.38 -  EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
    5.39 +"delete x (Node l a r) =
    5.40 +  (case cmp x a of
    5.41 +     LT \<Rightarrow>  Node (delete x l) a r |
    5.42 +     GT \<Rightarrow>  Node l a (delete x r) |
    5.43 +     EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
    5.44  
    5.45  
    5.46  subsection "Functional Correctness Proofs"