# HG changeset patch
# User bulwahn
# Date 1314727848 -7200
# Node ID fd520fa2fb09f36d7e99d0d920e2c2c6222f1c7a
# Parent  f3635643a376b7b3038fecce0de5eaa2934ac617
adding list_size_append (thanks to Rene Thiemann)

diff -r f3635643a376 -r fd520fa2fb09 src/HOL/List.thy
--- 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+