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