Theory MapSets

section ‹Sets of maps›
theory MapSets
imports SetMap Utils
begin

text ‹
In the section about the finiteness of the argument space, we need the fact that the set of maps from a finite domain to a finite range is finite, and the same for the set-valued maps defined in @{theory "Shivers-CFA.SetMap"}. Both these sets are defined (‹maps_over›, ‹smaps_over›) and the finiteness is shown.
›

definition maps_over :: "'a::type set ⇒ 'b::type set ⇒ ('a ⇀ 'b) set"
  where "maps_over A B = {m. dom m ⊆ A ∧ ran m ⊆ B}"

lemma maps_over_empty[simp]:
  "Map.empty ∈ maps_over A B"
unfolding maps_over_def by simp

lemma maps_over_upd:
  assumes "m ∈ maps_over A B"
  and "v ∈ A" and "k ∈ B"
shows "m(v ↦ k) ∈ maps_over A B"
  using assms unfolding maps_over_def
  by (auto dest: subsetD[OF ran_upd])

lemma maps_over_finite[intro]:
  assumes "finite A" and "finite B" shows "finite (maps_over A B)"
proof-
  have inj_map_graph: "inj (λf. {(x, y). Some y = f x})"
  proof (induct rule: inj_onI)
    case (1 x y)
    from "1.hyps"(3) have hyp: "⋀ a b. (Some b = x a) ⟷ (Some b = y a)"
      by (simp add: set_eq_iff)
    show ?case
    proof (rule ext)
    fix z show "x z = y z"
      using hyp[of _ z]
      by (cases "x z", cases "y z", auto)
    qed
  qed

  have "(λf. {(x, y). Some y = f x}) ` maps_over A B ⊆ Pow( A × B )" (is "?graph ⊆ _")
    unfolding maps_over_def
    by (auto dest!:subsetD[of _ A] subsetD[of _ B] intro:ranI)
  moreover
  have "finite (Pow( A × B ))" using assms by auto
  ultimately
  have "finite ?graph" by (rule finite_subset)
  thus ?thesis
    by (rule finite_imageD[OF _ subset_inj_on[OF inj_map_graph subset_UNIV]])
qed

definition smaps_over :: "'a::type set ⇒ 'b::type set ⇒ ('a ⇒ 'b set) set"
  where "smaps_over A B = {m. sdom m ⊆ A ∧ sran m ⊆ B}"

lemma smaps_over_empty[simp]:
  "{}. ∈ smaps_over A B"
unfolding smaps_over_def by simp

lemma smaps_over_singleton:
  assumes "k ∈ A" and "vs ⊆ B"
shows "{k := vs}. ∈ smaps_over A B"
  using assms unfolding smaps_over_def
  by(auto dest: subsetD[OF sdom_singleton])

lemma smaps_over_un:
  assumes "m1 ∈ smaps_over A B" and "m2 ∈ smaps_over A B"
  shows "m1 ∪. m2 ∈ smaps_over A B"
using assms unfolding smaps_over_def
by (auto simp add:smap_union_def)

lemma smaps_over_Union:
  assumes "set ms ⊆ smaps_over A B"
  shows "⋃.ms ∈ smaps_over A B"
using assms
by (induct ms)(auto intro: smaps_over_un)

lemma smaps_over_im:
 "⟦ f ∈ m a ; m ∈ smaps_over A B ⟧ ⟹ f ∈ B"
unfolding smaps_over_def by (auto simp add:sran_def)

lemma smaps_over_finite[intro]: 
  assumes "finite A" and "finite B" shows "finite (smaps_over A B)"
proof-
  have inj_smap_graph: "inj (λf. {(x, y). y = f x ∧ y ≠ {}})" (is "inj ?gr")
  proof (induct rule: inj_onI)
    case (1 x y)
    from "1.hyps"(3) have hyp: "⋀ a b. (b = x a ∧ b ≠ {}) = (b = y a ∧ b ≠ {})"
      by -(subst (asm) (3) set_eq_iff, simp)
    show ?case
    proof (rule ext)
    fix z show "x z = y z"
      using hyp[of _ z]
      by (cases "x z ≠ {}", cases "y z ≠ {}", auto)
    qed
  qed

  have "?gr ` smaps_over A B ⊆ Pow( A × Pow  B )" (is "?graph ⊆ _")
    unfolding smaps_over_def
    by (auto dest!:subsetD[of _ A] subsetD[of _ "Pow B"] sdom_not_mem intro:sranI)
  moreover
  have "finite (Pow( A × Pow B ))" using assms by auto
  ultimately
  have "finite ?graph" by (rule finite_subset)
  thus ?thesis
    by (rule finite_imageD[OF _ subset_inj_on[OF inj_smap_graph subset_UNIV]])
qed

end