# HG changeset patch
# User nipkow
# Date 1109010226 -3600
# Node ID ee6cd48cf840736e27a50b9b8308afdcd171ce70
# Parent  206d779ba96df19675014462be2f8283743038dc
more fine tuniung

diff -r 206d779ba96d -r ee6cd48cf840 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Feb 21 18:04:28 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Feb 21 19:23:46 2005 +0100
@@ -900,7 +900,7 @@
       ==> setsum h B = setsum g A"
   by (simp add: setsum_reindex cong: setsum_cong)
 
-lemma setsum_0: "setsum (%i. 0) A = 0"
+lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
 apply (clarsimp simp: setsum_def)
 apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
 done
@@ -1119,18 +1119,7 @@
   also have "A \<union> (B-A) = B" using sub by blast
   finally show ?thesis .
 qed
-(*
-lemma setsum_mono2_nat:
-  assumes fin: "finite B" and sub: "A \<subseteq> B"
-shows "setsum f A \<le> (setsum f B :: nat)"
-proof -
-  have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
-  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
-    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
-  also have "A \<union> (B-A) = B" using sub by blast
-  finally show ?thesis .
-qed
-*)
+
 lemma setsum_mult: 
   fixes f :: "'a => ('b::semiring_0_cancel)"
   shows "r * setsum f A = setsum (%n. r * f n) A"
@@ -1542,6 +1531,16 @@
   apply (auto simp add: power_Suc)
   done
 
+lemma setsum_bounded:
+  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
+  shows "setsum f A \<le> of_nat(card A) * K"
+proof (cases "finite A")
+  case True
+  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
+next
+  case False thus ?thesis by (simp add: setsum_def)
+qed
+
 
 subsubsection {* Cardinality of unions *}
 
diff -r 206d779ba96d -r ee6cd48cf840 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Mon Feb 21 18:04:28 2005 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy	Mon Feb 21 19:23:46 2005 +0100
@@ -147,12 +147,6 @@
          add: sumhr hypnat_add nat_mult_2 [symmetric] hypreal_zero_def 
               hypnat_zero_def hypnat_omega_def)
 
-(* FIXME move *)
-lemma setsum_ivl_cong:
- "i = m \<Longrightarrow> j = n \<Longrightarrow> (!!x. m <= x \<Longrightarrow> x < n \<Longrightarrow> f x = g x) \<Longrightarrow>
- setsum f {i..<j} = setsum g {m..<n}"
-by(rule setsum_cong, simp_all)
-
 lemma sumhr_interval_const:
      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
       ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =  
diff -r 206d779ba96d -r ee6cd48cf840 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Mon Feb 21 18:04:28 2005 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Mon Feb 21 19:23:46 2005 +0100
@@ -30,136 +30,22 @@
   "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
 by (simp add: atLeastLessThanSuc add_commute)
 
-(*
-lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"
-by (simp add: setsum_addf)
-
-lemma sumr_mult: "r * sumr m n (f::nat=>real) = sumr m n (%n. r * f n)"
-by (simp add: setsum_mult)
-
-lemma sumr_split_add [rule_format]:
-     "n < p --> sumr 0 n f + sumr n p f = sumr 0 p (f::nat=>real)"
-apply (induct "p", auto)
-apply (rename_tac k) 
-apply (subgoal_tac "n=k", auto) 
-done
-
-lemma sumr_split_add: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
-  setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
-by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
-
-lemma sumr_split_add_minus:
-fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
-shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
-  setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
-using sumr_split_add [of m n p f,symmetric]
-apply (simp add: add_ac)
-done
-*)
-
 lemma sumr_diff_mult_const:
  "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
 by (simp add: diff_minus setsum_addf real_of_nat_def)
 
-(*
-lemma sumr_rabs: "abs(sumr m n  (f::nat=>real)) \<le> sumr m n (%i. abs(f i))"
-by (simp add: setsum_abs)
-
-lemma sumr_rabs_ge_zero [iff]: "0 \<le> sumr m n (%n. abs (f n))"
-by (simp add: setsum_abs_ge_zero)
-
-text{*Just a congruence rule*}
-lemma sumr_fun_eq:
-     "(\<forall>r. m \<le> r & r < n --> f r = g r) ==> sumr m n f = sumr m n g"
-by (auto intro: setsum_cong) 
-
-lemma sumr_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0"
-by (simp add: atLeastLessThan_empty)
-
-lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
-by (simp add: Finite_Set.setsum_negf)
-
-lemma sumr_shift_bounds:
-  "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
-by (induct "n", auto)
-*)
+lemma real_setsum_nat_ivl_bounded:
+     "(!!p. p < n \<Longrightarrow> f(p) \<le> K)
+      \<Longrightarrow> setsum f {0..<n::nat} \<le> real n * K"
+using setsum_bounded[where A = "{0..<n}"]
+by (auto simp:real_of_nat_def)
 
 (* Generalize from real to some algebraic structure? *)
 lemma sumr_minus_one_realpow_zero [simp]:
   "setsum (%i. (-1) ^ Suc i) {0..<2*n} = (0::real)"
 by (induct "n", auto)
 
