src/HOL/Algebra/FiniteProduct.thy
 changeset 35848 5443079512ea parent 35847 19f1f7066917 child 35849 b5522b51cb1e
```     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 15:57:40 2010 +0100
1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 16:51:37 2010 +0100
1.3 @@ -26,8 +26,9 @@
1.4
1.5  inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
1.6
1.7 -definition foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" where
1.8 -  "foldD D f e A == THE x. (A, x) \<in> foldSetD D f e"
1.9 +definition
1.10 +  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
1.11 +  where "foldD D f e A = (THE x. (A, x) \<in> foldSetD D f e)"
1.12
1.13  lemma foldSetD_closed:
1.14    "[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D
1.15 @@ -286,11 +287,11 @@
1.16  subsubsection {* Products over Finite Sets *}
1.17
1.18  definition
1.19 -  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" where
1.20 -  "finprod G f A ==
1.21 -    if finite A
1.22 +  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
1.23 +  where "finprod G f A =
1.24 +   (if finite A
1.25      then foldD (carrier G) (mult G o f) \<one>\<^bsub>G\<^esub> A
1.26 -    else undefined"
1.27 +    else undefined)"
1.28
1.29  syntax
1.30    "_finprod" :: "index => idt => 'a set => 'b => 'b"
```