src/HOL/Groups_Big.thy
changeset 60353 838025c6e278
parent 59867 58043346ca64
child 60429 d3d1e185cd63
     1.1 --- a/src/HOL/Groups_Big.thy	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/src/HOL/Groups_Big.thy	Mon Jun 01 18:59:22 2015 +0200
     1.3 @@ -1153,10 +1153,29 @@
     1.4    shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
     1.5    using assms by (induct A) (auto simp: no_zero_divisors)
     1.6  
     1.7 -lemma (in field) setprod_diff1:
     1.8 -  "finite A \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow>
     1.9 -    (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
    1.10 -  by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
    1.11 +lemma (in semidom_divide) setprod_diff1:
    1.12 +  assumes "finite A" and "f a \<noteq> 0"
    1.13 +  shows "setprod f (A - {a}) = (if a \<in> A then divide (setprod f A) (f a) else setprod f A)"
    1.14 +proof (cases "a \<notin> A")
    1.15 +  case True then show ?thesis by simp
    1.16 +next
    1.17 +  case False with assms show ?thesis
    1.18 +  proof (induct A rule: finite_induct)
    1.19 +    case empty then show ?case by simp
    1.20 +  next
    1.21 +    case (insert b B)
    1.22 +    then show ?case
    1.23 +    proof (cases "a = b")
    1.24 +      case True with insert show ?thesis by simp
    1.25 +    next
    1.26 +      case False with insert have "a \<in> B" by simp
    1.27 +      def C \<equiv> "B - {a}"
    1.28 +      with `finite B` `a \<in> B`
    1.29 +        have *: "B = insert a C" "finite C" "a \<notin> C" by auto
    1.30 +      with insert show ?thesis by (auto simp add: insert_commute ac_simps)
    1.31 +    qed
    1.32 +  qed
    1.33 +qed
    1.34  
    1.35  lemma (in field) setprod_inversef: 
    1.36    "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"