--- 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]:
--- 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]:
--- 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:
--- 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]"
--- 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"