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

header {* Implementation of mappings with Red-Black Trees *}

(*<*)
theory RBT_Mapping
imports RBT Mapping
begin

subsection {* Implementation of mappings *}

lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is lookup .

code_datatype Mapping

lemma lookup_Mapping [simp, code]:
  "Mapping.lookup (Mapping t) = lookup t"
   by (transfer fixing: t) rule

lemma empty_Mapping [code]: "Mapping.empty = Mapping empty"
proof -
  note RBT.empty.transfer[transfer_rule del]
  show ?thesis by transfer simp
qed

lemma is_empty_Mapping [code]:
  "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
  unfolding is_empty_def by (transfer fixing: t) simp

lemma insert_Mapping [code]:
  "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
  by (transfer fixing: t) simp

lemma delete_Mapping [code]:
  "Mapping.delete k (Mapping t) = Mapping (delete k t)"
  by (transfer fixing: t) simp

lemma map_entry_Mapping [code]:
  "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
by (transfer fixing: t, case_tac "lookup t k") auto

lemma keys_Mapping [code]:
  "Mapping.keys (Mapping t) = set (keys t)"
by (transfer fixing: t) (simp add: lookup_keys)

lemma ordered_keys_Mapping [code]:
  "Mapping.ordered_keys (Mapping t) = keys t"
unfolding ordered_keys_def 
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique)

lemma Mapping_size_card_keys: (*FIXME*)
  "Mapping.size m = card (Mapping.keys m)"
unfolding size_def by transfer simp

lemma size_Mapping [code]:
  "Mapping.size (Mapping t) = length (keys t)"
unfolding size_def
by (transfer fixing: t) (simp add: lookup_keys distinct_card)

context
  notes RBT.bulkload.transfer[transfer_rule del]
begin
  lemma tabulate_Mapping [code]:
    "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
  by transfer (simp add: map_of_map_restrict)
  
  lemma bulkload_Mapping [code]:
    "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
  by transfer (simp add: map_of_map_restrict fun_eq_iff)<commit_msg>drop a workaround because of 8739f8abbecb<commit_after>(*  Title:      HOL/Library/RBT_Mapping.thy
    Author:     <NAME> and <NAME>
*)

header {* Implementation of mappings with Red-Black Trees *}

(*<*)
theory RBT_Mapping
imports RBT Mapping
begin

subsection {* Implementation of mappings *}

lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is lookup .

code_datatype Mapping

lemma lookup_Mapping [simp, code]:
  "Mapping.lookup (Mapping t) = lookup t"
   by (transfer fixing: t) rule

lemma empty_Mapping [code]: "Mapping.empty = Mapping empty"
proof -
  note RBT.empty.transfer[transfer_rule del]
  show ?thesis by transfer simp
qed

lemma is_empty_Mapping [code]:
  "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
  unfolding is_empty_def by (transfer fixing: t) simp

lemma insert_Mapping [code]:
  "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
  by (transfer fixing: t) simp

lemma delete_Mapping [code]:
  "Mapping.delete k (Mapping t) = Mapping (delete k t)"
  by (transfer fixing: t) simp

lemma map_entry_Mapping [code]:
  "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
  apply (transfer fixing: t) by (case_tac "lookup t k") auto

lemma keys_Mapping [code]:
  "Mapping.keys (Mapping t) = set (keys t)"
by (transfer fixing: t) (simp add: lookup_keys)

lemma ordered_keys_Mapping [code]:
  "Mapping.ordered_keys (Mapping t) = keys t"
unfolding ordered_keys_def 
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique)

lemma Mapping_size_card_keys: (*FIXME*)
  "Mapping.size m = card (Mapping.keys m)"
unfolding size_def by transfer simp

lemma size_Mapping [code]:
  "Mapping.size (Mapping t) = length (keys t)"
unfolding size_def
by (transfer fixing: t) (simp add: lookup_keys distinct_card)

context
  notes RBT.bulkload.transfer[transfer_rule del]
begin
  lemma tabulate_Mapping [code]:
    "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
  by transfer (simp add: map_of_map_restrict)
  
  lemma bulkload_Mapping [code]:
    "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
  by transfer (simp add: map_of_map_restrict fun_eq_iff)
{'fraction_non_alphanumeric': 0.11525499887665692, 'fraction_numerical': 0.0015726802965625702, 'mean_word_length': 4.671337579617834, 'pattern_counts': {'":': 0, '<': 21, '<?xml version=': 0, '>': 17, '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': '5085747', 'n_tokens_mistral': 1575, 'n_tokens_neox': 1537, 'n_words': 507}