Theory Utils

section ‹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 ‹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 ‹ran›, the range of a finite map.
›

lemma ran_upd: "ran (m (k ↦ 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 ↦ v))"
unfolding ran_def by auto

text ‹
Lemmas about ‹map›, ‹zip› and ‹fst›/‹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