src/HOL/Library/RBT_Set.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (18 months ago)
changeset 67951 655aa11359dc
parent 67682 00c436488398
child 68109 cebf36c14226
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
     1 (*  Title:      HOL/Library/RBT_Set.thy
     2     Author:     Ondrej Kuncar
     3 *)
     4 
     5 section \<open>Implementation of sets using RBT trees\<close>
     6 
     7 theory RBT_Set
     8 imports RBT Product_Lexorder
     9 begin
    10 
    11 (*
    12   Users should be aware that by including this file all code equations
    13   outside of List.thy using 'a list as an implementation of sets cannot be
    14   used for code generation. If such equations are not needed, they can be
    15   deleted from the code generator. Otherwise, a user has to provide their 
    16   own equations using RBT trees. 
    17 *)
    18 
    19 section \<open>Definition of code datatype constructors\<close>
    20 
    21 definition Set :: "('a::linorder, unit) rbt \<Rightarrow> 'a set" 
    22   where "Set t = {x . RBT.lookup t x = Some ()}"
    23 
    24 definition Coset :: "('a::linorder, unit) rbt \<Rightarrow> 'a set" 
    25   where [simp]: "Coset t = - Set t"
    26 
    27 
    28 section \<open>Deletion of already existing code equations\<close>
    29 
    30 declare [[code drop: Set.empty Set.is_empty uminus_set_inst.uminus_set
    31   Set.member Set.insert Set.remove UNIV Set.filter image
    32   Set.subset_eq Ball Bex can_select Set.union minus_set_inst.minus_set Set.inter
    33   card the_elem Pow sum prod Product_Type.product Id_on
    34   Image trancl relcomp wf Min Inf_fin Max Sup_fin
    35   "(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)"
    36   sorted_list_of_set List.map_project List.Bleast]]
    37 
    38 
    39 section \<open>Lemmas\<close>
    40 
    41 subsection \<open>Auxiliary lemmas\<close>
    42 
    43 lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
    44 by (auto simp: not_Some_eq[THEN iffD1])
    45 
    46 lemma Set_set_keys: "Set x = dom (RBT.lookup x)" 
    47 by (auto simp: Set_def)
    48 
    49 lemma finite_Set [simp, intro!]: "finite (Set x)"
    50 by (simp add: Set_set_keys)
    51 
    52 lemma set_keys: "Set t = set(RBT.keys t)"
    53 by (simp add: Set_set_keys lookup_keys)
    54 
    55 subsection \<open>fold and filter\<close>
    56 
    57 lemma finite_fold_rbt_fold_eq:
    58   assumes "comp_fun_commute f" 
    59   shows "Finite_Set.fold f A (set (RBT.entries t)) = RBT.fold (curry f) t A"
    60 proof -
    61   have *: "remdups (RBT.entries t) = RBT.entries t"
    62     using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
    63   show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
    64 qed
    65 
    66 definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b" 
    67   where [code_unfold]:"fold_keys f t A = RBT.fold (\<lambda>k _ t. f k t) t A"
    68 
    69 lemma fold_keys_def_alt:
    70   "fold_keys f t s = List.fold f (RBT.keys t) s"
    71 by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)
    72 
    73 lemma finite_fold_fold_keys:
    74   assumes "comp_fun_commute f"
    75   shows "Finite_Set.fold f A (Set t) = fold_keys f t A"
    76 using assms
    77 proof -
    78   interpret comp_fun_commute f by fact
    79   have "set (RBT.keys t) = fst ` (set (RBT.entries t))" by (auto simp: fst_eq_Domain keys_entries)
    80   moreover have "inj_on fst (set (RBT.entries t))" using distinct_entries distinct_map by auto
    81   ultimately show ?thesis 
    82     by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq 
    83       comp_comp_fun_commute)
    84 qed
    85 
    86 definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
    87   "rbt_filter P t = RBT.fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
    88 
    89 lemma Set_filter_rbt_filter:
    90   "Set.filter P (Set t) = rbt_filter P t"
    91 by (simp add: fold_keys_def Set_filter_fold rbt_filter_def 
    92   finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
    93 
    94 
    95 subsection \<open>foldi and Ball\<close>
    96 
    97 lemma Ball_False: "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t False = False"
    98 by (induction t) auto
    99 
   100 lemma rbt_foldi_fold_conj: 
   101   "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"
   102 proof (induction t arbitrary: val) 
   103   case (Branch c t1) then show ?case
   104     by (cases "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t1 True") (simp_all add: Ball_False) 
   105 qed simp
   106 
   107 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"
   108 unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_conj)
   109 
   110 
   111 subsection \<open>foldi and Bex\<close>
   112 
   113 lemma Bex_True: "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True"
   114 by (induction t) auto
   115 
   116 lemma rbt_foldi_fold_disj: 
   117   "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"
   118 proof (induction t arbitrary: val) 
   119   case (Branch c t1) then show ?case
   120     by (cases "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t1 False") (simp_all add: Bex_True) 
   121 qed simp
   122 
   123 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"
   124 unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_disj)
   125 
   126 
   127 subsection \<open>folding over non empty trees and selecting the minimal and maximal element\<close>
   128 
   129 subsubsection \<open>concrete\<close>
   130 
   131 text \<open>The concrete part is here because it's probably not general enough to be moved to \<open>RBT_Impl\<close>\<close>
   132 
   133 definition rbt_fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a" 
   134   where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))"
   135 
   136 
   137 paragraph \<open>minimum\<close>
   138 
   139 definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   140   where "rbt_min t = rbt_fold1_keys min t"
   141 
   142 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)"
   143 by  (auto simp: rbt_greater_prop less_imp_le)
   144 
   145 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)"
   146 by (auto simp: rbt_less_prop less_imp_le)
   147 
   148 lemma fold_min_triv:
   149   fixes k :: "_ :: linorder"
   150   shows "(\<forall>x\<in>set xs. k \<le> x) \<Longrightarrow> List.fold min xs k = k" 
   151 by (induct xs) (auto simp add: min_def)
   152 
   153 lemma rbt_min_simps:
   154   "is_rbt (Branch c RBT_Impl.Empty k v rt) \<Longrightarrow> rbt_min (Branch c RBT_Impl.Empty k v rt) = k"
   155 by (auto intro: fold_min_triv dest: key_le_right is_rbt_rbt_sorted simp: rbt_fold1_keys_def rbt_min_def)
   156 
   157 fun rbt_min_opt where
   158   "rbt_min_opt (Branch c RBT_Impl.Empty k v rt) = k" |
   159   "rbt_min_opt (Branch c (Branch lc llc lk lv lrt) k v rt) = rbt_min_opt (Branch lc llc lk lv lrt)"
   160 
   161 lemma rbt_min_opt_Branch:
   162   "t1 \<noteq> rbt.Empty \<Longrightarrow> rbt_min_opt (Branch c t1 k () t2) = rbt_min_opt t1" 
   163 by (cases t1) auto
   164 
   165 lemma rbt_min_opt_induct [case_names empty left_empty left_non_empty]:
   166   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   167   assumes "P rbt.Empty"
   168   assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   169   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)"
   170   shows "P t"
   171   using assms
   172 proof (induct t)
   173   case Empty
   174   then show ?case by simp
   175 next
   176   case (Branch x1 t1 x3 x4 t2)
   177   then show ?case by (cases "t1 = rbt.Empty") simp_all
   178 qed
   179 
   180 lemma rbt_min_opt_in_set: 
   181   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   182   assumes "t \<noteq> rbt.Empty"
   183   shows "rbt_min_opt t \<in> set (RBT_Impl.keys t)"
   184 using assms by (induction t rule: rbt_min_opt.induct) (auto)
   185 
   186 lemma rbt_min_opt_is_min:
   187   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   188   assumes "rbt_sorted t"
   189   assumes "t \<noteq> rbt.Empty"
   190   shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<ge> rbt_min_opt t"
   191 using assms 
   192 proof (induction t rule: rbt_min_opt_induct)
   193   case empty
   194   then show ?case by simp
   195 next
   196   case left_empty
   197   then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
   198 next
   199   case (left_non_empty c t1 k v t2 y)
   200   then consider "y = k" | "y \<in> set (RBT_Impl.keys t1)" | "y \<in> set (RBT_Impl.keys t2)"
   201     by auto
   202   then show ?case 
   203   proof cases
   204     case 1
   205     with left_non_empty show ?thesis
   206       by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
   207   next
   208     case 2
   209     with left_non_empty show ?thesis
   210       by (auto simp add: rbt_min_opt_Branch)
   211   next 
   212     case y: 3
   213     have "rbt_min_opt t1 \<le> k"
   214       using left_non_empty by (simp add: left_le_key rbt_min_opt_in_set)
   215     moreover have "k \<le> y"
   216       using left_non_empty y by (simp add: key_le_right)
   217     ultimately show ?thesis
   218       using left_non_empty y by (simp add: rbt_min_opt_Branch)
   219   qed
   220 qed
   221 
   222 lemma rbt_min_eq_rbt_min_opt:
   223   assumes "t \<noteq> RBT_Impl.Empty"
   224   assumes "is_rbt t"
   225   shows "rbt_min t = rbt_min_opt t"
   226 proof -
   227   from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
   228   with assms show ?thesis
   229     by (simp add: rbt_min_def rbt_fold1_keys_def rbt_min_opt_is_min
   230       Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
   231 qed
   232 
   233 
   234 paragraph \<open>maximum\<close>
   235 
   236 definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   237   where "rbt_max t = rbt_fold1_keys max t"
   238 
   239 lemma fold_max_triv:
   240   fixes k :: "_ :: linorder"
   241   shows "(\<forall>x\<in>set xs. x \<le> k) \<Longrightarrow> List.fold max xs k = k" 
   242 by (induct xs) (auto simp add: max_def)
   243 
   244 lemma fold_max_rev_eq:
   245   fixes xs :: "('a :: linorder) list"
   246   assumes "xs \<noteq> []"
   247   shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
   248   using assms by (simp add: Max.set_eq_fold [symmetric])
   249 
   250 lemma rbt_max_simps:
   251   assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)" 
   252   shows "rbt_max (Branch c lt k v RBT_Impl.Empty) = k"
   253 proof -
   254   have "List.fold max (tl (rev(RBT_Impl.keys lt @ [k]))) (hd (rev(RBT_Impl.keys lt @ [k]))) = k"
   255     using assms by (auto intro!: fold_max_triv dest!: left_le_key is_rbt_rbt_sorted)
   256   then show ?thesis by (auto simp add: rbt_max_def rbt_fold1_keys_def fold_max_rev_eq)
   257 qed
   258 
   259 fun rbt_max_opt where
   260   "rbt_max_opt (Branch c lt k v RBT_Impl.Empty) = k" |
   261   "rbt_max_opt (Branch c lt k v (Branch rc rlc rk rv rrt)) = rbt_max_opt (Branch rc rlc rk rv rrt)"
   262 
   263 lemma rbt_max_opt_Branch:
   264   "t2 \<noteq> rbt.Empty \<Longrightarrow> rbt_max_opt (Branch c t1 k () t2) = rbt_max_opt t2" 
   265 by (cases t2) auto
   266 
   267 lemma rbt_max_opt_induct [case_names empty right_empty right_non_empty]:
   268   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   269   assumes "P rbt.Empty"
   270   assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   271   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)"
   272   shows "P t"
   273   using assms
   274 proof (induct t)
   275   case Empty
   276   then show ?case by simp
   277 next
   278   case (Branch x1 t1 x3 x4 t2)
   279   then show ?case by (cases "t2 = rbt.Empty") simp_all
   280 qed
   281 
   282 lemma rbt_max_opt_in_set: 
   283   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   284   assumes "t \<noteq> rbt.Empty"
   285   shows "rbt_max_opt t \<in> set (RBT_Impl.keys t)"
   286 using assms by (induction t rule: rbt_max_opt.induct) (auto)
   287 
   288 lemma rbt_max_opt_is_max:
   289   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   290   assumes "rbt_sorted t"
   291   assumes "t \<noteq> rbt.Empty"
   292   shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<le> rbt_max_opt t"
   293 using assms 
   294 proof (induction t rule: rbt_max_opt_induct)
   295   case empty
   296   then show ?case by simp
   297 next
   298   case right_empty
   299   then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
   300 next
   301   case (right_non_empty c t1 k v t2 y)
   302   then consider "y = k" | "y \<in> set (RBT_Impl.keys t2)" | "y \<in> set (RBT_Impl.keys t1)"
   303     by auto
   304   then show ?case 
   305   proof cases
   306     case 1
   307     with right_non_empty show ?thesis
   308       by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
   309   next
   310     case 2
   311     with right_non_empty show ?thesis
   312       by (auto simp add: rbt_max_opt_Branch)
   313   next 
   314     case y: 3
   315     have "rbt_max_opt t2 \<ge> k"
   316       using right_non_empty by (simp add: key_le_right rbt_max_opt_in_set)
   317     moreover have "y \<le> k"
   318       using right_non_empty y by (simp add: left_le_key)
   319     ultimately show ?thesis
   320       using right_non_empty by (simp add: rbt_max_opt_Branch)
   321   qed
   322 qed
   323 
   324 lemma rbt_max_eq_rbt_max_opt:
   325   assumes "t \<noteq> RBT_Impl.Empty"
   326   assumes "is_rbt t"
   327   shows "rbt_max t = rbt_max_opt t"
   328 proof -
   329   from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
   330   with assms show ?thesis
   331     by (simp add: rbt_max_def rbt_fold1_keys_def rbt_max_opt_is_max
   332       Max.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set)
   333 qed
   334 
   335 
   336 subsubsection \<open>abstract\<close>
   337 
   338 context includes rbt.lifting begin
   339 lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
   340   is rbt_fold1_keys .
   341 
   342 lemma fold1_keys_def_alt:
   343   "fold1_keys f t = List.fold f (tl (RBT.keys t)) (hd (RBT.keys t))"
   344   by transfer (simp add: rbt_fold1_keys_def)
   345 
   346 lemma finite_fold1_fold1_keys:
   347   assumes "semilattice f"
   348   assumes "\<not> RBT.is_empty t"
   349   shows "semilattice_set.F f (Set t) = fold1_keys f t"
   350 proof -
   351   from \<open>semilattice f\<close> interpret semilattice_set f by (rule semilattice_set.intro)
   352   show ?thesis using assms 
   353     by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric])
   354 qed
   355 
   356 
   357 paragraph \<open>minimum\<close>
   358 
   359 lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min .
   360 
   361 lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt .
   362 
   363 lemma r_min_alt_def: "r_min t = fold1_keys min t"
   364 by transfer (simp add: rbt_min_def)
   365 
   366 lemma r_min_eq_r_min_opt:
   367   assumes "\<not> (RBT.is_empty t)"
   368   shows "r_min t = r_min_opt t"
   369 using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
   370 
   371 lemma fold_keys_min_top_eq:
   372   fixes t :: "('a::{linorder,bounded_lattice_top}, unit) rbt"
   373   assumes "\<not> (RBT.is_empty t)"
   374   shows "fold_keys min t top = fold1_keys min t"
   375 proof -
   376   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
   377       List.fold min (hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t)) top"
   378     by (simp add: hd_Cons_tl[symmetric])
   379   have **: "List.fold min (x # xs) top = List.fold min xs x" for x :: 'a and xs
   380     by (simp add: inf_min[symmetric])
   381   show ?thesis
   382     using assms
   383     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   384     apply transfer 
   385     apply (case_tac t) 
   386      apply simp 
   387     apply (subst *)
   388      apply simp
   389     apply (subst **)
   390     apply simp
   391     done
   392 qed
   393 
   394 
   395 paragraph \<open>maximum\<close>
   396 
   397 lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max .
   398 
   399 lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt .
   400 
   401 lemma r_max_alt_def: "r_max t = fold1_keys max t"
   402 by transfer (simp add: rbt_max_def)
   403 
   404 lemma r_max_eq_r_max_opt:
   405   assumes "\<not> (RBT.is_empty t)"
   406   shows "r_max t = r_max_opt t"
   407 using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
   408 
   409 lemma fold_keys_max_bot_eq:
   410   fixes t :: "('a::{linorder,bounded_lattice_bot}, unit) rbt"
   411   assumes "\<not> (RBT.is_empty t)"
   412   shows "fold_keys max t bot = fold1_keys max t"
   413 proof -
   414   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
   415       List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
   416     by (simp add: hd_Cons_tl[symmetric])
   417   have **: "List.fold max (x # xs) bot = List.fold max xs x" for x :: 'a and xs
   418     by (simp add: sup_max[symmetric])
   419   show ?thesis
   420     using assms
   421     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   422     apply transfer 
   423     apply (case_tac t) 
   424      apply simp 
   425     apply (subst *)
   426      apply simp
   427     apply (subst **)
   428     apply simp
   429     done
   430 qed
   431 
   432 end
   433 
   434 section \<open>Code equations\<close>
   435 
   436 code_datatype Set Coset
   437 
   438 declare list.set[code] (* needed? *)
   439 
   440 lemma empty_Set [code]:
   441   "Set.empty = Set RBT.empty"
   442 by (auto simp: Set_def)
   443 
   444 lemma UNIV_Coset [code]:
   445   "UNIV = Coset RBT.empty"
   446 by (auto simp: Set_def)
   447 
   448 lemma is_empty_Set [code]:
   449   "Set.is_empty (Set t) = RBT.is_empty t"
   450   unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1])
   451 
   452 lemma compl_code [code]:
   453   "- Set xs = Coset xs"
   454   "- Coset xs = Set xs"
   455 by (simp_all add: Set_def)
   456 
   457 lemma member_code [code]:
   458   "x \<in> (Set t) = (RBT.lookup t x = Some ())"
   459   "x \<in> (Coset t) = (RBT.lookup t x = None)"
   460 by (simp_all add: Set_def)
   461 
   462 lemma insert_code [code]:
   463   "Set.insert x (Set t) = Set (RBT.insert x () t)"
   464   "Set.insert x (Coset t) = Coset (RBT.delete x t)"
   465 by (auto simp: Set_def)
   466 
   467 lemma remove_code [code]:
   468   "Set.remove x (Set t) = Set (RBT.delete x t)"
   469   "Set.remove x (Coset t) = Coset (RBT.insert x () t)"
   470 by (auto simp: Set_def)
   471 
   472 lemma union_Set [code]:
   473   "Set t \<union> A = fold_keys Set.insert t A"
   474 proof -
   475   interpret comp_fun_idem Set.insert
   476     by (fact comp_fun_idem_insert)
   477   from finite_fold_fold_keys[OF comp_fun_commute_axioms]
   478   show ?thesis by (auto simp add: union_fold_insert)
   479 qed
   480 
   481 lemma inter_Set [code]:
   482   "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
   483 by (simp add: inter_Set_filter Set_filter_rbt_filter)
   484 
   485 lemma minus_Set [code]:
   486   "A - Set t = fold_keys Set.remove t A"
   487 proof -
   488   interpret comp_fun_idem Set.remove
   489     by (fact comp_fun_idem_remove)
   490   from finite_fold_fold_keys[OF comp_fun_commute_axioms]
   491   show ?thesis by (auto simp add: minus_fold_remove)
   492 qed
   493 
   494 lemma union_Coset [code]:
   495   "Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
   496 proof -
   497   have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
   498   show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
   499 qed
   500  
   501 lemma union_Set_Set [code]:
   502   "Set t1 \<union> Set t2 = Set (RBT.union t1 t2)"
   503 by (auto simp add: lookup_union map_add_Some_iff Set_def)
   504 
   505 lemma inter_Coset [code]:
   506   "A \<inter> Coset t = fold_keys Set.remove t A"
   507 by (simp add: Diff_eq [symmetric] minus_Set)
   508 
   509 lemma inter_Coset_Coset [code]:
   510   "Coset t1 \<inter> Coset t2 = Coset (RBT.union t1 t2)"
   511 by (auto simp add: lookup_union map_add_Some_iff Set_def)
   512 
   513 lemma minus_Coset [code]:
   514   "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
   515 by (simp add: inter_Set[simplified Int_commute])
   516 
   517 lemma filter_Set [code]:
   518   "Set.filter P (Set t) = (rbt_filter P t)"
   519 by (auto simp add: Set_filter_rbt_filter)
   520 
   521 lemma image_Set [code]:
   522   "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
   523 proof -
   524   have "comp_fun_commute (\<lambda>k. Set.insert (f k))"
   525     by standard auto
   526   then show ?thesis
   527     by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
   528 qed
   529 
   530 lemma Ball_Set [code]:
   531   "Ball (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   532 proof -
   533   have "comp_fun_commute (\<lambda>k s. s \<and> P k)"
   534     by standard auto
   535   then show ?thesis 
   536     by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
   537 qed
   538 
   539 lemma Bex_Set [code]:
   540   "Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   541 proof -
   542   have "comp_fun_commute (\<lambda>k s. s \<or> P k)"
   543     by standard auto
   544   then show ?thesis 
   545     by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
   546 qed
   547 
   548 lemma subset_code [code]:
   549   "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)"
   550   "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
   551 by auto
   552 
   553 lemma subset_Coset_empty_Set_empty [code]:
   554   "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (RBT.impl_of t1, RBT.impl_of t2) of 
   555     (rbt.Empty, rbt.Empty) \<Rightarrow> False |
   556     (_, _) \<Rightarrow> Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))"
   557 proof -
   558   have *: "\<And>t. RBT.impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
   559     by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
   560   have **: "eq_onp is_rbt rbt.Empty rbt.Empty" unfolding eq_onp_def by simp
   561   show ?thesis  
   562     by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
   563 qed
   564 
   565 text \<open>A frequent case -- avoid intermediate sets\<close>
   566 lemma [code_unfold]:
   567   "Set t1 \<subseteq> Set t2 \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   568 by (simp add: subset_code Ball_Set)
   569 
   570 lemma card_Set [code]:
   571   "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
   572   by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const)
   573 
   574 lemma sum_Set [code]:
   575   "sum f (Set xs) = fold_keys (plus \<circ> f) xs 0"
   576 proof -
   577   have "comp_fun_commute (\<lambda>x. (+) (f x))"
   578     by standard (auto simp: ac_simps)
   579   then show ?thesis 
   580     by (auto simp add: sum.eq_fold finite_fold_fold_keys o_def)
   581 qed
   582 
   583 lemma the_elem_set [code]:
   584   fixes t :: "('a :: linorder, unit) rbt"
   585   shows "the_elem (Set t) = (case RBT.impl_of t of 
   586     (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
   587     | _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))"
   588 proof -
   589   {
   590     fix x :: "'a :: linorder"
   591     let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" 
   592     have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
   593     then have **:"eq_onp is_rbt ?t ?t" unfolding eq_onp_def by auto
   594 
   595     have "RBT.impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
   596       by (subst(asm) RBT_inverse[symmetric, OF *])
   597         (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
   598   }
   599   then show ?thesis
   600     by(auto split: rbt.split unit.split color.split)
   601 qed
   602 
   603 lemma Pow_Set [code]: "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
   604   by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
   605 
   606 lemma product_Set [code]:
   607   "Product_Type.product (Set t1) (Set t2) = 
   608     fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
   609 proof -
   610   have *: "comp_fun_commute (\<lambda>y. Set.insert (x, y))" for x
   611     by standard auto
   612   show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]  
   613     by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
   614 qed
   615 
   616 lemma Id_on_Set [code]: "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
   617 proof -
   618   have "comp_fun_commute (\<lambda>x. Set.insert (x, x))"
   619     by standard auto
   620   then show ?thesis
   621     by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
   622 qed
   623 
   624 lemma Image_Set [code]:
   625   "(Set t) `` S = fold_keys (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) t {}"
   626 by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold])
   627 
   628 lemma trancl_set_ntrancl [code]:
   629   "trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)"
   630 by (simp add: finite_trancl_ntranl)
   631 
   632 lemma relcomp_Set[code]:
   633   "(Set t1) O (Set t2) = fold_keys 
   634     (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
   635 proof -
   636   interpret comp_fun_idem Set.insert
   637     by (fact comp_fun_idem_insert)
   638   have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
   639     by standard (auto simp add: fun_eq_iff)
   640   show ?thesis
   641     using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
   642     by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
   643 qed
   644 
   645 lemma wf_set [code]:
   646   "wf (Set t) = acyclic (Set t)"
   647 by (simp add: wf_iff_acyclic_if_finite)
   648 
   649 lemma Min_fin_set_fold [code]:
   650   "Min (Set t) = 
   651   (if RBT.is_empty t
   652    then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t))
   653    else r_min_opt t)"
   654 proof -
   655   have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
   656   with finite_fold1_fold1_keys [OF *, folded Min_def]
   657   show ?thesis
   658     by (simp add: r_min_alt_def r_min_eq_r_min_opt [symmetric])  
   659 qed
   660 
   661 lemma Inf_fin_set_fold [code]:
   662   "Inf_fin (Set t) = Min (Set t)"
   663 by (simp add: inf_min Inf_fin_def Min_def)
   664 
   665 lemma Inf_Set_fold:
   666   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   667   shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
   668 proof -
   669   have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
   670     by standard (simp add: fun_eq_iff ac_simps)
   671   then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   672     by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
   673   then show ?thesis 
   674     by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric]
   675       r_min_eq_r_min_opt[symmetric] r_min_alt_def)
   676 qed
   677 
   678 lemma Max_fin_set_fold [code]:
   679   "Max (Set t) = 
   680   (if RBT.is_empty t
   681    then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t))
   682    else r_max_opt t)"
   683 proof -
   684   have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
   685   with finite_fold1_fold1_keys [OF *, folded Max_def]
   686   show ?thesis
   687     by (simp add: r_max_alt_def r_max_eq_r_max_opt [symmetric])  
   688 qed
   689 
   690 lemma Sup_fin_set_fold [code]:
   691   "Sup_fin (Set t) = Max (Set t)"
   692 by (simp add: sup_max Sup_fin_def Max_def)
   693 
   694 lemma Sup_Set_fold:
   695   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   696   shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
   697 proof -
   698   have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
   699     by standard (simp add: fun_eq_iff ac_simps)
   700   then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   701     by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
   702   then show ?thesis 
   703     by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric]
   704       r_max_eq_r_max_opt[symmetric] r_max_alt_def)
   705 qed
   706 
   707 context
   708 begin
   709 
   710 qualified definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a"
   711   where [code_abbrev]: "Inf' = Inf"
   712 
   713 lemma Inf'_Set_fold [code]:
   714   "Inf' (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
   715   by (simp add: Inf'_def Inf_Set_fold)
   716 
   717 qualified definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a"
   718   where [code_abbrev]: "Sup' = Sup"
   719 
   720 lemma Sup'_Set_fold [code]:
   721   "Sup' (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
   722   by (simp add: Sup'_def Sup_Set_fold)
   723 
   724 lemma [code drop: Gcd_fin, code]:
   725   "Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) = fold_keys gcd t (0::'a::{semiring_gcd, linorder})"
   726 proof -
   727   have "comp_fun_commute (gcd :: 'a \<Rightarrow> _)"
   728     by standard (simp add: fun_eq_iff ac_simps)
   729   with finite_fold_fold_keys [of _ 0 t]
   730   have "Finite_Set.fold gcd 0 (Set t) = fold_keys gcd t 0"
   731     by blast
   732   then show ?thesis
   733     by (simp add: Gcd_fin.eq_fold)
   734 qed
   735     
   736 lemma [code drop: "Gcd :: _ \<Rightarrow> nat", code]:
   737   "Gcd (Set t) = (Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) :: nat)"
   738   by simp
   739 
   740 lemma [code drop: "Gcd :: _ \<Rightarrow> int", code]:
   741   "Gcd (Set t) = (Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) :: int)"
   742   by simp
   743 
   744 lemma [code drop: Lcm_fin,code]:
   745   "Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) = fold_keys lcm t (1::'a::{semiring_gcd, linorder})"
   746 proof -
   747   have "comp_fun_commute (lcm :: 'a \<Rightarrow> _)"
   748     by standard (simp add: fun_eq_iff ac_simps)
   749   with finite_fold_fold_keys [of _ 1 t]
   750   have "Finite_Set.fold lcm 1 (Set t) = fold_keys lcm t 1"
   751     by blast
   752   then show ?thesis
   753     by (simp add: Lcm_fin.eq_fold)
   754 qed
   755 
   756 qualified definition Lcm' :: "'a :: semiring_Gcd set \<Rightarrow> 'a"
   757   where [code_abbrev]: "Lcm' = Lcm"
   758 
   759 lemma [code drop: "Lcm :: _ \<Rightarrow> nat", code]:
   760   "Lcm (Set t) = (Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) :: nat)"
   761   by simp
   762 
   763 lemma [code drop: "Lcm :: _ \<Rightarrow> int", code]:
   764   "Lcm (Set t) = (Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) :: int)"
   765   by simp
   766 
   767 end
   768 
   769 lemma sorted_list_set[code]: "sorted_list_of_set (Set t) = RBT.keys t"
   770   by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
   771 
   772 lemma Bleast_code [code]:
   773   "Bleast (Set t) P =
   774     (case List.filter P (RBT.keys t) of
   775       x # xs \<Rightarrow> x
   776     | [] \<Rightarrow> abort_Bleast (Set t) P)"
   777 proof (cases "List.filter P (RBT.keys t)")
   778   case Nil
   779   thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
   780 next
   781   case (Cons x ys)
   782   have "(LEAST x. x \<in> Set t \<and> P x) = x"
   783   proof (rule Least_equality)
   784     show "x \<in> Set t \<and> P x"
   785       using Cons[symmetric]
   786       by (auto simp add: set_keys Cons_eq_filter_iff)
   787     next
   788       fix y
   789       assume "y \<in> Set t \<and> P y"
   790       then show "x \<le> y"
   791         using Cons[symmetric]
   792         by(auto simp add: set_keys Cons_eq_filter_iff)
   793           (metis sorted_Cons sorted_append sorted_keys)
   794   qed
   795   thus ?thesis using Cons by (simp add: Bleast_def)
   796 qed
   797 
   798 hide_const (open) RBT_Set.Set RBT_Set.Coset
   799 
   800 end