--- a/src/HOL/List.thy Tue Aug 30 20:10:47 2011 +0200
+++ b/src/HOL/List.thy Tue Aug 30 20:10:48 2011 +0200
@@ -4906,6 +4906,9 @@
lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
by (induct xs) auto
+lemma list_size_append[simp]: "list_size f (xs @ ys) = list_size f xs + list_size f ys"
+by (induct xs, auto)
+
lemma list_size_pointwise[termination_simp]:
"(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
by (induct xs) force+