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