got rid of class cmp; added height-size proofs by Daniel Stuewe
authornipkow
Thu Jul 07 18:08:02 2016 +0200 (2016-07-07)
changeset 63411e051eea34990
parent 63409 3f3223b90239
child 63412 def97df48390
got rid of class cmp; added height-size proofs by Daniel Stuewe
CONTRIBUTORS
src/HOL/Data_Structures/AA_Map.thy
src/HOL/Data_Structures/AA_Set.thy
src/HOL/Data_Structures/AVL_Map.thy
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Data_Structures/Brother12_Map.thy
src/HOL/Data_Structures/Brother12_Set.thy
src/HOL/Data_Structures/Cmp.thy
src/HOL/Data_Structures/Isin2.thy
src/HOL/Data_Structures/Lookup2.thy
src/HOL/Data_Structures/RBT_Map.thy
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Data_Structures/Splay_Map.thy
src/HOL/Data_Structures/Splay_Set.thy
src/HOL/Data_Structures/Tree234_Map.thy
src/HOL/Data_Structures/Tree234_Set.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/Data_Structures/Tree_Map.thy
src/HOL/Data_Structures/Tree_Set.thy
     1.1 --- a/CONTRIBUTORS	Thu Jul 07 09:24:03 2016 +0200
     1.2 +++ b/CONTRIBUTORS	Thu Jul 07 18:08:02 2016 +0200
     1.3 @@ -20,6 +20,9 @@
     1.4  * June 2016: Andreas Lochbihler
     1.5    Formalisation of discrete subprobability distributions.
     1.6  
     1.7 +* July 2016: Daniel Stuewe
     1.8 +  Height-size proofs in HOL/Data_Structures
     1.9 +
    1.10  Contributions to Isabelle2016
    1.11  -----------------------------
    1.12  
     2.1 --- a/src/HOL/Data_Structures/AA_Map.thy	Thu Jul 07 09:24:03 2016 +0200
     2.2 +++ b/src/HOL/Data_Structures/AA_Map.thy	Thu Jul 07 18:08:02 2016 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4    Lookup2
     2.5  begin
     2.6  
     2.7 -fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
     2.8 +fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
     2.9  "update x y Leaf = Node 1 Leaf (x,y) Leaf" |
    2.10  "update x y (Node lv t1 (a,b) t2) =
    2.11    (case cmp x a of
    2.12 @@ -16,7 +16,7 @@
    2.13       GT \<Rightarrow> split (skew (Node lv t1 (a,b) (update x y t2))) |
    2.14       EQ \<Rightarrow> Node lv t1 (x,y) t2)"
    2.15  
    2.16 -fun delete :: "'a::cmp \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
    2.17 +fun delete :: "'a::linorder \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
    2.18  "delete _ Leaf = Leaf" |
    2.19  "delete x (Node lv l (a,b) r) =
    2.20    (case cmp x a of
     3.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Thu Jul 07 09:24:03 2016 +0200
     3.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Thu Jul 07 18:08:02 2016 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  (*
     3.5 -Author: Tobias Nipkow and Daniel Stüwe
     3.6 +Author: Tobias Nipkow, Daniel Stüwe
     3.7  *)
     3.8  
     3.9  section \<open>AA Tree Implementation of Sets\<close>
    3.10 @@ -36,7 +36,7 @@
    3.11  
    3.12  hide_const (open) insert
    3.13  
    3.14 -fun insert :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    3.15 +fun insert :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    3.16  "insert x Leaf = Node 1 Leaf x Leaf" |
    3.17  "insert x (Node lv t1 a t2) =
    3.18    (case cmp x a of
    3.19 @@ -81,7 +81,7 @@
    3.20  "del_max (Node lv l a Leaf) = (l,a)" |
    3.21  "del_max (Node lv l a r) = (let (r',b) = del_max r in (adjust(Node lv l a r'), b))"
    3.22  
    3.23 -fun delete :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    3.24 +fun delete :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    3.25  "delete _ Leaf = Leaf" |
    3.26  "delete x (Node lv l a r) =
    3.27    (case cmp x a of
     4.1 --- a/src/HOL/Data_Structures/AVL_Map.thy	Thu Jul 07 09:24:03 2016 +0200
     4.2 +++ b/src/HOL/Data_Structures/AVL_Map.thy	Thu Jul 07 18:08:02 2016 +0200
     4.3 @@ -8,14 +8,14 @@
     4.4    Lookup2
     4.5  begin
     4.6  
     4.7 -fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
     4.8 +fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
     4.9  "update x y Leaf = Node 1 Leaf (x,y) Leaf" |
    4.10  "update x y (Node h l (a,b) r) = (case cmp x a of
    4.11     EQ \<Rightarrow> Node h l (x,y) r |
    4.12     LT \<Rightarrow> balL (update x y l) (a,b) r |
    4.13     GT \<Rightarrow> balR l (a,b) (update x y r))"
    4.14  
    4.15 -fun delete :: "'a::cmp \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
    4.16 +fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
    4.17  "delete _ Leaf = Leaf" |
    4.18  "delete x (Node h l (a,b) r) = (case cmp x a of
    4.19     EQ \<Rightarrow> del_root (Node h l (a,b) r) |
     5.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Thu Jul 07 09:24:03 2016 +0200
     5.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Thu Jul 07 18:08:02 2016 +0200
     5.3 @@ -1,12 +1,15 @@
     5.4  (*
     5.5 -Author:     Tobias Nipkow
     5.6 -Derived from AFP entry AVL.
     5.7 +Author:     Tobias Nipkow, Daniel Stüwe
     5.8 +Largely derived from AFP entry AVL.
     5.9  *)
    5.10  
    5.11  section "AVL Tree Implementation of Sets"
    5.12  
    5.13  theory AVL_Set
    5.14 -imports Cmp Isin2
    5.15 +imports
    5.16 + Cmp
    5.17 + Isin2
    5.18 +  "~~/src/HOL/Number_Theory/Fib"
    5.19  begin
    5.20  
    5.21  type_synonym 'a avl_tree = "('a,nat) tree"
    5.22 @@ -48,7 +51,7 @@
    5.23            else node (node l a bl) b br
    5.24    else node l a r)"
    5.25  
    5.26 -fun insert :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    5.27 +fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    5.28  "insert x Leaf = Node 1 Leaf x Leaf" |
    5.29  "insert x (Node h l a r) = (case cmp x a of
    5.30     EQ \<Rightarrow> Node h l a r |
    5.31 @@ -68,7 +71,7 @@
    5.32  
    5.33  lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node]
    5.34  
    5.35 -fun delete :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    5.36 +fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    5.37  "delete _ Leaf = Leaf" |
    5.38  "delete x (Node h l a r) =
    5.39    (case cmp x a of
    5.40 @@ -449,4 +452,83 @@
    5.41    qed
    5.42  qed simp_all
    5.43  
    5.44 +
    5.45 +subsection \<open>Height-Size Relation\<close>
    5.46 +
    5.47 +text \<open>By Daniel St\"uwe\<close>
    5.48 +
    5.49 +fun fib_tree :: "nat \<Rightarrow> unit avl_tree" where
    5.50 +"fib_tree 0 = Leaf" |
    5.51 +"fib_tree (Suc 0) = Node 1 Leaf () Leaf" |
    5.52 +"fib_tree (Suc(Suc n)) = Node (Suc(Suc(n))) (fib_tree (Suc n)) () (fib_tree n)"
    5.53 +
    5.54 +lemma [simp]: "ht (fib_tree h) = h"
    5.55 +by (induction h rule: "fib_tree.induct") auto
    5.56 +
    5.57 +lemma [simp]: "height (fib_tree h) = h"
    5.58 +by (induction h rule: "fib_tree.induct") auto
    5.59 +
    5.60 +lemma "avl(fib_tree h)"          
    5.61 +by (induction h rule: "fib_tree.induct") auto
    5.62 +
    5.63 +lemma fib_tree_size1: "size1 (fib_tree h) = fib (h+2)"
    5.64 +by (induction h rule: fib_tree.induct) auto
    5.65 +
    5.66 +lemma height_invers[simp]: 
    5.67 +  "(height t = 0) = (t = Leaf)"
    5.68 +  "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node (Suc h) l a r)"
    5.69 +by (induction t) auto
    5.70 +
    5.71 +lemma fib_Suc_lt: "fib n \<le> fib (Suc n)"
    5.72 +by (induction n rule: fib.induct) auto
    5.73 +
    5.74 +lemma fib_mono: "n \<le> m \<Longrightarrow> fib n \<le> fib m"
    5.75 +proof (induction n arbitrary: m rule: fib.induct )
    5.76 +  case (2 m)
    5.77 +  thus ?case using fib_neq_0_nat[of m] by auto
    5.78 +next
    5.79 +  case (3 n m)
    5.80 +  from 3 obtain m' where "m = Suc (Suc m')"
    5.81 +    by (metis le_Suc_ex plus_nat.simps(2)) 
    5.82 +  thus ?case using 3(1)[of "Suc m'"] 3(2)[of m'] 3(3) by auto
    5.83 +qed simp
    5.84 +
    5.85 +lemma size1_fib_tree_mono:
    5.86 +  assumes "n \<le> m"
    5.87 +  shows   "size1 (fib_tree n) \<le> size1 (fib_tree m)"
    5.88 +using fib_tree_size1 fib_mono[OF assms] fib_mono[of "Suc n"] add_le_mono assms by fastforce 
    5.89 +
    5.90 +lemma fib_tree_minimal: "avl t \<Longrightarrow> size1 (fib_tree (ht t)) \<le> size1 t"
    5.91 +proof (induction "ht t" arbitrary: t rule: fib_tree.induct)
    5.92 +  case (2 t)
    5.93 +  from 2 obtain l a r where "t = Node (Suc 0) l a r" by (cases t) auto
    5.94 +  with 2 show ?case by auto
    5.95 +next
    5.96 +  case (3 h t)
    5.97 +  note [simp] = 3(3)[symmetric] 
    5.98 +  from 3 obtain l a r where [simp]: "t = Node (Suc (Suc h)) l a r" by (cases t) auto
    5.99 +  show ?case proof (cases rule: linorder_cases[of "ht l" "ht r"]) 
   5.100 +    case equal
   5.101 +    with 3(3,4) have ht: "ht l = Suc h" "ht r = Suc h" by auto
   5.102 +    with 3 have "size1 (fib_tree (ht l)) \<le> size1 l" by auto moreover
   5.103 +    from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \<le> size1 r" by auto ultimately
   5.104 +    show ?thesis using ht size1_fib_tree_mono[of h "Suc h"] by auto
   5.105 +  next
   5.106 +    case greater
   5.107 +    with 3(3,4) have ht: "ht l = Suc h"  "ht r = h" by auto
   5.108 +    from ht 3(1,2,4) have "size1 (fib_tree (Suc h)) \<le> size1 l" by auto moreover
   5.109 +    from ht 3(1,2,4) have "size1 (fib_tree h) \<le> size1 r" by auto ultimately
   5.110 +    show ?thesis by auto
   5.111 +  next
   5.112 +    case less (* analogously *)
   5.113 +    with 3 have ht: "ht l = h"  "Suc h = ht r" by auto
   5.114 +    from ht 3 have "size1 (fib_tree h) \<le> size1 l" by auto moreover
   5.115 +    from ht 3 have "size1 (fib_tree (Suc h)) \<le> size1 r" by auto ultimately
   5.116 +    show ?thesis by auto
   5.117 +  qed
   5.118 +qed auto
   5.119 +
   5.120 +theorem avl_size_bound: "avl t \<Longrightarrow> fib(height t + 2) \<le> size1 t" 
   5.121 +using fib_tree_minimal fib_tree_size1 by fastforce
   5.122 +
   5.123  end
     6.1 --- a/src/HOL/Data_Structures/Brother12_Map.thy	Thu Jul 07 09:24:03 2016 +0200
     6.2 +++ b/src/HOL/Data_Structures/Brother12_Map.thy	Thu Jul 07 18:08:02 2016 +0200
     6.3 @@ -8,7 +8,7 @@
     6.4    Map_by_Ordered
     6.5  begin
     6.6  
     6.7 -fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::cmp \<Rightarrow> 'b option" where
     6.8 +fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::linorder \<Rightarrow> 'b option" where
     6.9  "lookup N0 x = None" |
    6.10  "lookup (N1 t) x = lookup t x" |
    6.11  "lookup (N2 l (a,b) r) x =
    6.12 @@ -20,7 +20,7 @@
    6.13  locale update = insert
    6.14  begin
    6.15  
    6.16 -fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    6.17 +fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    6.18  "upd x y N0 = L2 (x,y)" |
    6.19  "upd x y (N1 t) = n1 (upd x y t)" |
    6.20  "upd x y (N2 l (a,b) r) =
    6.21 @@ -29,7 +29,7 @@
    6.22       EQ \<Rightarrow> N2 l (a,y) r |
    6.23       GT \<Rightarrow> n2 l (a,b) (upd x y r))"
    6.24  
    6.25 -definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    6.26 +definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    6.27  "update x y t = tree(upd x y t)"
    6.28  
    6.29  end
    6.30 @@ -37,7 +37,7 @@
    6.31  context delete
    6.32  begin
    6.33  
    6.34 -fun del :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    6.35 +fun del :: "'a::linorder \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    6.36  "del _ N0         = N0" |
    6.37  "del x (N1 t)     = N1 (del x t)" |
    6.38  "del x (N2 l (a,b) r) =
    6.39 @@ -48,7 +48,7 @@
    6.40                None \<Rightarrow> N1 l |
    6.41                Some (ab, r') \<Rightarrow> n2 l ab r'))"
    6.42  
    6.43 -definition delete :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    6.44 +definition delete :: "'a::linorder \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    6.45  "delete a t = tree (del a t)"
    6.46  
    6.47  end
    6.48 @@ -180,7 +180,7 @@
    6.49            show ?thesis by simp
    6.50          qed
    6.51        qed
    6.52 -    } ultimately show ?case by auto
    6.53 +    } ultimately show ?case by auto                         
    6.54    }
    6.55    { case 2 with Suc.IH(1) show ?case by auto }
    6.56  qed auto
     7.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Thu Jul 07 09:24:03 2016 +0200
     7.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Thu Jul 07 18:08:02 2016 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(* Author: Tobias Nipkow *)
     7.5 +(* Author: Tobias Nipkow, Daniel Stüwe *)
     7.6  
     7.7  section \<open>1-2 Brother Tree Implementation of Sets\<close>
     7.8  
     7.9 @@ -6,6 +6,7 @@
    7.10  imports
    7.11    Cmp
    7.12    Set_by_Ordered
    7.13 +  "~~/src/HOL/Number_Theory/Fib"
    7.14  begin
    7.15  
    7.16  subsection \<open>Data Type and Operations\<close>
    7.17 @@ -25,7 +26,7 @@
    7.18  "inorder (L2 a) = [a]" |
    7.19  "inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"
    7.20  
    7.21 -fun isin :: "'a bro \<Rightarrow> 'a::cmp \<Rightarrow> bool" where
    7.22 +fun isin :: "'a bro \<Rightarrow> 'a::linorder \<Rightarrow> bool" where
    7.23  "isin N0 x = False" |
    7.24  "isin (N1 t) x = isin t x" |
    7.25  "isin (N2 l a r) x =
    7.26 @@ -53,7 +54,7 @@
    7.27  "n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
    7.28  "n2 t1 a t2 = N2 t1 a t2"
    7.29  
    7.30 -fun ins :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    7.31 +fun ins :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    7.32  "ins x N0 = L2 x" |
    7.33  "ins x (N1 t) = n1 (ins x t)" |
    7.34  "ins x (N2 l a r) =
    7.35 @@ -67,7 +68,7 @@
    7.36  "tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
    7.37  "tree t = t"
    7.38  
    7.39 -definition insert :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    7.40 +definition insert :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    7.41  "insert x t = tree(ins x t)"
    7.42  
    7.43  end
    7.44 @@ -102,7 +103,7 @@
    7.45       None \<Rightarrow> Some (a, N1 t2) |
    7.46       Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
    7.47  
    7.48 -fun del :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    7.49 +fun del :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    7.50  "del _ N0         = N0" |
    7.51  "del x (N1 t)     = N1 (del x t)" |
    7.52  "del x (N2 l a r) =
    7.53 @@ -117,7 +118,7 @@
    7.54  "tree (N1 t) = t" |
    7.55  "tree t = t"
    7.56  
    7.57 -definition delete :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    7.58 +definition delete :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    7.59  "delete a t = tree (del a t)"
    7.60  
    7.61  end
    7.62 @@ -483,4 +484,68 @@
    7.63    case 7 thus ?case using delete.delete_type by blast
    7.64  qed auto
    7.65  
    7.66 +
    7.67 +subsection \<open>Height-Size Relation\<close>
    7.68 +
    7.69 +text \<open>By Daniel St\"uwe\<close>
    7.70 +
    7.71 +fun fib_tree :: "nat \<Rightarrow> unit bro" where
    7.72 +  "fib_tree 0 = N0" 
    7.73 +| "fib_tree (Suc 0) = N2 N0 () N0"
    7.74 +| "fib_tree (Suc(Suc h)) = N2 (fib_tree (h+1)) () (N1 (fib_tree h))"
    7.75 +
    7.76 +fun fib' :: "nat \<Rightarrow> nat" where
    7.77 +  "fib' 0 = 0" 
    7.78 +| "fib' (Suc 0) = 1"
    7.79 +| "fib' (Suc(Suc h)) = 1 + fib' (Suc h) + fib' h"
    7.80 +
    7.81 +fun size :: "'a bro \<Rightarrow> nat" where
    7.82 +  "size N0 = 0" 
    7.83 +| "size (N1 t) = size t"
    7.84 +| "size (N2 t1 _ t2) = 1 + size t1 + size t2"
    7.85 +
    7.86 +lemma fib_tree_B: "fib_tree h \<in> B h"
    7.87 +by (induction h rule: fib_tree.induct) auto
    7.88 +
    7.89 +declare [[names_short]]
    7.90 +
    7.91 +lemma size_fib': "size (fib_tree h) = fib' h"
    7.92 +by (induction h rule: fib_tree.induct) auto
    7.93 +
    7.94 +lemma fibfib: "fib' h + 1 = fib (Suc(Suc h))"
    7.95 +by (induction h rule: fib_tree.induct) auto
    7.96 +
    7.97 +lemma B_N2_cases[consumes 1]:
    7.98 +assumes "N2 t1 a t2 \<in> B (Suc n)"
    7.99 +obtains 
   7.100 +  (BB) "t1 \<in> B n" and "t2 \<in> B n" |
   7.101 +  (UB) "t1 \<in> U n" and "t2 \<in> B n" |
   7.102 +  (BU) "t1 \<in> B n" and "t2 \<in> U n"
   7.103 +using assms by auto
   7.104 +
   7.105 +lemma size_bounded: "t \<in> B h \<Longrightarrow> size t \<ge> size (fib_tree h)"
   7.106 +unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct)
   7.107 +case (3 h t')
   7.108 +  note main = 3
   7.109 +  then obtain t1 a t2 where t': "t' = N2 t1 a t2" by auto
   7.110 +  with main have "N2 t1 a t2 \<in> B (Suc (Suc h))" by auto
   7.111 +  thus ?case proof (cases rule: B_N2_cases)
   7.112 +    case BB
   7.113 +    then obtain x y z where t2: "t2 = N2 x y z \<or> t2 = N2 z y x" "x \<in> B h" by auto
   7.114 +    show ?thesis unfolding t' using main(1)[OF BB(1)] main(2)[OF t2(2)] t2(1) by auto
   7.115 +  next
   7.116 +    case UB
   7.117 +    then obtain t11 where t1: "t1 = N1 t11" "t11 \<in> B h" by auto
   7.118 +    show ?thesis unfolding t' t1(1) using main(2)[OF t1(2)] main(1)[OF UB(2)] by simp
   7.119 +  next
   7.120 +    case BU
   7.121 +    then obtain t22 where t2: "t2 = N1 t22" "t22 \<in> B h" by auto
   7.122 +    show ?thesis unfolding t' t2(1) using main(2)[OF t2(2)] main(1)[OF BU(1)] by simp
   7.123 +  qed
   7.124 +qed auto
   7.125 +
   7.126 +theorem "t \<in> B h \<Longrightarrow> fib (h + 2) \<le> size t + 1"
   7.127 +using size_bounded
   7.128 +by (simp add: size_fib' fibfib[symmetric] del: fib.simps)
   7.129 +
   7.130  end
     8.1 --- a/src/HOL/Data_Structures/Cmp.thy	Thu Jul 07 09:24:03 2016 +0200
     8.2 +++ b/src/HOL/Data_Structures/Cmp.thy	Thu Jul 07 18:08:02 2016 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(* Author: Tobias Nipkow *)
     8.5 +(* Author: Tobias Nipkow, Daniel Stüwe *)
     8.6  
     8.7  section {* Three-Way Comparison *}
     8.8  
     8.9 @@ -6,16 +6,23 @@
    8.10  imports Main
    8.11  begin
    8.12  
    8.13 -datatype cmp = LT | EQ | GT
    8.14 +datatype cmp_val = LT | EQ | GT
    8.15  
    8.16 -class cmp = linorder +
    8.17 -fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> cmp"
    8.18 -assumes LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
    8.19 -assumes EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
    8.20 -assumes GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
    8.21 +function cmp :: "'a:: linorder \<Rightarrow> 'a \<Rightarrow> cmp_val" where
    8.22 +"x < y \<Longrightarrow> cmp x y = LT" |
    8.23 +"x = y \<Longrightarrow> cmp x y = EQ" |
    8.24 +"x > y \<Longrightarrow> cmp x y = GT"
    8.25 +by (auto, force)
    8.26 +termination by lexicographic_order
    8.27 +
    8.28 +lemma 
    8.29 +    LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
    8.30 +and EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
    8.31 +and GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
    8.32 +by (cases x y rule: linorder_cases, auto)+
    8.33  
    8.34  lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) =
    8.35    (if c = LT then l else if c = GT then g else e)"
    8.36 -by(simp split: cmp.split)
    8.37 +by(simp split: cmp_val.split)
    8.38  
    8.39  end
     9.1 --- a/src/HOL/Data_Structures/Isin2.thy	Thu Jul 07 09:24:03 2016 +0200
     9.2 +++ b/src/HOL/Data_Structures/Isin2.thy	Thu Jul 07 18:08:02 2016 +0200
     9.3 @@ -9,7 +9,7 @@
     9.4    Set_by_Ordered
     9.5  begin
     9.6  
     9.7 -fun isin :: "('a::cmp,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
     9.8 +fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
     9.9  "isin Leaf x = False" |
    9.10  "isin (Node _ l a r) x =
    9.11    (case cmp x a of
    10.1 --- a/src/HOL/Data_Structures/Lookup2.thy	Thu Jul 07 09:24:03 2016 +0200
    10.2 +++ b/src/HOL/Data_Structures/Lookup2.thy	Thu Jul 07 18:08:02 2016 +0200
    10.3 @@ -9,7 +9,7 @@
    10.4    Map_by_Ordered
    10.5  begin
    10.6  
    10.7 -fun lookup :: "('a::cmp * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
    10.8 +fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
    10.9  "lookup Leaf x = None" |
   10.10  "lookup (Node _ l (a,b) r) x =
   10.11    (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
    11.1 --- a/src/HOL/Data_Structures/RBT_Map.thy	Thu Jul 07 09:24:03 2016 +0200
    11.2 +++ b/src/HOL/Data_Structures/RBT_Map.thy	Thu Jul 07 18:08:02 2016 +0200
    11.3 @@ -8,7 +8,7 @@
    11.4    Lookup2
    11.5  begin
    11.6  
    11.7 -fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
    11.8 +fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
    11.9  "upd x y Leaf = R Leaf (x,y) Leaf" |
   11.10  "upd x y (B l (a,b) r) = (case cmp x a of
   11.11    LT \<Rightarrow> bal (upd x y l) (a,b) r |
   11.12 @@ -19,12 +19,12 @@
   11.13    GT \<Rightarrow> R l (a,b) (upd x y r) |
   11.14    EQ \<Rightarrow> R l (x,y) r)"
   11.15  
   11.16 -definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
   11.17 +definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
   11.18  "update x y t = paint Black (upd x y t)"
   11.19  
   11.20 -fun del :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
   11.21 -and delL :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
   11.22 -and delR :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
   11.23 +fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
   11.24 +and delL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
   11.25 +and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
   11.26  where
   11.27  "del x Leaf = Leaf" |
   11.28  "del x (Node c t1 (a,b) t2) = (case cmp x a of
   11.29 @@ -36,7 +36,7 @@
   11.30  "delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | 
   11.31  "delR x t1 a t2 = R t1 a (del x t2)"
   11.32  
   11.33 -definition delete :: "'a::cmp \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
   11.34 +definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
   11.35  "delete x t = paint Black (del x t)"
   11.36  
   11.37  
    12.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Jul 07 09:24:03 2016 +0200
    12.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Jul 07 18:08:02 2016 +0200
    12.3 @@ -1,4 +1,4 @@
    12.4 -(* Author: Tobias Nipkow *)
    12.5 +(* Author: Tobias Nipkow, Daniel Stüwe *)
    12.6  
    12.7  section \<open>Red-Black Tree Implementation of Sets\<close>
    12.8  
    12.9 @@ -9,7 +9,7 @@
   12.10    Isin2
   12.11  begin
   12.12  
   12.13 -fun ins :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
   12.14 +fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
   12.15  "ins x Leaf = R Leaf x Leaf" |
   12.16  "ins x (B l a r) =
   12.17    (case cmp x a of
   12.18 @@ -22,12 +22,12 @@
   12.19      GT \<Rightarrow> R l a (ins x r) |
   12.20      EQ \<Rightarrow> R l a r)"
   12.21  
   12.22 -definition insert :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
   12.23 +definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
   12.24  "insert x t = paint Black (ins x t)"
   12.25  
   12.26 -fun del :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
   12.27 -and delL :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
   12.28 -and delR :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
   12.29 +fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
   12.30 +and delL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
   12.31 +and delR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
   12.32  where
   12.33  "del x Leaf = Leaf" |
   12.34  "del x (Node _ l a r) =
   12.35 @@ -40,7 +40,7 @@
   12.36  "delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | 
   12.37  "delR x l a r = R l a (del x r)"
   12.38  
   12.39 -definition delete :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
   12.40 +definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
   12.41  "delete x t = paint Black (del x t)"
   12.42  
   12.43  
   12.44 @@ -88,21 +88,9 @@
   12.45  by (auto simp: delete_def inorder_del inorder_paint)
   12.46  
   12.47  
   12.48 -interpretation Set_by_Ordered
   12.49 -where empty = Leaf and isin = isin and insert = insert and delete = delete
   12.50 -and inorder = inorder and inv = "\<lambda>_. True"
   12.51 -proof (standard, goal_cases)
   12.52 -  case 1 show ?case by simp
   12.53 -next
   12.54 -  case 2 thus ?case by(simp add: isin_set)
   12.55 -next
   12.56 -  case 3 thus ?case by(simp add: inorder_insert)
   12.57 -next
   12.58 -  case 4 thus ?case by(simp add: inorder_delete)
   12.59 -qed auto
   12.60 +subsection \<open>Structural invariants\<close>
   12.61  
   12.62 -
   12.63 -subsection \<open>Structural invariants\<close>
   12.64 +text\<open>The proofs are due to Markus Reiter and Alexander Krauss,\<close>
   12.65  
   12.66  fun color :: "'a rbt \<Rightarrow> color" where
   12.67  "color Leaf = Black" |
   12.68 @@ -112,24 +100,24 @@
   12.69  "bheight Leaf = 0" |
   12.70  "bheight (Node c l x r) = (if c = Black then Suc(bheight l) else bheight l)"
   12.71  
   12.72 -fun inv1 :: "'a rbt \<Rightarrow> bool" where
   12.73 -"inv1 Leaf = True" |
   12.74 -"inv1 (Node c l a r) =
   12.75 -  (inv1 l \<and> inv1 r \<and> (c = Black \<or> color l = Black \<and> color r = Black))"
   12.76 +fun invc :: "'a rbt \<Rightarrow> bool" where
   12.77 +"invc Leaf = True" |
   12.78 +"invc (Node c l a r) =
   12.79 +  (invc l \<and> invc r \<and> (c = Black \<or> color l = Black \<and> color r = Black))"
   12.80  
   12.81 -fun inv1_root :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
   12.82 -"inv1_root Leaf = True" |
   12.83 -"inv1_root (Node c l a r) = (inv1 l \<and> inv1 r)"
   12.84 +fun invc_sons :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
   12.85 +"invc_sons Leaf = True" |
   12.86 +"invc_sons (Node c l a r) = (invc l \<and> invc r)"
   12.87  
   12.88 -fun inv2 :: "'a rbt \<Rightarrow> bool" where
   12.89 -"inv2 Leaf = True" |
   12.90 -"inv2 (Node c l x r) = (inv2 l \<and> inv2 r \<and> bheight l = bheight r)"
   12.91 +fun invh :: "'a rbt \<Rightarrow> bool" where
   12.92 +"invh Leaf = True" |
   12.93 +"invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
   12.94  
   12.95 -lemma inv1_rootI[simp]: "inv1 t \<Longrightarrow> inv1_root t"
   12.96 +lemma invc_sonsI: "invc t \<Longrightarrow> invc_sons t"
   12.97  by (cases t) simp+
   12.98  
   12.99  definition rbt :: "'a rbt \<Rightarrow> bool" where
  12.100 -"rbt t = (inv1 t \<and> inv2 t \<and> color t = Black)"
  12.101 +"rbt t = (invc t \<and> invh t \<and> color t = Black)"
  12.102  
  12.103  lemma color_paint_Black: "color (paint Black t) = Black"
  12.104  by (cases t) auto
  12.105 @@ -137,142 +125,386 @@
  12.106  theorem rbt_Leaf: "rbt Leaf"
  12.107  by (simp add: rbt_def)
  12.108  
  12.109 -lemma paint_inv1_root: "inv1_root t \<Longrightarrow> inv1_root (paint c t)"
  12.110 +lemma paint_invc_sons: "invc_sons t \<Longrightarrow> invc_sons (paint c t)"
  12.111  by (cases t) auto
  12.112  
  12.113 -lemma inv1_paint_Black: "inv1_root t \<Longrightarrow> inv1 (paint Black t)"
  12.114 +lemma invc_paint_Black: "invc_sons t \<Longrightarrow> invc (paint Black t)"
  12.115  by (cases t) auto
  12.116  
  12.117 -lemma inv2_paint: "inv2 t \<Longrightarrow> inv2 (paint c t)"
  12.118 +lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
  12.119  by (cases t) auto
  12.120  
  12.121 -lemma inv1_bal: "\<lbrakk>inv1_root l; inv1_root r\<rbrakk> \<Longrightarrow> inv1 (bal l a r)" 
  12.122 +lemma invc_bal: "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
  12.123  by (induct l a r rule: bal.induct) auto
  12.124  
  12.125  lemma bheight_bal:
  12.126    "bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)"
  12.127  by (induct l a r rule: bal.induct) auto
  12.128  
  12.129 -lemma inv2_bal: 
  12.130 -  "\<lbrakk> inv2 l; inv2 r; bheight l = bheight r \<rbrakk> \<Longrightarrow> inv2 (bal l a r)"
  12.131 +lemma invh_bal: 
  12.132 +  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (bal l a r)"
  12.133  by (induct l a r rule: bal.induct) auto
  12.134  
  12.135  
  12.136  subsubsection \<open>Insertion\<close>
  12.137  
  12.138 -lemma inv1_ins: assumes "inv1 t"
  12.139 -  shows "color t = Black \<Longrightarrow> inv1 (ins x t)" "inv1_root (ins x t)"
  12.140 +lemma invc_ins: assumes "invc t"
  12.141 +  shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc_sons (ins x t)"
  12.142  using assms
  12.143 -by (induct x t rule: ins.induct) (auto simp: inv1_bal)
  12.144 +by (induct x t rule: ins.induct) (auto simp: invc_bal invc_sonsI)
  12.145  
  12.146 -lemma inv2_ins: assumes "inv2 t"
  12.147 -  shows "inv2 (ins x t)" "bheight (ins x t) = bheight t"
  12.148 +lemma invh_ins: assumes "invh t"
  12.149 +  shows "invh (ins x t)" "bheight (ins x t) = bheight t"
  12.150  using assms
  12.151 -by (induct x t rule: ins.induct) (auto simp: inv2_bal bheight_bal)
  12.152 +by (induct x t rule: ins.induct) (auto simp: invh_bal bheight_bal)
  12.153  
  12.154 -theorem rbt_ins: "rbt t \<Longrightarrow> rbt (insert x t)"
  12.155 -by (simp add: inv1_ins inv2_ins color_paint_Black inv1_paint_Black inv2_paint
  12.156 +theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
  12.157 +by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
  12.158    rbt_def insert_def)
  12.159  
  12.160 -(*
  12.161 -lemma bheight_paintR'[simp]: "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
  12.162 +
  12.163 +subsubsection \<open>Deletion\<close>
  12.164 +
  12.165 +lemma bheight_paint_Red:
  12.166 +  "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
  12.167  by (cases t) auto
  12.168  
  12.169 -lemma balL_inv2_with_inv1:
  12.170 -  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
  12.171 -  shows "bheight (balL lt a rt) = bheight lt + 1"  "inv2 (balL lt a rt)"
  12.172 +lemma balL_invh_with_invc:
  12.173 +  assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "invc rt"
  12.174 +  shows "bheight (balL lt a rt) = bheight lt + 1"  "invh (balL lt a rt)"
  12.175  using assms 
  12.176 -by (induct lt a rt rule: balL.induct) (auto simp: inv2_bal inv2_paint bheight_bal)
  12.177 +by (induct lt a rt rule: balL.induct)
  12.178 +   (auto simp: invh_bal invh_paint bheight_bal bheight_paint_Red)
  12.179  
  12.180 -lemma balL_inv2_app: 
  12.181 -  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color rt = Black"
  12.182 -  shows "inv2 (balL lt a rt)" 
  12.183 +lemma balL_invh_app: 
  12.184 +  assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "color rt = Black"
  12.185 +  shows "invh (balL lt a rt)" 
  12.186          "bheight (balL lt a rt) = bheight rt"
  12.187  using assms 
  12.188 -by (induct lt a rt rule: balL.induct) (auto simp add: inv2_bal bheight_bal) 
  12.189 +by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal) 
  12.190  
  12.191 -lemma balL_inv1: "\<lbrakk>inv1_root l; inv1 r; color r = Black\<rbrakk> \<Longrightarrow> inv1 (balL l a r)"
  12.192 -by (induct l a r rule: balL.induct) (simp_all add: inv1_bal)
  12.193 +lemma balL_invc: "\<lbrakk>invc_sons l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
  12.194 +by (induct l a r rule: balL.induct) (simp_all add: invc_bal)
  12.195  
  12.196 -lemma balL_inv1_root: "\<lbrakk> inv1_root lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1_root (balL lt a rt)"
  12.197 -by (induct lt a rt rule: balL.induct) (auto simp: inv1_bal paint_inv1_root)
  12.198 +lemma balL_invc_sons: "\<lbrakk> invc_sons lt; invc rt \<rbrakk> \<Longrightarrow> invc_sons (balL lt a rt)"
  12.199 +by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI)
  12.200  
  12.201 -lemma balR_inv2_with_inv1:
  12.202 -  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
  12.203 -  shows "inv2 (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
  12.204 +lemma balR_invh_with_invc:
  12.205 +  assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt"
  12.206 +  shows "invh (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
  12.207  using assms
  12.208 -by(induct lt a rt rule: balR.induct)(auto simp: inv2_bal bheight_bal inv2_paint)
  12.209 +by(induct lt a rt rule: balR.induct)
  12.210 +  (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red)
  12.211  
  12.212 -lemma balR_inv1: "\<lbrakk>inv1 a; inv1_root b; color a = Black\<rbrakk> \<Longrightarrow> inv1 (balR a x b)"
  12.213 -by (induct a x b rule: balR.induct) (simp_all add: inv1_bal)
  12.214 +lemma invc_balR: "\<lbrakk>invc a; invc_sons b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
  12.215 +by (induct a x b rule: balR.induct) (simp_all add: invc_bal)
  12.216  
  12.217 -lemma balR_inv1_root: "\<lbrakk> inv1 lt; inv1_root rt \<rbrakk> \<Longrightarrow>inv1_root (balR lt x rt)"
  12.218 -by (induct lt x rt rule: balR.induct) (auto simp: inv1_bal paint_inv1_root)
  12.219 +lemma invc_sons_balR: "\<lbrakk> invc lt; invc_sons rt \<rbrakk> \<Longrightarrow>invc_sons (balR lt x rt)"
  12.220 +by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI)
  12.221  
  12.222 -lemma combine_inv2:
  12.223 -  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
  12.224 -  shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)"
  12.225 +lemma invh_combine:
  12.226 +  assumes "invh lt" "invh rt" "bheight lt = bheight rt"
  12.227 +  shows "bheight (combine lt rt) = bheight lt" "invh (combine lt rt)"
  12.228  using assms 
  12.229  by (induct lt rt rule: combine.induct) 
  12.230 -   (auto simp: balL_inv2_app split: tree.splits color.splits)
  12.231 +   (auto simp: balL_invh_app split: tree.splits color.splits)
  12.232  
  12.233 -lemma combine_inv1: 
  12.234 -  assumes "inv1 lt" "inv1 rt"
  12.235 -  shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> inv1 (combine lt rt)"
  12.236 -         "inv1_root (combine lt rt)"
  12.237 +lemma invc_combine: 
  12.238 +  assumes "invc lt" "invc rt"
  12.239 +  shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> invc (combine lt rt)"
  12.240 +         "invc_sons (combine lt rt)"
  12.241  using assms 
  12.242  by (induct lt rt rule: combine.induct)
  12.243 -   (auto simp: balL_inv1 split: tree.splits color.splits)
  12.244 +   (auto simp: balL_invc invc_sonsI split: tree.splits color.splits)
  12.245  
  12.246  
  12.247 -lemma 
  12.248 -  assumes "inv2 lt" "inv1 lt"
  12.249 +lemma assumes "invh lt" "invc lt"
  12.250    shows
  12.251 -  "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
  12.252 -   inv2 (rbt_del_from_left x lt k v rt) \<and> 
  12.253 -   bheight (rbt_del_from_left x lt k v rt) = bheight lt \<and> 
  12.254 -   (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_left x lt k v rt) \<or> 
  12.255 -    (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_left x lt k v rt))"
  12.256 -  and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
  12.257 -  inv2 (rbt_del_from_right x lt k v rt) \<and> 
  12.258 -  bheight (rbt_del_from_right x lt k v rt) = bheight lt \<and> 
  12.259 -  (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_right x lt k v rt) \<or> 
  12.260 -   (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_right x lt k v rt))"
  12.261 -  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) 
  12.262 -  \<or> color_of lt = B \<and> bheight (rbt_del x lt) = bheight lt - 1 \<and> inv1l (rbt_del x lt))"
  12.263 +  del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt) 
  12.264 +  \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc_sons (del x lt))"
  12.265 +and  "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
  12.266 +   invh (delL x lt k rt) \<and> 
  12.267 +   bheight (delL x lt k rt) = bheight lt \<and> 
  12.268 +   (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or> 
  12.269 +    (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delL x lt k rt))"
  12.270 +  and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
  12.271 +  invh (delR x lt k rt) \<and> 
  12.272 +  bheight (delR x lt k rt) = bheight lt \<and> 
  12.273 +  (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or> 
  12.274 +   (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delR x lt k rt))"
  12.275  using assms
  12.276 -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)
  12.277 +proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct)
  12.278  case (2 y c _ y')
  12.279    have "y = y' \<or> y < y' \<or> y > y'" by auto
  12.280    thus ?case proof (elim disjE)
  12.281      assume "y = y'"
  12.282 -    with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
  12.283 +    with 2 show ?thesis
  12.284 +    by (cases c) (simp_all add: invh_combine invc_combine)
  12.285    next
  12.286      assume "y < y'"
  12.287 -    with 2 show ?thesis by (cases c) auto
  12.288 +    with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
  12.289    next
  12.290      assume "y' < y"
  12.291 -    with 2 show ?thesis by (cases c) auto
  12.292 +    with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
  12.293    qed
  12.294  next
  12.295 -  case (3 y lt z v rta y' ss bb) 
  12.296 -  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)+
  12.297 +  case (3 y lt z rta y' bb)
  12.298 +  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)+
  12.299  next
  12.300 -  case (5 y a y' ss lt z v rta)
  12.301 -  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)+
  12.302 +  case (5 y a y' lt z rta)
  12.303 +  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)+
  12.304  next
  12.305 -  case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
  12.306 +  case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
  12.307  qed auto
  12.308  
  12.309 -theorem rbt_delete_is_rbt [simp]: assumes "rbt t" shows "rbt (delete k t)"
  12.310 +theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
  12.311 +by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc_sonsI invh_paint)
  12.312 +
  12.313 +text \<open>Overall correctness:\<close>
  12.314 +
  12.315 +interpretation Set_by_Ordered
  12.316 +where empty = Leaf and isin = isin and insert = insert and delete = delete
  12.317 +and inorder = inorder and inv = rbt
  12.318 +proof (standard, goal_cases)
  12.319 +  case 1 show ?case by simp
  12.320 +next
  12.321 +  case 2 thus ?case by(simp add: isin_set)
  12.322 +next
  12.323 +  case 3 thus ?case by(simp add: inorder_insert)
  12.324 +next
  12.325 +  case 4 thus ?case by(simp add: inorder_delete)
  12.326 +next
  12.327 +  case 5 thus ?case by (simp add: rbt_Leaf) 
  12.328 +next
  12.329 +  case 6 thus ?case by (simp add: rbt_insert) 
  12.330 +next
  12.331 +  case 7 thus ?case by (simp add: rbt_delete) 
  12.332 +qed
  12.333 +
  12.334 +
  12.335 +subsection \<open>Height-Size Relation\<close>
  12.336 +
  12.337 +text \<open>By Daniel St\"uwe\<close>
  12.338 +
  12.339 +lemma color_RedE:"color t = Red \<Longrightarrow> invc t =
  12.340 + (\<exists> l a r . t = R l a r \<and> color l = Black \<and> color r = Black \<and> invc l \<and> invc r)"
  12.341 +by (cases t) auto
  12.342 +
  12.343 +lemma rbt_induct[consumes 1]:
  12.344 +  assumes "rbt t"
  12.345 +  assumes [simp]: "P Leaf"
  12.346 +  assumes "\<And> t l a r. \<lbrakk>t = B l a r; invc t; invh t; Q(l); Q(r)\<rbrakk> \<Longrightarrow> P t"
  12.347 +  assumes "\<And> t l a r. \<lbrakk>t = R l a r; invc t; invh t; P(l); P(r)\<rbrakk> \<Longrightarrow> Q t"
  12.348 +  assumes "\<And> t . P(t) \<Longrightarrow> Q(t)"
  12.349 +  shows "P t"
  12.350 +using assms(1) unfolding rbt_def apply safe
  12.351 +proof (induction t rule: measure_induct[of size])
  12.352 +case (1 t)
  12.353 +  note * = 1 assms
  12.354 +  show ?case proof (cases t)
  12.355 +    case [simp]: (Node c l a r)
  12.356 +    show ?thesis proof (cases c)
  12.357 +      case Red thus ?thesis using 1 by simp
  12.358 +    next
  12.359 +      case [simp]: Black
  12.360 +      show ?thesis
  12.361 +      proof (cases "color l")
  12.362 +        case Red
  12.363 +        thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
  12.364 +      next
  12.365 +        case Black
  12.366 +        thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
  12.367 +      qed
  12.368 +    qed
  12.369 +  qed simp
  12.370 +qed
  12.371 +
  12.372 +lemma rbt_b_height: "rbt t \<Longrightarrow> bheight t * 2 \<ge> height t"
  12.373 +by (induction t rule: rbt_induct[where Q="\<lambda> t. bheight t * 2 + 1 \<ge> height t"]) auto
  12.374 +
  12.375 +lemma red_b_height: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t * 2 + 1 \<ge> height t"
  12.376 +apply (cases t) apply simp
  12.377 +  using rbt_b_height unfolding rbt_def
  12.378 +  by (cases "color t") fastforce+
  12.379 +
  12.380 +lemma red_b_height2: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t \<ge> height t div 2"
  12.381 +using red_b_height by fastforce
  12.382 +
  12.383 +lemma rbt_b_height2: "bheight t \<le> height t"
  12.384 +by (induction t) auto
  12.385 +
  12.386 +lemma "rbt t \<Longrightarrow> size1 t \<le>  4 ^ (bheight t)"
  12.387 +by(induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<le>  2 * 4 ^ (bheight t)"]) auto
  12.388 +
  12.389 +lemma bheight_size_bound:  "rbt t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
  12.390 +by (induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<ge>  2 ^ (bheight t)"]) auto
  12.391 +
  12.392 +text \<open>Balanced red-balck tree with all black nodes:\<close>
  12.393 +inductive balB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool"  where
  12.394 +"balB 0 Leaf" |
  12.395 +"balB h t \<Longrightarrow> balB (Suc h) (B t () t)"
  12.396 +
  12.397 +inductive_cases [elim!]: "balB 0 t"
  12.398 +inductive_cases [elim]: "balB (Suc h) t"
  12.399 +
  12.400 +lemma balB_hs: "balB h t \<Longrightarrow> bheight t = height t"
  12.401 +by (induction h t rule: "balB.induct") auto
  12.402 +
  12.403 +lemma balB_h: "balB h t \<Longrightarrow> h = height t"
  12.404 +by (induction h t rule: "balB.induct") auto
  12.405 +
  12.406 +lemma "rbt t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
  12.407 +by (induction t arbitrary: t' 
  12.408 + rule: rbt_induct[where Q="\<lambda> t . \<forall> h t'. balB (bheight t) t' \<longrightarrow> size t' \<le> size t"])
  12.409 + fastforce+
  12.410 +
  12.411 +lemma balB_bh: "invc t \<Longrightarrow> invh t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
  12.412 +by (induction t arbitrary: t') (fastforce split: if_split_asm)+
  12.413 +
  12.414 +lemma balB_bh3:"\<lbrakk> balB h t; balB (h' + h) t' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
  12.415 +by (induction h t arbitrary: t' h' rule: balB.induct)  fastforce+
  12.416 +
  12.417 +corollary balB_bh3': "\<lbrakk> balB h t; balB h' t'; h \<le> h' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
  12.418 +using balB_bh3 le_Suc_ex by (fastforce simp: algebra_simps)
  12.419 +
  12.420 +lemma exist_pt: "\<exists> t . balB h t"
  12.421 +by (induction h) (auto intro: balB.intros)
  12.422 +
  12.423 +corollary compact_pt:
  12.424 +  assumes "invc t" "invh t" "h \<le> bheight t" "balB h t'"
  12.425 +  shows   "size t' \<le> size t"
  12.426  proof -
  12.427 -  from assms have "inv2 t" and "inv1 t" unfolding rbt_def by auto 
  12.428 -  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))"
  12.429 -    by (rule rbt_del_inv1_inv2)
  12.430 -  hence "inv2 (del k t) \<and> inv1l (rbt_del k t)" by (cases "color_of t") auto
  12.431 -  with assms show ?thesis
  12.432 -    unfolding is_rbt_def rbt_delete_def
  12.433 -    by (auto intro: paint_rbt_sorted rbt_del_rbt_sorted)
  12.434 +  obtain t'' where "balB (bheight t) t''" using exist_pt by blast
  12.435 +  thus ?thesis using assms balB_bh[of t t''] balB_bh3'[of h t' "bheight t" t''] by auto
  12.436 +qed
  12.437 +
  12.438 +lemma balB_bh2: "balB (bheight t) t'\<Longrightarrow> invc t \<Longrightarrow> invh t \<Longrightarrow> height t' \<le> height t"
  12.439 +apply (induction "(bheight t)" t' arbitrary: t rule: balB.induct)
  12.440 +using balB_h rbt_b_height2 by auto
  12.441 +
  12.442 +lemma balB_rbt: "balB h t \<Longrightarrow> rbt t"
  12.443 +unfolding rbt_def
  12.444 +by (induction h t rule: balB.induct) auto
  12.445 +
  12.446 +lemma balB_size[simp]: "balB h t \<Longrightarrow> size1 t = 2^h"
  12.447 +by (induction h t rule: balB.induct) auto
  12.448 +
  12.449 +text \<open>Red-black tree (except that the root may be red) of minimal size
  12.450 +for a given height:\<close>
  12.451 +
  12.452 +inductive RB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool" where
  12.453 +"RB 0 Leaf" |
  12.454 +"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Red \<Longrightarrow> RB (Suc h) (B t' () t)" |
  12.455 +"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Black \<Longrightarrow> RB (Suc h) (R t' () t)" 
  12.456 +
  12.457 +lemmas RB.intros[intro]
  12.458 +
  12.459 +lemma RB_invc: "RB h t \<Longrightarrow> invc t"
  12.460 +apply (induction h t rule: RB.induct)
  12.461 +using balB_rbt unfolding rbt_def by auto
  12.462 +
  12.463 +lemma RB_h: "RB h t \<Longrightarrow> h = height t"
  12.464 +apply (induction h t rule: RB.induct)
  12.465 +using balB_h by auto
  12.466 +
  12.467 +lemma RB_mod: "RB h t \<Longrightarrow> (color t = Black \<longleftrightarrow> h mod 2 = 0)"
  12.468 +apply (induction h t rule: RB.induct)
  12.469 +apply auto
  12.470 +by presburger
  12.471 +
  12.472 +lemma RB_b_height: "RB h t \<Longrightarrow> height t div 2 = bheight t"
  12.473 +proof  (induction h t rule: RB.induct)
  12.474 +  case 1 
  12.475 +  thus ?case by auto 
  12.476 +next
  12.477 +  case (2 h t t')
  12.478 +  with RB_mod obtain n where "2*n + 1 = h" 
  12.479 +    by (metis color.distinct(1) mod_div_equality2 parity) 
  12.480 +  with 2 balB_h RB_h show ?case by auto
  12.481 +next
  12.482 +  case (3 h t t')
  12.483 +  with RB_mod[OF 3(2)] parity obtain n where "2*n = h" by blast
  12.484 +  with 3 balB_h RB_h show ?case by auto
  12.485  qed
  12.486 -*)
  12.487 +
  12.488 +lemma weak_RB_induct[consumes 1]: 
  12.489 +  "RB h t \<Longrightarrow> P 0 \<langle>\<rangle> \<Longrightarrow> (\<And>h t t' c . balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow>
  12.490 +    P h t' \<Longrightarrow> P (Suc h) (Node c t' () t)) \<Longrightarrow> P h t"
  12.491 +using RB.induct by metis
  12.492 +
  12.493 +lemma RB_invh: "RB h t \<Longrightarrow> invh t"
  12.494 +apply (induction h t rule: weak_RB_induct)
  12.495 +  using balB_h balB_hs RB_h balB_rbt RB_b_height
  12.496 +  unfolding rbt_def
  12.497 +by auto
  12.498 +
  12.499 +lemma RB_bheight_minimal:
  12.500 +  "\<lbrakk>RB (height t') t; invc t'; invh t'\<rbrakk> \<Longrightarrow> bheight t \<le> bheight t'"
  12.501 +using RB_b_height RB_h red_b_height2 by fastforce
  12.502 +
  12.503 +lemma RB_minimal: "RB (height t') t \<Longrightarrow> invh t \<Longrightarrow> invc t' \<Longrightarrow> invh t' \<Longrightarrow> size t \<le> size t'"
  12.504 +proof (induction "(height t')" t arbitrary: t' rule: weak_RB_induct)
  12.505 +  case 1 thus ?case by auto 
  12.506 +next
  12.507 +  case (2 h t t'')
  12.508 +  have ***: "size (Node c t'' () t) \<le> size t'"
  12.509 +    if assms:
  12.510 +      "\<And> (t' :: 'a rbt) . \<lbrakk> h = height t'; invh t''; invc t'; invh t' \<rbrakk>
  12.511 +                            \<Longrightarrow> size t'' \<le> size t'"
  12.512 +      "Suc h = height t'" "balB (h div 2) t" "RB h t''"
  12.513 +      "invc t'" "invh t'" "height l \<ge> height r"
  12.514 +      and tt[simp]:"t' = Node c l a r" and last: "invh (Node c t'' () t)"
  12.515 +  for t' :: "'a rbt" and c l a r
  12.516 +  proof -
  12.517 +    from assms have inv: "invc r" "invh r" by auto
  12.518 +    from assms have "height l = h" using max_def by auto
  12.519 +    with RB_bheight_minimal[of l t''] have
  12.520 +      "bheight t \<le> bheight r" using assms last by auto
  12.521 +    with compact_pt[OF inv] balB_h balB_hs have 
  12.522 +      "size t \<le> size r" using assms(3) by auto moreover
  12.523 +    have "size t'' \<le> size l" using assms last by auto ultimately
  12.524 +    show ?thesis by simp
  12.525 +  qed
  12.526 +  
  12.527 +  from 2 obtain c l a r where 
  12.528 +    t': "t' = Node c l a r" by (cases t') auto
  12.529 +  with 2 have inv: "invc l" "invh l" "invc r" "invh r" by auto
  12.530 +  show ?case proof (cases "height r \<le> height l")
  12.531 +    case True thus ?thesis using ***[OF 2(3,4,1,2,6,7)] t' 2(5) by auto
  12.532 +  next
  12.533 +    case False 
  12.534 +    obtain t''' where t''' : "t''' = Node c r a l" "invc t'''" "invh t'''" using 2 t' by auto
  12.535 +    have "size t''' = size t'" and 4 : "Suc h = height t'''" using 2(4) t' t''' by auto
  12.536 +    thus ?thesis using ***[OF 2(3) 4 2(1,2) t'''(2,3) _ t'''(1)] 2(5) False by auto
  12.537 +  qed
  12.538 +qed
  12.539 +
  12.540 +lemma RB_size: "RB h t \<Longrightarrow> size1 t + 1 = 2^((h+1) div 2) + 2^(h div 2)"
  12.541 +by (induction h t rule: "RB.induct" ) auto
  12.542 +
  12.543 +lemma RB_exist: "\<exists> t . RB h t"
  12.544 +proof (induction h) 
  12.545 +  case (Suc n)
  12.546 +  obtain r where r: "balB (n div 2) r"  using  exist_pt by blast
  12.547 +  obtain l where l: "RB n l"  using  Suc by blast
  12.548 +  obtain t where 
  12.549 +    "color l = Red   \<Longrightarrow> t = B l () r"
  12.550 +    "color l = Black \<Longrightarrow> t = R l () r" by auto
  12.551 +  with l and r have "RB (Suc n) t" by (cases "color l") auto
  12.552 +  thus ?case by auto
  12.553 +qed auto
  12.554 +
  12.555 +lemma bound:
  12.556 +  assumes "invc t"  "invh t" and [simp]:"height t = h"
  12.557 +  shows "size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
  12.558 +proof -
  12.559 +  obtain t' where t': "RB h t'" using RB_exist by auto
  12.560 +  show ?thesis using RB_size[OF t'] 
  12.561 +  RB_minimal[OF _ _ assms(1,2), simplified, OF t' RB_invh[OF t']] assms t' 
  12.562 +  unfolding  size1_def by auto
  12.563 +qed
  12.564 +
  12.565 +corollary "rbt t \<Longrightarrow> h = height t \<Longrightarrow> size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
  12.566 +using bound unfolding rbt_def by blast
  12.567 +
  12.568  end
    13.1 --- a/src/HOL/Data_Structures/Splay_Map.thy	Thu Jul 07 09:24:03 2016 +0200
    13.2 +++ b/src/HOL/Data_Structures/Splay_Map.thy	Thu Jul 07 18:08:02 2016 +0200
    13.3 @@ -42,7 +42,7 @@
    13.4  termination splay
    13.5  by lexicographic_order
    13.6  
    13.7 -lemma splay_code: "splay (x::_::cmp) t = (case t of Leaf \<Rightarrow> Leaf |
    13.8 +lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf |
    13.9    Node al a ar \<Rightarrow> (case cmp x (fst a) of
   13.10      EQ \<Rightarrow> t |
   13.11      LT \<Rightarrow> (case al of
    14.1 --- a/src/HOL/Data_Structures/Splay_Set.thy	Thu Jul 07 09:24:03 2016 +0200
    14.2 +++ b/src/HOL/Data_Structures/Splay_Set.thy	Thu Jul 07 18:08:02 2016 +0200
    14.3 @@ -51,7 +51,7 @@
    14.4    "\<lbrakk> x = x'; y = y'; z = z' \<rbrakk> \<Longrightarrow> case_tree x y z = case_tree x' y' z'"
    14.5  by auto
    14.6  
    14.7 -lemma splay_code: "splay (x::_::cmp) t = (case t of Leaf \<Rightarrow> Leaf |
    14.8 +lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf |
    14.9    Node al a ar \<Rightarrow> (case cmp x a of
   14.10      EQ \<Rightarrow> t |
   14.11      LT \<Rightarrow> (case al of
   14.12 @@ -83,7 +83,7 @@
   14.13  
   14.14  hide_const (open) insert
   14.15  
   14.16 -fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   14.17 +fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   14.18  "insert x t =
   14.19    (if t = Leaf then Node Leaf x Leaf
   14.20     else case splay x t of
    15.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Thu Jul 07 09:24:03 2016 +0200
    15.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Thu Jul 07 18:08:02 2016 +0200
    15.3 @@ -10,7 +10,7 @@
    15.4  
    15.5  subsection \<open>Map operations on 2-3-4 trees\<close>
    15.6  
    15.7 -fun lookup :: "('a::cmp * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
    15.8 +fun lookup :: "('a::linorder * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
    15.9  "lookup Leaf x = None" |
   15.10  "lookup (Node2 l (a,b) r) x = (case cmp x a of
   15.11    LT \<Rightarrow> lookup l x |
   15.12 @@ -30,7 +30,7 @@
   15.13    GT \<Rightarrow> (case cmp x a3 of
   15.14             LT \<Rightarrow> lookup t3 x | EQ \<Rightarrow> Some b3 | GT \<Rightarrow> lookup t4 x))"
   15.15  
   15.16 -fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
   15.17 +fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
   15.18  "upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
   15.19  "upd x y (Node2 l ab r) = (case cmp x (fst ab) of
   15.20     LT \<Rightarrow> (case upd x y l of
   15.21 @@ -72,10 +72,10 @@
   15.22                      T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
   15.23                    | Up\<^sub>i t41 q t42 => Up\<^sub>i (Node2 t1 ab1 t2) ab2 (Node3 t3 ab3 t41 q t42))))"
   15.24  
   15.25 -definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
   15.26 +definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
   15.27  "update x y t = tree\<^sub>i(upd x y t)"
   15.28  
   15.29 -fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d" where
   15.30 +fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d" where
   15.31  "del x Leaf = T\<^sub>d Leaf" |
   15.32  "del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
   15.33  "del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
   15.34 @@ -107,7 +107,7 @@
   15.35            EQ \<Rightarrow> let (ab',t4') = del_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
   15.36            GT \<Rightarrow> node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))"
   15.37  
   15.38 -definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
   15.39 +definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
   15.40  "delete x t = tree\<^sub>d(del x t)"
   15.41  
   15.42  
    16.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Thu Jul 07 09:24:03 2016 +0200
    16.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Thu Jul 07 18:08:02 2016 +0200
    16.3 @@ -11,7 +11,7 @@
    16.4  
    16.5  subsection \<open>Set operations on 2-3-4 trees\<close>
    16.6  
    16.7 -fun isin :: "'a::cmp tree234 \<Rightarrow> 'a \<Rightarrow> bool" where
    16.8 +fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where
    16.9  "isin Leaf x = False" |
   16.10  "isin (Node2 l a r) x =
   16.11    (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" |
   16.12 @@ -38,7 +38,7 @@
   16.13  "tree\<^sub>i (T\<^sub>i t) = t" |
   16.14  "tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
   16.15  
   16.16 -fun ins :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where
   16.17 +fun ins :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where
   16.18  "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
   16.19  "ins x (Node2 l a r) =
   16.20     (case cmp x a of
   16.21 @@ -91,7 +91,7 @@
   16.22  
   16.23  hide_const insert
   16.24  
   16.25 -definition insert :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
   16.26 +definition insert :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
   16.27  "insert x t = tree\<^sub>i(ins x t)"
   16.28  
   16.29  datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234"
   16.30 @@ -162,7 +162,7 @@
   16.31  "del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" |
   16.32  "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))"
   16.33  
   16.34 -fun del :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   16.35 +fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   16.36  "del k Leaf = T\<^sub>d Leaf" |
   16.37  "del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
   16.38  "del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf
   16.39 @@ -194,7 +194,7 @@
   16.40             EQ \<Rightarrow> let (c',r') = del_min r in node44 l a m b n c' r' |
   16.41             GT \<Rightarrow> node44 l a m b n c (del k r)))"
   16.42  
   16.43 -definition delete :: "'a::cmp \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
   16.44 +definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
   16.45  "delete x t = tree\<^sub>d(del x t)"
   16.46  
   16.47  
    17.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Thu Jul 07 09:24:03 2016 +0200
    17.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Thu Jul 07 18:08:02 2016 +0200
    17.3 @@ -8,7 +8,7 @@
    17.4    Map_by_Ordered
    17.5  begin
    17.6  
    17.7 -fun lookup :: "('a::cmp * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
    17.8 +fun lookup :: "('a::linorder * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
    17.9  "lookup Leaf x = None" |
   17.10  "lookup (Node2 l (a,b) r) x = (case cmp x a of
   17.11    LT \<Rightarrow> lookup l x |
   17.12 @@ -22,7 +22,7 @@
   17.13            EQ \<Rightarrow> Some b2 |
   17.14            GT \<Rightarrow> lookup r x))"
   17.15  
   17.16 -fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
   17.17 +fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
   17.18  "upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
   17.19  "upd x y (Node2 l ab r) = (case cmp x (fst ab) of
   17.20     LT \<Rightarrow> (case upd x y l of
   17.21 @@ -46,10 +46,10 @@
   17.22                     T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
   17.23                   | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))"
   17.24  
   17.25 -definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
   17.26 +definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
   17.27  "update a b t = tree\<^sub>i(upd a b t)"
   17.28  
   17.29 -fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where
   17.30 +fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where
   17.31  "del x Leaf = T\<^sub>d Leaf" |
   17.32  "del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
   17.33  "del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
   17.34 @@ -66,7 +66,7 @@
   17.35             EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
   17.36             GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))"
   17.37  
   17.38 -definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
   17.39 +definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
   17.40  "delete x t = tree\<^sub>d(del x t)"
   17.41  
   17.42  
    18.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Jul 07 09:24:03 2016 +0200
    18.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu Jul 07 18:08:02 2016 +0200
    18.3 @@ -9,7 +9,7 @@
    18.4    Set_by_Ordered
    18.5  begin
    18.6  
    18.7 -fun isin :: "'a::cmp tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
    18.8 +fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
    18.9  "isin Leaf x = False" |
   18.10  "isin (Node2 l a r) x =
   18.11    (case cmp x a of
   18.12 @@ -32,7 +32,7 @@
   18.13  "tree\<^sub>i (T\<^sub>i t) = t" |
   18.14  "tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
   18.15  
   18.16 -fun ins :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
   18.17 +fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
   18.18  "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
   18.19  "ins x (Node2 l a r) =
   18.20     (case cmp x a of
   18.21 @@ -66,7 +66,7 @@
   18.22  
   18.23  hide_const insert
   18.24  
   18.25 -definition insert :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   18.26 +definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   18.27  "insert x t = tree\<^sub>i(ins x t)"
   18.28  
   18.29  datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
   18.30 @@ -108,7 +108,7 @@
   18.31  "del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
   18.32  "del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
   18.33  
   18.34 -fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
   18.35 +fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
   18.36  "del x Leaf = T\<^sub>d Leaf" |
   18.37  "del x (Node2 Leaf a Leaf) =
   18.38    (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
   18.39 @@ -131,7 +131,7 @@
   18.40            EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
   18.41            GT \<Rightarrow> node33 l a m b (del x r)))"
   18.42  
   18.43 -definition delete :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   18.44 +definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   18.45  "delete x t = tree\<^sub>d(del x t)"
   18.46  
   18.47  
    19.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Thu Jul 07 09:24:03 2016 +0200
    19.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Thu Jul 07 18:08:02 2016 +0200
    19.3 @@ -1,6 +1,6 @@
    19.4  (* Author: Tobias Nipkow *)
    19.5  
    19.6 -section {* Unbalanced Tree as Map *}
    19.7 +section \<open>Unbalanced Tree Implementation of Map\<close>
    19.8  
    19.9  theory Tree_Map
   19.10  imports
   19.11 @@ -8,19 +8,19 @@
   19.12    Map_by_Ordered
   19.13  begin
   19.14  
   19.15 -fun lookup :: "('a::cmp*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
   19.16 +fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
   19.17  "lookup Leaf x = None" |
   19.18  "lookup (Node l (a,b) r) x =
   19.19    (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
   19.20  
   19.21 -fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
   19.22 +fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
   19.23  "update x y Leaf = Node Leaf (x,y) Leaf" |
   19.24  "update x y (Node l (a,b) r) = (case cmp x a of
   19.25     LT \<Rightarrow> Node (update x y l) (a,b) r |
   19.26     EQ \<Rightarrow> Node l (x,y) r |
   19.27     GT \<Rightarrow> Node l (a,b) (update x y r))"
   19.28  
   19.29 -fun delete :: "'a::cmp \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
   19.30 +fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
   19.31  "delete x Leaf = Leaf" |
   19.32  "delete x (Node l (a,b) r) = (case cmp x a of
   19.33    LT \<Rightarrow> Node (delete x l) (a,b) r |
    20.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Thu Jul 07 09:24:03 2016 +0200
    20.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Thu Jul 07 18:08:02 2016 +0200
    20.3 @@ -1,6 +1,6 @@
    20.4  (* Author: Tobias Nipkow *)
    20.5  
    20.6 -section {* Tree Implementation of Sets *}
    20.7 +section \<open>Unbalanced Tree Implementation of Set\<close>
    20.8  
    20.9  theory Tree_Set
   20.10  imports
   20.11 @@ -9,7 +9,7 @@
   20.12    Set_by_Ordered
   20.13  begin
   20.14  
   20.15 -fun isin :: "'a::cmp tree \<Rightarrow> 'a \<Rightarrow> bool" where
   20.16 +fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where
   20.17  "isin Leaf x = False" |
   20.18  "isin (Node l a r) x =
   20.19    (case cmp x a of
   20.20 @@ -19,7 +19,7 @@
   20.21  
   20.22  hide_const (open) insert
   20.23  
   20.24 -fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   20.25 +fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   20.26  "insert x Leaf = Node Leaf x Leaf" |
   20.27  "insert x (Node l a r) =
   20.28    (case cmp x a of
   20.29 @@ -31,7 +31,7 @@
   20.30  "del_min (Node l a r) =
   20.31    (if l = Leaf then (a,r) else let (x,l') = del_min l in (x, Node l' a r))"
   20.32  
   20.33 -fun delete :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   20.34 +fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   20.35  "delete x Leaf = Leaf" |
   20.36  "delete x (Node l a r) =
   20.37    (case cmp x a of