# Theory MapSets

Up to index of Isabelle/HOL/HOLCF/Shivers-CFA

theory MapSets
imports SetMap Utils
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)"
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

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