product over monoids for lists
authorhaftmann
Thu Sep 18 15:07:43 2014 +0200 (2014-09-18)
changeset 58368fe083c681ed8
parent 58367 8af1e68d7e1a
child 58369 149fb885dcd8
product over monoids for lists
NEWS
src/HOL/Groups_List.thy
src/HOL/Library/RBT_Set.thy
     1.1 --- a/NEWS	Thu Sep 18 00:03:46 2014 +0200
     1.2 +++ b/NEWS	Thu Sep 18 15:07:43 2014 +0200
     1.3 @@ -73,6 +73,8 @@
     1.4        weak_case_cong ~> case_cong_weak
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 +* Product over lists via constant "listprod".
     1.8 +
     1.9  * Sledgehammer:
    1.10    - Minimization is now always enabled by default.
    1.11      Removed subcommand:
     2.1 --- a/src/HOL/Groups_List.thy	Thu Sep 18 00:03:46 2014 +0200
     2.2 +++ b/src/HOL/Groups_List.thy	Thu Sep 18 15:07:43 2014 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  
     2.5  (* Author: Tobias Nipkow, TU Muenchen *)
     2.6  
     2.7 -header {* Sum over lists *}
     2.8 +header {* Sum and product over lists *}
     2.9  
    2.10  theory Groups_List
    2.11  imports List
    2.12 @@ -289,4 +289,63 @@
    2.13  
    2.14  end
    2.15  
    2.16 +
    2.17 +subsection {* List product *}
    2.18 +
    2.19 +context monoid_mult
    2.20 +begin
    2.21 +
    2.22 +definition listprod :: "'a list \<Rightarrow> 'a"
    2.23 +where
    2.24 +  "listprod  = monoid_list.F times 1"
    2.25 +
    2.26 +sublocale listprod!: monoid_list times 1
    2.27 +where
    2.28 +  "monoid_list.F times 1 = listprod"
    2.29 +proof -
    2.30 +  show "monoid_list times 1" ..
    2.31 +  then interpret listprod!: monoid_list times 1 .
    2.32 +  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    2.33 +qed
    2.34 +
    2.35  end
    2.36 +
    2.37 +context comm_monoid_mult
    2.38 +begin
    2.39 +
    2.40 +sublocale listprod!: comm_monoid_list times 1
    2.41 +where
    2.42 +  "monoid_list.F times 1 = listprod"
    2.43 +proof -
    2.44 +  show "comm_monoid_list times 1" ..
    2.45 +  then interpret listprod!: comm_monoid_list times 1 .
    2.46 +  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    2.47 +qed
    2.48 +
    2.49 +sublocale setprod!: comm_monoid_list_set times 1
    2.50 +where
    2.51 +  "monoid_list.F times 1 = listprod"
    2.52 +  and "comm_monoid_set.F times 1 = setprod"
    2.53 +proof -
    2.54 +  show "comm_monoid_list_set times 1" ..
    2.55 +  then interpret setprod!: comm_monoid_list_set times 1 .
    2.56 +  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    2.57 +  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    2.58 +qed
    2.59 +
    2.60 +end
    2.61 +
    2.62 +text {* Some syntactic sugar: *}
    2.63 +
    2.64 +syntax
    2.65 +  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
    2.66 +syntax (xsymbols)
    2.67 +  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
    2.68 +syntax (HTML output)
    2.69 +  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
    2.70 +
    2.71 +translations -- {* Beware of argument permutation! *}
    2.72 +  "PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
    2.73 +  "\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)"
    2.74 +
    2.75 +end
     3.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Sep 18 00:03:46 2014 +0200
     3.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Sep 18 15:07:43 2014 +0200
     3.3 @@ -88,6 +88,9 @@
     3.4    "setsum = setsum" ..
     3.5  
     3.6  lemma [code, code del]:
     3.7 +  "setprod = setprod" ..
     3.8 +
     3.9 +lemma [code, code del]:
    3.10    "Product_Type.product = Product_Type.product"  ..
    3.11  
    3.12  lemma [code, code del]: