--- a/NEWS Mon Apr 27 08:22:37 2009 +0200
+++ b/NEWS Mon Apr 27 10:11:44 2009 +0200
@@ -20,7 +20,7 @@
* Power operations on relations and functions are now one dedicate constant compow with
infix syntax "^^". Power operations on multiplicative monoids retains syntax "^"
-and is now defined generic in class recpower; class power disappeared. INCOMPATIBILITY.
+and is now defined generic in class power. INCOMPATIBILITY.
* ML antiquotation @{code_datatype} inserts definition of a datatype generated
by the code generator; see Predicate.thy for an example.
--- a/src/HOL/Algebra/abstract/Ring2.thy Mon Apr 27 08:22:37 2009 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Mon Apr 27 10:11:44 2009 +0200
@@ -12,7 +12,7 @@
subsection {* Ring axioms *}
-class ring = zero + one + plus + minus + uminus + times + inverse + recpower + Ring_and_Field.dvd +
+class ring = zero + one + plus + minus + uminus + times + inverse + power + dvd +
assumes a_assoc: "(a + b) + c = a + (b + c)"
and l_zero: "0 + a = a"
and l_neg: "(-a) + a = 0"
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Mon Apr 27 08:22:37 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Mon Apr 27 10:11:44 2009 +0200
@@ -345,11 +345,10 @@
by (simp add: up_inverse_def)
show "p / q = p * inverse q"
by (simp add: up_divide_def)
- show "p * 1 = p"
- unfolding `p * 1 = 1 * p` by (fact `1 * p = p`)
qed
-instance up :: (ring) recpower ..
+instance up :: (ring) recpower proof
+qed simp_all
(* Further properties of monom *)
--- a/src/HOL/Int.thy Mon Apr 27 08:22:37 2009 +0200
+++ b/src/HOL/Int.thy Mon Apr 27 10:11:44 2009 +0200
@@ -1536,7 +1536,7 @@
by (simp add: abs_if)
lemma abs_power_minus_one [simp]:
- "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
+ "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring})"
by (simp add: power_abs)
lemma of_int_number_of_eq [simp]:
@@ -1848,18 +1848,21 @@
subsection {* Integer Powers *}
-instance int :: recpower ..
+context ring_1
+begin
lemma of_int_power:
- "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
+ "of_int (z ^ n) = of_int z ^ n"
by (induct n) simp_all
+end
+
lemma zpower_zpower:
"(x ^ y) ^ z = (x ^ (y * z)::int)"
by (rule power_mult [symmetric])
lemma int_power:
- "int (m^n) = (int m) ^ n"
+ "int (m ^ n) = int m ^ n"
by (rule of_nat_power)
lemmas zpower_int = int_power [symmetric]
@@ -2200,6 +2203,8 @@
subsection {* Legacy theorems *}
+instance int :: recpower ..
+
lemmas zminus_zminus = minus_minus [of "z::int", standard]
lemmas zminus_0 = minus_zero [where 'a=int]
lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
--- a/src/HOL/NSA/HyperDef.thy Mon Apr 27 08:22:37 2009 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon Apr 27 10:11:44 2009 +0200
@@ -426,7 +426,7 @@
subsection{*Powers with Hypernatural Exponents*}
-definition pow :: "['a::recpower star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
+definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
(* hypernatural powers of hyperreals *)
@@ -459,7 +459,7 @@
by transfer (rule power_add)
lemma hyperpow_one [simp]:
- "\<And>r. (r::'a::recpower star) pow (1::hypnat) = r"
+ "\<And>r. (r::'a::monoid_mult star) pow (1::hypnat) = r"
by transfer (rule power_one_right)
lemma hyperpow_two:
--- a/src/HOL/Power.thy Mon Apr 27 08:22:37 2009 +0200
+++ b/src/HOL/Power.thy Mon Apr 27 10:11:44 2009 +0200
@@ -36,7 +36,7 @@
by (induct n) simp_all
lemma power_one_right [simp]:
- "a ^ 1 = a * 1"
+ "a ^ 1 = a"
by simp
lemma power_commutes: