# HG changeset patch
# User paulson
# Date 1089898352 -7200
# Node ID fa62de5862b9910ebf650fbb4a5fa2df82f84dee
# Parent  d6a4c3992e9dfd85123182bcdc57003ec9f7b155
redefining sumr to be a translation to setsum

diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/Auth/ZhouGollmann.thy
--- a/src/HOL/Auth/ZhouGollmann.thy	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Jul 15 15:32:32 2004 +0200
@@ -198,15 +198,17 @@
 
 text{*Holds also for @{term "A = Spy"}!*}
 theorem NRO_authenticity:
-     "[|Says A' B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
+     "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
         A \<notin> broken;  evs \<in> zg |]
      ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+apply (drule Gets_imp_Says, assumption) 
 apply clarify 
 apply (frule NRO_sender, auto)
-txt{*We are left with the case where @{term "A' = Spy"} and  @{term "A' \<noteq> A"},
-  i.e. @{term "A \<notin> bad"}, when we can apply @{text NRO_authenticity_good}.*}
- apply (blast dest: NRO_authenticity_good [OF refl])
+txt{*We are left with the case where the sender is @{term Spy} and not
+  equal to @{term A}, because @{term "A \<notin> bad"}. 
+  Thus theorem @{text NRO_authenticity_good} applies.*}
+apply (blast dest: NRO_authenticity_good [OF refl])
 done
 
 
@@ -276,15 +278,17 @@
 
 text{*Holds also for @{term "A = Spy"}!*}
 theorem sub_K_authenticity:
-     "[|Says A' TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
+     "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
         A \<notin> broken;  evs \<in> zg |]
      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+apply (drule Gets_imp_Says, assumption) 
 apply clarify 
 apply (frule sub_K_sender, auto)
-txt{*We are left with the case where @{term "A' = Spy"} and  @{term "A' \<noteq> A"},
-  i.e. @{term "A \<notin> bad"}, when we can apply @{text sub_K_authenticity_good}.*}
- apply (blast dest: sub_K_authenticity_good [OF refl])
+txt{*We are left with the case where the sender is @{term Spy} and not
+  equal to @{term A}, because @{term "A \<notin> bad"}. 
+  Thus theorem @{text sub_K_authenticity_good} applies.*}
+apply (blast dest: sub_K_authenticity_good [OF refl])
 done
 
 
@@ -326,7 +330,7 @@
 apply (erule zg.induct)
 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
 txt{*ZG4*}
-apply (clarify dest!: Gets_imp_Says) 
+apply clarify 
 apply (rule sub_K_authenticity, auto) 
 done
 
diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jul 15 15:32:32 2004 +0200
@@ -798,17 +798,14 @@
 end
 *}
 
-text{* As Jeremy Avigad notes: ultimately the analogous
-   thing should be done for setprod as well \dots *}
-
+text{* As Jeremy Avigad notes, setprod needs the same treatment \dots *}
 
 lemma setsum_empty [simp]: "setsum f {} = 0"
   by (simp add: setsum_def)
 
 lemma setsum_insert [simp]:
     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
-  by (simp add: setsum_def
-    LC.fold_insert [OF LC.intro] add_left_commute)
+  by (simp add: setsum_def LC.fold_insert [OF LC.intro] add_left_commute)
 
 lemma setsum_reindex [rule_format]:
      "finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
@@ -938,9 +935,10 @@
     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   by (induct set: Finites) auto
 
-lemma setsum_constant_nat [simp]:
+lemma setsum_constant_nat:
     "finite A ==> (\<Sum>x: A. y) = (card A) * y"
-  -- {* Later generalized to any @{text comm_semiring_1_cancel}. *}
+  -- {* Generalized to any @{text comm_semiring_1_cancel} in
+        @{text IntDef} as @{text setsum_constant}. *}
   by (erule finite_induct, auto)
 
 lemma setsum_Un: "finite A ==> finite B ==>
@@ -978,6 +976,41 @@
   apply (blast intro: add_mono)
   done
 
