# HG changeset patch
# User haftmann
# Date 1345118852 -7200
# Node ID 441a4eed7823f8d1a94a6260a053e2b6ae441db6
# Parent  45d0e40b07affc3996f2cc6c240a7a8933e7b9e7
prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala

diff -r 45d0e40b07af -r 441a4eed7823 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 15 23:06:17 2012 +0200
+++ b/src/HOL/List.thy	Thu Aug 16 14:07:32 2012 +0200
@@ -2392,6 +2392,11 @@
 
 subsubsection {* @{const fold} with natural argument order *}
 
+lemma fold_simps [code]: -- {* eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala *}
+  "fold f [] s = s"
+  "fold f (x # xs) s = fold f xs (f x s)" 
+  by simp_all
+
 lemma fold_remove1_split:
   assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     and x: "x \<in> set xs"