Theory Map_Extra

section ‹ Map Type: extra functions and properties ›

theory Map_Extra
  imports
  Relation_Extra
  "HOL-Library.Countable_Set"
  "HOL-Library.Monad_Syntax"
  "HOL-Library.AList"
begin

subsection ‹ Extensionality and Update ›

lemma map_eq_iff: "f = g ⟷ (∀ x ∈ dom(f) ∪ dom(g). f x = g x)"
  by (auto simp add: fun_eq_iff)

subsection ‹ Graphing Maps ›

definition map_graph :: "('a ⇀ 'b) ⇒ ('a ↔ 'b)" where
"map_graph f = {(x,y) | x y. f x = Some y}"

definition graph_map :: "('a ↔ 'b) ⇒ ('a ⇀ 'b)" where
"graph_map g = (λ x. if (x ∈ fst ` g) then Some (SOME y. (x,y) ∈ g) else None)"

definition graph_map' :: "('a ↔ 'b) ⇀ ('a ⇀ 'b)" where
"graph_map' R = (if (functional R) then Some (graph_map R) else None)"

lemma map_graph_mem_equiv: "(x, y) ∈ map_graph f ⟷ f(x) = Some y"
  by (simp add: map_graph_def)

lemma map_graph_functional[simp]: "functional (map_graph f)"
  by (simp add:functional_def map_graph_def inj_on_def)

lemma map_graph_countable [simp]: "countable (dom f) ⟹ countable (map_graph f)"
  by (metis countable_image graph_def graph_eq_to_snd_dom map_graph_def)

lemma map_graph_inv [simp]: "graph_map (map_graph f) = f"
  by (force simp add:map_graph_def graph_map_def image_def)

lemma graph_map_empty[simp]: "graph_map {} = Map.empty"
  by (simp add:graph_map_def)

lemma graph_map_insert [simp]: "⟦functional g; g``{x} ⊆ {y}⟧ ⟹ graph_map (insert (x,y) g) = (graph_map g)(x ↦ y)"
  by (rule ext, auto simp add:graph_map_def)

lemma dom_map_graph: "dom f = Domain(map_graph f)"
  by (simp add: map_graph_def dom_def image_def)

lemma ran_map_graph: "ran f = Range(map_graph f)"
  by (simp add: map_graph_def ran_def image_def)

lemma graph_map_set: "functional (set xs) ⟹ graph_map (set xs) = map_of xs"
  by (induct xs; force)

lemma rel_apply_map_graph:
  "x ∈ dom(f) ⟹ (map_graph f)(x)⇩r = the (f x)"
  by (auto simp add: rel_apply_def map_graph_def)

lemma ran_map_add_subset:
  "ran (x ++ y) ⊆ (ran x) ∪ (ran y)"
  by (auto simp add:ran_def)

lemma finite_dom_graph: "finite (dom f) ⟹ finite (map_graph f)"
  by (metis dom_map_graph finite_imageD fst_eq_Domain functional_def map_graph_functional)

lemma finite_dom_ran [simp]: "finite (dom f) ⟹ finite (ran f)"
  by (metis finite_Range finite_dom_graph ran_map_graph)

lemma functional_insert: "functional (insert a R) ⟹ functional R"
  by (simp add: single_valued_def)

lemma Domain_insert: "Domain (insert a R) = insert (fst a) (Domain R)"
  by (simp add: Domain_fst)

lemma card_map_graph: "⟦ finite R; functional R ⟧ ⟹ card R = card (Domain R)"
  by (induct R rule: finite.induct, simp_all add: functional_insert card_insert_if Domain_insert finite_Domain)
     (metis DiffD1 Diff_insert_absorb DomainE Map_Extra.Domain_insert insertI1 insert_Diff prod.collapse single_valued_def)

lemma graph_map_inv [simp]: "functional g ⟹ map_graph (graph_map g) = g"
  apply (simp add:map_graph_def graph_map_def functional_def, safe)
   apply (metis (lifting, no_types) image_iff option.distinct(1) option.inject someI surjective_pairing)
  apply (simp add:inj_on_def)
  apply safe
   apply (metis fst_conv snd_conv some_equality)
  apply (metis (lifting) fst_conv image_iff)
  done

lemma graph_map_dom: "dom (graph_map R) = fst ` R"
  by (simp add: graph_map_def dom_def)

lemma graph_map_countable_dom: "countable R ⟹ countable (dom (graph_map R))"
  by (simp add: graph_map_dom)

lemma countable_ran:
  assumes "countable (dom f)"
  shows "countable (ran f)"
proof -
  have "countable (map_graph f)"
    by (simp add: assms)
  then have "countable (Range(map_graph f))"
    by (simp add: Range_snd)
  thus ?thesis
    by (simp add: ran_map_graph)
qed

