generalized lemmas (particularly concerning dvd) as far as appropriate
authorhaftmann
Mon Nov 17 14:55:33 2014 +0100 (2014-11-17)
changeset 59009348561aa3869
parent 59008 f61482b0f240
child 59010 ec2b4270a502
generalized lemmas (particularly concerning dvd) as far as appropriate
src/HOL/Divides.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Power.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Divides.thy	Mon Nov 17 14:55:32 2014 +0100
     1.2 +++ b/src/HOL/Divides.thy	Mon Nov 17 14:55:33 2014 +0100
     1.3 @@ -28,6 +28,14 @@
     1.4  
     1.5  subclass semiring_no_zero_divisors ..
     1.6  
     1.7 +lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
     1.8 +  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
     1.9 +  by (induct n) (simp_all add: no_zero_divisors)
    1.10 +
    1.11 +lemma semiring_div_power_eq_0_iff: -- \<open>FIXME cf. @{text power_eq_0_iff}, @{text power_eq_0_nat_iff}\<close>
    1.12 +  "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
    1.13 +  using power_not_zero [of a n] by (auto simp add: zero_power)
    1.14 +
    1.15  text {* @{const div} and @{const mod} *}
    1.16  
    1.17  lemma mod_div_equality2: "b * (a div b) + a mod b = a"
    1.18 @@ -390,6 +398,20 @@
    1.19  lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
    1.20    by (fact mod_mult_mult1 [symmetric])
    1.21  
    1.22 +lemma dvd_times_left_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
    1.23 +  assumes "c \<noteq> 0"
    1.24 +  shows "c * a dvd c * b \<longleftrightarrow> a dvd b"
    1.25 +proof -
    1.26 +  have "(c * b) mod (c * a) = 0 \<longleftrightarrow> b mod a = 0" (is "?P \<longleftrightarrow> ?Q")
    1.27 +    using assms by (simp add: mod_mult_mult1)
    1.28 +  then show ?thesis by (simp add: mod_eq_0_iff_dvd)
    1.29 +qed
    1.30 +
    1.31 +lemma dvd_times_right_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
    1.32 +  assumes "c \<noteq> 0"
    1.33 +  shows "a * c dvd b * c \<longleftrightarrow> a dvd b"
    1.34 +  using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps)
    1.35 +
    1.36  lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
    1.37    unfolding dvd_def by (auto simp add: mod_mult_mult1)
    1.38  
    1.39 @@ -643,20 +665,6 @@
    1.40    "a - 0 = a"
    1.41    by (rule diff_invert_add1 [symmetric]) simp
    1.42  
    1.43 -lemma dvd_times_left_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
    1.44 -  assumes "c \<noteq> 0"
    1.45 -  shows "c * a dvd c * b \<longleftrightarrow> a dvd b"
    1.46 -proof -
    1.47 -  have "(c * b) mod (c * a) = 0 \<longleftrightarrow> b mod a = 0" (is "?P \<longleftrightarrow> ?Q")
    1.48 -    using assms by (simp add: mod_mult_mult1)
    1.49 -  then show ?thesis by (simp add: mod_eq_0_iff_dvd)
    1.50 -qed
    1.51 -
    1.52 -lemma dvd_times_right_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
    1.53 -  assumes "c \<noteq> 0"
    1.54 -  shows "a * c dvd b * c \<longleftrightarrow> a dvd b"
    1.55 -  using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps)
    1.56 -
    1.57  subclass semiring_div_parity
    1.58  proof
    1.59    fix a
     2.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:32 2014 +0100
     2.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:33 2014 +0100
     2.3 @@ -6,33 +6,6 @@
     2.4  imports Complex_Main
     2.5  begin
     2.6  
     2.7 -lemma finite_int_set_iff_bounded_le:
     2.8 -  "finite (N::int set) = (\<exists>m\<ge>0. \<forall>n\<in>N. abs n \<le> m)"
     2.9 -proof
    2.10 -  assume "finite (N::int set)"
    2.11 -  hence "finite (nat ` abs ` N)" by (intro finite_imageI)
    2.12 -  hence "\<exists>m. \<forall>n\<in>nat`abs`N. n \<le> m" by (simp add: finite_nat_set_iff_bounded_le)
    2.13 -  then obtain m :: nat where "\<forall>n\<in>N. nat (abs n) \<le> nat (int m)" by auto
    2.14 -  then show "\<exists>m\<ge>0. \<forall>n\<in>N. abs n \<le> m" by (intro exI[of _ "int m"]) (auto simp: nat_le_eq_zle)
    2.15 -next
    2.16 -  assume "\<exists>m\<ge>0. \<forall>n\<in>N. abs n \<le> m"
    2.17 -  then obtain m where "m \<ge> 0" and "\<forall>n\<in>N. abs n \<le> m" by blast
    2.18 -  hence "\<forall>n\<in>N. nat (abs n) \<le> nat m" by (auto simp: nat_le_eq_zle)
    2.19 -  hence "\<forall>n\<in>nat`abs`N. n \<le> nat m" by (auto simp: nat_le_eq_zle)
    2.20 -  hence A: "finite ((nat \<circ> abs)`N)" unfolding o_def 
    2.21 -      by (subst finite_nat_set_iff_bounded_le) blast
    2.22 -  {
    2.23 -    assume "\<not>finite N"
    2.24 -    from pigeonhole_infinite[OF this A] obtain x 
    2.25 -       where "x \<in> N" and B: "~finite {a\<in>N. nat (abs a) = nat (abs x)}" 
    2.26 -       unfolding o_def by blast
    2.27 -    have "{a\<in>N. nat (abs a) = nat (abs x)} \<subseteq> {x, -x}" by auto
    2.28 -    hence "finite {a\<in>N. nat (abs a) = nat (abs x)}" by (rule finite_subset) simp
    2.29 -    with B have False by contradiction
    2.30 -  }
    2.31 -  then show "finite N" by blast
    2.32 -qed
    2.33 -
    2.34  context semiring_div
    2.35  begin
    2.36  
    2.37 @@ -46,32 +19,6 @@
    2.38    finally show "setprod f A = f x * setprod f (A - {x})" .
    2.39  qed
    2.40  
    2.41 -lemma dvd_mult_cancel_left:
    2.42 -  assumes "a \<noteq> 0" and "a * b dvd a * c"
    2.43 -  shows "b dvd c"
    2.44 -proof-
    2.45 -  from assms(2) obtain k where "a * c = a * b * k" unfolding dvd_def by blast
    2.46 -  hence "c * a = b * k * a" by (simp add: ac_simps)
    2.47 -  hence "c * (a div a) = b * k * (a div a)" by (simp add: div_mult_swap)
    2.48 -  also from `a \<noteq> 0` have "a div a = 1" by simp
    2.49 -  finally show ?thesis by simp
    2.50 -qed
    2.51 -
    2.52 -lemma dvd_mult_cancel_right:
    2.53 -  "a \<noteq> 0 \<Longrightarrow> b * a dvd c * a \<Longrightarrow> b dvd c"
    2.54 -  by (subst (asm) (1 2) ac_simps, rule dvd_mult_cancel_left)
    2.55 -
    2.56 -lemma nonzero_pow_nonzero:
    2.57 -  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
    2.58 -  by (induct n) (simp_all add: no_zero_divisors)
    2.59 -
    2.60 -lemma zero_pow_zero: "n \<noteq> 0 \<Longrightarrow> 0 ^ n = 0"
    2.61 -  by (cases n, simp_all)
    2.62 -
    2.63 -lemma pow_zero_iff:
    2.64 -  "n \<noteq> 0 \<Longrightarrow> a^n = 0 \<longleftrightarrow> a = 0"
    2.65 -  using nonzero_pow_nonzero zero_pow_zero by auto
    2.66 -
    2.67  end
    2.68  
    2.69  context semiring_div
    2.70 @@ -260,9 +207,9 @@
    2.71      hence [simp]: "x dvd y" "y dvd x" using `associated x y`
    2.72          unfolding associated_def by simp_all
    2.73      hence "1 = x div y * (y div x)"
    2.74 -      by (simp add: div_mult_swap dvd_div_mult_self)
    2.75 +      by (simp add: div_mult_swap)
    2.76      hence "is_unit (x div y)" unfolding is_unit_def by (rule dvdI)
    2.77 -    moreover have "x = (x div y) * y" by (simp add: dvd_div_mult_self)
    2.78 +    moreover have "x = (x div y) * y" by simp
    2.79      ultimately show ?thesis by blast
    2.80    qed
    2.81  next
    2.82 @@ -364,7 +311,7 @@
    2.83    have "?nf (x div ?nf x) * ?nf (?nf x) = ?nf (x div ?nf x * ?nf x)" 
    2.84      by (simp add: normalisation_factor_mult)
    2.85    also have "x div ?nf x * ?nf x = x" using `x \<noteq> 0`
    2.86 -    by (simp add: dvd_div_mult_self)
    2.87 +    by simp
    2.88    also have "?nf (?nf x) = ?nf x" using `x \<noteq> 0` 
    2.89      normalisation_factor_is_unit normalisation_factor_unit by simp
    2.90    finally show ?thesis using `x \<noteq> 0` and `?nf x \<noteq> 0` 
    2.91 @@ -653,7 +600,7 @@
    2.92    also have "... = k * gcd x y div ?nf k"
    2.93      by (metis dvd_div_mult dvd_eq_mod_eq_0 mod_0 normalisation_factor_dvd)
    2.94    finally show ?thesis
    2.95 -    by (simp add: ac_simps dvd_mult_div_cancel)
    2.96 +    by simp
    2.97  qed
    2.98  
    2.99  lemma euclidean_size_gcd_le1 [simp]:
   2.100 @@ -711,7 +658,7 @@
   2.101    apply (simp add: ac_simps)
   2.102    apply (rule gcd_dvd2)
   2.103    apply (rule gcd_greatest, erule (1) gcd_greatest, assumption)
   2.104 -  apply (simp add: gcd_zero)
   2.105 +  apply simp
   2.106    done
   2.107  
   2.108  lemma gcd_left_idem: "gcd p (gcd p q) = gcd p q"
   2.109 @@ -719,7 +666,7 @@
   2.110    apply simp
   2.111    apply (rule dvd_trans, rule gcd_dvd2, rule gcd_dvd2)
   2.112    apply (rule gcd_greatest, assumption, erule gcd_greatest, assumption)
   2.113 -  apply (simp add: gcd_zero)
   2.114 +  apply simp
   2.115    done
   2.116  
   2.117  lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
   2.118 @@ -754,7 +701,7 @@
   2.119    have "gcd c d dvd d" by simp
   2.120    with A show "gcd a b dvd d" by (rule dvd_trans)
   2.121    show "normalisation_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)"
   2.122 -    by (simp add: gcd_zero)
   2.123 +    by simp
   2.124    fix l assume "l dvd c" and "l dvd d"
   2.125    hence "l dvd gcd c d" by (rule gcd_greatest)
   2.126    from this and B show "l dvd gcd a b" by (rule dvd_trans)
   2.127 @@ -786,10 +733,10 @@
   2.128    moreover from `?lhs` have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left) 
   2.129    hence "b dvd a" by (simp add: coprime_dvd_mult_iff)
   2.130    moreover from `?lhs` have "c dvd d * b" 
   2.131 -    unfolding associated_def by (metis dvd_mult_right ac_simps)
   2.132 +    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
   2.133    hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute)
   2.134    moreover from `?lhs` have "d dvd c * a"
   2.135 -    unfolding associated_def by (metis dvd_mult_right ac_simps)
   2.136 +    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
   2.137    hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute)
   2.138    ultimately show ?rhs unfolding associated_def by simp
   2.139  qed
   2.140 @@ -819,17 +766,18 @@
   2.141  proof (rule coprimeI)
   2.142    fix l assume "l dvd a'" "l dvd b'"
   2.143    then obtain s t where "a' = l * s" "b' = l * t" unfolding dvd_def by blast
   2.144 -  moreover have "a = a' * d" "b = b' * d" by (simp_all add: dvd_div_mult_self)
   2.145 +  moreover have "a = a' * d" "b = b' * d" by simp_all
   2.146    ultimately have "a = (l * d) * s" "b = (l * d) * t"
   2.147 -    by (metis ac_simps)+
   2.148 +    by (simp_all only: ac_simps)
   2.149    hence "l*d dvd a" and "l*d dvd b" by (simp_all only: dvd_triv_left)
   2.150    hence "l*d dvd d" by (simp add: gcd_greatest)
   2.151 -  then obtain u where "u * l * d = d" unfolding dvd_def
   2.152 -    by (metis ac_simps mult_assoc)
   2.153 -  moreover from nz have "d \<noteq> 0" by (simp add: gcd_zero)
   2.154 -  ultimately have "u * l = 1" 
   2.155 -    by (metis div_mult_self1_is_id div_self ac_simps)
   2.156 -  then show "l dvd 1" by force
   2.157 +  then obtain u where "d = l * d * u" ..
   2.158 +  then have "d * (l * u) = d" by (simp add: ac_simps)
   2.159 +  moreover from nz have "d \<noteq> 0" by simp
   2.160 +  with div_mult_self1_is_id have "d * (l * u) div d = l * u" . 
   2.161 +  ultimately have "1 = l * u"
   2.162 +    using `d \<noteq> 0` by simp
   2.163 +  then show "l dvd 1" ..
   2.164  qed
   2.165  
   2.166  lemma coprime_mult: 
   2.167 @@ -866,7 +814,7 @@
   2.168    assumes z: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b"
   2.169    shows "gcd a' b' = 1"
   2.170  proof -
   2.171 -  from z have "a \<noteq> 0 \<or> b \<noteq> 0" by (simp add: gcd_zero)
   2.172 +  from z have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
   2.173    with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
   2.174    also from assms have "a div gcd a b = a'" by (metis div_mult_self2_is_id)+
   2.175    also from assms have "b div gcd a b = b'" by (metis div_mult_self2_is_id)+
   2.176 @@ -886,7 +834,7 @@
   2.177    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
   2.178    apply (rule_tac x = "a div gcd a b" in exI)
   2.179    apply (rule_tac x = "b div gcd a b" in exI)
   2.180 -  apply (insert nz, auto simp add: dvd_div_mult gcd_0_left  gcd_zero intro: div_gcd_coprime)
   2.181 +  apply (insert nz, auto intro: div_gcd_coprime)
   2.182    done
   2.183  
   2.184  lemma coprime_exp:
   2.185 @@ -934,7 +882,7 @@
   2.186    shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   2.187  proof (cases "gcd a b = 0")
   2.188    assume "gcd a b = 0"
   2.189 -  hence "a = 0 \<and> b = 0" by (simp add: gcd_zero)
   2.190 +  hence "a = 0 \<and> b = 0" by simp
   2.191    hence "a = 0 * c \<and> 0 dvd b \<and> c dvd c" by simp
   2.192    then show ?thesis by blast
   2.193  next
   2.194 @@ -947,7 +895,7 @@
   2.195    with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   2.196    from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp
   2.197    hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac)
   2.198 -  with `?d \<noteq> 0` have "a' dvd b' * c" by (rule dvd_mult_cancel_left)
   2.199 +  with `?d \<noteq> 0` have "a' dvd b' * c" by simp
   2.200    with coprime_dvd_mult[OF ab'(3)] 
   2.201      have "a' dvd c" by (subst (asm) ac_simps, blast)
   2.202    with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac)
   2.203 @@ -959,12 +907,12 @@
   2.204    shows "a dvd b"
   2.205  proof (cases "gcd a b = 0")
   2.206    assume "gcd a b = 0"
   2.207 -  then show ?thesis by (simp add: gcd_zero)
   2.208 +  then show ?thesis by simp
   2.209  next
   2.210    let ?d = "gcd a b"
   2.211    assume "?d \<noteq> 0"
   2.212    from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   2.213 -  from `?d \<noteq> 0` have zn: "?d ^ n \<noteq> 0" by (rule nonzero_pow_nonzero)
   2.214 +  from `?d \<noteq> 0` have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
   2.215    from gcd_coprime_exists[OF `?d \<noteq> 0`]
   2.216      obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
   2.217      by blast
   2.218 @@ -972,7 +920,7 @@
   2.219      by (simp add: ab'(1,2)[symmetric])
   2.220    hence "?d^n * a'^n dvd ?d^n * b'^n"
   2.221      by (simp only: power_mult_distrib ac_simps)
   2.222 -  with zn have "a'^n dvd b'^n" by (rule dvd_mult_cancel_left)
   2.223 +  with zn have "a'^n dvd b'^n" by simp
   2.224    hence "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
   2.225    hence "a' dvd b'^m * b'" by (simp add: m ac_simps)
   2.226    with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
   2.227 @@ -1022,8 +970,18 @@
   2.228  qed
   2.229  
   2.230  lemma invertible_coprime:
   2.231 -  "x * y mod m = 1 \<Longrightarrow> gcd x m = 1"
   2.232 -  by (metis coprime_lmult gcd_1 ac_simps gcd_red)
   2.233 +  assumes "x * y mod m = 1"
   2.234 +  shows "coprime x m"
   2.235 +proof -
   2.236 +  from assms have "coprime m (x * y mod m)"
   2.237 +    by simp
   2.238 +  then have "coprime m (x * y)"
   2.239 +    by simp
   2.240 +  then have "coprime m x"
   2.241 +    by (rule coprime_lmult)
   2.242 +  then show ?thesis
   2.243 +    by (simp add: ac_simps)
   2.244 +qed
   2.245  
   2.246  lemma lcm_gcd:
   2.247    "lcm a b = a * b div (gcd a b * normalisation_factor (a*b))"
   2.248 @@ -1108,7 +1066,7 @@
   2.249    {
   2.250      assume "a \<noteq> 0" "b \<noteq> 0"
   2.251      hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
   2.252 -    moreover from `a \<noteq> 0` and `b \<noteq> 0` have "gcd a b \<noteq> 0" by (simp add: gcd_zero)
   2.253 +    moreover from `a \<noteq> 0` and `b \<noteq> 0` have "gcd a b \<noteq> 0" by simp
   2.254      ultimately have "lcm a b \<noteq> 0" using lcm_gcd_prod[of a b] by (intro notI, simp)
   2.255    } moreover {
   2.256      assume "a = 0 \<or> b = 0"
   2.257 @@ -1123,7 +1081,7 @@
   2.258    assumes "lcm a b \<noteq> 0"
   2.259    shows "gcd a b = a * b div (lcm a b * normalisation_factor (a * b))"
   2.260  proof-
   2.261 -  from assms have "gcd a b \<noteq> 0" by (simp add: gcd_zero lcm_zero)
   2.262 +  from assms have "gcd a b \<noteq> 0" by (simp add: lcm_zero)
   2.263    let ?c = "normalisation_factor (a*b)"
   2.264    from `lcm a b \<noteq> 0` have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
   2.265    hence "is_unit ?c" by simp
   2.266 @@ -1383,7 +1341,7 @@
   2.267      {
   2.268        fix l' assume "\<forall>x\<in>A. x dvd l'"
   2.269        with `\<forall>x\<in>A. x dvd l` have "\<forall>x\<in>A. x dvd gcd l l'" by (auto intro: gcd_greatest)
   2.270 -      moreover from `l \<noteq> 0` have "gcd l l' \<noteq> 0" by (simp add: gcd_zero)
   2.271 +      moreover from `l \<noteq> 0` have "gcd l l' \<noteq> 0" by simp
   2.272        ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
   2.273          by (intro exI[of _ "gcd l l'"], auto)
   2.274        hence "euclidean_size (gcd l l') \<ge> n" by (subst n_def) (rule Least_le)
   2.275 @@ -1585,7 +1543,7 @@
   2.276    then show "g' dvd Gcd A" by (simp add: Gcd_Lcm)
   2.277  next
   2.278    show "normalisation_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   2.279 -    by (simp add: Gcd_Lcm normalisation_factor_Lcm)
   2.280 +    by (simp add: Gcd_Lcm)
   2.281  qed
   2.282  
   2.283  lemma GcdI:
   2.284 @@ -1619,7 +1577,7 @@
   2.285    fix l assume "l dvd a" and "l dvd Gcd A"
   2.286    hence "\<forall>x\<in>A. l dvd x" by (blast intro: dvd_trans Gcd_dvd)
   2.287    with `l dvd a` show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
   2.288 -qed (auto intro: Gcd_dvd dvd_Gcd simp: normalisation_factor_Gcd)
   2.289 +qed auto
   2.290  
   2.291  lemma Gcd_finite:
   2.292    assumes "finite A"
   2.293 @@ -1653,11 +1611,11 @@
   2.294  
   2.295  lemma gcd_neg1 [simp]:
   2.296    "gcd (-x) y = gcd x y"
   2.297 -  by (rule sym, rule gcdI, simp_all add: gcd_greatest gcd_zero)
   2.298 +  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
   2.299  
   2.300  lemma gcd_neg2 [simp]:
   2.301    "gcd x (-y) = gcd x y"
   2.302 -  by (rule sym, rule gcdI, simp_all add: gcd_greatest gcd_zero)
   2.303 +  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
   2.304  
   2.305  lemma gcd_neg_numeral_1 [simp]:
   2.306    "gcd (- numeral n) x = gcd (numeral n) x"
     3.1 --- a/src/HOL/Power.thy	Mon Nov 17 14:55:32 2014 +0100
     3.2 +++ b/src/HOL/Power.thy	Mon Nov 17 14:55:33 2014 +0100
     3.3 @@ -149,7 +149,12 @@
     3.4    "of_nat (m ^ n) = of_nat m ^ n"
     3.5    by (induct n) (simp_all add: of_nat_mult)
     3.6  
     3.7 -lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
     3.8 +lemma zero_power:
     3.9 +  "0 < n \<Longrightarrow> 0 ^ n = 0"
    3.10 +  by (cases n) simp_all
    3.11 +
    3.12 +lemma power_zero_numeral [simp]:
    3.13 +  "0 ^ numeral k = 0"
    3.14    by (simp add: numeral_eq_Suc)
    3.15  
    3.16  lemma zero_power2: "0\<^sup>2 = 0" (* delete? *)
     4.1 --- a/src/HOL/Rings.thy	Mon Nov 17 14:55:32 2014 +0100
     4.2 +++ b/src/HOL/Rings.thy	Mon Nov 17 14:55:33 2014 +0100
     4.3 @@ -134,13 +134,13 @@
     4.4  
     4.5  end
     4.6  
     4.7 -class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd
     4.8 -  (*previously almost_semiring*)
     4.9 +context comm_monoid_mult
    4.10  begin
    4.11  
    4.12 -subclass semiring_1 ..
    4.13 +subclass dvd .
    4.14  
    4.15 -lemma dvd_refl[simp]: "a dvd a"
    4.16 +lemma dvd_refl [simp]:
    4.17 +  "a dvd a"
    4.18  proof
    4.19    show "a = a * 1" by simp
    4.20  qed
    4.21 @@ -155,30 +155,25 @@
    4.22    then show ?thesis ..
    4.23  qed
    4.24  
    4.25 -lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
    4.26 -by (auto intro: dvd_refl elim!: dvdE)
    4.27 +lemma one_dvd [simp]:
    4.28 +  "1 dvd a"
    4.29 +  by (auto intro!: dvdI)
    4.30  
    4.31 -lemma dvd_0_right [iff]: "a dvd 0"
    4.32 -proof
    4.33 -  show "0 = a * 0" by simp
    4.34 -qed
    4.35 -
    4.36 -lemma one_dvd [simp]: "1 dvd a"
    4.37 -by (auto intro!: dvdI)
    4.38 +lemma dvd_mult [simp]:
    4.39 +  "a dvd c \<Longrightarrow> a dvd (b * c)"
    4.40 +  by (auto intro!: mult.left_commute dvdI elim!: dvdE)
    4.41  
    4.42 -lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
    4.43 -by (auto intro!: mult.left_commute dvdI elim!: dvdE)
    4.44 +lemma dvd_mult2 [simp]:
    4.45 +  "a dvd b \<Longrightarrow> a dvd (b * c)"
    4.46 +  using dvd_mult [of a b c] by (simp add: ac_simps) 
    4.47  
    4.48 -lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
    4.49 -  apply (subst mult.commute)
    4.50 -  apply (erule dvd_mult)
    4.51 -  done
    4.52 +lemma dvd_triv_right [simp]:
    4.53 +  "a dvd b * a"
    4.54 +  by (rule dvd_mult) (rule dvd_refl)
    4.55  
    4.56 -lemma dvd_triv_right [simp]: "a dvd b * a"
    4.57 -by (rule dvd_mult) (rule dvd_refl)
    4.58 -
    4.59 -lemma dvd_triv_left [simp]: "a dvd a * b"
    4.60 -by (rule dvd_mult2) (rule dvd_refl)
    4.61 +lemma dvd_triv_left [simp]:
    4.62 +  "a dvd a * b"
    4.63 +  by (rule dvd_mult2) (rule dvd_refl)
    4.64  
    4.65  lemma mult_dvd_mono:
    4.66    assumes "a dvd b"
    4.67 @@ -191,17 +186,39 @@
    4.68    then show ?thesis ..
    4.69  qed
    4.70  
    4.71 -lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
    4.72 -by (simp add: dvd_def mult.assoc, blast)
    4.73 +lemma dvd_mult_left:
    4.74 +  "a * b dvd c \<Longrightarrow> a dvd c"
    4.75 +  by (simp add: dvd_def mult.assoc) blast
    4.76  
    4.77 -lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
    4.78 -  unfolding mult.commute [of a] by (rule dvd_mult_left)
    4.79 +lemma dvd_mult_right:
    4.80 +  "a * b dvd c \<Longrightarrow> b dvd c"
    4.81 +  using dvd_mult_left [of b a c] by (simp add: ac_simps)
    4.82 +  
    4.83 +end
    4.84 +
    4.85 +class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
    4.86 +  (*previously almost_semiring*)
    4.87 +begin
    4.88 +
    4.89 +subclass semiring_1 ..
    4.90  
    4.91 -lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
    4.92 -by simp
    4.93 +lemma dvd_0_left_iff [simp]:
    4.94 +  "0 dvd a \<longleftrightarrow> a = 0"
    4.95 +  by (auto intro: dvd_refl elim!: dvdE)
    4.96  
    4.97 -lemma dvd_add[simp]:
    4.98 -  assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"
    4.99 +lemma dvd_0_right [iff]:
   4.100 +  "a dvd 0"
   4.101 +proof
   4.102 +  show "0 = a * 0" by simp
   4.103 +qed
   4.104 +
   4.105 +lemma dvd_0_left:
   4.106 +  "0 dvd a \<Longrightarrow> a = 0"
   4.107 +  by simp
   4.108 +
   4.109 +lemma dvd_add [simp]:
   4.110 +  assumes "a dvd b" and "a dvd c"
   4.111 +  shows "a dvd (b + c)"
   4.112  proof -
   4.113    from `a dvd b` obtain b' where "b = a * b'" ..
   4.114    moreover from `a dvd c` obtain c' where "c = a * c'" ..