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