equal
deleted
inserted
replaced
2205 done |
2205 done |
2206 |
2206 |
2207 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y" |
2207 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y" |
2208 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult) |
2208 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult) |
2209 |
2209 |
2210 lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m" |
|
2211 apply (subgoal_tac "m mod n = 0") |
|
2212 apply (simp add: zmult_div_cancel) |
|
2213 apply (simp only: dvd_eq_mod_eq_0) |
|
2214 done |
|
2215 |
|
2216 text{*Suggested by Matthias Daum*} |
2210 text{*Suggested by Matthias Daum*} |
2217 lemma int_power_div_base: |
2211 lemma int_power_div_base: |
2218 "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)" |
2212 "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)" |
2219 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)") |
2213 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)") |
2220 apply (erule ssubst) |
2214 apply (erule ssubst) |