src/HOL/Groups_List.thy
changeset 58368 fe083c681ed8
parent 58320 351810c45a48
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Groups_List.thy	Thu Sep 18 00:03:46 2014 +0200
     1.2 +++ b/src/HOL/Groups_List.thy	Thu Sep 18 15:07:43 2014 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  
     1.5  (* Author: Tobias Nipkow, TU Muenchen *)
     1.6  
     1.7 -header {* Sum over lists *}
     1.8 +header {* Sum and product over lists *}
     1.9  
    1.10  theory Groups_List
    1.11  imports List
    1.12 @@ -289,4 +289,63 @@
    1.13  
    1.14  end
    1.15  
    1.16 +
    1.17 +subsection {* List product *}
    1.18 +
    1.19 +context monoid_mult
    1.20 +begin
    1.21 +
    1.22 +definition listprod :: "'a list \<Rightarrow> 'a"
    1.23 +where
    1.24 +  "listprod  = monoid_list.F times 1"
    1.25 +
    1.26 +sublocale listprod!: monoid_list times 1
    1.27 +where
    1.28 +  "monoid_list.F times 1 = listprod"
    1.29 +proof -
    1.30 +  show "monoid_list times 1" ..
    1.31 +  then interpret listprod!: monoid_list times 1 .
    1.32 +  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    1.33 +qed
    1.34 +
    1.35  end
    1.36 +
    1.37 +context comm_monoid_mult
    1.38 +begin
    1.39 +
    1.40 +sublocale listprod!: comm_monoid_list times 1
    1.41 +where
    1.42 +  "monoid_list.F times 1 = listprod"
    1.43 +proof -
    1.44 +  show "comm_monoid_list times 1" ..
    1.45 +  then interpret listprod!: comm_monoid_list times 1 .
    1.46 +  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    1.47 +qed
    1.48 +
    1.49 +sublocale setprod!: comm_monoid_list_set times 1
    1.50 +where
    1.51 +  "monoid_list.F times 1 = listprod"
    1.52 +  and "comm_monoid_set.F times 1 = setprod"
    1.53 +proof -
    1.54 +  show "comm_monoid_list_set times 1" ..
    1.55 +  then interpret setprod!: comm_monoid_list_set times 1 .
    1.56 +  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    1.57 +  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    1.58 +qed
    1.59 +
    1.60 +end
    1.61 +
    1.62 +text {* Some syntactic sugar: *}
    1.63 +
    1.64 +syntax
    1.65 +  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
    1.66 +syntax (xsymbols)
    1.67 +  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
    1.68 +syntax (HTML output)
    1.69 +  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
    1.70 +
    1.71 +translations -- {* Beware of argument permutation! *}
    1.72 +  "PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
    1.73 +  "\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)"
    1.74 +
    1.75 +end