+lemma setsum_mult: 
+  fixes f :: "'a => ('b::semiring_0_cancel)"
+  assumes fin: "finite A" 
+  shows "r * setsum f A = setsum (%n. r * f n) A"
+using fin 
+proof (induct) 
+  case empty thus ?case by simp
+next
+  case (insert A x)
+  thus ?case by (simp add: right_distrib) 
+qed
+
+lemma setsum_abs: 
+  fixes f :: "'a => ('b::lordered_ab_group_abs)"
+  assumes fin: "finite A" 
+  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
+using fin 
+proof (induct) 
+  case empty thus ?case by simp
+next
+  case (insert A x)
+  thus ?case by (auto intro: abs_triangle_ineq order_trans)
+qed
+
+lemma setsum_abs_ge_zero: 
+  fixes f :: "'a => ('b::lordered_ab_group_abs)"
+  assumes fin: "finite A" 
+  shows "0 \<le> setsum (%i. abs(f i)) A"
+using fin 
+proof (induct) 
+  case empty thus ?case by simp
+next
+  case (insert A x) thus ?case by (auto intro: order_trans)
+qed
+
 subsubsection {* Cardinality of unions and Sigma sets *}
 
 lemma card_UN_disjoint:
@@ -986,12 +1019,10 @@
       card (UNION I A) = setsum (%i. card (A i)) I"
   apply (subst card_eq_setsum)
   apply (subst finite_UN, assumption+)
-  apply (subgoal_tac "setsum (%i. card (A i)) I =
-      setsum (%i. (setsum (%x. 1) (A i))) I")
-  apply (erule ssubst)
-  apply (erule setsum_UN_disjoint, assumption+)
-  apply (rule setsum_cong)
-  apply simp+
+  apply (subgoal_tac
+           "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
+  apply (simp add: setsum_UN_disjoint) 
+  apply (simp add: setsum_constant_nat cong: setsum_cong) 
   done
 
 lemma card_Union_disjoint:
@@ -1023,9 +1054,10 @@
   apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
   done
 
-lemma card_cartesian_product: "[| finite A; finite B |] ==>
-  card (A <*> B) = card(A) * card(B)"
-  by simp
+lemma card_cartesian_product:
+     "[| finite A; finite B |] ==> card (A <*> B) = card(A) * card(B)"
+  by (simp add: setsum_constant_nat)
+
 
 
 subsection {* Generalized product over a set *}
diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Thu Jul 15 15:32:32 2004 +0200
@@ -102,17 +102,11 @@
 apply (simp add: sumhr hypnat_of_nat_eq)
 done
 
-lemma sumhr_const: "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r"
-apply (cases n)
-apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat hypreal_mult)
-done
-
-lemma sumhr_add_mult_const: 
-     "sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) =  
-      sumhr(0,n,%i. f i + -r)"
+lemma sumhr_const:
+     "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
 apply (cases n)
 apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat 
-                 hypreal_mult hypreal_add hypreal_minus sumr_add [symmetric])
+                 hypreal_mult real_of_nat_def)
 done
 
 lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
@@ -139,11 +133,12 @@
  (such as @{term whn})*}
 lemma sumhr_hypreal_of_hypnat_omega: 
       "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
-by (simp add: hypnat_omega_def hypnat_zero_def sumhr hypreal_of_hypnat)
+by (simp add: hypnat_omega_def hypnat_zero_def sumhr hypreal_of_hypnat
+              real_of_nat_def)
 
 lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
 by (simp add: hypnat_omega_def hypnat_zero_def omega_def hypreal_one_def
-              sumhr hypreal_diff real_of_nat_Suc)
+              sumhr hypreal_diff real_of_nat_def)
 
 lemma sumhr_minus_one_realpow_zero [simp]: 
      "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
@@ -254,8 +249,6 @@
 val sumhr_split_diff = thm "sumhr_split_diff";
 val sumhr_hrabs = thm "sumhr_hrabs";
 val sumhr_fun_hypnat_eq = thm "sumhr_fun_hypnat_eq";
-val sumhr_const = thm "sumhr_const";
-val sumhr_add_mult_const = thm "sumhr_add_mult_const";
 val sumhr_less_bounds_zero = thm "sumhr_less_bounds_zero";
 val sumhr_minus = thm "sumhr_minus";
 val sumhr_shift_bounds = thm "sumhr_shift_bounds";
diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/Hyperreal/MacLaurin_lemmas.ML
--- a/src/HOL/Hyperreal/MacLaurin_lemmas.ML	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin_lemmas.ML	Thu Jul 15 15:32:32 2004 +0200
@@ -110,7 +110,7 @@
 by (asm_simp_tac (simpset() addsimps 
     [CLAIM "Suc m = ma + d + 1 ==> m - ma = d"]
     delsimps [sumr_Suc]) 2);
-by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc]) 
+by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc])
           (read_instantiate [("k","1")] sumr_offset4))] 
     delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);
 by (rtac lemma_DERIV_subst 2);
diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Thu Jul 15 15:32:32 2004 +0200
@@ -9,10 +9,9 @@
 
 theory Series = SEQ + Lim:
 
-consts sumr :: "[nat,nat,(nat=>real)] => real"
-primrec
-   sumr_0:   "sumr m 0 f = 0"
-   sumr_Suc: "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
+syntax sumr :: "[nat,nat,(nat=>real)] => real"
+translations
+  "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)"
 
 constdefs
    sums  :: "[nat=>real,real] => bool"     (infixr "sums" 80)
@@ -25,83 +24,52 @@
    "suminf f == (@s. f sums s)"
 
 
-lemma sumr_Suc_zero [simp]: "sumr (Suc n) n f = 0"
-by (induct_tac "n", auto)
-
-lemma sumr_eq_bounds [simp]: "sumr m m f = 0"
-by (induct_tac "m", auto)
+text{*This simprule replaces @{text "sumr 0 n"} by a term involving 
+  @{term lessThan}, making other simprules inapplicable.*}
+declare atLeast0LessThan [simp del]
 
-lemma sumr_Suc_eq [simp]: "sumr m (Suc m) f = f(m)"
-by auto
-
-lemma sumr_add_lbound_zero [simp]: "sumr (m+k) k f = 0"
-by (induct_tac "k", auto)
+lemma sumr_Suc [simp]:
+     "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
+by (simp add: atLeastLessThanSuc)
 
 lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"
-apply (induct_tac "n")
-apply (simp_all add: add_ac)
-done
+by (simp add: setsum_addf)
 
-lemma sumr_mult: "r * sumr m n f = sumr m n (%n. r * f n)"
-apply (induct_tac "n")
-apply (simp_all add: right_distrib)
-done
+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"
+     "n < p --> sumr 0 n f + sumr n p f = sumr 0 p (f::nat=>real)"
 apply (induct_tac "p", auto)
 apply (rename_tac k) 
 apply (subgoal_tac "n=k", auto) 
 done
 
-lemma sumr_split_add_minus: "n < p ==> sumr 0 p f + - sumr 0 n f = sumr n p f"
+lemma sumr_split_add_minus:
+     "n < p ==> sumr 0 p f + - sumr 0 n f = sumr n p (f::nat=>real)"
 apply (drule_tac f1 = f in sumr_split_add [symmetric])
 apply (simp add: add_ac)
 done
 
-lemma sumr_split_add2 [rule_format]:
-     "0 < n --> n < p --> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"
-apply (induct_tac "p", auto) 
-apply (rename_tac k) 
-apply (subgoal_tac "n=k", auto)
-done
-
-lemma sumr_split_add3:
-     "[| 0<n; n \<le> p |] ==> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"
-apply (drule le_imp_less_or_eq, auto)
-apply (blast intro: sumr_split_add2)
-done
+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: "abs(sumr m n f) \<le> sumr m n (%i. abs(f i))"
-apply (induct_tac "n")
-apply (auto intro: abs_triangle_ineq [THEN order_trans] add_right_mono)
-done
-
-lemma sumr_fun_eq [rule_format (no_asm)]:
-     "(\<forall>r. m \<le> r & r < n --> f r = g r) --> sumr m n f = sumr m n g"
-by (induct_tac "n", auto)
+lemma sumr_rabs_ge_zero [iff]: "0 \<le> sumr m n (%n. abs (f n))"
+by (simp add: setsum_abs_ge_zero)
 
-lemma sumr_const [simp]: "sumr 0 n (%i. r) = real n * r"
-apply (induct_tac "n")
-apply (simp_all add: left_distrib real_of_nat_zero real_of_nat_Suc)
-done
-
-lemma sumr_add_mult_const:
-     "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)"
-by (simp only: sumr_add [symmetric] minus_mult_right, simp)
+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_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
-by (simp add: real_diff_def sumr_add_mult_const)
+by (simp add: diff_minus setsum_addf real_of_nat_def)
 
-lemma sumr_less_bounds_zero [rule_format, simp]: "n < m --> sumr m n f = 0"
-apply (induct_tac "n")
-apply (auto dest: less_imp_le)
-done
+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"
-apply (induct_tac "n")
-apply (case_tac [2] "Suc n \<le> m", simp_all)
-done
+by (simp add: Finite_Set.setsum_negf)
 
 lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
 by (induct_tac "n", auto)
@@ -109,15 +77,12 @@
 lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0"
 by (induct_tac "n", auto)
 
