# 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 \ 'a \ 'a avl_tree \ 'a avl_tree" where -"balL l a r = ( - if ht l = ht r + 2 then (case l of - Node _ bl b br \ (if ht bl < ht br - then case br of - Node _ cl c cr \ 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 \ + if ht bl < ht br then + case br of + Node _ cl c cr \ 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 \ 'a \ 'a avl_tree \ 'a avl_tree" where -"balR l a r = ( - if ht r = ht l + 2 then (case r of - Node _ bl b br \ (if ht bl > ht br - then case bl of - Node _ cl c cr \ 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 \ + if ht bl > ht br then + case bl of + Node _ cl c cr \ 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 \ 'a avl_tree \ 'a avl_tree" where @@ -52,8 +56,8 @@ GT \ balR l a (insert x r))" fun del_max :: "'a avl_tree \ '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 \ 'a avl_tree \ 'a avl_tree" where "delete _ Leaf = Leaf" | -"delete x (Node h l a r) = (case cmp x a of - EQ \ del_root (Node h l a r) | - LT \ balR (delete x l) a r | - GT \ balL l a (delete x r))" +"delete x (Node h l a r) = + (case cmp x a of + EQ \ del_root (Node h l a r) | + LT \ balR (delete x l) a r | + GT \ 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 \ 'a rbt \ '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 \ (R (R t1 a u2) b (R u3 c t4)) | - t23 \ 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' \ R (B t1 a t2') b (B t3' c t4) | - t23 \ 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 \ (R (R t1 a u2) b (R u3 c t4)) | + t23 \ 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' \ R (B t1 a t2') b (B t3' c t4) | + t23 \ 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 \ 'a rbt \ 'a rbt" where "insert x Leaf = R Leaf x Leaf" | -"insert x (B l a r) = (case cmp x a of - LT \ bal (insert x l) a r | - GT \ bal l a (insert x r) | - EQ \ B l a r)" | -"insert x (R l a r) = (case cmp x a of - LT \ R (insert x l) a r | - GT \ R l a (insert x r) | - EQ \ R l a r)" +"insert x (B l a r) = + (case cmp x a of + LT \ bal (insert x l) a r | + GT \ bal l a (insert x r) | + EQ \ B l a r)" | +"insert x (R l a r) = + (case cmp x a of + LT \ R (insert x l) a r | + GT \ R l a (insert x r) | + EQ \ R l a r)" fun delete :: "'a::cmp \ 'a rbt \ 'a rbt" and deleteL :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" and deleteR :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" where "delete x Leaf = Leaf" | -"delete x (Node _ l a r) = (case cmp x a of - LT \ deleteL x l a r | - GT \ deleteR x l a r | - EQ \ combine l r)" | +"delete x (Node _ l a r) = + (case cmp x a of + LT \ deleteL x l a r | + GT \ deleteR x l a r | + EQ \ 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) \ inorder(delete x t) = del_list x (inorder t)" and + "sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" "sorted(inorder l) \ 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) \ 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 \ 'a \ bool" where "isin Leaf x = False" | "isin (Node2 l a r) x = - (case cmp x a of LT \ isin l x | EQ \ True | GT \ isin r x)" | + (case cmp x a of + LT \ isin l x | + EQ \ True | + GT \ isin r x)" | "isin (Node3 l a m b r) x = - (case cmp x a of LT \ isin l x | EQ \ True | GT \ (case cmp x b of - LT \ isin m x | EQ \ True | GT \ isin r x))" + (case cmp x a of + LT \ isin l x | + EQ \ True | + GT \ + (case cmp x b of + LT \ isin m x | + EQ \ True | + GT \ 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 \ (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 \ + (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 \ T\<^sub>i (Node2 l x r) | - GT \ (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 \ + (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 \ (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 \ + (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 \ T\<^sub>i (Node3 l a m b r) | - GT \ (case cmp x b of - GT \ (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 \ T\<^sub>i (Node3 l a m b r) | - LT \ (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 \ + (case cmp x b of + GT \ + (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 \ T\<^sub>i (Node3 l a m b r) | + LT \ + (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 \ 'a tree23 \ 'a up\<^sub>d" -where +fun del :: "'a::cmp \ 'a tree23 \ '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 \ node21 (del x l) a r | - GT \ node22 l a (del x r) | - EQ \ 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 \ node31 (del x l) a m b r | - EQ \ let (a',m') = del_min m in node32 l a' m' b r | - GT \ (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 \ node21 (del x l) a r | + GT \ node22 l a (del x r) | + EQ \ 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 \ node31 (del x l) a m b r | + EQ \ let (a',m') = del_min m in node32 l a' m' b r | + GT \ + (case cmp x b of LT \ node32 l a (del x m) b r | EQ \ let (b',r') = del_min r in node33 l a m b' r' | GT \ 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 \ 'a \ bool" where "isin Leaf x = False" | "isin (Node l a r) x = - (case cmp x a of LT \ isin l x | EQ \ True | GT \ isin r x)" + (case cmp x a of + LT \ isin l x | + EQ \ True | + GT \ isin r x)" hide_const (open) insert fun insert :: "'a::cmp \ 'a tree \ 'a tree" where "insert x Leaf = Node Leaf x Leaf" | -"insert x (Node l a r) = (case cmp x a of - LT \ Node (insert x l) a r | - EQ \ Node l a r | - GT \ Node l a (insert x r))" +"insert x (Node l a r) = + (case cmp x a of + LT \ Node (insert x l) a r | + EQ \ Node l a r | + GT \ Node l a (insert x r))" fun del_min :: "'a tree \ '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 \ 'a tree \ 'a tree" where "delete x Leaf = Leaf" | -"delete x (Node l a r) = (case cmp x a of - LT \ Node (delete x l) a r | - GT \ Node l a (delete x r) | - EQ \ 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 \ Node (delete x l) a r | + GT \ Node l a (delete x r) | + EQ \ if r = Leaf then l else let (a',r') = del_min r in Node l a' r')" subsection "Functional Correctness Proofs"