src/HOL/Data_Structures/Tree23_Set.thy
changeset 61678 b594e9277be3
parent 61640 44c9198f210c
child 61709 47f7263870a0
     1.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Sun Nov 15 11:27:55 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sun Nov 15 12:45:28 2015 +0100
     1.3 @@ -12,10 +12,19 @@
     1.4  fun isin :: "'a::cmp tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
     1.5  "isin Leaf x = False" |
     1.6  "isin (Node2 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  "isin (Node3 l a m b r) x =
    1.13 -  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of
    1.14 -   LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))"
    1.15 +  (case cmp x a of
    1.16 +     LT \<Rightarrow> isin l x |
    1.17 +     EQ \<Rightarrow> True |
    1.18 +     GT \<Rightarrow>
    1.19 +       (case cmp x b of
    1.20 +          LT \<Rightarrow> isin m x |
    1.21 +          EQ \<Rightarrow> True |
    1.22 +          GT \<Rightarrow> isin r x))"
    1.23  
    1.24  datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
    1.25  
    1.26 @@ -27,27 +36,33 @@
    1.27  "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
    1.28  "ins x (Node2 l a r) =
    1.29     (case cmp x a of
    1.30 -      LT \<Rightarrow> (case ins x l of
    1.31 -              T\<^sub>i l' => T\<^sub>i (Node2 l' a r)
    1.32 -            | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
    1.33 +      LT \<Rightarrow>
    1.34 +        (case ins x l of
    1.35 +           T\<^sub>i l' => T\<^sub>i (Node2 l' a r) |
    1.36 +           Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
    1.37        EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
    1.38 -      GT \<Rightarrow> (case ins x r of
    1.39 -              T\<^sub>i r' => T\<^sub>i (Node2 l a r')
    1.40 -            | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
    1.41 +      GT \<Rightarrow>
    1.42 +        (case ins x r of
    1.43 +           T\<^sub>i r' => T\<^sub>i (Node2 l a r') |
    1.44 +           Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
    1.45  "ins x (Node3 l a m b r) =
    1.46     (case cmp x a of
    1.47 -      LT \<Rightarrow> (case ins x l of
    1.48 -              T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r)
    1.49 -            | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
    1.50 +      LT \<Rightarrow>
    1.51 +        (case ins x l of
    1.52 +           T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) |
    1.53 +           Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
    1.54        EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    1.55 -      GT \<Rightarrow> (case cmp x b of
    1.56 -               GT \<Rightarrow> (case ins x r of
    1.57 -                       T\<^sub>i r' => T\<^sub>i (Node3 l a m b r')
    1.58 -                     | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
    1.59 -               EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    1.60 -               LT \<Rightarrow> (case ins x m of
    1.61 -                       T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r)
    1.62 -                     | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))"
    1.63 +      GT \<Rightarrow>
    1.64 +        (case cmp x b of
    1.65 +           GT \<Rightarrow>
    1.66 +             (case ins x r of
    1.67 +                T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') |
    1.68 +                Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
    1.69 +           EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    1.70 +           LT \<Rightarrow>
    1.71 +             (case ins x m of
    1.72 +                T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) |
    1.73 +                Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))"
    1.74  
    1.75  hide_const insert
    1.76  
    1.77 @@ -93,20 +108,25 @@
    1.78  "del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
    1.79  "del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
    1.80  
    1.81 -fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d"
    1.82 -where
    1.83 +fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    1.84  "del x Leaf = T\<^sub>d Leaf" |
    1.85 -"del x (Node2 Leaf a Leaf) = (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
    1.86 -"del x (Node3 Leaf a Leaf b Leaf) = T\<^sub>d(if x = a then Node2 Leaf b Leaf
    1.87 -  else if x = b then Node2 Leaf a Leaf else Node3 Leaf a Leaf b Leaf)" |
    1.88 -"del x (Node2 l a r) = (case cmp x a of
    1.89 -  LT \<Rightarrow> node21 (del x l) a r |
    1.90 -  GT \<Rightarrow> node22 l a (del x r) |
    1.91 -  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
    1.92 -"del x (Node3 l a m b r) = (case cmp x a of
    1.93 -  LT \<Rightarrow> node31 (del x l) a m b r |
    1.94 -  EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
    1.95 -  GT \<Rightarrow> (case cmp x b of
    1.96 +"del x (Node2 Leaf a Leaf) =
    1.97 +  (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
    1.98 +"del x (Node3 Leaf a Leaf b Leaf) =
    1.99 +  T\<^sub>d(if x = a then Node2 Leaf b Leaf else
   1.100 +     if x = b then Node2 Leaf a Leaf
   1.101 +     else Node3 Leaf a Leaf b Leaf)" |
   1.102 +"del x (Node2 l a r) =
   1.103 +  (case cmp x a of
   1.104 +     LT \<Rightarrow> node21 (del x l) a r |
   1.105 +     GT \<Rightarrow> node22 l a (del x r) |
   1.106 +     EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
   1.107 +"del x (Node3 l a m b r) =
   1.108 +  (case cmp x a of
   1.109 +     LT \<Rightarrow> node31 (del x l) a m b r |
   1.110 +     EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
   1.111 +     GT \<Rightarrow>
   1.112 +       (case cmp x b of
   1.113            LT \<Rightarrow> node32 l a (del x m) b r |
   1.114            EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
   1.115            GT \<Rightarrow> node33 l a m b (del x r)))"