src/HOL/Int.thy
changeset 33341 5a989586d102
parent 33320 73998ef6ea91
child 33364 2bd12592c5e8
     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)