# HG changeset patch
# User haftmann
# Date 1445090910 -7200
# Node ID 7d1127ac2251c5082ac5ab2533a101181b2b41ed
# Parent  282f69026f91f96254224a861df9c3bf78c24305
code abbreviation for mapping over a fixed range

diff -r 282f69026f91 -r 7d1127ac2251 src/HOL/List.thy
--- 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>