# HG changeset patch
# User haftmann
# Date 1266396533 -3600
# Node ID df38e92af9268b20cf9c709d612595b729355555
# Parent  63d0ed5a027cb41bd1e6c58101105138875c56dd
added lemma map_of_map_restrict; generalized lemma dom_const

diff -r 63d0ed5a027c -r df38e92af926 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Feb 17 09:48:53 2010 +0100
+++ b/src/HOL/Map.thy	Wed Feb 17 09:48:53 2010 +0100
@@ -389,6 +389,10 @@
   "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
 by (simp add: restrict_map_def expand_fun_eq)
 
+lemma map_of_map_restrict:
+  "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
+  by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
+
 
 subsection {* @{term [source] map_upds} *}
 
@@ -534,7 +538,7 @@
 by (auto simp add: map_add_def split: option.split_asm)
 
 lemma dom_const [simp]:
-  "dom (\<lambda>x. Some y) = UNIV"
+  "dom (\<lambda>x. Some (f x)) = UNIV"
   by auto
 
 (* Due to John Matthews - could be rephrased with dom *)