--- a/src/HOL/Divides.thy Wed Apr 01 11:31:24 2009 -0700
+++ b/src/HOL/Divides.thy Wed Apr 01 11:34:21 2009 -0700
@@ -238,6 +238,10 @@
by (simp only: mod_add_eq [symmetric])
qed
+lemma div_add[simp]: "z dvd x \<Longrightarrow> z dvd y
+ \<Longrightarrow> (x + y) div z = x div z + y div z"
+by(cases "z=0", simp, unfold dvd_def, auto simp add: algebra_simps)
+
text {* Multiplication respects modular equivalence. *}
lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
@@ -765,7 +769,7 @@
(* Monotonicity of div in first argument *)
-lemma div_le_mono [rule_format (no_asm)]:
+lemma div_le_mono [rule_format]:
"\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
apply (case_tac "k=0", simp)
apply (induct "n" rule: nat_less_induct, clarify)
@@ -820,6 +824,12 @@
apply (simp_all)
done
+lemma nat_div_eq_0 [simp]: "(n::nat) > 0 ==> ((m div n) = 0) = (m < n)"
+by(auto, subst mod_div_equality [of m n, symmetric], auto)
+
+lemma nat_div_gt_0 [simp]: "(n::nat) > 0 ==> ((m div n) > 0) = (m >= n)"
+by (subst neq0_conv [symmetric], auto)
+
declare div_less_dividend [simp]
text{*A fact for the mutilated chess board*}
@@ -905,13 +915,10 @@
done
lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
- apply (unfold dvd_def, clarify)
- apply (simp_all (no_asm_use) add: zero_less_mult_iff)
- apply (erule conjE)
- apply (rule le_trans)
- apply (rule_tac [2] le_refl [THEN mult_le_mono])
- apply (erule_tac [2] Suc_leI, simp)
- done
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
+lemma nat_dvd_not_less: "(0::nat) < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
apply (subgoal_tac "m mod n = 0")
@@ -1148,9 +1155,4 @@
with j show ?thesis by blast
qed
-lemma nat_dvd_not_less:
- fixes m n :: nat
- shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
-by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
-
end
--- a/src/HOL/Finite_Set.thy Wed Apr 01 11:31:24 2009 -0700
+++ b/src/HOL/Finite_Set.thy Wed Apr 01 11:34:21 2009 -0700
@@ -1084,10 +1084,8 @@
qed
lemma setsum_mono_zero_right:
- assumes fT: "finite T" and ST: "S \<subseteq> T"
- and z: "\<forall>i \<in> T - S. f i = 0"
- shows "setsum f T = setsum f S"
-using setsum_mono_zero_left[OF fT ST z] by simp
+ "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
+by(blast intro!: setsum_mono_zero_left[symmetric])
lemma setsum_mono_zero_cong_left:
assumes fT: "finite T" and ST: "S \<subseteq> T"
@@ -1645,7 +1643,7 @@
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
by(fastsimp simp: setprod_def intro: fold_image_cong)
-lemma strong_setprod_cong:
+lemma strong_setprod_cong[cong]:
"A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
@@ -1662,7 +1660,7 @@
then show ?thesis apply simp
apply (rule setprod_cong)
apply simp
- by (erule eq[symmetric])
+ by (simp add: eq)
qed
lemma setprod_Un_one:
@@ -1694,6 +1692,20 @@
==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
by (subst setprod_Un_Int [symmetric], auto)
+lemma setprod_mono_one_left:
+ assumes fT: "finite T" and ST: "S \<subseteq> T"
+ and z: "\<forall>i \<in> T - S. f i = 1"
+ shows "setprod f S = setprod f T"
+proof-
+ have eq: "T = S \<union> (T - S)" using ST by blast
+ have d: "S \<inter> (T - S) = {}" using ST by blast
+ from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
+ show ?thesis
+ by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
+qed
+
+lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
+
lemma setprod_delta:
assumes fS: "finite S"
shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
--- a/src/HOL/Int.thy Wed Apr 01 11:31:24 2009 -0700
+++ b/src/HOL/Int.thy Wed Apr 01 11:34:21 2009 -0700
@@ -1408,6 +1408,10 @@
"finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
by (rule setprod_nonzero, auto)
+lemma setprod_pos_nat:
+ "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
+using setprod_nonzero_nat by simp
+
lemma setprod_zero_eq_nat:
"finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
by (rule setprod_zero_eq, auto)
--- a/src/HOL/Library/Determinants.thy Wed Apr 01 11:31:24 2009 -0700
+++ b/src/HOL/Library/Determinants.thy Wed Apr 01 11:34:21 2009 -0700
@@ -106,7 +106,7 @@
moreover
{assume fS: "finite S"
then have ?thesis
- apply (simp add: setprod_def)
+ apply (simp add: setprod_def cong del:strong_setprod_cong)
apply (rule ab_semigroup_mult.fold_image_permute)
apply (auto simp add: p)
apply unfold_locales
@@ -115,7 +115,7 @@
qed
lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"
- by (auto intro: setprod_permute)
+ by (blast intro!: setprod_permute)
(* ------------------------------------------------------------------------- *)
(* Basic determinant properties. *)
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Apr 01 11:31:24 2009 -0700
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Apr 01 11:34:21 2009 -0700
@@ -1289,10 +1289,6 @@
apply auto
unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k]
apply (clarsimp simp add: natpermute_def nth_append)
- apply (rule_tac f="\<lambda>x. x * a (Suc k) $ (n - foldl op + 0 aa)" in cong[OF refl])
- apply (rule setprod_cong)
- apply simp
- apply simp
done
finally have "?P m n" .}
ultimately show "?P m n " by (cases m, auto)
@@ -1321,9 +1317,7 @@
{fix n assume m: "m = Suc n"
have c: "m = card {0..n}" using m by simp
have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
- apply (simp add: m fps_power_nth del: replicate.simps power_Suc)
- apply (rule setprod_cong)
- by (simp_all del: replicate.simps)
+ by (simp add: m fps_power_nth del: replicate.simps power_Suc)
also have "\<dots> = (a$0) ^ m"
unfolding c by (rule setprod_constant, simp)
finally have ?thesis .}
--- a/src/HOL/NumberTheory/Gauss.thy Wed Apr 01 11:31:24 2009 -0700
+++ b/src/HOL/NumberTheory/Gauss.thy Wed Apr 01 11:34:21 2009 -0700
@@ -290,7 +290,7 @@
using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
- using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
+by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
subsection {* Relationships Between Gauss Sets *}
@@ -416,8 +416,8 @@
then have one:
"[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
apply simp
- apply (insert p_g_0 finite_E)
- by (auto simp add: StandardRes_prod)
+ apply (insert p_g_0 finite_E StandardRes_prod)
+ by (auto)
moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
apply clarify
apply (insert zcong_id [of p])
@@ -435,10 +435,9 @@
ultimately have c:
"[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
apply simp
- apply (insert finite_E p_g_0)
- apply (rule setprod_same_function_zcong
- [of E "StandardRes p o (op - p)" uminus p], auto)
- done
+ using finite_E p_g_0
+ setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
+ by auto
then have two: "[setprod id F = setprod (uminus) E](mod p)"
apply (insert one c)
apply (rule zcong_trans [of "setprod id F"
@@ -463,11 +462,11 @@
"[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
have "[setprod id A = setprod id F * setprod id D](mod p)"
- by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
+ by (auto simp add: prod_D_F_eq_prod_A zmult_commute cong del:setprod_cong)
then have "[setprod id A = ((-1)^(card E) * setprod id E) *
setprod id D] (mod p)"
apply (rule zcong_trans)
- apply (auto simp add: prod_F_zcong zcong_scalar)
+ apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod_cong)
done
then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
apply (rule zcong_trans)
@@ -476,14 +475,14 @@
done
then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
apply (rule zcong_trans)
- apply (simp add: C_B_zcong_prod zcong_scalar2)
+ apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod_cong)
done
then have "[setprod id A = ((-1)^(card E) *
(setprod id ((%x. x * a) ` A)))] (mod p)"
by (simp add: B_def)
then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
(mod p)"
- by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
+ by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
moreover have "setprod (%x. x * a) A =
setprod (%x. a) A * setprod id A"
using finite_A by (induct set: finite) auto
@@ -506,7 +505,7 @@
then have "[setprod id A * (-1)^(card E) = setprod id A *
a^(card A)](mod p)"
apply (rule zcong_trans)
- apply (simp add: aux)
+ apply (simp add: aux cong del:setprod_cong)
done
with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"