Theory SetMap

section ‹Set-valued maps›
theory SetMap
  imports Main
begin

text ‹
For the abstract semantics, we need methods to work with set-valued maps, i.e.\ functions from a key type to sets of values. For this type, some well known operations are introduced and properties shown, either borrowing the nomenclature from finite maps (‹sdom›, ‹sran›,...) or of sets (‹{}.›, ‹∪.›,...).
›

definition
  sdom :: "('a => 'b set) => 'a set" where
  "sdom m = {a. m a ~= {}}"

definition
  sran :: "('a => 'b set) => 'b set" where
  "sran m = {b. ∃a. b ∈ m a}"

lemma sranI: "b ∈ m a ⟹ b ∈ sran m"
  by(auto simp: sran_def)

lemma sdom_not_mem[elim]: "a ∉ sdom m ⟹ m a = {}"
  by (auto simp: sdom_def)

definition smap_empty (‹{}.›)
 where "{}. k = {}"

definition smap_union :: "('a::type ⇒ 'b::type set)  ⇒ ('a ⇒ 'b set) ⇒ ('a ⇒ 'b set)" (‹_ ∪. _›)
 where "smap1 ∪. smap2 k =  smap1 k ∪ smap2 k"

primrec smap_Union :: "('a::type ⇒ 'b::type set) list ⇒ 'a ⇒ 'b set" (‹⋃._›)
  where [simp]:"⋃. [] = {}."
      | "⋃. (m#ms) = m  ∪. ⋃. ms"

definition smap_singleton :: "'a::type ⇒ 'b::type set ⇒ 'a ⇒ 'b set" (‹{ _ := _}.›)
  where "{k := vs}. = {}. (k := vs)"

definition smap_less :: "('a ⇒ 'b set) ⇒ ('a ⇒ 'b set) ⇒ bool" (‹_/ ⊆. _› [50, 51] 50)
  where "smap_less m1 m2 = (∀k. m1 k ⊆ m2 k)"

lemma sdom_empty[simp]: "sdom {}. = {}"
  unfolding sdom_def smap_empty_def by auto

lemma sdom_singleton[simp]: "sdom {k := vs}. ⊆ {k}"
  by (auto simp add: sdom_def smap_singleton_def smap_empty_def)

lemma sran_singleton[simp]: "sran {k := vs}. = vs"
  by (auto simp add: sran_def smap_singleton_def smap_empty_def)

lemma sran_empty[simp]: "sran {}. = {}"
  unfolding sran_def smap_empty_def by auto

lemma sdom_union[simp]: "sdom (m ∪. n) = sdom m ∪ sdom n"
  by(auto simp add:smap_union_def sdom_def)

lemma sran_union[simp]: "sran (m ∪. n) = sran m ∪ sran n"
  by(auto simp add:smap_union_def sran_def)

lemma smap_empty[simp]: "{}. ⊆. {}."
  unfolding smap_less_def by auto

lemma smap_less_refl: "m ⊆. m"
  unfolding smap_less_def by simp

lemma smap_less_trans[trans]: "⟦ m1 ⊆. m2; m2 ⊆. m3 ⟧ ⟹ m1 ⊆. m3"
  unfolding smap_less_def by auto

lemma smap_union_mono: "⟦ ve1 ⊆. ve1'; ve2 ⊆. ve2' ⟧ ⟹ ve1 ∪. ve2 ⊆. ve1' ∪. ve2'"
  by (auto simp add:smap_less_def smap_union_def)

lemma smap_Union_union: "m1 ∪. ⋃.ms = ⋃.(m1#ms)"
  by (rule ext, auto simp add: smap_union_def smap_Union_def)

lemma smap_Union_mono:
  assumes "list_all2 smap_less ms1 ms2"
  shows "⋃. ms1 ⊆. ⋃. ms2"
using assms 
  by(induct rule:list_induct2[OF list_all2_lengthD[OF assms]])
    (auto intro:smap_union_mono)

lemma smap_singleton_mono: "v ⊆ v' ⟹ {k := v}. ⊆. {k := v'}."
 by (auto simp add: smap_singleton_def smap_less_def)

lemma smap_union_comm: "m1 ∪. m2 = m2 ∪. m1"
by (rule ext,auto simp add:smap_union_def)

lemma smap_union_empty1[simp]: "{}. ∪. m = m"
  by(rule ext, auto simp add:smap_union_def smap_empty_def)

lemma smap_union_empty2[simp]: "m ∪. {}. = m"
  by(rule ext, auto simp add:smap_union_def smap_empty_def)

lemma smap_union_assoc [simp]: "(m1 ∪. m2) ∪. m3 = m1 ∪. (m2 ∪. m3)"
  by (rule ext, auto simp add:smap_union_def)

lemma smap_Union_append[simp]: "⋃. (m1@m2) = (⋃. m1) ∪. (⋃. m2)"
  by (induct m1) auto

lemma smap_Union_rev[simp]: "⋃. (rev l) = ⋃. l"
  by(induct l)(auto simp add:smap_union_comm)

lemma smap_Union_map_rev[simp]: "⋃. (map f (rev l)) = ⋃. (map f l)"
  by(subst rev_map[THEN sym], subst smap_Union_rev, rule refl)

end