hide implementation details
authorkuncar
Mon Mar 10 17:14:57 2014 +0100 (2014-03-10)
changeset 56019682bba24e474
parent 56018 c3fc8692dbc1
child 56020 f92479477c52
hide implementation details
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Mapping.thy
src/HOL/Library/RBT_Set.thy
     1.1 --- a/src/HOL/Library/RBT.thy	Mon Mar 10 15:24:49 2014 +0100
     1.2 +++ b/src/HOL/Library/RBT.thy	Mon Mar 10 17:14:57 2014 +0100
     1.3 @@ -36,7 +36,6 @@
     1.4  subsection {* Primitive operations *}
     1.5  
     1.6  setup_lifting type_definition_rbt
     1.7 -print_theorems
     1.8  
     1.9  lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" .
    1.10  
    1.11 @@ -187,4 +186,14 @@
    1.12  
    1.13  quickcheck_generator rbt predicate: is_rbt constructors: empty, insert
    1.14  
    1.15 +subsection {* Hide implementation details *}
    1.16 +
    1.17 +lifting_update rbt.lifting
    1.18 +lifting_forget rbt.lifting
    1.19 +
    1.20 +hide_const (open) impl_of empty lookup keys entries bulkload delete map fold union insert map_entry foldi 
    1.21 +  is_empty
    1.22 +hide_fact (open) empty_def lookup_def keys_def entries_def bulkload_def delete_def map_def fold_def 
    1.23 +  union_def insert_def map_entry_def foldi_def is_empty_def
    1.24 +
    1.25  end
     2.1 --- a/src/HOL/Library/RBT_Mapping.thy	Mon Mar 10 15:24:49 2014 +0100
     2.2 +++ b/src/HOL/Library/RBT_Mapping.thy	Mon Mar 10 17:14:57 2014 +0100
     2.3 @@ -11,42 +11,46 @@
     2.4  
     2.5  subsection {* Implementation of mappings *}
     2.6  
     2.7 -lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is lookup .
     2.8 +context includes rbt.lifting begin
     2.9 +lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is RBT.lookup .
    2.10 +end
    2.11  
    2.12  code_datatype Mapping
    2.13  
    2.14 +context includes rbt.lifting begin
    2.15 +
    2.16  lemma lookup_Mapping [simp, code]:
    2.17 -  "Mapping.lookup (Mapping t) = lookup t"
    2.18 +  "Mapping.lookup (Mapping t) = RBT.lookup t"
    2.19     by (transfer fixing: t) rule
    2.20  
    2.21 -lemma empty_Mapping [code]: "Mapping.empty = Mapping empty"
    2.22 +lemma empty_Mapping [code]: "Mapping.empty = Mapping RBT.empty"
    2.23  proof -
    2.24    note RBT.empty.transfer[transfer_rule del]
    2.25    show ?thesis by transfer simp
    2.26  qed
    2.27  
    2.28  lemma is_empty_Mapping [code]:
    2.29 -  "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
    2.30 +  "Mapping.is_empty (Mapping t) \<longleftrightarrow> RBT.is_empty t"
    2.31    unfolding is_empty_def by (transfer fixing: t) simp
    2.32  
    2.33  lemma insert_Mapping [code]:
    2.34 -  "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
    2.35 +  "Mapping.update k v (Mapping t) = Mapping (RBT.insert k v t)"
    2.36    by (transfer fixing: t) simp
    2.37  
    2.38  lemma delete_Mapping [code]:
    2.39 -  "Mapping.delete k (Mapping t) = Mapping (delete k t)"
    2.40 +  "Mapping.delete k (Mapping t) = Mapping (RBT.delete k t)"
    2.41    by (transfer fixing: t) simp
    2.42  
    2.43  lemma map_entry_Mapping [code]:
    2.44 -  "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
    2.45 -  apply (transfer fixing: t) by (case_tac "lookup t k") auto
    2.46 +  "Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)"
    2.47 +  apply (transfer fixing: t) by (case_tac "RBT.lookup t k") auto
    2.48  
    2.49  lemma keys_Mapping [code]:
    2.50 -  "Mapping.keys (Mapping t) = set (keys t)"
    2.51 +  "Mapping.keys (Mapping t) = set (RBT.keys t)"
    2.52  by (transfer fixing: t) (simp add: lookup_keys)
    2.53  
    2.54  lemma ordered_keys_Mapping [code]:
    2.55 -  "Mapping.ordered_keys (Mapping t) = keys t"
    2.56 +  "Mapping.ordered_keys (Mapping t) = RBT.keys t"
    2.57  unfolding ordered_keys_def 
    2.58  by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique)
    2.59  
    2.60 @@ -55,7 +59,7 @@
    2.61  unfolding size_def by transfer simp
    2.62  
    2.63  lemma size_Mapping [code]:
    2.64 -  "Mapping.size (Mapping t) = length (keys t)"
    2.65 +  "Mapping.size (Mapping t) = length (RBT.keys t)"
    2.66  unfolding size_def
    2.67  by (transfer fixing: t) (simp add: lookup_keys distinct_card)
    2.68  
    2.69 @@ -63,25 +67,24 @@
    2.70    notes RBT.bulkload.transfer[transfer_rule del]
    2.71  begin
    2.72    lemma tabulate_Mapping [code]:
    2.73 -    "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
    2.74 +    "Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\<lambda>k. (k, f k)) ks))"
    2.75    by transfer (simp add: map_of_map_restrict)
    2.76    
    2.77    lemma bulkload_Mapping [code]:
    2.78 -    "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
    2.79 +    "Mapping.bulkload vs = Mapping (RBT.bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
    2.80    by transfer (simp add: map_of_map_restrict fun_eq_iff)
    2.81  end
    2.82  
    2.83  lemma equal_Mapping [code]:
    2.84 -  "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
    2.85 +  "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> RBT.entries t1 = RBT.entries t2"
    2.86    by (transfer fixing: t1 t2) (simp add: entries_lookup)
    2.87  
    2.88  lemma [code nbe]:
    2.89    "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
    2.90    by (fact equal_refl)
    2.91  
    2.92 +end
    2.93  
    2.94 -hide_const (open) impl_of lookup empty insert delete
    2.95 -  entries keys bulkload map_entry map fold
    2.96  (*>*)
    2.97  
    2.98  text {* 
     3.1 --- a/src/HOL/Library/RBT_Set.thy	Mon Mar 10 15:24:49 2014 +0100
     3.2 +++ b/src/HOL/Library/RBT_Set.thy	Mon Mar 10 17:14:57 2014 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4  section {* Definition of code datatype constructors *}
     3.5  
     3.6  definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
     3.7 -  where "Set t = {x . lookup t x = Some ()}"
     3.8 +  where "Set t = {x . RBT.lookup t x = Some ()}"
     3.9  
    3.10  definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
    3.11    where [simp]: "Coset t = - Set t"
    3.12 @@ -146,31 +146,31 @@
    3.13  lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
    3.14  by (auto simp: not_Some_eq[THEN iffD1])
    3.15  
    3.16 -lemma Set_set_keys: "Set x = dom (lookup x)" 
    3.17 +lemma Set_set_keys: "Set x = dom (RBT.lookup x)" 
    3.18  by (auto simp: Set_def)
    3.19  
    3.20  lemma finite_Set [simp, intro!]: "finite (Set x)"
    3.21  by (simp add: Set_set_keys)
    3.22  
    3.23 -lemma set_keys: "Set t = set(keys t)"
    3.24 +lemma set_keys: "Set t = set(RBT.keys t)"
    3.25  by (simp add: Set_set_keys lookup_keys)
    3.26  
    3.27  subsection {* fold and filter *}
    3.28  
    3.29  lemma finite_fold_rbt_fold_eq:
    3.30    assumes "comp_fun_commute f" 
    3.31 -  shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
    3.32 +  shows "Finite_Set.fold f A (set (RBT.entries t)) = RBT.fold (curry f) t A"
    3.33  proof -
    3.34 -  have *: "remdups (entries t) = entries t"
    3.35 +  have *: "remdups (RBT.entries t) = RBT.entries t"
    3.36      using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
    3.37    show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
    3.38  qed
    3.39  
    3.40  definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b" 
    3.41 -  where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"
    3.42 +  where [code_unfold]:"fold_keys f t A = RBT.fold (\<lambda>k _ t. f k t) t A"
    3.43  
    3.44  lemma fold_keys_def_alt:
    3.45 -  "fold_keys f t s = List.fold f (keys t) s"
    3.46 +  "fold_keys f t s = List.fold f (RBT.keys t) s"
    3.47  by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)
    3.48  
    3.49  lemma finite_fold_fold_keys:
    3.50 @@ -179,15 +179,15 @@
    3.51  using assms
    3.52  proof -
    3.53    interpret comp_fun_commute f by fact
    3.54 -  have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries)
    3.55 -  moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto
    3.56 +  have "set (RBT.keys t) = fst ` (set (RBT.entries t))" by (auto simp: fst_eq_Domain keys_entries)
    3.57 +  moreover have "inj_on fst (set (RBT.entries t))" using distinct_entries distinct_map by auto
    3.58    ultimately show ?thesis 
    3.59      by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq 
    3.60        comp_comp_fun_commute)
    3.61  qed
    3.62  
    3.63  definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
    3.64 -  "rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
    3.65 +  "rbt_filter P t = RBT.fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
    3.66  
    3.67  lemma Set_filter_rbt_filter:
    3.68    "Set.filter P (Set t) = rbt_filter P t"
    3.69 @@ -207,8 +207,8 @@
    3.70      by (cases "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t1 True") (simp_all add: Ball_False) 
    3.71  qed simp
    3.72  
    3.73 -lemma foldi_fold_conj: "foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
    3.74 -unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj)
    3.75 +lemma foldi_fold_conj: "RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
    3.76 +unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_conj)
    3.77  
    3.78  
    3.79  subsection {* foldi and Bex *}
    3.80 @@ -223,8 +223,8 @@
    3.81      by (cases "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t1 False") (simp_all add: Bex_True) 
    3.82  qed simp
    3.83  
    3.84 -lemma foldi_fold_disj: "foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
    3.85 -unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj)
    3.86 +lemma foldi_fold_disj: "RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
    3.87 +unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_disj)
    3.88  
    3.89  
    3.90  subsection {* folding over non empty trees and selecting the minimal and maximal element *}
    3.91 @@ -422,16 +422,17 @@
    3.92  
    3.93  (** abstract **)
    3.94  
    3.95 +context includes rbt.lifting begin
    3.96  lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
    3.97    is rbt_fold1_keys .
    3.98  
    3.99  lemma fold1_keys_def_alt:
   3.100 -  "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
   3.101 +  "fold1_keys f t = List.fold f (tl (RBT.keys t)) (hd (RBT.keys t))"
   3.102    by transfer (simp add: rbt_fold1_keys_def)
   3.103  
   3.104  lemma finite_fold1_fold1_keys:
   3.105    assumes "semilattice f"
   3.106 -  assumes "\<not> is_empty t"
   3.107 +  assumes "\<not> RBT.is_empty t"
   3.108    shows "semilattice_set.F f (Set t) = fold1_keys f t"
   3.109  proof -
   3.110    from `semilattice f` interpret semilattice_set f by (rule semilattice_set.intro)
   3.111 @@ -449,13 +450,13 @@
   3.112  by transfer (simp add: rbt_min_def)
   3.113  
   3.114  lemma r_min_eq_r_min_opt:
   3.115 -  assumes "\<not> (is_empty t)"
   3.116 +  assumes "\<not> (RBT.is_empty t)"
   3.117    shows "r_min t = r_min_opt t"
   3.118  using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
   3.119  
   3.120  lemma fold_keys_min_top_eq:
   3.121    fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
   3.122 -  assumes "\<not> (is_empty t)"
   3.123 +  assumes "\<not> (RBT.is_empty t)"
   3.124    shows "fold_keys min t top = fold1_keys min t"
   3.125  proof -
   3.126    have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
   3.127 @@ -487,13 +488,13 @@
   3.128  by transfer (simp add: rbt_max_def)
   3.129  
   3.130  lemma r_max_eq_r_max_opt:
   3.131 -  assumes "\<not> (is_empty t)"
   3.132 +  assumes "\<not> (RBT.is_empty t)"
   3.133    shows "r_max t = r_max_opt t"
   3.134  using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
   3.135  
   3.136  lemma fold_keys_max_bot_eq:
   3.137    fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
   3.138 -  assumes "\<not> (is_empty t)"
   3.139 +  assumes "\<not> (RBT.is_empty t)"
   3.140    shows "fold_keys max t bot = fold1_keys max t"
   3.141  proof -
   3.142    have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
   3.143 @@ -515,6 +516,7 @@
   3.144    done
   3.145  qed
   3.146  
   3.147 +end
   3.148  
   3.149  section {* Code equations *}
   3.150  
   3.151 @@ -584,7 +586,7 @@
   3.152  qed
   3.153   
   3.154  lemma union_Set_Set [code]:
   3.155 -  "Set t1 \<union> Set t2 = Set (union t1 t2)"
   3.156 +  "Set t1 \<union> Set t2 = Set (RBT.union t1 t2)"
   3.157  by (auto simp add: lookup_union map_add_Some_iff Set_def)
   3.158  
   3.159  lemma inter_Coset [code]:
   3.160 @@ -592,7 +594,7 @@
   3.161  by (simp add: Diff_eq [symmetric] minus_Set)
   3.162  
   3.163  lemma inter_Coset_Coset [code]:
   3.164 -  "Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
   3.165 +  "Coset t1 \<inter> Coset t2 = Coset (RBT.union t1 t2)"
   3.166  by (auto simp add: lookup_union map_add_Some_iff Set_def)
   3.167  
   3.168  lemma minus_Coset [code]:
   3.169 @@ -611,7 +613,7 @@
   3.170  qed
   3.171  
   3.172  lemma Ball_Set [code]:
   3.173 -  "Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   3.174 +  "Ball (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   3.175  proof -
   3.176    have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
   3.177    then show ?thesis 
   3.178 @@ -619,7 +621,7 @@
   3.179  qed
   3.180  
   3.181  lemma Bex_Set [code]:
   3.182 -  "Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   3.183 +  "Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   3.184  proof -
   3.185    have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
   3.186    then show ?thesis 
   3.187 @@ -632,11 +634,11 @@
   3.188  by auto
   3.189  
   3.190  lemma subset_Coset_empty_Set_empty [code]:
   3.191 -  "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of 
   3.192 +  "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (RBT.impl_of t1, RBT.impl_of t2) of 
   3.193      (rbt.Empty, rbt.Empty) => False |
   3.194      (_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))"
   3.195  proof -
   3.196 -  have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
   3.197 +  have *: "\<And>t. RBT.impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
   3.198      by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
   3.199    have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
   3.200    show ?thesis  
   3.201 @@ -645,7 +647,7 @@
   3.202  
   3.203  text {* A frequent case – avoid intermediate sets *}
   3.204  lemma [code_unfold]:
   3.205 -  "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   3.206 +  "Set t1 \<subseteq> Set t2 \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   3.207  by (simp add: subset_code Ball_Set)
   3.208  
   3.209  lemma card_Set [code]:
   3.210 @@ -662,7 +664,7 @@
   3.211  
   3.212  lemma the_elem_set [code]:
   3.213    fixes t :: "('a :: linorder, unit) rbt"
   3.214 -  shows "the_elem (Set t) = (case impl_of t of 
   3.215 +  shows "the_elem (Set t) = (case RBT.impl_of t of 
   3.216      (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
   3.217      | _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))"
   3.218  proof -
   3.219 @@ -672,7 +674,7 @@
   3.220      have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
   3.221      then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
   3.222  
   3.223 -    have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
   3.224 +    have "RBT.impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
   3.225        by (subst(asm) RBT_inverse[symmetric, OF *])
   3.226          (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
   3.227    }
   3.228 @@ -726,7 +728,7 @@
   3.229  
   3.230  lemma Min_fin_set_fold [code]:
   3.231    "Min (Set t) = 
   3.232 -  (if is_empty t
   3.233 +  (if RBT.is_empty t
   3.234     then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t))
   3.235     else r_min_opt t)"
   3.236  proof -
   3.237 @@ -742,10 +744,10 @@
   3.238  
   3.239  lemma Inf_Set_fold:
   3.240    fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   3.241 -  shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
   3.242 +  shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
   3.243  proof -
   3.244    have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   3.245 -  then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   3.246 +  then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   3.247      by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
   3.248    then show ?thesis 
   3.249      by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
   3.250 @@ -767,7 +769,7 @@
   3.251  
   3.252  lemma Max_fin_set_fold [code]:
   3.253    "Max (Set t) = 
   3.254 -  (if is_empty t
   3.255 +  (if RBT.is_empty t
   3.256     then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t))
   3.257     else r_max_opt t)"
   3.258  proof -
   3.259 @@ -783,10 +785,10 @@
   3.260  
   3.261  lemma Sup_Set_fold:
   3.262    fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   3.263 -  shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
   3.264 +  shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
   3.265  proof -
   3.266    have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   3.267 -  then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   3.268 +  then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   3.269      by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
   3.270    then show ?thesis 
   3.271      by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
   3.272 @@ -807,14 +809,14 @@
   3.273  qed
   3.274  
   3.275  lemma sorted_list_set[code]:
   3.276 -  "sorted_list_of_set (Set t) = keys t"
   3.277 +  "sorted_list_of_set (Set t) = RBT.keys t"
   3.278  by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
   3.279  
   3.280  lemma Bleast_code [code]:
   3.281 - "Bleast (Set t) P = (case filter P (keys t) of
   3.282 + "Bleast (Set t) P = (case filter P (RBT.keys t) of
   3.283      x#xs \<Rightarrow> x |
   3.284      [] \<Rightarrow> abort_Bleast (Set t) P)"
   3.285 -proof (cases "filter P (keys t)")
   3.286 +proof (cases "filter P (RBT.keys t)")
   3.287    case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
   3.288  next
   3.289    case (Cons x ys)
   3.290 @@ -831,7 +833,6 @@
   3.291    thus ?thesis using Cons by (simp add: Bleast_def)
   3.292  qed
   3.293  
   3.294 -
   3.295  hide_const (open) RBT_Set.Set RBT_Set.Coset
   3.296  
   3.297  end