generalize zmod_zmod_cancel -> mod_mod_cancel
authorhuffman
Thu Jan 08 08:36:16 2009 -0800 (2009-01-08)
changeset 29404ee15ccdeaa72
parent 29403 fe17df4e4ab3
child 29405 98ab21b14f09
generalize zmod_zmod_cancel -> mod_mod_cancel
src/HOL/Divides.thy
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Jan 08 08:24:08 2009 -0800
     1.2 +++ b/src/HOL/Divides.thy	Thu Jan 08 08:36:16 2009 -0800
     1.3 @@ -248,6 +248,23 @@
     1.4      by (simp only: mod_mult_eq [symmetric])
     1.5  qed
     1.6  
     1.7 +lemma mod_mod_cancel:
     1.8 +  assumes "c dvd b"
     1.9 +  shows "a mod b mod c = a mod c"
    1.10 +proof -
    1.11 +  from `c dvd b` obtain k where "b = c * k"
    1.12 +    by (rule dvdE)
    1.13 +  have "a mod b mod c = a mod (c * k) mod c"
    1.14 +    by (simp only: `b = c * k`)
    1.15 +  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
    1.16 +    by (simp only: mod_mult_self1)
    1.17 +  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
    1.18 +    by (simp only: add_ac mult_ac)
    1.19 +  also have "\<dots> = a mod c"
    1.20 +    by (simp only: mod_div_equality)
    1.21 +  finally show ?thesis .
    1.22 +qed
    1.23 +
    1.24  end
    1.25  
    1.26  
     2.1 --- a/src/HOL/IntDiv.thy	Thu Jan 08 08:24:08 2009 -0800
     2.2 +++ b/src/HOL/IntDiv.thy	Thu Jan 08 08:36:16 2009 -0800
     2.3 @@ -938,18 +938,8 @@
     2.4  apply (auto simp add: mult_commute)
     2.5  done
     2.6  
     2.7 -lemma zmod_zmod_cancel:
     2.8 -assumes "n dvd m" shows "(k::int) mod m mod n = k mod n"
     2.9 -proof -
    2.10 -  from `n dvd m` obtain r where "m = n*r" by(auto simp:dvd_def)
    2.11 -  have "k mod n = (m * (k div m) + k mod m) mod n"
    2.12 -    using zmod_zdiv_equality[of k m] by simp
    2.13 -  also have "\<dots> = (m * (k div m) mod n + k mod m mod n) mod n"
    2.14 -    by(subst zmod_zadd1_eq, rule refl)
    2.15 -  also have "m * (k div m) mod n = 0" using `m = n*r`
    2.16 -    by(simp add:mult_ac)
    2.17 -  finally show ?thesis by simp
    2.18 -qed
    2.19 +lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
    2.20 +by (rule mod_mod_cancel)
    2.21  
    2.22  
    2.23  subsection {*Splitting Rules for div and mod*}