# HG changeset patch
# User haftmann
# Date 1256850791 -3600
# Node ID 5a989586d102c69952af8301d2159767e3243729
# Parent  a165b97f3658cc307ab158a6500fd47c37304bb9
moved some dvd [int] facts to Int

diff -r a165b97f3658 -r 5a989586d102 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Oct 29 22:13:09 2009 +0100
+++ b/src/HOL/Int.thy	Thu Oct 29 22:13:11 2009 +0100
@@ -2105,6 +2105,14 @@
 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
   by (auto simp add: dvd_int_iff)
 
+lemma eq_nat_nat_iff:
+  "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
+  by (auto elim!: nonneg_eq_int)
+
+lemma nat_power_eq:
+  "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
+  by (induct n) (simp_all add: nat_mult_distrib)
+
 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   apply (rule_tac z=n in int_cases)
   apply (auto simp add: dvd_int_iff)