src/HOL/Algebra/FiniteProduct.thy
changeset 14651 02b8f3bcf7fe
parent 14590 276ef51cedbf
child 14666 65f8680c3f16
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu Apr 22 11:00:22 2004 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Apr 22 11:01:34 2004 +0200
     1.3 @@ -9,9 +9,10 @@
     1.4  
     1.5  theory FiniteProduct = Group:
     1.6  
     1.7 -(* Instantiation of LC from Finite_Set.thy is not possible,
     1.8 -   because here we have explicit typing rules like x : carrier G.
     1.9 -   We introduce an explicit argument for the domain D *)
    1.10 +text {* Instantiation of @{text LC} from theory @{text Finite_Set} is not
    1.11 +  possible, because here we have explicit typing rules like @{text "x
    1.12 +  : carrier G"}.  We introduce an explicit argument for the domain
    1.13 +  @{text D}. *}
    1.14  
    1.15  consts
    1.16    foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
    1.17 @@ -281,14 +282,23 @@
    1.18  
    1.19  subsection {* Products over Finite Sets *}
    1.20  
    1.21 -constdefs
    1.22 -  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
    1.23 +constdefs (structure G)
    1.24 +  finprod :: "[_, 'a => 'b, 'a set] => 'b"
    1.25    "finprod G f A == if finite A
    1.26 -      then foldD (carrier G) (mult G o f) (one G) A
    1.27 +      then foldD (carrier G) (mult G o f) \<one> A
    1.28        else arbitrary"
    1.29  
    1.30 -(* TODO: nice syntax for the summation operator inside the locale
    1.31 -   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
    1.32 +syntax
    1.33 +  "_finprod" :: "index => idt => 'a set => 'b => 'b"
    1.34 +      ("\<Otimes>__:_. _" [1000, 0, 51, 10] 10)
    1.35 +syntax (xsymbols)
    1.36 +  "_finprod" :: "index => idt => 'a set => 'b => 'b"
    1.37 +      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
    1.38 +syntax (HTML output)
    1.39 +  "_finprod" :: "index => idt => 'a set => 'b => 'b"
    1.40 +      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
    1.41 +translations
    1.42 +  "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
    1.43  
    1.44  ML_setup {* 
    1.45    simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.46 @@ -324,7 +334,7 @@
    1.47    done
    1.48  
    1.49  lemma (in comm_monoid) finprod_one [simp]:
    1.50 -  "finite A ==> finprod G (%i. \<one>) A = \<one>"
    1.51 +  "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
    1.52  proof (induct set: Finites)
    1.53    case empty show ?case by simp
    1.54  next