# HG changeset patch
# User nipkow
# Date 1367801298 -7200
# Node ID dafd097dd1f4496f100cee6a2ca64d5720342031
# Parent  730b9802d6fe4b31989cb9fade2537f492388baf
tail recursive version of map, for code generation, optionally

diff -r 730b9802d6fe -r dafd097dd1f4 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon May 06 00:25:04 2013 +0200
+++ b/src/HOL/List.thy	Mon May 06 02:48:18 2013 +0200
@@ -5604,6 +5604,26 @@
 
 subsection {* Code generation *}
 
+
+text{* Optional tail recursive version of @{const map}. Can avoid
+stack overflow in some target languages. *}
+
+fun map_tailrec_rev ::  "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'b list" where
+"map_tailrec_rev f [] bs = bs" |
+"map_tailrec_rev f (a#as) bs = map_tailrec_rev f as (f a # bs)"
+
+lemma map_tailrec_rev:
+  "map_tailrec_rev f as bs = rev(map f as) @ bs"
+by(induction as arbitrary: bs) simp_all
+
+definition map_tailrec :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
+"map_tailrec f as = rev (map_tailrec_rev f as [])"
+
+text{* Code equation: *}
+lemma map_eq_map_tailrec: "map = map_tailrec"
+by(simp add: fun_eq_iff map_tailrec_def map_tailrec_rev)
+
+
 subsubsection {* Counterparts for set-related operations *}
 
 definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where