# HG changeset patch
# User nipkow
# Date 1090510651 -7200
# Node ID 277b3a4da3411bbb85fec2ea7c8ec4b5ceb79ba2
# Parent  279c2daaf5171e33828bee6b9ad8625137a091b7
Modified \<Sum> syntax a little.

diff -r 279c2daaf517 -r 277b3a4da341 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jul 22 12:55:36 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jul 22 17:37:31 2004 +0200
@@ -765,25 +765,29 @@
 written @{text"\<Sum>x\<in>A. e"}. *}
 
 syntax
-  "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_:_. _)" [0, 51, 10] 10)
+  "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
 syntax (xsymbols)
   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
 syntax (HTML output)
   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
-translations
-  "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
+
+translations -- {* Beware of argument permutation! *}
+  "SUM i:A. b" == "setsum (%i. b) A"
+  "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
 
 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
  @{text"\<Sum>x|P. e"}. *}
 
 syntax
-  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ | / _./ _)" [0,0,10] 10)
+  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
 syntax (xsymbols)
   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
 syntax (HTML output)
   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
 
-translations "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
+translations
+  "SUM x|P. t" => "setsum (%x. t) {x. P}"
+  "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
 
 print_translation {*
 let
@@ -894,8 +898,8 @@
   done
 
 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
-    (\<Sum>x:A. (\<Sum>y:B x. f x y)) =
-    (\<Sum>z:(SIGMA x:A. B x). f (fst z) (snd z))"
+    (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
+    (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
   apply (subst Sigma_def)
   apply (subst setsum_UN_disjoint)
   apply assumption
@@ -911,8 +915,8 @@
   done
 
 lemma setsum_cartesian_product: "finite A ==> finite B ==>
-    (\<Sum>x:A. (\<Sum>y:B. f x y)) =
-    (\<Sum>z:A <*> B. f (fst z) (snd z))"
+    (\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) =
+    (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
   by (erule setsum_Sigma, auto);
 
 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
@@ -936,7 +940,7 @@
   by (induct set: Finites) auto
 
 lemma setsum_constant_nat:
-    "finite A ==> (\<Sum>x: A. y) = (card A) * y"
+    "finite A ==> (\<Sum>x\<in>A. y) = (card A) * y"
   -- {* Generalized to any @{text comm_semiring_1_cancel} in
         @{text IntDef} as @{text setsum_constant}. *}
   by (erule finite_induct, auto)
@@ -1047,7 +1051,7 @@
 
 lemma card_SigmaI [rule_format,simp]: "finite A ==>
   (ALL a:A. finite (B a)) -->
-  card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))"
+  card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
   apply (erule finite_induct, auto)
   apply (subst SigmaI_insert, assumption)
   apply (subst card_Un_disjoint)
diff -r 279c2daaf517 -r 277b3a4da341 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 22 12:55:36 2004 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 22 17:37:31 2004 +0200
@@ -52,8 +52,8 @@
   (*spec (1)*)
   system_safety :: 'a systemState program set
     "system_safety ==
-     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)}"
+     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. (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv)s)
-         <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
+	 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 279c2daaf517 -r 277b3a4da341 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 22 12:55:36 2004 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 22 17:37:31 2004 +0200
@@ -71,13 +71,13 @@
 declare setsum_cong [cong]
 
 lemma bag_of_sublist_lemma:
-     "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
-      (\<Sum>i: A Int lessThan k. {#f i#})"
+     "(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) =  
+      (\<Sum>i\<in> A Int lessThan k. {#f i#})"
 by (rule setsum_cong, auto)
 
 lemma bag_of_sublist:
      "bag_of (sublist l A) =  
-      (\<Sum>i: A Int lessThan (length l). {# l!i #})"
+      (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
 apply (rule_tac xs = l in rev_induct, simp)
 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
                  bag_of_sublist_lemma add_ac)
@@ -101,7 +101,7 @@
 lemma bag_of_sublist_UN_disjoint [rule_format]:
      "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
       ==> bag_of (sublist l (UNION I A)) =   
-          (\<Sum>i:I. bag_of (sublist l (A i)))"
+          (\<Sum>i\<in>I. bag_of (sublist l (A i)))"
 apply (simp del: UN_simps 
             add: UN_simps [symmetric] add: bag_of_sublist)
 apply (subst setsum_UN_disjoint, auto)
diff -r 279c2daaf517 -r 277b3a4da341 src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 22 12:55:36 2004 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 22 17:37:31 2004 +0200
@@ -353,7 +353,7 @@
 
 lemma alloc_refinement_lemma:
      "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
-      \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x: lessThan n. g x s)}"
+      \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}"
 apply (induct_tac "n")
 apply (auto simp add: lessThan_Suc)
 done