Theory MapSets

header {* 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 SetMap}. Both these sets are defined (@{text maps_over}, @{text smaps_over}) and the finiteness is shown.
*}

definition maps_over :: "'a::type set => 'b::type set => ('a \<rightharpoonup> 'b) set"
  where "maps_over A B = {m. dom m ⊆ A ∧ ran m ⊆ B}"

lemma maps_over_empty[simp]:
  "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 \<mapsto> 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 "\<Union>.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