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"\x\A. e"}. *} syntax - "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\_:_. _)" [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\_\_. _)" [0, 51, 10] 10) syntax (HTML output) "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\_\_. _)" [0, 51, 10] 10) -translations - "\i:A. b" == "setsum (%i. b) A" -- {* Beware of argument permutation! *} + +translations -- {* Beware of argument permutation! *} + "SUM i:A. b" == "setsum (%i. b) A" + "\i\A. b" == "setsum (%i. b) A" text{* Instead of @{term"\x\{x. P}. e"} we introduce the shorter @{text"\x|P. e"}. *} syntax - "_qsetsum" :: "idt \ bool \ 'a \ 'a" ("(3SUM _ | / _./ _)" [0,0,10] 10) + "_qsetsum" :: "idt \ bool \ 'a \ 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10) syntax (xsymbols) "_qsetsum" :: "idt \ bool \ 'a \ 'a" ("(3\_ | (_)./ _)" [0,0,10] 10) syntax (HTML output) "_qsetsum" :: "idt \ bool \ 'a \ 'a" ("(3\_ | (_)./ _)" [0,0,10] 10) -translations "\x|P. t" => "setsum (%x. t) {x. P}" +translations + "SUM x|P. t" => "setsum (%x. t) {x. P}" + "\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) ==> - (\x:A. (\y:B x. f x y)) = - (\z:(SIGMA x:A. B x). f (fst z) (snd z))" + (\x\A. (\y\B x. f x y)) = + (\z\(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 ==> - (\x:A. (\y:B. f x y)) = - (\z:A <*> B. f (fst z) (snd z))" + (\x\A. (\y\B. f x y)) = + (\z\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 ==> (\x: A. y) = (card A) * y" + "finite A ==> (\x\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) = (\a: A. card (B a))" + card (SIGMA x: A. B x) = (\a\A. card (B a))" apply (erule finite_induct, auto) apply (subst SigmaI_insert, assumption) apply (subst card_Un_disjoint)