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