author nipkow Wed, 01 Apr 2009 16:03:00 +0200 changeset 30837 3d4832d9f7e4 parent 30829 d64a293f23ba child 30838 d09a0794d457
 src/HOL/Divides.thy file | annotate | diff | comparison | revisions src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Library/Determinants.thy file | annotate | diff | comparison | revisions src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | comparison | revisions src/HOL/NumberTheory/Gauss.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Divides.thy	Tue Mar 31 15:57:10 2009 -0700
+++ b/src/HOL/Divides.thy	Wed Apr 01 16:03:00 2009 +0200
@@ -238,6 +238,10 @@
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,9 @@
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)
+
declare div_less_dividend [simp]

text{*A fact for the mutilated chess board*}
@@ -905,13 +912,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 +1152,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	Tue Mar 31 15:57:10 2009 -0700
+++ b/src/HOL/Finite_Set.thy	Wed Apr 01 16:03:00 2009 +0200
@@ -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])
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/Library/Determinants.thy	Tue Mar 31 15:57:10 2009 -0700
+++ b/src/HOL/Library/Determinants.thy	Wed Apr 01 16:03:00 2009 +0200
@@ -106,7 +106,7 @@
moreover
{assume fS: "finite S"
then have ?thesis
+      apply (simp add: setprod_def cong del:strong_setprod_cong)
apply (rule ab_semigroup_mult.fold_image_permute)
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	Tue Mar 31 15:57:10 2009 -0700
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 01 16:03:00 2009 +0200
@@ -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	Tue Mar 31 15:57:10 2009 -0700
+++ b/src/HOL/NumberTheory/Gauss.thy	Wed Apr 01 16:03:00 2009 +0200
@@ -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)"
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)