# HG changeset patch
# User nipkow
# Date 1180040153 -7200
# Node ID 423ad2fe9f7662ea2272339b6a2443c07a0c032f
# Parent  45f10b70e8919dbc7795eab485558f28eea64c7c
*** empty log message ***

diff -r 45f10b70e891 -r 423ad2fe9f76 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Thu May 24 16:52:54 2007 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu May 24 22:55:53 2007 +0200
@@ -87,14 +87,14 @@
      "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
 apply (rule hypreal_sqrt_approx_zero2)
 apply (rule add_nonneg_nonneg)+
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma hypreal_sqrt_sum_squares2 [simp]:
      "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
 apply (rule hypreal_sqrt_approx_zero2)
 apply (rule add_nonneg_nonneg)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)"
@@ -157,7 +157,7 @@
      "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
 apply (rule HFinite_hypreal_sqrt_iff)
 apply (rule add_nonneg_nonneg)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma Infinitesimal_hypreal_sqrt:
@@ -184,7 +184,7 @@
      "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
 apply (rule Infinitesimal_hypreal_sqrt_iff)
 apply (rule add_nonneg_nonneg)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma HInfinite_hypreal_sqrt:
@@ -211,7 +211,7 @@
      "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
 apply (rule HInfinite_hypreal_sqrt_iff)
 apply (rule add_nonneg_nonneg)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma HFinite_exp [simp]:
diff -r 45f10b70e891 -r 423ad2fe9f76 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Thu May 24 16:52:54 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Thu May 24 22:55:53 2007 +0200
@@ -1723,13 +1723,13 @@
      "(x::hypreal)*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
 apply (rule Infinitesimal_interval2)
 apply (rule_tac [3] zero_le_square, assumption)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma HFinite_square_cancel [simp]:
   "(x::hypreal)*x + y*y \<in> HFinite ==> x*x \<in> HFinite"
 apply (rule HFinite_bounded, assumption)
-apply (auto simp add: zero_le_square)
+apply (auto)
 done
 
 lemma Infinitesimal_square_cancel2 [simp]:
@@ -1751,7 +1751,7 @@
 apply (rule Infinitesimal_interval2, assumption)
 apply (rule_tac [2] zero_le_square, simp)
 apply (insert zero_le_square [of y]) 
-apply (insert zero_le_square [of z], simp)
+apply (insert zero_le_square [of z], simp del:zero_le_square)
 done
 
 lemma HFinite_sum_square_cancel [simp]:
@@ -1759,7 +1759,7 @@
 apply (rule HFinite_bounded, assumption)
 apply (rule_tac [2] zero_le_square)
 apply (insert zero_le_square [of y]) 
-apply (insert zero_le_square [of z], simp)
+apply (insert zero_le_square [of z], simp del:zero_le_square)
 done
 
 lemma Infinitesimal_sum_square_cancel2 [simp]:
diff -r 45f10b70e891 -r 423ad2fe9f76 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Thu May 24 16:52:54 2007 +0200
+++ b/src/HOL/Integ/NatBin.thy	Thu May 24 22:55:53 2007 +0200
@@ -343,7 +343,7 @@
 
 lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
 apply (induct "n")
-apply (auto simp add: power_Suc power_add power2_minus)
+apply (auto simp add: power_Suc power_add)
 done
 
 lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
@@ -366,7 +366,7 @@
     have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
       by (simp add: mult_ac power_add power2_eq_square)
     thus ?case
-      by (simp add: prems zero_le_square zero_le_mult_iff)
+      by (simp add: prems zero_le_mult_iff)
 qed
 
 lemma odd_power_less_zero:
diff -r 45f10b70e891 -r 423ad2fe9f76 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 24 16:52:54 2007 +0200
+++ b/src/HOL/List.thy	Thu May 24 22:55:53 2007 +0200
@@ -28,6 +28,7 @@
   butlast :: "'a list => 'a list"
   set :: "'a list => 'a set"
   map :: "('a=>'b) => ('a list => 'b list)"
