author | haftmann |

Thu Mar 04 11:22:06 2010 +0100 (2010-03-04) | |

changeset 35565 | 56b070cd7ab3 |

parent 35564 | 20995afa8fa1 |

child 35566 | 3c01f5ad1d34 |

child 35576 | 5f6bd3ac99f9 |

child 35602 | e814157560e8 |

lemmas set_map_of_compr, map_of_inject_set

src/HOL/Map.thy | file | annotate | diff | revisions |

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