setsum syntax;
authorwenzelm
Mon Oct 15 20:42:06 2001 +0200 (2001-10-15)
changeset 1178651ce34ef5113
parent 11785 3087d6f19adc
child 11787 85b3735a51e1
setsum syntax;
src/HOL/Finite.ML
src/HOL/Finite.thy
src/HOL/NumberTheory/Fib.thy
src/HOL/UNITY/Comp/Alloc.ML
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Comp/AllocBase.ML
src/HOL/UNITY/Comp/AllocImpl.ML
src/HOL/UNITY/Follows.ML
src/HOL/ex/NatSum.thy
     1.1 --- a/src/HOL/Finite.ML	Mon Oct 15 20:41:14 2001 +0200
     1.2 +++ b/src/HOL/Finite.ML	Mon Oct 15 20:42:06 2001 +0200
     1.3 @@ -716,14 +716,14 @@
     1.4  Addsimps [setsum_empty];
     1.5  
     1.6  Goalw [setsum_def]
     1.7 - "!!f::'a=>'b::plus_ac0. [| finite F; a ~: F |] ==> \
     1.8 -\      setsum f (insert a F) = f(a) + setsum f F";
     1.9 + "!!f. [| finite F; a ~: F |] ==> \
    1.10 +\      setsum f (insert a F) = f a + setsum f F";
    1.11  by (asm_simp_tac (simpset() addsimps [export fold_insert,
    1.12  				      thm "plus_ac0_left_commute"]) 1);
    1.13  qed "setsum_insert";
    1.14  Addsimps [setsum_insert];
    1.15  
    1.16 -Goal "setsum (%i. 0) A = (0::'a::plus_ac0)";
    1.17 +Goal "setsum (%i. 0) A = 0";
    1.18  by (case_tac "finite A" 1);
    1.19   by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); 
    1.20  by (etac finite_induct 1);
    1.21 @@ -751,7 +751,7 @@
    1.22  qed "card_eq_setsum";
    1.23  
    1.24  (*The reversed orientation looks more natural, but LOOPS as a simprule!*)
    1.25 -Goal "!!g::'a=>'b::plus_ac0. [| finite A; finite B |] \
    1.26 +Goal "!!g. [| finite A; finite B |] \
    1.27  \     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B";
    1.28  by (etac finite_induct 1);
    1.29  by (Simp_tac 1);
    1.30 @@ -760,7 +760,7 @@
    1.31  qed "setsum_Un_Int";
    1.32  
    1.33  Goal "[| finite A; finite B; A Int B = {} |] \
    1.34 -\     ==> setsum g (A Un B) = (setsum g A + setsum g B::'a::plus_ac0)";  
    1.35 +\     ==> setsum g (A Un B) = setsum g A + setsum g B";
    1.36  by (stac (setsum_Un_Int RS sym) 1);
    1.37  by Auto_tac;
    1.38  qed "setsum_Un_disjoint";
    1.39 @@ -779,7 +779,7 @@
    1.40  by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
    1.41  qed_spec_mp "setsum_UN_disjoint";
    1.42  
    1.43 -Goal "setsum (%x. f x + g x) A = (setsum f A + setsum g A::'a::plus_ac0)";
    1.44 +Goal "setsum (%x. f x + g x) A = (setsum f A + setsum g A)";
    1.45  by (case_tac "finite A" 1);
    1.46   by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
    1.47  by (etac finite_induct 1);
    1.48 @@ -808,7 +808,7 @@
    1.49  
    1.50  val prems = Goal
    1.51      "[| A = B; !!x. x:B ==> f x = g x|] \
    1.52 -\    ==> setsum f A = (setsum g B::'a::plus_ac0)";
    1.53 +\    ==> setsum f A = setsum g B";
    1.54  by (case_tac "finite B" 1);
    1.55   by (asm_simp_tac (simpset() addsimps [setsum_def]@prems) 2); 
    1.56  by (simp_tac (simpset() addsimps prems) 1);
     2.1 --- a/src/HOL/Finite.thy	Mon Oct 15 20:41:14 2001 +0200
     2.2 +++ b/src/HOL/Finite.thy	Mon Oct 15 20:42:06 2001 +0200
     2.3 @@ -36,7 +36,7 @@
     2.4    InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"
     2.5  
     2.6  constdefs
     2.7 -  card :: 'a set => nat
     2.8 + card :: 'a set => nat
     2.9   "card A == THE n. (A,n) : cardR"
    2.10  
    2.11  (*
    2.12 @@ -55,12 +55,20 @@
    2.13  	      ==> (insert x A, f x y) : foldSet f e"
    2.14  
    2.15  constdefs
    2.16 -   fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
    2.17 +  fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
    2.18    "fold f e A == THE x. (A,x) : foldSet f e"
    2.19  
    2.20 -   setsum :: "('a => 'b) => 'a set => ('b::{plus, zero})"
    2.21 +  setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
    2.22    "setsum f A == if finite A then fold (op+ o f) 0 A else 0"
    2.23  
    2.24 +syntax
    2.25 +  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\\<Sum>_:_. _" [0, 51, 10] 10)
    2.26 +syntax (symbols)
    2.27 +  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10)
    2.28 +translations
    2.29 +  "\\<Sum>i:A. b" == "setsum (%i. b) A"  (* Beware of argument permutation! *)
    2.30 +
    2.31 +
    2.32  locale LC =
    2.33    fixes
    2.34      f    :: ['b,'a] => 'a
     3.1 --- a/src/HOL/NumberTheory/Fib.thy	Mon Oct 15 20:41:14 2001 +0200
     3.2 +++ b/src/HOL/NumberTheory/Fib.thy	Mon Oct 15 20:42:06 2001 +0200
     3.3 @@ -118,7 +118,7 @@
     3.4    done
     3.5  
     3.6  lemma fib_mult_eq_setsum:
     3.7 -    "fib (Suc n) * fib n = setsum (\<lambda>k. fib k * fib k) (atMost n)"
     3.8 +    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
     3.9    apply (induct n rule: fib.induct)
    3.10      apply (auto simp add: atMost_Suc fib.Suc_Suc)
    3.11    apply (simp add: add_mult_distrib add_mult_distrib2)
     4.1 --- a/src/HOL/UNITY/Comp/Alloc.ML	Mon Oct 15 20:41:14 2001 +0200
     4.2 +++ b/src/HOL/UNITY/Comp/Alloc.ML	Mon Oct 15 20:42:06 2001 +0200
     4.3 @@ -524,10 +524,8 @@
     4.4  
     4.5  (*safety (1), step 3*)
     4.6  Goal
     4.7 -  "System : Always {s. setsum (%i. (tokens o sub i o allocGiv) s) \
     4.8 -\                             (lessThan Nclients)                 \
     4.9 -\           <= NbT + setsum (%i. (tokens o sub i o allocRel) s)   \
    4.10 -\                           (lessThan Nclients)}";
    4.11 +  "System : Always {s. (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv) s) \
    4.12 +\           <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel) s)}";
    4.13  by (simp_tac (simpset() addsimps [o_apply]) 1);
    4.14  by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
    4.15  by (auto_tac (claset(), 
     5.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Mon Oct 15 20:41:14 2001 +0200
     5.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Oct 15 20:42:06 2001 +0200
     5.3 @@ -52,8 +52,8 @@
     5.4    (*spec (1)*)
     5.5    system_safety :: 'a systemState program set
     5.6      "system_safety ==
     5.7 -     Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients)
     5.8 -     <= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}"
     5.9 +     Always {s. (\\<Sum>i: lessThan Nclients. (tokens o giv o sub i o client)s)
    5.10 +     <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
    5.11  
    5.12    (*spec (2)*)
    5.13    system_progress :: 'a systemState program set
    5.14 @@ -111,8 +111,8 @@
    5.15      "alloc_safety ==
    5.16  	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
    5.17           guarantees
    5.18 -	 Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
    5.19 -         <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
    5.20 +	 Always {s. (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv)s)
    5.21 +         <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
    5.22  
    5.23    (*spec (8)*)
    5.24    alloc_progress :: 'a allocState_d program set
     6.1 --- a/src/HOL/UNITY/Comp/AllocBase.ML	Mon Oct 15 20:41:14 2001 +0200
     6.2 +++ b/src/HOL/UNITY/Comp/AllocBase.ML	Mon Oct 15 20:42:06 2001 +0200
     6.3 @@ -48,14 +48,14 @@
     6.4  
     6.5  Addcongs [setsum_cong];
     6.6  
     6.7 -Goal "setsum (%i. {#if i<k then f i else g i#}) (A Int lessThan k) = \
     6.8 -\     setsum (%i. {#f i#}) (A Int lessThan k)";
     6.9 +Goal "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) = \
    6.10 +\     (\\<Sum>i: A Int lessThan k. {#f i#})";
    6.11  by (rtac setsum_cong 1);
    6.12  by Auto_tac;  
    6.13  qed "bag_of_sublist_lemma";
    6.14  
    6.15  Goal "bag_of (sublist l A) = \
    6.16 -\     setsum (%i. {# l!i #}) (A Int lessThan (length l))";
    6.17 +\     (\\<Sum>i: A Int lessThan (length l). {# l!i #})";
    6.18  by (rev_induct_tac "l" 1);
    6.19  by (Simp_tac 1);
    6.20  by (asm_simp_tac
    6.21 @@ -81,7 +81,7 @@
    6.22  
    6.23  Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
    6.24  \     ==> bag_of (sublist l (UNION I A)) =  \
    6.25 -\         setsum (%i. bag_of (sublist l (A i))) I";  
    6.26 +\         (\\<Sum>i:I. bag_of (sublist l (A i)))";  
    6.27  by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
    6.28  			    addsimps [bag_of_sublist]) 1);
    6.29  by (stac setsum_UN_disjoint 1);
     7.1 --- a/src/HOL/UNITY/Comp/AllocImpl.ML	Mon Oct 15 20:41:14 2001 +0200
     7.2 +++ b/src/HOL/UNITY/Comp/AllocImpl.ML	Mon Oct 15 20:42:06 2001 +0200
     7.3 @@ -44,9 +44,8 @@
     7.4  
     7.5  Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
     7.6  \ ==> M Join G : Always \
     7.7 -\         {s. setsum (%i. bag_of (sublist (merge.Out s) \
     7.8 -\                                 {k. k < length (iOut s) & iOut s ! k = i})) \
     7.9 -\                    (lessThan Nclients)   =  \
    7.10 +\         {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (merge.Out s) \
    7.11 +\                                 {k. k < length (iOut s) & iOut s ! k = i})) = \
    7.12  \             (bag_of o merge.Out) s}";
    7.13  by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I,
    7.14  	   UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
    7.15 @@ -65,8 +64,7 @@
    7.16  Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
    7.17  \         guarantees  \
    7.18  \            (bag_of o merge.Out) Fols \
    7.19 -\            (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
    7.20 -\                        (lessThan Nclients))";
    7.21 +\            (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o merge.In) s)";
    7.22  by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
    7.23  by Auto_tac;  
    7.24  by (rtac Follows_setsum 1);
    7.25 @@ -103,9 +101,8 @@
    7.26  Goal "[| G : preserves distr.Out; \
    7.27  \        D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
    7.28  \ ==> D Join G : Always \
    7.29 -\         {s. setsum (%i. bag_of (sublist (distr.In s) \
    7.30 -\                                 {k. k < length (iIn s) & iIn s ! k = i})) \
    7.31 -\                    (lessThan Nclients)   = \
    7.32 +\         {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (distr.In s) \
    7.33 +\                                 {k. k < length (iIn s) & iIn s ! k = i})) = \
    7.34  \             bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}";
    7.35  by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
    7.36  by Auto_tac; 
    7.37 @@ -133,7 +130,7 @@
    7.38  \     Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
    7.39  \     guarantees  \
    7.40  \      (INT i : lessThan Nclients. \
    7.41 -\       (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \
    7.42 +\       (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o distr.Out) s) \
    7.43  \       Fols \
    7.44  \       (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
    7.45  by (rtac guaranteesI 1);
    7.46 @@ -152,8 +149,8 @@
    7.47  Close_locale "Distrib";
    7.48  
    7.49  
    7.50 -Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s})  \
    7.51 -\     <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}";
    7.52 +Goal "!!f::nat=>nat. (INT i: lessThan n. {s. f i <= g i s})  \
    7.53 +\     <= {s. (\\<Sum>i: lessThan n. f i) <= (\\<Sum>i: lessThan n. g i s)}";
    7.54  by (induct_tac "n" 1);
    7.55  by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
    7.56  qed "alloc_refinement_lemma";
    7.57 @@ -177,8 +174,8 @@
    7.58  \ Int   \
    7.59  \ (INT hf. (INT i : lessThan Nclients.  \
    7.60  \        {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \
    7.61 -\ LeadsTo {s. setsum (%i. tokens (hf i)) (lessThan Nclients) <=         \
    7.62 -\   setsum (%i. (tokens o sub i o allocRel)s) (lessThan Nclients) })";
    7.63 +\ LeadsTo {s. (\\<Sum>i: lessThan Nclients. tokens (hf i)) <=         \
    7.64 +\   (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)})";
    7.65  by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib]));  
    7.66  by (rename_tac "F hf" 1);
    7.67  by (rtac ([Finite_stable_completion, alloc_refinement_lemma]
     8.1 --- a/src/HOL/UNITY/Follows.ML	Mon Oct 15 20:41:14 2001 +0200
     8.2 +++ b/src/HOL/UNITY/Follows.ML	Mon Oct 15 20:42:06 2001 +0200
     8.3 @@ -233,7 +233,7 @@
     8.4  
     8.5  Goal "!!f ::['c,'b] => ('a::order) multiset. \
     8.6  \       [| ALL i: I. F : f' i Fols f i;  finite I |] \
     8.7 -\       ==> F : (%s. setsum (%i. f' i s) I) Fols (%s. setsum (%i. f i s) I)";
     8.8 +\       ==> F : (%s. \\<Sum>i:I. f' i s) Fols (%s. \\<Sum>i:I. f i s)";
     8.9  by (etac rev_mp 1); 
    8.10  by (etac finite_induct 1);
    8.11  by (asm_simp_tac (simpset() addsimps [Follows_union]) 2);
     9.1 --- a/src/HOL/ex/NatSum.thy	Mon Oct 15 20:41:14 2001 +0200
     9.2 +++ b/src/HOL/ex/NatSum.thy	Mon Oct 15 20:42:06 2001 +0200
     9.3 @@ -1,21 +1,22 @@
     9.4  (*  Title:      HOL/ex/NatSum.ML
     9.5      ID:         $Id$
     9.6      Author:     Tobias Nipkow
     9.7 -    Copyright   1994 TU Muenchen
     9.8 -
     9.9 -Summing natural numbers, squares, cubes, etc.
    9.10 -
    9.11 -Originally demonstrated permutative rewriting, but add_ac is no longer
    9.12 -needed thanks to new simprocs.
    9.13 -
    9.14 -Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
    9.15 -http://www.research.att.com/~njas/sequences/
    9.16  *)
    9.17  
    9.18  header {* Summing natural numbers *}
    9.19  
    9.20  theory NatSum = Main:
    9.21  
    9.22 +text {*
    9.23 +  Summing natural numbers, squares, cubes, etc.
    9.24 +
    9.25 +  Originally demonstrated permutative rewriting, but @{thm [source]
    9.26 +  add_ac} is no longer needed thanks to new simprocs.
    9.27 +
    9.28 +  Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
    9.29 +  \url{http://www.research.att.com/~njas/sequences/}.
    9.30 +*}
    9.31 +
    9.32  declare lessThan_Suc [simp] atMost_Suc [simp]
    9.33  declare add_mult_distrib [simp] add_mult_distrib2 [simp]
    9.34  declare diff_mult_distrib [simp] diff_mult_distrib2 [simp]
    9.35 @@ -25,7 +26,7 @@
    9.36    squared.
    9.37  *}
    9.38  
    9.39 -lemma sum_of_odds: "setsum (\<lambda>i. Suc (i + i)) (lessThan n) = n * n"
    9.40 +lemma sum_of_odds: "(\<Sum>i \<in> {..n(}. Suc (i + i)) = n * n"
    9.41    apply (induct n)
    9.42     apply auto
    9.43    done
    9.44 @@ -36,11 +37,10 @@
    9.45  *}
    9.46  
    9.47  lemma sum_of_odd_squares:
    9.48 -  "3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
    9.49 -    n * (4 * n * n - Numeral1)"
    9.50 +  "3 * (\<Sum>i \<in> {..n(}. Suc (i + i) * Suc (i + i)) =
    9.51 +    n * (4 * n * n - 1)"
    9.52    apply (induct n)
    9.53 -  txt {* This removes the @{term "-Numeral1"} from the inductive step *}
    9.54 -   apply (case_tac [2] n)
    9.55 +   apply (case_tac [2] n)  -- {* eliminates the subtraction *}
    9.56      apply auto
    9.57    done
    9.58  
    9.59 @@ -50,11 +50,10 @@
    9.60  *}
    9.61  
    9.62  lemma sum_of_odd_cubes:
    9.63 -  "setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) =
    9.64 -    n * n * (2 * n * n - Numeral1)"
    9.65 -  apply (induct "n")
    9.66 -  txt {* This removes the @{term "-Numeral1"} from the inductive step *}
    9.67 -   apply (case_tac [2] "n")
    9.68 +  "(\<Sum>i \<in> {..n(}. Suc (i + i) * Suc (i + i) * Suc (i + i)) =
    9.69 +    n * n * (2 * n * n - 1)"
    9.70 +  apply (induct n)
    9.71 +   apply (case_tac [2] n)  -- {* eliminates the subtraction *}
    9.72      apply auto
    9.73    done
    9.74  
    9.75 @@ -63,19 +62,19 @@
    9.76    @{text "n (n + 1) / 2"}.*}
    9.77  
    9.78  lemma sum_of_naturals:
    9.79 -    "2 * setsum id (atMost n) = n * Suc n"
    9.80 +    "2 * (\<Sum>i \<in> {..n}. i) = n * Suc n"
    9.81    apply (induct n)
    9.82     apply auto
    9.83    done
    9.84  
    9.85  lemma sum_of_squares:
    9.86 -    "6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (2 * n)"
    9.87 +    "6 * (\<Sum>i \<in> {..n}. i * i) = n * Suc n * Suc (2 * n)"
    9.88    apply (induct n)
    9.89     apply auto
    9.90    done
    9.91  
    9.92  lemma sum_of_cubes:
    9.93 -    "4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
    9.94 +    "4 * (\<Sum>i \<in> {..n}. i * i * i) = n * n * Suc n * Suc n"
    9.95    apply (induct n)
    9.96     apply auto
    9.97    done
    9.98 @@ -86,12 +85,11 @@
    9.99  *}
   9.100  
   9.101  lemma sum_of_fourth_powers:
   9.102 -  "30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
   9.103 -    n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - Numeral1)"
   9.104 +  "30 * (\<Sum>i \<in> {..n}. i * i * i * i) =
   9.105 +    n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
   9.106    apply (induct n)
   9.107     apply auto
   9.108 -  txt {* Eliminates the subtraction *}
   9.109 -  apply (case_tac n)
   9.110 +  apply (case_tac n)  -- {* eliminates the subtraction *}
   9.111     apply simp_all
   9.112    done
   9.113  
   9.114 @@ -107,28 +105,30 @@
   9.115    zdiff_zmult_distrib2 [simp]
   9.116  
   9.117  lemma int_sum_of_fourth_powers:
   9.118 -  "30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
   9.119 -    int m * (int m - Numeral1) * (int (2 * m) - Numeral1) *
   9.120 -    (int (3 * m * m) - int (3 * m) - Numeral1)"
   9.121 +  "30 * int (\<Sum>i \<in> {..m(}. i * i * i * i) =
   9.122 +    int m * (int m - 1) * (int (2 * m) - 1) *
   9.123 +    (int (3 * m * m) - int (3 * m) - 1)"
   9.124    apply (induct m)
   9.125     apply simp_all
   9.126    done
   9.127  
   9.128  
   9.129  text {*
   9.130 -  \medskip Sums of geometric series: 2, 3 and the general case *}
   9.131 +  \medskip Sums of geometric series: @{term 2}, @{term 3} and the
   9.132 +  general case.
   9.133 +*}
   9.134  
   9.135 -lemma sum_of_2_powers: "setsum (\<lambda>i. 2^i) (lessThan n) = 2^n - (1::nat)"
   9.136 +lemma sum_of_2_powers: "(\<Sum>i \<in> {..n(}. 2^i) = 2^n - (1::nat)"
   9.137    apply (induct n)
   9.138 -   apply (auto split: nat_diff_split) 
   9.139 +   apply (auto split: nat_diff_split)
   9.140    done
   9.141  
   9.142 -lemma sum_of_3_powers: "2 * setsum (\<lambda>i. 3^i) (lessThan n) = 3^n - (1::nat)"
   9.143 +lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..n(}. 3^i) = 3^n - (1::nat)"
   9.144    apply (induct n)
   9.145     apply auto
   9.146    done
   9.147  
   9.148 -lemma sum_of_powers: "0 < k ==> (k - 1) * setsum (\<lambda>i. k^i) (lessThan n) = k^n - (1::nat)"
   9.149 +lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..n(}. k^i) = k^n - (1::nat)"
   9.150    apply (induct n)
   9.151     apply auto
   9.152    done