Theory Mapping_Code

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