src/HOL/Algebra/FiniteProduct.thy
changeset 15095 63f5f4c265dd
parent 14750 8f1ee65bd3ea
child 15328 35951e6a7855
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sat Jul 31 20:54:23 2004 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Aug 02 09:44:46 2004 +0200
     1.3 @@ -283,7 +283,7 @@
     1.4  subsection {* Products over Finite Sets *}
     1.5  
     1.6  constdefs (structure G)
     1.7 -  finprod :: "[_, 'a => 'b, 'a set] => 'b"
     1.8 +  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
     1.9    "finprod G f A == if finite A
    1.10        then foldD (carrier G) (mult G o f) \<one> A
    1.11        else arbitrary"
    1.12 @@ -298,7 +298,8 @@
    1.13    "_finprod" :: "index => idt => 'a set => 'b => 'b"
    1.14        ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
    1.15  translations
    1.16 -  "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
    1.17 +  "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"
    1.18 +  -- {* Beware of argument permutation! *}
    1.19  
    1.20  ML_setup {* 
    1.21    simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.22 @@ -402,9 +403,8 @@
    1.23    from insert have ga: "g a \<in> carrier G" by fast
    1.24    from insert have fgA: "(%x. f x \<otimes> g x) \<in> A -> carrier G"
    1.25      by (simp add: Pi_def)
    1.26 -  show ?case  (* check if all simps are really necessary *)
    1.27 -    by (simp add: insert fA fa gA ga fgA m_ac Int_insert_left insert_absorb
    1.28 -      Int_mono2 Un_subset_iff)
    1.29 +  show ?case
    1.30 +    by (simp add: insert fA fa gA ga fgA m_ac)
    1.31  qed
    1.32  
    1.33  lemma (in comm_monoid) finprod_cong':