[isabelle] No tail-recursive code equation for List.map


when I export list-based code to Scala and run it on huge inputs, it
always gives me a StackOverflowException. Looking at the stack trace
and providing the following tail-recursive version of map, everything
works fine.

  fun map_tailrec ::  "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list ⇒ 'b list" where
  "map_tailrec f [] accs = accs" |
  "map_tailrec f (a#as) accs = (map_tailrec f as ((f a)#accs))"

  lemma map_tailrec_is_listmap:
  "rev (map_tailrec f l accs) = (rev accs)@(List.map f l)"
    apply(induction l accs rule: map_tailrec.induct)

  definition efficient_map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "efficient_map f l ≡ rev (map_tailrec f l [])"

  lemma[code]: "List.map f l = efficient_map f l"
   by(simp add: efficient_map_def map_tailrec_is_listmap)

Why is there no tail-recursive code equation of List.map in the default library?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.