-(*
-lemma sumr_interval_const2:
-     "[|\<forall>n\<ge>m. f n = r; m \<le> k|]
-      ==> sumr m k f = (real (k - m) * r)"
-apply (induct "k", auto)
-apply (drule_tac x = k in spec)
-apply (auto dest!: le_imp_less_or_eq)
-apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
-done
-*)
-(* FIXME split in tow steps
-lemma setsum_nat_set_real_const:
-  "(\<And>n. n\<in>A \<Longrightarrow> f n = r) \<Longrightarrow> setsum f A = real(card A) * r" (is "PROP ?P")
-proof (cases "finite A")
-  case True
-  thus "PROP ?P"
-  proof induct
-    case empty thus ?case by simp
-  next
-    case insert thus ?case by(simp add: left_distrib real_of_nat_Suc)
-  qed
-next
-  case False thus "PROP ?P" by (simp add: setsum_def)
-qed
- *)
-
-(*
-lemma sumr_le:
-     "[|\<forall>n\<ge>m. 0 \<le> (f n::real); m < k|] ==> setsum f {0..<m} \<le> setsum f {0..<k::nat}"
-apply (induct "k")
-apply (auto simp add: less_Suc_eq_le)
-apply (drule_tac x = k in spec, safe)
-apply (drule le_imp_less_or_eq, safe)
-apply (arith)
-apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
-done
-
-lemma sumr_le:
-     "[|\<forall>n\<ge>m. 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
-apply (induct "k")
-apply (auto simp add: less_Suc_eq_le)
-apply (drule_tac x = k in spec, safe)
-apply (drule le_imp_less_or_eq, safe)
-apply (arith) 
-apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
-done
-
-lemma sumr_le2 [rule_format (no_asm)]:
-     "(\<forall>r. m \<le> r & r < n --> f r \<le> g r) --> sumr m n f \<le> sumr m n g"
-apply (induct "n")
-apply (auto intro: add_mono simp add: le_def)
-done
-*)
-
-(*
-lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) --> 0 \<le> sumr m n f"
-apply (induct "n", auto)
-apply (drule_tac x = n in spec, arith)
-done
-*)
-
-(*
-lemma rabs_sumr_rabs_cancel [simp]:
-     "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
-by (induct "n", simp_all add: add_increasing)
-
-lemma sumr_zero [rule_format]:
-     "\<forall>n \<ge> N. f n = 0 ==> N \<le> m --> sumr m n f = 0"
-by (induct "n", auto)
-*)
-
+(* FIXME get rid of this one! *)
 lemma Suc_le_imp_diff_ge2:
      "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> setsum f {m..<n} = 0"
 apply (rule setsum_0')
@@ -174,41 +60,7 @@
 apply (induct "n")
 apply (case_tac [2] "n", auto)
 done
-(*
-lemma sumr_diff: "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"
-by (simp add: diff_minus setsum_addf setsum_negf)
-*)
-(*
-lemma sumr_subst [rule_format (no_asm)]:
-     "(\<forall>p. m \<le> p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g"
-by (induct "n", auto)
-*)
 
-lemma setsum_bounded:
-  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
-  shows "setsum f A \<le> of_nat(card A) * K"
-proof (cases "finite A")
-  case True
-  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
-next
-  case False thus ?thesis by (simp add: setsum_def)
-qed
-(*
-lemma sumr_bound [rule_format (no_asm)]:
-     "(\<forall>p. m \<le> p & p < m + n --> (f(p) \<le> K))  
-      --> setsum f {m..<m+n::nat} \<le> (real n * K)"
-apply (induct "n")
-apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc)
-done
-*)
-(* FIXME should be generalized
-lemma sumr_bound2 [rule_format (no_asm)]:
-     "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))  
-      --> setsum f {0..<n::nat} \<le> (real n * K)"
-apply (induct "n")
-apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute)
-done
- *)
 (* FIXME a bit specialized for [simp]! *)
 lemma sumr_group [simp]:
      "(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}"
@@ -216,7 +68,6 @@
 apply (induct "n")
 apply (simp_all add: setsum_add_nat_ivl add_commute)
 done
-(* FIXME setsum_0[simp] *)
 
 
 subsection{* Infinite Sums, by the Properties of Limits*}
@@ -246,43 +97,11 @@
 apply (auto intro!: LIMSEQ_unique simp add: sums_def)
 done
 
