# HG changeset patch
# User nipkow
# Date 1447587928 -3600
# Node ID b594e9277be38c84e35114c4390f2a497996471f
# Parent  a97232cf19812e8379c73e2cf91398461cdba1f4
tuned white space

diff -r a97232cf1981 -r b594e9277be3 src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Sun Nov 15 11:27:55 2015 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Sun Nov 15 12:45:28 2015 +0100
@@ -27,21 +27,25 @@
 "node l a r = Node (max (ht l) (ht r) + 1) l a r"
 
 definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
-"balL l a r = (
-  if ht l = ht r + 2 then (case l of 
-    Node _ bl b br \<Rightarrow> (if ht bl < ht br
-    then case br of
-      Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
-    else node bl b (node br a r)))
-  else node l a r)"
+"balL l a r =
+  (if ht l = ht r + 2 then
+     case l of 
+       Node _ bl b br \<Rightarrow>
+         if ht bl < ht br then
+           case br of
+             Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
+         else node bl b (node br a r)
+   else node l a r)"
 
 definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
-"balR l a r = (
-  if ht r = ht l + 2 then (case r of
-    Node _ bl b br \<Rightarrow> (if ht bl > ht br
-    then case bl of
-      Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
-    else node (node l a bl) b br))
+"balR l a r =
+   (if ht r = ht l + 2 then
+      case r of
+        Node _ bl b br \<Rightarrow>
+          if ht bl > ht br then
+            case bl of
+              Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
+          else node (node l a bl) b br
   else node l a r)"
 
 fun insert :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
@@ -52,8 +56,8 @@
    GT \<Rightarrow> balR l a (insert x r))"
 
 fun del_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
-"del_max (Node _ l a r) = (if r = Leaf then (l,a)
-  else let (r',a') = del_max r in (balL l a r', a'))"
+"del_max (Node _ l a r) =
+  (if r = Leaf then (l,a) else let (r',a') = del_max r in (balL l a r', a'))"
 
 lemmas del_max_induct = del_max.induct[case_names Node Leaf]
 
@@ -66,10 +70,11 @@
 
 fun delete :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
 "delete _ Leaf = Leaf" |
-"delete x (Node h l a r) = (case cmp x a of
-   EQ \<Rightarrow> del_root (Node h l a r) |
-   LT \<Rightarrow> balR (delete x l) a r |
-   GT \<Rightarrow> balL l a (delete x r))"
+"delete x (Node h l a r) =
+  (case cmp x a of
+     EQ \<Rightarrow> del_root (Node h l a r) |
+     LT \<Rightarrow> balR (delete x l) a r |
+     GT \<Rightarrow> balL l a (delete x r))"
 
 
 subsection {* Functional Correctness Proofs *}
diff -r a97232cf1981 -r b594e9277be3 src/HOL/Data_Structures/RBT.thy
--- a/src/HOL/Data_Structures/RBT.thy	Sun Nov 15 11:27:55 2015 +0100
+++ b/src/HOL/Data_Structures/RBT.thy	Sun Nov 15 12:45:28 2015 +0100
@@ -41,12 +41,14 @@
 fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "combine Leaf t = t" |
 "combine t Leaf = t" |
-"combine (R t1 a t2) (R t3 c t4) = (case combine t2 t3 of
-    R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
-    t23 \<Rightarrow> R t1 a (R t23 c t4))" |
-"combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of
-    R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
-    t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
+"combine (R t1 a t2) (R t3 c t4) =
+  (case combine t2 t3 of
+     R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
+     t23 \<Rightarrow> R t1 a (R t23 c t4))" |
+"combine (B t1 a t2) (B t3 c t4) =
+  (case combine t2 t3 of
+     R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
+     t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
 "combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
 "combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" 
 
diff -r a97232cf1981 -r b594e9277be3 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Sun Nov 15 11:27:55 2015 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Nov 15 12:45:28 2015 +0100
@@ -11,24 +11,27 @@
 
 fun insert :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "insert x Leaf = R Leaf x Leaf" |
-"insert x (B l a r) = (case cmp x a of
-  LT \<Rightarrow> bal (insert x l) a r |
-  GT \<Rightarrow> bal l a (insert x r) |
-  EQ \<Rightarrow> B l a r)" |
-"insert x (R l a r) = (case cmp x a of
-  LT \<Rightarrow> R (insert x l) a r |
-  GT \<Rightarrow> R l a (insert x r) |
-  EQ \<Rightarrow> R l a r)"
+"insert x (B l a r) =
+  (case cmp x a of
+     LT \<Rightarrow> bal (insert x l) a r |
+     GT \<Rightarrow> bal l a (insert x r) |
+     EQ \<Rightarrow> B l a r)" |
+"insert x (R l a r) =
+  (case cmp x a of
+    LT \<Rightarrow> R (insert x l) a r |
+    GT \<Rightarrow> R l a (insert x r) |
+    EQ \<Rightarrow> R l a r)"
 
 fun delete :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
 and deleteL :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
 and deleteR :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
 where
 "delete x Leaf = Leaf" |
