theory Mapping_Code
  imports "Containers.Mapping_Impl"
begin

lift_definition set_of_idx :: "('a, 'b set) mapping → 'b set" is
  "λm. ∪(ran m)" .

lemma set_of_idx_code[code]:
  fixes t :: "('a :: ccompare, 'b set) mapping_rbt"
  shows "set_of_idx (RBT_Mapping t) =
    (case ID CCOMPARE('a) of None → Code.abort (STR ''set_of_idx RBT_Mapping: ccompare = None'') (λ_. set_of_idx (RBT_Mapping t))
    | Some _ → ∪(snd ` set (RBT_Mapping2.entries t)))"
  unfolding RBT_Mapping_def
  by transfer (auto simp: ran_def rbt_comp_lookup[OF ID_ccompare'] ord.is_rbt_def linorder.rbt_lookup_in_tree[OF comparator.linorder[OF ID_ccompare']] split: option.splits)+

lemma mapping_combine[code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt"
  shows "Mapping.combine f (RBT_Mapping t) (RBT_Mapping u) =
    (case ID CCOMPARE('a) of None → Code.abort (STR ''combine RBT_Mapping: ccompare = None'') (λ_. Mapping.combine f (RBT_Mapping t) (RBT_Mapping u))
    | Some _ → RBT_Mapping (RBT_Mapping2.join (λ_. f) t u))"
  by (auto simp add: Mapping.combine.abs_eq Mapping_inject lookup_join split: option.split)

lift_definition mapping_join :: "('b → 'b → 'b) → ('a, 'b) mapping → ('a, 'b) mapping → ('a, 'b) mapping" is
  "λf m m' x. case m x of None → None | Some y → (case m' x of None → None | Some y' → Some (f y y'))" .

lemma mapping_join_code[code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt"
  shows "mapping_join f (RBT_Mapping t) (RBT_Mapping u) =
    (case ID CCOMPARE('a) of None → Code.abort (STR ''mapping_join RBT_Mapping: ccompare = None'') (λ_. mapping_join f (RBT_Mapping t) (RBT_Mapping u))
    | Some _ → RBT_Mapping (RBT_Mapping2.meet (λ_. f) t u))"
  by (auto simp add: mapping_join.abs_eq Mapping_inject lookup_meet split: option.split)

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

lift_definition diff ::
  "('a, 'b) mapping_rbt → ('a, 'b) mapping_rbt → ('a, 'b) mapping_rbt" is "rbt_comp_minus ccomp"
  by (auto 4 3 intro: linorder.rbt_minus_is_rbt ID_ccompare ord.is_rbt_rbt_sorted simp: rbt_comp_minus[OF ID_ccompare'])

end

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

lemma lookup_diff:
  "RBT_Mapping2.lookup (diff (t1 :: ('a, 'b) mapping_rbt) t2) =
  (λk. case RBT_Mapping2.lookup t1 k of None → None | Some v1 → (case RBT_Mapping2.lookup t2 k of None → Some v1 | Some v2 → None))"
  by transfer (auto simp add: fun_eq_iff linorder.rbt_lookup_rbt_minus[OF mapping_linorder] ID_ccompare_neq_None restrict_map_def split: option.splits)

end

lift_definition mapping_antijoin :: "('a, 'b) mapping → ('a, 'b) mapping → ('a, 'b) mapping" is
  "λm m' x. case m x of None → None | Some y → (case m' x of None → Some y | Some y' → None)" .

lemma mapping_antijoin_code[code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt"
  shows "mapping_antijoin (RBT_Mapping t) (RBT_Mapping u) =
    (case ID CCOMPARE('a) of None → Code.abort (STR ''mapping_antijoin RBT_Mapping: ccompare = None'') (λ_. mapping_antijoin (RBT_Mapping t) (RBT_Mapping u))
    | Some _ → RBT_Mapping (diff t u))"
  by (auto simp add: mapping_antijoin.abs_eq Mapping_inject lookup_diff split: option.split)

end