equal
deleted
inserted
replaced
206 assume ?L thus ?P using False by simp |
206 assume ?L thus ?P using False by simp |
207 qed |
207 qed |
208 with False show ?thesis by simp |
208 with False show ?thesis by simp |
209 qed |
209 qed |
210 |
210 |
211 lemma of_int_of_nat: "of_int k = (if k < 0 then - of_nat (nat (- k)) |
211 context ring_1 |
212 else of_nat (nat k))" |
212 begin |
213 by (auto simp add: of_nat_nat) |
213 |
|
214 lemma of_int_of_nat: |
|
215 "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" |
|
216 proof (cases "k < 0") |
|
217 case True then have "0 \<le> - k" by simp |
|
218 then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat) |
|
219 with True show ?thesis by simp |
|
220 next |
|
221 case False then show ?thesis by (simp add: not_less of_nat_nat) |
|
222 qed |
|
223 |
|
224 end |
214 |
225 |
215 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'" |
226 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'" |
216 apply (cases "0 \<le> z'") |
227 apply (cases "0 \<le> z'") |
217 apply (rule inj_int [THEN injD]) |
228 apply (rule inj_int [THEN injD]) |
218 apply (simp add: int_mult zero_le_mult_iff) |
229 apply (simp add: int_mult zero_le_mult_iff) |