--- a/src/HOL/Complex.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Complex.thy Wed Apr 22 19:09:21 2009 +0200
@@ -159,19 +159,7 @@
subsection {* Exponentiation *}
-instantiation complex :: recpower
-begin
-
-primrec power_complex where
- "z ^ 0 = (1\<Colon>complex)"
-| "z ^ Suc n = (z\<Colon>complex) * z ^ n"
-
-instance proof
-qed simp_all
-
-declare power_complex.simps [simp del]
-
-end
+instance complex :: recpower ..
subsection {* Numerals and Arithmetic *}
--- a/src/HOL/Int.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Int.thy Wed Apr 22 19:09:21 2009 +0200
@@ -1848,42 +1848,18 @@
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
-
-declare power_int.simps [simp del]
-
-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)
+instance int :: recpower ..
lemma of_int_power:
"of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
by (induct n) simp_all
-lemma int_power: "int (m^n) = (int m) ^ n"
+lemma zpower_zpower:
+ "(x ^ y) ^ z = (x ^ (y * z)::int)"
+ by (rule power_mult [symmetric])
+
+lemma int_power:
+ "int (m^n) = (int m) ^ n"
by (rule of_nat_power)
lemmas zpower_int = int_power [symmetric]
@@ -2278,4 +2254,15 @@
lemmas zless_le = less_int_def
lemmas int_eq_of_nat = TrueI
+lemma zpower_zadd_distrib:
+ "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
+ by (rule power_add)
+
+lemma zero_less_zpower_abs_iff:
+ "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
+ by (rule zero_less_power_abs_iff)
+
+lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
+ by (rule zero_le_power_abs)
+
end
--- a/src/HOL/Library/Euclidean_Space.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Wed Apr 22 19:09:21 2009 +0200
@@ -253,12 +253,7 @@
"vector_power x 0 = 1"
| "vector_power x (Suc n) = x * vector_power x n"
-instantiation "^" :: (recpower,type) recpower
-begin
- definition vec_power_def: "op ^ \<equiv> vector_power"
- instance
- apply (intro_classes) by (simp_all add: vec_power_def)
-end
+instance "^" :: (recpower,type) recpower ..
instance "^" :: (semiring,type) semiring
apply (intro_classes) by (vector ring_simps)+
--- a/src/HOL/Library/Float.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Float.thy Wed Apr 22 19:09:21 2009 +0200
@@ -15,8 +15,8 @@
datatype float = Float int int
-fun Ifloat :: "float \<Rightarrow> real" where
-"Ifloat (Float a b) = real a * pow2 b"
+primrec Ifloat :: "float \<Rightarrow> real" where
+ "Ifloat (Float a b) = real a * pow2 b"
instantiation float :: zero begin
definition zero_float where "0 = Float 0 0"
@@ -33,11 +33,11 @@
instance ..
end
-fun mantissa :: "float \<Rightarrow> int" where
-"mantissa (Float a b) = a"
+primrec mantissa :: "float \<Rightarrow> int" where
+ "mantissa (Float a b) = a"
-fun scale :: "float \<Rightarrow> int" where
-"scale (Float a b) = b"
+primrec scale :: "float \<Rightarrow> int" where
+ "scale (Float a b) = b"
lemma Ifloat_neg_exp: "e < 0 \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto
lemma Ifloat_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto
@@ -320,12 +320,12 @@
end
instantiation float :: uminus begin
-fun uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
+primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
instance ..
end
instantiation float :: minus begin
-fun minus_float where [simp del]: "(z::float) - w = z + (- w)"
+definition minus_float where [simp del]: "(z::float) - w = z + (- w)"
instance ..
end
@@ -334,11 +334,11 @@
instance ..
end
-fun float_pprt :: "float \<Rightarrow> float" where
-"float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)"
+primrec float_pprt :: "float \<Rightarrow> float" where
+ "float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)"
-fun float_nprt :: "float \<Rightarrow> float" where
-"float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))"
+primrec float_nprt :: "float \<Rightarrow> float" where
+ "float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))"
instantiation float :: ord begin
definition le_float_def: "z \<le> w \<equiv> Ifloat z \<le> Ifloat w"
@@ -354,7 +354,7 @@
by (cases a, simp add: uminus_float.simps)
lemma Ifloat_sub[simp]: "Ifloat (a - b) = Ifloat a - Ifloat b"
- by (cases a, cases b, simp add: minus_float.simps)
+ by (cases a, cases b, simp add: minus_float_def)
lemma Ifloat_mult[simp]: "Ifloat (a*b) = Ifloat a * Ifloat b"
by (cases a, cases b, simp add: times_float.simps pow2_add)
@@ -443,37 +443,10 @@
lemma Ifloat_min: "Ifloat (min x y) = min (Ifloat x) (Ifloat y)" unfolding min_def le_float_def by auto
lemma Ifloat_max: "Ifloat (max a b) = max (Ifloat a) (Ifloat b)" unfolding max_def le_float_def by auto
-instantiation float :: power begin
-fun power_float where [simp del]: "(Float m e) ^ n = Float (m ^ n) (e * int n)"
-instance ..
-end
-
-instance float :: recpower
-proof (intro_classes)
- fix a :: float show "a ^ 0 = 1" by (cases a, auto simp add: power_float.simps one_float_def)
-next
- fix a :: float and n :: nat show "a ^ (Suc n) = a * a ^ n"
- by (cases a, auto simp add: power_float.simps times_float.simps algebra_simps)
-qed
+instance float :: recpower ..
-lemma float_power: "Ifloat (x ^ n) = (Ifloat x) ^ n"
-proof (cases x)
- case (Float m e)
-
- have "pow2 e ^ n = pow2 (e * int n)"
- proof (cases "e >= 0")
- case True hence e_nat: "e = int (nat e)" by auto
- hence "pow2 e ^ n = (2 ^ nat e) ^ n" using pow2_int[of "nat e"] by auto
- thus ?thesis unfolding power_mult[symmetric] unfolding pow2_int[symmetric] int_mult e_nat[symmetric] .
- next
- case False hence e_minus: "-e = int (nat (-e))" by auto
- hence "pow2 (-e) ^ n = (2 ^ nat (-e)) ^ n" using pow2_int[of "nat (-e)"] by auto
- hence "pow2 (-e) ^ n = pow2 ((-e) * int n)" unfolding power_mult[symmetric] unfolding pow2_int[symmetric] int_mult e_minus[symmetric] zmult_zminus .
- thus ?thesis unfolding pow2_neg[of "-e"] pow2_neg[of "-e * int n"] unfolding zmult_zminus zminus_zminus nonzero_power_inverse[OF pow2_neq_zero, symmetric]
- using nonzero_inverse_eq_imp_eq[OF _ pow2_neq_zero pow2_neq_zero] by auto
- qed
- thus ?thesis by (auto simp add: Float power_mult_distrib Ifloat.simps power_float.simps)
-qed
+lemma float_power: "Ifloat (x ^ n) = Ifloat x ^ n"
+ by (induct n) simp_all
lemma zero_le_pow2[simp]: "0 \<le> pow2 s"
apply (subgoal_tac "0 < pow2 s")
@@ -1182,12 +1155,12 @@
unfolding x_eq y_eq float_divr.simps Let_def le_float_def Ifloat_0 Ifloat_mult by (auto intro!: mult_nonneg_nonpos)
qed
-fun round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
+primrec round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
"round_down prec (Float m e) = (let d = bitlen m - int prec in
if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
else Float m e)"
-fun round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
+primrec round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
"round_up prec (Float m e) = (let d = bitlen m - int prec in
if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d)
else Float m e)"
@@ -1314,8 +1287,8 @@
finally show ?thesis .
qed
-fun float_abs :: "float \<Rightarrow> float" where
-"float_abs (Float m e) = Float \<bar>m\<bar> e"
+primrec float_abs :: "float \<Rightarrow> float" where
+ "float_abs (Float m e) = Float \<bar>m\<bar> e"
instantiation float :: abs begin
definition abs_float_def: "\<bar>x\<bar> = float_abs x"
@@ -1329,8 +1302,8 @@
thus ?thesis unfolding Float abs_float_def float_abs.simps Ifloat.simps by auto
qed
-fun floor_fl :: "float \<Rightarrow> float" where
-"floor_fl (Float m e) = (if 0 \<le> e then Float m e
+primrec floor_fl :: "float \<Rightarrow> float" where
+ "floor_fl (Float m e) = (if 0 \<le> e then Float m e
else Float (m div (2 ^ (nat (-e)))) 0)"
lemma floor_fl: "Ifloat (floor_fl x) \<le> Ifloat x"
@@ -1358,8 +1331,8 @@
declare floor_fl.simps[simp del]
-fun ceiling_fl :: "float \<Rightarrow> float" where
-"ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
+primrec ceiling_fl :: "float \<Rightarrow> float" where
+ "ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
else Float (m div (2 ^ (nat (-e))) + 1) 0)"
lemma ceiling_fl: "Ifloat x \<le> Ifloat (ceiling_fl x)"
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Apr 22 19:09:21 2009 +0200
@@ -680,30 +680,14 @@
subsection {* Powers*}
-instantiation fps :: (semiring_1) power
-begin
-
-fun fps_pow :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where
- "fps_pow 0 f = 1"
-| "fps_pow (Suc n) f = f * fps_pow n f"
-
-definition fps_power_def: "power (f::'a fps) n = fps_pow n f"
-instance ..
-end
-
-instantiation fps :: (comm_ring_1) recpower
-begin
-instance
- apply (intro_classes)
- by (simp_all add: fps_power_def)
-end
+instance fps :: (semiring_1) recpower ..
lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
- by (induct n, auto simp add: fps_power_def expand_fps_eq fps_mult_nth)
+ by (induct n, auto simp add: expand_fps_eq fps_mult_nth)
lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)$0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
proof(induct n)
- case 0 thus ?case by (simp add: fps_power_def)
+ case 0 thus ?case by simp
next
case (Suc n)
note h = Suc.hyps[OF `a$0 = 1`]
@@ -712,13 +696,13 @@
qed
lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n $ 0 = 1"
- by (induct n, auto simp add: fps_power_def fps_mult_nth)
+ by (induct n, auto simp add: fps_mult_nth)
lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
- by (induct n, auto simp add: fps_power_def fps_mult_nth)
+ by (induct n, auto simp add: fps_mult_nth)
lemma startsby_power:"a $0 = (v::'a::{comm_ring_1, recpower}) \<Longrightarrow> a^n $0 = v^n"
- by (induct n, auto simp add: fps_power_def fps_mult_nth power_Suc)
+ by (induct n, auto simp add: fps_mult_nth power_Suc)
lemma startsby_zero_power_iff[simp]:
"a^n $0 = (0::'a::{idom, recpower}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
@@ -901,7 +885,7 @@
lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)"
proof(induct k)
- case 0 thus ?case by (simp add: X_def fps_power_def fps_eq_iff)
+ case 0 thus ?case by (simp add: X_def fps_eq_iff)
next
case (Suc k)
{fix m
@@ -1903,19 +1887,16 @@
done
lemma fps_compose_1[simp]: "1 oo a = 1"
- by (simp add: fps_eq_iff fps_compose_nth fps_power_def mult_delta_left setsum_delta)
+ by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
lemma fps_compose_0[simp]: "0 oo a = 0"
by (simp add: fps_eq_iff fps_compose_nth)
-lemma fps_pow_0: "fps_pow n 0 = (if n = 0 then 1 else 0)"
- by (induct n, simp_all)
-
lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a$0)"
- by (auto simp add: fps_eq_iff fps_compose_nth fps_power_def fps_pow_0 setsum_0')
+ by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum_0')
lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)"
- by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_addf)
+ by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_addf)
lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\<lambda>i. f i oo a) S"
proof-
@@ -2343,11 +2324,11 @@
proof-
have "fps_deriv ?lhs = 0"
apply (simp add: fps_deriv_power fps_sin_deriv fps_cos_deriv power_Suc)
- by (simp add: fps_power_def ring_simps fps_const_neg[symmetric] del: fps_const_neg)
+ by (simp add: ring_simps fps_const_neg[symmetric] del: fps_const_neg)
then have "?lhs = fps_const (?lhs $ 0)"
unfolding fps_deriv_eq_0_iff .
also have "\<dots> = 1"
- by (auto simp add: fps_eq_iff fps_power_def numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def)
+ by (auto simp add: fps_eq_iff numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def)
finally show ?thesis .
qed
--- a/src/HOL/Library/Numeral_Type.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Wed Apr 22 19:09:21 2009 +0200
@@ -154,8 +154,8 @@
locale mod_type =
fixes n :: int
- and Rep :: "'a::{zero,one,plus,times,uminus,minus,power} \<Rightarrow> int"
- and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus,power}"
+ and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
+ and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"
assumes type: "type_definition Rep Abs {0..<n}"
and size1: "1 < n"
and zero_def: "0 = Abs 0"
@@ -164,14 +164,13 @@
and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
and minus_def: "- x = Abs ((- Rep x) mod n)"
- and power_def: "x ^ k = Abs (Rep x ^ k mod n)"
begin
lemma size0: "0 < n"
by (cut_tac size1, simp)
lemmas definitions =
- zero_def one_def add_def mult_def minus_def diff_def power_def
+ zero_def one_def add_def mult_def minus_def diff_def
lemma Rep_less_n: "Rep x < n"
by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
@@ -227,8 +226,8 @@
locale mod_ring = mod_type +
constrains n :: int
- and Rep :: "'a::{number_ring,power} \<Rightarrow> int"
- and Abs :: "int \<Rightarrow> 'a::{number_ring,power}"
+ and Rep :: "'a::{number_ring} \<Rightarrow> int"
+ and Abs :: "int \<Rightarrow> 'a::{number_ring}"
begin
lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
@@ -272,7 +271,7 @@
@{typ num1}, since 0 and 1 are not distinct.
*}
-instantiation num1 :: "{comm_ring,comm_monoid_mult,number,recpower}"
+instantiation num1 :: "{comm_ring,comm_monoid_mult,number}"
begin
lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
@@ -284,7 +283,7 @@
end
instantiation
- bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}"
+ bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}"
begin
definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
@@ -299,7 +298,6 @@
definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)"
definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)"
definition "- x = Abs_bit0' (- Rep_bit0 x)"
-definition "x ^ k = Abs_bit0' (Rep_bit0 x ^ k)"
definition "0 = Abs_bit1 0"
definition "1 = Abs_bit1 1"
@@ -307,7 +305,6 @@
definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)"
definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)"
definition "- x = Abs_bit1' (- Rep_bit1 x)"
-definition "x ^ k = Abs_bit1' (Rep_bit1 x ^ k)"
instance ..
@@ -326,7 +323,6 @@
apply (rule times_bit0_def [unfolded Abs_bit0'_def])
apply (rule minus_bit0_def [unfolded Abs_bit0'_def])
apply (rule uminus_bit0_def [unfolded Abs_bit0'_def])
-apply (rule power_bit0_def [unfolded Abs_bit0'_def])
done
interpretation bit1:
@@ -342,7 +338,6 @@
apply (rule times_bit1_def [unfolded Abs_bit1'_def])
apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
-apply (rule power_bit1_def [unfolded Abs_bit1'_def])
done
instance bit0 :: (finite) "{comm_ring_1,recpower}"
@@ -386,9 +381,6 @@
lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
-declare power_Suc [where ?'a="'a::finite bit0", standard, simp]
-declare power_Suc [where ?'a="'a::finite bit1", standard, simp]
-
subsection {* Syntax *}
--- a/src/HOL/Library/Polynomial.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy Wed Apr 22 19:09:21 2009 +0200
@@ -632,19 +632,7 @@
shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
by (safe elim!: dvd_smult dvd_smult_cancel)
-instantiation poly :: (comm_semiring_1) recpower
-begin
-
-primrec power_poly where
- "(p::'a poly) ^ 0 = 1"
-| "(p::'a poly) ^ (Suc n) = p * p ^ n"
-
-instance
- by default simp_all
-
-declare power_poly.simps [simp del]
-
-end
+instance poly :: (comm_semiring_1) recpower ..
lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
by (induct n, simp, auto intro: order_trans degree_mult_le)
--- a/src/HOL/Library/Word.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Word.thy Wed Apr 22 19:09:21 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Library/Word.thy
- ID: $Id$
Author: Sebastian Skalberg (TU Muenchen)
*)
@@ -40,10 +39,8 @@
Zero ("\<zero>")
| One ("\<one>")
-primrec
- bitval :: "bit => nat"
-where
- "bitval \<zero> = 0"
+primrec bitval :: "bit => nat" where
+ "bitval \<zero> = 0"
| "bitval \<one> = 1"
consts
@@ -1531,7 +1528,7 @@
show ?thesis
apply simp
apply (subst power_Suc [symmetric])
- apply (simp del: power_int.simps)
+ apply simp
done
qed
finally show ?thesis .
--- a/src/HOL/Nat_Numeral.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Wed Apr 22 19:09:21 2009 +0200
@@ -28,9 +28,12 @@
"nat (number_of v) = number_of v"
unfolding nat_number_of_def ..
+context recpower
+begin
+
abbreviation (xsymbols)
- power2 :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
- "x\<twosuperior> == x^2"
+ power2 :: "'a \<Rightarrow> 'a" ("(_\<twosuperior>)" [1000] 999) where
+ "x\<twosuperior> \<equiv> x ^ 2"
notation (latex output)
power2 ("(_\<twosuperior>)" [1000] 999)
@@ -38,6 +41,8 @@
notation (HTML output)
power2 ("(_\<twosuperior>)" [1000] 999)
+end
+
subsection {* Predicate for negative binary numbers *}
@@ -397,8 +402,8 @@
by (simp add: power_even_eq)
lemma power_minus_even [simp]:
- "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
-by (simp add: power_minus1_even power_minus [of a])
+ "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
+ by (simp add: power_minus [of a])
lemma zero_le_even_power'[simp]:
"0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
@@ -972,4 +977,4 @@
Suc_mod_eq_add3_mod [of _ "number_of v", standard]
declare Suc_mod_eq_add3_mod_number_of [simp]
-end
+end
\ No newline at end of file
--- a/src/HOL/Power.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Power.thy Wed Apr 22 19:09:21 2009 +0200
@@ -1,24 +1,24 @@
(* Title: HOL/Power.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-
*)
-header{*Exponentiation*}
+header {* Exponentiation *}
theory Power
imports Nat
begin
-class power =
- fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80)
+subsection {* Powers for Arbitrary Monoids *}
+
+class recpower = monoid_mult
+begin
-subsection{*Powers for Arbitrary Monoids*}
+primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where
+ power_0: "a ^ 0 = 1"
+ | power_Suc: "a ^ Suc n = a * a ^ n"
-class recpower = monoid_mult + power +
- assumes power_0 [simp]: "a ^ 0 = 1"
- assumes power_Suc [simp]: "a ^ Suc n = a * (a ^ n)"
+end
lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
by simp
@@ -360,24 +360,9 @@
done
-subsection{*Exponentiation for the Natural Numbers*}
-
-instantiation nat :: recpower
-begin
-
-primrec power_nat where
- "p ^ 0 = (1\<Colon>nat)"
- | "p ^ (Suc n) = (p\<Colon>nat) * (p ^ n)"
+subsection {* Exponentiation for the Natural Numbers *}
-instance proof
- fix z n :: nat
- show "z^0 = 1" by simp
- show "z^(Suc n) = z * (z^n)" by simp
-qed
-
-declare power_nat.simps [simp del]
-
-end
+instance nat :: recpower ..
lemma of_nat_power:
"of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
@@ -391,7 +376,7 @@
lemma nat_power_eq_Suc_0_iff [simp]:
"((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
-by (induct_tac m, auto)
+by (induct m, auto)
lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
by simp
--- a/src/HOL/Rational.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Rational.thy Wed Apr 22 19:09:21 2009 +0200
@@ -156,11 +156,6 @@
then show ?thesis by (simp add: mult_rat [symmetric])
qed
-primrec power_rat
-where
- "q ^ 0 = (1\<Colon>rat)"
-| "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
-
instance proof
fix q r s :: rat show "(q * r) * s = q * (r * s)"
by (cases q, cases r, cases s) (simp add: eq_rat)
@@ -193,15 +188,8 @@
next
fix q :: rat show "q * 1 = q"
by (cases q) (simp add: One_rat_def eq_rat)
-next
- fix q :: rat
- fix n :: nat
- show "q ^ 0 = 1" by simp
- show "q ^ (Suc n) = q * (q ^ n)" by simp
qed
-declare power_rat.simps [simp del]
-
end
lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
@@ -222,7 +210,8 @@
definition
rat_number_of_def [code del]: "number_of w = Fract w 1"
-instance by intro_classes (simp add: rat_number_of_def of_int_rat)
+instance proof
+qed (simp add: rat_number_of_def of_int_rat)
end
--- a/src/HOL/RealPow.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/RealPow.thy Wed Apr 22 19:09:21 2009 +0200
@@ -12,24 +12,7 @@
declare abs_mult_self [simp]
-instantiation real :: recpower
-begin
-
-primrec power_real where
- "r ^ 0 = (1\<Colon>real)"
-| "r ^ Suc n = (r\<Colon>real) * r ^ n"
-
-instance proof
- fix z :: real
- fix n :: nat
- show "z^0 = 1" by simp
- show "z^(Suc n) = z * (z^n)" by simp
-qed
-
-declare power_real.simps [simp del]
-
-end
-
+instance real :: recpower ..
lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
by simp
@@ -47,7 +30,6 @@
lemma realpow_minus_mult [rule_format]:
"0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
-unfolding One_nat_def
apply (simp split add: nat_diff_split)
done