# HG changeset patch
# User wenzelm
# Date 1003171326 -7200
# Node ID 51ce34ef51136b6589d67aa052435cd3669c8952
# Parent  3087d6f19adc9a6f46af1ea2595ce63c74fb1cd8
setsum syntax;

diff -r 3087d6f19adc -r 51ce34ef5113 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/Finite.ML	Mon Oct 15 20:42:06 2001 +0200
@@ -716,14 +716,14 @@
 Addsimps [setsum_empty];
 
 Goalw [setsum_def]
- "!!f::'a=>'b::plus_ac0. [| finite F; a ~: F |] ==> \
-\      setsum f (insert a F) = f(a) + setsum f F";
+ "!!f. [| finite F; a ~: F |] ==> \
+\      setsum f (insert a F) = f a + setsum f F";
 by (asm_simp_tac (simpset() addsimps [export fold_insert,
 				      thm "plus_ac0_left_commute"]) 1);
 qed "setsum_insert";
 Addsimps [setsum_insert];
 
-Goal "setsum (%i. 0) A = (0::'a::plus_ac0)";
+Goal "setsum (%i. 0) A = 0";
 by (case_tac "finite A" 1);
  by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); 
 by (etac finite_induct 1);
@@ -751,7 +751,7 @@
 qed "card_eq_setsum";
 
 (*The reversed orientation looks more natural, but LOOPS as a simprule!*)
-Goal "!!g::'a=>'b::plus_ac0. [| finite A; finite B |] \
+Goal "!!g. [| finite A; finite B |] \
 \     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B";
 by (etac finite_induct 1);
 by (Simp_tac 1);
@@ -760,7 +760,7 @@
 qed "setsum_Un_Int";
 
 Goal "[| finite A; finite B; A Int B = {} |] \
-\     ==> setsum g (A Un B) = (setsum g A + setsum g B::'a::plus_ac0)";  
+\     ==> setsum g (A Un B) = setsum g A + setsum g B";
 by (stac (setsum_Un_Int RS sym) 1);
 by Auto_tac;
 qed "setsum_Un_disjoint";
@@ -779,7 +779,7 @@
 by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
 qed_spec_mp "setsum_UN_disjoint";
 
-Goal "setsum (%x. f x + g x) A = (setsum f A + setsum g A::'a::plus_ac0)";
+Goal "setsum (%x. f x + g x) A = (setsum f A + setsum g A)";
 by (case_tac "finite A" 1);
  by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
 by (etac finite_induct 1);
@@ -808,7 +808,7 @@
 
 val prems = Goal
     "[| A = B; !!x. x:B ==> f x = g x|] \
-\    ==> setsum f A = (setsum g B::'a::plus_ac0)";
+\    ==> setsum f A = setsum g B";
 by (case_tac "finite B" 1);
  by (asm_simp_tac (simpset() addsimps [setsum_def]@prems) 2); 
 by (simp_tac (simpset() addsimps prems) 1);
diff -r 3087d6f19adc -r 51ce34ef5113 src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/Finite.thy	Mon Oct 15 20:42:06 2001 +0200
@@ -36,7 +36,7 @@
   InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"
 
 constdefs
-  card :: 'a set => nat
+ card :: 'a set => nat
  "card A == THE n. (A,n) : cardR"
 
 (*
@@ -55,12 +55,20 @@
 	      ==> (insert x A, f x y) : foldSet f e"
 
 constdefs
-   fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
+  fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
   "fold f e A == THE x. (A,x) : foldSet f e"
 
-   setsum :: "('a => 'b) => 'a set => ('b::{plus, zero})"
+  setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
   "setsum f A == if finite A then fold (op+ o f) 0 A else 0"
 
+syntax
+  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\\<Sum>_:_. _" [0, 51, 10] 10)
+syntax (symbols)
+  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10)
+translations
+  "\\<Sum>i:A. b" == "setsum (%i. b) A"  (* Beware of argument permutation! *)
+
+
 locale LC =
   fixes
     f    :: ['b,'a] => 'a
diff -r 3087d6f19adc -r 51ce34ef5113 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Mon Oct 15 20:42:06 2001 +0200
@@ -118,7 +118,7 @@
   done
 
 lemma fib_mult_eq_setsum:
