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