implementation of sets by RBT trees for the code generator
authorkuncar
Tue Jul 31 13:55:39 2012 +0200 (2012-07-31)
changeset 48623bea613f2543d
parent 48622 caaa1a02c650
child 48624 9b71daba4ec7
implementation of sets by RBT trees for the code generator
src/HOL/Library/Library.thy
src/HOL/Library/RBT_Set.thy
     1.1 --- a/src/HOL/Library/Library.thy	Tue Jul 31 13:55:39 2012 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Tue Jul 31 13:55:39 2012 +0200
     1.3 @@ -55,6 +55,7 @@
     1.4    Ramsey
     1.5    Reflection
     1.6    RBT_Mapping
     1.7 +  (* RBT_Set *) (* not included because it breaks Codegenerator_Test/Generate*.thy *)
     1.8    Saturated
     1.9    Set_Algebras
    1.10    State_Monad
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Jul 31 13:55:39 2012 +0200
     2.3 @@ -0,0 +1,824 @@
     2.4 +(*  Title:      HOL/Library/RBT_Set.thy
     2.5 +    Author:     Ondrej Kuncar
     2.6 +*)
     2.7 +
     2.8 +header {* Implementation of sets using RBT trees *}
     2.9 +
    2.10 +theory RBT_Set
    2.11 +imports RBT Product_ord
    2.12 +begin
    2.13 +
    2.14 +(*
    2.15 +  Users should be aware that by including this file all code equations
    2.16 +  outside of List.thy using 'a list as an implenentation of sets cannot be
    2.17 +  used for code generation. If such equations are not needed, they can be
    2.18 +  deleted from the code generator. Otherwise, a user has to provide their 
    2.19 +  own equations using RBT trees. 
    2.20 +*)
    2.21 +
    2.22 +section {* Definition of code datatype constructors *}
    2.23 +
    2.24 +definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
    2.25 +  where "Set t = {x . lookup t x = Some ()}"
    2.26 +
    2.27 +definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
    2.28 +  where [simp]: "Coset t = - Set t"
    2.29 +
    2.30 +
    2.31 +section {* Deletion of already existing code equations *}
    2.32 +
    2.33 +lemma [code, code del]:
    2.34 +  "Set.empty = Set.empty" ..
    2.35 +
    2.36 +lemma [code, code del]:
    2.37 +  "Set.is_empty = Set.is_empty" ..
    2.38 +
    2.39 +lemma [code, code del]:
    2.40 +  "uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" ..
    2.41 +
    2.42 +lemma [code, code del]:
    2.43 +  "Set.member = Set.member" ..
    2.44 +
    2.45 +lemma [code, code del]:
    2.46 +  "Set.insert = Set.insert" ..
    2.47 +
    2.48 +lemma [code, code del]:
    2.49 +  "Set.remove = Set.remove" ..
    2.50 +
    2.51 +lemma [code, code del]:
    2.52 +  "UNIV = UNIV" ..
    2.53 +
    2.54 +lemma [code, code del]:
    2.55 +  "Set.project = Set.project" ..
    2.56 +
    2.57 +lemma [code, code del]:
    2.58 +  "image = image" ..
    2.59 +
    2.60 +lemma [code, code del]:
    2.61 +  "Set.subset_eq = Set.subset_eq" ..
    2.62 +
    2.63 +lemma [code, code del]:
    2.64 +  "Ball = Ball" ..
    2.65 +
    2.66 +lemma [code, code del]:
    2.67 +  "Bex = Bex" ..
    2.68 +
    2.69 +lemma [code, code del]:
    2.70 +  "Set.union = Set.union" ..
    2.71 +
    2.72 +lemma [code, code del]:
    2.73 +  "minus_set_inst.minus_set = minus_set_inst.minus_set" ..
    2.74 +
    2.75 +lemma [code, code del]:
    2.76 +  "Set.inter = Set.inter" ..
    2.77 +
    2.78 +lemma [code, code del]:
    2.79 +  "card = card" ..
    2.80 +
    2.81 +lemma [code, code del]:
    2.82 +  "the_elem = the_elem" ..
    2.83 +
    2.84 +lemma [code, code del]:
    2.85 +  "Pow = Pow" ..
    2.86 +
    2.87 +lemma [code, code del]:
    2.88 +  "setsum = setsum" ..
    2.89 +
    2.90 +lemma [code, code del]:
    2.91 +  "Product_Type.product = Product_Type.product"  ..
    2.92 +
    2.93 +lemma [code, code del]:
    2.94 +  "Id_on = Id_on" ..
    2.95 +
    2.96 +lemma [code, code del]:
    2.97 +  "Image = Image" ..
    2.98 +
    2.99 +lemma [code, code del]:
   2.100 +  "trancl = trancl" ..
   2.101 +
   2.102 +lemma [code, code del]:
   2.103 +  "relcomp = relcomp" ..
   2.104 +
   2.105 +lemma [code, code del]:
   2.106 +  "wf = wf" ..
   2.107 +
   2.108 +lemma [code, code del]:
   2.109 +  "Min = Min" ..
   2.110 +
   2.111 +lemma [code, code del]:
   2.112 +  "Inf_fin = Inf_fin" ..
   2.113 +
   2.114 +lemma [code, code del]:
   2.115 +  "INFI = INFI" ..
   2.116 +
   2.117 +lemma [code, code del]:
   2.118 +  "Max = Max" ..
   2.119 +
   2.120 +lemma [code, code del]:
   2.121 +  "Sup_fin = Sup_fin" ..
   2.122 +
   2.123 +lemma [code, code del]:
   2.124 +  "SUPR = SUPR" ..
   2.125 +
   2.126 +lemma [code, code del]:
   2.127 +  "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
   2.128 +
   2.129 +lemma [code, code del]:
   2.130 +  "(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" ..
   2.131 +
   2.132 +lemma [code, code del]:
   2.133 +  "sorted_list_of_set = sorted_list_of_set" ..
   2.134 +
   2.135 +lemma [code, code del]: 
   2.136 +  "List.map_project = List.map_project" ..
   2.137 +
   2.138 +section {* Lemmas *}
   2.139 +
   2.140 +
   2.141 +subsection {* Auxiliary lemmas *}
   2.142 +
   2.143 +lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
   2.144 +by (auto simp: not_Some_eq[THEN iffD1])
   2.145 +
   2.146 +lemma finite_Set [simp, intro!]: "finite (Set x)"
   2.147 +proof -
   2.148 +  have "Set x = dom (lookup x)" by (auto simp: Set_def)
   2.149 +  then show ?thesis by simp
   2.150 +qed
   2.151 +
   2.152 +lemma set_keys: "Set t = set(keys t)"
   2.153 +proof -
   2.154 + have "\<And>k. ((k, ()) \<in> set (entries t)) = (k \<in> set (keys t))" 
   2.155 +    by (simp add: keys_entries)
   2.156 +  then show ?thesis by (auto simp: lookup_in_tree Set_def)
   2.157 +qed
   2.158 +
   2.159 +subsection {* fold and filter *}
   2.160 +
   2.161 +lemma finite_fold_rbt_fold_eq:
   2.162 +  assumes "comp_fun_commute f" 
   2.163 +  shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
   2.164 +proof -
   2.165 +  have *: "remdups (entries t) = entries t"
   2.166 +    using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
   2.167 +  show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
   2.168 +qed
   2.169 +
   2.170 +definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b" 
   2.171 +  where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"
   2.172 +
   2.173 +lemma fold_keys_def_alt:
   2.174 +  "fold_keys f t s = List.fold f (keys t) s"
   2.175 +by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)
   2.176 +
   2.177 +lemma finite_fold_fold_keys:
   2.178 +  assumes "comp_fun_commute f"
   2.179 +  shows "Finite_Set.fold f A (Set t) = fold_keys f t A"
   2.180 +using assms
   2.181 +proof -
   2.182 +  interpret comp_fun_commute f by fact
   2.183 +  have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries)
   2.184 +  moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto
   2.185 +  ultimately show ?thesis 
   2.186 +    by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq 
   2.187 +      comp_comp_fun_commute)
   2.188 +qed
   2.189 +
   2.190 +definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
   2.191 +  "rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
   2.192 +
   2.193 +lemma finite_filter_rbt_filter:
   2.194 +  "Finite_Set.filter P (Set t) = rbt_filter P t"
   2.195 +by (simp add: fold_keys_def Finite_Set.filter_def rbt_filter_def 
   2.196 +  finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
   2.197 +
   2.198 +
   2.199 +subsection {* foldi and Ball *}
   2.200 +
   2.201 +lemma Ball_False: "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t False = False"
   2.202 +by (induction t) auto
   2.203 +
   2.204 +lemma rbt_foldi_fold_conj: 
   2.205 +  "RBT_Impl.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t val"
   2.206 +proof (induction t arbitrary: val) 
   2.207 +  case (Branch c t1) then show ?case
   2.208 +    by (cases "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t1 True") (simp_all add: Ball_False) 
   2.209 +qed simp
   2.210 +
   2.211 +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"
   2.212 +unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj)
   2.213 +
   2.214 +
   2.215 +subsection {* foldi and Bex *}
   2.216 +
   2.217 +lemma Bex_True: "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True"
   2.218 +by (induction t) auto
   2.219 +
   2.220 +lemma rbt_foldi_fold_disj: 
   2.221 +  "RBT_Impl.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t val"
   2.222 +proof (induction t arbitrary: val) 
   2.223 +  case (Branch c t1) then show ?case
   2.224 +    by (cases "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t1 False") (simp_all add: Bex_True) 
   2.225 +qed simp
   2.226 +
   2.227 +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"
   2.228 +unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj)
   2.229 +
   2.230 +
   2.231 +subsection {* folding over non empty trees and selecting the minimal and maximal element *}
   2.232 +
   2.233 +(** concrete **)
   2.234 +
   2.235 +(* The concrete part is here because it's probably not general enough to be moved to RBT_Impl *)
   2.236 +
   2.237 +definition rbt_fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a" 
   2.238 +  where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))"
   2.239 +
   2.240 +(* minimum *)
   2.241 +
   2.242 +definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   2.243 +  where "rbt_min t = rbt_fold1_keys min t"
   2.244 +
   2.245 +lemma key_le_right: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys rt) \<Longrightarrow> k \<le> x)"
   2.246 +by  (auto simp: rbt_greater_prop less_imp_le)
   2.247 +
   2.248 +lemma left_le_key: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys lt) \<Longrightarrow> x \<le> k)"
   2.249 +by (auto simp: rbt_less_prop less_imp_le)
   2.250 +
   2.251 +lemma fold_min_triv:
   2.252 +  fixes k :: "_ :: linorder"
   2.253 +  shows "(\<forall>x\<in>set xs. k \<le> x) \<Longrightarrow> List.fold min xs k = k" 
   2.254 +by (induct xs) (auto simp add: min_def)
   2.255 +
   2.256 +lemma rbt_min_simps:
   2.257 +  "is_rbt (Branch c RBT_Impl.Empty k v rt) \<Longrightarrow> rbt_min (Branch c RBT_Impl.Empty k v rt) = k"
   2.258 +by (auto intro: fold_min_triv dest: key_le_right is_rbt_rbt_sorted simp: rbt_fold1_keys_def rbt_min_def)
   2.259 +
   2.260 +fun rbt_min_opt where
   2.261 +  "rbt_min_opt (Branch c RBT_Impl.Empty k v rt) = k" |
   2.262 +  "rbt_min_opt (Branch c (Branch lc llc lk lv lrt) k v rt) = rbt_min_opt (Branch lc llc lk lv lrt)"
   2.263 +
   2.264 +lemma rbt_min_opt_Branch:
   2.265 +  "t1 \<noteq> rbt.Empty \<Longrightarrow> rbt_min_opt (Branch c t1 k () t2) = rbt_min_opt t1" 
   2.266 +by (cases t1) auto
   2.267 +
   2.268 +lemma rbt_min_opt_induct [case_names empty left_empty left_non_empty]:
   2.269 +  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   2.270 +  assumes "P rbt.Empty"
   2.271 +  assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   2.272 +  assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   2.273 +  shows "P t"
   2.274 +using assms
   2.275 +  apply (induction t)
   2.276 +  apply simp
   2.277 +  apply (case_tac "t1 = rbt.Empty")
   2.278 +  apply simp_all
   2.279 +done
   2.280 +
   2.281 +lemma rbt_min_opt_in_set: 
   2.282 +  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   2.283 +  assumes "t \<noteq> rbt.Empty"
   2.284 +  shows "rbt_min_opt t \<in> set (RBT_Impl.keys t)"
   2.285 +using assms by (induction t rule: rbt_min_opt.induct) (auto)
   2.286 +
   2.287 +lemma rbt_min_opt_is_min:
   2.288 +  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   2.289 +  assumes "rbt_sorted t"
   2.290 +  assumes "t \<noteq> rbt.Empty"
   2.291 +  shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<ge> rbt_min_opt t"
   2.292 +using assms 
   2.293 +proof (induction t rule: rbt_min_opt_induct)
   2.294 +  case empty
   2.295 +    then show ?case by simp
   2.296 +next
   2.297 +  case left_empty
   2.298 +    then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
   2.299 +next
   2.300 +  case (left_non_empty c t1 k v t2 y)
   2.301 +    then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
   2.302 +    with left_non_empty show ?case 
   2.303 +    proof(elim disjE)
   2.304 +      case goal1 then show ?case 
   2.305 +        by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
   2.306 +    next
   2.307 +      case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
   2.308 +    next 
   2.309 +      case goal3 show ?case
   2.310 +      proof -
   2.311 +        from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
   2.312 +        moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
   2.313 +        ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
   2.314 +      qed
   2.315 +    qed
   2.316 +qed
   2.317 +
   2.318 +lemma rbt_min_eq_rbt_min_opt:
   2.319 +  assumes "t \<noteq> RBT_Impl.Empty"
   2.320 +  assumes "is_rbt t"
   2.321 +  shows "rbt_min t = rbt_min_opt t"
   2.322 +proof -
   2.323 +  interpret ab_semigroup_idem_mult "(min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_min
   2.324 +    unfolding class.ab_semigroup_idem_mult_def by blast
   2.325 +  show ?thesis
   2.326 +    by (simp add: Min_eqI rbt_min_opt_is_min rbt_min_opt_in_set assms Min_def[symmetric]
   2.327 +      non_empty_rbt_keys fold1_set_fold[symmetric] rbt_min_def rbt_fold1_keys_def)
   2.328 +qed
   2.329 +
   2.330 +(* maximum *)
   2.331 +
   2.332 +definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   2.333 +  where "rbt_max t = rbt_fold1_keys max t"
   2.334 +
   2.335 +lemma fold_max_triv:
   2.336 +  fixes k :: "_ :: linorder"
   2.337 +  shows "(\<forall>x\<in>set xs. x \<le> k) \<Longrightarrow> List.fold max xs k = k" 
   2.338 +by (induct xs) (auto simp add: max_def)
   2.339 +
   2.340 +lemma fold_max_rev_eq:
   2.341 +  fixes xs :: "('a :: linorder) list"
   2.342 +  assumes "xs \<noteq> []"
   2.343 +  shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
   2.344 +proof -
   2.345 +  interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
   2.346 +    unfolding class.ab_semigroup_idem_mult_def by blast
   2.347 +  show ?thesis
   2.348 +  using assms by (auto simp add: fold1_set_fold[symmetric])
   2.349 +qed
   2.350 +
   2.351 +lemma rbt_max_simps:
   2.352 +  assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)" 
   2.353 +  shows "rbt_max (Branch c lt k v RBT_Impl.Empty) = k"
   2.354 +proof -
   2.355 +  have "List.fold max (tl (rev(RBT_Impl.keys lt @ [k]))) (hd (rev(RBT_Impl.keys lt @ [k]))) = k"
   2.356 +    using assms by (auto intro!: fold_max_triv dest!: left_le_key is_rbt_rbt_sorted)
   2.357 +  then show ?thesis by (auto simp add: rbt_max_def rbt_fold1_keys_def fold_max_rev_eq)
   2.358 +qed
   2.359 +
   2.360 +fun rbt_max_opt where
   2.361 +  "rbt_max_opt (Branch c lt k v RBT_Impl.Empty) = k" |
   2.362 +  "rbt_max_opt (Branch c lt k v (Branch rc rlc rk rv rrt)) = rbt_max_opt (Branch rc rlc rk rv rrt)"
   2.363 +
   2.364 +lemma rbt_max_opt_Branch:
   2.365 +  "t2 \<noteq> rbt.Empty \<Longrightarrow> rbt_max_opt (Branch c t1 k () t2) = rbt_max_opt t2" 
   2.366 +by (cases t2) auto
   2.367 +
   2.368 +lemma rbt_max_opt_induct [case_names empty right_empty right_non_empty]:
   2.369 +  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   2.370 +  assumes "P rbt.Empty"
   2.371 +  assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   2.372 +  assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   2.373 +  shows "P t"
   2.374 +using assms
   2.375 +  apply (induction t)
   2.376 +  apply simp
   2.377 +  apply (case_tac "t2 = rbt.Empty")
   2.378 +  apply simp_all
   2.379 +done
   2.380 +
   2.381 +lemma rbt_max_opt_in_set: 
   2.382 +  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   2.383 +  assumes "t \<noteq> rbt.Empty"
   2.384 +  shows "rbt_max_opt t \<in> set (RBT_Impl.keys t)"
   2.385 +using assms by (induction t rule: rbt_max_opt.induct) (auto)
   2.386 +
   2.387 +lemma rbt_max_opt_is_max:
   2.388 +  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   2.389 +  assumes "rbt_sorted t"
   2.390 +  assumes "t \<noteq> rbt.Empty"
   2.391 +  shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<le> rbt_max_opt t"
   2.392 +using assms 
   2.393 +proof (induction t rule: rbt_max_opt_induct)
   2.394 +  case empty
   2.395 +    then show ?case by simp
   2.396 +next
   2.397 +  case right_empty
   2.398 +    then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
   2.399 +next
   2.400 +  case (right_non_empty c t1 k v t2 y)
   2.401 +    then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
   2.402 +    with right_non_empty show ?case 
   2.403 +    proof(elim disjE)
   2.404 +      case goal1 then show ?case 
   2.405 +        by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
   2.406 +    next
   2.407 +      case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
   2.408 +    next 
   2.409 +      case goal3 show ?case
   2.410 +      proof -
   2.411 +        from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
   2.412 +        moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
   2.413 +        ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
   2.414 +      qed
   2.415 +    qed
   2.416 +qed
   2.417 +
   2.418 +lemma rbt_max_eq_rbt_max_opt:
   2.419 +  assumes "t \<noteq> RBT_Impl.Empty"
   2.420 +  assumes "is_rbt t"
   2.421 +  shows "rbt_max t = rbt_max_opt t"
   2.422 +proof -
   2.423 +  interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
   2.424 +    unfolding class.ab_semigroup_idem_mult_def by blast
   2.425 +  show ?thesis
   2.426 +    by (simp add: Max_eqI rbt_max_opt_is_max rbt_max_opt_in_set assms Max_def[symmetric]
   2.427 +      non_empty_rbt_keys fold1_set_fold[symmetric] rbt_max_def rbt_fold1_keys_def)
   2.428 +qed
   2.429 +
   2.430 +
   2.431 +(** abstract **)
   2.432 +
   2.433 +lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
   2.434 +  is rbt_fold1_keys by simp
   2.435 +
   2.436 +lemma fold1_keys_def_alt:
   2.437 +  "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
   2.438 +  by transfer (simp add: rbt_fold1_keys_def)
   2.439 +
   2.440 +lemma finite_fold1_fold1_keys:
   2.441 +  assumes "class.ab_semigroup_mult f"
   2.442 +  assumes "\<not> (is_empty t)"
   2.443 +  shows "Finite_Set.fold1 f (Set t) = fold1_keys f t"
   2.444 +proof -
   2.445 +  interpret ab_semigroup_mult f by fact
   2.446 +  show ?thesis using assms 
   2.447 +    by (auto simp: fold1_keys_def_alt set_keys fold_def_alt fold1_distinct_set_fold non_empty_keys)
   2.448 +qed
   2.449 +
   2.450 +(* minimum *)
   2.451 +
   2.452 +lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
   2.453 +
   2.454 +lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
   2.455 +
   2.456 +lemma r_min_alt_def: "r_min t = fold1_keys min t"
   2.457 +by transfer (simp add: rbt_min_def)
   2.458 +
   2.459 +lemma r_min_eq_r_min_opt:
   2.460 +  assumes "\<not> (is_empty t)"
   2.461 +  shows "r_min t = r_min_opt t"
   2.462 +using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
   2.463 +
   2.464 +lemma fold_keys_min_top_eq:
   2.465 +  fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
   2.466 +  assumes "\<not> (is_empty t)"
   2.467 +  shows "fold_keys min t top = fold1_keys min t"
   2.468 +proof -
   2.469 +  have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
   2.470 +    List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
   2.471 +    by (simp add: hd_Cons_tl[symmetric])
   2.472 +  { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
   2.473 +    have "List.fold min (x#xs) top = List.fold min xs x"
   2.474 +    by (simp add: inf_min[symmetric])
   2.475 +  } note ** = this
   2.476 +  show ?thesis using assms
   2.477 +    unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   2.478 +    apply transfer 
   2.479 +    apply (case_tac t) 
   2.480 +    apply simp 
   2.481 +    apply (subst *)
   2.482 +    apply simp
   2.483 +    apply (subst **)
   2.484 +    apply simp
   2.485 +  done
   2.486 +qed
   2.487 +
   2.488 +(* maximum *)
   2.489 +
   2.490 +lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
   2.491 +
   2.492 +lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
   2.493 +
   2.494 +lemma r_max_alt_def: "r_max t = fold1_keys max t"
   2.495 +by transfer (simp add: rbt_max_def)
   2.496 +
   2.497 +lemma r_max_eq_r_max_opt:
   2.498 +  assumes "\<not> (is_empty t)"
   2.499 +  shows "r_max t = r_max_opt t"
   2.500 +using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
   2.501 +
   2.502 +lemma fold_keys_max_bot_eq:
   2.503 +  fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
   2.504 +  assumes "\<not> (is_empty t)"
   2.505 +  shows "fold_keys max t bot = fold1_keys max t"
   2.506 +proof -
   2.507 +  have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
   2.508 +    List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
   2.509 +    by (simp add: hd_Cons_tl[symmetric])
   2.510 +  { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
   2.511 +    have "List.fold max (x#xs) bot = List.fold max xs x"
   2.512 +    by (simp add: sup_max[symmetric])
   2.513 +  } note ** = this
   2.514 +  show ?thesis using assms
   2.515 +    unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   2.516 +    apply transfer 
   2.517 +    apply (case_tac t) 
   2.518 +    apply simp 
   2.519 +    apply (subst *)
   2.520 +    apply simp
   2.521 +    apply (subst **)
   2.522 +    apply simp
   2.523 +  done
   2.524 +qed
   2.525 +
   2.526 +
   2.527 +section {* Code equations *}
   2.528 +
   2.529 +code_datatype Set Coset
   2.530 +
   2.531 +lemma empty_Set [code]:
   2.532 +  "Set.empty = Set RBT.empty"
   2.533 +by (auto simp: Set_def)
   2.534 +
   2.535 +lemma UNIV_Coset [code]:
   2.536 +  "UNIV = Coset RBT.empty"
   2.537 +by (auto simp: Set_def)
   2.538 +
   2.539 +lemma is_empty_Set [code]:
   2.540 +  "Set.is_empty (Set t) = RBT.is_empty t"
   2.541 +  unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1])
   2.542 +
   2.543 +lemma compl_code [code]:
   2.544 +  "- Set xs = Coset xs"
   2.545 +  "- Coset xs = Set xs"
   2.546 +by (simp_all add: Set_def)
   2.547 +
   2.548 +lemma member_code [code]:
   2.549 +  "x \<in> (Set t) = (RBT.lookup t x = Some ())"
   2.550 +  "x \<in> (Coset t) = (RBT.lookup t x = None)"
   2.551 +by (simp_all add: Set_def)
   2.552 +
   2.553 +lemma insert_code [code]:
   2.554 +  "Set.insert x (Set t) = Set (RBT.insert x () t)"
   2.555 +  "Set.insert x (Coset t) = Coset (RBT.delete x t)"
   2.556 +by (auto simp: Set_def)
   2.557 +
   2.558 +lemma remove_code [code]:
   2.559 +  "Set.remove x (Set t) = Set (RBT.delete x t)"
   2.560 +  "Set.remove x (Coset t) = Coset (RBT.insert x () t)"
   2.561 +by (auto simp: Set_def)
   2.562 +
   2.563 +lemma union_Set [code]:
   2.564 +  "Set t \<union> A = fold_keys Set.insert t A"
   2.565 +proof -
   2.566 +  interpret comp_fun_idem Set.insert
   2.567 +    by (fact comp_fun_idem_insert)
   2.568 +  from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`]
   2.569 +  show ?thesis by (auto simp add: union_fold_insert)
   2.570 +qed
   2.571 +
   2.572 +lemma inter_Set [code]:
   2.573 +  "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
   2.574 +by (simp add: inter_filter finite_filter_rbt_filter)
   2.575 +
   2.576 +lemma minus_Set [code]:
   2.577 +  "A - Set t = fold_keys Set.remove t A"
   2.578 +proof -
   2.579 +  interpret comp_fun_idem Set.remove
   2.580 +    by (fact comp_fun_idem_remove)
   2.581 +  from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`]
   2.582 +  show ?thesis by (auto simp add: minus_fold_remove)
   2.583 +qed
   2.584 +
   2.585 +lemma union_Coset [code]:
   2.586 +  "Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
   2.587 +proof -
   2.588 +  have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
   2.589 +  show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
   2.590 +qed
   2.591 + 
   2.592 +lemma union_Set_Set [code]:
   2.593 +  "Set t1 \<union> Set t2 = Set (union t1 t2)"
   2.594 +by (auto simp add: lookup_union map_add_Some_iff Set_def)
   2.595 +
   2.596 +lemma inter_Coset [code]:
   2.597 +  "A \<inter> Coset t = fold_keys Set.remove t A"
   2.598 +by (simp add: Diff_eq [symmetric] minus_Set)
   2.599 +
   2.600 +lemma inter_Coset_Coset [code]:
   2.601 +  "Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
   2.602 +by (auto simp add: lookup_union map_add_Some_iff Set_def)
   2.603 +
   2.604 +lemma minus_Coset [code]:
   2.605 +  "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
   2.606 +by (simp add: inter_Set[simplified Int_commute])
   2.607 +
   2.608 +lemma project_Set [code]:
   2.609 +  "Set.project P (Set t) = (rbt_filter P t)"
   2.610 +by (auto simp add: project_filter finite_filter_rbt_filter)
   2.611 +
   2.612 +lemma image_Set [code]:
   2.613 +  "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
   2.614 +proof -
   2.615 +  have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
   2.616 +  then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
   2.617 +qed
   2.618 +
   2.619 +lemma Ball_Set [code]:
   2.620 +  "Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   2.621 +proof -
   2.622 +  have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
   2.623 +  then show ?thesis 
   2.624 +    by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
   2.625 +qed
   2.626 +
   2.627 +lemma Bex_Set [code]:
   2.628 +  "Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   2.629 +proof -
   2.630 +  have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
   2.631 +  then show ?thesis 
   2.632 +    by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
   2.633 +qed
   2.634 +
   2.635 +lemma subset_code [code]:
   2.636 +  "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)"
   2.637 +  "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
   2.638 +by auto
   2.639 +
   2.640 +definition non_empty_trees where [code del]: "non_empty_trees t1 t2 \<longleftrightarrow> Coset t1 \<le> Set t2"
   2.641 +
   2.642 +code_abort non_empty_trees
   2.643 +
   2.644 +lemma subset_Coset_empty_Set_empty [code]:
   2.645 +  "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of 
   2.646 +    (rbt.Empty, rbt.Empty) => False |
   2.647 +    (_, _) => non_empty_trees t1 t2)"
   2.648 +proof -
   2.649 +  have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
   2.650 +    by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
   2.651 +  have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
   2.652 +  show ?thesis  
   2.653 +    by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split simp: non_empty_trees_def)
   2.654 +qed
   2.655 +
   2.656 +text {* A frequent case – avoid intermediate sets *}
   2.657 +lemma [code_unfold]:
   2.658 +  "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   2.659 +by (simp add: subset_code Ball_Set)
   2.660 +
   2.661 +lemma card_Set [code]:
   2.662 +  "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
   2.663 +by (auto simp add: card_def fold_image_def intro!: finite_fold_fold_keys) (default, simp) 
   2.664 +
   2.665 +lemma setsum_Set [code]:
   2.666 +  "setsum f (Set xs) = fold_keys (plus o f) xs 0"
   2.667 +proof -
   2.668 +  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
   2.669 +  then show ?thesis 
   2.670 +    by (auto simp add: setsum_def fold_image_def finite_fold_fold_keys o_def)
   2.671 +qed
   2.672 +
   2.673 +definition not_a_singleton_tree  where [code del]: "not_a_singleton_tree x y = x y"
   2.674 +
   2.675 +code_abort not_a_singleton_tree
   2.676 +
   2.677 +lemma the_elem_set [code]:
   2.678 +  fixes t :: "('a :: linorder, unit) rbt"
   2.679 +  shows "the_elem (Set t) = (case impl_of t of 
   2.680 +    (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
   2.681 +    | _ \<Rightarrow> not_a_singleton_tree the_elem (Set t))"
   2.682 +proof -
   2.683 +  {
   2.684 +    fix x :: "'a :: linorder"
   2.685 +    let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" 
   2.686 +    have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
   2.687 +    then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
   2.688 +
   2.689 +    have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
   2.690 +      by (subst(asm) RBT_inverse[symmetric, OF *])
   2.691 +        (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
   2.692 +  }
   2.693 +  then show ?thesis unfolding not_a_singleton_tree_def
   2.694 +    by(auto split: rbt.split unit.split color.split)
   2.695 +qed
   2.696 +
   2.697 +lemma Pow_Set [code]:
   2.698 +  "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
   2.699 +by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
   2.700 +
   2.701 +lemma product_Set [code]:
   2.702 +  "Product_Type.product (Set t1) (Set t2) = 
   2.703 +    fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
   2.704 +proof -
   2.705 +  have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
   2.706 +  show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]  
   2.707 +    by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
   2.708 +qed
   2.709 +
   2.710 +lemma Id_on_Set [code]:
   2.711 +  "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
   2.712 +proof -
   2.713 +  have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
   2.714 +  then show ?thesis
   2.715 +    by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
   2.716 +qed
   2.717 +
   2.718 +lemma Image_Set [code]:
   2.719 +  "(Set t) `` S = fold_keys (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) t {}"
   2.720 +by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold])
   2.721 +
   2.722 +lemma trancl_set_ntrancl [code]:
   2.723 +  "trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)"
   2.724 +by (simp add: finite_trancl_ntranl)
   2.725 +
   2.726 +lemma relcomp_Set[code]:
   2.727 +  "(Set t1) O (Set t2) = fold_keys 
   2.728 +    (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
   2.729 +proof -
   2.730 +  interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
   2.731 +  have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
   2.732 +    by default (auto simp add: fun_eq_iff)
   2.733 +  show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
   2.734 +    by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
   2.735 +qed
   2.736 +
   2.737 +lemma wf_set [code]:
   2.738 +  "wf (Set t) = acyclic (Set t)"
   2.739 +by (simp add: wf_iff_acyclic_if_finite)
   2.740 +
   2.741 +definition not_non_empty_tree  where [code del]: "not_non_empty_tree x y = x y"
   2.742 +
   2.743 +code_abort not_non_empty_tree
   2.744 +
   2.745 +lemma Min_fin_set_fold [code]:
   2.746 +  "Min (Set t) = (if is_empty t then not_non_empty_tree Min (Set t) else r_min_opt t)"
   2.747 +proof -
   2.748 +  have *:"(class.ab_semigroup_mult (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_min
   2.749 +    unfolding class.ab_semigroup_idem_mult_def by blast
   2.750 +  show ?thesis
   2.751 +    by (auto simp add: Min_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_min_alt_def 
   2.752 +      r_min_eq_r_min_opt[symmetric])  
   2.753 +qed
   2.754 +
   2.755 +lemma Inf_fin_set_fold [code]:
   2.756 +  "Inf_fin (Set t) = Min (Set t)"
   2.757 +by (simp add: inf_min Inf_fin_def Min_def)
   2.758 +
   2.759 +lemma Inf_Set_fold:
   2.760 +  fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   2.761 +  shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
   2.762 +proof -
   2.763 +  have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   2.764 +  then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   2.765 +    by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
   2.766 +  then show ?thesis 
   2.767 +    by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
   2.768 +qed
   2.769 +
   2.770 +definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
   2.771 +declare Inf'_def[symmetric, code_unfold]
   2.772 +declare Inf_Set_fold[folded Inf'_def, code]
   2.773 +
   2.774 +lemma INFI_Set_fold [code]:
   2.775 +  "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
   2.776 +proof -
   2.777 +  have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   2.778 +    by default (auto simp add: fun_eq_iff ac_simps)
   2.779 +  then show ?thesis
   2.780 +    by (auto simp: INF_fold_inf finite_fold_fold_keys)
   2.781 +qed
   2.782 +
   2.783 +lemma Max_fin_set_fold [code]:
   2.784 +  "Max (Set t) = (if is_empty t then not_non_empty_tree Max (Set t) else r_max_opt t)"
   2.785 +proof -
   2.786 +  have *:"(class.ab_semigroup_mult (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_max
   2.787 +    unfolding class.ab_semigroup_idem_mult_def by blast
   2.788 +  show ?thesis
   2.789 +    by (auto simp add: Max_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_max_alt_def 
   2.790 +      r_max_eq_r_max_opt[symmetric])  
   2.791 +qed
   2.792 +
   2.793 +lemma Sup_fin_set_fold [code]:
   2.794 +  "Sup_fin (Set t) = Max (Set t)"
   2.795 +by (simp add: sup_max Sup_fin_def Max_def)
   2.796 +
   2.797 +lemma Sup_Set_fold:
   2.798 +  fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   2.799 +  shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
   2.800 +proof -
   2.801 +  have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   2.802 +  then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   2.803 +    by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
   2.804 +  then show ?thesis 
   2.805 +    by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
   2.806 +qed
   2.807 +
   2.808 +definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
   2.809 +declare Sup'_def[symmetric, code_unfold]
   2.810 +declare Sup_Set_fold[folded Sup'_def, code]
   2.811 +
   2.812 +lemma SUPR_Set_fold [code]:
   2.813 +  "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
   2.814 +proof -
   2.815 +  have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   2.816 +    by default (auto simp add: fun_eq_iff ac_simps)
   2.817 +  then show ?thesis
   2.818 +    by (auto simp: SUP_fold_sup finite_fold_fold_keys)
   2.819 +qed
   2.820 +
   2.821 +lemma sorted_list_set[code]:
   2.822 +  "sorted_list_of_set (Set t) = keys t"
   2.823 +by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
   2.824 +
   2.825 +hide_const (open) RBT_Set.Set RBT_Set.Coset
   2.826 +
   2.827 +end