src/HOL/Library/RBT_Set.thy
 author Manuel Eberl 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
```