Quelle Map.thy Sprache: Isabelle

(*  Title:      HOL/Map.thy
    Author:     Tobias Nipkow, based on a theory by David von Oheimb
    Copyright   1997-2003 TU Muenchen

The datatype of "maps"; strongly resembles maps in VDM.
*)

section \<open>Maps\<close>

theory Map
  imports List
  abbrevs "(=" = "\\<^sub>m"
begin

type_synonym ('a, 'b) "map" = "'a \ 'b option" (infixr \\\ 0)

abbreviation (input)
  empty :: "'a \ 'b" where
  "empty \ \x. None"

definition
  map_comp :: "('b \ 'c) \ ('a \ 'b) \ ('a \ 'c)" (infixl \\\<^sub>m\ 55) where
  "f \\<^sub>m g = (\k. case g k of None \ None | Some v \ f v)"

definition
  map_add :: "('a \ 'b) \ ('a \ 'b) \ ('a \ 'b)" (infixl \++\ 100) where
  "m1 ++ m2 = (\x. case m2 x of None \ m1 x | Some y \ Some y)"

definition
  restrict_map :: "('a \ 'b) \ 'a set \ ('a \ 'b)" (infixl \|`\ 110) where
  "m|`A = (\x. if x \ A then m x else None)"

notation (latex output)
  restrict_map  (\<open>_\<restriction>\<^bsub>_\<^esub>\<close> [111,110] 110)

definition
  dom :: "('a \ 'b) \ 'a set" where
  "dom m = {a. m a \ None}"

definition
  ran :: "('a \ 'b) \ 'b set" where
  "ran m = {b. \a. m a = Some b}"

definition
  graph :: "('a \ 'b) \ ('a \ 'b) set" where
  "graph m = {(a, b) | a b. m a = Some b}"

definition
  map_le :: "('a \ 'b) \ ('a \ 'b) \ bool" (infix \\\<^sub>m\ 50) where
  "(m\<^sub>1 \\<^sub>m m\<^sub>2) \ (\a \ dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)"

text \<open>Function update syntax \<open>f(x := y, \<dots>)\<close> is extended with \<open>x \<mapsto> y\<close>, which is short for
\<open>x := Some y\<close>. \<open>:=\<close> and \<open>\<mapsto>\<close> can be mixed freely.
The syntax \<open>[x \<mapsto> y, \<dots>]\<close> is short for \<open>Map.empty(x \<mapsto> y, \<dots>)\<close>
but must only contain \<open>\<mapsto>\<close>, not \<open>:=\<close>, because \<open>[x:=y]\<close> clashes with the list update syntax \<open>xs[i:=x]\<close>.\<close>

nonterminal maplet and maplets

open_bundle maplet_syntax
begin

syntax
  "_maplet"  :: "['a, 'a] \ maplet" (\(\open_block notation=\mixfix maplet\\_ /\/ _)\)
  ""         :: "maplet \ updbind" (\_\)
  ""         :: "maplet \ maplets" (\_\)
  "_Maplets" :: "[maplet, maplets] \ maplets" (\_,/ _\)
  "_Map"     :: "maplets \ 'a \ 'b" (\(\indent=1 notation=\mixfix map\\[_])\)
(* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *)

syntax (ASCII)
  "_maplet"  :: "['a, 'a] \ maplet" (\(\open_block notation=\mixfix maplet\\_ /|->/ _)\)

syntax_consts
  "_maplet" "_Maplets" "_Map" \<rightleftharpoons> fun_upd

translations
  "_Update f (_maplet x y)" \<rightleftharpoons> "f(x := CONST Some y)"
  "_Maplets m ms" \<rightharpoonup> "_updbinds m ms"
  "_Map ms" \<rightharpoonup> "_Update (CONST empty) ms"

(* Printing must create \<open>_Map\<close> only for \<open>_maplet\<close> *)
  "_Map (_maplet x y)"  \<leftharpoondown> "_Update (\<lambda>u. CONST None) (_maplet x y)"
  "_Map (_updbinds m (_maplet x y))"  \<leftharpoondown> "_Update (_Map m) (_maplet x y)"

end

text \<open>Updating with lists:\<close>

primrec map_of :: "('a \ 'b) list \ 'a \ 'b" where
  "map_of [] = empty"
| "map_of (p # ps) = (map_of ps)(fst p \ snd p)"

lemma map_of_Cons_code [code]:
  "map_of [] k = None"
  "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
  by simp_all

definition map_upds :: "('a \ 'b) \ 'a list \ 'b list \ 'a \ 'b" where
"map_upds m xs ys = m ++ map_of (rev (zip xs ys))"

text \<open>There is also the more specialized update syntax \<open>xs [\<mapsto>] ys\<close> for lists \<open>xs\<close> and \<open>ys\<close>.\<close>

open_bundle list_maplet_syntax
begin

syntax
  "_maplets"  :: "['a, 'a] \ maplet" (\(\open_block notation=\mixfix maplet\\_ /[\]/ _)\)

syntax (ASCII)
  "_maplets" :: "['a, 'a] \ maplet" (\(\open_block notation=\mixfix maplet\\_ /[|->]/ _)\)

syntax_consts
  "_maplets" \<rightleftharpoons> map_upds

translations
  "_Update m (_maplets xs ys)" \<rightleftharpoons> "CONST map_upds m xs ys"

  "_Map (_maplets xs ys)"  \<leftharpoondown> "_Update (\<lambda>u. CONST None) (_maplets xs ys)"
  "_Map (_updbinds m (_maplets xs ys))"  \<leftharpoondown> "_Update (_Map m) (_maplets xs ys)"

end

subsection \<open>@{term [source] empty}\<close>

lemma empty_upd_none [simp]: "empty(x := None) = empty"
  by (rule ext) simp

subsection \<open>@{term [source] map_upd}\<close>

lemma map_upd_triv: "t k = Some x \ t(k\x) = t"
  by (rule ext) simp

lemma map_upd_nonempty [simp]: "t(k\x) \ empty"
proof
  assume "t(k \ x) = empty"
  then have "(t(k \ x)) k = None" by simp
  then show False by simp
qed

lemma map_upd_eqD1:
  assumes "m(a\x) = n(a\y)"
  shows "x = y"
proof -
  from assms have "(m(a\x)) a = (n(a\y)) a" by simp
  then show ?thesis by simp
qed

lemma map_upd_Some_unfold:
  "((m(a\b)) x = Some y) = (x = a \ b = y \ x \ a \ m x = Some y)"
  by auto

lemma image_map_upd [simp]: "x \ A \ m(x \ y) ` A = m ` A"
  by auto

lemma finite_range_updI:
  assumes "finite (range f)" shows "finite (range (f(a\b)))"
proof -
  have "range (f(a\b)) \ insert (Some b) (range f)"
    by auto
  then show ?thesis
    by (rule finite_subset) (use assms in auto)
qed

subsection \<open>@{term [source] map_of}\<close>

lemma map_of_eq_empty_iff [simp]:
  "map_of xys = empty \ xys = []"
proof
  show "map_of xys = empty \ xys = []"
    by (induction xys) simp_all
qed simp

lemma empty_eq_map_of_iff [simp]:
  "empty = map_of xys \ xys = []"
by(subst eq_commute) simp

lemma map_of_eq_None_iff:
  "(map_of xys x = None) = (x \ fst ` (set xys))"
by (induct xys) simp_all

lemma map_of_eq_Some_iff [simp]:
  "distinct(map fst xys) \ (map_of xys x = Some y) = ((x,y) \ set xys)"
proof (induct xys)
  case (Cons xy xys)
  then show ?case
    by (cases xy) (auto simp flip: map_of_eq_None_iff)
qed auto

lemma Some_eq_map_of_iff [simp]:
  "distinct(map fst xys) \ (Some y = map_of xys x) = ((x,y) \ set xys)"
by (auto simp del: map_of_eq_Some_iff simp: map_of_eq_Some_iff [symmetric])

lemma map_of_is_SomeI [simp]:
  "\distinct(map fst xys); (x,y) \ set xys\ \ map_of xys x = Some y"
  by simp

lemma map_of_zip_is_None [simp]:
  "length xs = length ys \ (map_of (zip xs ys) x = None) = (x \ set xs)"
by (induct rule: list_induct2) simp_all

lemma map_of_zip_is_Some:
  assumes "length xs = length ys"
  shows "x \ set xs \ (\y. map_of (zip xs ys) x = Some y)"
using assms by (induct rule: list_induct2) simp_all

lemma map_of_zip_upd:
  fixes x :: 'a and xs :: "'a list" and ys zs :: "'b list"
  assumes "length ys = length xs"
    and "length zs = length xs"
    and "x \ set xs"
    and "(map_of (zip xs ys))(x \ y) = (map_of (zip xs zs))(x \ z)"
  shows "map_of (zip xs ys) = map_of (zip xs zs)"
proof
  fix x' :: 'a
  show "map_of (zip xs ys) x' = map_of (zip xs zs) x'"
  proof (cases "x = x'")
    case True
    from assms True map_of_zip_is_None [of xs ys x']
      have "map_of (zip xs ys) x' = None" by simp
    moreover from assms True map_of_zip_is_None [of xs zs x']
      have "map_of (zip xs zs) x' = None" by simp
    ultimately show ?thesis by simp
  next
    case False from assms
      have "((map_of (zip xs ys))(x \ y)) x' = ((map_of (zip xs zs))(x \ z)) x'" by auto
    with False show ?thesis by simp
  qed
qed

lemma map_of_zip_inject:
  assumes "length ys = length xs"
    and "length zs = length xs"
    and dist: "distinct xs"
    and map_of: "map_of (zip xs ys) = map_of (zip xs zs)"
  shows "ys = zs"
  using assms(1) assms(2)[symmetric]
  using dist map_of
proof (induct ys xs zs rule: list_induct3)
  case Nil show ?case by simp
next
  case (Cons y ys x xs z zs)
  from \<open>map_of (zip (x#xs) (y#ys)) = map_of (zip (x#xs) (z#zs))\<close>
    have map_of: "(map_of (zip xs ys))(x \ y) = (map_of (zip xs zs))(x \ z)" by simp
  from Cons have "length ys = length xs" and "length zs = length xs"
    and "x \ set xs" by simp_all
  then have "map_of (zip xs ys) = map_of (zip xs zs)" using map_of by (rule map_of_zip_upd)
  with Cons.hyps \<open>distinct (x # xs)\<close> have "ys = zs" by simp
  moreover from map_of have "y = z" by (rule map_upd_eqD1)
  ultimately show ?case by simp
qed

lemma map_of_zip_nth:
  assumes "length xs = length ys"
  assumes "distinct xs"
  assumes "i < length ys"
  shows "map_of (zip xs ys) (xs ! i) = Some (ys ! i)"
using assms proof (induct arbitrary: i rule: list_induct2)
  case Nil
  then show ?case by simp
next
  case (Cons x xs y ys)
  then show ?case
    using less_Suc_eq_0_disj by auto
qed

lemma map_of_zip_map:
  "map_of (zip xs (map f xs)) = (\x. if x \ set xs then Some (f x) else None)"
  by (induct xs) (simp_all add: fun_eq_iff)

lemma finite_range_map_of: "finite (range (map_of xys))"
proof (induct xys)
  case (Cons a xys)
  then show ?case
    using finite_range_updI by fastforce
qed auto

lemma map_of_SomeD: "map_of xs k = Some y \ (k, y) \ set xs"
  by (induct xs) (auto split: if_splits)

lemma map_of_mapk_SomeI:
  "inj f \ map_of t k = Some x \
   map_of (map (case_prod (\<lambda>k. Pair (f k))) t) (f k) = Some x"
by (induct t) (auto simp: inj_eq)

lemma weak_map_of_SomeI: "(k, x) \ set l \ \x. map_of l k = Some x"
by (induct l) auto

lemma map_of_filter_in:
  "map_of xs k = Some z \ P k z \ map_of (filter (case_prod P) xs) k = Some z"
by (induct xs) auto

lemma map_of_map:
  "map_of (map (\(k, v). (k, f v)) xs) = map_option f \ map_of xs"
  by (induct xs) (auto simp: fun_eq_iff)

lemma map_of_filter:
  "map_of (filter (\x. P (fst x)) xs) = map_of xs |` Collect P"
  by (induct xs) (simp_all add: fun_eq_iff restrict_map_def)

lemma dom_map_option:
  "dom (\k. map_option (f k) (m k)) = dom m"
  by (simp add: dom_def)

lemma dom_map_option_comp [simp]:
  "dom (map_option g \ m) = dom m"
  using dom_map_option [of "\_. g" m] by (simp add: comp_def)

subsection \<open>\<^const>\<open>map_option\<close> related\<close>

lemma map_option_o_empty [simp]: "map_option f \ empty = empty"
by (rule ext) simp

lemma map_option_o_map_upd [simp]:
  "map_option f \ m(a\b) = (map_option f \ m)(a\f b)"
by (rule ext) simp

subsection \<open>@{term [source] map_comp} related\<close>

lemma map_comp_empty [simp]:
  "m \\<^sub>m empty = empty"
  "empty \\<^sub>m m = empty"
by (auto simp: map_comp_def split: option.splits)

lemma map_comp_simps [simp]:
  "m2 k = None \ (m1 \\<^sub>m m2) k = None"
  "m2 k = Some k' \ (m1 \\<^sub>m m2) k = m1 k'"
by (auto simp: map_comp_def)

lemma map_comp_Some_iff:
  "((m1 \\<^sub>m m2) k = Some v) = (\k'. m2 k = Some k' \ m1 k' = Some v)"
by (auto simp: map_comp_def split: option.splits)

lemma map_comp_None_iff:
  "((m1 \\<^sub>m m2) k = None) = (m2 k = None \ (\k'. m2 k = Some k' \ m1 k' = None)) "
by (auto simp: map_comp_def split: option.splits)

subsection \<open>\<open>++\<close>\<close>

lemma map_add_empty[simp]: "m ++ empty = m"
by(simp add: map_add_def)

lemma empty_map_add[simp]: "empty ++ m = m"
by (rule ext) (simp add: map_add_def split: option.split)

lemma map_add_assoc[simp]: "m1 ++ (m2 ++ m3) = (m1 ++ m2) ++ m3"
by (rule ext) (simp add: map_add_def split: option.split)

lemma map_add_Some_iff:
  "((m ++ n) k = Some x) = (n k = Some x \ n k = None \ m k = Some x)"
by (simp add: map_add_def split: option.split)

lemma map_add_SomeD [dest!]:
  "(m ++ n) k = Some x \ n k = Some x \ n k = None \ m k = Some x"
by (rule map_add_Some_iff [THEN iffD1])

lemma map_add_find_right [simp]: "n k = Some xx \ (m ++ n) k = Some xx"
by (subst map_add_Some_iff) fast

lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None \ m k = None)"
by (simp add: map_add_def split: option.split)

lemma map_add_upd[simp]: "f ++ g(x\y) = (f ++ g)(x\y)"
by (rule ext) (simp add: map_add_def)

lemma map_add_upds[simp]: "m1 ++ (m2(xs[\]ys)) = (m1++m2)(xs[\]ys)"
by (simp add: map_upds_def)

lemma map_add_upd_left: "m\dom e2 \ e1(m \ u1) ++ e2 = (e1 ++ e2)(m \ u1)"
by (rule ext) (auto simp: map_add_def dom_def split: option.split)

lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
  unfolding map_add_def
proof (induct xs)
  case (Cons a xs)
  then show ?case
    by (force split: option.split)
qed auto

lemma finite_range_map_of_map_add:
  "finite (range f) \ finite (range (f ++ map_of l))"
proof (induct l)
case (Cons a l)
  then show ?case
    by (metis finite_range_updI map_add_upd map_of.simps(2))
qed auto

lemma inj_on_map_add_dom [iff]:
  "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
  by (fastforce simp: map_add_def dom_def inj_on_def split: option.splits)

lemma map_upds_fold_map_upd:
  "m(ks[\]vs) = foldl (\m (k, v). m(k \ v)) m (zip ks vs)"
unfolding map_upds_def proof (rule sym, rule zip_obtain_same_length)
  fix ks :: "'a list" and vs :: "'b list"
  assume "length ks = length vs"
  then show "foldl (\m (k, v). m(k\v)) m (zip ks vs) = m ++ map_of (rev (zip ks vs))"
    by(induct arbitrary: m rule: list_induct2) simp_all
qed

lemma map_add_map_of_foldr:
  "m ++ map_of ps = foldr (\(k, v) m. m(k \ v)) ps m"
  by (induct ps) (auto simp: fun_eq_iff map_add_def)

subsection \<open>@{term [source] restrict_map}\<close>

lemma restrict_map_to_empty [simp]: "m|`{} = empty"
  by (simp add: restrict_map_def)

lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
  by (auto simp: restrict_map_def)

lemma restrict_map_empty [simp]: "empty|`D = empty"
  by (simp add: restrict_map_def)

lemma restrict_in [simp]: "x \ A \ (m|`A) x = m x"
  by (simp add: restrict_map_def)

lemma restrict_out [simp]: "x \ A \ (m|`A) x = None"
  by (simp add: restrict_map_def)

lemma ran_restrictD: "y \ ran (m|`A) \ \x\A. m x = Some y"
  by (auto simp: restrict_map_def ran_def split: if_split_asm)

lemma dom_restrict [simp]: "dom (m|`A) = dom m \ A"
  by (auto simp: restrict_map_def dom_def split: if_split_asm)

lemma restrict_upd_same [simp]: "m(x\y)|`(-{x}) = m|`(-{x})"
  by (rule ext) (auto simp: restrict_map_def)

lemma restrict_restrict [simp]: "m|`A|`B = m|`(A\B)"
  by (rule ext) (auto simp: restrict_map_def)

lemma restrict_fun_upd [simp]:
  "m(x := y)|`D = (if x \ D then (m|`(D-{x}))(x := y) else m|`D)"
  by (simp add: restrict_map_def fun_eq_iff)

lemma fun_upd_None_restrict [simp]:
  "(m|`D)(x := None) = (if x \ D then m|`(D - {x}) else m|`D)"
  by (simp add: restrict_map_def fun_eq_iff)

lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
  by (simp add: restrict_map_def fun_eq_iff)

lemma fun_upd_restrict_conv [simp]:
  "x \ D \ (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
  by (rule fun_upd_restrict)

lemma map_of_map_restrict:
  "map_of (map (\k. (k, f k)) ks) = (Some \ f) |` set ks"
  by (induct ks) (simp_all add: fun_eq_iff restrict_map_insert)

lemma restrict_complement_singleton_eq:
  "f |` (- {x}) = f(x := None)"
  by auto

subsection \<open>@{term [source] map_upds}\<close>

lemma map_upds_Nil1 [simp]: "m([] [\] bs) = m"
  by (simp add: map_upds_def)

lemma map_upds_Nil2 [simp]: "m(as [\] []) = m"
  by (simp add:map_upds_def)

lemma map_upds_Cons [simp]: "m(a#as [\] b#bs) = (m(a\b))(as[\]bs)"
  by (simp add:map_upds_def)

lemma map_upds_append1 [simp]:
  "size xs < size ys \ m(xs@[x] [\] ys) = m(xs [\] ys, x \ ys!size xs)"
proof (induct xs arbitrary: ys m)
  case Nil
  then show ?case
    by (auto simp: neq_Nil_conv)
next
  case (Cons a xs)
  then show ?case
    by (cases ys) auto
qed

lemma map_upds_list_update2_drop [simp]:
  "size xs \ i \ m(xs[\]ys[i:=y]) = m(xs[\]ys)"
proof (induct xs arbitrary: m ys i)
  case Nil
  then show ?case
    by auto
next
  case (Cons a xs)
  then show ?case
    by (cases ys) (use Cons in \<open>auto split: nat.split\<close>)
qed

text \<open>Something weirdly sensitive about this proof, which needs only four lines in apply style\<close>
lemma map_upd_upds_conv_if:
  "(f(x\y))(xs [\] ys) =
   (if x \<in> set(take (length ys) xs) then f(xs [\<mapsto>] ys)
                                    else (f(xs [\<mapsto>] ys))(x\<mapsto>y))"
proof (induct xs arbitrary: x y ys f)
  case (Cons a xs)
  show ?case
  proof (cases ys)
    case (Cons z zs)
    then show ?thesis
      using Cons.hyps
      apply (auto split: if_split simp: fun_upd_twist)
      using Cons.hyps apply fastforce+
      done
  qed auto
qed auto

lemma map_upds_twist [simp]:
  "a \ set as \ m(a\b, as[\]bs) = m(as[\]bs, a\b)"
using set_take_subset by (fastforce simp add: map_upd_upds_conv_if)

lemma map_upds_apply_nontin [simp]:
  "x \ set xs \ (f(xs[\]ys)) x = f x"
proof (induct xs arbitrary: ys)
  case (Cons a xs)
  then show ?case
    by (cases ys) (auto simp: map_upd_upds_conv_if)
qed auto

lemma fun_upds_append_drop [simp]:
  "size xs = size ys \ m(xs@zs[\]ys) = m(xs[\]ys)"
proof (induct xs arbitrary: ys)
  case (Cons a xs)
  then show ?case
    by (cases ys) (auto simp: map_upd_upds_conv_if)
qed auto

lemma fun_upds_append2_drop [simp]:
  "size xs = size ys \ m(xs[\]ys@zs) = m(xs[\]ys)"
proof (induct xs arbitrary: ys)
  case (Cons a xs)
  then show ?case
    by (cases ys) (auto simp: map_upd_upds_conv_if)
qed auto

lemma restrict_map_upds[simp]:
  "\ length xs = length ys; set xs \ D \
    \<Longrightarrow> m(xs [\<mapsto>] ys)|`D = (m|`(D - set xs))(xs [\<mapsto>] ys)"
proof (induct xs arbitrary: m ys)
  case (Cons a xs)
  then show ?case
  proof (cases ys)
    case (Cons z zs)
    with Cons.hyps Cons.prems show ?thesis
      apply (simp add: insert_absorb flip: Diff_insert)
      apply (auto simp add: map_upd_upds_conv_if)
      done
  qed auto
qed auto

subsection \<open>@{term [source] dom}\<close>

lemma dom_eq_empty_conv [simp]: "dom f = {} \ f = empty"
  by (auto simp: dom_def)

lemma domI: "m a = Some b \ a \ dom m"
  by (simp add: dom_def)
(* declare domI [intro]? *)

lemma domD: "a \ dom m \ \b. m a = Some b"
  by (cases "m a") (auto simp add: dom_def)

lemma domIff [iff, simp del, code_unfold]: "a \ dom m \ m a \ None"
  by (simp add: dom_def)

lemma dom_empty [simp]: "dom empty = {}"
  by (simp add: dom_def)

lemma dom_fun_upd [simp]:
  "dom(f(x := y)) = (if y = None then dom f - {x} else insert x (dom f))"
  by (auto simp: dom_def)

lemma dom_if:
  "dom (\x. if P x then f x else g x) = dom f \ {x. P x} \ dom g \ {x. \ P x}"
  by (auto split: if_splits)

lemma dom_map_of_conv_image_fst:
  "dom (map_of xys) = fst ` set xys"
  by (induct xys) (auto simp add: dom_if)

lemma dom_map_of_zip [simp]: "length xs = length ys \ dom (map_of (zip xs ys)) = set xs"
  by (induct rule: list_induct2) (auto simp: dom_if)

lemma finite_dom_map_of: "finite (dom (map_of l))"
  by (induct l) (auto simp: dom_def insert_Collect [symmetric])

lemma dom_map_upds [simp]:
  "dom(m(xs[\]ys)) = set(take (length ys) xs) \ dom m"
proof (induct xs arbitrary: ys)
  case (Cons a xs)
  then show ?case
    by (cases ys) (auto simp: map_upd_upds_conv_if)
qed auto

lemma dom_map_add [simp]: "dom (m ++ n) = dom n \ dom m"
  by (auto simp: dom_def)

lemma dom_override_on [simp]:
  "dom (override_on f g A) =
    (dom f  - {a. a \<in> A - dom g}) \<union> {a. a \<in> A \<inter> dom g}"
  by (auto simp: dom_def override_on_def)

lemma map_add_comm: "dom m1 \ dom m2 = {} \ m1 ++ m2 = m2 ++ m1"
  by (rule ext) (force simp: map_add_def dom_def split: option.split)

lemma map_add_dom_app_simps:
  "m \ dom l2 \ (l1 ++ l2) m = l2 m"
  "m \ dom l1 \ (l1 ++ l2) m = l2 m"
  "m \ dom l2 \ (l1 ++ l2) m = l1 m"
  by (auto simp add: map_add_def split: option.split_asm)

lemma dom_const [simp]:
  "dom (\x. Some (f x)) = UNIV"
  by auto

(* Due to John Matthews - could be rephrased with dom *)
lemma finite_map_freshness:
  "finite (dom (f :: 'a \ 'b)) \ \ finite (UNIV :: 'a set) \
   \<exists>x. f x = None"
  by (bestsimp dest: ex_new_if_finite)

lemma dom_minus:
  "f x = None \ dom f - insert x A = dom f - A"
  unfolding dom_def by simp

lemma insert_dom:
  "f x = Some y \ insert x (dom f) = dom f"
  unfolding dom_def by auto

lemma map_of_map_keys:
  "set xs = dom m \ map_of (map (\k. (k, the (m k))) xs) = m"
  by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def)

lemma map_of_eqI:
  assumes set_eq: "set (map fst xs) = set (map fst ys)"
  assumes map_eq: "\k\set (map fst xs). map_of xs k = map_of ys k"
  shows "map_of xs = map_of ys"
proof (rule ext)
  fix k show "map_of xs k = map_of ys k"
  proof (cases "map_of xs k")
    case None
    then have "k \ set (map fst xs)" by (simp add: map_of_eq_None_iff)
    with set_eq have "k \ set (map fst ys)" by simp
    then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
    with None show ?thesis by simp
  next
    case (Some v)
    then have "k \ set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
    with map_eq show ?thesis by auto
  qed
qed

lemma map_of_eq_dom:
  assumes "map_of xs = map_of ys"
  shows "fst ` set xs = fst ` set ys"
proof -
  from assms have "dom (map_of xs) = dom (map_of ys)" by simp
  then show ?thesis by (simp add: dom_map_of_conv_image_fst)
qed

lemma finite_set_of_finite_maps:
  assumes "finite A" "finite B"
  shows "finite {m. dom m = A \ ran m \ B}" (is "finite ?S")
proof -
  let ?S' = "{m. \x. (x \ A \ m x \ Some ` B) \ (x \ A \ m x = None)}"
  have "?S = ?S'"
  proof
    show "?S \ ?S'" by (auto simp: dom_def ran_def image_def)
    show "?S' \ ?S"
    proof
      fix m assume "m \ ?S'"
      hence 1: "dom m = A" by force
      hence 2: "ran m \ B" using \m \ ?S'\ by (auto simp: dom_def ran_def)
      from 1 2 show "m \ ?S" by blast
    qed
  qed
  with assms show ?thesis by(simp add: finite_set_of_finite_funs)
qed

subsection \<open>@{term [source] ran}\<close>

lemma ranI: "m a = Some b \ b \ ran m"
  by (auto simp: ran_def)
(* declare ranI [intro]? *)

lemma ran_empty [simp]: "ran empty = {}"
  by (auto simp: ran_def)

lemma ran_map_upd [simp]:  "m a = None \ ran(m(a\b)) = insert b (ran m)"
  unfolding ran_def
  by force

lemma fun_upd_None_if_notin_dom[simp]: "k \ dom m \ m(k := None) = m"
  by auto

lemma ran_map_upd_Some:
  "\ m x = Some y; inj_on m (dom m); z \ ran m \ \ ran(m(x := Some z)) = ran m - {y} \ {z}"
by(force simp add: ran_def domI inj_onD)

lemma ran_map_add:
  assumes "dom m1 \ dom m2 = {}"
  shows "ran (m1 ++ m2) = ran m1 \ ran m2"
proof
  show "ran (m1 ++ m2) \ ran m1 \ ran m2"
    unfolding ran_def by auto
next
  show "ran m1 \ ran m2 \ ran (m1 ++ m2)"
  proof -
    have "(m1 ++ m2) x = Some y" if "m1 x = Some y" for x y
      using assms map_add_comm that by fastforce
    moreover have "(m1 ++ m2) x = Some y" if "m2 x = Some y" for x y
      using assms that by auto
    ultimately show ?thesis
      unfolding ran_def by blast
  qed
qed

lemma finite_ran:
  assumes "finite (dom p)"
  shows "finite (ran p)"
proof -
  have "ran p = (\x. the (p x)) ` dom p"
    unfolding ran_def by force
  from this \<open>finite (dom p)\<close> show ?thesis by auto
qed

lemma ran_distinct:
  assumes dist: "distinct (map fst al)"
  shows "ran (map_of al) = snd ` set al"
  using assms
proof (induct al)
  case Nil
  then show ?case by simp
next
  case (Cons kv al)
  then have "ran (map_of al) = snd ` set al" by simp
  moreover from Cons.prems have "map_of al (fst kv) = None"
    by (simp add: map_of_eq_None_iff)
  ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
qed

lemma ran_map_of_zip:
  assumes "length xs = length ys" "distinct xs"
  shows "ran (map_of (zip xs ys)) = set ys"
using assms by (simp add: ran_distinct set_map[symmetric])

lemma ran_map_option: "ran (\x. map_option f (m x)) = f ` ran m"
  by (auto simp add: ran_def)

subsection \<open>@{term [source] graph}\<close>

lemma graph_empty[simp]: "graph empty = {}"
  unfolding graph_def by simp

lemma in_graphI: "m k = Some v \ (k, v) \ graph m"
  unfolding graph_def by blast

lemma in_graphD: "(k, v) \ graph m \ m k = Some v"
  unfolding graph_def by blast

lemma graph_map_upd[simp]: "graph (m(k \ v)) = insert (k, v) (graph (m(k := None)))"
  unfolding graph_def by (auto split: if_splits)

lemma graph_fun_upd_None: "graph (m(k := None)) = {e \ graph m. fst e \ k}"
  unfolding graph_def by (auto split: if_splits)

lemma graph_restrictD:
  assumes "(k, v) \ graph (m |` A)"
  shows "k \ A" and "m k = Some v"
  using assms unfolding graph_def
  by (auto simp: restrict_map_def split: if_splits)

lemma graph_map_comp[simp]: "graph (m1 \\<^sub>m m2) = graph m2 O graph m1"
  unfolding graph_def by (auto simp: map_comp_Some_iff relcomp_unfold)

lemma graph_map_add: "dom m1 \ dom m2 = {} \ graph (m1 ++ m2) = graph m1 \ graph m2"
  unfolding graph_def using map_add_comm by force

lemma graph_eq_to_snd_dom: "graph m = (\x. (x, the (m x))) ` dom m"
  unfolding graph_def dom_def by force

lemma fst_graph_eq_dom: "fst ` graph m = dom m"
  unfolding graph_eq_to_snd_dom by force

lemma graph_domD: "x \ graph m \ fst x \ dom m"
  using fst_graph_eq_dom by (metis imageI)

lemma snd_graph_ran: "snd ` graph m = ran m"
  unfolding graph_def ran_def by force

lemma graph_ranD: "x \ graph m \ snd x \ ran m"
  using snd_graph_ran by (metis imageI)

lemma finite_graph_map_of: "finite (graph (map_of al))"
  unfolding graph_eq_to_snd_dom finite_dom_map_of
  using finite_dom_map_of by blast

lemma graph_map_of_if_distinct_dom: "distinct (map fst al) \ graph (map_of al) = set al"
  unfolding graph_def by auto

lemma finite_graph_iff_finite_dom[simp]: "finite (graph m) = finite (dom m)"
  by (metis graph_eq_to_snd_dom finite_imageI fst_graph_eq_dom)

lemma inj_on_fst_graph: "inj_on fst (graph m)"
  unfolding graph_def inj_on_def by force

subsection \<open>\<open>map_le\<close>\<close>

lemma map_le_empty [simp]: "empty \\<^sub>m g"
  by (simp add: map_le_def)

lemma upd_None_map_le [simp]: "f(x := None) \\<^sub>m f"
  by (force simp add: map_le_def)

lemma map_le_upd[simp]: "f \\<^sub>m g ==> f(a := b) \\<^sub>m g(a := b)"
  by (fastforce simp add: map_le_def)

lemma map_le_imp_upd_le [simp]: "m1 \\<^sub>m m2 \ m1(x := None) \\<^sub>m m2(x \ y)"
  by (force simp add: map_le_def)

lemma map_le_upds [simp]:
  "f \\<^sub>m g \ f(as [\] bs) \\<^sub>m g(as [\] bs)"
proof (induct as arbitrary: f g bs)
  case (Cons a as)
  then show ?case
    by (cases bs) (use Cons in auto)
qed auto

lemma map_le_implies_dom_le: "(f \\<^sub>m g) \ (dom f \ dom g)"
  by (fastforce simp add: map_le_def dom_def)

lemma map_le_refl [simp]: "f \\<^sub>m f"
  by (simp add: map_le_def)

lemma map_le_trans[trans]: "\ m1 \\<^sub>m m2; m2 \\<^sub>m m3\ \ m1 \\<^sub>m m3"
  by (auto simp add: map_le_def dom_def)

lemma map_le_antisym: "\ f \\<^sub>m g; g \\<^sub>m f \ \ f = g"
  unfolding map_le_def
  by (metis ext domIff)

lemma map_le_map_add [simp]: "f \\<^sub>m g ++ f"
  by (fastforce simp: map_le_def)

lemma map_le_iff_map_add_commute: "f \\<^sub>m f ++ g \ f ++ g = g ++ f"
  by (fastforce simp: map_add_def map_le_def fun_eq_iff split: option.splits)

lemma map_add_le_mapE: "f ++ g \\<^sub>m h \ g \\<^sub>m h"
  by (fastforce simp: map_le_def map_add_def dom_def)

lemma map_add_le_mapI: "\ f \\<^sub>m h; g \\<^sub>m h \ \ f ++ g \\<^sub>m h"
  by (auto simp: map_le_def map_add_def dom_def split: option.splits)

lemma map_add_subsumed1: "f \\<^sub>m g \ f++g = g"
by (simp add: map_add_le_mapI map_le_antisym)

lemma map_add_subsumed2: "f \\<^sub>m g \ g++f = g"
by (metis map_add_subsumed1 map_le_iff_map_add_commute)

lemma dom_eq_singleton_conv: "dom f = {x} \ (\v. f = [x \ v])"
  (is "?lhs \ ?rhs")
proof
  assume ?rhs
  then show ?lhs by (auto split: if_split_asm)
next
  assume ?lhs
  then obtain v where v: "f x = Some v" by auto
  show ?rhs
  proof
    show "f = [x \ v]"
    proof (rule map_le_antisym)
      show "[x \ v] \\<^sub>m f"
        using v by (auto simp add: map_le_def)
      show "f \\<^sub>m [x \ v]"
        using \<open>dom f = {x}\<close> \<open>f x = Some v\<close> by (auto simp add: map_le_def)
    qed
  qed
qed

lemma map_add_eq_empty_iff[simp]:
  "(f++g = empty) \ f = empty \ g = empty"
by (metis map_add_None)

lemma empty_eq_map_add_iff[simp]:
  "(empty = f++g) \ f = empty \ g = empty"
by(subst map_add_eq_empty_iff[symmetric])(rule eq_commute)

subsection \<open>Various\<close>

lemma set_map_of_compr:
  assumes distinct: "distinct (map fst xs)"
  shows "set xs = {(k, v). map_of xs k = Some v}"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  obtain k v where "x = (k, v)" by (cases x) blast
  with Cons.prems have "k \ dom (map_of xs)"
    by (simp add: dom_map_of_conv_image_fst)
  then have *: "insert (k, v) {(k, v). map_of xs k = Some v} =
    {(k', v'). ((map_of xs)(k \<mapsto> v)) k' = Some v'}"
    by (auto split: if_splits)
  from Cons have "set xs = {(k, v). map_of xs k = Some v}" by simp
  with * \<open>x = (k, v)\<close> show ?case by simp
qed

lemma eq_key_imp_eq_value:
  "v1 = v2"
  if "distinct (map fst xs)" "(k, v1) \ set xs" "(k, v2) \ set xs"
proof -
  from that have "inj_on fst (set xs)"
    by (simp add: distinct_map)
  moreover have "fst (k, v1) = fst (k, v2)"
    by simp
  ultimately have "(k, v1) = (k, v2)"
    by (rule inj_onD) (fact that)+
  then show ?thesis
    by simp
qed

lemma map_of_inject_set:
  assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
  shows "map_of xs = map_of ys \ set xs = set ys" (is "?lhs \ ?rhs")
proof
  assume ?lhs
  moreover from \<open>distinct (map fst xs)\<close> have "set xs = {(k, v). map_of xs k = Some v}"
    by (rule set_map_of_compr)
  moreover from \<open>distinct (map fst ys)\<close> have "set ys = {(k, v). map_of ys k = Some v}"
    by (rule set_map_of_compr)
  ultimately show ?rhs by simp
next
  assume ?rhs show ?lhs
  proof
    fix k
    show "map_of xs k = map_of ys k"
    proof (cases "map_of xs k")
      case None
      with \<open>?rhs\<close> have "map_of ys k = None"
        by (simp add: map_of_eq_None_iff)
      with None show ?thesis by simp
    next
      case (Some v)
      with distinct \<open>?rhs\<close> have "map_of ys k = Some v"
        by simp
      with Some show ?thesis by simp
    qed
  qed
qed

lemma finite_Map_induct[consumes 1, case_names empty update]:
  assumes "finite (dom m)"
  assumes "P Map.empty"
  assumes "\k v m. finite (dom m) \ k \ dom m \ P m \ P (m(k \ v))"
  shows "P m"
  using assms(1)
proof(induction "dom m" arbitrary: m rule: finite_induct)
  case empty
  then show ?case using assms(2) unfolding dom_def by simp
next
  case (insert x F)
  then have "finite (dom (m(x:=None)))" "x \ dom (m(x:=None))" "P (m(x:=None))"
    by (metis Diff_insert_absorb dom_fun_upd)+
  with assms(3)[OF this] show ?case
    by (metis fun_upd_triv fun_upd_upd option.exhaust)
qed

hide_const (open) Map.empty Map.graph

end

quality99%

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.