+  listsum ::  "'a list => 'a::monoid_add"
   nth :: "'a list => nat => 'a"    (infixl "!" 100)
   list_update :: "'a list => nat => 'a => 'a list"
   take:: "nat => 'a list => 'a list"
@@ -134,6 +135,10 @@
   "concat(x#xs) = x @ concat(xs)"
 
 primrec
+"listsum [] = 0"
+"listsum (x # xs) = x + listsum xs"
+
+primrec
   drop_Nil:"drop n [] = []"
   drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
   -- {*Warning: simpset does not contain this definition, but separate
@@ -1417,6 +1422,20 @@
 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
 by (induct rule:list_induct2, simp_all)
 
+lemma map_zip_map:
+ "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
+apply(induct xs arbitrary:ys) apply simp
+apply(case_tac ys)
+apply simp_all
+done
+
+lemma map_zip_map2:
+ "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
+apply(induct xs arbitrary:ys) apply simp
+apply(case_tac ys)
+apply simp_all
+done
+
 lemma nth_zip [simp]:
 "!!i xs. [| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
 apply (induct ys, simp)
@@ -1618,6 +1637,12 @@
 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
 by (induct xs) auto
 
+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"
+by(induct xs arbitrary:a) simp_all
+
 lemma foldl_cong [fundef_cong, recdef_cong]:
   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   ==> foldl f a l = foldl g b k"
@@ -1628,6 +1653,19 @@
   ==> foldr f l a = foldr g k b"
   by (induct k arbitrary: a b l) simp_all
 
+text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
+
+lemma foldl_foldr1_lemma:
+ "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
+by (induct xs arbitrary: a) (auto simp:add_assoc)
+
+corollary foldl_foldr1:
+ "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
+by (simp add:foldl_foldr1_lemma)
+
+
+text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
+
 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
 by (induct xs) auto
 
@@ -1649,6 +1687,37 @@
 "!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
 by (induct ns) auto
 
+subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
+
+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"
+by(simp add:listsum_foldr foldl_foldr1)
+
+text{* Some syntactic sugar for summing a function over a list: *}
+
+syntax
+  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
+syntax (xsymbols)
+  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+syntax (HTML output)
+  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+
+translations -- {* Beware of argument permutation! *}
+  "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
+  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
+
+lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
+by (induct xs) simp_all
+
+text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
+lemma uminus_listsum_map:
+ "- listsum (map f xs) = (listsum (map (uminus o f) xs) :: 'a::ab_group_add)"
+by(induct xs) simp_all
+
 
 subsubsection {* @{text upto} *}
 
@@ -2763,6 +2832,7 @@
   "map_filter f P (x#xs) =
      (if P x then f x # map_filter f P xs else map_filter f P xs)"
 
+
 text {*
   Only use @{text mem} for generating executable code.  Otherwise use
   @{prop "x : set xs"} instead --- it is much easier to reason about.
@@ -2850,8 +2920,11 @@
   "map_filter f P xs = map f (filter P xs)"
   by (induct xs) auto
 
-
-text {* code for bounded quantification over nats *}
+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. *}
 
 lemma atMost_upto [code unfold]:
   "{..n} = set [0..n]"
diff -r 45f10b70e891 -r 423ad2fe9f76 src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Thu May 24 16:52:54 2007 +0200
+++ b/src/HOL/Real/RealPow.thy	Thu May 24 22:55:53 2007 +0200
@@ -149,7 +149,7 @@
 lemma sum_squares_eq_zero_iff:
   fixes x y :: "'a::ordered_ring_strict"
   shows "(x * x + y * y = 0) = (x = 0 \<and> y = 0)"
-by (simp add: sum_nonneg_eq_zero_iff zero_le_square)
+by (simp add: sum_nonneg_eq_zero_iff)
 
 lemma sum_squares_le_zero_iff:
   fixes x y :: "'a::ordered_ring_strict"