adding list_size_append (thanks to Rene Thiemann)
authorbulwahn
Tue Aug 30 20:10:48 2011 +0200 (2011-08-30)
changeset 44619fd520fa2fb09
parent 44618 f3635643a376
child 44620 49e7dbaf19aa
adding list_size_append (thanks to Rene Thiemann)
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Tue Aug 30 20:10:47 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Aug 30 20:10:48 2011 +0200
     1.3 @@ -4906,6 +4906,9 @@
     1.4  lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
     1.5  by (induct xs) auto
     1.6  
     1.7 +lemma list_size_append[simp]: "list_size f (xs @ ys) = list_size f xs + list_size f ys"
     1.8 +by (induct xs, auto)
     1.9 +
    1.10  lemma list_size_pointwise[termination_simp]: 
    1.11    "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
    1.12  by (induct xs) force+