src/HOL/Library/Product_plus.thy
changeset 44066 d74182c93f04
parent 37678 0040bafffdef
child 51002 496013a6eb38
     1.1 --- a/src/HOL/Library/Product_plus.thy	Mon Aug 08 10:26:26 2011 -0700
     1.2 +++ b/src/HOL/Library/Product_plus.thy	Mon Aug 08 10:32:55 2011 -0700
     1.3 @@ -78,39 +78,36 @@
     1.4  lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
     1.5    unfolding uminus_prod_def by simp
     1.6  
     1.7 -lemmas expand_prod_eq = Pair_fst_snd_eq
     1.8 -
     1.9 -
    1.10  subsection {* Class instances *}
    1.11  
    1.12  instance prod :: (semigroup_add, semigroup_add) semigroup_add
    1.13 -  by default (simp add: expand_prod_eq add_assoc)
    1.14 +  by default (simp add: prod_eq_iff add_assoc)
    1.15  
    1.16  instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    1.17 -  by default (simp add: expand_prod_eq add_commute)
    1.18 +  by default (simp add: prod_eq_iff add_commute)
    1.19  
    1.20  instance prod :: (monoid_add, monoid_add) monoid_add
    1.21 -  by default (simp_all add: expand_prod_eq)
    1.22 +  by default (simp_all add: prod_eq_iff)
    1.23  
    1.24  instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    1.25 -  by default (simp add: expand_prod_eq)
    1.26 +  by default (simp add: prod_eq_iff)
    1.27  
    1.28  instance prod ::
    1.29    (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
    1.30 -    by default (simp_all add: expand_prod_eq)
    1.31 +    by default (simp_all add: prod_eq_iff)
    1.32  
    1.33  instance prod ::
    1.34    (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    1.35 -    by default (simp add: expand_prod_eq)
    1.36 +    by default (simp add: prod_eq_iff)
    1.37  
    1.38  instance prod ::
    1.39    (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    1.40  
    1.41  instance prod :: (group_add, group_add) group_add
    1.42 -  by default (simp_all add: expand_prod_eq diff_minus)
    1.43 +  by default (simp_all add: prod_eq_iff diff_minus)
    1.44  
    1.45  instance prod :: (ab_group_add, ab_group_add) ab_group_add
    1.46 -  by default (simp_all add: expand_prod_eq)
    1.47 +  by default (simp_all add: prod_eq_iff)
    1.48  
    1.49  lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
    1.50  by (cases "finite A", induct set: finite, simp_all)