equal
deleted
inserted
replaced
210 assume ?L thus ?P using False by simp |
210 assume ?L thus ?P using False by simp |
211 qed |
211 qed |
212 with False show ?thesis by simp |
212 with False show ?thesis by simp |
213 qed |
213 qed |
214 |
214 |
|
215 lemma of_int_of_nat: "of_int k = (if k < 0 then - of_nat (nat (- k)) |
|
216 else of_nat (nat k))" |
|
217 by (auto simp add: of_nat_nat) |
215 |
218 |
216 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'" |
219 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'" |
217 apply (cases "0 \<le> z'") |
220 apply (cases "0 \<le> z'") |
218 apply (rule inj_int [THEN injD]) |
221 apply (rule inj_int [THEN injD]) |
219 apply (simp add: int_mult zero_le_mult_iff) |
222 apply (simp add: int_mult zero_le_mult_iff) |