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)"
```