1.1 --- a/src/HOL/List.thy	Tue Aug 28 11:51:27 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Aug 28 15:34:15 2007 +0200
     1.3 @@ -451,6 +451,11 @@
     1.4  lemma append_Nil2 [simp]: "xs @ [] = xs"
     1.5  by (induct xs) auto
     1.6  
     1.7 +interpretation semigroup_append: semigroup_add ["op @"]
     1.8 +by unfold_locales simp
     1.9 +interpretation monoid_append: monoid_add ["[]" "op @"]
    1.10 +by unfold_locales (simp+)
    1.11 +
    1.12  lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
    1.13  by (induct xs) auto
    1.14  
    1.15 @@ -1738,7 +1743,9 @@
    1.16  lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
    1.17  by(induct xs) simp_all
    1.18  
    1.19 -lemma foldl_map: "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
    1.20 +text{* For efficient code generation: avoid intermediate list. *}
    1.21 +lemma foldl_map[code unfold]:
    1.22 +  "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
    1.23  by(induct xs arbitrary:a) simp_all
    1.24  
    1.25  lemma foldl_cong [fundef_cong, recdef_cong]:
    1.26 @@ -1751,6 +1758,15 @@
    1.27    ==> foldr f l a = foldr g k b"
    1.28  by (induct k arbitrary: a b l) simp_all
    1.29  
    1.30 +lemma (in semigroup_add) foldl_assoc:
    1.31 +shows "foldl op\<^loc>+ (x\<^loc>+y) zs = x \<^loc>+ (foldl op\<^loc>+ y zs)"
    1.32 +by (induct zs arbitrary: y) (simp_all add:add_assoc)
    1.33 +
    1.34 +lemma (in monoid_add) foldl_absorb0:
    1.35 +shows "x \<^loc>+ (foldl op\<^loc>+ \<^loc>0 zs) = foldl op\<^loc>+ x zs"
    1.36 +by (induct zs) (simp_all add:foldl_assoc)
    1.37 +
    1.38 +
    1.39  text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
    1.40  
    1.41  lemma foldl_foldr1_lemma:
    1.42 @@ -1785,16 +1801,35 @@
    1.43  "!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
    1.44  by (induct ns) auto
    1.45  
    1.46 +text{* @{const foldl} and @{text concat} *}
    1.47 +
    1.48 +lemma concat_conv_foldl: "concat xss = foldl op@ [] xss"
    1.49 +by (induct xss) (simp_all add:monoid_append.foldl_absorb0)
    1.50 +
    1.51 +lemma foldl_conv_concat:
    1.52 +  "foldl (op @) xs xxs = xs @ (concat xxs)"
    1.53 +by(simp add:concat_conv_foldl monoid_append.foldl_absorb0)
    1.54 +
    1.55  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
    1.56  
    1.57 +lemma listsum_append[simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
    1.58 +by (induct xs) (simp_all add:add_assoc)
    1.59 +
    1.60 +lemma listsum_rev[simp]:
    1.61 +fixes xs :: "'a::comm_monoid_add list"
    1.62 +shows "listsum (rev xs) = listsum xs"
    1.63 +by (induct xs) (simp_all add:add_ac)
    1.64 +
    1.65  lemma listsum_foldr:
    1.66   "listsum xs = foldr (op +) xs 0"
    1.67  by(induct xs) auto
    1.68  
    1.69 -(* for efficient code generation *)
    1.70 -lemma listsum[code]: "listsum xs = foldl (op +) 0 xs"
    1.71 +text{* For efficient code generation ---
    1.72 +       @{const listsum} is not tail recursive but @{const foldl} is. *}
    1.73 +lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
    1.74  by(simp add:listsum_foldr foldl_foldr1)
    1.75  
    1.76 +
    1.77  text{* Some syntactic sugar for summing a function over a list: *}
    1.78  
    1.79  syntax
    1.80 @@ -2990,11 +3025,8 @@
    1.81    "map_filter f P xs = map f (filter P xs)"
    1.82  by (induct xs) auto
    1.83  
    1.84 -lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs"
    1.85 -by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
    1.86 -
    1.87 -
    1.88 -text {* Code for bounded quantification over nats. *}
    1.89 +
    1.90 +text {* Code for bounded quantification and summation over nats. *}
    1.91  
    1.92  lemma atMost_upto [code unfold]:
    1.93    "{..n} = set [0..n]"
    1.94 @@ -3004,11 +3036,11 @@
    1.95    "{..<n} = set [0..<n]"
    1.96  by auto
    1.97  
    1.98 -lemma greaterThanLessThan_upd [code unfold]:
    1.99 +lemma greaterThanLessThan_upt [code unfold]:
   1.100    "{n<..<m} = set [Suc n..<m]"
   1.101  by auto
   1.102  
   1.103 -lemma atLeastLessThan_upd [code unfold]:
   1.104 +lemma atLeastLessThan_upt [code unfold]:
   1.105    "{n..<m} = set [n..<m]"
   1.106  by auto
   1.107  
   1.108 @@ -3036,9 +3068,23 @@
   1.109    "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
   1.110  by auto
   1.111  
   1.112 -lemma foldl_append_append: "\<And> ss ss'. foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)"
   1.113 -by (induct xs, simp_all)
   1.114 -
   1.115 +lemma setsum_set_upt_conv_listsum[code unfold]:
   1.116 +  "setsum f (set[k..<n]) = listsum (map f [k..<n])"
   1.117 +apply(subst atLeastLessThan_upt[symmetric])
   1.118 +by (induct n) simp_all
   1.119 +
   1.120 +
   1.121 +(* FIXME Amine *)
   1.122 +
   1.123 +(* is now available as thm semigroup_append.foldl_assoc *)
   1.124 +lemma foldl_append_append: "foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)"
   1.125 +by (induct xs arbitrary: ss ss', simp_all)
   1.126 +
   1.127 +(* now superfluous *)
   1.128 +lemma foldl_append_map_set:
   1.129 + "set (foldl (op @) ss (map f xs)) = set ss \<union> UNION (set xs) (\<lambda>x. set (f x))"
   1.130 +by(simp add:foldl_conv_concat)
   1.131 +(*
   1.132  lemma foldl_append_map_set: "\<And> ss. set (foldl (op @) ss (map f xs)) = set ss \<union> UNION (set xs) (\<lambda>x. set (f x))"
   1.133  proof(induct xs)
   1.134    case Nil thus ?case by simp
   1.135 @@ -3052,11 +3098,15 @@
   1.136      by (simp add: Un_assoc)
   1.137    finally show ?case by simp
   1.138  qed
   1.139 -
   1.140 +*)
   1.141 +
   1.142 +(* also superfluous *)
   1.143  lemma foldl_append_map_Nil_set: 
   1.144    "set (foldl (op @) [] (map f xs)) = UNION (set xs) (\<lambda>x. set (f x))"
   1.145 +by(simp add:foldl_conv_concat)
   1.146 +(*
   1.147  using foldl_append_map_set[where ss="[]" and xs="xs" and f="f"] by simp
   1.148 -
   1.149 +*)
   1.150  
   1.151  subsubsection {* List partitioning *}
   1.152  

     2.1 --- a/src/HOL/SetInterval.thy	Tue Aug 28 11:51:27 2007 +0200
     2.2 +++ b/src/HOL/SetInterval.thy	Tue Aug 28 15:34:15 2007 +0200
     2.3 @@ -253,14 +253,20 @@
     2.4  
     2.5  subsubsection {* The Constant @{term atLeastLessThan} *}
     2.6  
     2.7 -text{*But not a simprule because some concepts are better left in terms
     2.8 -  of @{term atLeastLessThan}*}
     2.9 +text{*The orientation of the following rule is tricky. The lhs is
    2.10 +defined in terms of the rhs.  Hence the chosen orientation makes sense
    2.11 +in this theory --- the reverse orientation complicates proofs (eg
    2.12 +nontermination). But outside, when the definition of the lhs is rarely
    2.13 +used, the opposite orientation seems preferable because it reduces a
    2.14 +specific concept to a more general one. *}
    2.15  lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
    2.16  by(simp add:lessThan_def atLeastLessThan_def)
    2.17 -(*
    2.18 -lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
    2.19 +
    2.20 +declare atLeast0LessThan[symmetric, code unfold]
    2.21 +
    2.22 +lemma atLeastLessThan0: "{m..<0::nat} = {}"
    2.23  by (simp add: atLeastLessThan_def)
    2.24 -*)
    2.25 +
    2.26  subsubsection {* Intervals of nats with @{term Suc} *}
    2.27  
    2.28  text{*Not a simprule because the RHS is too messy.*}