moved some dvd [int] facts to Int
authorhaftmann
Thu Oct 29 22:13:11 2009 +0100 (2009-10-29)
changeset 333415a989586d102
parent 33340 a165b97f3658
child 33342 df8b5c05546f
moved some dvd [int] facts to Int
src/HOL/Int.thy
     1.1 --- a/src/HOL/Int.thy	Thu Oct 29 22:13:09 2009 +0100
     1.2 +++ b/src/HOL/Int.thy	Thu Oct 29 22:13:11 2009 +0100
     1.3 @@ -2105,6 +2105,14 @@
     1.4  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
     1.5    by (auto simp add: dvd_int_iff)
     1.6  
     1.7 +lemma eq_nat_nat_iff:
     1.8 +  "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
     1.9 +  by (auto elim!: nonneg_eq_int)
    1.10 +
    1.11 +lemma nat_power_eq:
    1.12 +  "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
    1.13 +  by (induct n) (simp_all add: nat_mult_distrib)
    1.14 +
    1.15  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
    1.16    apply (rule_tac z=n in int_cases)
    1.17    apply (auto simp add: dvd_int_iff)