src/HOL/Library/RBT_Set.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 61076 bdc1e2f0a86a
child 63194 0b7bdb75f451
permissions -rw-r--r--
tuned references
     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   "setsum = setsum" ..
    89 
    90 lemma [code, code del]:
    91   "setprod = setprod" ..
    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   apply (induction t)
   278   apply simp
   279   apply (case_tac "t1 = rbt.Empty")
   280   apply simp_all
   281 done
   282 
   283 lemma rbt_min_opt_in_set: 
   284   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   285   assumes "t \<noteq> rbt.Empty"
   286   shows "rbt_min_opt t \<in> set (RBT_Impl.keys t)"
   287 using assms by (induction t rule: rbt_min_opt.induct) (auto)
   288 
   289 lemma rbt_min_opt_is_min:
   290   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   291   assumes "rbt_sorted t"
   292   assumes "t \<noteq> rbt.Empty"
   293   shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<ge> rbt_min_opt t"
   294 using assms 
   295 proof (induction t rule: rbt_min_opt_induct)
   296   case empty
   297   then show ?case by simp
   298 next
   299   case left_empty
   300   then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
   301 next
   302   case (left_non_empty c t1 k v t2 y)
   303   then consider "y = k" | "y \<in> set (RBT_Impl.keys t1)" | "y \<in> set (RBT_Impl.keys t2)"
   304     by auto
   305   then show ?case 
   306   proof cases
   307     case 1
   308     with left_non_empty show ?thesis
   309       by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
   310   next
   311     case 2
   312     with left_non_empty show ?thesis
   313       by (auto simp add: rbt_min_opt_Branch)
   314   next 
   315     case y: 3
   316     have "rbt_min_opt t1 \<le> k"
   317       using left_non_empty by (simp add: left_le_key rbt_min_opt_in_set)
   318     moreover have "k \<le> y"
   319       using left_non_empty y by (simp add: key_le_right)
   320     ultimately show ?thesis
   321       using left_non_empty y by (simp add: rbt_min_opt_Branch)
   322   qed
   323 qed
   324 
   325 lemma rbt_min_eq_rbt_min_opt:
   326   assumes "t \<noteq> RBT_Impl.Empty"
   327   assumes "is_rbt t"
   328   shows "rbt_min t = rbt_min_opt t"
   329 proof -
   330   from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
   331   with assms show ?thesis
   332     by (simp add: rbt_min_def rbt_fold1_keys_def rbt_min_opt_is_min
   333       Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
   334 qed
   335 
   336 (* maximum *)
   337 
   338 definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   339   where "rbt_max t = rbt_fold1_keys max t"
   340 
   341 lemma fold_max_triv:
   342   fixes k :: "_ :: linorder"
   343   shows "(\<forall>x\<in>set xs. x \<le> k) \<Longrightarrow> List.fold max xs k = k" 
   344 by (induct xs) (auto simp add: max_def)
   345 
   346 lemma fold_max_rev_eq:
   347   fixes xs :: "('a :: linorder) list"
   348   assumes "xs \<noteq> []"
   349   shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
   350   using assms by (simp add: Max.set_eq_fold [symmetric])
   351 
   352 lemma rbt_max_simps:
   353   assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)" 
   354   shows "rbt_max (Branch c lt k v RBT_Impl.Empty) = k"
   355 proof -
   356   have "List.fold max (tl (rev(RBT_Impl.keys lt @ [k]))) (hd (rev(RBT_Impl.keys lt @ [k]))) = k"
   357     using assms by (auto intro!: fold_max_triv dest!: left_le_key is_rbt_rbt_sorted)
   358   then show ?thesis by (auto simp add: rbt_max_def rbt_fold1_keys_def fold_max_rev_eq)
   359 qed
   360 
   361 fun rbt_max_opt where
   362   "rbt_max_opt (Branch c lt k v RBT_Impl.Empty) = k" |
   363   "rbt_max_opt (Branch c lt k v (Branch rc rlc rk rv rrt)) = rbt_max_opt (Branch rc rlc rk rv rrt)"
   364 
   365 lemma rbt_max_opt_Branch:
   366   "t2 \<noteq> rbt.Empty \<Longrightarrow> rbt_max_opt (Branch c t1 k () t2) = rbt_max_opt t2" 
   367 by (cases t2) auto
   368 
   369 lemma rbt_max_opt_induct [case_names empty right_empty right_non_empty]:
   370   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   371   assumes "P rbt.Empty"
   372   assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   373   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)"
   374   shows "P t"
   375 using assms
   376   apply (induction t)
   377   apply simp
   378   apply (case_tac "t2 = rbt.Empty")
   379   apply simp_all
   380 done
   381 
   382 lemma rbt_max_opt_in_set: 
   383   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   384   assumes "t \<noteq> rbt.Empty"
   385   shows "rbt_max_opt t \<in> set (RBT_Impl.keys t)"
   386 using assms by (induction t rule: rbt_max_opt.induct) (auto)
   387 
   388 lemma rbt_max_opt_is_max:
   389   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   390   assumes "rbt_sorted t"
   391   assumes "t \<noteq> rbt.Empty"
   392   shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<le> rbt_max_opt t"
   393 using assms 
   394 proof (induction t rule: rbt_max_opt_induct)
   395   case empty
   396   then show ?case by simp
   397 next
   398   case right_empty
   399   then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
   400 next
   401   case (right_non_empty c t1 k v t2 y)
   402   then consider "y = k" | "y \<in> set (RBT_Impl.keys t2)" | "y \<in> set (RBT_Impl.keys t1)"
   403     by auto
   404   then show ?case 
   405   proof cases
   406     case 1
   407     with right_non_empty show ?thesis
   408       by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
   409   next
   410     case 2
   411     with right_non_empty show ?thesis
   412       by (auto simp add: rbt_max_opt_Branch)
   413   next 
   414     case y: 3
   415     have "rbt_max_opt t2 \<ge> k"
   416       using right_non_empty by (simp add: key_le_right rbt_max_opt_in_set)
   417     moreover have "y \<le> k"
   418       using right_non_empty y by (simp add: left_le_key)
   419     ultimately show ?thesis
   420       using right_non_empty by (simp add: rbt_max_opt_Branch)
   421   qed
   422 qed
   423 
   424 lemma rbt_max_eq_rbt_max_opt:
   425   assumes "t \<noteq> RBT_Impl.Empty"
   426   assumes "is_rbt t"
   427   shows "rbt_max t = rbt_max_opt t"
   428 proof -
   429   from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
   430   with assms show ?thesis
   431     by (simp add: rbt_max_def rbt_fold1_keys_def rbt_max_opt_is_max
   432       Max.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set)
   433 qed
   434 
   435 
   436 (** abstract **)
   437 
   438 context includes rbt.lifting begin
   439 lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
   440   is rbt_fold1_keys .
   441 
   442 lemma fold1_keys_def_alt:
   443   "fold1_keys f t = List.fold f (tl (RBT.keys t)) (hd (RBT.keys t))"
   444   by transfer (simp add: rbt_fold1_keys_def)
   445 
   446 lemma finite_fold1_fold1_keys:
   447   assumes "semilattice f"
   448   assumes "\<not> RBT.is_empty t"
   449   shows "semilattice_set.F f (Set t) = fold1_keys f t"
   450 proof -
   451   from \<open>semilattice f\<close> interpret semilattice_set f by (rule semilattice_set.intro)
   452   show ?thesis using assms 
   453     by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric])
   454 qed
   455 
   456 (* minimum *)
   457 
   458 lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min .
   459 
   460 lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt .
   461 
   462 lemma r_min_alt_def: "r_min t = fold1_keys min t"
   463 by transfer (simp add: rbt_min_def)
   464 
   465 lemma r_min_eq_r_min_opt:
   466   assumes "\<not> (RBT.is_empty t)"
   467   shows "r_min t = r_min_opt t"
   468 using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
   469 
   470 lemma fold_keys_min_top_eq:
   471   fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
   472   assumes "\<not> (RBT.is_empty t)"
   473   shows "fold_keys min t top = fold1_keys min t"
   474 proof -
   475   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
   476     List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
   477     by (simp add: hd_Cons_tl[symmetric])
   478   { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
   479     have "List.fold min (x#xs) top = List.fold min xs x"
   480     by (simp add: inf_min[symmetric])
   481   } note ** = this
   482   show ?thesis using assms
   483     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   484     apply transfer 
   485     apply (case_tac t) 
   486     apply simp 
   487     apply (subst *)
   488     apply simp
   489     apply (subst **)
   490     apply simp
   491   done
   492 qed
   493 
   494 (* maximum *)
   495 
   496 lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max .
   497 
   498 lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt .
   499 
   500 lemma r_max_alt_def: "r_max t = fold1_keys max t"
   501 by transfer (simp add: rbt_max_def)
   502 
   503 lemma r_max_eq_r_max_opt:
   504   assumes "\<not> (RBT.is_empty t)"
   505   shows "r_max t = r_max_opt t"
   506 using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
   507 
   508 lemma fold_keys_max_bot_eq:
   509   fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
   510   assumes "\<not> (RBT.is_empty t)"
   511   shows "fold_keys max t bot = fold1_keys max t"
   512 proof -
   513   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
   514     List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
   515     by (simp add: hd_Cons_tl[symmetric])
   516   { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
   517     have "List.fold max (x#xs) bot = List.fold max xs x"
   518     by (simp add: sup_max[symmetric])
   519   } note ** = this
   520   show ?thesis using assms
   521     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   522     apply transfer 
   523     apply (case_tac t) 
   524     apply simp 
   525     apply (subst *)
   526     apply simp
   527     apply (subst **)
   528     apply simp
   529   done
   530 qed
   531 
   532 end
   533 
   534 section \<open>Code equations\<close>
   535 
   536 code_datatype Set Coset
   537 
   538 declare list.set[code] (* needed? *)
   539 
   540 lemma empty_Set [code]:
   541   "Set.empty = Set RBT.empty"
   542 by (auto simp: Set_def)
   543 
   544 lemma UNIV_Coset [code]:
   545   "UNIV = Coset RBT.empty"
   546 by (auto simp: Set_def)
   547 
   548 lemma is_empty_Set [code]:
   549   "Set.is_empty (Set t) = RBT.is_empty t"
   550   unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1])
   551 
   552 lemma compl_code [code]:
   553   "- Set xs = Coset xs"
   554   "- Coset xs = Set xs"
   555 by (simp_all add: Set_def)
   556 
   557 lemma member_code [code]:
   558   "x \<in> (Set t) = (RBT.lookup t x = Some ())"
   559   "x \<in> (Coset t) = (RBT.lookup t x = None)"
   560 by (simp_all add: Set_def)
   561 
   562 lemma insert_code [code]:
   563   "Set.insert x (Set t) = Set (RBT.insert x () t)"
   564   "Set.insert x (Coset t) = Coset (RBT.delete x t)"
   565 by (auto simp: Set_def)
   566 
   567 lemma remove_code [code]:
   568   "Set.remove x (Set t) = Set (RBT.delete x t)"
   569   "Set.remove x (Coset t) = Coset (RBT.insert x () t)"
   570 by (auto simp: Set_def)
   571 
   572 lemma union_Set [code]:
   573   "Set t \<union> A = fold_keys Set.insert t A"
   574 proof -
   575   interpret comp_fun_idem Set.insert
   576     by (fact comp_fun_idem_insert)
   577   from finite_fold_fold_keys[OF \<open>comp_fun_commute Set.insert\<close>]
   578   show ?thesis by (auto simp add: union_fold_insert)
   579 qed
   580 
   581 lemma inter_Set [code]:
   582   "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
   583 by (simp add: inter_Set_filter Set_filter_rbt_filter)
   584 
   585 lemma minus_Set [code]:
   586   "A - Set t = fold_keys Set.remove t A"
   587 proof -
   588   interpret comp_fun_idem Set.remove
   589     by (fact comp_fun_idem_remove)
   590   from finite_fold_fold_keys[OF \<open>comp_fun_commute Set.remove\<close>]
   591   show ?thesis by (auto simp add: minus_fold_remove)
   592 qed
   593 
   594 lemma union_Coset [code]:
   595   "Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
   596 proof -
   597   have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
   598   show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
   599 qed
   600  
   601 lemma union_Set_Set [code]:
   602   "Set t1 \<union> Set t2 = Set (RBT.union t1 t2)"
   603 by (auto simp add: lookup_union map_add_Some_iff Set_def)
   604 
   605 lemma inter_Coset [code]:
   606   "A \<inter> Coset t = fold_keys Set.remove t A"
   607 by (simp add: Diff_eq [symmetric] minus_Set)
   608 
   609 lemma inter_Coset_Coset [code]:
   610   "Coset t1 \<inter> Coset t2 = Coset (RBT.union t1 t2)"
   611 by (auto simp add: lookup_union map_add_Some_iff Set_def)
   612 
   613 lemma minus_Coset [code]:
   614   "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
   615 by (simp add: inter_Set[simplified Int_commute])
   616 
   617 lemma filter_Set [code]:
   618   "Set.filter P (Set t) = (rbt_filter P t)"
   619 by (auto simp add: Set_filter_rbt_filter)
   620 
   621 lemma image_Set [code]:
   622   "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
   623 proof -
   624   have "comp_fun_commute (\<lambda>k. Set.insert (f k))"
   625     by standard auto
   626   then show ?thesis
   627     by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
   628 qed
   629 
   630 lemma Ball_Set [code]:
   631   "Ball (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   632 proof -
   633   have "comp_fun_commute (\<lambda>k s. s \<and> P k)"
   634     by standard auto
   635   then show ?thesis 
   636     by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
   637 qed
   638 
   639 lemma Bex_Set [code]:
   640   "Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   641 proof -
   642   have "comp_fun_commute (\<lambda>k s. s \<or> P k)"
   643     by standard auto
   644   then show ?thesis 
   645     by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
   646 qed
   647 
   648 lemma subset_code [code]:
   649   "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)"
   650   "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
   651 by auto
   652 
   653 lemma subset_Coset_empty_Set_empty [code]:
   654   "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (RBT.impl_of t1, RBT.impl_of t2) of 
   655     (rbt.Empty, rbt.Empty) => False |
   656     (_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))"
   657 proof -
   658   have *: "\<And>t. RBT.impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
   659     by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
   660   have **: "eq_onp is_rbt rbt.Empty rbt.Empty" unfolding eq_onp_def by simp
   661   show ?thesis  
   662     by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
   663 qed
   664 
   665 text \<open>A frequent case -- avoid intermediate sets\<close>
   666 lemma [code_unfold]:
   667   "Set t1 \<subseteq> Set t2 \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   668 by (simp add: subset_code Ball_Set)
   669 
   670 lemma card_Set [code]:
   671   "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
   672   by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const)
   673 
   674 lemma setsum_Set [code]:
   675   "setsum f (Set xs) = fold_keys (plus o f) xs 0"
   676 proof -
   677   have "comp_fun_commute (\<lambda>x. op + (f x))"
   678     by standard (auto simp: ac_simps)
   679   then show ?thesis 
   680     by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
   681 qed
   682 
   683 lemma the_elem_set [code]:
   684   fixes t :: "('a :: linorder, unit) rbt"
   685   shows "the_elem (Set t) = (case RBT.impl_of t of 
   686     (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
   687     | _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))"
   688 proof -
   689   {
   690     fix x :: "'a :: linorder"
   691     let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" 
   692     have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
   693     then have **:"eq_onp is_rbt ?t ?t" unfolding eq_onp_def by auto
   694 
   695     have "RBT.impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
   696       by (subst(asm) RBT_inverse[symmetric, OF *])
   697         (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
   698   }
   699   then show ?thesis
   700     by(auto split: rbt.split unit.split color.split)
   701 qed
   702 
   703 lemma Pow_Set [code]: "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
   704   by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
   705 
   706 lemma product_Set [code]:
   707   "Product_Type.product (Set t1) (Set t2) = 
   708     fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
   709 proof -
   710   have *: "comp_fun_commute (\<lambda>y. Set.insert (x, y))" for x
   711     by standard auto
   712   show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]  
   713     by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
   714 qed
   715 
   716 lemma Id_on_Set [code]: "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
   717 proof -
   718   have "comp_fun_commute (\<lambda>x. Set.insert (x, x))"
   719     by standard auto
   720   then show ?thesis
   721     by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
   722 qed
   723 
   724 lemma Image_Set [code]:
   725   "(Set t) `` S = fold_keys (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) t {}"
   726 by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold])
   727 
   728 lemma trancl_set_ntrancl [code]:
   729   "trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)"
   730 by (simp add: finite_trancl_ntranl)
   731 
   732 lemma relcomp_Set[code]:
   733   "(Set t1) O (Set t2) = fold_keys 
   734     (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
   735 proof -
   736   interpret comp_fun_idem Set.insert
   737     by (fact comp_fun_idem_insert)
   738   have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
   739     by standard (auto simp add: fun_eq_iff)
   740   show ?thesis
   741     using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
   742     by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
   743 qed
   744 
   745 lemma wf_set [code]:
   746   "wf (Set t) = acyclic (Set t)"
   747 by (simp add: wf_iff_acyclic_if_finite)
   748 
   749 lemma Min_fin_set_fold [code]:
   750   "Min (Set t) = 
   751   (if RBT.is_empty t
   752    then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t))
   753    else r_min_opt t)"
   754 proof -
   755   have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
   756   with finite_fold1_fold1_keys [OF *, folded Min_def]
   757   show ?thesis
   758     by (simp add: r_min_alt_def r_min_eq_r_min_opt [symmetric])  
   759 qed
   760 
   761 lemma Inf_fin_set_fold [code]:
   762   "Inf_fin (Set t) = Min (Set t)"
   763 by (simp add: inf_min Inf_fin_def Min_def)
   764 
   765 lemma Inf_Set_fold:
   766   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   767   shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
   768 proof -
   769   have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
   770     by standard (simp add: fun_eq_iff ac_simps)
   771   then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   772     by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
   773   then show ?thesis 
   774     by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric]
   775       r_min_eq_r_min_opt[symmetric] r_min_alt_def)
   776 qed
   777 
   778 definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
   779 declare Inf'_def[symmetric, code_unfold]
   780 declare Inf_Set_fold[folded Inf'_def, code]
   781 
   782 lemma INF_Set_fold [code]:
   783   fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
   784   shows "INFIMUM (Set t) f = fold_keys (inf \<circ> f) t top"
   785 proof -
   786   have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   787     by standard (auto simp add: fun_eq_iff ac_simps)
   788   then show ?thesis
   789     by (auto simp: INF_fold_inf finite_fold_fold_keys)
   790 qed
   791 
   792 lemma Max_fin_set_fold [code]:
   793   "Max (Set t) = 
   794   (if RBT.is_empty t
   795    then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t))
   796    else r_max_opt t)"
   797 proof -
   798   have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
   799   with finite_fold1_fold1_keys [OF *, folded Max_def]
   800   show ?thesis
   801     by (simp add: r_max_alt_def r_max_eq_r_max_opt [symmetric])  
   802 qed
   803 
   804 lemma Sup_fin_set_fold [code]:
   805   "Sup_fin (Set t) = Max (Set t)"
   806 by (simp add: sup_max Sup_fin_def Max_def)
   807 
   808 lemma Sup_Set_fold:
   809   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   810   shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
   811 proof -
   812   have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
   813     by standard (simp add: fun_eq_iff ac_simps)
   814   then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   815     by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
   816   then show ?thesis 
   817     by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric]
   818       r_max_eq_r_max_opt[symmetric] r_max_alt_def)
   819 qed
   820 
   821 definition Sup' :: "'a :: {linorder,complete_lattice} set \<Rightarrow> 'a"
   822   where [code del]: "Sup' x = Sup x"
   823 declare Sup'_def[symmetric, code_unfold]
   824 declare Sup_Set_fold[folded Sup'_def, code]
   825 
   826 lemma SUP_Set_fold [code]:
   827   fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
   828   shows "SUPREMUM (Set t) f = fold_keys (sup \<circ> f) t bot"
   829 proof -
   830   have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   831     by standard (auto simp add: fun_eq_iff ac_simps)
   832   then show ?thesis
   833     by (auto simp: SUP_fold_sup finite_fold_fold_keys)
   834 qed
   835 
   836 lemma sorted_list_set[code]: "sorted_list_of_set (Set t) = RBT.keys t"
   837   by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
   838 
   839 lemma Bleast_code [code]:
   840   "Bleast (Set t) P =
   841     (case filter P (RBT.keys t) of
   842       x # xs \<Rightarrow> x
   843     | [] \<Rightarrow> abort_Bleast (Set t) P)"
   844 proof (cases "filter P (RBT.keys t)")
   845   case Nil
   846   thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
   847 next
   848   case (Cons x ys)
   849   have "(LEAST x. x \<in> Set t \<and> P x) = x"
   850   proof (rule Least_equality)
   851     show "x \<in> Set t \<and> P x"
   852       using Cons[symmetric]
   853       by (auto simp add: set_keys Cons_eq_filter_iff)
   854     next
   855       fix y
   856       assume "y \<in> Set t \<and> P y"
   857       then show "x \<le> y"
   858         using Cons[symmetric]
   859         by(auto simp add: set_keys Cons_eq_filter_iff)
   860           (metis sorted_Cons sorted_append sorted_keys)
   861   qed
   862   thus ?thesis using Cons by (simp add: Bleast_def)
   863 qed
   864 
   865 hide_const (open) RBT_Set.Set RBT_Set.Coset
   866 
   867 end