# Theory SetMap

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

theory SetMap
imports Main
`header {* Set-valued maps *}theory SetMap  imports Mainbegintext {*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 (@{text sdom}, @{text sran},...) or of sets (@{text "{}."}, @{text "∪."},...).*}definition  sdom :: "('a => 'b set) => 'a set" where  "sdom m = {a. m a ~= {}}"definition  sran :: "('a => 'b set) => 'b set" where  "sran m = {b. EX 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" ("\<Union>._")  where [simp]:"\<Union>. [] = {}."      | "\<Union>. (m#ms) = m  ∪. \<Union>. 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 autolemma 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 autolemma 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 autolemma smap_less_refl: "m ⊆. m"  unfolding smap_less_def by simplemma smap_less_trans[trans]: "[| m1 ⊆. m2; m2 ⊆. m3 |] ==> m1 ⊆. m3"  unfolding smap_less_def by autolemma 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 ∪. \<Union>.ms = \<Union>.(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 "\<Union>. ms1 ⊆. \<Union>. 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]: "\<Union>. (m1@m2) = (\<Union>. m1) ∪. (\<Union>. m2)"  by (induct m1) autolemma smap_Union_rev[simp]: "\<Union>. (rev l) = \<Union>. l"  by(induct l)(auto simp add:smap_union_comm)lemma smap_Union_map_rev[simp]: "\<Union>. (map f (rev l)) = \<Union>. (map f l)"  by(subst rev_map[THEN sym], subst smap_Union_rev, rule refl)end`