<commit_before>(*  Title:      HOL/Library/RBT_Set.thy
    Author:     <NAME>
*)

header {* Implementation of sets using RBT trees *}

theory RBT_Set
imports RBT Product_ord
begin

(*
  Users should be aware that by including this file all code equations
  outside of List.thy using 'a list as an implenentation of sets cannot be
  used for code generation. If such equations are not needed, they can be
  deleted from the code generator. Otherwise, a user has to provide their 
  own equations using RBT trees. 
*)

section {* Definition of code datatype constructors *}

definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
  where "Set t = {x . lookup t x = Some ()}"

definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
  where [simp]: "Coset t = - Set t"


section {* Deletion of already existing code equations *}

lemma [code, code del]:
  "Set.empty = Set.empty" ..

lemma [code, code del]:
  "Set.is_empty = Set.is_empty" ..

lemma [code, code del]:
  "uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" ..

lemma [code, code del]:
  "Set.member = Set.member" ..

lemma [code, code del]:
  "Set.insert = Set.insert" ..

lemma [code, code del]:
  "Set.remove = Set.remove" ..

lemma [code, code del]:
  "UNIV = UNIV" ..

lemma [code, code del]:
  "Set.filter = Set.filter" ..

lemma [code, code del]:
  "image = image" ..

lemma [code, code del]:
  "Set.subset_eq = Set.subset_eq" ..

lemma [code, code del]:
  "Ball = Ball" ..

lemma [code, code del]:
  "Bex = Bex" ..

lemma [code, code del]:
  "Set.union = Set.union" ..

lemma [code, code del]:
  "minus_set_inst.minus_set = minus_set_inst.minus_set" ..

lemma [code, code del]:
  "Set.inter = Set.inter" ..

lemma [code, code del]:
  "card = card" ..

lemma [code, code del]:
  "the_elem = the_elem" ..

lemma [code, code del]:
  "Pow = Pow" ..

lemma [code, code del]:
  "setsum = setsum" ..

lemma [code, code del]:
  "Product_Type.product = Product_Type.product"  ..

lemma [code, code del]:
  "Id_on = Id_on" ..

lemma [code, code del]:
  "Image = Image" ..

lemma [code, code del]:
  "trancl = trancl" ..

lemma [code, code del]:
  "relcomp = relcomp" ..

lemma [code, code del]:
  "wf = wf" ..

lemma [code, code del]:
  "Min = Min" ..

lemma [code, code del]:
  "Inf_fin = Inf_fin" ..

lemma [code, code del]:
  "INFI = INFI" ..

lemma [code, code del]:
  "Max = Max" ..

lemma [code, code del]:
  "Sup_fin = Sup_fin" ..

lemma [code, code del]:
  "SUPR = SUPR" ..

lemma [code, code del]:
  "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..

lemma [code, code del]:
  "(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" ..

lemma [code, code del]:
  "sorted_list_of_set = sorted_list_of_set" ..

lemma [code, code del]: 
  "List.map_project = List.map_project" ..

section {* Lemmas *}


subsection {* Auxiliary lemmas *}

lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
by (auto simp: not_Some_eq[THEN iffD1])

lemma finite_Set [simp, intro!]: "finite (Set x)"
proof -
  have "Set x = dom (lookup x)" by (auto simp: Set_def)
  then show ?thesis by simp
qed

lemma set_keys: "Set t = set(keys t)"
proof -
 have "\<And>k. ((k, ()) \<in> set (entries t)) = (k \<in> set (keys t))" 
    by (simp add: keys_entries)
  then show ?thesis by (auto simp: lookup_in_tree Set_def)
qed

subsection {* fold and filter *}

lemma finite_fold_rbt_fold_eq:
  assumes "comp_fun_commute f" 
  shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
proof -
  have *: "remdups (entries t) = entries t"
    using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
  show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
qed

definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b" 
  where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"

lemma fold_keys_def_alt:
  "fold_keys f t s = List.fold f (keys t) s"
by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)

lemma finite_fold_fold_keys:
  assumes "comp_fun_commute f"
  shows "Finite_Set.fold f A (Set t) = fold_keys f t A"
using assms
proof -
  interpret comp_fun_commute f by fact<commit_msg>tuned proofs<commit_after>(*  Title:      HOL/Library/RBT_Set.thy
    Author:     <NAME>
*)

