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