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