product over monoids for lists

--- a/NEWS	Thu Sep 18 00:03:46 2014 +0200
+++ b/NEWS	Thu Sep 18 15:07:43 2014 +0200
@@ -73,6 +73,8 @@
       weak_case_cong ~> case_cong_weak
     INCOMPATIBILITY.
 
+* Product over lists via constant "listprod".
+
 * Sledgehammer:
   - Minimization is now always enabled by default.
     Removed subcommand:

--- a/src/HOL/Groups_List.thy	Thu Sep 18 00:03:46 2014 +0200
+++ b/src/HOL/Groups_List.thy	Thu Sep 18 15:07:43 2014 +0200
@@ -1,7 +1,7 @@
 
 (* Author: Tobias Nipkow, TU Muenchen *)
 
-header {* Sum over lists *}
+header {* Sum and product over lists *}
 
 theory Groups_List
 imports List
@@ -289,4 +289,63 @@
 
 end
 
+
+subsection {* List product *}
+
+context monoid_mult
+begin
+
+definition listprod :: "'a list \<Rightarrow> 'a"
+where
+  "listprod  = monoid_list.F times 1"
+
+sublocale listprod!: monoid_list times 1
+where
+  "monoid_list.F times 1 = listprod"
+proof -
+  show "monoid_list times 1" ..
+  then interpret listprod!: monoid_list times 1 .
+  from listprod_def show "monoid_list.F times 1 = listprod" by rule
+qed
+
 end
+
+context comm_monoid_mult
+begin
+
+sublocale listprod!: comm_monoid_list times 1
+where
+  "monoid_list.F times 1 = listprod"
+proof -
+  show "comm_monoid_list times 1" ..
+  then interpret listprod!: comm_monoid_list times 1 .
+  from listprod_def show "monoid_list.F times 1 = listprod" by rule
+qed
+
+sublocale setprod!: comm_monoid_list_set times 1
+where
+  "monoid_list.F times 1 = listprod"
+  and "comm_monoid_set.F times 1 = setprod"
+proof -
+  show "comm_monoid_list_set times 1" ..
+  then interpret setprod!: comm_monoid_list_set times 1 .
+  from listprod_def show "monoid_list.F times 1 = listprod" by rule
+  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
+qed
+
+end
+
+text {* Some syntactic sugar: *}
+
+syntax
+  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
+syntax (xsymbols)
+  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
+syntax (HTML output)
+  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
+
+translations -- {* Beware of argument permutation! *}
+  "PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
+  "\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)"
+
+end

--- a/src/HOL/Library/RBT_Set.thy	Thu Sep 18 00:03:46 2014 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Thu Sep 18 15:07:43 2014 +0200
@@ -88,6 +88,9 @@
   "setsum = setsum" ..
 
 lemma [code, code del]:
+  "setprod = setprod" ..
+
+lemma [code, code del]:
   "Product_Type.product = Product_Type.product"  ..
 
 lemma [code, code del]: