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"