src/HOL/Finite_Set.thy
changeset 17189 b15f8e094874
parent 17149 e2b19c92ef51
child 17589 58eeffd73be1
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Aug 29 16:51:39 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Aug 30 12:47:53 2005 +0200
     1.3 @@ -806,11 +806,11 @@
     1.4  written @{text"\<Sum>x\<in>A. e"}. *}
     1.5  
     1.6  syntax
     1.7 -  "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
     1.8 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
     1.9  syntax (xsymbols)
    1.10 -  "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    1.11 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    1.12  syntax (HTML output)
    1.13 -  "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    1.14 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    1.15  
    1.16  translations -- {* Beware of argument permutation! *}
    1.17    "SUM i:A. b" == "setsum (%i. b) A"
    1.18 @@ -820,11 +820,11 @@
    1.19   @{text"\<Sum>x|P. e"}. *}
    1.20  
    1.21  syntax
    1.22 -  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
    1.23 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
    1.24  syntax (xsymbols)
    1.25 -  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.26 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.27  syntax (HTML output)
    1.28 -  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.29 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.30  
    1.31  translations
    1.32    "SUM x|P. t" => "setsum (%x. t) {x. P}"
    1.33 @@ -930,13 +930,12 @@
    1.34  (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
    1.35    the rhs need not be, since SIGMA A B could still be finite.*)
    1.36  lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
    1.37 -    (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
    1.38 -    (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
    1.39 +    (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
    1.40  by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong)
    1.41  
    1.42  text{*Here we can eliminate the finiteness assumptions, by cases.*}
    1.43  lemma setsum_cartesian_product: 
    1.44 -   "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
    1.45 +   "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
    1.46  apply (cases "finite A") 
    1.47   apply (cases "finite B") 
    1.48    apply (simp add: setsum_Sigma)
    1.49 @@ -1255,13 +1254,13 @@
    1.50  lemma setsum_commute:
    1.51    "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
    1.52  proof (simp add: setsum_cartesian_product)
    1.53 -  have "(\<Sum>z\<in>A \<times> B. f (fst z) (snd z)) =
    1.54 -    (\<Sum>z\<in>(%(i, j). (j, i)) ` (A \<times> B). f (snd z) (fst z))"
    1.55 +  have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
    1.56 +    (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
    1.57      (is "?s = _")
    1.58      apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
    1.59      apply (simp add: split_def)
    1.60      done
    1.61 -  also have "... = (\<Sum>z\<in>B \<times> A. f (snd z) (fst z))"
    1.62 +  also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
    1.63      (is "_ = ?t")
    1.64      apply (simp add: swap_product)
    1.65      done
    1.66 @@ -1276,11 +1275,11 @@
    1.67    "setprod f A == if finite A then fold (op *) f 1 A else 1"
    1.68  
    1.69  syntax
    1.70 -  "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
    1.71 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
    1.72  syntax (xsymbols)
    1.73 -  "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
    1.74 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
    1.75  syntax (HTML output)
    1.76 -  "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
    1.77 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
    1.78  
    1.79  translations -- {* Beware of argument permutation! *}
    1.80    "PROD i:A. b" == "setprod (%i. b) A" 
    1.81 @@ -1290,11 +1289,11 @@
    1.82   @{text"\<Prod>x|P. e"}. *}
    1.83  
    1.84  syntax
    1.85 -  "_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
    1.86 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
    1.87  syntax (xsymbols)
    1.88 -  "_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
    1.89 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
    1.90  syntax (HTML output)
    1.91 -  "_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
    1.92 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
    1.93  
    1.94  translations
    1.95    "PROD x|P. t" => "setprod (%x. t) {x. P}"
    1.96 @@ -1386,12 +1385,12 @@
    1.97  
    1.98  lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
    1.99      (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
   1.100 -    (\<Prod>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
   1.101 +    (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   1.102  by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong)
   1.103  
   1.104  text{*Here we can eliminate the finiteness assumptions, by cases.*}
   1.105  lemma setprod_cartesian_product: 
   1.106 -     "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>z\<in>(A <*> B). f (fst z) (snd z))"
   1.107 +     "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
   1.108  apply (cases "finite A") 
   1.109   apply (cases "finite B") 
   1.110    apply (simp add: setprod_Sigma)