Theory RBT_Mapping2

(*  Title:      Containers/RBT_Mapping2.thy
    Author:     Andreas Lochbihler, KIT *)

theory RBT_Mapping2
imports
  Collection_Order
  RBT_ext
  Deriving.RBT_Comparator_Impl
begin

section ‹Mappings implemented by red-black trees›

lemma distinct_map_filterI: "distinct (map f xs) ⟹ distinct (map f (filter P xs))"
by(induct xs) auto

lemma map_of_filter_apply:
  "distinct (map fst xs)
  ⟹ map_of (filter P xs) k = 
  (case map_of xs k of None ⇒ None | Some v ⇒ if P (k, v) then Some v else None)"
by(induct xs)(auto simp add: map_of_eq_None_iff split: option.split)

subsection ‹Type definition›

typedef (overloaded) ('a, 'b) mapping_rbt
  = "{t :: ('a :: ccompare, 'b) RBT_Impl.rbt. ord.is_rbt cless t ∨ ID CCOMPARE('a) = None}"
  morphisms impl_of Mapping_RBT'
proof
  show "RBT_Impl.Empty ∈ ?mapping_rbt" by(simp add: ord.Empty_is_rbt)
qed

definition Mapping_RBT :: "('a :: ccompare, 'b) rbt ⇒ ('a, 'b) mapping_rbt"
where
  "Mapping_RBT t = Mapping_RBT'
  (if ord.is_rbt cless t ∨ ID CCOMPARE('a) = None then t
   else RBT_Impl.fold (ord.rbt_insert cless) t rbt.Empty)"

lemma Mapping_RBT_inverse:
  fixes y :: "('a :: ccompare, 'b) rbt"
  assumes "y ∈ {t. ord.is_rbt cless t ∨ ID CCOMPARE('a) = None}"
  shows "impl_of (Mapping_RBT y) = y"
using assms by(auto simp add: Mapping_RBT_def Mapping_RBT'_inverse)

lemma impl_of_inverse: "Mapping_RBT (impl_of t) = t"
by(cases t)(auto simp add: Mapping_RBT'_inverse Mapping_RBT_def)

lemma type_definition_mapping_rbt': 
  "type_definition impl_of Mapping_RBT 
    {t :: ('a, 'b) rbt. ord.is_rbt cless t ∨ ID CCOMPARE('a :: ccompare) = None}"
by unfold_locales(rule mapping_rbt.impl_of impl_of_inverse Mapping_RBT_inverse)+

lemmas Mapping_RBT_cases[cases type: mapping_rbt] = 
  type_definition.Abs_cases[OF type_definition_mapping_rbt'] 
  and Mapping_RBT_induct[induct type: mapping_rbt] =
  type_definition.Abs_induct[OF type_definition_mapping_rbt'] and
  Mapping_RBT_inject = type_definition.Abs_inject[OF type_definition_mapping_rbt']

lemma rbt_eq_iff:
  "t1 = t2 ⟷ impl_of t1 = impl_of t2"
  by (simp add: impl_of_inject)

lemma rbt_eqI:
  "impl_of t1 = impl_of t2 ⟹ t1 = t2"
  by (simp add: rbt_eq_iff)

lemma Mapping_RBT_impl_of [simp]:
  "Mapping_RBT (impl_of t) = t"
  by (simp add: impl_of_inverse)

subsection ‹Operations›

setup_lifting type_definition_mapping_rbt'

context fixes dummy :: "'a :: ccompare" begin

lift_definition lookup :: "('a, 'b) mapping_rbt ⇒ 'a ⇀ 'b" is "rbt_comp_lookup ccomp" .

lift_definition empty :: "('a, 'b) mapping_rbt" is "RBT_Impl.Empty"
by(simp add: ord.Empty_is_rbt)

lift_definition insert :: "'a ⇒ 'b ⇒ ('a, 'b) mapping_rbt ⇒ ('a, 'b) mapping_rbt" is
  "rbt_comp_insert ccomp"
by(auto 4 3 intro: linorder.rbt_insert_is_rbt ID_ccompare simp: rbt_comp_insert[OF ID_ccompare'])

lift_definition delete :: "'a ⇒ ('a, 'b) mapping_rbt ⇒ ('a, 'b) mapping_rbt" is
  "rbt_comp_delete ccomp"
by(auto 4 3 intro: linorder.rbt_delete_is_rbt ID_ccompare simp: rbt_comp_delete[OF ID_ccompare'])

lift_definition bulkload :: "('a × 'b) list ⇒ ('a, 'b) mapping_rbt" is
  "rbt_comp_bulkload ccomp"
by(auto 4 3 intro: linorder.rbt_bulkload_is_rbt ID_ccompare simp: rbt_comp_bulkload[OF ID_ccompare'])

lift_definition map_entry :: "'a ⇒ ('b ⇒ 'b) ⇒ ('a, 'b) mapping_rbt ⇒ ('a, 'b) mapping_rbt" is
  "rbt_comp_map_entry ccomp"
by(auto simp: ord.rbt_map_entry_is_rbt rbt_comp_map_entry[OF ID_ccompare'])

lift_definition map :: "('a ⇒ 'b ⇒ 'c) ⇒ ('a, 'b) mapping_rbt ⇒ ('a, 'c) mapping_rbt" is "RBT_Impl.map"
by(simp add: ord.map_is_rbt)

lift_definition entries :: "('a, 'b) mapping_rbt ⇒ ('a × 'b) list" is "RBT_Impl.entries" .

lift_definition keys :: "('a, 'b) mapping_rbt ⇒ 'a set" is "set ∘ RBT_Impl.keys" .

lift_definition fold :: "('a ⇒ 'b ⇒ 'c ⇒ 'c) ⇒ ('a, 'b) mapping_rbt ⇒ 'c ⇒ 'c" is "RBT_Impl.fold" .

lift_definition is_empty :: "('a, 'b) mapping_rbt ⇒ bool" is "case_rbt True (λ_ _ _ _ _. False)" .

lift_definition filter :: "('a × 'b ⇒ bool) ⇒ ('a, 'b) mapping_rbt ⇒ ('a, 'b) mapping_rbt" is
  "λP t. rbtreeify (List.filter P (RBT_Impl.entries t))"
by(auto intro!: linorder.is_rbt_rbtreeify ID_ccompare linorder.sorted_filter linorder.rbt_sorted_entries ord.is_rbt_rbt_sorted linorder.distinct_entries distinct_map_filterI simp add: filter_map[symmetric])

lift_definition join ::
  "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a, 'b) mapping_rbt ⇒ ('a, 'b) mapping_rbt ⇒ ('a, 'b) mapping_rbt"
is "rbt_comp_union_with_key ccomp"
by(auto 4 3 intro: linorder.is_rbt_rbt_unionwk ID_ccompare simp: rbt_comp_union_with_key[OF ID_ccompare'])

lift_definition meet ::
  "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a, 'b) mapping_rbt ⇒ ('a, 'b) mapping_rbt ⇒ ('a, 'b) mapping_rbt" 
is "rbt_comp_inter_with_key ccomp"
by(auto 4 3 intro: linorder.rbt_interwk_is_rbt ID_ccompare ord.is_rbt_rbt_sorted simp: rbt_comp_inter_with_key[OF ID_ccompare'])

lift_definition all :: "('a ⇒ 'b ⇒ bool) ⇒ ('a, 'b) mapping_rbt ⇒ bool" 
is "RBT_Impl_rbt_all" .

lift_definition ex :: "('a ⇒ 'b ⇒ bool) ⇒ ('a, 'b) mapping_rbt ⇒ bool"
is "RBT_Impl_rbt_ex" .

lift_definition product ::
  "('a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e) ⇒ ('a, 'b) mapping_rbt
  ⇒ ('c :: ccompare, 'd) mapping_rbt ⇒ ('a × 'c, 'e) mapping_rbt"
is "rbt_product"
  by (fastforce intro: is_rbt_rbt_product ID_ccompare simp add: lt_of_comp_less_prod ccompare_prod_def ID_Some ID_None split: option.split_asm)

lift_definition diag ::
  "('a, 'b) mapping_rbt ⇒ ('a × 'a, 'b) mapping_rbt"
is "RBT_Impl_diag"
by(auto simp add: lt_of_comp_less_prod ccompare_prod_def ID_Some ID_None is_rbt_RBT_Impl_diag split: option.split_asm)

lift_definition init :: "('a, 'b) mapping_rbt ⇒ ('a, 'b, 'c) rbt_generator_state"
is "rbt_init" .

end

subsection ‹Properties›

lemma unfoldr_rbt_entries_generator:
  "list.unfoldr rbt_entries_generator (init t) = entries t"
  by transfer(simp add: unfoldr_rbt_entries_generator)

lemma lookup_RBT:
  "ord.is_rbt cless t ⟹
  lookup (Mapping_RBT t) = rbt_comp_lookup ccomp t"
by(simp add: lookup_def Mapping_RBT_inverse)

lemma lookup_impl_of:
  "rbt_comp_lookup ccomp (impl_of t) = lookup t"
by(transfer) simp

lemma entries_impl_of:
  "RBT_Impl.entries (impl_of t) = entries t"
by transfer simp

lemma keys_impl_of:
  "set (RBT_Impl.keys (impl_of t)) = keys t"
  by (simp add: keys_def)

lemma lookup_empty [simp]:
  "lookup empty = Map.empty"
by transfer (simp add: fun_eq_iff ord.rbt_lookup.simps)

lemma fold_conv_fold:
  "fold f t = List.fold (case_prod f) (entries t)"
by transfer(simp add: RBT_Impl.fold_def)

lemma is_empty_empty [simp]:
  "is_empty t ⟷ t = empty"
by transfer (simp split: rbt.split)

context assumes ID_ccompare_neq_None: "ID CCOMPARE('a :: ccompare) ≠ None"
begin

lemma mapping_linorder: "class.linorder (cless_eq :: 'a ⇒ 'a ⇒ bool) cless"
using ID_ccompare_neq_None by(clarsimp)(rule ID_ccompare)

lemma mapping_comparator: "comparator (ccomp :: 'a comparator)"
using ID_ccompare_neq_None by(clarsimp)(rule ID_ccompare')

lemmas rbt_comp[simp] = rbt_comp_simps[OF mapping_comparator]

lemma is_rbt_impl_of [simp, intro]:
  fixes t :: "('a, 'b) mapping_rbt"
  shows "ord.is_rbt cless (impl_of t)"
using ID_ccompare_neq_None impl_of [of t] by auto

lemma lookup_insert [simp]:
  "lookup (insert (k :: 'a) v t) = (lookup t)(k ↦ v)"
by transfer (simp add: ID_ccompare_neq_None 
  linorder.rbt_lookup_rbt_insert[OF mapping_linorder])

lemma lookup_delete [simp]:
  "lookup (delete (k :: 'a) t) = (lookup t)(k := None)"
by transfer(simp add: ID_ccompare_neq_None linorder.rbt_lookup_rbt_delete[OF mapping_linorder] restrict_complement_singleton_eq)

lemma map_of_entries [simp]:
  "map_of (entries (t :: ('a, 'b) mapping_rbt)) = lookup t"
by transfer(simp add: ID_ccompare_neq_None linorder.map_of_entries[OF mapping_linorder] ord.is_rbt_rbt_sorted)

lemma entries_lookup:
  "entries (t1 :: ('a, 'b) mapping_rbt) = entries t2 ⟷ lookup t1 = lookup t2"
by transfer(simp add: ID_ccompare_neq_None linorder.entries_rbt_lookup[OF mapping_linorder] ord.is_rbt_rbt_sorted)

lemma lookup_bulkload [simp]:
  "lookup (bulkload xs) = map_of (xs :: ('a × 'b) list)"
by transfer(simp add: linorder.rbt_lookup_rbt_bulkload[OF mapping_linorder])

lemma lookup_map_entry [simp]:
  "lookup (map_entry (k :: 'a) f t) = (lookup t)(k := map_option f (lookup t k))"
by transfer(simp add: ID_ccompare_neq_None linorder.rbt_lookup_rbt_map_entry[OF mapping_linorder])

lemma lookup_map [simp]:
  "lookup (map f t) (k :: 'a) = map_option (f k) (lookup t k)"
by transfer(simp add: linorder.rbt_lookup_map[OF mapping_linorder])

lemma RBT_lookup_empty [simp]:
  "ord.rbt_lookup cless (t :: ('a, 'b) RBT_Impl.rbt) = Map.empty ⟷ t = RBT_Impl.Empty"
proof -
  interpret linorder "cless_eq :: 'a ⇒ 'a ⇒ bool" cless by(rule mapping_linorder)
  show ?thesis by(cases t)(auto simp add: fun_eq_iff)
qed

lemma lookup_empty_empty [simp]:
  "lookup t = Map.empty ⟷ (t :: ('a, 'b) mapping_rbt) = empty"
by transfer simp

lemma finite_dom_lookup [simp]: "finite (dom (lookup (t :: ('a, 'b) mapping_rbt)))"
by transfer(auto simp add: linorder.finite_dom_rbt_lookup[OF mapping_linorder])

lemma card_com_lookup [unfolded length_map, simp]:
  "card (dom (lookup (t :: ('a, 'b) mapping_rbt))) = length (List.map fst (entries t))"
by transfer(auto simp add: linorder.rbt_lookup_keys[OF mapping_linorder] linorder.distinct_entries[OF mapping_linorder] RBT_Impl.keys_def ord.is_rbt_rbt_sorted ID_ccompare_neq_None List.card_set simp del: set_map length_map)

lemma lookup_join:
  "lookup (join f (t1 :: ('a, 'b) mapping_rbt) t2) =
  (λk. case lookup t1 k of None ⇒ lookup t2 k | Some v1 ⇒ Some (case lookup t2 k of None ⇒ v1 | Some v2 ⇒ f k v1 v2))"
by transfer(auto simp add: fun_eq_iff linorder.rbt_lookup_rbt_unionwk[OF mapping_linorder] ord.is_rbt_rbt_sorted ID_ccompare_neq_None split: option.splits)

lemma lookup_meet:
  "lookup (meet f (t1 :: ('a, 'b) mapping_rbt) t2) =
  (λk. case lookup t1 k of None ⇒ None | Some v1 ⇒ case lookup t2 k of None ⇒ None | Some v2 ⇒ Some (f k v1 v2))"
by transfer(auto simp add: fun_eq_iff linorder.rbt_lookup_rbt_interwk[OF mapping_linorder] ord.is_rbt_rbt_sorted ID_ccompare_neq_None split: option.splits)

lemma lookup_filter [simp]:
  "lookup (filter P (t :: ('a, 'b) mapping_rbt)) k = 
  (case lookup t k of None ⇒ None | Some v ⇒ if P (k, v) then Some v else None)"
by transfer(simp split: option.split add: ID_ccompare_neq_None linorder.rbt_lookup_rbtreeify[OF mapping_linorder] linorder.sorted_filter[OF mapping_linorder] ord.is_rbt_rbt_sorted linorder.rbt_sorted_entries[OF mapping_linorder] distinct_map_filterI linorder.distinct_entries[OF mapping_linorder] map_of_filter_apply linorder.map_of_entries[OF mapping_linorder])

lemma all_conv_all_lookup:
  "all P t ⟷ (∀(k :: 'a) v. lookup t k = Some v ⟶ P k v)"
by transfer(auto simp add: ID_ccompare_neq_None linorder.rbt_lookup_keys[OF mapping_linorder] ord.is_rbt_rbt_sorted RBT_Impl.keys_def RBT_Impl_rbt_all_def linorder.map_of_entries[OF mapping_linorder, symmetric] linorder.distinct_entries[OF mapping_linorder] dest: map_of_SomeD intro: map_of_is_SomeI)

lemma ex_conv_ex_lookup:
  "ex P t ⟷ (∃(k :: 'a) v. lookup t k = Some v ∧ P k v)"
by transfer(auto simp add: ID_ccompare_neq_None linorder.rbt_lookup_keys[OF mapping_linorder] ord.is_rbt_rbt_sorted RBT_Impl.keys_def RBT_Impl_rbt_ex_def linorder.map_of_entries[OF mapping_linorder, symmetric] linorder.distinct_entries[OF mapping_linorder] intro: map_of_is_SomeI)

lemma diag_lookup:
  "lookup (diag t) = (λ(k :: 'a, k'). if k = k' then lookup t k else None)"
using linorder.rbt_lookup_RBT_Impl_diag[where ?'b='b, OF mapping_linorder]
apply transfer
apply (clarsimp simp add: ID_ccompare_neq_None ccompare_prod_def lt_of_comp_less_prod[symmetric] 
  rbt_comp_lookup[OF comparator_prod[OF mapping_comparator mapping_comparator], symmetric]
  ID_Some split: option.split) 
apply (unfold rbt_comp_lookup[OF mapping_comparator], simp)
done

context assumes ID_ccompare_neq_None': "ID CCOMPARE('b :: ccompare) ≠ None"
begin

lemma mapping_linorder': "class.linorder (cless_eq :: 'b ⇒ 'b ⇒ bool) cless"
using ID_ccompare_neq_None' by(clarsimp)(rule ID_ccompare)

lemma mapping_comparator': "comparator (ccomp :: 'b comparator)"
using ID_ccompare_neq_None' by(clarsimp)(rule ID_ccompare')

lemmas rbt_comp'[simp] = rbt_comp_simps[OF mapping_comparator']

lemma ccomp_comparator_prod:
  "ccomp = (comparator_prod ccomp ccomp :: ('a × 'b)comparator)"
  by(simp add: ccompare_prod_def lt_of_comp_less_prod ID_ccompare_neq_None ID_ccompare_neq_None' ID_Some split: option.splits)

lemma lookup_product: 
  "lookup (product f rbt1 rbt2) (a :: 'a, b :: 'b) = 
  (case lookup rbt1 a of None ⇒ None
   | Some c ⇒ map_option (f a c b) (lookup rbt2 b))"
using mapping_linorder mapping_linorder'
apply transfer
apply (unfold ccomp_comparator_prod rbt_comp_lookup[OF comparator_prod[OF mapping_comparator mapping_comparator']]
  rbt_comp rbt_comp' lt_of_comp_less_prod)
apply (simp add: ID_ccompare_neq_None ID_ccompare_neq_None' rbt_lookup_rbt_product)
done
end

end

hide_const (open) impl_of lookup empty insert delete
  entries keys bulkload map_entry map fold join meet filter all ex product diag init

end