header {* Implementation of sets using RBT trees *}

theory RBT_Set
imports RBT Product_ord
begin

(*
  Users should be aware that by including this file all code equations
  outside of List.thy using 'a list as an implenentation of sets cannot be
  used for code generation. If such equations are not needed, they can be
  deleted from the code generator. Otherwise, a user has to provide their 
  own equations using RBT trees. 
*)

section {* Definition of code datatype constructors *}

definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
  where "Set t = {x . lookup t x = Some ()}"

definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
  where [simp]: "Coset t = - Set t"


section {* Deletion of already existing code equations *}

lemma [code, code del]:
  "Set.empty = Set.empty" ..

lemma [code, code del]:
  "Set.is_empty = Set.is_empty" ..

lemma [code, code del]:
  "uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" ..

lemma [code, code del]:
  "Set.member = Set.member" ..

lemma [code, code del]:
  "Set.insert = Set.insert" ..

lemma [code, code del]:
  "Set.remove = Set.remove" ..

lemma [code, code del]:
  "UNIV = UNIV" ..

lemma [code, code del]:
  "Set.filter = Set.filter" ..

lemma [code, code del]:
  "image = image" ..

lemma [code, code del]:
  "Set.subset_eq = Set.subset_eq" ..

lemma [code, code del]:
  "Ball = Ball" ..

lemma [code, code del]:
  "Bex = Bex" ..

lemma [code, code del]:
  "Set.union = Set.union" ..

lemma [code, code del]:
  "minus_set_inst.minus_set = minus_set_inst.minus_set" ..

lemma [code, code del]:
  "Set.inter = Set.inter" ..

lemma [code, code del]:
  "card = card" ..

lemma [code, code del]:
  "the_elem = the_elem" ..

lemma [code, code del]:
  "Pow = Pow" ..

lemma [code, code del]:
  "setsum = setsum" ..

lemma [code, code del]:
  "Product_Type.product = Product_Type.product"  ..

lemma [code, code del]:
  "Id_on = Id_on" ..

lemma [code, code del]:
  "Image = Image" ..

lemma [code, code del]:
  "trancl = trancl" ..

lemma [code, code del]:
  "relcomp = relcomp" ..

lemma [code, code del]:
  "wf = wf" ..

lemma [code, code del]:
  "Min = Min" ..

lemma [code, code del]:
  "Inf_fin = Inf_fin" ..

lemma [code, code del]:
  "INFI = INFI" ..

lemma [code, code del]:
  "Max = Max" ..

lemma [code, code del]:
  "Sup_fin = Sup_fin" ..

lemma [code, code del]:
  "SUPR = SUPR" ..

lemma [code, code del]:
  "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..

lemma [code, code del]:
  "(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" ..

lemma [code, code del]:
  "sorted_list_of_set = sorted_list_of_set" ..

lemma [code, code del]: 
  "List.map_project = List.map_project" ..

section {* Lemmas *}


subsection {* Auxiliary lemmas *}

lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
by (auto simp: not_Some_eq[THEN iffD1])

lemma Set_set_keys: "Set x = dom (lookup x)" 
by (auto simp: Set_def)

lemma finite_Set [simp, intro!]: "finite (Set x)"
by (simp add: Set_set_keys)

lemma set_keys: "Set t = set(keys t)"
by (simp add: Set_set_keys lookup_keys)

subsection {* fold and filter *}

lemma finite_fold_rbt_fold_eq:
  assumes "comp_fun_commute f" 
  shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
proof -
  have *: "remdups (entries t) = entries t"
    using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
  show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
qed

definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b" 
  where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"

lemma fold_keys_def_alt:
  "fold_keys f t s = List.fold f (keys t) s"
by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)

lemma finite_fold_fold_keys:
  assumes "comp_fun_commute f"
  shows "Finite_Set.fold f A (Set t) = fold_keys f t A"
using assms
proof -
  interpret comp_fun_commute f by fact
{'fraction_non_alphanumeric': 0.1458383019317911, 'fraction_numerical': 0.00023849272597185786, 'mean_word_length': 3.4258575197889183, 'pattern_counts': {'":': 0, '<': 36, '<?xml version=': 0, '>': 36, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6245842', 'n_tokens_mistral': 3218, 'n_tokens_neox': 3134, 'n_words': 1033}