--- a/src/HOL/IntDiv.thy Thu Jan 24 23:51:22 2008 +0100
+++ b/src/HOL/IntDiv.thy Fri Jan 25 14:53:52 2008 +0100
@@ -1418,28 +1418,6 @@
apply (auto simp add: dvd_imp_le)
done
-
-subsection{*Integer Powers*}
-
-instance int :: power ..
-
-primrec
- "p ^ 0 = 1"
- "p ^ (Suc n) = (p::int) * (p ^ n)"
-
-
-instance int :: recpower
-proof
- fix z :: int
- fix n :: nat
- show "z^0 = 1" by simp
- show "z^(Suc n) = z * (z^n)" by simp
-qed
-
-lemma of_int_power:
- "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
- by (induct n) (simp_all add: power_Suc)
-
lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
apply (induct "y", auto)
apply (rule zmod_zmult1_eq [THEN trans])
@@ -1447,29 +1425,6 @@
apply (rule zmod_zmult_distrib [symmetric])
done
-lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
- by (rule Power.power_add)
-
-lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
- by (rule Power.power_mult [symmetric])
-
-lemma zero_less_zpower_abs_iff [simp]:
- "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
-apply (induct "n")
-apply (auto simp add: zero_less_mult_iff)
-done
-
-lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
-apply (induct "n")
-apply (auto simp add: zero_le_mult_iff)
-done
-
-lemma int_power: "int (m^n) = (int m) ^ n"
- by (rule of_nat_power)
-
-text{*Compatibility binding*}
-lemmas zpower_int = int_power [symmetric]
-
lemma zdiv_int: "int (a div b) = (int a) div (int b)"
apply (subst split_div, auto)
apply (subst split_zdiv, auto)