--- a/src/HOL/List.thy Sat Oct 17 23:07:28 2015 +0200
+++ b/src/HOL/List.thy Sat Oct 17 16:08:30 2015 +0200
@@ -6389,6 +6389,15 @@
"map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"
by (simp add: map_filter_def)
+definition map_range :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list"
+where
+ [code_abbrev]: "map_range f n = map f [0..<n]"
+
+lemma map_range_simps [simp, code]:
+ "map_range f 0 = []"
+ "map_range f (Suc n) = map_range f n @ [f n]"
+ by (simp_all add: map_range_def)
+
text \<open>Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
and similiarly for @{text"\<exists>"}.\<close>