-    "fib (Suc n) * fib n = setsum (\<lambda>k. fib k * fib k) (atMost n)"
+    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   apply (induct n rule: fib.induct)
     apply (auto simp add: atMost_Suc fib.Suc_Suc)
   apply (simp add: add_mult_distrib add_mult_distrib2)
diff -r 3087d6f19adc -r 51ce34ef5113 src/HOL/UNITY/Comp/Alloc.ML
--- a/src/HOL/UNITY/Comp/Alloc.ML	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.ML	Mon Oct 15 20:42:06 2001 +0200
@@ -524,10 +524,8 @@
 
 (*safety (1), step 3*)
 Goal
-  "System : Always {s. setsum (%i. (tokens o sub i o allocGiv) s) \
-\                             (lessThan Nclients)                 \
-\           <= NbT + setsum (%i. (tokens o sub i o allocRel) s)   \
-\                           (lessThan Nclients)}";
+  "System : Always {s. (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv) s) \
+\           <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel) s)}";
 by (simp_tac (simpset() addsimps [o_apply]) 1);
 by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
 by (auto_tac (claset(), 
diff -r 3087d6f19adc -r 51ce34ef5113 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Oct 15 20:42:06 2001 +0200
@@ -52,8 +52,8 @@
   (*spec (1)*)
   system_safety :: 'a systemState program set
     "system_safety ==
-     Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients)
-     <= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}"
+     Always {s. (\\<Sum>i: lessThan Nclients. (tokens o giv o sub i o client)s)
+     <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
 
   (*spec (2)*)
   system_progress :: 'a systemState program set
@@ -111,8 +111,8 @@
     "alloc_safety ==
 	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
          guarantees
-	 Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
-         <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
+	 Always {s. (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv)s)
+         <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
 
   (*spec (8)*)
   alloc_progress :: 'a allocState_d program set
diff -r 3087d6f19adc -r 51ce34ef5113 src/HOL/UNITY/Comp/AllocBase.ML
--- a/src/HOL/UNITY/Comp/AllocBase.ML	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.ML	Mon Oct 15 20:42:06 2001 +0200
@@ -48,14 +48,14 @@
 
 Addcongs [setsum_cong];
 
-Goal "setsum (%i. {#if i<k then f i else g i#}) (A Int lessThan k) = \
-\     setsum (%i. {#f i#}) (A Int lessThan k)";
+Goal "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) = \
+\     (\\<Sum>i: A Int lessThan k. {#f i#})";
 by (rtac setsum_cong 1);
 by Auto_tac;  
 qed "bag_of_sublist_lemma";
 
 Goal "bag_of (sublist l A) = \
-\     setsum (%i. {# l!i #}) (A Int lessThan (length l))";
+\     (\\<Sum>i: A Int lessThan (length l). {# l!i #})";
 by (rev_induct_tac "l" 1);
 by (Simp_tac 1);
 by (asm_simp_tac
@@ -81,7 +81,7 @@
 
 Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
 \     ==> bag_of (sublist l (UNION I A)) =  \
-\         setsum (%i. bag_of (sublist l (A i))) I";  
+\         (\\<Sum>i:I. bag_of (sublist l (A i)))";  
 by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
 			    addsimps [bag_of_sublist]) 1);
 by (stac setsum_UN_disjoint 1);
diff -r 3087d6f19adc -r 51ce34ef5113 src/HOL/UNITY/Comp/AllocImpl.ML
--- a/src/HOL/UNITY/Comp/AllocImpl.ML	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.ML	Mon Oct 15 20:42:06 2001 +0200
@@ -44,9 +44,8 @@
 
 Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
 \ ==> M Join G : Always \
-\         {s. setsum (%i. bag_of (sublist (merge.Out s) \
-\                                 {k. k < length (iOut s) & iOut s ! k = i})) \
-\                    (lessThan Nclients)   =  \
+\         {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (merge.Out s) \
+\                                 {k. k < length (iOut s) & iOut s ! k = i})) = \
 \             (bag_of o merge.Out) s}";
 by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I,
 	   UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
@@ -65,8 +64,7 @@
 Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
 \         guarantees  \
 \            (bag_of o merge.Out) Fols \
-\            (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
-\                        (lessThan Nclients))";
+\            (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o merge.In) s)";
 by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
 by Auto_tac;  
 by (rtac Follows_setsum 1);