-"delete x (Node _ l a r) = (case cmp x a of
-  LT \<Rightarrow> deleteL x l a r |
-  GT \<Rightarrow> deleteR x l a r |
-  EQ \<Rightarrow> combine l r)" |
+"delete x (Node _ l a r) =
+  (case cmp x a of
+     LT \<Rightarrow> deleteL x l a r |
+     GT \<Rightarrow> deleteR x l a r |
+     EQ \<Rightarrow> combine l r)" |
 "deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" |
 "deleteL x l a r = R (delete x l) a r" |
 "deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | 
@@ -62,9 +65,9 @@
   (auto simp: inorder_balL inorder_balR split: tree.split color.split)
 
 lemma inorder_delete:
- "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)" and
+ "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)"
  "sorted(inorder l) \<Longrightarrow>  inorder(deleteL x l a r) =
-    del_list x (inorder l) @ a # inorder r" and
+    del_list x (inorder l) @ a # inorder r"
  "sorted(inorder r) \<Longrightarrow>  inorder(deleteR x l a r) =
     inorder l @ a # del_list x (inorder r)"
 by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
@@ -81,7 +84,7 @@
 next
   case 3 thus ?case by(simp add: inorder_insert)
 next
-  case 4 thus ?case by(simp add: inorder_delete)
+  case 4 thus ?case by(simp add: inorder_delete(1))
 qed (rule TrueI)+
 
 end
diff -r a97232cf1981 -r b594e9277be3 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Sun Nov 15 11:27:55 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sun Nov 15 12:45:28 2015 +0100
@@ -12,10 +12,19 @@
 fun isin :: "'a::cmp tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
 "isin Leaf x = False" |
 "isin (Node2 l a r) x =
-  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" |
+  (case cmp x a of
+     LT \<Rightarrow> isin l x |
+     EQ \<Rightarrow> True |
+     GT \<Rightarrow> isin r x)" |
 "isin (Node3 l a m b r) x =
-  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of
-   LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))"
+  (case cmp x a of
+     LT \<Rightarrow> isin l x |
+     EQ \<Rightarrow> True |
+     GT \<Rightarrow>
+       (case cmp x b of
+          LT \<Rightarrow> isin m x |
+          EQ \<Rightarrow> True |
+          GT \<Rightarrow> isin r x))"
 
 datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
 
