added strong_setprod_cong[cong] (in analogy with setsum)
authornipkow
Wed Apr 01 16:03:00 2009 +0200 (2009-04-01)
changeset 308373d4832d9f7e4
parent 30829 d64a293f23ba
child 30838 d09a0794d457
added strong_setprod_cong[cong] (in analogy with setsum)
added some lemmas
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/Library/Determinants.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/NumberTheory/Gauss.thy
     1.1 --- a/src/HOL/Divides.thy	Tue Mar 31 15:57:10 2009 -0700
     1.2 +++ b/src/HOL/Divides.thy	Wed Apr 01 16:03:00 2009 +0200
     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,9 @@
    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  declare div_less_dividend [simp]
    1.31  
    1.32  text{*A fact for the mutilated chess board*}
    1.33 @@ -905,13 +912,10 @@
    1.34    done
    1.35  
    1.36  lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
    1.37 -  apply (unfold dvd_def, clarify)
    1.38 -  apply (simp_all (no_asm_use) add: zero_less_mult_iff)
    1.39 -  apply (erule conjE)
    1.40 -  apply (rule le_trans)
    1.41 -   apply (rule_tac [2] le_refl [THEN mult_le_mono])
    1.42 -   apply (erule_tac [2] Suc_leI, simp)
    1.43 -  done
    1.44 +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
    1.45 +
    1.46 +lemma nat_dvd_not_less: "(0::nat) < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
    1.47 +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
    1.48  
    1.49  lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
    1.50    apply (subgoal_tac "m mod n = 0")
    1.51 @@ -1148,9 +1152,4 @@
    1.52    with j show ?thesis by blast
    1.53  qed
    1.54  
    1.55 -lemma nat_dvd_not_less:
    1.56 -  fixes m n :: nat
    1.57 -  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
    1.58 -by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
    1.59 -
    1.60  end
     2.1 --- a/src/HOL/Finite_Set.thy	Tue Mar 31 15:57:10 2009 -0700
     2.2 +++ b/src/HOL/Finite_Set.thy	Wed Apr 01 16:03:00 2009 +0200
     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/Library/Determinants.thy	Tue Mar 31 15:57:10 2009 -0700
     3.2 +++ b/src/HOL/Library/Determinants.thy	Wed Apr 01 16:03:00 2009 +0200
     3.3 @@ -106,7 +106,7 @@
     3.4    moreover
     3.5    {assume fS: "finite S"
     3.6      then have ?thesis
     3.7 -      apply (simp add: setprod_def)
     3.8 +      apply (simp add: setprod_def cong del:strong_setprod_cong)
     3.9        apply (rule ab_semigroup_mult.fold_image_permute)
    3.10        apply (auto simp add: p)
    3.11        apply unfold_locales
    3.12 @@ -115,7 +115,7 @@
    3.13  qed
    3.14  
    3.15  lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"
    3.16 -  by (auto intro: setprod_permute)
    3.17 +  by (blast intro!: setprod_permute)
    3.18  
    3.19  (* ------------------------------------------------------------------------- *)
    3.20  (* Basic determinant properties.                                             *)
     4.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 31 15:57:10 2009 -0700
     4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 01 16:03:00 2009 +0200
     4.3 @@ -1289,10 +1289,6 @@
     4.4        apply auto
     4.5        unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k]
     4.6        apply (clarsimp simp add: natpermute_def nth_append)
     4.7 -      apply (rule_tac f="\<lambda>x. x * a (Suc k) $ (n - foldl op + 0 aa)" in cong[OF refl])
     4.8 -      apply (rule setprod_cong)
     4.9 -      apply simp
    4.10 -      apply simp
    4.11        done
    4.12      finally have "?P m n" .}
    4.13    ultimately show "?P m n " by (cases m, auto)
    4.14 @@ -1321,9 +1317,7 @@
    4.15    {fix n assume m: "m = Suc n"
    4.16      have c: "m = card {0..n}" using m by simp
    4.17     have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
    4.18 -     apply (simp add: m fps_power_nth del: replicate.simps power_Suc)
    4.19 -     apply (rule setprod_cong)
    4.20 -     by (simp_all del: replicate.simps)
    4.21 +     by (simp add: m fps_power_nth del: replicate.simps power_Suc)
    4.22     also have "\<dots> = (a$0) ^ m"
    4.23       unfolding c by (rule setprod_constant, simp)
    4.24     finally have ?thesis .}
     5.1 --- a/src/HOL/NumberTheory/Gauss.thy	Tue Mar 31 15:57:10 2009 -0700
     5.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Wed Apr 01 16:03:00 2009 +0200
     5.3 @@ -290,7 +290,7 @@
     5.4    using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
     5.5  
     5.6  lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
     5.7 -  using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
     5.8 +by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
     5.9  
    5.10  
    5.11  subsection {* Relationships Between Gauss Sets *}
    5.12 @@ -416,8 +416,8 @@
    5.13    then have one:
    5.14      "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
    5.15      apply simp
    5.16 -    apply (insert p_g_0 finite_E)
    5.17 -    by (auto simp add: StandardRes_prod)
    5.18 +    apply (insert p_g_0 finite_E StandardRes_prod)
    5.19 +    by (auto)
    5.20    moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
    5.21      apply clarify
    5.22      apply (insert zcong_id [of p])
    5.23 @@ -435,10 +435,9 @@
    5.24    ultimately have c:
    5.25      "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
    5.26      apply simp
    5.27 -    apply (insert finite_E p_g_0)
    5.28 -    apply (rule setprod_same_function_zcong
    5.29 -      [of E "StandardRes p o (op - p)" uminus p], auto)
    5.30 -    done
    5.31 +    using finite_E p_g_0
    5.32 +      setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
    5.33 +    by auto
    5.34    then have two: "[setprod id F = setprod (uminus) E](mod p)"
    5.35      apply (insert one c)
    5.36      apply (rule zcong_trans [of "setprod id F"
    5.37 @@ -463,11 +462,11 @@
    5.38    "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
    5.39  proof -
    5.40    have "[setprod id A = setprod id F * setprod id D](mod p)"
    5.41 -    by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
    5.42 +    by (auto simp add: prod_D_F_eq_prod_A zmult_commute cong del:setprod_cong)
    5.43    then have "[setprod id A = ((-1)^(card E) * setprod id E) *
    5.44        setprod id D] (mod p)"
    5.45      apply (rule zcong_trans)
    5.46 -    apply (auto simp add: prod_F_zcong zcong_scalar)
    5.47 +    apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod_cong)
    5.48      done
    5.49    then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
    5.50      apply (rule zcong_trans)
    5.51 @@ -476,14 +475,14 @@
    5.52      done
    5.53    then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
    5.54      apply (rule zcong_trans)
    5.55 -    apply (simp add: C_B_zcong_prod zcong_scalar2)
    5.56 +    apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod_cong)
    5.57      done
    5.58    then have "[setprod id A = ((-1)^(card E) *
    5.59      (setprod id ((%x. x * a) ` A)))] (mod p)"
    5.60      by (simp add: B_def)
    5.61    then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
    5.62      (mod p)"
    5.63 -    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
    5.64 +    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
    5.65    moreover have "setprod (%x. x * a) A =
    5.66      setprod (%x. a) A * setprod id A"
    5.67      using finite_A by (induct set: finite) auto
    5.68 @@ -506,7 +505,7 @@
    5.69    then have "[setprod id A * (-1)^(card E) = setprod id A *
    5.70        a^(card A)](mod p)"
    5.71      apply (rule zcong_trans)
    5.72 -    apply (simp add: aux)
    5.73 +    apply (simp add: aux cong del:setprod_cong)
    5.74      done
    5.75    with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
    5.76        p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"