src/HOL/Library/RBT_Set.thy
author kuncar
Tue Jan 15 12:13:27 2013 +0100 (2013-01-15)
changeset 50996 51ad7b4ac096
parent 49948 744934b818c7
child 51115 7dbd6832a689
permissions -rw-r--r--
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
     1 (*  Title:      HOL/Library/RBT_Set.thy
     2     Author:     Ondrej Kuncar
     3 *)
     4 
     5 header {* Implementation of sets using RBT trees *}
     6 
     7 theory RBT_Set
     8 imports RBT Product_ord
     9 begin
    10 
    11 (*
    12   Users should be aware that by including this file all code equations
    13   outside of List.thy using 'a list as an implenentation of sets cannot be
    14   used for code generation. If such equations are not needed, they can be
    15   deleted from the code generator. Otherwise, a user has to provide their 
    16   own equations using RBT trees. 
    17 *)
    18 
    19 section {* Definition of code datatype constructors *}
    20 
    21 definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
    22   where "Set t = {x . lookup t x = Some ()}"
    23 
    24 definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
    25   where [simp]: "Coset t = - Set t"
    26 
    27 
    28 section {* Deletion of already existing code equations *}
    29 
    30 lemma [code, code del]:
    31   "Set.empty = Set.empty" ..
    32 
    33 lemma [code, code del]:
    34   "Set.is_empty = Set.is_empty" ..
    35 
    36 lemma [code, code del]:
    37   "uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" ..
    38 
    39 lemma [code, code del]:
    40   "Set.member = Set.member" ..
    41 
    42 lemma [code, code del]:
    43   "Set.insert = Set.insert" ..
    44 
    45 lemma [code, code del]:
    46   "Set.remove = Set.remove" ..
    47 
    48 lemma [code, code del]:
    49   "UNIV = UNIV" ..
    50 
    51 lemma [code, code del]:
    52   "Set.filter = Set.filter" ..
    53 
    54 lemma [code, code del]:
    55   "image = image" ..
    56 
    57 lemma [code, code del]:
    58   "Set.subset_eq = Set.subset_eq" ..
    59 
    60 lemma [code, code del]:
    61   "Ball = Ball" ..
    62 
    63 lemma [code, code del]:
    64   "Bex = Bex" ..
    65 
    66 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   interpret ab_semigroup_idem_mult "(min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_min
   320     unfolding class.ab_semigroup_idem_mult_def by blast
   321   show ?thesis
   322     by (simp add: Min_eqI rbt_min_opt_is_min rbt_min_opt_in_set assms Min_def[symmetric]
   323       non_empty_rbt_keys fold1_set_fold[symmetric] rbt_min_def rbt_fold1_keys_def)
   324 qed
   325 
   326 (* maximum *)
   327 
   328 definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   329   where "rbt_max t = rbt_fold1_keys max t"
   330 
   331 lemma fold_max_triv:
   332   fixes k :: "_ :: linorder"
   333   shows "(\<forall>x\<in>set xs. x \<le> k) \<Longrightarrow> List.fold max xs k = k" 
   334 by (induct xs) (auto simp add: max_def)
   335 
   336 lemma fold_max_rev_eq:
   337   fixes xs :: "('a :: linorder) list"
   338   assumes "xs \<noteq> []"
   339   shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
   340 proof -
   341   interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
   342     unfolding class.ab_semigroup_idem_mult_def by blast
   343   show ?thesis
   344   using assms by (auto simp add: fold1_set_fold[symmetric])
   345 qed
   346 
   347 lemma rbt_max_simps:
   348   assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)" 
   349   shows "rbt_max (Branch c lt k v RBT_Impl.Empty) = k"
   350 proof -
   351   have "List.fold max (tl (rev(RBT_Impl.keys lt @ [k]))) (hd (rev(RBT_Impl.keys lt @ [k]))) = k"
   352     using assms by (auto intro!: fold_max_triv dest!: left_le_key is_rbt_rbt_sorted)
   353   then show ?thesis by (auto simp add: rbt_max_def rbt_fold1_keys_def fold_max_rev_eq)
   354 qed
   355 
   356 fun rbt_max_opt where
   357   "rbt_max_opt (Branch c lt k v RBT_Impl.Empty) = k" |
   358   "rbt_max_opt (Branch c lt k v (Branch rc rlc rk rv rrt)) = rbt_max_opt (Branch rc rlc rk rv rrt)"
   359 
   360 lemma rbt_max_opt_Branch:
   361   "t2 \<noteq> rbt.Empty \<Longrightarrow> rbt_max_opt (Branch c t1 k () t2) = rbt_max_opt t2" 
   362 by (cases t2) auto
   363 
   364 lemma rbt_max_opt_induct [case_names empty right_empty right_non_empty]:
   365   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   366   assumes "P rbt.Empty"
   367   assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   368   assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   369   shows "P t"
   370 using assms
   371   apply (induction t)
   372   apply simp
   373   apply (case_tac "t2 = rbt.Empty")
   374   apply simp_all
   375 done
   376 
   377 lemma rbt_max_opt_in_set: 
   378   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   379   assumes "t \<noteq> rbt.Empty"
   380   shows "rbt_max_opt t \<in> set (RBT_Impl.keys t)"
   381 using assms by (induction t rule: rbt_max_opt.induct) (auto)
   382 
   383 lemma rbt_max_opt_is_max:
   384   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   385   assumes "rbt_sorted t"
   386   assumes "t \<noteq> rbt.Empty"
   387   shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<le> rbt_max_opt t"
   388 using assms 
   389 proof (induction t rule: rbt_max_opt_induct)
   390   case empty
   391     then show ?case by simp
   392 next
   393   case right_empty
   394     then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
   395 next
   396   case (right_non_empty c t1 k v t2 y)
   397     then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
   398     with right_non_empty show ?case 
   399     proof(elim disjE)
   400       case goal1 then show ?case 
   401         by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
   402     next
   403       case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
   404     next 
   405       case goal3 show ?case
   406       proof -
   407         from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
   408         moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
   409         ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
   410       qed
   411     qed
   412 qed
   413 
   414 lemma rbt_max_eq_rbt_max_opt:
   415   assumes "t \<noteq> RBT_Impl.Empty"
   416   assumes "is_rbt t"
   417   shows "rbt_max t = rbt_max_opt t"
   418 proof -
   419   interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
   420     unfolding class.ab_semigroup_idem_mult_def by blast
   421   show ?thesis
   422     by (simp add: Max_eqI rbt_max_opt_is_max rbt_max_opt_in_set assms Max_def[symmetric]
   423       non_empty_rbt_keys fold1_set_fold[symmetric] rbt_max_def rbt_fold1_keys_def)
   424 qed
   425 
   426 
   427 (** abstract **)
   428 
   429 lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
   430   is rbt_fold1_keys by simp
   431 
   432 lemma fold1_keys_def_alt:
   433   "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
   434   by transfer (simp add: rbt_fold1_keys_def)
   435 
   436 lemma finite_fold1_fold1_keys:
   437   assumes "class.ab_semigroup_mult f"
   438   assumes "\<not> (is_empty t)"
   439   shows "Finite_Set.fold1 f (Set t) = fold1_keys f t"
   440 proof -
   441   interpret ab_semigroup_mult f by fact
   442   show ?thesis using assms 
   443     by (auto simp: fold1_keys_def_alt set_keys fold_def_alt fold1_distinct_set_fold non_empty_keys)
   444 qed
   445 
   446 (* minimum *)
   447 
   448 lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
   449 
   450 lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
   451 
   452 lemma r_min_alt_def: "r_min t = fold1_keys min t"
   453 by transfer (simp add: rbt_min_def)
   454 
   455 lemma r_min_eq_r_min_opt:
   456   assumes "\<not> (is_empty t)"
   457   shows "r_min t = r_min_opt t"
   458 using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
   459 
   460 lemma fold_keys_min_top_eq:
   461   fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
   462   assumes "\<not> (is_empty t)"
   463   shows "fold_keys min t top = fold1_keys min t"
   464 proof -
   465   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
   466     List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
   467     by (simp add: hd_Cons_tl[symmetric])
   468   { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
   469     have "List.fold min (x#xs) top = List.fold min xs x"
   470     by (simp add: inf_min[symmetric])
   471   } note ** = this
   472   show ?thesis using assms
   473     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   474     apply transfer 
   475     apply (case_tac t) 
   476     apply simp 
   477     apply (subst *)
   478     apply simp
   479     apply (subst **)
   480     apply simp
   481   done
   482 qed
   483 
   484 (* maximum *)
   485 
   486 lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
   487 
   488 lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
   489 
   490 lemma r_max_alt_def: "r_max t = fold1_keys max t"
   491 by transfer (simp add: rbt_max_def)
   492 
   493 lemma r_max_eq_r_max_opt:
   494   assumes "\<not> (is_empty t)"
   495   shows "r_max t = r_max_opt t"
   496 using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
   497 
   498 lemma fold_keys_max_bot_eq:
   499   fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
   500   assumes "\<not> (is_empty t)"
   501   shows "fold_keys max t bot = fold1_keys max t"
   502 proof -
   503   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
   504     List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
   505     by (simp add: hd_Cons_tl[symmetric])
   506   { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
   507     have "List.fold max (x#xs) bot = List.fold max xs x"
   508     by (simp add: sup_max[symmetric])
   509   } note ** = this
   510   show ?thesis using assms
   511     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   512     apply transfer 
   513     apply (case_tac t) 
   514     apply simp 
   515     apply (subst *)
   516     apply simp
   517     apply (subst **)
   518     apply simp
   519   done
   520 qed
   521 
   522 
   523 section {* Code equations *}
   524 
   525 code_datatype Set Coset
   526 
   527 declare set.simps[code]
   528 
   529 lemma empty_Set [code]:
   530   "Set.empty = Set RBT.empty"
   531 by (auto simp: Set_def)
   532 
   533 lemma UNIV_Coset [code]:
   534   "UNIV = Coset RBT.empty"
   535 by (auto simp: Set_def)
   536 
   537 lemma is_empty_Set [code]:
   538   "Set.is_empty (Set t) = RBT.is_empty t"
   539   unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1])
   540 
   541 lemma compl_code [code]:
   542   "- Set xs = Coset xs"
   543   "- Coset xs = Set xs"
   544 by (simp_all add: Set_def)
   545 
   546 lemma member_code [code]:
   547   "x \<in> (Set t) = (RBT.lookup t x = Some ())"
   548   "x \<in> (Coset t) = (RBT.lookup t x = None)"
   549 by (simp_all add: Set_def)
   550 
   551 lemma insert_code [code]:
   552   "Set.insert x (Set t) = Set (RBT.insert x () t)"
   553   "Set.insert x (Coset t) = Coset (RBT.delete x t)"
   554 by (auto simp: Set_def)
   555 
   556 lemma remove_code [code]:
   557   "Set.remove x (Set t) = Set (RBT.delete x t)"
   558   "Set.remove x (Coset t) = Coset (RBT.insert x () t)"
   559 by (auto simp: Set_def)
   560 
   561 lemma union_Set [code]:
   562   "Set t \<union> A = fold_keys Set.insert t A"
   563 proof -
   564   interpret comp_fun_idem Set.insert
   565     by (fact comp_fun_idem_insert)
   566   from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`]
   567   show ?thesis by (auto simp add: union_fold_insert)
   568 qed
   569 
   570 lemma inter_Set [code]:
   571   "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
   572 by (simp add: inter_Set_filter Set_filter_rbt_filter)
   573 
   574 lemma minus_Set [code]:
   575   "A - Set t = fold_keys Set.remove t A"
   576 proof -
   577   interpret comp_fun_idem Set.remove
   578     by (fact comp_fun_idem_remove)
   579   from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`]
   580   show ?thesis by (auto simp add: minus_fold_remove)
   581 qed
   582 
   583 lemma union_Coset [code]:
   584   "Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
   585 proof -
   586   have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
   587   show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
   588 qed
   589  
   590 lemma union_Set_Set [code]:
   591   "Set t1 \<union> Set t2 = Set (union t1 t2)"
   592 by (auto simp add: lookup_union map_add_Some_iff Set_def)
   593 
   594 lemma inter_Coset [code]:
   595   "A \<inter> Coset t = fold_keys Set.remove t A"
   596 by (simp add: Diff_eq [symmetric] minus_Set)
   597 
   598 lemma inter_Coset_Coset [code]:
   599   "Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
   600 by (auto simp add: lookup_union map_add_Some_iff Set_def)
   601 
   602 lemma minus_Coset [code]:
   603   "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
   604 by (simp add: inter_Set[simplified Int_commute])
   605 
   606 lemma filter_Set [code]:
   607   "Set.filter P (Set t) = (rbt_filter P t)"
   608 by (auto simp add: Set_filter_rbt_filter)
   609 
   610 lemma image_Set [code]:
   611   "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
   612 proof -
   613   have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
   614   then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
   615 qed
   616 
   617 lemma Ball_Set [code]:
   618   "Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   619 proof -
   620   have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
   621   then show ?thesis 
   622     by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
   623 qed
   624 
   625 lemma Bex_Set [code]:
   626   "Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   627 proof -
   628   have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
   629   then show ?thesis 
   630     by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
   631 qed
   632 
   633 lemma subset_code [code]:
   634   "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)"
   635   "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
   636 by auto
   637 
   638 definition non_empty_trees where [code del]: "non_empty_trees t1 t2 \<longleftrightarrow> Coset t1 \<le> Set t2"
   639 
   640 code_abort non_empty_trees
   641 
   642 lemma subset_Coset_empty_Set_empty [code]:
   643   "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of 
   644     (rbt.Empty, rbt.Empty) => False |
   645     (_, _) => non_empty_trees t1 t2)"
   646 proof -
   647   have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
   648     by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
   649   have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
   650   show ?thesis  
   651     by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split simp: non_empty_trees_def)
   652 qed
   653 
   654 text {* A frequent case – avoid intermediate sets *}
   655 lemma [code_unfold]:
   656   "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   657 by (simp add: subset_code Ball_Set)
   658 
   659 lemma card_Set [code]:
   660   "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
   661 by (auto simp add: card_def fold_image_def intro!: finite_fold_fold_keys) (default, simp) 
   662 
   663 lemma setsum_Set [code]:
   664   "setsum f (Set xs) = fold_keys (plus o f) xs 0"
   665 proof -
   666   have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
   667   then show ?thesis 
   668     by (auto simp add: setsum_def fold_image_def finite_fold_fold_keys o_def)
   669 qed
   670 
   671 definition not_a_singleton_tree  where [code del]: "not_a_singleton_tree x y = x y"
   672 
   673 code_abort not_a_singleton_tree
   674 
   675 lemma the_elem_set [code]:
   676   fixes t :: "('a :: linorder, unit) rbt"
   677   shows "the_elem (Set t) = (case impl_of t of 
   678     (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
   679     | _ \<Rightarrow> not_a_singleton_tree the_elem (Set t))"
   680 proof -
   681   {
   682     fix x :: "'a :: linorder"
   683     let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" 
   684     have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
   685     then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
   686 
   687     have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
   688       by (subst(asm) RBT_inverse[symmetric, OF *])
   689         (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
   690   }
   691   then show ?thesis unfolding not_a_singleton_tree_def
   692     by(auto split: rbt.split unit.split color.split)
   693 qed
   694 
   695 lemma Pow_Set [code]:
   696   "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
   697 by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
   698 
   699 lemma product_Set [code]:
   700   "Product_Type.product (Set t1) (Set t2) = 
   701     fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
   702 proof -
   703   have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
   704   show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]  
   705     by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
   706 qed
   707 
   708 lemma Id_on_Set [code]:
   709   "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
   710 proof -
   711   have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
   712   then show ?thesis
   713     by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
   714 qed
   715 
   716 lemma Image_Set [code]:
   717   "(Set t) `` S = fold_keys (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) t {}"
   718 by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold])
   719 
   720 lemma trancl_set_ntrancl [code]:
   721   "trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)"
   722 by (simp add: finite_trancl_ntranl)
   723 
   724 lemma relcomp_Set[code]:
   725   "(Set t1) O (Set t2) = fold_keys 
   726     (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
   727 proof -
   728   interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
   729   have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
   730     by default (auto simp add: fun_eq_iff)
   731   show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
   732     by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
   733 qed
   734 
   735 lemma wf_set [code]:
   736   "wf (Set t) = acyclic (Set t)"
   737 by (simp add: wf_iff_acyclic_if_finite)
   738 
   739 definition not_non_empty_tree  where [code del]: "not_non_empty_tree x y = x y"
   740 
   741 code_abort not_non_empty_tree
   742 
   743 lemma Min_fin_set_fold [code]:
   744   "Min (Set t) = (if is_empty t then not_non_empty_tree Min (Set t) else r_min_opt t)"
   745 proof -
   746   have *:"(class.ab_semigroup_mult (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_min
   747     unfolding class.ab_semigroup_idem_mult_def by blast
   748   show ?thesis
   749     by (auto simp add: Min_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_min_alt_def 
   750       r_min_eq_r_min_opt[symmetric])  
   751 qed
   752 
   753 lemma Inf_fin_set_fold [code]:
   754   "Inf_fin (Set t) = Min (Set t)"
   755 by (simp add: inf_min Inf_fin_def Min_def)
   756 
   757 lemma Inf_Set_fold:
   758   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   759   shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
   760 proof -
   761   have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   762   then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   763     by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
   764   then show ?thesis 
   765     by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
   766 qed
   767 
   768 definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
   769 declare Inf'_def[symmetric, code_unfold]
   770 declare Inf_Set_fold[folded Inf'_def, code]
   771 
   772 lemma INFI_Set_fold [code]:
   773   "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
   774 proof -
   775   have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   776     by default (auto simp add: fun_eq_iff ac_simps)
   777   then show ?thesis
   778     by (auto simp: INF_fold_inf finite_fold_fold_keys)
   779 qed
   780 
   781 lemma Max_fin_set_fold [code]:
   782   "Max (Set t) = (if is_empty t then not_non_empty_tree Max (Set t) else r_max_opt t)"
   783 proof -
   784   have *:"(class.ab_semigroup_mult (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_max
   785     unfolding class.ab_semigroup_idem_mult_def by blast
   786   show ?thesis
   787     by (auto simp add: Max_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_max_alt_def 
   788       r_max_eq_r_max_opt[symmetric])  
   789 qed
   790 
   791 lemma Sup_fin_set_fold [code]:
   792   "Sup_fin (Set t) = Max (Set t)"
   793 by (simp add: sup_max Sup_fin_def Max_def)
   794 
   795 lemma Sup_Set_fold:
   796   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   797   shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
   798 proof -
   799   have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   800   then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   801     by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
   802   then show ?thesis 
   803     by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
   804 qed
   805 
   806 definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
   807 declare Sup'_def[symmetric, code_unfold]
   808 declare Sup_Set_fold[folded Sup'_def, code]
   809 
   810 lemma SUPR_Set_fold [code]:
   811   "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
   812 proof -
   813   have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   814     by default (auto simp add: fun_eq_iff ac_simps)
   815   then show ?thesis
   816     by (auto simp: SUP_fold_sup finite_fold_fold_keys)
   817 qed
   818 
   819 lemma sorted_list_set[code]:
   820   "sorted_list_of_set (Set t) = keys t"
   821 by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
   822 
   823 hide_const (open) RBT_Set.Set RBT_Set.Coset
   824 
   825 end