-lemma Suc_diff_n: "m < Suc n ==> Suc n - m = Suc (n - m)"
-by (drule less_imp_Suc_add, auto)
-
 lemma sumr_interval_const [rule_format (no_asm)]:
      "(\<forall>n. m \<le> Suc n --> f n = r) --> m \<le> k --> sumr m k f = (real(k-m) * r)"
 apply (induct_tac "k", auto) 
 apply (drule_tac x = n in spec)
 apply (auto dest!: le_imp_less_or_eq)
-apply (simp (no_asm_simp) add: left_distrib Suc_diff_n real_of_nat_Suc)
+apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
 done
 
 lemma sumr_interval_const2 [rule_format (no_asm)]:
@@ -126,16 +91,17 @@
 apply (induct_tac "k", auto) 
 apply (drule_tac x = n in spec)
 apply (auto dest!: le_imp_less_or_eq)
-apply (simp (no_asm_simp) add: Suc_diff_n left_distrib real_of_nat_Suc)
+apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
 done
 
+
 lemma sumr_le [rule_format (no_asm)]:
      "(\<forall>n. m \<le> n --> 0 \<le> f n) --> m < k --> sumr 0 m f \<le> sumr 0 k f"
 apply (induct_tac "k")
 apply (auto simp add: less_Suc_eq_le)
 apply (drule_tac [!] x = n in spec, safe)
 apply (drule le_imp_less_or_eq, safe)
-apply (drule_tac [2] a = "sumr 0 m f" in add_mono)
+apply (arith) 
 apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
 done
 
@@ -156,9 +122,6 @@
 apply (drule_tac x = n in spec, arith)
 done
 
-lemma sumr_rabs_ge_zero [iff]: "0 \<le> sumr m n (%n. abs (f n))"
-by (induct_tac "n", auto, arith)
-
 lemma rabs_sumr_rabs_cancel [simp]:
      "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"
 apply (induct_tac "n")
@@ -198,7 +161,7 @@
      "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))  
       --> (sumr 0 n f \<le> (real n * K))"
 apply (induct_tac "n")
-apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc)
+apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute)
 done
 
 lemma sumr_group [simp]:
@@ -523,35 +486,18 @@
 
 ML
 {*
-val sumr_0 = thm"sumr_0";
 val sumr_Suc = thm"sumr_Suc";
 val sums_def = thm"sums_def";
 val summable_def = thm"summable_def";
 val suminf_def = thm"suminf_def";
 
-val sumr_Suc_zero = thm "sumr_Suc_zero";
-val sumr_eq_bounds = thm "sumr_eq_bounds";
-val sumr_Suc_eq = thm "sumr_Suc_eq";
-val sumr_add_lbound_zero = thm "sumr_add_lbound_zero";
 val sumr_add = thm "sumr_add";
 val sumr_mult = thm "sumr_mult";
 val sumr_split_add = thm "sumr_split_add";
-val sumr_split_add_minus = thm "sumr_split_add_minus";
-val sumr_split_add2 = thm "sumr_split_add2";
-val sumr_split_add3 = thm "sumr_split_add3";
 val sumr_rabs = thm "sumr_rabs";
 val sumr_fun_eq = thm "sumr_fun_eq";
-val sumr_const = thm "sumr_const";
-val sumr_add_mult_const = thm "sumr_add_mult_const";
 val sumr_diff_mult_const = thm "sumr_diff_mult_const";
-val sumr_less_bounds_zero = thm "sumr_less_bounds_zero";
-val sumr_minus = thm "sumr_minus";
-val sumr_shift_bounds = thm "sumr_shift_bounds";
 val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
-val Suc_diff_n = thm "Suc_diff_n";
-val sumr_interval_const = thm "sumr_interval_const";
-val sumr_interval_const2 = thm "sumr_interval_const2";
-val sumr_le = thm "sumr_le";
 val sumr_le2 = thm "sumr_le2";
 val sumr_ge_zero = thm "sumr_ge_zero";
 val sumr_ge_zero2 = thm "sumr_ge_zero2";
diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/Hyperreal/Transcendental.ML
--- a/src/HOL/Hyperreal/Transcendental.ML	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.ML	Thu Jul 15 15:32:32 2004 +0200
@@ -394,6 +394,8 @@
 (* Properties of power series                                               *)
 (*--------------------------------------------------------------------------*)
 
+Delsimps [thm"atLeast0LessThan"];
+
 Goal "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) = \
 \     y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))";
 by (auto_tac (claset(),simpset() addsimps [sumr_mult] delsimps [sumr_Suc]));
@@ -406,6 +408,7 @@
 Goal "x ^ (Suc n) - y ^ (Suc n) = \
 \     (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))";
 by (induct_tac "n" 1);
+by (Asm_full_simp_tac 1); 
 by (auto_tac (claset(),simpset() delsimps [sumr_Suc]));
 by (stac sumr_Suc 1);
 by (dtac sym 1);
diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu Jul 15 15:32:32 2004 +0200
@@ -869,7 +869,7 @@
 lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"
   by (subst int_eq_of_nat, rule setprod_of_nat)
 
-lemma setsum_constant: "finite A ==> (\<Sum>x \<in> A. y) = of_nat(card A) * y"
+lemma setsum_constant [simp]: "finite A ==> (\<Sum>x \<in> A. y) = of_nat(card A) * y"
   apply (erule finite_induct)
   apply (auto simp add: ring_distrib add_ac)
   done
diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/NumberTheory/Euler.thy
--- a/src/HOL/NumberTheory/Euler.thy	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/NumberTheory/Euler.thy	Thu Jul 15 15:32:32 2004 +0200
@@ -138,7 +138,7 @@
     also have "... = int(setsum (%x.2) (SetS a p))";
       apply (insert prems)
       apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
-        card_setsum_aux simp del: setsum_constant_nat)
+        card_setsum_aux simp del: setsum_constant)
     done
     also have "... = 2 * int(card( SetS a p))";
       by (auto simp add: prems SetS_finite setsum_const2)
diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/NumberTheory/Finite2.thy
--- a/src/HOL/NumberTheory/Finite2.thy	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/NumberTheory/Finite2.thy	Thu Jul 15 15:32:32 2004 +0200
@@ -76,7 +76,8 @@
 
 lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)";
   apply (induct set: Finites)
-by (auto simp add: zadd_zmult_distrib2)
+  apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
+  done
 
 lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = 
     int(c) * int(card X)";
diff -r d6a4c3992e9d -r fa62de5862b9 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/SetInterval.thy	Thu Jul 15 15:32:32 2004 +0200
@@ -192,6 +192,8 @@
 
 subsection {* Intervals of natural numbers *}
 
+subsubsection {* The Constant @{term lessThan} *}
+
 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
 by (simp add: lessThan_def)
 
@@ -204,6 +206,8 @@
 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
 by blast
 
+subsubsection {* The Constant @{term greaterThan} *}
+
 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
 apply (simp add: greaterThan_def)
 apply (blast dest: gr0_conv_Suc [THEN iffD1])
@@ -217,6 +221,8 @@
 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
 by blast
 
+subsubsection {* The Constant @{term atLeast} *}
+
 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
 by (unfold atLeast_def UNIV_def, simp)
 
@@ -232,6 +238,8 @@
 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
 by blast
 
+subsubsection {* The Constant @{term atMost} *}
+
 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
 by (simp add: atMost_def)
 
@@ -243,10 +251,37 @@
 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
 by blast
 
-lemma atLeast0LessThan [simp]: "{0::nat..<n} = {..<n}"
+subsubsection {* The Constant @{term atLeastLessThan} *}
+
+text{*But not a simprule because some concepts are better left in terms
+  of @{term atLeastLessThan}*}
+lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
 by(simp add:lessThan_def atLeastLessThan_def)
 
-text {* Intervals of nats with @{text Suc} *}
+lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
+by (simp add: atLeastLessThan_def)
+
+lemma atLeastLessThan_self [simp]: "{n::'a::order..<n} = {}"
+by (auto simp add: atLeastLessThan_def)
+
+lemma atLeastLessThan_empty: "n \<le> m ==> {m..<n::'a::order} = {}"
+by (auto simp add: atLeastLessThan_def)
+
+subsubsection {* Intervals of nats with @{term Suc} *}
+
+text{*Not a simprule because the RHS is too messy.*}
+lemma atLeastLessThanSuc:
+    "{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})"
+by (auto simp add: atLeastLessThan_def) 
+
+lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
+by (auto simp add: atLeastLessThan_def)
+
+lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
+by (induct k, simp_all add: atLeastLessThanSuc)
+
+lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}"
+by (auto simp add: atLeastLessThan_def)
 
 lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
   by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
@@ -312,7 +347,7 @@
   apply arith
   done
 
-lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
+lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"  
   by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
 
 lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"