generalized lemmas and tuned proofs
authorhaftmann
Mon Nov 17 14:55:34 2014 +0100 (2014-11-17)
changeset 59010ec2b4270a502
parent 59009 348561aa3869
child 59011 4902a2fec434
generalized lemmas and tuned proofs
src/HOL/Groups_Big.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/UniqueFactorization.thy
     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
     2.1 --- a/src/HOL/Number_Theory/Cong.thy	Mon Nov 17 14:55:33 2014 +0100
     2.2 +++ b/src/HOL/Number_Theory/Cong.thy	Mon Nov 17 14:55:34 2014 +0100
     2.3 @@ -820,7 +820,7 @@
     2.4          apply (drule (1) bspec)
     2.5          apply (erule conjE)
     2.6          apply assumption
     2.7 -        apply (rule dvd_setprod)
     2.8 +        apply rule
     2.9          using fin a apply auto
    2.10          done
    2.11        finally show ?thesis
    2.12 @@ -863,7 +863,7 @@
    2.13      apply (rule cong_dvd_modulus_nat)
    2.14      apply (rule cong_mod_nat)
    2.15      using prodnz apply auto
    2.16 -    apply (rule dvd_setprod)
    2.17 +    apply rule
    2.18      apply (rule fin)
    2.19      apply assumption
    2.20      done
     3.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:33 2014 +0100
     3.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:34 2014 +0100
     3.3 @@ -7,21 +7,6 @@
     3.4  begin
     3.5  
     3.6  context semiring_div
     3.7 -begin
     3.8 -
     3.9 -lemma dvd_setprod [intro]:
    3.10 -  assumes "finite A" and "x \<in> A"
    3.11 -  shows "f x dvd setprod f A"
    3.12 -proof
    3.13 -  from `finite A` have "setprod f (insert x (A - {x})) = f x * setprod f (A - {x})"
    3.14 -    by (intro setprod.insert) auto
    3.15 -  also from `x \<in> A` have "insert x (A - {x}) = A" by blast
    3.16 -  finally show "setprod f A = f x * setprod f (A - {x})" .
    3.17 -qed
    3.18 -
    3.19 -end
    3.20 -
    3.21 -context semiring_div
    3.22  begin 
    3.23  
    3.24  definition ring_inv :: "'a \<Rightarrow> 'a"
    3.25 @@ -1463,7 +1448,7 @@
    3.26        apply (rule no_zero_divisors)
    3.27        apply blast+
    3.28        done
    3.29 -    moreover from `finite A` have "\<forall>x\<in>A. x dvd \<Prod>A" by (intro ballI dvd_setprod)
    3.30 +    moreover from `finite A` have "\<forall>x\<in>A. x dvd \<Prod>A" by blast
    3.31      ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l)" by blast
    3.32      with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
    3.33    }
     4.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Nov 17 14:55:33 2014 +0100
     4.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Nov 17 14:55:34 2014 +0100
     4.3 @@ -79,7 +79,7 @@
     4.4    assume M: "a : set_of M"
     4.5    with assms have a: "prime a" by auto
     4.6    with M have "a ^ count M a dvd (PROD i :# M. i)"
     4.7 -    by (auto simp add: msetprod_multiplicity intro: dvd_setprod)
     4.8 +    by (auto simp add: msetprod_multiplicity)
     4.9    also have "... dvd (PROD i :# N. i)" by (rule assms)
    4.10    also have "... = (PROD i : (set_of N). i ^ (count N i))"
    4.11      by (simp add: msetprod_multiplicity)
    4.12 @@ -309,7 +309,7 @@
    4.13      apply (simp add: set_of_def msetprod_multiplicity)
    4.14      done
    4.15    with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
    4.16 -    by (simp add: Abs_multiset_inverse)
    4.17 +    by simp
    4.18    with S_eq show ?thesis
    4.19      by (simp add: set_of_def multiset_def prime_factors_nat_def multiplicity_nat_def)
    4.20  qed
    4.21 @@ -681,7 +681,7 @@
    4.22    apply (rule dvd_trans) 
    4.23    apply (rule dvd_power [where x = p and n = "multiplicity p n"])
    4.24    apply (subst (asm) prime_factors_altdef_nat, force)
    4.25 -  apply (rule dvd_setprod)
    4.26 +  apply rule
    4.27    apply auto
    4.28    apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
    4.29    done