# Theory Utils

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

theory Utils
imports Main
header {* General utility lemmas *}
theory Utils imports Main
begin

text {*
This is a potpourri of various lemmas not specific to our project. Some of them could very well be included in the default Isabelle library.
*}

text {*
Lemmas about the @{text single_valued} predicate.
*}

lemma single_valued_empty[simp]:"single_valued {}"
by (rule single_valuedI) auto

lemma single_valued_insert:
assumes "single_valued rel"
and "!! x y . [|(x,y) ∈ rel; x=a|] ==> y = b"
shows "single_valued (insert (a,b) rel)"
using assms
by (auto intro:single_valuedI dest:single_valuedD)

text {*
Lemmas about @{text ran}, the range of a finite map.
*}

lemma ran_upd: "ran (m (k \<mapsto> v)) ⊆ ran m ∪ {v}"
unfolding ran_def by auto

lemma ran_map_of: "ran (map_of xs) ⊆ snd ` set xs"
by (induct xs)(auto simp del:fun_upd_apply dest: ran_upd[THEN subsetD])

lemma ran_concat: "ran (m1 ++ m2) ⊆ ran m1 ∪ ran m2"
unfolding ran_def
by auto

lemma ran_upds:
assumes eq_length: "length ks = length vs"
shows "ran (map_upds m ks vs) ⊆ ran m ∪ set vs"
proof-
have "ran (map_upds m ks vs) ⊆ ran (m++map_of (rev (zip ks vs)))"
unfolding map_upds_def by simp
also have "… ⊆ ran m ∪ ran (map_of (rev (zip ks vs)))" by (rule ran_concat)
also have "… ⊆ ran m ∪ snd ` set (rev (zip ks vs))"
by (intro Un_mono[of "ran m" "ran m"] subset_refl ran_map_of)
also have "…⊆ ran m ∪ set vs"
by (auto intro:Un_mono[of "ran m" "ran m"] subset_refl simp del:set_map simp add:set_map[THEN sym] map_snd_zip[OF eq_length])
finally show ?thesis .
qed

lemma ran_upd_mem[simp]: "v ∈ ran (m (k \<mapsto> v))"
unfolding ran_def by auto

text {*
Lemmas about @{text map}, @{text zip} and @{text fst}/@{text snd}
*}

lemma map_fst_zip: "length xs = length ys ==> map fst (zip xs ys) = xs"
apply (induct xs ys rule:list_induct2) by auto

lemma map_snd_zip: "length xs = length ys ==> map snd (zip xs ys) = ys"
apply (induct xs ys rule:list_induct2) by auto

end