src/HOL/List.thy
changeset 51875 dafd097dd1f4
parent 51738 9e4220605179
child 52122 510709f8881d
     1.1 --- a/src/HOL/List.thy	Mon May 06 00:25:04 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Mon May 06 02:48:18 2013 +0200
     1.3 @@ -5604,6 +5604,26 @@
     1.4  
     1.5  subsection {* Code generation *}
     1.6  
     1.7 +
     1.8 +text{* Optional tail recursive version of @{const map}. Can avoid
     1.9 +stack overflow in some target languages. *}
    1.10 +
    1.11 +fun map_tailrec_rev ::  "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    1.12 +"map_tailrec_rev f [] bs = bs" |
    1.13 +"map_tailrec_rev f (a#as) bs = map_tailrec_rev f as (f a # bs)"
    1.14 +
    1.15 +lemma map_tailrec_rev:
    1.16 +  "map_tailrec_rev f as bs = rev(map f as) @ bs"
    1.17 +by(induction as arbitrary: bs) simp_all
    1.18 +
    1.19 +definition map_tailrec :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    1.20 +"map_tailrec f as = rev (map_tailrec_rev f as [])"
    1.21 +
    1.22 +text{* Code equation: *}
    1.23 +lemma map_eq_map_tailrec: "map = map_tailrec"
    1.24 +by(simp add: fun_eq_iff map_tailrec_def map_tailrec_rev)
    1.25 +
    1.26 +
    1.27  subsubsection {* Counterparts for set-related operations *}
    1.28  
    1.29  definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where