src/HOL/Algebra/FiniteProduct.thy
changeset 29237 e90d9d51106b
parent 28524 644b62cf678f
child 31727 2621a957d417
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Tue Dec 16 15:09:37 2008 +0100
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Tue Dec 16 21:10:53 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Algebra/FiniteProduct.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Clemens Ballarin, started 19 November 2002
     1.7  
     1.8  This file is largely based on HOL/Finite_Set.thy.
     1.9 @@ -519,9 +518,9 @@
    1.10  lemma finprod_singleton:
    1.11    assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
    1.12    shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i"
    1.13 -  using i_in_A G.finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
    1.14 -    fin_A f_Pi G.finprod_one [of "A - {i}"]
    1.15 -    G.finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] 
    1.16 +  using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
    1.17 +    fin_A f_Pi finprod_one [of "A - {i}"]
    1.18 +    finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] 
    1.19    unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
    1.20  
    1.21  end