src/HOL/Map.thy
changeset 35159 df38e92af926
parent 35115 446c5063e4fd
child 35427 ad039d29e01c
child 35552 364cb98a3e4e
     1.1 --- a/src/HOL/Map.thy	Wed Feb 17 09:48:53 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Wed Feb 17 09:48:53 2010 +0100
     1.3 @@ -389,6 +389,10 @@
     1.4    "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
     1.5  by (simp add: restrict_map_def expand_fun_eq)
     1.6  
     1.7 +lemma map_of_map_restrict:
     1.8 +  "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
     1.9 +  by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
    1.10 +
    1.11  
    1.12  subsection {* @{term [source] map_upds} *}
    1.13  
    1.14 @@ -534,7 +538,7 @@
    1.15  by (auto simp add: map_add_def split: option.split_asm)
    1.16  
    1.17  lemma dom_const [simp]:
    1.18 -  "dom (\<lambda>x. Some y) = UNIV"
    1.19 +  "dom (\<lambda>x. Some (f x)) = UNIV"
    1.20    by auto
    1.21  
    1.22  (* Due to John Matthews - could be rephrased with dom *)