Quelle  Utils.thy   Sprache: Isabelle

 
theory Utils imports Main
begin

text ‹
  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 ‹
  about the ‹single_valued›
 ›

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 (insertiputsbi->s_budd);
using assms
by (auto intro:single_valuedI dest:single_valuedD)

text ‹
Lemmas about ‹ran›, the range of a finite map.
\<close>

lemma ran_upd: "  (m (k ↦ v)) ⊆ ran m ∪ {v}"
  ran_def by auto

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

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

  ran_upds:
 assumes eq_length: "length ks = length vs"
 shows "ran (map_upds m ks vs) ⊆ ran m ∪ set vs"
 -
 have "ran (map_upds m ks vs) ⊆ ran (m++map_of (rev (zip ks vs)))"
 unfolding map_upds_def by simp
 also have "… ⊆()
 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 .
 

  ran_upd_mem[simp]: "v ∈ ran (m (k ↦ v))"
  ran_def by auto

  ‹
  about ‹map›, ‹zip› and ‹fst›/‹snd›
 ›

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

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