lemma map_graph_inv' [simp]:
  "graph_map' (map_graph f) = Some f"
  by (simp add: graph_map'_def)

lemma map_graph_inj:
  "inj map_graph"
  by (metis injI map_graph_inv)

lemma map_eq_graph: "f = g ⟷ map_graph f = map_graph g"
  by (auto simp add: inj_eq map_graph_inj)

lemma map_le_graph: "f ⊆⇩m g ⟷ map_graph f ⊆ map_graph g"
  by (force simp add: map_le_def map_graph_def)

lemma map_graph_comp: "map_graph (g ∘⇩m f) = (map_graph f) O (map_graph g)"
  by (metis graph_def graph_map_comp map_graph_def)

lemma rel_comp_map: "R O map_graph f = (λ p. (fst p, the (f (snd p)))) ` (R ⊳⇩r dom(f))"
  by (force simp add: map_graph_def relcomp_unfold rel_ranres_def image_def dom_def)

lemma map_graph_update: "map_graph (f(k ↦ v)) = insert (k, v) ((- {k}) ⊲⇩r map_graph f)"
  by (simp add: map_graph_def rel_domres_def, safe, simp_all, metis option.sel)

subsection ‹ Map Application ›

definition map_apply :: "('a ⇀ 'b) ⇒ 'a ⇒ 'b" ("_'(_')⇩m" [999,0] 999) where
"map_apply = (λ f x. the (f x))"

subsection ‹ Map Membership ›

fun map_member :: "'a × 'b ⇒ ('a ⇀ 'b) ⇒ bool" (infix "∈⇩m" 50) where
"(k, v) ∈⇩m m ⟷ m(k) = Some(v)"

lemma map_ext:
  "⟦ ⋀ x y. (x, y) ∈⇩m A ⟷ (x, y) ∈⇩m B ⟧ ⟹ A = B"
  by (rule ext, simp_all, metis not_None_eq)

lemma map_member_alt_def:
  "(x, y) ∈⇩m A ⟷ (x ∈ dom A ∧ A(x)⇩m = y)"
  by (auto simp add: map_apply_def)

lemma map_le_member:
  "f ⊆⇩m g ⟷ (∀ x y. (x,y) ∈⇩m f ⟶ (x,y) ∈⇩m g)"
  by (force simp add: map_le_def)

subsection ‹ Preimage ›

definition preimage :: "('a ⇀ 'b) ⇒ 'b set ⇒ 'a set" where
"preimage f B = {x ∈ dom(f). the(f(x)) ∈ B}"

lemma preimage_range: "preimage f (ran f) = dom f"
  by (auto simp add: preimage_def ran_def)

lemma dom_preimage: "dom (m ∘⇩m f) = preimage f (dom m)"
  apply (simp add: dom_def preimage_def, safe, simp_all)
   apply (meson map_comp_Some_iff)
  apply (metis map_comp_def option.case_eq_if option.distinct(1))
  done



lemma countable_preimage:
  assumes "countable A" "inj_on f (preimage f A)"
  shows "countable (preimage f A)"
proof -
  obtain g :: "'a ⇒ nat" where g: "inj_on g A"
    using assms(1) by blast
  have "inj_on (g ∘ the ∘ f) (preimage f A)"
  proof (rule inj_onI)
    fix x y
    assume "x ∈ preimage f A" "y ∈ preimage f A" "(g ∘ the ∘ f) x = (g ∘ the ∘ f) y"
    with assms g show "x = y"
      unfolding preimage_def by (metis (lifting) comp_apply domIff inj_onD mem_Collect_eq option.expand)
  qed
  thus ?thesis
    by (simp add: countableI)
qed

subsection ‹ Minus operation for maps ›

definition map_minus :: "('a ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ ('a ⇀ 'b)" (infixl "--" 100)
where "map_minus f g = (λ x. if (f x = g x) then None else f x)"

lemma map_minus_apply [simp]: "y ∈ dom(f -- g) ⟹ (f -- g)(y)⇩m = f(y)⇩m"
  by (auto simp add: map_minus_def dom_def map_apply_def)

lemma map_member_plus:
  "(x, y) ∈⇩m f ++ g ⟷ ((x ∉ dom(g) ∧ (x, y) ∈⇩m f) ∨ (x, y) ∈⇩m g)"
  by (auto simp add: map_add_Some_iff)

lemma map_member_minus:
  "(x, y) ∈⇩m f -- g ⟷ (x, y) ∈⇩m f ∧ (¬ (x, y) ∈⇩m g)"
  by (auto simp add: map_minus_def)

lemma map_minus_plus_commute:
  "dom(g) ∩ dom(h) = {} ⟹ (f -- g) ++ h = (f ++ h) -- g"
  apply (rule map_ext)
  apply (simp add: map_member_plus map_member_minus del: map_member.simps)
  apply (auto simp add: map_member_alt_def)
  done

lemma map_graph_minus: "map_graph (f -- g) = map_graph f - map_graph g"
  by (simp add: map_minus_def map_graph_def, safe, simp_all, (meson option.distinct(1))+)

lemma map_minus_common_subset:
  "⟦ h ⊆⇩m f; h ⊆⇩m g ⟧ ⟹ (f -- h = g -- h) = (f = g)"
  by (auto simp add: map_eq_graph map_graph_minus map_le_graph)

subsection ‹ Map Bind ›

text ‹ Create some extra intro/elim rules to help dealing with proof about option bind. ›

lemma option_bindSomeE [elim!]:
  "⟦ X >>= F = Some(v); ⋀ x. ⟦ X = Some(x); F(x) = Some(v) ⟧ ⟹ P ⟧ ⟹ P"
  by (cases X, auto)

lemma option_bindSomeI [intro]:
  "⟦ X = Some(x); F(x) = Some(y) ⟧ ⟹ X >>= F = Some(y)"
  by (simp)

lemma ifSomeE [elim]: "⟦ (if c then Some(x) else None) = Some(y); ⟦ c; x = y ⟧ ⟹ P ⟧ ⟹ P"
  by (cases c, auto)

subsection ‹ Range Restriction ›

text ‹ A range restriction operator; only domain restriction is provided in HOL. ›

definition ran_restrict_map :: "('a ⇀ 'b) ⇒ 'b set ⇒ 'a ⇀ 'b" ("_↿⇘_⇙" [111,110] 110) where
"ran_restrict_map f B = (λx. do { v <- f(x); if (v ∈ B) then Some(v) else None })"

lemma ran_restrict_alt_def: "f↿⇘B⇙ = (λ x. if x ∈ dom(f) ∧ the(f(x)) ∈ B then f x else None)"
  by (auto simp add: ran_restrict_map_def fun_eq_iff bind_eq_None_conv)

lemma ran_restrict_empty [simp]: "f↿⇘{}⇙ = Map.empty"
  by (simp add:ran_restrict_map_def)

lemma ran_restrict_ran [simp]: "f↿⇘ran(f) ⇙ = f"
proof
  fix x
  show "(f↿⇘ran(f)⇙) x = f x"
  proof (cases "f(x)")
    case None
    then show ?thesis by (simp add: ran_restrict_map_def ran_def)
  next
    case (Some a)
    then show ?thesis by (auto simp add: ran_restrict_map_def ran_def)
  qed
qed

lemma ran_ran_restrict [simp]: "ran(f↿⇘B⇙) = ran(f) ∩ B"
  by (force simp add:ran_restrict_map_def ran_def)

lemma dom_ran_restrict: "dom(f↿⇘B⇙) ⊆ dom(f)"
  by (auto simp add:ran_restrict_map_def dom_def)

lemma ran_restrict_finite_dom [intro]:
  "finite(dom(f)) ⟹ finite(dom(f↿⇘B⇙))"
  by (metis finite_subset dom_ran_restrict)

lemma dom_Some [simp]: "dom (Some ∘ f) = UNIV"
  by (auto)

lemma map_dres_rres_commute: "f↿⇘B⇙ |` A = (f |` A)↿⇘B⇙"
  by (auto simp add: restrict_map_def ran_restrict_map_def)

lemma ran_restrict_map_twice [simp]: "(f↿⇘A⇙)↿⇘B⇙ = f↿⇘(A ∩ B)⇙"
proof 
  fix x
  show "((f↿⇘A⇙)↿⇘B⇙) x = (f↿⇘(A ∩ B)⇙) x"
  proof (cases "f x")
    case None
    then show ?thesis by (simp add: ran_restrict_map_def)
  next
    case (Some a)
    then show ?thesis by (simp add: ran_restrict_map_def fun_eq_iff option.case_eq_if)
  qed
qed

lemma dom_left_map_add [simp]: "x ∈ dom g ⟹ (f ++ g) x = g x"
  by (auto simp add:map_add_def dom_def)

lemma dom_right_map_add [simp]: "⟦ x ∉ dom g; x ∈ dom f ⟧ ⟹ (f ++ g) x = f x"
  by (auto simp add:map_add_def dom_def)

lemma map_add_restrict:
  "f ++ g = (f |` (- dom g)) ++ g"
  by (rule ext, auto simp add: map_add_def restrict_map_def)

subsection ‹ Map Inverse and Identity ›

definition map_inv :: "('a ⇀ 'b) ⇒ ('b ⇀ 'a)" where
"map_inv f ≡ λ y. if (y ∈ ran f) then Some (SOME x. f x = Some y) else None"

definition map_id_on :: "'a set ⇒ ('a ⇀ 'a)" where
"map_id_on xs ≡ λ x. if (x ∈ xs) then Some x else None"

lemma map_id_on_in [simp]:
  "x ∈ xs ⟹ map_id_on xs x = Some x"
  by (simp add:map_id_on_def)

lemma map_id_on_out [simp]:
  "x ∉ xs ⟹ map_id_on xs x = None"
  by (simp add:map_id_on_def)

lemma map_id_dom [simp]: "dom (map_id_on xs) = xs"
  by (simp add:dom_def map_id_on_def)

lemma map_id_ran [simp]: "ran (map_id_on xs) = xs"
  by (force simp add:ran_def map_id_on_def)

lemma map_id_on_UNIV[simp]: "map_id_on UNIV = Some"
  by (simp add:map_id_on_def)

lemma map_id_on_inj [simp]:
  "inj_on (map_id_on xs) xs"
  by (simp add:inj_on_def)

lemma restrict_map_inj_on:
  "inj_on f (dom f) ⟹ inj_on (f |` A) (dom f ∩ A)"
  by (auto simp add:inj_on_def)

lemma map_inv_empty [simp]: "map_inv Map.empty = Map.empty"
  by (simp add:map_inv_def)

lemma map_inv_id [simp]:
  "map_inv (map_id_on xs) = map_id_on xs"
  by (force simp add:map_inv_def map_id_on_def ran_def)

lemma map_inv_Some [simp]: "map_inv Some = Some"
  by (simp add:map_inv_def ran_def)

lemma map_inv_f_f [simp]:
  "⟦ inj_on f (dom f); f x = Some y ⟧ ⟹ map_inv f y = Some x"
  apply (simp add: map_inv_def, safe)
   apply (rule some_equality)
    apply (auto simp add:inj_on_def dom_def ran_def)
  done

lemma dom_map_inv [simp]:
  "dom (map_inv f) = ran f"
  by (auto simp add:map_inv_def)

lemma ran_map_inv [simp]:
  "inj_on f (dom f) ⟹ ran (map_inv f) = dom f"
  apply (simp add:map_inv_def ran_def, safe)
   apply (metis (mono_tags, lifting) verit_sko_ex')
  apply (metis (mono_tags, lifting) domI domIff map_inv_def map_inv_f_f option.inject)
  done

lemma dom_image_ran: "f ` dom f = Some ` ran f"
  by (auto simp add:dom_def ran_def image_def)

lemma inj_map_inv [intro]:
  "inj_on f (dom f) ⟹ inj_on (map_inv f) (ran f)"
  apply (simp add:map_inv_def inj_on_def dom_def ran_def, safe)
  apply (metis (mono_tags, lifting) option.sel someI_ex)
  done

lemma inj_map_bij: "inj_on f (dom f) ⟹ bij_betw f (dom f) (Some ` ran f)"
  by (auto simp add:inj_on_def dom_def ran_def image_def bij_betw_def)

lemma map_inv_map_inv [simp]:
  assumes "inj_on f (dom f)"
  shows "map_inv (map_inv f) = f"
proof -

  from assms have "inj_on (map_inv f) (ran f)"
    by auto

  thus ?thesis
    by (metis (no_types, lifting) ext assms domIff dom_map_inv map_inv_f_f option.collapse
        ran_map_inv)
qed

lemma map_self_adjoin_complete [intro]:
  assumes "dom f ∩ ran f = {}" "inj_on f (dom f)"
  shows "inj_on (map_inv f ++ f) (dom f ∪ ran f)"
proof (rule inj_onI)
  fix x y
  assume x:"x ∈ dom f ∪ ran f" and y:"y ∈ dom f ∪ ran f" 
     and f:"(map_inv f ++ f) x = (map_inv f ++ f) y"

  show "x = y"
  proof (cases "x ∈ dom f")
    case True
    then show ?thesis
      by (metis assms(1,2) disjoint_iff_not_equal domD dom_left_map_add f inj_on_def
          map_add_dom_app_simps(3) ranI ran_map_inv) 
  next
    case False
    then show ?thesis
      by (metis (full_types) UnE assms(1,2) disjoint_iff domIff dom_left_map_add dom_map_inv
          f inj_map_inv inj_on_def map_add_dom_app_simps(3) ran_map_inv ran_restrict_alt_def
          ran_restrict_ran x) 
  qed
qed

lemma inj_completed_map [intro]:
  assumes "dom f = ran f" "inj_on f (dom f)"
  shows "inj (Some ++ f)"
proof (rule injI)
  fix x y
  assume f:"(Some ++ f) x = (Some ++ f) y"
  have bb: "bij_betw f (dom f) (Some ` ran f)"
    using assms(2) inj_map_bij by blast
  thus "x = y"
  proof (cases "x ∈ dom f")
    case True
    then show ?thesis
      by (metis assms(1,2) f inj_on_contraD map_add_dom_app_simps(1,3) ranI) 
  next
    case False
    then show ?thesis
      by (metis assms(1) dom_left_map_add f map_add_dom_app_simps(3) option.inject
          ranI) 
  qed
qed

lemma bij_completed_map [intro]:
  fixes f :: "'a ⇀ 'a"
  assumes "dom f = ran f" "inj_on f (dom f)"
  shows "bij_betw (Some ++ f) UNIV (range Some)"
proof -
  have "range (Some ++ f) = range Some"
  proof (rule set_eqI, rule iffI)
    fix x
    assume "x ∈ range (Some ++ f)"
    thus "x ∈ range Some"
      using image_iff by fastforce
  next
    fix x :: "'a option"
    assume "x ∈ range Some"
    thus "x ∈ range (Some ++ f)"
      by (metis assms(1) dom_image_ran[of f] image_iff[of x f "dom f"] image_iff[of "Some _" Some "dom f"] image_iff[of x Some UNIV]
          map_add_dom_app_simps(1)[of _ f Some] map_add_dom_app_simps(3)[of _ f Some] rangeI[of "Some ++ f"])
  qed
  thus ?thesis
    by (metis assms(1,2) inj_completed_map inj_on_imp_bij_betw)
qed


lemma bij_map_Some:
  "bij_betw f a (Some ` b) ⟹ bij_betw (the ∘ f) a b"
  apply (simp add:bij_betw_def)
  apply (safe)
    apply (metis (opaque_lifting, no_types) comp_inj_on_iff f_the_inv_into_f inj_on_inverseI option.sel)
   apply (metis (opaque_lifting, no_types) image_iff option.sel)
  apply (metis Option.these_def Some_image_these_eq image_image these_image_Some_eq)
  done

lemma ran_map_add [simp]:
  "m`(dom m ∩ dom n) = n`(dom m ∩ dom n) ⟹
   ran(m++n) = ran n ∪ ran m"
  apply (simp add:ran_def, safe, simp_all)
   apply (metis)
  apply (metis domI map_add_dom_app_simps(1))
  apply (metis (no_types, opaque_lifting) IntI domI dom_left_map_add image_iff map_add_dom_app_simps(3))
  done

lemma ran_maplets [simp]:
  "⟦ length xs = length ys; distinct xs ⟧ ⟹ ran [xs [↦] ys] = set ys"
    by (induct rule:list_induct2, simp_all)

lemma inj_map_add:
  "⟦ inj_on f (dom f); inj_on g (dom g); ran f ∩ ran g = {} ⟧ ⟹
   inj_on (f ++ g) (dom f ∪ dom g)"
  apply (simp add:inj_on_def, safe, simp_all)
     apply (metis (full_types) disjoint_iff_not_equal domI dom_left_map_add map_add_dom_app_simps(3) ranI)
    apply (metis disjoint_iff_not_equal domI map_add_SomeD ranI)
   apply (metis disjoint_iff_not_equal domIff map_add_Some_iff ranI)
  apply (metis domI)
  done

lemma map_inv_add':
  assumes "inj_on f (dom f)" "inj_on g (dom g)"
          "dom f ∩ dom g = {}" "ran f ∩ ran g = {}"
 shows "map_inv (f ++ g) = map_inv f ++ map_inv g"
proof (rule ext)

  from assms have minj: "inj_on (f ++ g) (dom (f ++ g))"
    by (simp, metis inj_map_add sup_commute)

  fix x
  have "x ∈ ran g ⟹ map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
  proof -
    assume ran:"x ∈ ran g"
    then obtain y where dom:"g y = Some x" "y ∈ dom g"
      by (auto simp add:ran_def)

    hence "(f ++ g) y = Some x"
      by simp

    with assms minj ran dom show "map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
      by simp
  qed

  moreover have "⟦ x ∉ ran g; x ∈ ran f ⟧ ⟹ map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
  proof -
    assume ran:"x ∉ ran g" "x ∈ ran f"
    with assms obtain y where dom:"f y = Some x" "y ∈ dom f" "y ∉ dom g"
      by (auto simp add:ran_def)

    with ran have "(f ++ g) y = Some x"
      by (simp)

    with assms minj ran dom show "map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
      by simp
  qed

  moreover from assms minj have "⟦ x ∉ ran g; x ∉ ran f ⟧ ⟹ map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
    apply (simp add:map_inv_def ran_def map_add_def)
    apply (metis dom_left_map_add map_add_def map_add_dom_app_simps(3))
    done

  ultimately show "map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
    by blast
qed

lemma map_inv_dom_res:
  assumes "inj_on f (dom f)"
  shows "map_inv (f |` A) = (map_inv f) ↿⇘A⇙"
  using assms
  apply (simp add: map_inv_def restrict_map_def ran_restrict_map_def dom_def ran_def fun_eq_iff inj_on_def)
  apply (safe intro!: some_equality)
     apply (metis (mono_tags, lifting) someI_ex)+
  done

lemma map_inv_ran_res:
  assumes "inj_on f (dom f)"
  shows "map_inv (f ↿⇘A⇙) = (map_inv f) |` A"
  using assms someI_ex by (force intro!: some_equality simp add: map_inv_def restrict_map_def ran_restrict_map_def dom_def ran_def fun_eq_iff inj_on_def)

lemma map_update_as_add: "f(x ↦ y) = f ++ [x ↦ y]"
  by (auto simp add: map_add_def)

lemma map_add_lookup [simp]:
  "x ∉ dom f ⟹ ([x ↦ y] ++ f) x = Some y"
  by (simp add:map_add_def dom_def)

lemma map_add_Some: "Some ++ f = map_id_on (- dom f) ++ f"
proof 
  fix x
  show "(Some ++ f) x = (map_id_on (- dom f) ++ f) x"
  proof (cases "x ∈ dom f")
    case True
    then show ?thesis by simp
  next
    case False
    then show ?thesis by simp
  qed
qed

lemma distinct_map_dom:
  "x ∉ set xs ⟹ x ∉ dom [xs [↦] ys]"
  by (simp add:dom_def)

lemma distinct_map_ran:
  "⟦ distinct xs; y ∉ set ys; length xs = length ys ⟧ ⟹
   y ∉ ran ([xs [↦] ys])"
  apply (simp add:map_upds_def)
  apply (subgoal_tac "distinct (map fst (rev (zip xs ys)))")
  apply (simp add:ran_distinct)
  apply (metis (opaque_lifting, no_types) image_iff set_zip_rightD surjective_pairing)
  apply (simp add:zip_rev[THEN sym])
done

lemma maplets_lookup [dest]:
  "⟦ length xs = length ys; distinct xs; ∀ y. [xs [↦] ys] x = Some y ⟧ ⟹ y ∈ set ys"
  using ranI by fastforce
  
lemma maplets_distinct_inj [intro]:
  "⟦ length xs = length ys; distinct xs; distinct ys; set xs ∩ set ys = {} ⟧ ⟹
   inj_on [xs [↦] ys] (set xs)"
  apply (induct rule:list_induct2)
   apply (simp_all)
  apply (rule conjI)
   apply (rule inj_onI)
  apply (metis fun_upd_def inj_on_contraD)
  apply (metis image_iff ranI ran_maplets)
  done

lemma map_inv_maplet[simp]: "map_inv [x ↦ y] = [y ↦ x]"
  by (auto simp add:map_inv_def)

lemma map_inv_add:
  assumes "inj_on f (dom f)" "inj_on g (dom g)"
          "ran f ∩ ran g = {}"
  shows "map_inv (f ++ g) = map_inv f↿⇘(- dom g)⇙ ++ map_inv g"
proof -
  have "map_inv (f ++ g) = map_inv (f |` (- dom(g))  ++ g)"
    by (metis map_add_restrict)
  also have "... = map_inv (f |` (- dom g)) ++ map_inv g"
    by (rule map_inv_add', simp_all add: assms restrict_map_inj_on)
       (metis assms(3) disjoint_iff ranI ran_restrictD)
  also have "... = map_inv f↿⇘(- dom g)⇙ ++ map_inv g"
    by (simp add: map_inv_dom_res assms) 
  finally show ?thesis .
qed

lemma map_inv_upd:
  assumes "inj_on f (dom f)" "inj_on g (dom g)" "v ∉ ran f"
  shows "map_inv (f(k ↦ v)) = (map_inv (f |` (- {k})))(v ↦ k)"
proof -
  have "map_inv (f(k ↦ v)) = map_inv (f ++ [k ↦ v])"
    by (auto)
  also have "... = map_inv f↿⇘(- dom [k ↦ v])⇙ ++ map_inv [k ↦ v]"
    by (rule map_inv_add, simp_all add: assms)
  also have "... = (map_inv f↿⇘(- {k})⇙)(v ↦ k)"
    by (simp)
  also have "... = (map_inv (f |` (- {k})))(v ↦ k)"
    by (simp add: assms(1) map_inv_dom_res)
  finally show ?thesis .
qed
  
lemma map_inv_maplets [simp]:
  "⟦ length xs = length ys; distinct xs; distinct ys; set xs ∩ set ys = {} ⟧ ⟹
  map_inv [xs [↦] ys] = [ys [↦] xs]"
proof (induct rule:list_induct2)
  case Nil
  then show ?case by simp
next
  case (Cons x xs y ys)
  have "map_inv ([xs [↦] ys] ++ [x ↦ y]) = map_inv [xs [↦] ys] ++ map_inv [x ↦ y]"
  proof (rule map_inv_add')
    from Cons show "inj_on [xs [↦] ys] (dom [xs [↦] ys])" by auto
    from Cons show "inj_on [x ↦ y] (dom [x ↦ y])" by auto
    from Cons show "dom [xs [↦] ys] ∩ dom [x ↦ y] = {}" by auto
    from Cons show "ran [xs [↦] ys] ∩ ran [x ↦ y] = {}" by auto
  qed
  with Cons show ?case
    by (metis disjoint_iff distinct.simps(2) list.set_intros(2) map_inv_maplet map_update_as_add map_upds_Cons map_upds_twist)
qed

lemma maplets_lookup_nth [simp]:
  "⟦ length xs = length ys; distinct xs; i < length ys ⟧ ⟹
   [xs [↦] ys] (xs ! i) = Some (ys ! i)"
  apply (induct arbitrary: i rule:list_induct2)
  apply simp
  using less_Suc_eq_0_disj apply auto
  done

theorem inv_map_inv:
  assumes "inj_on f (dom f)" "ran f = dom f"
  shows "inv (the ∘ (Some ++ f)) = the ∘ map_inv (Some ++ f)"
proof
  fix x
  show "(inv (the ∘ (Some ++ f))) x = (the ∘ map_inv (Some ++ f)) x"
  proof (cases "x ∈ ran f")
    case True
    then obtain y where y:"f y = Some x"
      by (metis dom_image_ran image_iff)
    with assms show ?thesis 
      apply (simp add:map_add_Some map_inv_add' inv_def)
      apply (rule some_equality)
      apply simp
      apply (metis (full_types) Compl_iff domIff inj_on_def map_add_Some map_add_dom_app_simps(2,3) map_id_dom option.exhaust_sel ranI)
      done
  next
    case False
    then show ?thesis 
      apply (simp add:map_add_Some map_inv_add' inv_def)
      apply (rule some_equality)
      apply (simp add: assms(1,2) map_inv_add')
      apply (metis (no_types, opaque_lifting) Un_UNIV_right assms(1,2) dom_map_add inj_completed_map map_add_None map_add_Some map_id_dom map_id_on_UNIV map_inv_f_f option.exhaust_sel
          option.sel)
      done
  qed
qed

lemma map_comp_dom: "dom (g ∘⇩m f) ⊆ dom f"
  by (metis (lifting, full_types) Collect_mono dom_def map_comp_simps(1))

lemma map_comp_assoc: "f ∘⇩m (g ∘⇩m h) = f ∘⇩m g ∘⇩m h"
proof
  fix x
  show "(f ∘⇩m (g ∘⇩m h)) x = (f ∘⇩m g ∘⇩m h) x"
  proof (cases "h x")
    case None thus ?thesis
      by (auto simp add: map_comp_def)
  next
    case (Some y) thus ?thesis
      by (auto simp add: map_comp_def)
  qed
qed

lemma map_comp_runit [simp]: "f ∘⇩m Some = f"
  by (simp add: map_comp_def)

lemma map_comp_lunit [simp]: "Some ∘⇩m f = f"
proof
  fix x
  show "(Some ∘⇩m f) x = f x"
  proof (cases "f x")
    case None thus ?thesis
      by (simp add: map_comp_def)
  next
    case (Some y) thus ?thesis
      by (simp add: map_comp_def)
  qed
qed

lemma map_comp_apply [simp]: "(f ∘⇩m g) x = g(x) >>= f"
  by (auto simp add: map_comp_def option.case_eq_if)

lemma map_graph_map_inv: "inj_on f (dom f) ⟹ map_graph (map_inv f) = (map_graph f)¯"
  by (simp add: map_graph_def, safe, simp_all, metis dom_map_inv inj_map_inv map_inv_f_f map_inv_map_inv)

subsection ‹ Merging of compatible maps ›

definition comp_map :: "('a ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ bool" (infixl "∥⇩m" 60) where
"comp_map f g = (∀ x ∈ dom(f) ∩ dom(g). the(f(x)) = the(g(x)))"

lemma comp_map_unit: "Map.empty ∥⇩m f"
  by (simp add: comp_map_def)

lemma comp_map_refl: "f ∥⇩m f"
  by (simp add: comp_map_def)

lemma comp_map_sym: "f ∥⇩m g ⟹ g ∥⇩m f"
  by (simp add: comp_map_def)

definition merge :: "('a ⇀ 'b) set ⇒ 'a ⇀ 'b" where
"merge fs =
  (λ x. if (∃ f ∈ fs. x ∈ dom(f)) then (THE y. ∀ f ∈ fs. x ∈ dom(f) ⟶ f(x) = y) else None)"

lemma merge_empty: "merge {} = Map.empty"
  by (simp add: merge_def)

lemma merge_singleton: "merge {f} = f"
  unfolding merge_def
  by (auto simp add: fun_eq_iff domIff)

subsection ‹ Conversion between lists and maps ›

definition map_of_list :: "'a list ⇒ (nat ⇀ 'a)" where
"map_of_list xs = (λ i. if (i < length xs) then Some (xs!i) else None)"

lemma map_of_list_nil [simp]: "map_of_list [] = Map.empty"
  by (simp add: map_of_list_def)

lemma dom_map_of_list [simp]: "dom (map_of_list xs) = {0..<length xs}"
  by (auto simp add: map_of_list_def dom_def)

lemma ran_map_of_list [simp]: "ran (map_of_list xs) = set xs"
  apply (simp add: ran_def map_of_list_def)
  apply (safe)
   apply (force)
  apply (meson in_set_conv_nth)
  done

definition list_of_map :: "(nat ⇀ 'a) ⇒ 'a list" where
"list_of_map f = (if (f = Map.empty) then [] else map (the ∘ f) [0 ..< Suc(GREATEST x. x ∈ dom f)])"

lemma list_of_map_empty [simp]: "list_of_map Map.empty = []"
  by (simp add: list_of_map_def)

definition list_of_map' :: "(nat ⇀ 'a) ⇀ 'a list" where
"list_of_map' f = (if (∃ n. dom f = {0..<n}) then Some (list_of_map f) else None)"

lemma map_of_list_inv [simp]: "list_of_map (map_of_list xs) = xs"
proof (cases "xs = []")
  case True thus ?thesis by (simp)
next
  case False
  moreover hence "(GREATEST x. x ∈ dom (map_of_list xs)) = length xs - 1"
    by (auto intro: Greatest_equality)
  moreover from False have "map_of_list xs ≠ Map.empty"
    by (metis ran_empty ran_map_of_list set_empty)
  ultimately show ?thesis
    by (auto intro!:nth_equalityI simp add: list_of_map_def map_of_list_def  fun_eq_iff)
qed

subsection ‹ Map Comprehension ›

text ‹ Map comprehension simply converts a relation built through set comprehension into a map. ›

syntax
  "_Mapcompr" :: "'a ⇒ 'b ⇒ idts ⇒ bool ⇒ 'a ⇀ 'b"    ("(1[_ ↦ _ |/_./ _])")

translations
  "_Mapcompr F G xs P" == "CONST graph_map {(F, G) | xs. P}"

lemma map_compr_eta:
  "[x ↦ y | x y. (x, y) ∈⇩m f] = f"
  apply (rule ext)
  apply (simp add: graph_map_def, safe, simp_all)
  apply (metis (mono_tags, lifting) Domain.DomainI fst_eq_Domain mem_Collect_eq old.prod.case option.distinct(1) option.expand option.sel)
  done

lemma map_compr_simple:
  "[x ↦ F x y | x y. (x, y) ∈⇩m f] = (λ x. do { y ← f(x); Some(F x y) })"
  apply (rule ext)
  apply (auto simp add: graph_map_def image_Collect)
  done

lemma map_compr_dom_simple [simp]:
  "dom [x ↦ f x | x. P x] = {x. P x}"
  by (force simp add: graph_map_dom image_Collect)

lemma map_compr_ran_simple [simp]:
  "ran [x ↦ f x | x. P x] = {f x | x. P x}"
  apply (simp add: graph_map_def ran_def, safe, simp_all)
  apply blast
  apply (metis (mono_tags, lifting) fst_eqD image_eqI mem_Collect_eq someI)
  done

lemma map_compr_eval_simple [simp]:
  "[x ↦ f x | x. P x] x = (if (P x) then Some (f x) else None)"
  by (auto simp add: graph_map_def image_Collect)

subsection ‹ Sorted lists from maps ›

definition sorted_list_of_map :: "('a::linorder ⇀ 'b) ⇒ ('a × 'b) list" where
"sorted_list_of_map f = map (λ k. (k, the (f k))) (sorted_list_of_set(dom(f)))"

lemma sorted_list_of_map_empty [simp]:
  "sorted_list_of_map Map.empty = []"
  by (simp add: sorted_list_of_map_def)

lemma sorted_list_of_map_inv:
  assumes "finite(dom(f))"
  shows "map_of (sorted_list_of_map f) = f"
proof -
  obtain A where "finite A" "A = dom(f)"
    by (simp add: assms)
  thus ?thesis
  proof (induct A rule: finite_induct)
    case empty thus ?thesis
      by (simp add: sorted_list_of_map_def, metis dom_empty empty_iff map_le_antisym map_le_def)
  next
    case (insert x A) thus ?thesis
      by (simp add: assms sorted_list_of_map_def map_of_map_keys)
  qed
qed

declare map_member.simps [simp del]

subsection ‹ Extra map lemmas ›

lemma map_eqI:
  "⟦ dom f = dom g; ∀ x∈dom(f). the(f x) = the(g x) ⟧ ⟹ f = g"
  by (metis domIff map_le_antisym map_le_def option.expand)

lemma map_restrict_dom [simp]: "f |` dom f = f"
  by (simp add: map_eqI)

lemma map_restrict_dom_compl: "f |` (- dom f) = Map.empty"
  by (metis dom_eq_empty_conv dom_restrict inf_compl_bot)

lemma restrict_map_neg_disj:
  "dom(f) ∩ A = {} ⟹ f |` (- A) = f"
  by (simp add: restrict_map_def, rule ext, metis IntI domIff empty_iff)

lemma map_plus_restrict_dist: "(f ++ g) |` A = (f |` A) ++ (g |` A)"
  by (auto simp add: restrict_map_def map_add_def)

lemma map_plus_eq_left:
  assumes "f ++ h = g ++ h"
  shows "(f |` (- dom h)) = (g |` (- dom h))"
proof -
  have "h |` (- dom h) = Map.empty"
    by (metis Compl_disjoint dom_eq_empty_conv dom_restrict)
  then have f2: "f |` (- dom h) = (f ++ h) |` (- dom h)"
    by (simp add: map_plus_restrict_dist)
  have "h |` (- dom h) = Map.empty"
    by (metis (no_types) Compl_disjoint dom_eq_empty_conv dom_restrict)
  then show ?thesis
    using f2 assms by (simp add: map_plus_restrict_dist)
qed

lemma map_add_split:
  "dom(f) = A ∪ B ⟹ (f |` A) ++ (f |` B) = f"
  by (rule ext, auto simp add: map_add_def restrict_map_def option.case_eq_if)

lemma map_le_via_restrict:
  "f ⊆⇩m g ⟷ g |` dom(f) = f"
  by (auto simp add: map_le_def restrict_map_def dom_def fun_eq_iff)

lemma map_add_cancel:
  "f ⊆⇩m g ⟹ f ++ (g -- f) = g"
  by (simp add: map_le_def map_add_def map_minus_def fun_eq_iff option.case_eq_if)
     (metis domIff)

lemma map_le_iff_add: "f ⊆⇩m g ⟷ (∃ h. dom(f) ∩ dom(h) = {} ∧ f ++ h = g)"
proof 
  assume "f ⊆⇩m g" 
  hence "dom f ∩ dom (g -- f) = {} ∧ f ++ (g -- f) = g"
    by (metis (no_types, lifting) Int_emptyI domIff map_add_cancel map_le_def map_minus_def)
  thus "∃h. dom f ∩ dom h = {} ∧ f ++ h = g" by blast
next
  assume "∃h. dom f ∩ dom h = {} ∧ f ++ h = g"
  thus "f ⊆⇩m g"
    by (auto simp add: map_add_comm)
qed

lemma map_add_comm_weak: "(∀ k ∈ dom m1 ∩ dom m2. m1(k) = m2(k)) ⟹ m1 ++ m2 = m2 ++ m1"
  by (simp add: map_add_def option.case_eq_if fun_eq_iff)
     (metis IntI domI)

lemma map_add_comm_weak': "Q |` dom P = P |` dom Q ⟹ P ++ Q = Q ++ P"
  by (metis IntD1 IntD2 map_add_comm_weak restrict_in)

lemma map_compat_add: "Q |` dom P = P |` dom Q ⟹ R |` (dom Q ∪ dom P) = (P ++ Q) |` dom R ⟹ R |` dom P = P |` dom R"
  by (metis Int_commute Map.restrict_restrict Un_Int_eq(2) map_add_comm_weak' map_le_iff_map_add_commute map_le_via_restrict)

abbreviation "rel_map R ≡ rel_fun (=) (rel_option R)"

lemma rel_map_iff: 
  "rel_map R f g ⟷ (dom(f) = dom(g) ∧ (∀ x∈dom(f). R (the (f x)) (the (g x))))"
  apply (simp add: rel_fun_def, safe)
  apply (metis not_None_eq option.rel_distinct(2))
  apply (metis not_None_eq option.rel_distinct(1))
  apply (metis option.rel_sel option.sel option.simps(3))
  apply (metis domIff option.rel_sel)
  done

end