1.1 --- a/src/HOL/Divides.thy Wed Apr 01 11:31:24 2009 -0700
1.2 +++ b/src/HOL/Divides.thy Wed Apr 01 11:34:21 2009 -0700
1.3 @@ -238,6 +238,10 @@
1.4 by (simp only: mod_add_eq [symmetric])
1.5 qed
1.6
1.7 +lemma div_add[simp]: "z dvd x \<Longrightarrow> z dvd y
1.8 + \<Longrightarrow> (x + y) div z = x div z + y div z"
1.9 +by(cases "z=0", simp, unfold dvd_def, auto simp add: algebra_simps)
1.10 +
1.11 text {* Multiplication respects modular equivalence. *}
1.12
1.13 lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
1.14 @@ -765,7 +769,7 @@
1.15
1.16
1.17 (* Monotonicity of div in first argument *)
1.18 -lemma div_le_mono [rule_format (no_asm)]:
1.19 +lemma div_le_mono [rule_format]:
1.20 "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
1.21 apply (case_tac "k=0", simp)
1.22 apply (induct "n" rule: nat_less_induct, clarify)
1.23 @@ -820,6 +824,12 @@
1.24 apply (simp_all)
1.25 done
1.26
1.27 +lemma nat_div_eq_0 [simp]: "(n::nat) > 0 ==> ((m div n) = 0) = (m < n)"
1.28 +by(auto, subst mod_div_equality [of m n, symmetric], auto)
1.29 +
1.30 +lemma nat_div_gt_0 [simp]: "(n::nat) > 0 ==> ((m div n) > 0) = (m >= n)"
1.31 +by (subst neq0_conv [symmetric], auto)
1.32 +
1.33 declare div_less_dividend [simp]
1.34
1.35 text{*A fact for the mutilated chess board*}
1.36 @@ -905,13 +915,10 @@
1.37 done
1.38
1.39 lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
1.40 - apply (unfold dvd_def, clarify)
1.41 - apply (simp_all (no_asm_use) add: zero_less_mult_iff)
1.42 - apply (erule conjE)
1.43 - apply (rule le_trans)
1.44 - apply (rule_tac [2] le_refl [THEN mult_le_mono])
1.45 - apply (erule_tac [2] Suc_leI, simp)
1.46 - done
1.47 +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
1.48 +
1.49 +lemma nat_dvd_not_less: "(0::nat) < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
1.50 +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
1.51
1.52 lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
1.53 apply (subgoal_tac "m mod n = 0")
1.54 @@ -1148,9 +1155,4 @@
1.55 with j show ?thesis by blast
1.56 qed
1.57
1.58 -lemma nat_dvd_not_less:
1.59 - fixes m n :: nat
1.60 - shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
1.61 -by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
1.62 -
1.63 end
2.1 --- a/src/HOL/Finite_Set.thy Wed Apr 01 11:31:24 2009 -0700
2.2 +++ b/src/HOL/Finite_Set.thy Wed Apr 01 11:34:21 2009 -0700
2.3 @@ -1084,10 +1084,8 @@
2.4 qed
2.5
2.6 lemma setsum_mono_zero_right:
2.7 - assumes fT: "finite T" and ST: "S \<subseteq> T"
2.8 - and z: "\<forall>i \<in> T - S. f i = 0"
2.9 - shows "setsum f T = setsum f S"
2.10 -using setsum_mono_zero_left[OF fT ST z] by simp
2.11 + "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
2.12 +by(blast intro!: setsum_mono_zero_left[symmetric])
2.13
2.14 lemma setsum_mono_zero_cong_left:
2.15 assumes fT: "finite T" and ST: "S \<subseteq> T"
2.16 @@ -1645,7 +1643,7 @@
2.17 "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
2.18 by(fastsimp simp: setprod_def intro: fold_image_cong)
2.19
2.20 -lemma strong_setprod_cong:
2.21 +lemma strong_setprod_cong[cong]:
2.22 "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
2.23 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
2.24
2.25 @@ -1662,7 +1660,7 @@
2.26 then show ?thesis apply simp
2.27 apply (rule setprod_cong)
2.28 apply simp
2.29 - by (erule eq[symmetric])
2.30 + by (simp add: eq)
2.31 qed
2.32
2.33 lemma setprod_Un_one:
2.34 @@ -1694,6 +1692,20 @@
2.35 ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
2.36 by (subst setprod_Un_Int [symmetric], auto)
2.37
2.38 +lemma setprod_mono_one_left:
2.39 + assumes fT: "finite T" and ST: "S \<subseteq> T"
2.40 + and z: "\<forall>i \<in> T - S. f i = 1"
2.41 + shows "setprod f S = setprod f T"
2.42 +proof-
2.43 + have eq: "T = S \<union> (T - S)" using ST by blast
2.44 + have d: "S \<inter> (T - S) = {}" using ST by blast
2.45 + from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
2.46 + show ?thesis
2.47 + by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
2.48 +qed
2.49 +
2.50 +lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
2.51 +
2.52 lemma setprod_delta:
2.53 assumes fS: "finite S"
2.54 shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
3.1 --- a/src/HOL/Int.thy Wed Apr 01 11:31:24 2009 -0700
3.2 +++ b/src/HOL/Int.thy Wed Apr 01 11:34:21 2009 -0700
3.3 @@ -1408,6 +1408,10 @@
3.4 "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
3.5 by (rule setprod_nonzero, auto)
3.6
3.7 +lemma setprod_pos_nat:
3.8 + "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
3.9 +using setprod_nonzero_nat by simp
3.10 +
3.11 lemma setprod_zero_eq_nat:
3.12 "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
3.13 by (rule setprod_zero_eq, auto)
4.1 --- a/src/HOL/Library/Determinants.thy Wed Apr 01 11:31:24 2009 -0700
4.2 +++ b/src/HOL/Library/Determinants.thy Wed Apr 01 11:34:21 2009 -0700
4.3 @@ -106,7 +106,7 @@
4.4 moreover
4.5 {assume fS: "finite S"
4.6 then have ?thesis
4.7 - apply (simp add: setprod_def)
4.8 + apply (simp add: setprod_def cong del:strong_setprod_cong)
4.9 apply (rule ab_semigroup_mult.fold_image_permute)
4.10 apply (auto simp add: p)
4.11 apply unfold_locales
4.12 @@ -115,7 +115,7 @@
4.13 qed
4.14
4.15 lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"
4.16 - by (auto intro: setprod_permute)
4.17 + by (blast intro!: setprod_permute)
4.18
4.19 (* ------------------------------------------------------------------------- *)
4.20 (* Basic determinant properties. *)
5.1 --- a/src/HOL/Library/Formal_Power_Series.thy Wed Apr 01 11:31:24 2009 -0700
5.2 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Apr 01 11:34:21 2009 -0700
5.3 @@ -1289,10 +1289,6 @@
5.4 apply auto
5.5 unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k]
5.6 apply (clarsimp simp add: natpermute_def nth_append)
5.7 - apply (rule_tac f="\<lambda>x. x * a (Suc k) $ (n - foldl op + 0 aa)" in cong[OF refl])
5.8 - apply (rule setprod_cong)
5.9 - apply simp
5.10 - apply simp
5.11 done
5.12 finally have "?P m n" .}
5.13 ultimately show "?P m n " by (cases m, auto)
5.14 @@ -1321,9 +1317,7 @@
5.15 {fix n assume m: "m = Suc n"
5.16 have c: "m = card {0..n}" using m by simp
5.17 have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
5.18 - apply (simp add: m fps_power_nth del: replicate.simps power_Suc)
5.19 - apply (rule setprod_cong)
5.20 - by (simp_all del: replicate.simps)
5.21 + by (simp add: m fps_power_nth del: replicate.simps power_Suc)
5.22 also have "\<dots> = (a$0) ^ m"
5.23 unfolding c by (rule setprod_constant, simp)
5.24 finally have ?thesis .}
6.1 --- a/src/HOL/NumberTheory/Gauss.thy Wed Apr 01 11:31:24 2009 -0700
6.2 +++ b/src/HOL/NumberTheory/Gauss.thy Wed Apr 01 11:34:21 2009 -0700
6.3 @@ -290,7 +290,7 @@
6.4 using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
6.5
6.6 lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
6.7 - using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
6.8 +by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
6.9
6.10
6.11 subsection {* Relationships Between Gauss Sets *}
6.12 @@ -416,8 +416,8 @@
6.13 then have one:
6.14 "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
6.15 apply simp
6.16 - apply (insert p_g_0 finite_E)
6.17 - by (auto simp add: StandardRes_prod)
6.18 + apply (insert p_g_0 finite_E StandardRes_prod)
6.19 + by (auto)
6.20 moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
6.21 apply clarify
6.22 apply (insert zcong_id [of p])
6.23 @@ -435,10 +435,9 @@
6.24 ultimately have c:
6.25 "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
6.26 apply simp
6.27 - apply (insert finite_E p_g_0)
6.28 - apply (rule setprod_same_function_zcong
6.29 - [of E "StandardRes p o (op - p)" uminus p], auto)
6.30 - done
6.31 + using finite_E p_g_0
6.32 + setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
6.33 + by auto
6.34 then have two: "[setprod id F = setprod (uminus) E](mod p)"
6.35 apply (insert one c)
6.36 apply (rule zcong_trans [of "setprod id F"
6.37 @@ -463,11 +462,11 @@
6.38 "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
6.39 proof -
6.40 have "[setprod id A = setprod id F * setprod id D](mod p)"
6.41 - by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
6.42 + by (auto simp add: prod_D_F_eq_prod_A zmult_commute cong del:setprod_cong)
6.43 then have "[setprod id A = ((-1)^(card E) * setprod id E) *
6.44 setprod id D] (mod p)"
6.45 apply (rule zcong_trans)
6.46 - apply (auto simp add: prod_F_zcong zcong_scalar)
6.47 + apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod_cong)
6.48 done
6.49 then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
6.50 apply (rule zcong_trans)
6.51 @@ -476,14 +475,14 @@
6.52 done
6.53 then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
6.54 apply (rule zcong_trans)
6.55 - apply (simp add: C_B_zcong_prod zcong_scalar2)
6.56 + apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod_cong)
6.57 done
6.58 then have "[setprod id A = ((-1)^(card E) *
6.59 (setprod id ((%x. x * a) ` A)))] (mod p)"
6.60 by (simp add: B_def)
6.61 then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
6.62 (mod p)"
6.63 - by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
6.64 + by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
6.65 moreover have "setprod (%x. x * a) A =
6.66 setprod (%x. a) A * setprod id A"
6.67 using finite_A by (induct set: finite) auto
6.68 @@ -506,7 +505,7 @@
6.69 then have "[setprod id A * (-1)^(card E) = setprod id A *
6.70 a^(card A)](mod p)"
6.71 apply (rule zcong_trans)
6.72 - apply (simp add: aux)
6.73 + apply (simp add: aux cong del:setprod_cong)
6.74 done
6.75 with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
6.76 p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"