# HG changeset patch # User nipkow # Date 1467907690 -7200 # Node ID def97df48390daca8d829f9f8eb9f36346e3cdaf # Parent 9789ccc2a477724791d0cd4607976426dd32a7d0# Parent e051eea34990bf89f425f177160e75524ec6d328 merged diff -r 9789ccc2a477 -r def97df48390 CONTRIBUTORS --- a/CONTRIBUTORS Thu Jul 07 17:34:39 2016 +0200 +++ b/CONTRIBUTORS Thu Jul 07 18:08:10 2016 +0200 @@ -20,6 +20,9 @@ * June 2016: Andreas Lochbihler Formalisation of discrete subprobability distributions. +* July 2016: Daniel Stuewe + Height-size proofs in HOL/Data_Structures + Contributions to Isabelle2016 ----------------------------- diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/AA_Map.thy --- a/src/HOL/Data_Structures/AA_Map.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/AA_Map.thy Thu Jul 07 18:08:10 2016 +0200 @@ -8,7 +8,7 @@ Lookup2 begin -fun update :: "'a::cmp \ 'b \ ('a*'b) aa_tree \ ('a*'b) aa_tree" where +fun update :: "'a::linorder \ 'b \ ('a*'b) aa_tree \ ('a*'b) aa_tree" where "update x y Leaf = Node 1 Leaf (x,y) Leaf" | "update x y (Node lv t1 (a,b) t2) = (case cmp x a of @@ -16,7 +16,7 @@ GT \ split (skew (Node lv t1 (a,b) (update x y t2))) | EQ \ Node lv t1 (x,y) t2)" -fun delete :: "'a::cmp \ ('a*'b) aa_tree \ ('a*'b) aa_tree" where +fun delete :: "'a::linorder \ ('a*'b) aa_tree \ ('a*'b) aa_tree" where "delete _ Leaf = Leaf" | "delete x (Node lv l (a,b) r) = (case cmp x a of diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/AA_Set.thy --- a/src/HOL/Data_Structures/AA_Set.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/AA_Set.thy Thu Jul 07 18:08:10 2016 +0200 @@ -1,5 +1,5 @@ (* -Author: Tobias Nipkow and Daniel Stüwe +Author: Tobias Nipkow, Daniel Stüwe *) section \AA Tree Implementation of Sets\ @@ -36,7 +36,7 @@ hide_const (open) insert -fun insert :: "'a::cmp \ 'a aa_tree \ 'a aa_tree" where +fun insert :: "'a::linorder \ 'a aa_tree \ 'a aa_tree" where "insert x Leaf = Node 1 Leaf x Leaf" | "insert x (Node lv t1 a t2) = (case cmp x a of @@ -81,7 +81,7 @@ "del_max (Node lv l a Leaf) = (l,a)" | "del_max (Node lv l a r) = (let (r',b) = del_max r in (adjust(Node lv l a r'), b))" -fun delete :: "'a::cmp \ 'a aa_tree \ 'a aa_tree" where +fun delete :: "'a::linorder \ 'a aa_tree \ 'a aa_tree" where "delete _ Leaf = Leaf" | "delete x (Node lv l a r) = (case cmp x a of diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/AVL_Map.thy --- a/src/HOL/Data_Structures/AVL_Map.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/AVL_Map.thy Thu Jul 07 18:08:10 2016 +0200 @@ -8,14 +8,14 @@ Lookup2 begin -fun update :: "'a::cmp \ 'b \ ('a*'b) avl_tree \ ('a*'b) avl_tree" where +fun update :: "'a::linorder \ 'b \ ('a*'b) avl_tree \ ('a*'b) avl_tree" where "update x y Leaf = Node 1 Leaf (x,y) Leaf" | "update x y (Node h l (a,b) r) = (case cmp x a of EQ \ Node h l (x,y) r | LT \ balL (update x y l) (a,b) r | GT \ balR l (a,b) (update x y r))" -fun delete :: "'a::cmp \ ('a*'b) avl_tree \ ('a*'b) avl_tree" where +fun delete :: "'a::linorder \ ('a*'b) avl_tree \ ('a*'b) avl_tree" where "delete _ Leaf = Leaf" | "delete x (Node h l (a,b) r) = (case cmp x a of EQ \ del_root (Node h l (a,b) r) | diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/AVL_Set.thy --- a/src/HOL/Data_Structures/AVL_Set.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/AVL_Set.thy Thu Jul 07 18:08:10 2016 +0200 @@ -1,12 +1,15 @@ (* -Author: Tobias Nipkow -Derived from AFP entry AVL. +Author: Tobias Nipkow, Daniel Stüwe +Largely derived from AFP entry AVL. *) section "AVL Tree Implementation of Sets" theory AVL_Set -imports Cmp Isin2 +imports + Cmp + Isin2 + "~~/src/HOL/Number_Theory/Fib" begin type_synonym 'a avl_tree = "('a,nat) tree" @@ -48,7 +51,7 @@ else node (node l a bl) b br else node l a r)" -fun insert :: "'a::cmp \ 'a avl_tree \ 'a avl_tree" where +fun insert :: "'a::linorder \ 'a avl_tree \ 'a avl_tree" where "insert x Leaf = Node 1 Leaf x Leaf" | "insert x (Node h l a r) = (case cmp x a of EQ \ Node h l a r | @@ -68,7 +71,7 @@ lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node] -fun delete :: "'a::cmp \ 'a avl_tree \ 'a avl_tree" where +fun delete :: "'a::linorder \ 'a avl_tree \ 'a avl_tree" where "delete _ Leaf = Leaf" | "delete x (Node h l a r) = (case cmp x a of @@ -449,4 +452,83 @@ qed qed simp_all + +subsection \Height-Size Relation\ + +text \By Daniel St\"uwe\ + +fun fib_tree :: "nat \ unit avl_tree" where +"fib_tree 0 = Leaf" | +"fib_tree (Suc 0) = Node 1 Leaf () Leaf" | +"fib_tree (Suc(Suc n)) = Node (Suc(Suc(n))) (fib_tree (Suc n)) () (fib_tree n)" + +lemma [simp]: "ht (fib_tree h) = h" +by (induction h rule: "fib_tree.induct") auto + +lemma [simp]: "height (fib_tree h) = h" +by (induction h rule: "fib_tree.induct") auto + +lemma "avl(fib_tree h)" +by (induction h rule: "fib_tree.induct") auto + +lemma fib_tree_size1: "size1 (fib_tree h) = fib (h+2)" +by (induction h rule: fib_tree.induct) auto + +lemma height_invers[simp]: + "(height t = 0) = (t = Leaf)" + "avl t \ (height t = Suc h) = (\ l a r . t = Node (Suc h) l a r)" +by (induction t) auto + +lemma fib_Suc_lt: "fib n \ fib (Suc n)" +by (induction n rule: fib.induct) auto + +lemma fib_mono: "n \ m \ fib n \ fib m" +proof (induction n arbitrary: m rule: fib.induct ) + case (2 m) + thus ?case using fib_neq_0_nat[of m] by auto +next + case (3 n m) + from 3 obtain m' where "m = Suc (Suc m')" + by (metis le_Suc_ex plus_nat.simps(2)) + thus ?case using 3(1)[of "Suc m'"] 3(2)[of m'] 3(3) by auto +qed simp + +lemma size1_fib_tree_mono: + assumes "n \ m" + shows "size1 (fib_tree n) \ size1 (fib_tree m)" +using fib_tree_size1 fib_mono[OF assms] fib_mono[of "Suc n"] add_le_mono assms by fastforce + +lemma fib_tree_minimal: "avl t \ size1 (fib_tree (ht t)) \ size1 t" +proof (induction "ht t" arbitrary: t rule: fib_tree.induct) + case (2 t) + from 2 obtain l a r where "t = Node (Suc 0) l a r" by (cases t) auto + with 2 show ?case by auto +next + case (3 h t) + note [simp] = 3(3)[symmetric] + from 3 obtain l a r where [simp]: "t = Node (Suc (Suc h)) l a r" by (cases t) auto + show ?case proof (cases rule: linorder_cases[of "ht l" "ht r"]) + case equal + with 3(3,4) have ht: "ht l = Suc h" "ht r = Suc h" by auto + with 3 have "size1 (fib_tree (ht l)) \ size1 l" by auto moreover + from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \ size1 r" by auto ultimately + show ?thesis using ht size1_fib_tree_mono[of h "Suc h"] by auto + next + case greater + with 3(3,4) have ht: "ht l = Suc h" "ht r = h" by auto + from ht 3(1,2,4) have "size1 (fib_tree (Suc h)) \ size1 l" by auto moreover + from ht 3(1,2,4) have "size1 (fib_tree h) \ size1 r" by auto ultimately + show ?thesis by auto + next + case less (* analogously *) + with 3 have ht: "ht l = h" "Suc h = ht r" by auto + from ht 3 have "size1 (fib_tree h) \ size1 l" by auto moreover + from ht 3 have "size1 (fib_tree (Suc h)) \ size1 r" by auto ultimately + show ?thesis by auto + qed +qed auto + +theorem avl_size_bound: "avl t \ fib(height t + 2) \ size1 t" +using fib_tree_minimal fib_tree_size1 by fastforce + end diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/Brother12_Map.thy --- a/src/HOL/Data_Structures/Brother12_Map.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/Brother12_Map.thy Thu Jul 07 18:08:10 2016 +0200 @@ -8,7 +8,7 @@ Map_by_Ordered begin -fun lookup :: "('a \ 'b) bro \ 'a::cmp \ 'b option" where +fun lookup :: "('a \ 'b) bro \ 'a::linorder \ 'b option" where "lookup N0 x = None" | "lookup (N1 t) x = lookup t x" | "lookup (N2 l (a,b) r) x = @@ -20,7 +20,7 @@ locale update = insert begin -fun upd :: "'a::cmp \ 'b \ ('a\'b) bro \ ('a\'b) bro" where +fun upd :: "'a::linorder \ 'b \ ('a\'b) bro \ ('a\'b) bro" where "upd x y N0 = L2 (x,y)" | "upd x y (N1 t) = n1 (upd x y t)" | "upd x y (N2 l (a,b) r) = @@ -29,7 +29,7 @@ EQ \ N2 l (a,y) r | GT \ n2 l (a,b) (upd x y r))" -definition update :: "'a::cmp \ 'b \ ('a\'b) bro \ ('a\'b) bro" where +definition update :: "'a::linorder \ 'b \ ('a\'b) bro \ ('a\'b) bro" where "update x y t = tree(upd x y t)" end @@ -37,7 +37,7 @@ context delete begin -fun del :: "'a::cmp \ ('a\'b) bro \ ('a\'b) bro" where +fun del :: "'a::linorder \ ('a\'b) bro \ ('a\'b) bro" where "del _ N0 = N0" | "del x (N1 t) = N1 (del x t)" | "del x (N2 l (a,b) r) = @@ -48,7 +48,7 @@ None \ N1 l | Some (ab, r') \ n2 l ab r'))" -definition delete :: "'a::cmp \ ('a\'b) bro \ ('a\'b) bro" where +definition delete :: "'a::linorder \ ('a\'b) bro \ ('a\'b) bro" where "delete a t = tree (del a t)" end @@ -180,7 +180,7 @@ show ?thesis by simp qed qed - } ultimately show ?case by auto + } ultimately show ?case by auto } { case 2 with Suc.IH(1) show ?case by auto } qed auto diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/Brother12_Set.thy --- a/src/HOL/Data_Structures/Brother12_Set.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/Brother12_Set.thy Thu Jul 07 18:08:10 2016 +0200 @@ -1,4 +1,4 @@ -(* Author: Tobias Nipkow *) +(* Author: Tobias Nipkow, Daniel Stüwe *) section \1-2 Brother Tree Implementation of Sets\ @@ -6,6 +6,7 @@ imports Cmp Set_by_Ordered + "~~/src/HOL/Number_Theory/Fib" begin subsection \Data Type and Operations\ @@ -25,7 +26,7 @@ "inorder (L2 a) = [a]" | "inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3" -fun isin :: "'a bro \ 'a::cmp \ bool" where +fun isin :: "'a bro \ 'a::linorder \ bool" where "isin N0 x = False" | "isin (N1 t) x = isin t x" | "isin (N2 l a r) x = @@ -53,7 +54,7 @@ "n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" | "n2 t1 a t2 = N2 t1 a t2" -fun ins :: "'a::cmp \ 'a bro \ 'a bro" where +fun ins :: "'a::linorder \ 'a bro \ 'a bro" where "ins x N0 = L2 x" | "ins x (N1 t) = n1 (ins x t)" | "ins x (N2 l a r) = @@ -67,7 +68,7 @@ "tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" | "tree t = t" -definition insert :: "'a::cmp \ 'a bro \ 'a bro" where +definition insert :: "'a::linorder \ 'a bro \ 'a bro" where "insert x t = tree(ins x t)" end @@ -102,7 +103,7 @@ None \ Some (a, N1 t2) | Some (b, t1') \ Some (b, n2 t1' a t2))" -fun del :: "'a::cmp \ 'a bro \ 'a bro" where +fun del :: "'a::linorder \ 'a bro \ 'a bro" where "del _ N0 = N0" | "del x (N1 t) = N1 (del x t)" | "del x (N2 l a r) = @@ -117,7 +118,7 @@ "tree (N1 t) = t" | "tree t = t" -definition delete :: "'a::cmp \ 'a bro \ 'a bro" where +definition delete :: "'a::linorder \ 'a bro \ 'a bro" where "delete a t = tree (del a t)" end @@ -483,4 +484,68 @@ case 7 thus ?case using delete.delete_type by blast qed auto + +subsection \Height-Size Relation\ + +text \By Daniel St\"uwe\ + +fun fib_tree :: "nat \ unit bro" where + "fib_tree 0 = N0" +| "fib_tree (Suc 0) = N2 N0 () N0" +| "fib_tree (Suc(Suc h)) = N2 (fib_tree (h+1)) () (N1 (fib_tree h))" + +fun fib' :: "nat \ nat" where + "fib' 0 = 0" +| "fib' (Suc 0) = 1" +| "fib' (Suc(Suc h)) = 1 + fib' (Suc h) + fib' h" + +fun size :: "'a bro \ nat" where + "size N0 = 0" +| "size (N1 t) = size t" +| "size (N2 t1 _ t2) = 1 + size t1 + size t2" + +lemma fib_tree_B: "fib_tree h \ B h" +by (induction h rule: fib_tree.induct) auto + +declare [[names_short]] + +lemma size_fib': "size (fib_tree h) = fib' h" +by (induction h rule: fib_tree.induct) auto + +lemma fibfib: "fib' h + 1 = fib (Suc(Suc h))" +by (induction h rule: fib_tree.induct) auto + +lemma B_N2_cases[consumes 1]: +assumes "N2 t1 a t2 \ B (Suc n)" +obtains + (BB) "t1 \ B n" and "t2 \ B n" | + (UB) "t1 \ U n" and "t2 \ B n" | + (BU) "t1 \ B n" and "t2 \ U n" +using assms by auto + +lemma size_bounded: "t \ B h \ size t \ size (fib_tree h)" +unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct) +case (3 h t') + note main = 3 + then obtain t1 a t2 where t': "t' = N2 t1 a t2" by auto + with main have "N2 t1 a t2 \ B (Suc (Suc h))" by auto + thus ?case proof (cases rule: B_N2_cases) + case BB + then obtain x y z where t2: "t2 = N2 x y z \ t2 = N2 z y x" "x \ B h" by auto + show ?thesis unfolding t' using main(1)[OF BB(1)] main(2)[OF t2(2)] t2(1) by auto + next + case UB + then obtain t11 where t1: "t1 = N1 t11" "t11 \ B h" by auto + show ?thesis unfolding t' t1(1) using main(2)[OF t1(2)] main(1)[OF UB(2)] by simp + next + case BU + then obtain t22 where t2: "t2 = N1 t22" "t22 \ B h" by auto + show ?thesis unfolding t' t2(1) using main(2)[OF t2(2)] main(1)[OF BU(1)] by simp + qed +qed auto + +theorem "t \ B h \ fib (h + 2) \ size t + 1" +using size_bounded +by (simp add: size_fib' fibfib[symmetric] del: fib.simps) + end diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/Cmp.thy --- a/src/HOL/Data_Structures/Cmp.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/Cmp.thy Thu Jul 07 18:08:10 2016 +0200 @@ -1,4 +1,4 @@ -(* Author: Tobias Nipkow *) +(* Author: Tobias Nipkow, Daniel Stüwe *) section {* Three-Way Comparison *} @@ -6,16 +6,23 @@ imports Main begin -datatype cmp = LT | EQ | GT +datatype cmp_val = LT | EQ | GT -class cmp = linorder + -fixes cmp :: "'a \ 'a \ cmp" -assumes LT[simp]: "cmp x y = LT \ x < y" -assumes EQ[simp]: "cmp x y = EQ \ x = y" -assumes GT[simp]: "cmp x y = GT \ x > y" +function cmp :: "'a:: linorder \ 'a \ cmp_val" where +"x < y \ cmp x y = LT" | +"x = y \ cmp x y = EQ" | +"x > y \ cmp x y = GT" +by (auto, force) +termination by lexicographic_order + +lemma + LT[simp]: "cmp x y = LT \ x < y" +and EQ[simp]: "cmp x y = EQ \ x = y" +and GT[simp]: "cmp x y = GT \ x > y" +by (cases x y rule: linorder_cases, auto)+ lemma case_cmp_if[simp]: "(case c of EQ \ e | LT \ l | GT \ g) = (if c = LT then l else if c = GT then g else e)" -by(simp split: cmp.split) +by(simp split: cmp_val.split) end diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/Isin2.thy --- a/src/HOL/Data_Structures/Isin2.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/Isin2.thy Thu Jul 07 18:08:10 2016 +0200 @@ -9,7 +9,7 @@ Set_by_Ordered begin -fun isin :: "('a::cmp,'b) tree \ 'a \ bool" where +fun isin :: "('a::linorder,'b) tree \ 'a \ bool" where "isin Leaf x = False" | "isin (Node _ l a r) x = (case cmp x a of diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/Lookup2.thy --- a/src/HOL/Data_Structures/Lookup2.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/Lookup2.thy Thu Jul 07 18:08:10 2016 +0200 @@ -9,7 +9,7 @@ Map_by_Ordered begin -fun lookup :: "('a::cmp * 'b, 'c) tree \ 'a \ 'b option" where +fun lookup :: "('a::linorder * 'b, 'c) tree \ 'a \ 'b option" where "lookup Leaf x = None" | "lookup (Node _ l (a,b) r) x = (case cmp x a of LT \ lookup l x | GT \ lookup r x | EQ \ Some b)" diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/RBT_Map.thy --- a/src/HOL/Data_Structures/RBT_Map.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/RBT_Map.thy Thu Jul 07 18:08:10 2016 +0200 @@ -8,7 +8,7 @@ Lookup2 begin -fun upd :: "'a::cmp \ 'b \ ('a*'b) rbt \ ('a*'b) rbt" where +fun upd :: "'a::linorder \ 'b \ ('a*'b) rbt \ ('a*'b) rbt" where "upd x y Leaf = R Leaf (x,y) Leaf" | "upd x y (B l (a,b) r) = (case cmp x a of LT \ bal (upd x y l) (a,b) r | @@ -19,12 +19,12 @@ GT \ R l (a,b) (upd x y r) | EQ \ R l (x,y) r)" -definition update :: "'a::cmp \ 'b \ ('a*'b) rbt \ ('a*'b) rbt" where +definition update :: "'a::linorder \ 'b \ ('a*'b) rbt \ ('a*'b) rbt" where "update x y t = paint Black (upd x y t)" -fun del :: "'a::cmp \ ('a*'b)rbt \ ('a*'b)rbt" -and delL :: "'a::cmp \ ('a*'b)rbt \ 'a*'b \ ('a*'b)rbt \ ('a*'b)rbt" -and delR :: "'a::cmp \ ('a*'b)rbt \ 'a*'b \ ('a*'b)rbt \ ('a*'b)rbt" +fun del :: "'a::linorder \ ('a*'b)rbt \ ('a*'b)rbt" +and delL :: "'a::linorder \ ('a*'b)rbt \ 'a*'b \ ('a*'b)rbt \ ('a*'b)rbt" +and delR :: "'a::linorder \ ('a*'b)rbt \ 'a*'b \ ('a*'b)rbt \ ('a*'b)rbt" where "del x Leaf = Leaf" | "del x (Node c t1 (a,b) t2) = (case cmp x a of @@ -36,7 +36,7 @@ "delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | "delR x t1 a t2 = R t1 a (del x t2)" -definition delete :: "'a::cmp \ ('a*'b) rbt \ ('a*'b) rbt" where +definition delete :: "'a::linorder \ ('a*'b) rbt \ ('a*'b) rbt" where "delete x t = paint Black (del x t)" diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/RBT_Set.thy --- a/src/HOL/Data_Structures/RBT_Set.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/RBT_Set.thy Thu Jul 07 18:08:10 2016 +0200 @@ -1,4 +1,4 @@ -(* Author: Tobias Nipkow *) +(* Author: Tobias Nipkow, Daniel Stüwe *) section \Red-Black Tree Implementation of Sets\ @@ -9,7 +9,7 @@ Isin2 begin -fun ins :: "'a::cmp \ 'a rbt \ 'a rbt" where +fun ins :: "'a::linorder \ 'a rbt \ 'a rbt" where "ins x Leaf = R Leaf x Leaf" | "ins x (B l a r) = (case cmp x a of @@ -22,12 +22,12 @@ GT \ R l a (ins x r) | EQ \ R l a r)" -definition insert :: "'a::cmp \ 'a rbt \ 'a rbt" where +definition insert :: "'a::linorder \ 'a rbt \ 'a rbt" where "insert x t = paint Black (ins x t)" -fun del :: "'a::cmp \ 'a rbt \ 'a rbt" -and delL :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" -and delR :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" +fun del :: "'a::linorder \ 'a rbt \ 'a rbt" +and delL :: "'a::linorder \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" +and delR :: "'a::linorder \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" where "del x Leaf = Leaf" | "del x (Node _ l a r) = @@ -40,7 +40,7 @@ "delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | "delR x l a r = R l a (del x r)" -definition delete :: "'a::cmp \ 'a rbt \ 'a rbt" where +definition delete :: "'a::linorder \ 'a rbt \ 'a rbt" where "delete x t = paint Black (del x t)" @@ -88,21 +88,9 @@ by (auto simp: delete_def inorder_del inorder_paint) -interpretation Set_by_Ordered -where empty = Leaf and isin = isin and insert = insert and delete = delete -and inorder = inorder and inv = "\_. True" -proof (standard, goal_cases) - case 1 show ?case by simp -next - case 2 thus ?case by(simp add: isin_set) -next - case 3 thus ?case by(simp add: inorder_insert) -next - case 4 thus ?case by(simp add: inorder_delete) -qed auto +subsection \Structural invariants\ - -subsection \Structural invariants\ +text\The proofs are due to Markus Reiter and Alexander Krauss,\ fun color :: "'a rbt \ color" where "color Leaf = Black" | @@ -112,24 +100,24 @@ "bheight Leaf = 0" | "bheight (Node c l x r) = (if c = Black then Suc(bheight l) else bheight l)" -fun inv1 :: "'a rbt \ bool" where -"inv1 Leaf = True" | -"inv1 (Node c l a r) = - (inv1 l \ inv1 r \ (c = Black \ color l = Black \ color r = Black))" +fun invc :: "'a rbt \ bool" where +"invc Leaf = True" | +"invc (Node c l a r) = + (invc l \ invc r \ (c = Black \ color l = Black \ color r = Black))" -fun inv1_root :: "'a rbt \ bool" \ \Weaker version\ where -"inv1_root Leaf = True" | -"inv1_root (Node c l a r) = (inv1 l \ inv1 r)" +fun invc_sons :: "'a rbt \ bool" \ \Weaker version\ where +"invc_sons Leaf = True" | +"invc_sons (Node c l a r) = (invc l \ invc r)" -fun inv2 :: "'a rbt \ bool" where -"inv2 Leaf = True" | -"inv2 (Node c l x r) = (inv2 l \ inv2 r \ bheight l = bheight r)" +fun invh :: "'a rbt \ bool" where +"invh Leaf = True" | +"invh (Node c l x r) = (invh l \ invh r \ bheight l = bheight r)" -lemma inv1_rootI[simp]: "inv1 t \ inv1_root t" +lemma invc_sonsI: "invc t \ invc_sons t" by (cases t) simp+ definition rbt :: "'a rbt \ bool" where -"rbt t = (inv1 t \ inv2 t \ color t = Black)" +"rbt t = (invc t \ invh t \ color t = Black)" lemma color_paint_Black: "color (paint Black t) = Black" by (cases t) auto @@ -137,142 +125,386 @@ theorem rbt_Leaf: "rbt Leaf" by (simp add: rbt_def) -lemma paint_inv1_root: "inv1_root t \ inv1_root (paint c t)" +lemma paint_invc_sons: "invc_sons t \ invc_sons (paint c t)" by (cases t) auto -lemma inv1_paint_Black: "inv1_root t \ inv1 (paint Black t)" +lemma invc_paint_Black: "invc_sons t \ invc (paint Black t)" by (cases t) auto -lemma inv2_paint: "inv2 t \ inv2 (paint c t)" +lemma invh_paint: "invh t \ invh (paint c t)" by (cases t) auto -lemma inv1_bal: "\inv1_root l; inv1_root r\ \ inv1 (bal l a r)" +lemma invc_bal: "\invc_sons l; invc_sons r\ \ invc (bal l a r)" by (induct l a r rule: bal.induct) auto lemma bheight_bal: "bheight l = bheight r \ bheight (bal l a r) = Suc (bheight l)" by (induct l a r rule: bal.induct) auto -lemma inv2_bal: - "\ inv2 l; inv2 r; bheight l = bheight r \ \ inv2 (bal l a r)" +lemma invh_bal: + "\ invh l; invh r; bheight l = bheight r \ \ invh (bal l a r)" by (induct l a r rule: bal.induct) auto subsubsection \Insertion\ -lemma inv1_ins: assumes "inv1 t" - shows "color t = Black \ inv1 (ins x t)" "inv1_root (ins x t)" +lemma invc_ins: assumes "invc t" + shows "color t = Black \ invc (ins x t)" "invc_sons (ins x t)" using assms -by (induct x t rule: ins.induct) (auto simp: inv1_bal) +by (induct x t rule: ins.induct) (auto simp: invc_bal invc_sonsI) -lemma inv2_ins: assumes "inv2 t" - shows "inv2 (ins x t)" "bheight (ins x t) = bheight t" +lemma invh_ins: assumes "invh t" + shows "invh (ins x t)" "bheight (ins x t) = bheight t" using assms -by (induct x t rule: ins.induct) (auto simp: inv2_bal bheight_bal) +by (induct x t rule: ins.induct) (auto simp: invh_bal bheight_bal) -theorem rbt_ins: "rbt t \ rbt (insert x t)" -by (simp add: inv1_ins inv2_ins color_paint_Black inv1_paint_Black inv2_paint +theorem rbt_insert: "rbt t \ rbt (insert x t)" +by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint rbt_def insert_def) -(* -lemma bheight_paintR'[simp]: "color t = Black \ bheight (paint Red t) = bheight t - 1" + +subsubsection \Deletion\ + +lemma bheight_paint_Red: + "color t = Black \ bheight (paint Red t) = bheight t - 1" by (cases t) auto -lemma balL_inv2_with_inv1: - assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt" - shows "bheight (balL lt a rt) = bheight lt + 1" "inv2 (balL lt a rt)" +lemma balL_invh_with_invc: + assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "invc rt" + shows "bheight (balL lt a rt) = bheight lt + 1" "invh (balL lt a rt)" using assms -by (induct lt a rt rule: balL.induct) (auto simp: inv2_bal inv2_paint bheight_bal) +by (induct lt a rt rule: balL.induct) + (auto simp: invh_bal invh_paint bheight_bal bheight_paint_Red) -lemma balL_inv2_app: - assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color rt = Black" - shows "inv2 (balL lt a rt)" +lemma balL_invh_app: + assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "color rt = Black" + shows "invh (balL lt a rt)" "bheight (balL lt a rt) = bheight rt" using assms -by (induct lt a rt rule: balL.induct) (auto simp add: inv2_bal bheight_bal) +by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal) -lemma balL_inv1: "\inv1_root l; inv1 r; color r = Black\ \ inv1 (balL l a r)" -by (induct l a r rule: balL.induct) (simp_all add: inv1_bal) +lemma balL_invc: "\invc_sons l; invc r; color r = Black\ \ invc (balL l a r)" +by (induct l a r rule: balL.induct) (simp_all add: invc_bal) -lemma balL_inv1_root: "\ inv1_root lt; inv1 rt \ \ inv1_root (balL lt a rt)" -by (induct lt a rt rule: balL.induct) (auto simp: inv1_bal paint_inv1_root) +lemma balL_invc_sons: "\ invc_sons lt; invc rt \ \ invc_sons (balL lt a rt)" +by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI) -lemma balR_inv2_with_inv1: - assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt" - shows "inv2 (balR lt a rt) \ bheight (balR lt a rt) = bheight lt" +lemma balR_invh_with_invc: + assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt" + shows "invh (balR lt a rt) \ bheight (balR lt a rt) = bheight lt" using assms -by(induct lt a rt rule: balR.induct)(auto simp: inv2_bal bheight_bal inv2_paint) +by(induct lt a rt rule: balR.induct) + (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red) -lemma balR_inv1: "\inv1 a; inv1_root b; color a = Black\ \ inv1 (balR a x b)" -by (induct a x b rule: balR.induct) (simp_all add: inv1_bal) +lemma invc_balR: "\invc a; invc_sons b; color a = Black\ \ invc (balR a x b)" +by (induct a x b rule: balR.induct) (simp_all add: invc_bal) -lemma balR_inv1_root: "\ inv1 lt; inv1_root rt \ \inv1_root (balR lt x rt)" -by (induct lt x rt rule: balR.induct) (auto simp: inv1_bal paint_inv1_root) +lemma invc_sons_balR: "\ invc lt; invc_sons rt \ \invc_sons (balR lt x rt)" +by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI) -lemma combine_inv2: - assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt" - shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)" +lemma invh_combine: + assumes "invh lt" "invh rt" "bheight lt = bheight rt" + shows "bheight (combine lt rt) = bheight lt" "invh (combine lt rt)" using assms by (induct lt rt rule: combine.induct) - (auto simp: balL_inv2_app split: tree.splits color.splits) + (auto simp: balL_invh_app split: tree.splits color.splits) -lemma combine_inv1: - assumes "inv1 lt" "inv1 rt" - shows "color lt = Black \ color rt = Black \ inv1 (combine lt rt)" - "inv1_root (combine lt rt)" +lemma invc_combine: + assumes "invc lt" "invc rt" + shows "color lt = Black \ color rt = Black \ invc (combine lt rt)" + "invc_sons (combine lt rt)" using assms by (induct lt rt rule: combine.induct) - (auto simp: balL_inv1 split: tree.splits color.splits) + (auto simp: balL_invc invc_sonsI split: tree.splits color.splits) -lemma - assumes "inv2 lt" "inv1 lt" +lemma assumes "invh lt" "invc lt" shows - "\inv2 rt; bheight lt = bheight rt; inv1 rt\ \ - inv2 (rbt_del_from_left x lt k v rt) \ - bheight (rbt_del_from_left x lt k v rt) = bheight lt \ - (color_of lt = B \ color_of rt = B \ inv1 (rbt_del_from_left x lt k v rt) \ - (color_of lt \ B \ color_of rt \ B) \ inv1l (rbt_del_from_left x lt k v rt))" - and "\inv2 rt; bheight lt = bheight rt; inv1 rt\ \ - inv2 (rbt_del_from_right x lt k v rt) \ - bheight (rbt_del_from_right x lt k v rt) = bheight lt \ - (color_of lt = B \ color_of rt = B \ inv1 (rbt_del_from_right x lt k v rt) \ - (color_of lt \ B \ color_of rt \ B) \ inv1l (rbt_del_from_right x lt k v rt))" - and rbt_del_inv1_inv2: "inv2 (rbt_del x lt) \ (color_of lt = R \ bheight (rbt_del x lt) = bheight lt \ inv1 (rbt_del x lt) - \ color_of lt = B \ bheight (rbt_del x lt) = bheight lt - 1 \ inv1l (rbt_del x lt))" + del_invc_invh: "invh (del x lt) \ (color lt = Red \ bheight (del x lt) = bheight lt \