@@ -103,9 +101,8 @@
 Goal "[| G : preserves distr.Out; \
 \        D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
 \ ==> D Join G : Always \
-\         {s. setsum (%i. bag_of (sublist (distr.In s) \
-\                                 {k. k < length (iIn s) & iIn s ! k = i})) \
-\                    (lessThan Nclients)   = \
+\         {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (distr.In s) \
+\                                 {k. k < length (iIn s) & iIn s ! k = i})) = \
 \             bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}";
 by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
 by Auto_tac; 
@@ -133,7 +130,7 @@
 \     Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
 \     guarantees  \
 \      (INT i : lessThan Nclients. \
-\       (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \
+\       (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o distr.Out) s) \
 \       Fols \
 \       (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
 by (rtac guaranteesI 1);
@@ -152,8 +149,8 @@
 Close_locale "Distrib";
 
 
-Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s})  \
-\     <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}";
+Goal "!!f::nat=>nat. (INT i: lessThan n. {s. f i <= g i s})  \
+\     <= {s. (\\<Sum>i: lessThan n. f i) <= (\\<Sum>i: lessThan n. g i s)}";
 by (induct_tac "n" 1);
 by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
 qed "alloc_refinement_lemma";
@@ -177,8 +174,8 @@
 \ Int   \
 \ (INT hf. (INT i : lessThan Nclients.  \
 \        {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \
-\ LeadsTo {s. setsum (%i. tokens (hf i)) (lessThan Nclients) <=         \
-\   setsum (%i. (tokens o sub i o allocRel)s) (lessThan Nclients) })";
+\ LeadsTo {s. (\\<Sum>i: lessThan Nclients. tokens (hf i)) <=         \
+\   (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)})";
 by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib]));  
 by (rename_tac "F hf" 1);
 by (rtac ([Finite_stable_completion, alloc_refinement_lemma]
diff -r 3087d6f19adc -r 51ce34ef5113 src/HOL/UNITY/Follows.ML
--- a/src/HOL/UNITY/Follows.ML	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Follows.ML	Mon Oct 15 20:42:06 2001 +0200
@@ -233,7 +233,7 @@
 
 Goal "!!f ::['c,'b] => ('a::order) multiset. \
 \       [| ALL i: I. F : f' i Fols f i;  finite I |] \
-\       ==> F : (%s. setsum (%i. f' i s) I) Fols (%s. setsum (%i. f i s) I)";
+\       ==> F : (%s. \\<Sum>i:I. f' i s) Fols (%s. \\<Sum>i:I. f i s)";
 by (etac rev_mp 1); 
 by (etac finite_induct 1);
 by (asm_simp_tac (simpset() addsimps [Follows_union]) 2);
diff -r 3087d6f19adc -r 51ce34ef5113 src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/ex/NatSum.thy	Mon Oct 15 20:42:06 2001 +0200
@@ -1,21 +1,22 @@
 (*  Title:      HOL/ex/NatSum.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1994 TU Muenchen
-
-Summing natural numbers, squares, cubes, etc.
-
-Originally demonstrated permutative rewriting, but add_ac is no longer
-needed thanks to new simprocs.
-
-Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
-http://www.research.att.com/~njas/sequences/
 *)
 
 header {* Summing natural numbers *}
 
 theory NatSum = Main:
 
+text {*
+  Summing natural numbers, squares, cubes, etc.
+
+  Originally demonstrated permutative rewriting, but @{thm [source]
+  add_ac} is no longer needed thanks to new simprocs.
+
+  Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
+  \url{http://www.research.att.com/~njas/sequences/}.
+*}
+
 declare lessThan_Suc [simp] atMost_Suc [simp]
 declare add_mult_distrib [simp] add_mult_distrib2 [simp]
 declare diff_mult_distrib [simp] diff_mult_distrib2 [simp]
@@ -25,7 +26,7 @@
   squared.
 *}
 
-lemma sum_of_odds: "setsum (\<lambda>i. Suc (i + i)) (lessThan n) = n * n"
+lemma sum_of_odds: "(\<Sum>i \<in> {..n(}. Suc (i + i)) = n * n"
   apply (induct n)
    apply auto
   done
@@ -36,11 +37,10 @@
 *}
 
 lemma sum_of_odd_squares:
-  "3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
-    n * (4 * n * n - Numeral1)"
+  "3 * (\<Sum>i \<in> {..n(}. Suc (i + i) * Suc (i + i)) =
+    n * (4 * n * n - 1)"
   apply (induct n)
-  txt {* This removes the @{term "-Numeral1"} from the inductive step *}
-   apply (case_tac [2] n)
+   apply (case_tac [2] n)  -- {* eliminates the subtraction *}
     apply auto
   done
 
@@ -50,11 +50,10 @@
 *}
 
 lemma sum_of_odd_cubes:
-  "setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) =
-    n * n * (2 * n * n - Numeral1)"
-  apply (induct "n")
-  txt {* This removes the @{term "-Numeral1"} from the inductive step *}
-   apply (case_tac [2] "n")
+  "(\<Sum>i \<in> {..n(}. Suc (i + i) * Suc (i + i) * Suc (i + i)) =
+    n * n * (2 * n * n - 1)"
+  apply (induct n)
+   apply (case_tac [2] n)  -- {* eliminates the subtraction *}
     apply auto
   done
 
@@ -63,19 +62,19 @@
   @{text "n (n + 1) / 2"}.*}
 
 lemma sum_of_naturals:
-    "2 * setsum id (atMost n) = n * Suc n"
+    "2 * (\<Sum>i \<in> {..n}. i) = n * Suc n"
   apply (induct n)
    apply auto
   done
 
 lemma sum_of_squares:
-    "6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (2 * n)"
+    "6 * (\<Sum>i \<in> {..n}. i * i) = n * Suc n * Suc (2 * n)"
   apply (induct n)
    apply auto
   done
 
 lemma sum_of_cubes:
-    "4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
+    "4 * (\<Sum>i \<in> {..n}. i * i * i) = n * n * Suc n * Suc n"
   apply (induct n)
    apply auto
   done
@@ -86,12 +85,11 @@
 *}
 
 lemma sum_of_fourth_powers:
-  "30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
-    n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - Numeral1)"
+  "30 * (\<Sum>i \<in> {..n}. i * i * i * i) =
+    n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
   apply (induct n)
    apply auto
-  txt {* Eliminates the subtraction *}
-  apply (case_tac n)
+  apply (case_tac n)  -- {* eliminates the subtraction *}
    apply simp_all
   done
 
@@ -107,28 +105,30 @@
   zdiff_zmult_distrib2 [simp]
 
 lemma int_sum_of_fourth_powers:
-  "30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
-    int m * (int m - Numeral1) * (int (2 * m) - Numeral1) *
-    (int (3 * m * m) - int (3 * m) - Numeral1)"
+  "30 * int (\<Sum>i \<in> {..m(}. i * i * i * i) =
+    int m * (int m - 1) * (int (2 * m) - 1) *
+    (int (3 * m * m) - int (3 * m) - 1)"
   apply (induct m)
    apply simp_all
   done
 
 
 text {*
-  \medskip Sums of geometric series: 2, 3 and the general case *}
+  \medskip Sums of geometric series: @{term 2}, @{term 3} and the
+  general case.
+*}
 
-lemma sum_of_2_powers: "setsum (\<lambda>i. 2^i) (lessThan n) = 2^n - (1::nat)"
+lemma sum_of_2_powers: "(\<Sum>i \<in> {..n(}. 2^i) = 2^n - (1::nat)"
   apply (induct n)
-   apply (auto split: nat_diff_split) 
+   apply (auto split: nat_diff_split)
   done
 
-lemma sum_of_3_powers: "2 * setsum (\<lambda>i. 3^i) (lessThan n) = 3^n - (1::nat)"
+lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..n(}. 3^i) = 3^n - (1::nat)"
   apply (induct n)
    apply auto
   done
 
-lemma sum_of_powers: "0 < k ==> (k - 1) * setsum (\<lambda>i. k^i) (lessThan n) = k^n - (1::nat)"
+lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..n(}. k^i) = k^n - (1::nat)"
   apply (induct n)
    apply auto
   done