229 |
229 |
230 lemma m_rcancel: |
230 lemma m_rcancel: |
231 "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)" |
231 "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)" |
232 by (simp add: m_lcancel) |
232 by (simp add: m_lcancel) |
233 |
233 |
|
234 lemma power_0 [simp]: |
|
235 "(a::'a::ring) ^ 0 = 1" unfolding power_def by simp |
|
236 |
|
237 lemma power_Suc [simp]: |
|
238 "(a::'a::ring) ^ Suc n = a ^ n * a" unfolding power_def by simp |
|
239 |
|
240 lemma power_one [simp]: |
|
241 "1 ^ n = (1::'a::ring)" by (induct n) simp_all |
|
242 |
|
243 lemma power_zero [simp]: |
|
244 "n \<noteq> 0 \<Longrightarrow> 0 ^ n = (0::'a::ring)" by (induct n) simp_all |
|
245 |
|
246 lemma power_mult [simp]: |
|
247 "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)" |
|
248 by (induct m) simp_all |
|
249 |
|
250 |
|
251 section "Divisibility" |
|
252 |
|
253 lemma dvd_zero_right [simp]: |
|
254 "(a::'a::ring) dvd 0" |
|
255 proof |
|
256 show "0 = a * 0" by simp |
|
257 qed |
|
258 |
|
259 lemma dvd_zero_left: |
|
260 "0 dvd (a::'a::ring) \<Longrightarrow> a = 0" unfolding dvd_def by simp |
|
261 |
|
262 lemma dvd_refl_ring [simp]: |
|
263 "(a::'a::ring) dvd a" |
|
264 proof |
|
265 show "a = a * 1" by simp |
|
266 qed |
|
267 |
|
268 lemma dvd_trans_ring: |
|
269 fixes a b c :: "'a::ring" |
|
270 assumes a_dvd_b: "a dvd b" |
|
271 and b_dvd_c: "b dvd c" |
|
272 shows "a dvd c" |
|
273 proof - |
|
274 from a_dvd_b obtain l where "b = a * l" using dvd_def by blast |
|
275 moreover from b_dvd_c obtain j where "c = b * j" using dvd_def by blast |
|
276 ultimately have "c = a * (l * j)" by simp |
|
277 then have "\<exists>k. c = a * k" .. |
|
278 then show ?thesis using dvd_def by blast |
|
279 qed |
|
280 |
|
281 lemma dvd_def': |
|
282 "m dvd n \<equiv> \<exists>k. n = m * k" unfolding dvd_def by simp |
|
283 |
234 end |
284 end |