src/HOL/Groups_Big.thy
 changeset 59010 ec2b4270a502 parent 58889 5b7a9633cfa8 child 59416 fde2659085e1
```     1.1 --- a/src/HOL/Groups_Big.thy	Mon Nov 17 14:55:33 2014 +0100
1.2 +++ b/src/HOL/Groups_Big.thy	Mon Nov 17 14:55:34 2014 +0100
1.3 @@ -926,6 +926,10 @@
1.4    case True then show ?thesis by (induct A) (simp_all add: assms)
1.5  qed
1.6
1.7 +lemma (in comm_semiring_1) dvd_setsum:
1.8 +  "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
1.9 +  by (induct A rule: infinite_finite_induct) simp_all
1.10 +
1.11
1.12  subsubsection {* Cardinality as special case of @{const setsum} *}
1.13
1.14 @@ -1072,128 +1076,133 @@
1.15    "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
1.16    "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
1.17
1.18 +context comm_monoid_mult
1.19 +begin
1.20 +
1.21 +lemma setprod_dvd_setprod:
1.22 +  "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
1.23 +proof (induct A rule: infinite_finite_induct)
1.24 +  case infinite then show ?case by (auto intro: dvdI)
1.25 +next
1.26 +  case empty then show ?case by (auto intro: dvdI)
1.27 +next
1.28 +  case (insert a A) then
1.29 +  have "f a dvd g a" and "setprod f A dvd setprod g A" by simp_all
1.30 +  then obtain r s where "g a = f a * r" and "setprod g A = setprod f A * s" by (auto elim!: dvdE)
1.31 +  then have "g a * setprod g A = f a * setprod f A * (r * s)" by (simp add: ac_simps)
1.32 +  with insert.hyps show ?case by (auto intro: dvdI)
1.33 +qed
1.34 +
1.35 +lemma setprod_dvd_setprod_subset:
1.36 +  "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> setprod f A dvd setprod f B"
1.37 +  by (auto simp add: setprod.subset_diff ac_simps intro: dvdI)
1.38 +
1.39 +end
1.40 +
1.41
1.42  subsubsection {* Properties in more restricted classes of structures *}
1.43
1.44 -lemma setprod_zero:
1.45 -     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
1.46 -apply (induct set: finite, force, clarsimp)
1.47 -apply (erule disjE, auto)
1.48 -done
1.49 -
1.50 -lemma setprod_zero_iff[simp]: "finite A ==>
1.51 -  (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
1.52 -  (EX x: A. f x = 0)"
1.53 -by (erule finite_induct, auto simp:no_zero_divisors)
1.54 +context comm_semiring_1
1.55 +begin
1.56
1.57 -lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
1.58 -  (setprod f (A Un B) :: 'a ::{field})
1.59 -   = setprod f A * setprod f B / setprod f (A Int B)"
1.60 -by (subst setprod.union_inter [symmetric], auto)
1.61 -
1.62 -lemma setprod_nonneg [rule_format]:
1.63 -   "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
1.64 -by (cases "finite A", induct set: finite, simp_all)
1.65 -
1.66 -lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
1.67 -  --> 0 < setprod f A"
1.68 -by (cases "finite A", induct set: finite, simp_all)
1.69 -
1.70 -lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
1.71 -  (setprod f (A - {a}) :: 'a :: {field}) =
1.72 -  (if a:A then setprod f A / f a else setprod f A)"
1.73 -  by (erule finite_induct) (auto simp add: insert_Diff_if)
1.74 +lemma dvd_setprod_eqI [intro]:
1.75 +  assumes "finite A" and "a \<in> A" and "b = f a"
1.76 +  shows "b dvd setprod f A"
1.77 +proof -
1.78 +  from `finite A` have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
1.79 +    by (intro setprod.insert) auto
1.80 +  also from `a \<in> A` have "insert a (A - {a}) = A" by blast
1.81 +  finally have "setprod f A = f a * setprod f (A - {a})" .
1.82 +  with `b = f a` show ?thesis by simp
1.83 +qed
1.84
1.85 -lemma setprod_inversef:
1.86 -  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
1.87 -  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
1.88 -by (erule finite_induct) auto
1.89 +lemma dvd_setprodI [intro]:
1.90 +  assumes "finite A" and "a \<in> A"
1.91 +  shows "f a dvd setprod f A"
1.92 +  using assms by auto
1.93
1.94 -lemma setprod_dividef:
1.95 -  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
1.96 -  shows "finite A
1.97 -    ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
1.98 -apply (subgoal_tac
1.99 -         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
1.100 -apply (erule ssubst)
1.101 -apply (subst divide_inverse)
1.102 -apply (subst setprod.distrib)
1.103 -apply (subst setprod_inversef, assumption+, rule refl)
1.104 -apply (rule setprod.cong, rule refl)
1.105 -apply (subst divide_inverse, auto)
1.106 -done
1.107 -
1.108 -lemma setprod_dvd_setprod [rule_format]:
1.109 -    "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
1.110 -  apply (cases "finite A")
1.111 -  apply (induct set: finite)
1.112 -  apply (auto simp add: dvd_def)
1.113 -  apply (rule_tac x = "k * ka" in exI)
1.114 -  apply (simp add: algebra_simps)
1.115 -done
1.116 -
1.117 -lemma setprod_dvd_setprod_subset:
1.118 -  "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
1.119 -  apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
1.120 -  apply (unfold dvd_def, blast)
1.121 -  apply (subst setprod.union_disjoint [symmetric])
1.122 -  apply (auto elim: finite_subset intro: setprod.cong)
1.123 -done
1.124 +lemma setprod_zero:
1.125 +  assumes "finite A" and "\<exists>a\<in>A. f a = 0"
1.126 +  shows "setprod f A = 0"
1.127 +using assms proof (induct A)
1.128 +  case empty then show ?case by simp
1.129 +next
1.130 +  case (insert a A)
1.131 +  then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
1.132 +  then have "f a * setprod f A = 0" by rule (simp_all add: insert)
1.133 +  with insert show ?case by simp
1.134 +qed
1.135
1.136  lemma setprod_dvd_setprod_subset2:
1.137 -  "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow>
1.138 -      setprod f A dvd setprod g B"
1.139 -  apply (rule dvd_trans)
1.140 -  apply (rule setprod_dvd_setprod, erule (1) bspec)
1.141 -  apply (erule (1) setprod_dvd_setprod_subset)
1.142 -done
1.143 +  assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
1.144 +  shows "setprod f A dvd setprod g B"
1.145 +proof -
1.146 +  from assms have "setprod f A dvd setprod g A"
1.147 +    by (auto intro: setprod_dvd_setprod)
1.148 +  moreover from assms have "setprod g A dvd setprod g B"
1.149 +    by (auto intro: setprod_dvd_setprod_subset)
1.150 +  ultimately show ?thesis by (rule dvd_trans)
1.151 +qed
1.152 +
1.153 +end
1.154 +
1.155 +lemma setprod_zero_iff [simp]:
1.156 +  assumes "finite A"
1.157 +  shows "setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors}) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
1.158 +  using assms by (induct A) (auto simp: no_zero_divisors)
1.159 +
1.160 +lemma (in field) setprod_diff1:
1.161 +  "finite A \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow>
1.162 +    (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
1.163 +  by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
1.164
1.165 -lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow>
1.166 -    (f i ::'a::comm_semiring_1) dvd setprod f A"
1.167 -by (induct set: finite) (auto intro: dvd_mult)
1.168 +lemma (in field_inverse_zero) setprod_inversef:
1.169 +  "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
1.170 +  by (induct A rule: finite_induct) simp_all
1.171 +
1.172 +lemma (in field_inverse_zero) setprod_dividef:
1.173 +  "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
1.174 +  using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
1.175
1.176 -lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow>
1.177 -    (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
1.178 -  apply (cases "finite A")
1.179 -  apply (induct set: finite)
1.180 -  apply auto
1.181 -done
1.182 +lemma setprod_Un:
1.183 +  fixes f :: "'b \<Rightarrow> 'a :: field"
1.184 +  assumes "finite A" and "finite B"
1.185 +  and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
1.186 +  shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)"
1.187 +proof -
1.188 +  from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)"
1.189 +    by (simp add: setprod.union_inter [symmetric, of A B])
1.190 +  with assms show ?thesis by simp
1.191 +qed
1.192
1.193 -lemma setprod_mono:
1.194 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
1.195 +lemma (in linordered_semidom) setprod_nonneg:
1.196 +  "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A"
1.197 +  by (induct A rule: infinite_finite_induct) simp_all
1.198 +
1.199 +lemma (in linordered_semidom) setprod_pos:
1.200 +  "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A"
1.201 +  by (induct A rule: infinite_finite_induct) simp_all
1.202 +
1.203 +lemma (in linordered_semidom) setprod_mono:
1.204    assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
1.205    shows "setprod f A \<le> setprod g A"
1.206 -proof (cases "finite A")
1.207 -  case True
1.208 -  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
1.209 -  proof (induct A rule: finite_subset_induct)
1.210 -    case (insert a F)
1.211 -    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
1.212 -      unfolding setprod.insert[OF insert(1,3)]
1.213 -      using assms[rule_format,OF insert(2)] insert
1.214 -      by (auto intro: mult_mono)
1.215 -  qed auto
1.216 -  thus ?thesis by simp
1.217 -qed auto
1.218 +  using assms by (induct A rule: infinite_finite_induct)
1.219 +    (auto intro!: setprod_nonneg mult_mono)
1.220
1.221 -lemma abs_setprod:
1.222 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
1.223 -  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
1.224 -proof (cases "finite A")
1.225 -  case True thus ?thesis
1.226 -    by induct (auto simp add: field_simps abs_mult)
1.227 -qed auto
1.228 +lemma (in linordered_field) abs_setprod:
1.229 +  "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
1.230 +  by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
1.231
1.232  lemma setprod_eq_1_iff [simp]:
1.233 -  "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
1.234 -  by (induct set: finite) auto
1.235 +  "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))"
1.236 +  by (induct A rule: finite_induct) simp_all
1.237
1.238  lemma setprod_pos_nat:
1.239 -  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
1.240 -using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
1.241 +  "finite A \<Longrightarrow> (\<forall>a\<in>A. f a > (0::nat)) \<Longrightarrow> setprod f A > 0"
1.242 +  using setprod_zero_iff by (simp del: neq0_conv add: neq0_conv [symmetric])
1.243
1.244 -lemma setprod_pos_nat_iff[simp]:
1.245 -  "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
1.246 -using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
1.247 +lemma setprod_pos_nat_iff [simp]:
1.248 +  "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
1.249 +  using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
1.250
1.251  end
```