--- a/NEWS Thu Jan 24 23:51:22 2008 +0100
+++ b/NEWS Fri Jan 25 14:53:52 2008 +0100
@@ -25,6 +25,8 @@
*** HOL ***
+* Theorems "power.simps" renamed to "power_int.simps".
+
* New class semiring_div provides basic abstract properties of semirings
with division and modulo operations. Subsumes former class dvd_mod.
--- a/src/HOL/Int.thy Thu Jan 24 23:51:22 2008 +0100
+++ b/src/HOL/Int.thy Fri Jan 25 14:53:52 2008 +0100
@@ -221,6 +221,7 @@
by (cases i, cases j, cases k) (simp add: le add)
qed
+
text{*Strict Monotonicity of Multiplication*}
text{*strict, in 1st argument; proof is by induction on k>0*}
@@ -261,6 +262,13 @@
by (simp only: zsgn_def)
qed
+instance int :: lordered_ring
+proof
+ fix k :: int
+ show "abs k = sup k (- k)"
+ by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric])
+qed
+
lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
apply (cases w, cases z)
apply (simp add: less le add One_int_def)
@@ -1729,6 +1737,46 @@
qed
+subsection{*Integer Powers*}
+
+instantiation int :: recpower
+begin
+
+primrec power_int where
+ "p ^ 0 = (1\<Colon>int)"
+ | "p ^ (Suc n) = (p\<Colon>int) * (p ^ n)"
+
+instance proof
+ fix z :: int
+ fix n :: nat
+ show "z ^ 0 = 1" by simp
+ show "z ^ Suc n = z * (z ^ n)" by simp
+qed
+
+end
+
+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) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
+ by (induct n) (auto simp add: zero_less_mult_iff)
+
+lemma zero_le_zpower_abs [simp]: "(0::int) \<le> abs x ^ n"
+ by (induct n) (auto simp add: zero_le_mult_iff)
+
+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 int_power: "int (m^n) = (int m) ^ n"
+ by (rule of_nat_power)
+
+lemmas zpower_int = int_power [symmetric]
+
subsection {* Configuration of the code generator *}
instance int :: eq ..
@@ -1765,7 +1813,7 @@
lemma one_is_num_one [code func, code inline, symmetric, code post]:
"(1\<Colon>int) = Numeral1"
- by simp
+ by simp
code_modulename SML
Int Integer
--- 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)
--- a/src/HOL/Library/Word.thy Thu Jan 24 23:51:22 2008 +0100
+++ b/src/HOL/Library/Word.thy Fri Jan 25 14:53:52 2008 +0100
@@ -40,11 +40,11 @@
Zero ("\<zero>")
| One ("\<one>")
-consts
+primrec
bitval :: "bit => nat"
-primrec
+where
"bitval \<zero> = 0"
- "bitval \<one> = 1"
+ | "bitval \<one> = 1"
consts
bitnot :: "bit => bit"
@@ -1531,7 +1531,7 @@
show ?thesis
apply simp
apply (subst power_Suc [symmetric])
- apply (simp del: power.simps)
+ apply (simp del: power_int.simps)
done
qed
finally show ?thesis .