-(*
-Goalw [sums_def,LIMSEQ_def] 
-     "(\<forall>m. n \<le> Suc m --> f(m) = 0) ==> f sums (sumr 0 n f)"
-by safe
-by (res_inst_tac [("x","n")] exI 1);
-by (safe THEN ftac le_imp_less_or_eq 1)
-by safe
-by (dres_inst_tac [("f","f")] sumr_split_add_minus 1);
-by (ALLGOALS (Asm_simp_tac));
-by (dtac (conjI RS sumr_interval_const) 1);
-by Auto_tac
-qed "series_zero";
-next one was called series_zero2
-**********************)
-
-lemma ivl_subset[simp]:
- "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
-apply(auto simp:linorder_not_le)
-apply(rule ccontr)
-apply(frule subsetCE[where c = n])
-apply(auto simp:linorder_not_le)
-done
-
-lemma ivl_diff[simp]:
- "i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
-by(auto)
-
-
-(* FIXME the last step should work w/o Ball_def, ideally just with
-   setsum_0 and setsum_cong. Currently the simplifier does not simplify
-   the premise x:{i..<j} that ball_cong (or a modified version of setsum_0')
-   generates. FIX simplifier??? *)
 lemma series_zero: 
      "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
 apply (rule_tac x = n in exI)
-apply (clarsimp simp add:setsum_diff[symmetric] setsum_0' Ball_def)
+apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
 done
 
 
@@ -423,7 +242,6 @@
 apply(simp add: setsum_diff[symmetric])
 apply(simp add: setsum_diff[symmetric])
 done
-(* FIXME move ivl_ lemmas out of this theory *)
 
 text{*Comparison test*}
 
diff -r 206d779ba96d -r ee6cd48cf840 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Mon Feb 21 18:04:28 2005 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy	Mon Feb 21 19:23:46 2005 +0100
@@ -503,13 +503,6 @@
                  del: setsum_Suc realpow_Suc)
 done
 
-(* FIXME move *)
-lemma sumr_bound2 [rule_format (no_asm)]:
-     "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))  
-      --> setsum f {0..<n::nat} \<le> (real n * K)"
-using setsum_bounded[where A = "{0..<n}"]
-by (auto simp:real_of_nat_def)
-
 lemma lemma_termdiff3:
      "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]  
       ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0))  
@@ -520,7 +513,7 @@
 apply (rule setsum_abs [THEN real_le_trans])
 apply (simp add: mult_assoc [symmetric])
 apply (simp add: mult_commute [of _ "real (n - Suc 0)"])
-apply (auto intro!: sumr_bound2)
+apply (auto intro!: real_setsum_nat_ivl_bounded)
 apply (case_tac "n", auto)
 apply (drule less_add_one)
 (*CLAIM_SIMP " (a * b * c = a * (c * (b::real))" mult_ac]*)
@@ -535,7 +528,7 @@
 apply (drule_tac [2] n = d in zero_le_power)
 apply (auto simp del: setsum_Suc)
 apply (rule setsum_abs [THEN real_le_trans])
-apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: power_add)
+apply (rule real_setsum_nat_ivl_bounded, auto dest!: less_add_one intro!: mult_mono simp add: power_add)
 apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
 done
 
diff -r 206d779ba96d -r ee6cd48cf840 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Mon Feb 21 18:04:28 2005 +0100
+++ b/src/HOL/Real/RealDef.thy	Mon Feb 21 19:23:46 2005 +0100
@@ -353,7 +353,7 @@
 done
 
 lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
-by (cases z, cases w, simp add: real_le order_antisym)
+by (cases z, cases w, simp add: real_le)
 
 lemma real_trans_lemma:
   assumes "x + v \<le> u + y"
@@ -368,7 +368,7 @@
     by (simp add: preal_add_le_cancel_left prems) 
   also have "... = (u'+y) + (u+v)"  by (simp add: preal_add_ac)
   finally show ?thesis by (simp add: preal_add_le_cancel_right)
-qed						 
+qed
 
 lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
 apply (cases i, cases j, cases k)
@@ -401,7 +401,7 @@
 apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
                       preal_add_ac)
 apply (simp_all add: preal_add_assoc [symmetric] preal_cancels)
-done 
+done
 
 lemma real_add_left_mono: 
   assumes le: "x \<le> y" shows "z + x \<le> z + (y::real)"
diff -r 206d779ba96d -r ee6cd48cf840 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Feb 21 18:04:28 2005 +0100
+++ b/src/HOL/SetInterval.thy	Mon Feb 21 19:23:46 2005 +0100
@@ -534,6 +534,24 @@
 
 lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
 
+subsubsection {* Some Differences *}
+
+lemma ivl_diff[simp]:
+ "i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
+by(auto)
+
+
+subsubsection {* Some Subset Conditions *}
+
+lemma ivl_subset[simp]:
+ "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
+apply(auto simp:linorder_not_le)
+apply(rule ccontr)
+apply(insert linorder_le_less_linear[of i n])
+apply(clarsimp simp:linorder_not_le)
+apply(fastsimp)
+done
+
 
 subsection {* Summation indexed over intervals *}
 
@@ -585,6 +603,17 @@
 not provide all lemmas available for @{term"{m..<n}"} also in the
 special form for @{term"{..<n}"}. *}
 
+(* FIXME change the simplifier's treatment of congruence rules?? *)
+
+text{* This congruence rule should be used for sums over intervals as
+the standard theorem @{text[source]setsum_cong} does not work well
+with the simplifier who adds the unsimplified premise @{term"x:B"} to
+the context. *}
+
+lemma setsum_ivl_cong:
+ "\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow>
+ setsum f {a..<b} = setsum g {c..<d}"
+by(rule setsum_cong, simp_all)
 
 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
 by (simp add:lessThan_Suc)