Theory Maps

section ‹Maps›

theory Maps
imports Sequence_Zip
begin

  section ‹Basics›

  lemma fun_upd_None[simp]:
    assumes "p ∉ dom f"
    shows "f (p := None) = f"
    using assms by auto

  (* TODO: this is a strictly stronger version of finite_set_of_finite_maps, move to library *)
  lemma finite_set_of_finite_maps':
    assumes "finite A" "finite B"
    shows "finite {m. dom m ⊆ A ∧ ran m ⊆ B}"
  proof -
    have "{m. dom m ⊆ A ∧ ran m ⊆ B} = (⋃ 𝒜 ∈ Pow A. {m. dom m = 𝒜 ∧ ran m ⊆ B})" by auto
    also have "finite …" using finite_subset assms by (auto intro: finite_set_of_finite_maps)
    finally show ?thesis by this
  qed

  lemma fold_map_of:
    assumes "distinct xs"
    shows "fold (λ x (k, m). (Suc k, m (x ↦ k))) xs (k, m) =
      (k + length xs, m ++ map_of (xs || [k ..< k + length xs]))"
  using assms
  proof (induct xs arbitrary: k m)
    case Nil
    show ?case by simp
  next
    case (Cons x xs)
    have "fold (λ x (k, m). (Suc k, m (x ↦ k))) (x # xs) (k, m) =
      (Suc k + length xs, (m ++ map_of (xs || [Suc k ..< Suc k + length xs])) (x ↦ k))"
      using Cons by (fastforce simp add: map_add_upd_left)
    also have "… = (k + length (x # xs), m ++ map_of (x # xs || [k ..< k + length (x # xs)]))"
      by (simp add: upt_rec)
    finally show ?case by this
  qed

  subsection ‹Expanding set functions to sets of functions›

  definition expand :: "('a ⇒ 'b set) ⇒ ('a ⇒ 'b) set" where
    "expand f = {g. ∀ x. g x ∈ f x}"

  lemma expand_update[simp]:
    assumes "f x ≠ {}"
    shows "expand (f (x := S)) = (⋃ y ∈ S. (λ g. g (x := y)) ` expand f)"
  unfolding expand_def
  proof (intro equalityI subsetI)
    fix g
    assume 1: "g ∈ {g. ∀ y. g y ∈ (f (x := S)) y}"
    have 2: "g x ∈ S" "⋀ y. x ≠ y ⟹ g y ∈ f y" using 1 by (auto split: if_splits)
    obtain y where 3: "y ∈ f x" using assms by auto
    show "g ∈ (⋃ y ∈ S. (λ g. g (x := y)) ` {g. ∀ x. g x ∈ f x})"
    proof (intro UN_I image_eqI)
      show "g x ∈ S" using 2(1) by this
      show "g (x := y) ∈ {g. ∀ x. g x ∈ f x}" using 2 3 by auto
      show "g = g (x := y, x := g x)" by simp
    qed
  next
    fix g
    assume 1: "g ∈ (⋃ y ∈ S. (λ g. g (x := y)) ` {g. ∀ x. g x ∈ f x})"
    show "g ∈ {g. ∀ y. g y ∈ (f (x := S)) y}" using 1 by auto
  qed

  subsection ‹Expanding set maps into sets of maps›

  definition expand_map :: "('a ⇀ 'b set) ⇒ ('a ⇀ 'b) set" where
    "expand_map f ≡ expand (case_option {None} (image Some) ∘ f)"

  lemma expand_map_alt_def: "expand_map f =
    {g. dom g = dom f ∧ (∀ x S y. f x = Some S ⟶ g x = Some y ⟶ y ∈ S)}"
    unfolding expand_map_def expand_def by (auto split: option.splits) (force+)

  lemma expand_map_dom:
    assumes "g ∈ expand_map f"
    shows "dom g = dom f"
    using assms unfolding expand_map_def expand_def by (auto split: option.splits)

  lemma expand_map_empty[simp]: "expand_map Map.empty = {Map.empty}" unfolding expand_map_def expand_def by auto
  lemma expand_map_update[simp]:
    "expand_map (f (x ↦ S)) = (⋃ y ∈ S. (λ g. g (x ↦ y)) ` expand_map (f (x := None)))"
  proof -
    let ?m = "case_option {None} (image Some)"
    have 1: "((?m ∘ f) (x := {None})) x ≠ {}" by simp
    have "expand_map (f (x := Some S)) = expand_map (f (x := None, x := Some S))" by simp
    also have "… = expand ((?m ∘ f) (x := {None}, x := ?m (Some S)))"
      unfolding expand_map_def fun_upd_comp by simp
    also have "… = (⋃ y ∈ ?m (Some S). (λ g. g (x := y)) ` expand ((?m ∘ f) (x := {None})))"
      using expand_update 1 by this
    also have "… = (⋃ y ∈ S. (λ g. g (x ↦ y)) ` expand_map (f (x := None)))"
      unfolding expand_map_def fun_upd_comp by simp
    finally show ?thesis by this
  qed

end