# HG changeset patch
# User nipkow
# Date 1188308055 -7200
# Node ID 2f05cb7fed855942b66522b17336aa725b1f74d7
# Parent  46a32e2456172ba01466af3d0080cfdb315ac6a4
added (code) lemmas for setsum and foldl

diff -r 46a32e245617 -r 2f05cb7fed85 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 28 11:51:27 2007 +0200
+++ b/src/HOL/List.thy	Tue Aug 28 15:34:15 2007 +0200
@@ -451,6 +451,11 @@
 lemma append_Nil2 [simp]: "xs @ [] = xs"
 by (induct xs) auto
 
+interpretation semigroup_append: semigroup_add ["op @"]
+by unfold_locales simp
+interpretation monoid_append: monoid_add ["[]" "op @"]
+by unfold_locales (simp+)
+
 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
 by (induct xs) auto
 
@@ -1738,7 +1743,9 @@
 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
 by(induct xs) simp_all
 
-lemma foldl_map: "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
+text{* For efficient code generation: avoid intermediate list. *}
+lemma foldl_map[code unfold]:
+  "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
 by(induct xs arbitrary:a) simp_all
 
 lemma foldl_cong [fundef_cong, recdef_cong]:
@@ -1751,6 +1758,15 @@
   ==> foldr f l a = foldr g k b"
 by (induct k arbitrary: a b l) simp_all
 
+lemma (in semigroup_add) foldl_assoc:
+shows "foldl op\<^loc>+ (x\<^loc>+y) zs = x \<^loc>+ (foldl op\<^loc>+ y zs)"
+by (induct zs arbitrary: y) (simp_all add:add_assoc)
+
+lemma (in monoid_add) foldl_absorb0:
+shows "x \<^loc>+ (foldl op\<^loc>+ \<^loc>0 zs) = foldl op\<^loc>+ x zs"
+by (induct zs) (simp_all add:foldl_assoc)
+
+
 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
 
 lemma foldl_foldr1_lemma:
@@ -1785,16 +1801,35 @@
 "!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
 by (induct ns) auto
 
+text{* @{const foldl} and @{text concat} *}
+
+lemma concat_conv_foldl: "concat xss = foldl op@ [] xss"
+by (induct xss) (simp_all add:monoid_append.foldl_absorb0)
+
+lemma foldl_conv_concat:
+  "foldl (op @) xs xxs = xs @ (concat xxs)"
+by(simp add:concat_conv_foldl monoid_append.foldl_absorb0)
+
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
 
+lemma listsum_append[simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
+by (induct xs) (simp_all add:add_assoc)
+
+lemma listsum_rev[simp]:
+fixes xs :: "'a::comm_monoid_add list"
+shows "listsum (rev xs) = listsum xs"
+by (induct xs) (simp_all add:add_ac)
+
 lemma listsum_foldr:
  "listsum xs = foldr (op +) xs 0"
 by(induct xs) auto
 
-(* for efficient code generation *)
-lemma listsum[code]: "listsum xs = foldl (op +) 0 xs"
+text{* For efficient code generation ---
+       @{const listsum} is not tail recursive but @{const foldl} is. *}
+lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
 by(simp add:listsum_foldr foldl_foldr1)
 
+
 text{* Some syntactic sugar for summing a function over a list: *}
 
 syntax
@@ -2990,11 +3025,8 @@
   "map_filter f P xs = map f (filter P xs)"
 by (induct xs) auto
 
-lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs"
-by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
-
-
-text {* Code for bounded quantification over nats. *}
+
+text {* Code for bounded quantification and summation over nats. *}
 
 lemma atMost_upto [code unfold]:
   "{..n} = set [0..n]"
@@ -3004,11 +3036,11 @@
   "{..<n} = set [0..<n]"
 by auto
 
-lemma greaterThanLessThan_upd [code unfold]:
+lemma greaterThanLessThan_upt [code unfold]:
   "{n<..<m} = set [Suc n..<m]"
 by auto
 
-lemma atLeastLessThan_upd [code unfold]:
+lemma atLeastLessThan_upt [code unfold]:
   "{n..<m} = set [n..<m]"
 by auto
 
@@ -3036,9 +3068,23 @@
   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
 by auto
 
-lemma foldl_append_append: "\<And> ss ss'. foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)"
-by (induct xs, simp_all)
-
+lemma setsum_set_upt_conv_listsum[code unfold]:
+  "setsum f (set[k..<n]) = listsum (map f [k..<n])"
+apply(subst atLeastLessThan_upt[symmetric])
+by (induct n) simp_all
+
+
+(* FIXME Amine *)
+
+(* is now available as thm semigroup_append.foldl_assoc *)
+lemma foldl_append_append: "foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)"
+by (induct xs arbitrary: ss ss', simp_all)
+
+(* now superfluous *)
+lemma foldl_append_map_set:
+ "set (foldl (op @) ss (map f xs)) = set ss \<union> UNION (set xs) (\<lambda>x. set (f x))"
+by(simp add:foldl_conv_concat)
+(*
 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))"
 proof(induct xs)
   case Nil thus ?case by simp
@@ -3052,11 +3098,15 @@
     by (simp add: Un_assoc)
   finally show ?case by simp
 qed
-
+*)
+
+(* also superfluous *)
 lemma foldl_append_map_Nil_set: 
   "set (foldl (op @) [] (map f xs)) = UNION (set xs) (\<lambda>x. set (f x))"
+by(simp add:foldl_conv_concat)
+(*
 using foldl_append_map_set[where ss="[]" and xs="xs" and f="f"] by simp
-
+*)
 
 subsubsection {* List partitioning *}
 
diff -r 46a32e245617 -r 2f05cb7fed85 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Tue Aug 28 11:51:27 2007 +0200
+++ b/src/HOL/SetInterval.thy	Tue Aug 28 15:34:15 2007 +0200
@@ -253,14 +253,20 @@
 
 subsubsection {* The Constant @{term atLeastLessThan} *}
 
-text{*But not a simprule because some concepts are better left in terms
-  of @{term atLeastLessThan}*}
+text{*The orientation of the following rule is tricky. The lhs is
+defined in terms of the rhs.  Hence the chosen orientation makes sense
+in this theory --- the reverse orientation complicates proofs (eg
+nontermination). But outside, when the definition of the lhs is rarely
+used, the opposite orientation seems preferable because it reduces a
+specific concept to a more general one. *}
 lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
 by(simp add:lessThan_def atLeastLessThan_def)
-(*
-lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
+
+declare atLeast0LessThan[symmetric, code unfold]
+
+lemma atLeastLessThan0: "{m..<0::nat} = {}"
 by (simp add: atLeastLessThan_def)
-*)
+
 subsubsection {* Intervals of nats with @{term Suc} *}
 
 text{*Not a simprule because the RHS is too messy.*}