@@ -27,27 +36,33 @@
 "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
 "ins x (Node2 l a r) =
    (case cmp x a of
-      LT \<Rightarrow> (case ins x l of
-              T\<^sub>i l' => T\<^sub>i (Node2 l' a r)
-            | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
+      LT \<Rightarrow>
+        (case ins x l of
+           T\<^sub>i l' => T\<^sub>i (Node2 l' a r) |
+           Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
       EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
-      GT \<Rightarrow> (case ins x r of
-              T\<^sub>i r' => T\<^sub>i (Node2 l a r')
-            | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
+      GT \<Rightarrow>
+        (case ins x r of
+           T\<^sub>i r' => T\<^sub>i (Node2 l a r') |
+           Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
 "ins x (Node3 l a m b r) =
    (case cmp x a of
-      LT \<Rightarrow> (case ins x l of
-              T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r)
-            | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
+      LT \<Rightarrow>
+        (case ins x l of
+           T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) |
+           Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
       EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
-      GT \<Rightarrow> (case cmp x b of
-               GT \<Rightarrow> (case ins x r of
-                       T\<^sub>i r' => T\<^sub>i (Node3 l a m b r')
-                     | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
-               EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
-               LT \<Rightarrow> (case ins x m of
-                       T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r)
-                     | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))"
+      GT \<Rightarrow>
+        (case cmp x b of
+           GT \<Rightarrow>
+             (case ins x r of
+                T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') |
+                Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
+           EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
+           LT \<Rightarrow>
+             (case ins x m of
+                T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) |
+                Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))"
 
 hide_const insert
 
@@ -93,20 +108,25 @@
 "del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
 "del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
 
-fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d"
-where
+fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
 "del x Leaf = T\<^sub>d Leaf" |
-"del x (Node2 Leaf a Leaf) = (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
-"del x (Node3 Leaf a Leaf b Leaf) = T\<^sub>d(if x = a then Node2 Leaf b Leaf
-  else if x = b then Node2 Leaf a Leaf else Node3 Leaf a Leaf b Leaf)" |
-"del x (Node2 l a r) = (case cmp x a of
-  LT \<Rightarrow> node21 (del x l) a r |
-  GT \<Rightarrow> node22 l a (del x r) |
-  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
-"del x (Node3 l a m b r) = (case cmp x a of
-  LT \<Rightarrow> node31 (del x l) a m b r |
-  EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
-  GT \<Rightarrow> (case cmp x b of
+"del x (Node2 Leaf a Leaf) =
+  (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
+"del x (Node3 Leaf a Leaf b Leaf) =
+  T\<^sub>d(if x = a then Node2 Leaf b Leaf else
+     if x = b then Node2 Leaf a Leaf
+     else Node3 Leaf a Leaf b Leaf)" |
+"del x (Node2 l a r) =
+  (case cmp x a of
+     LT \<Rightarrow> node21 (del x l) a r |
+     GT \<Rightarrow> node22 l a (del x r) |
+     EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
+"del x (Node3 l a m b r) =
+  (case cmp x a of
+     LT \<Rightarrow> node31 (del x l) a m b r |
+     EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
+     GT \<Rightarrow>
+       (case cmp x b of
           LT \<Rightarrow> node32 l a (del x m) b r |
           EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
           GT \<Rightarrow> node33 l a m b (del x r)))"
diff -r a97232cf1981 -r b594e9277be3 src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Sun Nov 15 11:27:55 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Sun Nov 15 12:45:28 2015 +0100
@@ -12,27 +12,32 @@
 fun isin :: "'a::cmp tree \<Rightarrow> 'a \<Rightarrow> bool" where
 "isin Leaf x = False" |
 "isin (Node l a r) x =
-  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)"
+  (case cmp x a of
+     LT \<Rightarrow> isin l x |
+     EQ \<Rightarrow> True |
+     GT \<Rightarrow> isin r x)"
 
 hide_const (open) insert
 
 fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "insert x Leaf = Node Leaf x Leaf" |
-"insert x (Node l a r) = (case cmp x a of
-      LT \<Rightarrow> Node (insert x l) a r |
-      EQ \<Rightarrow> Node l a r |
-      GT \<Rightarrow> Node l a (insert x r))"
+"insert x (Node l a r) =
+  (case cmp x a of
+     LT \<Rightarrow> Node (insert x l) a r |
+     EQ \<Rightarrow> Node l a r |
+     GT \<Rightarrow> Node l a (insert x r))"
 
 fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
-"del_min (Node l a r) = (if l = Leaf then (a,r)
-  else let (x,l') = del_min l in (x, Node l' a r))"
+"del_min (Node l a r) =
+  (if l = Leaf then (a,r) else let (x,l') = del_min l in (x, Node l' a r))"
 
 fun delete :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "delete x Leaf = Leaf" |
-"delete x (Node l a r) = (case cmp x a of
-  LT \<Rightarrow>  Node (delete x l) a r |
-  GT \<Rightarrow>  Node l a (delete x r) |
-  EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
+"delete x (Node l a r) =
+  (case cmp x a of
+     LT \<Rightarrow>  Node (delete x l) a r |
+     GT \<Rightarrow>  Node l a (delete x r) |
+     EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
 
 
 subsection "Functional Correctness Proofs"