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