src/HOL/Library/Product_plus.thy
changeset 60679 ade12ef2773c
parent 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Product_plus.thy	Mon Jul 06 22:06:02 2015 +0200
     1.2 +++ b/src/HOL/Library/Product_plus.thy	Mon Jul 06 22:57:34 2015 +0200
     1.3 @@ -81,41 +81,56 @@
     1.4  subsection \<open>Class instances\<close>
     1.5  
     1.6  instance prod :: (semigroup_add, semigroup_add) semigroup_add
     1.7 -  by default (simp add: prod_eq_iff add.assoc)
     1.8 +  by standard (simp add: prod_eq_iff add.assoc)
     1.9  
    1.10  instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
    1.11 -  by default (simp add: prod_eq_iff add.commute)
    1.12 +  by standard (simp add: prod_eq_iff add.commute)
    1.13  
    1.14  instance prod :: (monoid_add, monoid_add) monoid_add
    1.15 -  by default (simp_all add: prod_eq_iff)
    1.16 +  by standard (simp_all add: prod_eq_iff)
    1.17  
    1.18  instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
    1.19 -  by default (simp add: prod_eq_iff)
    1.20 +  by standard (simp add: prod_eq_iff)
    1.21  
    1.22 -instance prod ::
    1.23 -  (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
    1.24 -    by default (simp_all add: prod_eq_iff)
    1.25 +instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
    1.26 +    by standard (simp_all add: prod_eq_iff)
    1.27  
    1.28 -instance prod ::
    1.29 -  (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    1.30 -    by default (simp_all add: prod_eq_iff diff_diff_eq)
    1.31 +instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    1.32 +    by standard (simp_all add: prod_eq_iff diff_diff_eq)
    1.33  
    1.34 -instance prod ::
    1.35 -  (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    1.36 +instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    1.37  
    1.38  instance prod :: (group_add, group_add) group_add
    1.39 -  by default (simp_all add: prod_eq_iff)
    1.40 +  by standard (simp_all add: prod_eq_iff)
    1.41  
    1.42  instance prod :: (ab_group_add, ab_group_add) ab_group_add
    1.43 -  by default (simp_all add: prod_eq_iff)
    1.44 +  by standard (simp_all add: prod_eq_iff)
    1.45  
    1.46  lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
    1.47 -by (cases "finite A", induct set: finite, simp_all)
    1.48 +proof (cases "finite A")
    1.49 +  case True
    1.50 +  then show ?thesis by induct simp_all
    1.51 +next
    1.52 +  case False
    1.53 +  then show ?thesis by simp
    1.54 +qed
    1.55  
    1.56  lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
    1.57 -by (cases "finite A", induct set: finite, simp_all)
    1.58 +proof (cases "finite A")
    1.59 +  case True
    1.60 +  then show ?thesis by induct simp_all
    1.61 +next
    1.62 +  case False
    1.63 +  then show ?thesis by simp
    1.64 +qed
    1.65  
    1.66  lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
    1.67 -by (cases "finite A", induct set: finite) (simp_all add: zero_prod_def)
    1.68 +proof (cases "finite A")
    1.69 +  case True
    1.70 +  then show ?thesis by induct (simp_all add: zero_prod_def)
    1.71 +next
    1.72 +  case False
    1.73 +  then show ?thesis by (simp add: zero_prod_def)
    1.74 +qed
    1.75  
    1.76  end