src/HOL/Library/RBT_Set.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 53955 436649a2ed62
child 54263 c4159fe6fa46
permissions -rw-r--r--
more simplification rules on unary and binary minus
     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 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 (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(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(entries t)) = fold (curry f) t A"
   163 proof -
   164   have *: "remdups (entries t) = 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 = 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 (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 (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries)
   183   moreover have "inj_on fst (set (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 = 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: "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 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: "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 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 lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
   426   is rbt_fold1_keys by simp
   427 
   428 lemma fold1_keys_def_alt:
   429   "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
   430   by transfer (simp add: rbt_fold1_keys_def)
   431 
   432 lemma finite_fold1_fold1_keys:
   433   assumes "semilattice f"
   434   assumes "\<not> is_empty t"
   435   shows "semilattice_set.F f (Set t) = fold1_keys f t"
   436 proof -
   437   from `semilattice f` interpret semilattice_set f by (rule semilattice_set.intro)
   438   show ?thesis using assms 
   439     by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric])
   440 qed
   441 
   442 (* minimum *)
   443 
   444 lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
   445 
   446 lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
   447 
   448 lemma r_min_alt_def: "r_min t = fold1_keys min t"
   449 by transfer (simp add: rbt_min_def)
   450 
   451 lemma r_min_eq_r_min_opt:
   452   assumes "\<not> (is_empty t)"
   453   shows "r_min t = r_min_opt t"
   454 using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
   455 
   456 lemma fold_keys_min_top_eq:
   457   fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
   458   assumes "\<not> (is_empty t)"
   459   shows "fold_keys min t top = fold1_keys min t"
   460 proof -
   461   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
   462     List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
   463     by (simp add: hd_Cons_tl[symmetric])
   464   { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
   465     have "List.fold min (x#xs) top = List.fold min xs x"
   466     by (simp add: inf_min[symmetric])
   467   } note ** = this
   468   show ?thesis using assms
   469     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   470     apply transfer 
   471     apply (case_tac t) 
   472     apply simp 
   473     apply (subst *)
   474     apply simp
   475     apply (subst **)
   476     apply simp
   477   done
   478 qed
   479 
   480 (* maximum *)
   481 
   482 lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
   483 
   484 lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
   485 
   486 lemma r_max_alt_def: "r_max t = fold1_keys max t"
   487 by transfer (simp add: rbt_max_def)
   488 
   489 lemma r_max_eq_r_max_opt:
   490   assumes "\<not> (is_empty t)"
   491   shows "r_max t = r_max_opt t"
   492 using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
   493 
   494 lemma fold_keys_max_bot_eq:
   495   fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
   496   assumes "\<not> (is_empty t)"
   497   shows "fold_keys max t bot = fold1_keys max t"
   498 proof -
   499   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
   500     List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
   501     by (simp add: hd_Cons_tl[symmetric])
   502   { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
   503     have "List.fold max (x#xs) bot = List.fold max xs x"
   504     by (simp add: sup_max[symmetric])
   505   } note ** = this
   506   show ?thesis using assms
   507     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   508     apply transfer 
   509     apply (case_tac t) 
   510     apply simp 
   511     apply (subst *)
   512     apply simp
   513     apply (subst **)
   514     apply simp
   515   done
   516 qed
   517 
   518 
   519 section {* Code equations *}
   520 
   521 code_datatype Set Coset
   522 
   523 declare set.simps[code]
   524 
   525 lemma empty_Set [code]:
   526   "Set.empty = Set RBT.empty"
   527 by (auto simp: Set_def)
   528 
   529 lemma UNIV_Coset [code]:
   530   "UNIV = Coset RBT.empty"
   531 by (auto simp: Set_def)
   532 
   533 lemma is_empty_Set [code]:
   534   "Set.is_empty (Set t) = RBT.is_empty t"
   535   unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1])
   536 
   537 lemma compl_code [code]:
   538   "- Set xs = Coset xs"
   539   "- Coset xs = Set xs"
   540 by (simp_all add: Set_def)
   541 
   542 lemma member_code [code]:
   543   "x \<in> (Set t) = (RBT.lookup t x = Some ())"
   544   "x \<in> (Coset t) = (RBT.lookup t x = None)"
   545 by (simp_all add: Set_def)
   546 
   547 lemma insert_code [code]:
   548   "Set.insert x (Set t) = Set (RBT.insert x () t)"
   549   "Set.insert x (Coset t) = Coset (RBT.delete x t)"
   550 by (auto simp: Set_def)
   551 
   552 lemma remove_code [code]:
   553   "Set.remove x (Set t) = Set (RBT.delete x t)"
   554   "Set.remove x (Coset t) = Coset (RBT.insert x () t)"
   555 by (auto simp: Set_def)
   556 
   557 lemma union_Set [code]:
   558   "Set t \<union> A = fold_keys Set.insert t A"
   559 proof -
   560   interpret comp_fun_idem Set.insert
   561     by (fact comp_fun_idem_insert)
   562   from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`]
   563   show ?thesis by (auto simp add: union_fold_insert)
   564 qed
   565 
   566 lemma inter_Set [code]:
   567   "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
   568 by (simp add: inter_Set_filter Set_filter_rbt_filter)
   569 
   570 lemma minus_Set [code]:
   571   "A - Set t = fold_keys Set.remove t A"
   572 proof -
   573   interpret comp_fun_idem Set.remove
   574     by (fact comp_fun_idem_remove)
   575   from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`]
   576   show ?thesis by (auto simp add: minus_fold_remove)
   577 qed
   578 
   579 lemma union_Coset [code]:
   580   "Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
   581 proof -
   582   have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
   583   show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
   584 qed
   585  
   586 lemma union_Set_Set [code]:
   587   "Set t1 \<union> Set t2 = Set (union t1 t2)"
   588 by (auto simp add: lookup_union map_add_Some_iff Set_def)
   589 
   590 lemma inter_Coset [code]:
   591   "A \<inter> Coset t = fold_keys Set.remove t A"
   592 by (simp add: Diff_eq [symmetric] minus_Set)
   593 
   594 lemma inter_Coset_Coset [code]:
   595   "Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
   596 by (auto simp add: lookup_union map_add_Some_iff Set_def)
   597 
   598 lemma minus_Coset [code]:
   599   "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
   600 by (simp add: inter_Set[simplified Int_commute])
   601 
   602 lemma filter_Set [code]:
   603   "Set.filter P (Set t) = (rbt_filter P t)"
   604 by (auto simp add: Set_filter_rbt_filter)
   605 
   606 lemma image_Set [code]:
   607   "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
   608 proof -
   609   have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
   610   then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
   611 qed
   612 
   613 lemma Ball_Set [code]:
   614   "Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   615 proof -
   616   have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
   617   then show ?thesis 
   618     by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
   619 qed
   620 
   621 lemma Bex_Set [code]:
   622   "Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   623 proof -
   624   have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
   625   then show ?thesis 
   626     by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
   627 qed
   628 
   629 lemma subset_code [code]:
   630   "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)"
   631   "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
   632 by auto
   633 
   634 lemma subset_Coset_empty_Set_empty [code]:
   635   "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of 
   636     (rbt.Empty, rbt.Empty) => False |
   637     (_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))"
   638 proof -
   639   have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
   640     by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
   641   have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
   642   show ?thesis  
   643     by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
   644 qed
   645 
   646 text {* A frequent case – avoid intermediate sets *}
   647 lemma [code_unfold]:
   648   "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   649 by (simp add: subset_code Ball_Set)
   650 
   651 lemma card_Set [code]:
   652   "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
   653   by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const)
   654 
   655 lemma setsum_Set [code]:
   656   "setsum f (Set xs) = fold_keys (plus o f) xs 0"
   657 proof -
   658   have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
   659   then show ?thesis 
   660     by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
   661 qed
   662 
   663 lemma the_elem_set [code]:
   664   fixes t :: "('a :: linorder, unit) rbt"
   665   shows "the_elem (Set t) = (case impl_of t of 
   666     (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
   667     | _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))"
   668 proof -
   669   {
   670     fix x :: "'a :: linorder"
   671     let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" 
   672     have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
   673     then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
   674 
   675     have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
   676       by (subst(asm) RBT_inverse[symmetric, OF *])
   677         (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
   678   }
   679   then show ?thesis
   680     by(auto split: rbt.split unit.split color.split)
   681 qed
   682 
   683 lemma Pow_Set [code]:
   684   "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
   685 by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
   686 
   687 lemma product_Set [code]:
   688   "Product_Type.product (Set t1) (Set t2) = 
   689     fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
   690 proof -
   691   have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
   692   show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]  
   693     by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
   694 qed
   695 
   696 lemma Id_on_Set [code]:
   697   "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
   698 proof -
   699   have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
   700   then show ?thesis
   701     by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
   702 qed
   703 
   704 lemma Image_Set [code]:
   705   "(Set t) `` S = fold_keys (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) t {}"
   706 by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold])
   707 
   708 lemma trancl_set_ntrancl [code]:
   709   "trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)"
   710 by (simp add: finite_trancl_ntranl)
   711 
   712 lemma relcomp_Set[code]:
   713   "(Set t1) O (Set t2) = fold_keys 
   714     (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
   715 proof -
   716   interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
   717   have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
   718     by default (auto simp add: fun_eq_iff)
   719   show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
   720     by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
   721 qed
   722 
   723 lemma wf_set [code]:
   724   "wf (Set t) = acyclic (Set t)"
   725 by (simp add: wf_iff_acyclic_if_finite)
   726 
   727 lemma Min_fin_set_fold [code]:
   728   "Min (Set t) = 
   729   (if is_empty t
   730    then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t))
   731    else r_min_opt t)"
   732 proof -
   733   have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
   734   with finite_fold1_fold1_keys [OF *, folded Min_def]
   735   show ?thesis
   736     by (simp add: r_min_alt_def r_min_eq_r_min_opt [symmetric])  
   737 qed
   738 
   739 lemma Inf_fin_set_fold [code]:
   740   "Inf_fin (Set t) = Min (Set t)"
   741 by (simp add: inf_min Inf_fin_def Min_def)
   742 
   743 lemma Inf_Set_fold:
   744   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   745   shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
   746 proof -
   747   have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   748   then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   749     by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
   750   then show ?thesis 
   751     by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
   752 qed
   753 
   754 definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
   755 declare Inf'_def[symmetric, code_unfold]
   756 declare Inf_Set_fold[folded Inf'_def, code]
   757 
   758 lemma INFI_Set_fold [code]:
   759   "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
   760 proof -
   761   have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   762     by default (auto simp add: fun_eq_iff ac_simps)
   763   then show ?thesis
   764     by (auto simp: INF_fold_inf finite_fold_fold_keys)
   765 qed
   766 
   767 lemma Max_fin_set_fold [code]:
   768   "Max (Set t) = 
   769   (if is_empty t
   770    then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t))
   771    else r_max_opt t)"
   772 proof -
   773   have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
   774   with finite_fold1_fold1_keys [OF *, folded Max_def]
   775   show ?thesis
   776     by (simp add: r_max_alt_def r_max_eq_r_max_opt [symmetric])  
   777 qed
   778 
   779 lemma Sup_fin_set_fold [code]:
   780   "Sup_fin (Set t) = Max (Set t)"
   781 by (simp add: sup_max Sup_fin_def Max_def)
   782 
   783 lemma Sup_Set_fold:
   784   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   785   shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
   786 proof -
   787   have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   788   then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   789     by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
   790   then show ?thesis 
   791     by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
   792 qed
   793 
   794 definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
   795 declare Sup'_def[symmetric, code_unfold]
   796 declare Sup_Set_fold[folded Sup'_def, code]
   797 
   798 lemma SUPR_Set_fold [code]:
   799   "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
   800 proof -
   801   have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   802     by default (auto simp add: fun_eq_iff ac_simps)
   803   then show ?thesis
   804     by (auto simp: SUP_fold_sup finite_fold_fold_keys)
   805 qed
   806 
   807 lemma sorted_list_set[code]:
   808   "sorted_list_of_set (Set t) = keys t"
   809 by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
   810 
   811 lemma Bleast_code [code]:
   812  "Bleast (Set t) P = (case filter P (keys t) of
   813     x#xs \<Rightarrow> x |
   814     [] \<Rightarrow> abort_Bleast (Set t) P)"
   815 proof (cases "filter P (keys t)")
   816   case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
   817 next
   818   case (Cons x ys)
   819   have "(LEAST x. x \<in> Set t \<and> P x) = x"
   820   proof (rule Least_equality)
   821     show "x \<in> Set t \<and> P x" using Cons[symmetric]
   822       by(auto simp add: set_keys Cons_eq_filter_iff)
   823     next
   824       fix y assume "y : Set t \<and> P y"
   825       then show "x \<le> y" using Cons[symmetric]
   826         by(auto simp add: set_keys Cons_eq_filter_iff)
   827           (metis sorted_Cons sorted_append sorted_keys)
   828   qed
   829   thus ?thesis using Cons by (simp add: Bleast_def)
   830 qed
   831 
   832 
   833 hide_const (open) RBT_Set.Set RBT_Set.Coset
   834 
   835 end