--- 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
-----------------------------
--- 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 \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
+fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('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 \<Rightarrow> split (skew (Node lv t1 (a,b) (update x y t2))) |
EQ \<Rightarrow> Node lv t1 (x,y) t2)"
-fun delete :: "'a::cmp \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
+fun delete :: "'a::linorder \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
"delete _ Leaf = Leaf" |
"delete x (Node lv l (a,b) r) =
(case cmp x a of
--- 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 \<open>AA Tree Implementation of Sets\<close>
@@ -36,7 +36,7 @@
hide_const (open) insert
-fun insert :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
+fun insert :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> '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 \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
+fun delete :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
"delete _ Leaf = Leaf" |
"delete x (Node lv l a r) =
(case cmp x a of
--- 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 \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
+fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('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 \<Rightarrow> Node h l (x,y) r |
LT \<Rightarrow> balL (update x y l) (a,b) r |
GT \<Rightarrow> balR l (a,b) (update x y r))"
-fun delete :: "'a::cmp \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
+fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
"delete _ Leaf = Leaf" |
"delete x (Node h l (a,b) r) = (case cmp x a of
EQ \<Rightarrow> del_root (Node h l (a,b) r) |
--- 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 \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> '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 \<Rightarrow> 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 \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> '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 \<open>Height-Size Relation\<close>
+
+text \<open>By Daniel St\"uwe\<close>
+
+fun fib_tree :: "nat \<Rightarrow> 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 \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node (Suc h) l a r)"
+by (induction t) auto
+
+lemma fib_Suc_lt: "fib n \<le> fib (Suc n)"
+by (induction n rule: fib.induct) auto
+
+lemma fib_mono: "n \<le> m \<Longrightarrow> fib n \<le> 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 \<le> m"
+ shows "size1 (fib_tree n) \<le> 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 \<Longrightarrow> size1 (fib_tree (ht t)) \<le> 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)) \<le> size1 l" by auto moreover
+ from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \<le> 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)) \<le> size1 l" by auto moreover
+ from ht 3(1,2,4) have "size1 (fib_tree h) \<le> 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) \<le> size1 l" by auto moreover
+ from ht 3 have "size1 (fib_tree (Suc h)) \<le> size1 r" by auto ultimately
+ show ?thesis by auto
+ qed
+qed auto
+
+theorem avl_size_bound: "avl t \<Longrightarrow> fib(height t + 2) \<le> size1 t"
+using fib_tree_minimal fib_tree_size1 by fastforce
+
end
--- 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 \<times> 'b) bro \<Rightarrow> 'a::cmp \<Rightarrow> 'b option" where
+fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::linorder \<Rightarrow> '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 \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
+fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'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 \<Rightarrow> N2 l (a,y) r |
GT \<Rightarrow> n2 l (a,b) (upd x y r))"
-definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
+definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
"update x y t = tree(upd x y t)"
end
@@ -37,7 +37,7 @@
context delete
begin
-fun del :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
+fun del :: "'a::linorder \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'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 \<Rightarrow> N1 l |
Some (ab, r') \<Rightarrow> n2 l ab r'))"
-definition delete :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
+definition delete :: "'a::linorder \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'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
--- 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 \<open>1-2 Brother Tree Implementation of Sets\<close>
@@ -6,6 +6,7 @@
imports
Cmp
Set_by_Ordered
+ "~~/src/HOL/Number_Theory/Fib"
begin
subsection \<open>Data Type and Operations\<close>
@@ -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 \<Rightarrow> 'a::cmp \<Rightarrow> bool" where
+fun isin :: "'a bro \<Rightarrow> 'a::linorder \<Rightarrow> 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 \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
+fun ins :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> '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 \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
+definition insert :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
"insert x t = tree(ins x t)"
end
@@ -102,7 +103,7 @@
None \<Rightarrow> Some (a, N1 t2) |
Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
-fun del :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
+fun del :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> '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 \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
+definition delete :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> '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 \<open>Height-Size Relation\<close>
+
+text \<open>By Daniel St\"uwe\<close>
+
+fun fib_tree :: "nat \<Rightarrow> 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 \<Rightarrow> nat" where
+ "fib' 0 = 0"
+| "fib' (Suc 0) = 1"
+| "fib' (Suc(Suc h)) = 1 + fib' (Suc h) + fib' h"
+
+fun size :: "'a bro \<Rightarrow> 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 \<in> 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 \<in> B (Suc n)"
+obtains
+ (BB) "t1 \<in> B n" and "t2 \<in> B n" |
+ (UB) "t1 \<in> U n" and "t2 \<in> B n" |
+ (BU) "t1 \<in> B n" and "t2 \<in> U n"
+using assms by auto
+
+lemma size_bounded: "t \<in> B h \<Longrightarrow> size t \<ge> 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 \<in> 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 \<or> t2 = N2 z y x" "x \<in> 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 \<in> 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 \<in> 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 \<in> B h \<Longrightarrow> fib (h + 2) \<le> size t + 1"
+using size_bounded
+by (simp add: size_fib' fibfib[symmetric] del: fib.simps)
+
end
--- 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 \<Rightarrow> 'a \<Rightarrow> cmp"
-assumes LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
-assumes EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
-assumes GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
+function cmp :: "'a:: linorder \<Rightarrow> 'a \<Rightarrow> cmp_val" where
+"x < y \<Longrightarrow> cmp x y = LT" |
+"x = y \<Longrightarrow> cmp x y = EQ" |
+"x > y \<Longrightarrow> cmp x y = GT"
+by (auto, force)
+termination by lexicographic_order
+
+lemma
+ LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
+and EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
+and GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
+by (cases x y rule: linorder_cases, auto)+
lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> 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
--- 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 \<Rightarrow> 'a \<Rightarrow> bool" where
+fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
"isin Leaf x = False" |
"isin (Node _ l a r) x =
(case cmp x a of
--- 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 \<Rightarrow> 'a \<Rightarrow> 'b option" where
+fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
"lookup Leaf x = None" |
"lookup (Node _ l (a,b) r) x =
(case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
--- 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 \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
+fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('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 \<Rightarrow> bal (upd x y l) (a,b) r |
@@ -19,12 +19,12 @@
GT \<Rightarrow> R l (a,b) (upd x y r) |
EQ \<Rightarrow> R l (x,y) r)"
-definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
+definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
"update x y t = paint Black (upd x y t)"
-fun del :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
-and delL :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
-and delR :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
+fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
+and delL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
+and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('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 \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
+definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
"delete x t = paint Black (del x t)"
--- 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 \<open>Red-Black Tree Implementation of Sets\<close>
@@ -9,7 +9,7 @@
Isin2
begin
-fun ins :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> '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 \<Rightarrow> R l a (ins x r) |
EQ \<Rightarrow> R l a r)"
-definition insert :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"insert x t = paint Black (ins x t)"
-fun del :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
-and delL :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
-and delR :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
+fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
+and delL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
+and delR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> '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 \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> '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 = "\<lambda>_. 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 \<open>Structural invariants\<close>
-
-subsection \<open>Structural invariants\<close>
+text\<open>The proofs are due to Markus Reiter and Alexander Krauss,\<close>
fun color :: "'a rbt \<Rightarrow> 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 \<Rightarrow> bool" where
-"inv1 Leaf = True" |
-"inv1 (Node c l a r) =
- (inv1 l \<and> inv1 r \<and> (c = Black \<or> color l = Black \<and> color r = Black))"
+fun invc :: "'a rbt \<Rightarrow> bool" where
+"invc Leaf = True" |
+"invc (Node c l a r) =
+ (invc l \<and> invc r \<and> (c = Black \<or> color l = Black \<and> color r = Black))"
-fun inv1_root :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
-"inv1_root Leaf = True" |
-"inv1_root (Node c l a r) = (inv1 l \<and> inv1 r)"
+fun invc_sons :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
+"invc_sons Leaf = True" |
+"invc_sons (Node c l a r) = (invc l \<and> invc r)"
-fun inv2 :: "'a rbt \<Rightarrow> bool" where
-"inv2 Leaf = True" |
-"inv2 (Node c l x r) = (inv2 l \<and> inv2 r \<and> bheight l = bheight r)"
+fun invh :: "'a rbt \<Rightarrow> bool" where
+"invh Leaf = True" |
+"invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
-lemma inv1_rootI[simp]: "inv1 t \<Longrightarrow> inv1_root t"
+lemma invc_sonsI: "invc t \<Longrightarrow> invc_sons t"
by (cases t) simp+
definition rbt :: "'a rbt \<Rightarrow> bool" where
-"rbt t = (inv1 t \<and> inv2 t \<and> color t = Black)"
+"rbt t = (invc t \<and> invh t \<and> 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 \<Longrightarrow> inv1_root (paint c t)"
+lemma paint_invc_sons: "invc_sons t \<Longrightarrow> invc_sons (paint c t)"
by (cases t) auto
-lemma inv1_paint_Black: "inv1_root t \<Longrightarrow> inv1 (paint Black t)"
+lemma invc_paint_Black: "invc_sons t \<Longrightarrow> invc (paint Black t)"
by (cases t) auto
-lemma inv2_paint: "inv2 t \<Longrightarrow> inv2 (paint c t)"
+lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
by (cases t) auto
-lemma inv1_bal: "\<lbrakk>inv1_root l; inv1_root r\<rbrakk> \<Longrightarrow> inv1 (bal l a r)"
+lemma invc_bal: "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)"
by (induct l a r rule: bal.induct) auto
lemma bheight_bal:
"bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)"
by (induct l a r rule: bal.induct) auto
-lemma inv2_bal:
- "\<lbrakk> inv2 l; inv2 r; bheight l = bheight r \<rbrakk> \<Longrightarrow> inv2 (bal l a r)"
+lemma invh_bal:
+ "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (bal l a r)"
by (induct l a r rule: bal.induct) auto
subsubsection \<open>Insertion\<close>
-lemma inv1_ins: assumes "inv1 t"
- shows "color t = Black \<Longrightarrow> inv1 (ins x t)" "inv1_root (ins x t)"
+lemma invc_ins: assumes "invc t"
+ shows "color t = Black \<Longrightarrow> 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 \<Longrightarrow> rbt (insert x t)"
-by (simp add: inv1_ins inv2_ins color_paint_Black inv1_paint_Black inv2_paint
+theorem rbt_insert: "rbt t \<Longrightarrow> 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 \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
+
+subsubsection \<open>Deletion\<close>
+
+lemma bheight_paint_Red:
+ "color t = Black \<Longrightarrow> 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: "\<lbrakk>inv1_root l; inv1 r; color r = Black\<rbrakk> \<Longrightarrow> inv1 (balL l a r)"
-by (induct l a r rule: balL.induct) (simp_all add: inv1_bal)
+lemma balL_invc: "\<lbrakk>invc_sons l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
+by (induct l a r rule: balL.induct) (simp_all add: invc_bal)
-lemma balL_inv1_root: "\<lbrakk> inv1_root lt; inv1 rt \<rbrakk> \<Longrightarrow> 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: "\<lbrakk> invc_sons lt; invc rt \<rbrakk> \<Longrightarrow> 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) \<and> 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) \<and> 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: "\<lbrakk>inv1 a; inv1_root b; color a = Black\<rbrakk> \<Longrightarrow> inv1 (balR a x b)"
-by (induct a x b rule: balR.induct) (simp_all add: inv1_bal)
+lemma invc_balR: "\<lbrakk>invc a; invc_sons b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
+by (induct a x b rule: balR.induct) (simp_all add: invc_bal)
-lemma balR_inv1_root: "\<lbrakk> inv1 lt; inv1_root rt \<rbrakk> \<Longrightarrow>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: "\<lbrakk> invc lt; invc_sons rt \<rbrakk> \<Longrightarrow>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 \<Longrightarrow> color rt = Black \<Longrightarrow> inv1 (combine lt rt)"
- "inv1_root (combine lt rt)"
+lemma invc_combine:
+ assumes "invc lt" "invc rt"
+ shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> 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
- "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
- inv2 (rbt_del_from_left x lt k v rt) \<and>
- bheight (rbt_del_from_left x lt k v rt) = bheight lt \<and>
- (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_left x lt k v rt) \<or>
- (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_left x lt k v rt))"
- and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
- inv2 (rbt_del_from_right x lt k v rt) \<and>
- bheight (rbt_del_from_right x lt k v rt) = bheight lt \<and>
- (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_right x lt k v rt) \<or>
- (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_right x lt k v rt))"
- and rbt_del_inv1_inv2: "inv2 (rbt_del x lt) \<and> (color_of lt = R \<and> bheight (rbt_del x lt) = bheight lt \<and> inv1 (rbt_del x lt)
- \<or> color_of lt = B \<and> bheight (rbt_del x lt) = bheight lt - 1 \<and> inv1l (rbt_del x lt))"
+ del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt)
+ \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc_sons (del x lt))"
+and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
+ invh (delL x lt k rt) \<and>
+ bheight (delL x lt k rt) = bheight lt \<and>
+ (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or>
+ (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delL x lt k rt))"
+ and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
+ invh (delR x lt k rt) \<and>
+ bheight (delR x lt k rt) = bheight lt \<and>
+ (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or>
+ (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delR x lt k rt))"
using assms
-proof (induct x lt k v rt and x lt k v rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
+proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct)
case (2 y c _ y')
have "y = y' \<or> y < y' \<or> y > y'" by auto
thus ?case proof (elim disjE)
assume "y = y'"
- with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
+ with 2 show ?thesis
+ by (cases c) (simp_all add: invh_combine invc_combine)
next
assume "y < y'"
- with 2 show ?thesis by (cases c) auto
+ with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
next
assume "y' < y"
- with 2 show ?thesis by (cases c) auto
+ with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
qed
next
- case (3 y lt z v rta y' ss bb)
- thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
+ case (3 y lt z rta y' bb)
+ thus ?case by (cases "color (Node Black lt z rta) = Black \<and> color bb = Black") (simp add: balL_invh_with_invc balL_invc balL_invc_sons)+
next
- case (5 y a y' ss lt z v rta)
- thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
+ case (5 y a y' lt z rta)
+ thus ?case by (cases "color a = Black \<and> color (Node Black lt z rta) = Black") (simp add: balR_invh_with_invc invc_balR invc_sons_balR)+
next
- case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
+ case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
qed auto
-theorem rbt_delete_is_rbt [simp]: assumes "rbt t" shows "rbt (delete k t)"
+theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
+by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc_sonsI invh_paint)
+
+text \<open>Overall correctness:\<close>
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete
+and inorder = inorder and inv = rbt
+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)
+next
+ case 5 thus ?case by (simp add: rbt_Leaf)
+next
+ case 6 thus ?case by (simp add: rbt_insert)
+next
+ case 7 thus ?case by (simp add: rbt_delete)
+qed
+
+
+subsection \<open>Height-Size Relation\<close>
+
+text \<open>By Daniel St\"uwe\<close>
+
+lemma color_RedE:"color t = Red \<Longrightarrow> invc t =
+ (\<exists> l a r . t = R l a r \<and> color l = Black \<and> color r = Black \<and> invc l \<and> invc r)"
+by (cases t) auto
+
+lemma rbt_induct[consumes 1]:
+ assumes "rbt t"
+ assumes [simp]: "P Leaf"
+ assumes "\<And> t l a r. \<lbrakk>t = B l a r; invc t; invh t; Q(l); Q(r)\<rbrakk> \<Longrightarrow> P t"
+ assumes "\<And> t l a r. \<lbrakk>t = R l a r; invc t; invh t; P(l); P(r)\<rbrakk> \<Longrightarrow> Q t"
+ assumes "\<And> t . P(t) \<Longrightarrow> Q(t)"
+ shows "P t"
+using assms(1) unfolding rbt_def apply safe
+proof (induction t rule: measure_induct[of size])
+case (1 t)
+ note * = 1 assms
+ show ?case proof (cases t)
+ case [simp]: (Node c l a r)
+ show ?thesis proof (cases c)
+ case Red thus ?thesis using 1 by simp
+ next
+ case [simp]: Black
+ show ?thesis
+ proof (cases "color l")
+ case Red
+ thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
+ next
+ case Black
+ thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
+ qed
+ qed
+ qed simp
+qed
+
+lemma rbt_b_height: "rbt t \<Longrightarrow> bheight t * 2 \<ge> height t"
+by (induction t rule: rbt_induct[where Q="\<lambda> t. bheight t * 2 + 1 \<ge> height t"]) auto
+
+lemma red_b_height: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t * 2 + 1 \<ge> height t"
+apply (cases t) apply simp
+ using rbt_b_height unfolding rbt_def
+ by (cases "color t") fastforce+
+
+lemma red_b_height2: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t \<ge> height t div 2"
+using red_b_height by fastforce
+
+lemma rbt_b_height2: "bheight t \<le> height t"
+by (induction t) auto
+
+lemma "rbt t \<Longrightarrow> size1 t \<le> 4 ^ (bheight t)"
+by(induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<le> 2 * 4 ^ (bheight t)"]) auto
+
+lemma bheight_size_bound: "rbt t \<Longrightarrow> size1 t \<ge> 2 ^ (bheight t)"
+by (induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<ge> 2 ^ (bheight t)"]) auto
+
+text \<open>Balanced red-balck tree with all black nodes:\<close>
+inductive balB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool" where
+"balB 0 Leaf" |
+"balB h t \<Longrightarrow> balB (Suc h) (B t () t)"
+
+inductive_cases [elim!]: "balB 0 t"
+inductive_cases [elim]: "balB (Suc h) t"
+
+lemma balB_hs: "balB h t \<Longrightarrow> bheight t = height t"
+by (induction h t rule: "balB.induct") auto
+
+lemma balB_h: "balB h t \<Longrightarrow> h = height t"
+by (induction h t rule: "balB.induct") auto
+
+lemma "rbt t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
+by (induction t arbitrary: t'
+ rule: rbt_induct[where Q="\<lambda> t . \<forall> h t'. balB (bheight t) t' \<longrightarrow> size t' \<le> size t"])
+ fastforce+
+
+lemma balB_bh: "invc t \<Longrightarrow> invh t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
+by (induction t arbitrary: t') (fastforce split: if_split_asm)+
+
+lemma balB_bh3:"\<lbrakk> balB h t; balB (h' + h) t' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
+by (induction h t arbitrary: t' h' rule: balB.induct) fastforce+
+
+corollary balB_bh3': "\<lbrakk> balB h t; balB h' t'; h \<le> h' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
+using balB_bh3 le_Suc_ex by (fastforce simp: algebra_simps)
+
+lemma exist_pt: "\<exists> t . balB h t"
+by (induction h) (auto intro: balB.intros)
+
+corollary compact_pt:
+ assumes "invc t" "invh t" "h \<le> bheight t" "balB h t'"
+ shows "size t' \<le> size t"
proof -
- from assms have "inv2 t" and "inv1 t" unfolding rbt_def by auto
- hence "inv2 (del k t) \<and> (color t = Red \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color t = Black \<and> bheight (del k t) = bheight t - 1 \<and> inv1_root (del k t))"
- by (rule rbt_del_inv1_inv2)
- hence "inv2 (del k t) \<and> inv1l (rbt_del k t)" by (cases "color_of t") auto
- with assms show ?thesis
- unfolding is_rbt_def rbt_delete_def
- by (auto intro: paint_rbt_sorted rbt_del_rbt_sorted)
+ obtain t'' where "balB (bheight t) t''" using exist_pt by blast
+ thus ?thesis using assms balB_bh[of t t''] balB_bh3'[of h t' "bheight t" t''] by auto
+qed
+
+lemma balB_bh2: "balB (bheight t) t'\<Longrightarrow> invc t \<Longrightarrow> invh t \<Longrightarrow> height t' \<le> height t"
+apply (induction "(bheight t)" t' arbitrary: t rule: balB.induct)
+using balB_h rbt_b_height2 by auto
+
+lemma balB_rbt: "balB h t \<Longrightarrow> rbt t"
+unfolding rbt_def
+by (induction h t rule: balB.induct) auto
+
+lemma balB_size[simp]: "balB h t \<Longrightarrow> size1 t = 2^h"
+by (induction h t rule: balB.induct) auto
+
+text \<open>Red-black tree (except that the root may be red) of minimal size
+for a given height:\<close>
+
+inductive RB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool" where
+"RB 0 Leaf" |
+"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Red \<Longrightarrow> RB (Suc h) (B t' () t)" |
+"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Black \<Longrightarrow> RB (Suc h) (R t' () t)"
+
+lemmas RB.intros[intro]
+
+lemma RB_invc: "RB h t \<Longrightarrow> invc t"
+apply (induction h t rule: RB.induct)
+using balB_rbt unfolding rbt_def by auto
+
+lemma RB_h: "RB h t \<Longrightarrow> h = height t"
+apply (induction h t rule: RB.induct)
+using balB_h by auto
+
+lemma RB_mod: "RB h t \<Longrightarrow> (color t = Black \<longleftrightarrow> h mod 2 = 0)"
+apply (induction h t rule: RB.induct)
+apply auto
+by presburger
+
+lemma RB_b_height: "RB h t \<Longrightarrow> height t div 2 = bheight t"
+proof (induction h t rule: RB.induct)
+ case 1
+ thus ?case by auto
+next
+ case (2 h t t')
+ with RB_mod obtain n where "2*n + 1 = h"
+ by (metis color.distinct(1) mod_div_equality2 parity)
+ with 2 balB_h RB_h show ?case by auto
+next
+ case (3 h t t')
+ with RB_mod[OF 3(2)] parity obtain n where "2*n = h" by blast
+ with 3 balB_h RB_h show ?case by auto
qed
-*)
+
+lemma weak_RB_induct[consumes 1]:
+ "RB h t \<Longrightarrow> P 0 \<langle>\<rangle> \<Longrightarrow> (\<And>h t t' c . balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow>
+ P h t' \<Longrightarrow> P (Suc h) (Node c t' () t)) \<Longrightarrow> P h t"
+using RB.induct by metis
+
+lemma RB_invh: "RB h t \<Longrightarrow> invh t"
+apply (induction h t rule: weak_RB_induct)
+ using balB_h balB_hs RB_h balB_rbt RB_b_height
+ unfolding rbt_def
+by auto
+
+lemma RB_bheight_minimal:
+ "\<lbrakk>RB (height t') t; invc t'; invh t'\<rbrakk> \<Longrightarrow> bheight t \<le> bheight t'"
+using RB_b_height RB_h red_b_height2 by fastforce
+
+lemma RB_minimal: "RB (height t') t \<Longrightarrow> invh t \<Longrightarrow> invc t' \<Longrightarrow> invh t' \<Longrightarrow> size t \<le> size t'"
+proof (induction "(height t')" t arbitrary: t' rule: weak_RB_induct)
+ case 1 thus ?case by auto
+next
+ case (2 h t t'')
+ have ***: "size (Node c t'' () t) \<le> size t'"
+ if assms:
+ "\<And> (t' :: 'a rbt) . \<lbrakk> h = height t'; invh t''; invc t'; invh t' \<rbrakk>
+ \<Longrightarrow> size t'' \<le> size t'"
+ "Suc h = height t'" "balB (h div 2) t" "RB h t''"
+ "invc t'" "invh t'" "height l \<ge> height r"
+ and tt[simp]:"t' = Node c l a r" and last: "invh (Node c t'' () t)"
+ for t' :: "'a rbt" and c l a r
+ proof -
+ from assms have inv: "invc r" "invh r" by auto
+ from assms have "height l = h" using max_def by auto
+ with RB_bheight_minimal[of l t''] have
+ "bheight t \<le> bheight r" using assms last by auto
+ with compact_pt[OF inv] balB_h balB_hs have
+ "size t \<le> size r" using assms(3) by auto moreover
+ have "size t'' \<le> size l" using assms last by auto ultimately
+ show ?thesis by simp
+ qed
+
+ from 2 obtain c l a r where
+ t': "t' = Node c l a r" by (cases t') auto
+ with 2 have inv: "invc l" "invh l" "invc r" "invh r" by auto
+ show ?case proof (cases "height r \<le> height l")
+ case True thus ?thesis using ***[OF 2(3,4,1,2,6,7)] t' 2(5) by auto
+ next
+ case False
+ obtain t''' where t''' : "t''' = Node c r a l" "invc t'''" "invh t'''" using 2 t' by auto
+ have "size t''' = size t'" and 4 : "Suc h = height t'''" using 2(4) t' t''' by auto
+ thus ?thesis using ***[OF 2(3) 4 2(1,2) t'''(2,3) _ t'''(1)] 2(5) False by auto
+ qed
+qed
+
+lemma RB_size: "RB h t \<Longrightarrow> size1 t + 1 = 2^((h+1) div 2) + 2^(h div 2)"
+by (induction h t rule: "RB.induct" ) auto
+
+lemma RB_exist: "\<exists> t . RB h t"
+proof (induction h)
+ case (Suc n)
+ obtain r where r: "balB (n div 2) r" using exist_pt by blast
+ obtain l where l: "RB n l" using Suc by blast
+ obtain t where
+ "color l = Red \<Longrightarrow> t = B l () r"
+ "color l = Black \<Longrightarrow> t = R l () r" by auto
+ with l and r have "RB (Suc n) t" by (cases "color l") auto
+ thus ?case by auto
+qed auto
+
+lemma bound:
+ assumes "invc t" "invh t" and [simp]:"height t = h"
+ shows "size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
+proof -
+ obtain t' where t': "RB h t'" using RB_exist by auto
+ show ?thesis using RB_size[OF t']
+ RB_minimal[OF _ _ assms(1,2), simplified, OF t' RB_invh[OF t']] assms t'
+ unfolding size1_def by auto
+qed
+
+corollary "rbt t \<Longrightarrow> h = height t \<Longrightarrow> size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
+using bound unfolding rbt_def by blast
+
end
--- a/src/HOL/Data_Structures/Splay_Map.thy Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Splay_Map.thy Thu Jul 07 18:08:10 2016 +0200
@@ -42,7 +42,7 @@
termination splay
by lexicographic_order
-lemma splay_code: "splay (x::_::cmp) t = (case t of Leaf \<Rightarrow> Leaf |
+lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf |
Node al a ar \<Rightarrow> (case cmp x (fst a) of
EQ \<Rightarrow> t |
LT \<Rightarrow> (case al of
--- a/src/HOL/Data_Structures/Splay_Set.thy Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Splay_Set.thy Thu Jul 07 18:08:10 2016 +0200
@@ -51,7 +51,7 @@
"\<lbrakk> x = x'; y = y'; z = z' \<rbrakk> \<Longrightarrow> case_tree x y z = case_tree x' y' z'"
by auto
-lemma splay_code: "splay (x::_::cmp) t = (case t of Leaf \<Rightarrow> Leaf |
+lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf |
Node al a ar \<Rightarrow> (case cmp x a of
EQ \<Rightarrow> t |
LT \<Rightarrow> (case al of
@@ -83,7 +83,7 @@
hide_const (open) insert
-fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
"insert x t =
(if t = Leaf then Node Leaf x Leaf
else case splay x t of
--- a/src/HOL/Data_Structures/Tree234_Map.thy Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Tree234_Map.thy Thu Jul 07 18:08:10 2016 +0200
@@ -10,7 +10,7 @@
subsection \<open>Map operations on 2-3-4 trees\<close>
-fun lookup :: "('a::cmp * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
+fun lookup :: "('a::linorder * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
"lookup Leaf x = None" |
"lookup (Node2 l (a,b) r) x = (case cmp x a of
LT \<Rightarrow> lookup l x |
@@ -30,7 +30,7 @@
GT \<Rightarrow> (case cmp x a3 of
LT \<Rightarrow> lookup t3 x | EQ \<Rightarrow> Some b3 | GT \<Rightarrow> lookup t4 x))"
-fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
+fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
LT \<Rightarrow> (case upd x y l of
@@ -72,10 +72,10 @@
T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
| Up\<^sub>i t41 q t42 => Up\<^sub>i (Node2 t1 ab1 t2) ab2 (Node3 t3 ab3 t41 q t42))))"
-definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
+definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
"update x y t = tree\<^sub>i(upd x y t)"
-fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d" where
+fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d" where
"del x Leaf = T\<^sub>d Leaf" |
"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
@@ -107,7 +107,7 @@
EQ \<Rightarrow> let (ab',t4') = del_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
GT \<Rightarrow> node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))"
-definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
+definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
"delete x t = tree\<^sub>d(del x t)"
--- a/src/HOL/Data_Structures/Tree234_Set.thy Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Tree234_Set.thy Thu Jul 07 18:08:10 2016 +0200
@@ -11,7 +11,7 @@
subsection \<open>Set operations on 2-3-4 trees\<close>
-fun isin :: "'a::cmp tree234 \<Rightarrow> 'a \<Rightarrow> bool" where
+fun isin :: "'a::linorder tree234 \<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)" |
@@ -38,7 +38,7 @@
"tree\<^sub>i (T\<^sub>i t) = t" |
"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
-fun ins :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where
+fun ins :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where
"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
"ins x (Node2 l a r) =
(case cmp x a of
@@ -91,7 +91,7 @@
hide_const insert
-definition insert :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
+definition insert :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
"insert x t = tree\<^sub>i(ins x t)"
datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234"
@@ -162,7 +162,7 @@
"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" |
"del_min (Node4 l a m b n c r) = (let (x,l') = del_min l in (x, node41 l' a m b n c r))"
-fun del :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
+fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
"del k Leaf = T\<^sub>d Leaf" |
"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf
@@ -194,7 +194,7 @@
EQ \<Rightarrow> let (c',r') = del_min r in node44 l a m b n c' r' |
GT \<Rightarrow> node44 l a m b n c (del k r)))"
-definition delete :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
+definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
"delete x t = tree\<^sub>d(del x t)"
--- a/src/HOL/Data_Structures/Tree23_Map.thy Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Tree23_Map.thy Thu Jul 07 18:08:10 2016 +0200
@@ -8,7 +8,7 @@
Map_by_Ordered
begin
-fun lookup :: "('a::cmp * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
+fun lookup :: "('a::linorder * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
"lookup Leaf x = None" |
"lookup (Node2 l (a,b) r) x = (case cmp x a of
LT \<Rightarrow> lookup l x |
@@ -22,7 +22,7 @@
EQ \<Rightarrow> Some b2 |
GT \<Rightarrow> lookup r x))"
-fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
+fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
LT \<Rightarrow> (case upd x y l of
@@ -46,10 +46,10 @@
T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
| Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))"
-definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
+definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
"update a b t = tree\<^sub>i(upd a b t)"
-fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where
+fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where
"del x Leaf = T\<^sub>d Leaf" |
"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
@@ -66,7 +66,7 @@
EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))"
-definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
+definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
"delete x t = tree\<^sub>d(del x t)"
--- a/src/HOL/Data_Structures/Tree23_Set.thy Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Thu Jul 07 18:08:10 2016 +0200
@@ -9,7 +9,7 @@
Set_by_Ordered
begin
-fun isin :: "'a::cmp tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
+fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
"isin Leaf x = False" |
"isin (Node2 l a r) x =
(case cmp x a of
@@ -32,7 +32,7 @@
"tree\<^sub>i (T\<^sub>i t) = t" |
"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
-fun ins :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
+fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
"ins x (Node2 l a r) =
(case cmp x a of
@@ -66,7 +66,7 @@
hide_const insert
-definition insert :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
"insert x t = tree\<^sub>i(ins x t)"
datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
@@ -108,7 +108,7 @@
"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::linorder \<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))" |
@@ -131,7 +131,7 @@
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)))"
-definition delete :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
"delete x t = tree\<^sub>d(del x t)"
--- a/src/HOL/Data_Structures/Tree_Map.thy Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Tree_Map.thy Thu Jul 07 18:08:10 2016 +0200
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)
-section {* Unbalanced Tree as Map *}
+section \<open>Unbalanced Tree Implementation of Map\<close>
theory Tree_Map
imports
@@ -8,19 +8,19 @@
Map_by_Ordered
begin
-fun lookup :: "('a::cmp*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
+fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
"lookup Leaf x = None" |
"lookup (Node l (a,b) r) x =
(case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
-fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
"update x y Leaf = Node Leaf (x,y) Leaf" |
"update x y (Node l (a,b) r) = (case cmp x a of
LT \<Rightarrow> Node (update x y l) (a,b) r |
EQ \<Rightarrow> Node l (x,y) r |
GT \<Rightarrow> Node l (a,b) (update x y r))"
-fun delete :: "'a::cmp \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
"delete x Leaf = Leaf" |
"delete x (Node l (a,b) r) = (case cmp x a of
LT \<Rightarrow> Node (delete x l) (a,b) r |
--- a/src/HOL/Data_Structures/Tree_Set.thy Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy Thu Jul 07 18:08:10 2016 +0200
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)
-section {* Tree Implementation of Sets *}
+section \<open>Unbalanced Tree Implementation of Set\<close>
theory Tree_Set
imports
@@ -9,7 +9,7 @@
Set_by_Ordered
begin
-fun isin :: "'a::cmp tree \<Rightarrow> 'a \<Rightarrow> bool" where
+fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where
"isin Leaf x = False" |
"isin (Node l a r) x =
(case cmp x a of
@@ -19,7 +19,7 @@
hide_const (open) insert
-fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+fun insert :: "'a::linorder \<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
@@ -31,7 +31,7 @@
"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
+fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
"delete x Leaf = Leaf" |
"delete x (Node l a r) =
(case cmp x a of