Modified \<Sum> syntax a little.
--- 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)
--- 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
--- 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)
--- 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