1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 06 10:19:48 2012 +0100
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 06 10:19:48 2012 +0100
     1.3 @@ -1279,64 +1279,21 @@
     1.4  subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary
     1.5    finite product of FPS, also the relvant instance of powers of a FPS*}
     1.6  
     1.7 -definition "natpermute n k = {l:: nat list. length l = k \<and> foldl op + 0 l = n}"
     1.8 +definition "natpermute n k = {l :: nat list. length l = k \<and> listsum l = n}"
     1.9  
    1.10  lemma natlist_trivial_1: "natpermute n 1 = {[n]}"
    1.11    apply (auto simp add: natpermute_def)
    1.12    apply (case_tac x, auto)
    1.13    done
    1.14  
    1.15 -lemma foldl_add_start0:
    1.16 -  "foldl op + x xs = x + foldl op + (0::nat) xs"
    1.17 -  apply (induct xs arbitrary: x)
    1.18 -  apply simp
    1.19 -  unfolding foldl.simps
    1.20 -  apply atomize
    1.21 -  apply (subgoal_tac "\<forall>x\<Colon>nat. foldl op + x xs = x + foldl op + (0\<Colon>nat) xs")
    1.22 -  apply (erule_tac x="x + a" in allE)
    1.23 -  apply (erule_tac x="a" in allE)
    1.24 -  apply simp
    1.25 -  apply assumption
    1.26 -  done
    1.27 -
    1.28 -lemma foldl_add_append: "foldl op + (x::nat) (xs@ys) = foldl op + x xs + foldl op + 0 ys"
    1.29 -  apply (induct ys arbitrary: x xs)
    1.30 -  apply auto
    1.31 -  apply (subst (2) foldl_add_start0)
    1.32 -  apply simp
    1.33 -  apply (subst (2) foldl_add_start0)
    1.34 -  by simp
    1.35 -
    1.36 -lemma foldl_add_setsum: "foldl op + (x::nat) xs = x + setsum (nth xs) {0..<length xs}"
    1.37 -proof(induct xs arbitrary: x)
    1.38 -  case Nil thus ?case by simp
    1.39 -next
    1.40 -  case (Cons a as x)
    1.41 -  have eq: "setsum (op ! (a#as)) {1..<length (a#as)} = setsum (op ! as) {0..<length as}"
    1.42 -    apply (rule setsum_reindex_cong [where f=Suc])
    1.43 -    by (simp_all add: inj_on_def)
    1.44 -  have f: "finite {0}" "finite {1 ..< length (a#as)}" by simp_all
    1.45 -  have d: "{0} \<inter> {1..<length (a#as)} = {}" by simp
    1.46 -  have seq: "{0} \<union> {1..<length(a#as)} = {0 ..<length (a#as)}" by auto
    1.47 -  have "foldl op + x (a#as) = x + foldl op + a as "
    1.48 -    apply (subst foldl_add_start0)    by simp
    1.49 -  also have "\<dots> = x + a + setsum (op ! as) {0..<length as}" unfolding Cons.hyps by simp
    1.50 -  also have "\<dots> = x + setsum (op ! (a#as)) {0..<length (a#as)}"
    1.51 -    unfolding eq[symmetric]
    1.52 -    unfolding setsum_Un_disjoint[OF f d, unfolded seq]
    1.53 -    by simp
    1.54 -  finally show ?case  .
    1.55 -qed
    1.56 -
    1.57 -
    1.58  lemma append_natpermute_less_eq:
    1.59 -  assumes h: "xs@ys \<in> natpermute n k" shows "foldl op + 0 xs \<le> n" and "foldl op + 0 ys \<le> n"
    1.60 +  assumes h: "xs@ys \<in> natpermute n k" shows "listsum xs \<le> n" and "listsum ys \<le> n"
    1.61  proof-
    1.62 -  {from h have "foldl op + 0 (xs@ ys) = n" by (simp add: natpermute_def)
    1.63 -    hence "foldl op + 0 xs + foldl op + 0 ys = n" unfolding foldl_add_append .}
    1.64 +  {from h have "listsum (xs @ ys) = n" by (simp add: natpermute_def)
    1.65 +    hence "listsum xs + listsum ys = n" by simp}
    1.66    note th = this
    1.67 -  {from th show "foldl op + 0 xs \<le> n" by simp}
    1.68 -  {from th show "foldl op + 0 ys \<le> n" by simp}
    1.69 +  {from th show "listsum xs \<le> n" by simp}
    1.70 +  {from th show "listsum ys \<le> n" by simp}
    1.71  qed
    1.72  
    1.73  lemma natpermute_split:
    1.74 @@ -1345,12 +1302,10 @@
    1.75  proof-
    1.76    {fix l assume l: "l \<in> ?R"
    1.77      from l obtain m xs ys where h: "m \<in> {0..n}" and xs: "xs \<in> natpermute m h" and ys: "ys \<in> natpermute (n - m) (k - h)"  and leq: "l = xs@ys" by blast
    1.78 -    from xs have xs': "foldl op + 0 xs = m" by (simp add: natpermute_def)
    1.79 -    from ys have ys': "foldl op + 0 ys = n - m" by (simp add: natpermute_def)
    1.80 +    from xs have xs': "listsum xs = m" by (simp add: natpermute_def)
    1.81 +    from ys have ys': "listsum ys = n - m" by (simp add: natpermute_def)
    1.82      have "l \<in> ?L" using leq xs ys h
    1.83 -      apply simp
    1.84 -      apply (clarsimp simp add: natpermute_def simp del: foldl_append)
    1.85 -      apply (simp add: foldl_add_append[unfolded foldl_append])
    1.86 +      apply (clarsimp simp add: natpermute_def)
    1.87        unfolding xs' ys'
    1.88        using mn xs ys
    1.89        unfolding natpermute_def by simp}
    1.90 @@ -1358,19 +1313,21 @@
    1.91    {fix l assume l: "l \<in> natpermute n k"
    1.92      let ?xs = "take h l"
    1.93      let ?ys = "drop h l"
    1.94 -    let ?m = "foldl op + 0 ?xs"
    1.95 -    from l have ls: "foldl op + 0 (?xs @ ?ys) = n" by (simp add: natpermute_def)
    1.96 +    let ?m = "listsum ?xs"
    1.97 +    from l have ls: "listsum (?xs @ ?ys) = n" by (simp add: natpermute_def)
    1.98      have xs: "?xs \<in> natpermute ?m h" using l mn by (simp add: natpermute_def)
    1.99 -    have ys: "?ys \<in> natpermute (n - ?m) (k - h)" using l mn ls[unfolded foldl_add_append]
   1.100 -      by (simp add: natpermute_def)
   1.101 -    from ls have m: "?m \<in> {0..n}"  unfolding foldl_add_append by simp
   1.102 +    have l_take_drop: "listsum l = listsum (take h l @ drop h l)" by simp
   1.103 +    then have ys: "?ys \<in> natpermute (n - ?m) (k - h)" using l mn ls
   1.104 +      by (auto simp add: natpermute_def simp del: append_take_drop_id)
   1.105 +    from ls have m: "?m \<in> {0..n}" by (simp add: l_take_drop del: append_take_drop_id)
   1.106      from xs ys ls have "l \<in> ?R"
   1.107        apply auto
   1.108        apply (rule bexI[where x = "?m"])
   1.109        apply (rule exI[where x = "?xs"])
   1.110        apply (rule exI[where x = "?ys"])
   1.111 -      using ls l unfolding foldl_add_append
   1.112 -      by (auto simp add: natpermute_def)}
   1.113 +      using ls l 
   1.114 +      apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id)
   1.115 +      by simp}
   1.116    ultimately show ?thesis by blast
   1.117  qed
   1.118  
   1.119 @@ -1408,7 +1365,7 @@
   1.120      have f: "finite({0..k} - {i})" "finite {i}" by auto
   1.121      have d: "({0..k} - {i}) \<inter> {i} = {}" using i by auto
   1.122      from H have "n = setsum (nth xs) {0..k}" apply (simp add: natpermute_def)
   1.123 -      unfolding foldl_add_setsum by (auto simp add: atLeastLessThanSuc_atLeastAtMost)
   1.124 +      by (auto simp add: atLeastLessThanSuc_atLeastAtMost listsum_setsum_nth)
   1.125      also have "\<dots> = n + setsum (nth xs) ({0..k} - {i})"
   1.126        unfolding setsum_Un_disjoint[OF f d, unfolded eqs] using i by simp
   1.127      finally have zxs: "\<forall> j\<in> {0..k} - {i}. xs!j = 0" by auto
   1.128 @@ -1430,8 +1387,8 @@
   1.129      have nxs: "n \<in> set ?xs"
   1.130        apply (rule set_update_memI) using i by simp
   1.131      have xsl: "length ?xs = k+1" by (simp only: length_replicate length_list_update)
   1.132 -    have "foldl op + 0 ?xs = setsum (nth ?xs) {0..<k+1}"
   1.133 -      unfolding foldl_add_setsum add_0 length_replicate length_list_update ..
   1.134 +    have "listsum ?xs = setsum (nth ?xs) {0..<k+1}"
   1.135 +      unfolding listsum_setsum_nth xsl ..
   1.136      also have "\<dots> = setsum (\<lambda>j. if j = i then n else 0) {0..< k+1}"
   1.137        apply (rule setsum_cong2) by (simp del: replicate.simps)
   1.138      also have "\<dots> = n" using i by (simp add: setsum_delta)
   1.139 @@ -1579,9 +1536,9 @@
   1.140        have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}" by simp_all
   1.141        have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}" by auto
   1.142        have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})" using i by auto
   1.143 -      from xs have "Suc n = foldl op + 0 xs" by (simp add: natpermute_def)
   1.144 -      also have "\<dots> = setsum (nth xs) {0..<Suc k}" unfolding foldl_add_setsum using xs
   1.145 -        by (simp add: natpermute_def)
   1.146 +      from xs have "Suc n = listsum xs" by (simp add: natpermute_def)
   1.147 +      also have "\<dots> = setsum (nth xs) {0..<Suc k}" using xs
   1.148 +        by (simp add: natpermute_def listsum_setsum_nth)
   1.149        also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
   1.150          unfolding eqs  setsum_Un_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
   1.151          unfolding setsum_Un_disjoint[OF fths(2) fths(3) d(2)]
   1.152 @@ -1824,9 +1781,9 @@
   1.153              have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}" by simp_all
   1.154              have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}" by auto
   1.155              have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})" using i by auto
   1.156 -            from xs have "n = foldl op + 0 xs" by (simp add: natpermute_def)
   1.157 -            also have "\<dots> = setsum (nth xs) {0..<Suc k}" unfolding foldl_add_setsum using xs
   1.158 -              by (simp add: natpermute_def)
   1.159 +            from xs have "n = listsum xs" by (simp add: natpermute_def)
   1.160 +            also have "\<dots> = setsum (nth xs) {0..<Suc k}" using xs
   1.161 +              by (simp add: natpermute_def listsum_setsum_nth)
   1.162              also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
   1.163                unfolding eqs  setsum_Un_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
   1.164                unfolding setsum_Un_disjoint[OF fths(2) fths(3) d(2)]