# HG changeset patch
# User nipkow
# Date 1238594598 -7200
# Node ID d09a0794d4571c8b6eee016a3666e120e811e466
# Parent  1344132160bb303faae60525e2d86bd8e0505990# Parent  3d4832d9f7e4cdea055a5fd365cc3b5257e5c236
merged

diff -r 1344132160bb -r d09a0794d457 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Apr 01 15:16:09 2009 +0200
+++ b/src/HOL/Divides.thy	Wed Apr 01 16:03:18 2009 +0200
@@ -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,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
diff -r 1344132160bb -r d09a0794d457 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Apr 01 15:16:09 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Apr 01 16:03:18 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])
+      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)"
diff -r 1344132160bb -r d09a0794d457 src/HOL/Library/Determinants.thy
--- a/src/HOL/Library/Determinants.thy	Wed Apr 01 15:16:09 2009 +0200
+++ b/src/HOL/Library/Determinants.thy	Wed Apr 01 16:03:18 2009 +0200
@@ -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.                                             *)
diff -r 1344132160bb -r d09a0794d457 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 01 15:16:09 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 01 16:03:18 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 .}
diff -r 1344132160bb -r d09a0794d457 src/HOL/NumberTheory/Gauss.thy
--- a/src/HOL/NumberTheory/Gauss.thy	Wed Apr 01 15:16:09 2009 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy	Wed Apr 01 16:03:18 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)"
     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)"