src/HOL/Groups_Big.thy
changeset 61955 e96292f32c3c
parent 61952 546958347e05
child 62376 85f38d5f8807
     1.1 --- a/src/HOL/Groups_Big.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Groups_Big.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -471,35 +471,28 @@
     1.4  defines
     1.5    setsum = setsum.F ..
     1.6  
     1.7 -abbreviation
     1.8 -  Setsum ("\<Sum>_" [1000] 999) where
     1.9 -  "\<Sum>A \<equiv> setsum (%x. x) A"
    1.10 +abbreviation Setsum ("\<Sum>_" [1000] 999)
    1.11 +  where "\<Sum>A \<equiv> setsum (\<lambda>x. x) A"
    1.12  
    1.13  end
    1.14  
    1.15 -text\<open>Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
    1.16 -written \<open>\<Sum>x\<in>A. e\<close>.\<close>
    1.17 +text \<open>Now: lot's of fancy syntax. First, @{term "setsum (\<lambda>x. e) A"} is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
    1.18  
    1.19 +syntax (ASCII)
    1.20 +  "_setsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(3SUM _:_./ _)" [0, 51, 10] 10)
    1.21  syntax
    1.22 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_./ _)" [0, 51, 10] 10)
    1.23 -syntax (xsymbols)
    1.24 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
    1.25 -
    1.26 +  "_setsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
    1.27  translations \<comment> \<open>Beware of argument permutation!\<close>
    1.28 -  "SUM i:A. b" == "CONST setsum (%i. b) A"
    1.29 -  "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
    1.30 +  "\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST setsum (\<lambda>i. b) A"
    1.31  
    1.32 -text\<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
    1.33 - \<open>\<Sum>x|P. e\<close>.\<close>
    1.34 +text \<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>
    1.35  
    1.36 +syntax (ASCII)
    1.37 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SUM _ |/ _./ _)" [0, 0, 10] 10)
    1.38  syntax
    1.39 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
    1.40 -syntax (xsymbols)
    1.41 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.42 -
    1.43 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Sum>_ | (_)./ _)" [0, 0, 10] 10)
    1.44  translations
    1.45 -  "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
    1.46 -  "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
    1.47 +  "\<Sum>x|P. t" => "CONST setsum (\<lambda>x. t) {x. P}"
    1.48  
    1.49  print_translation \<open>
    1.50  let
    1.51 @@ -1059,26 +1052,21 @@
    1.52  
    1.53  end
    1.54  
    1.55 -syntax
    1.56 +syntax (ASCII)
    1.57    "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
    1.58 -syntax (xsymbols)
    1.59 +syntax
    1.60    "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
    1.61 -
    1.62  translations \<comment> \<open>Beware of argument permutation!\<close>
    1.63 -  "PROD i:A. b" == "CONST setprod (%i. b) A" 
    1.64 -  "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
    1.65 +  "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A" 
    1.66  
    1.67 -text\<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
    1.68 - \<open>\<Prod>x|P. e\<close>.\<close>
    1.69 +text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
    1.70  
    1.71 +syntax (ASCII)
    1.72 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
    1.73  syntax
    1.74 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
    1.75 -syntax (xsymbols)
    1.76 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
    1.77 -
    1.78 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
    1.79  translations
    1.80 -  "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
    1.81 -  "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
    1.82 +  "\<Prod>x|P. t" => "CONST setprod (\<lambda>x. t) {x. P}"
    1.83  
    1.84  context comm_monoid_mult
    1.85  begin