src/HOL/Map.thy
changeset 35565 56b070cd7ab3
parent 35553 a8c8008a2c9d
child 35607 896f01fe825b
     1.1 --- a/src/HOL/Map.thy	Wed Mar 03 20:20:41 2010 -0800
     1.2 +++ b/src/HOL/Map.thy	Thu Mar 04 11:22:06 2010 +0100
     1.3 @@ -11,11 +11,11 @@
     1.4  imports List
     1.5  begin
     1.6  
     1.7 -types ('a,'b) "~=>" = "'a => 'b option"  (infixr "~=>" 0)
     1.8 +types ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0)
     1.9  translations (type) "'a ~=> 'b" <= (type) "'a => 'b option"
    1.10  
    1.11  type_notation (xsymbols)
    1.12 -  "~=>"  (infixr "\<rightharpoonup>" 0)
    1.13 +  "map" (infixr "\<rightharpoonup>" 0)
    1.14  
    1.15  abbreviation
    1.16    empty :: "'a ~=> 'b" where
    1.17 @@ -650,5 +650,52 @@
    1.18    thus "\<exists>v. f = [x \<mapsto> v]" by blast
    1.19  qed
    1.20  
    1.21 +
    1.22 +subsection {* Various *}
    1.23 +
    1.24 +lemma set_map_of_compr:
    1.25 +  assumes distinct: "distinct (map fst xs)"
    1.26 +  shows "set xs = {(k, v). map_of xs k = Some v}"
    1.27 +using assms proof (induct xs)
    1.28 +  case Nil then show ?case by simp
    1.29 +next
    1.30 +  case (Cons x xs)
    1.31 +  obtain k v where "x = (k, v)" by (cases x) blast
    1.32 +  with Cons.prems have "k \<notin> dom (map_of xs)"
    1.33 +    by (simp add: dom_map_of_conv_image_fst)
    1.34 +  then have *: "insert (k, v) {(k, v). map_of xs k = Some v} =
    1.35 +    {(k', v'). (map_of xs(k \<mapsto> v)) k' = Some v'}"
    1.36 +    by (auto split: if_splits)
    1.37 +  from Cons have "set xs = {(k, v). map_of xs k = Some v}" by simp
    1.38 +  with * `x = (k, v)` show ?case by simp
    1.39 +qed
    1.40 +
    1.41 +lemma map_of_inject_set:
    1.42 +  assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
    1.43 +  shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys" (is "?lhs \<longleftrightarrow> ?rhs")
    1.44 +proof
    1.45 +  assume ?lhs
    1.46 +  moreover from `distinct (map fst xs)` have "set xs = {(k, v). map_of xs k = Some v}"
    1.47 +    by (rule set_map_of_compr)
    1.48 +  moreover from `distinct (map fst ys)` have "set ys = {(k, v). map_of ys k = Some v}"
    1.49 +    by (rule set_map_of_compr)
    1.50 +  ultimately show ?rhs by simp
    1.51 +next
    1.52 +  assume ?rhs show ?lhs proof
    1.53 +    fix k
    1.54 +    show "map_of xs k = map_of ys k" proof (cases "map_of xs k")
    1.55 +      case None
    1.56 +      moreover with `?rhs` have "map_of ys k = None"
    1.57 +        by (simp add: map_of_eq_None_iff)
    1.58 +      ultimately show ?thesis by simp
    1.59 +    next
    1.60 +      case (Some v)
    1.61 +      moreover with distinct `?rhs` have "map_of ys k = Some v"
    1.62 +        by simp
    1.63 +      ultimately show ?thesis by simp
    1.64 +    qed
    1.65 +  qed
    1.66 +qed
    1.67 +
    1.68  end
    1.69