src/HOL/Library/Product_plus.thy
changeset 37678 0040bafffdef
parent 37664 2946b8f057df
child 44066 d74182c93f04
     1.1 --- a/src/HOL/Library/Product_plus.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Library/Product_plus.thy	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  subsection {* Operations *}
     1.6  
     1.7 -instantiation "*" :: (zero, zero) zero
     1.8 +instantiation prod :: (zero, zero) zero
     1.9  begin
    1.10  
    1.11  definition zero_prod_def: "0 = (0, 0)"
    1.12 @@ -18,7 +18,7 @@
    1.13  instance ..
    1.14  end
    1.15  
    1.16 -instantiation "*" :: (plus, plus) plus
    1.17 +instantiation prod :: (plus, plus) plus
    1.18  begin
    1.19  
    1.20  definition plus_prod_def:
    1.21 @@ -27,7 +27,7 @@
    1.22  instance ..
    1.23  end
    1.24  
    1.25 -instantiation "*" :: (minus, minus) minus
    1.26 +instantiation prod :: (minus, minus) minus
    1.27  begin
    1.28  
    1.29  definition minus_prod_def:
    1.30 @@ -36,7 +36,7 @@
    1.31  instance ..
    1.32  end
    1.33  
    1.34 -instantiation "*" :: (uminus, uminus) uminus
    1.35 +instantiation prod :: (uminus, uminus) uminus
    1.36  begin
    1.37  
    1.38  definition uminus_prod_def:
    1.39 @@ -83,33 +83,33 @@
    1.40  
    1.41  subsection {* Class instances *}
    1.42  
    1.43 -instance "*" :: (semigroup_add, semigroup_add) semigroup_add
    1.44 +instance prod :: (semigroup_add, semigroup_add) semigroup_add
    1.45    by default (simp add: expand_prod_eq add_assoc)
    1.46  
    1.47 -instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    1.48 +instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    1.49    by default (simp add: expand_prod_eq add_commute)
    1.50  
    1.51 -instance "*" :: (monoid_add, monoid_add) monoid_add
    1.52 +instance prod :: (monoid_add, monoid_add) monoid_add
    1.53    by default (simp_all add: expand_prod_eq)
    1.54  
    1.55 -instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    1.56 +instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    1.57    by default (simp add: expand_prod_eq)
    1.58  
    1.59 -instance "*" ::
    1.60 +instance prod ::
    1.61    (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
    1.62      by default (simp_all add: expand_prod_eq)
    1.63  
    1.64 -instance "*" ::
    1.65 +instance prod ::
    1.66    (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    1.67      by default (simp add: expand_prod_eq)
    1.68  
    1.69 -instance "*" ::
    1.70 +instance prod ::
    1.71    (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    1.72  
    1.73 -instance "*" :: (group_add, group_add) group_add
    1.74 +instance prod :: (group_add, group_add) group_add
    1.75    by default (simp_all add: expand_prod_eq diff_minus)
    1.76  
    1.77 -instance "*" :: (ab_group_add, ab_group_add) ab_group_add
    1.78 +instance prod :: (ab_group_add, ab_group_add) ab_group_add
    1.79    by default (simp_all add: expand_prod_eq)
    1.80  
    1.81  lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"