power operation defined generic
authorhaftmann
Wed Apr 22 19:09:21 2009 +0200 (2009-04-22)
changeset 30960fec1a04b7220
parent 30959 458e55fd0a33
child 30961 541bfff659af
power operation defined generic
src/HOL/Complex.thy
src/HOL/Int.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Word.thy
src/HOL/Nat_Numeral.thy
src/HOL/Power.thy
src/HOL/Rational.thy
src/HOL/RealPow.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Apr 22 19:09:19 2009 +0200
     1.2 +++ b/src/HOL/Complex.thy	Wed Apr 22 19:09:21 2009 +0200
     1.3 @@ -159,19 +159,7 @@
     1.4  
     1.5  subsection {* Exponentiation *}
     1.6  
     1.7 -instantiation complex :: recpower
     1.8 -begin
     1.9 -
    1.10 -primrec power_complex where
    1.11 -  "z ^ 0     = (1\<Colon>complex)"
    1.12 -| "z ^ Suc n = (z\<Colon>complex) * z ^ n"
    1.13 -
    1.14 -instance proof
    1.15 -qed simp_all
    1.16 -
    1.17 -declare power_complex.simps [simp del]
    1.18 -
    1.19 -end
    1.20 +instance complex :: recpower ..
    1.21  
    1.22  
    1.23  subsection {* Numerals and Arithmetic *}
     2.1 --- a/src/HOL/Int.thy	Wed Apr 22 19:09:19 2009 +0200
     2.2 +++ b/src/HOL/Int.thy	Wed Apr 22 19:09:21 2009 +0200
     2.3 @@ -1848,42 +1848,18 @@
     2.4  
     2.5  subsection {* Integer Powers *} 
     2.6  
     2.7 -instantiation int :: recpower
     2.8 -begin
     2.9 -
    2.10 -primrec power_int where
    2.11 -  "p ^ 0 = (1\<Colon>int)"
    2.12 -  | "p ^ (Suc n) = (p\<Colon>int) * (p ^ n)"
    2.13 -
    2.14 -instance proof
    2.15 -  fix z :: int
    2.16 -  fix n :: nat
    2.17 -  show "z ^ 0 = 1" by simp
    2.18 -  show "z ^ Suc n = z * (z ^ n)" by simp
    2.19 -qed
    2.20 -
    2.21 -declare power_int.simps [simp del]
    2.22 -
    2.23 -end
    2.24 -
    2.25 -lemma zpower_zadd_distrib: "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
    2.26 -  by (rule Power.power_add)
    2.27 -
    2.28 -lemma zpower_zpower: "(x ^ y) ^ z = (x ^ (y * z)::int)"
    2.29 -  by (rule Power.power_mult [symmetric])
    2.30 -
    2.31 -lemma zero_less_zpower_abs_iff [simp]:
    2.32 -  "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
    2.33 -  by (induct n) (auto simp add: zero_less_mult_iff)
    2.34 -
    2.35 -lemma zero_le_zpower_abs [simp]: "(0::int) \<le> abs x ^ n"
    2.36 -  by (induct n) (auto simp add: zero_le_mult_iff)
    2.37 +instance int :: recpower ..
    2.38  
    2.39  lemma of_int_power:
    2.40    "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
    2.41    by (induct n) simp_all
    2.42  
    2.43 -lemma int_power: "int (m^n) = (int m) ^ n"
    2.44 +lemma zpower_zpower:
    2.45 +  "(x ^ y) ^ z = (x ^ (y * z)::int)"
    2.46 +  by (rule power_mult [symmetric])
    2.47 +
    2.48 +lemma int_power:
    2.49 +  "int (m^n) = (int m) ^ n"
    2.50    by (rule of_nat_power)
    2.51  
    2.52  lemmas zpower_int = int_power [symmetric]
    2.53 @@ -2278,4 +2254,15 @@
    2.54  lemmas zless_le = less_int_def
    2.55  lemmas int_eq_of_nat = TrueI
    2.56  
    2.57 +lemma zpower_zadd_distrib:
    2.58 +  "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
    2.59 +  by (rule power_add)
    2.60 +
    2.61 +lemma zero_less_zpower_abs_iff:
    2.62 +  "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
    2.63 +  by (rule zero_less_power_abs_iff)
    2.64 +
    2.65 +lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
    2.66 +  by (rule zero_le_power_abs)
    2.67 +
    2.68  end
     3.1 --- a/src/HOL/Library/Euclidean_Space.thy	Wed Apr 22 19:09:19 2009 +0200
     3.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Apr 22 19:09:21 2009 +0200
     3.3 @@ -253,12 +253,7 @@
     3.4    "vector_power x 0 = 1"
     3.5    | "vector_power x (Suc n) = x * vector_power x n"
     3.6  
     3.7 -instantiation "^" :: (recpower,type) recpower
     3.8 -begin
     3.9 -  definition vec_power_def: "op ^ \<equiv> vector_power"
    3.10 -  instance
    3.11 -  apply (intro_classes) by (simp_all add: vec_power_def)
    3.12 -end
    3.13 +instance "^" :: (recpower,type) recpower ..
    3.14  
    3.15  instance "^" :: (semiring,type) semiring
    3.16    apply (intro_classes) by (vector ring_simps)+
     4.1 --- a/src/HOL/Library/Float.thy	Wed Apr 22 19:09:19 2009 +0200
     4.2 +++ b/src/HOL/Library/Float.thy	Wed Apr 22 19:09:21 2009 +0200
     4.3 @@ -15,8 +15,8 @@
     4.4  
     4.5  datatype float = Float int int
     4.6  
     4.7 -fun Ifloat :: "float \<Rightarrow> real" where
     4.8 -"Ifloat (Float a b) = real a * pow2 b"
     4.9 +primrec Ifloat :: "float \<Rightarrow> real" where
    4.10 +  "Ifloat (Float a b) = real a * pow2 b"
    4.11  
    4.12  instantiation float :: zero begin
    4.13  definition zero_float where "0 = Float 0 0" 
    4.14 @@ -33,11 +33,11 @@
    4.15  instance ..
    4.16  end
    4.17  
    4.18 -fun mantissa :: "float \<Rightarrow> int" where
    4.19 -"mantissa (Float a b) = a"
    4.20 +primrec mantissa :: "float \<Rightarrow> int" where
    4.21 +  "mantissa (Float a b) = a"
    4.22  
    4.23 -fun scale :: "float \<Rightarrow> int" where
    4.24 -"scale (Float a b) = b"
    4.25 +primrec scale :: "float \<Rightarrow> int" where
    4.26 +  "scale (Float a b) = b"
    4.27  
    4.28  lemma Ifloat_neg_exp: "e < 0 \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto
    4.29  lemma Ifloat_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto
    4.30 @@ -320,12 +320,12 @@
    4.31  end
    4.32  
    4.33  instantiation float :: uminus begin
    4.34 -fun uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
    4.35 +primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
    4.36  instance ..
    4.37  end
    4.38  
    4.39  instantiation float :: minus begin
    4.40 -fun minus_float where [simp del]: "(z::float) - w = z + (- w)"
    4.41 +definition minus_float where [simp del]: "(z::float) - w = z + (- w)"
    4.42  instance ..
    4.43  end
    4.44  
    4.45 @@ -334,11 +334,11 @@
    4.46  instance ..
    4.47  end
    4.48  
    4.49 -fun float_pprt :: "float \<Rightarrow> float" where
    4.50 -"float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)"
    4.51 +primrec float_pprt :: "float \<Rightarrow> float" where
    4.52 +  "float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)"
    4.53  
    4.54 -fun float_nprt :: "float \<Rightarrow> float" where
    4.55 -"float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))" 
    4.56 +primrec float_nprt :: "float \<Rightarrow> float" where
    4.57 +  "float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))" 
    4.58  
    4.59  instantiation float :: ord begin
    4.60  definition le_float_def: "z \<le> w \<equiv> Ifloat z \<le> Ifloat w"
    4.61 @@ -354,7 +354,7 @@
    4.62    by (cases a, simp add: uminus_float.simps)
    4.63  
    4.64  lemma Ifloat_sub[simp]: "Ifloat (a - b) = Ifloat a - Ifloat b" 
    4.65 -  by (cases a, cases b, simp add: minus_float.simps)
    4.66 +  by (cases a, cases b, simp add: minus_float_def)
    4.67  
    4.68  lemma Ifloat_mult[simp]: "Ifloat (a*b) = Ifloat a * Ifloat b"
    4.69    by (cases a, cases b, simp add: times_float.simps pow2_add)
    4.70 @@ -443,37 +443,10 @@
    4.71  lemma Ifloat_min: "Ifloat (min x y) = min (Ifloat x) (Ifloat y)" unfolding min_def le_float_def by auto
    4.72  lemma Ifloat_max: "Ifloat (max a b) = max (Ifloat a) (Ifloat b)" unfolding max_def le_float_def by auto
    4.73  
    4.74 -instantiation float :: power begin 
    4.75 -fun power_float where [simp del]: "(Float m e) ^ n = Float (m ^ n) (e * int n)"
    4.76 -instance ..
    4.77 -end
    4.78 -
    4.79 -instance float :: recpower
    4.80 -proof (intro_classes)
    4.81 -  fix a :: float show "a ^ 0 = 1" by (cases a, auto simp add: power_float.simps one_float_def)
    4.82 -next
    4.83 -  fix a :: float and n :: nat show "a ^ (Suc n) = a * a ^ n" 
    4.84 -  by (cases a, auto simp add: power_float.simps times_float.simps algebra_simps)
    4.85 -qed
    4.86 +instance float :: recpower ..
    4.87  
    4.88 -lemma float_power: "Ifloat (x ^ n) = (Ifloat x) ^ n"
    4.89 -proof (cases x)
    4.90 -  case (Float m e)
    4.91 -  
    4.92 -  have "pow2 e ^ n = pow2 (e * int n)"
    4.93 -  proof (cases "e >= 0")
    4.94 -    case True hence e_nat: "e = int (nat e)" by auto
    4.95 -    hence "pow2 e ^ n = (2 ^ nat e) ^ n" using pow2_int[of "nat e"] by auto
    4.96 -    thus ?thesis unfolding power_mult[symmetric] unfolding pow2_int[symmetric] int_mult e_nat[symmetric] .
    4.97 -  next
    4.98 -    case False hence e_minus: "-e = int (nat (-e))" by auto
    4.99 -    hence "pow2 (-e) ^ n = (2 ^ nat (-e)) ^ n" using pow2_int[of "nat (-e)"] by auto
   4.100 -    hence "pow2 (-e) ^ n = pow2 ((-e) * int n)" unfolding power_mult[symmetric] unfolding pow2_int[symmetric] int_mult e_minus[symmetric] zmult_zminus .
   4.101 -    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]
   4.102 -      using nonzero_inverse_eq_imp_eq[OF _ pow2_neq_zero pow2_neq_zero] by auto
   4.103 -  qed
   4.104 -  thus ?thesis by (auto simp add: Float power_mult_distrib Ifloat.simps power_float.simps)
   4.105 -qed
   4.106 +lemma float_power: "Ifloat (x ^ n) = Ifloat x ^ n"
   4.107 +  by (induct n) simp_all
   4.108  
   4.109  lemma zero_le_pow2[simp]: "0 \<le> pow2 s"
   4.110    apply (subgoal_tac "0 < pow2 s")
   4.111 @@ -1182,12 +1155,12 @@
   4.112      unfolding x_eq y_eq float_divr.simps Let_def le_float_def Ifloat_0 Ifloat_mult by (auto intro!: mult_nonneg_nonpos)
   4.113  qed
   4.114  
   4.115 -fun round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
   4.116 +primrec round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
   4.117  "round_down prec (Float m e) = (let d = bitlen m - int prec in
   4.118       if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
   4.119                else Float m e)"
   4.120  
   4.121 -fun round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
   4.122 +primrec round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
   4.123  "round_up prec (Float m e) = (let d = bitlen m - int prec in
   4.124    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) 
   4.125             else Float m e)"
   4.126 @@ -1314,8 +1287,8 @@
   4.127    finally show ?thesis .
   4.128  qed
   4.129  
   4.130 -fun float_abs :: "float \<Rightarrow> float" where
   4.131 -"float_abs (Float m e) = Float \<bar>m\<bar> e"
   4.132 +primrec float_abs :: "float \<Rightarrow> float" where
   4.133 +  "float_abs (Float m e) = Float \<bar>m\<bar> e"
   4.134  
   4.135  instantiation float :: abs begin
   4.136  definition abs_float_def: "\<bar>x\<bar> = float_abs x"
   4.137 @@ -1329,8 +1302,8 @@
   4.138    thus ?thesis unfolding Float abs_float_def float_abs.simps Ifloat.simps by auto
   4.139  qed
   4.140  
   4.141 -fun floor_fl :: "float \<Rightarrow> float" where
   4.142 -"floor_fl (Float m e) = (if 0 \<le> e then Float m e
   4.143 +primrec floor_fl :: "float \<Rightarrow> float" where
   4.144 +  "floor_fl (Float m e) = (if 0 \<le> e then Float m e
   4.145                                    else Float (m div (2 ^ (nat (-e)))) 0)"
   4.146  
   4.147  lemma floor_fl: "Ifloat (floor_fl x) \<le> Ifloat x"
   4.148 @@ -1358,8 +1331,8 @@
   4.149  
   4.150  declare floor_fl.simps[simp del]
   4.151  
   4.152 -fun ceiling_fl :: "float \<Rightarrow> float" where
   4.153 -"ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
   4.154 +primrec ceiling_fl :: "float \<Rightarrow> float" where
   4.155 +  "ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
   4.156                                      else Float (m div (2 ^ (nat (-e))) + 1) 0)"
   4.157  
   4.158  lemma ceiling_fl: "Ifloat x \<le> Ifloat (ceiling_fl x)"
     5.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 22 19:09:19 2009 +0200
     5.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 22 19:09:21 2009 +0200
     5.3 @@ -680,30 +680,14 @@
     5.4  
     5.5  subsection {* Powers*}
     5.6  
     5.7 -instantiation fps :: (semiring_1) power
     5.8 -begin
     5.9 -
    5.10 -fun fps_pow :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where
    5.11 -  "fps_pow 0 f = 1"
    5.12 -| "fps_pow (Suc n) f = f * fps_pow n f"
    5.13 -
    5.14 -definition fps_power_def: "power (f::'a fps) n = fps_pow n f"
    5.15 -instance ..
    5.16 -end
    5.17 -
    5.18 -instantiation fps :: (comm_ring_1) recpower
    5.19 -begin
    5.20 -instance
    5.21 -  apply (intro_classes)
    5.22 -  by (simp_all add: fps_power_def)
    5.23 -end
    5.24 +instance fps :: (semiring_1) recpower ..
    5.25  
    5.26  lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
    5.27 -  by (induct n, auto simp add: fps_power_def expand_fps_eq fps_mult_nth)
    5.28 +  by (induct n, auto simp add: expand_fps_eq fps_mult_nth)
    5.29  
    5.30  lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)$0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
    5.31  proof(induct n)
    5.32 -  case 0 thus ?case by (simp add: fps_power_def)
    5.33 +  case 0 thus ?case by simp
    5.34  next
    5.35    case (Suc n)
    5.36    note h = Suc.hyps[OF `a$0 = 1`]
    5.37 @@ -712,13 +696,13 @@
    5.38  qed
    5.39  
    5.40  lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n $ 0 = 1"
    5.41 -  by (induct n, auto simp add: fps_power_def fps_mult_nth)
    5.42 +  by (induct n, auto simp add: fps_mult_nth)
    5.43  
    5.44  lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
    5.45 -  by (induct n, auto simp add: fps_power_def fps_mult_nth)
    5.46 +  by (induct n, auto simp add: fps_mult_nth)
    5.47  
    5.48  lemma startsby_power:"a $0 = (v::'a::{comm_ring_1, recpower}) \<Longrightarrow> a^n $0 = v^n"
    5.49 -  by (induct n, auto simp add: fps_power_def fps_mult_nth power_Suc)
    5.50 +  by (induct n, auto simp add: fps_mult_nth power_Suc)
    5.51  
    5.52  lemma startsby_zero_power_iff[simp]:
    5.53    "a^n $0 = (0::'a::{idom, recpower}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
    5.54 @@ -901,7 +885,7 @@
    5.55  
    5.56  lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)"
    5.57  proof(induct k)
    5.58 -  case 0 thus ?case by (simp add: X_def fps_power_def fps_eq_iff)
    5.59 +  case 0 thus ?case by (simp add: X_def fps_eq_iff)
    5.60  next
    5.61    case (Suc k)
    5.62    {fix m
    5.63 @@ -1903,19 +1887,16 @@
    5.64    done
    5.65  
    5.66  lemma fps_compose_1[simp]: "1 oo a = 1"
    5.67 -  by (simp add: fps_eq_iff fps_compose_nth fps_power_def mult_delta_left setsum_delta)
    5.68 +  by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
    5.69  
    5.70  lemma fps_compose_0[simp]: "0 oo a = 0"
    5.71    by (simp add: fps_eq_iff fps_compose_nth)
    5.72  
    5.73 -lemma fps_pow_0: "fps_pow n 0 = (if n = 0 then 1 else 0)"
    5.74 -  by (induct n, simp_all)
    5.75 -
    5.76  lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a$0)"
    5.77 -  by (auto simp add: fps_eq_iff fps_compose_nth fps_power_def fps_pow_0 setsum_0')
    5.78 +  by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum_0')
    5.79  
    5.80  lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)"
    5.81 -  by (simp add: fps_eq_iff fps_compose_nth  ring_simps setsum_addf)
    5.82 +  by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_addf)
    5.83  
    5.84  lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\<lambda>i. f i oo a) S"
    5.85  proof-
    5.86 @@ -2343,11 +2324,11 @@
    5.87  proof-
    5.88    have "fps_deriv ?lhs = 0"
    5.89      apply (simp add:  fps_deriv_power fps_sin_deriv fps_cos_deriv power_Suc)
    5.90 -    by (simp add: fps_power_def ring_simps fps_const_neg[symmetric] del: fps_const_neg)
    5.91 +    by (simp add: ring_simps fps_const_neg[symmetric] del: fps_const_neg)
    5.92    then have "?lhs = fps_const (?lhs $ 0)"
    5.93      unfolding fps_deriv_eq_0_iff .
    5.94    also have "\<dots> = 1"
    5.95 -    by (auto simp add: fps_eq_iff fps_power_def numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def)
    5.96 +    by (auto simp add: fps_eq_iff numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def)
    5.97    finally show ?thesis .
    5.98  qed
    5.99  
     6.1 --- a/src/HOL/Library/Numeral_Type.thy	Wed Apr 22 19:09:19 2009 +0200
     6.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Apr 22 19:09:21 2009 +0200
     6.3 @@ -154,8 +154,8 @@
     6.4  
     6.5  locale mod_type =
     6.6    fixes n :: int
     6.7 -  and Rep :: "'a::{zero,one,plus,times,uminus,minus,power} \<Rightarrow> int"
     6.8 -  and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus,power}"
     6.9 +  and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
    6.10 +  and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"
    6.11    assumes type: "type_definition Rep Abs {0..<n}"
    6.12    and size1: "1 < n"
    6.13    and zero_def: "0 = Abs 0"
    6.14 @@ -164,14 +164,13 @@
    6.15    and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
    6.16    and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
    6.17    and minus_def: "- x = Abs ((- Rep x) mod n)"
    6.18 -  and power_def: "x ^ k = Abs (Rep x ^ k mod n)"
    6.19  begin
    6.20  
    6.21  lemma size0: "0 < n"
    6.22  by (cut_tac size1, simp)
    6.23  
    6.24  lemmas definitions =
    6.25 -  zero_def one_def add_def mult_def minus_def diff_def power_def
    6.26 +  zero_def one_def add_def mult_def minus_def diff_def
    6.27  
    6.28  lemma Rep_less_n: "Rep x < n"
    6.29  by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
    6.30 @@ -227,8 +226,8 @@
    6.31  
    6.32  locale mod_ring = mod_type +
    6.33    constrains n :: int
    6.34 -  and Rep :: "'a::{number_ring,power} \<Rightarrow> int"
    6.35 -  and Abs :: "int \<Rightarrow> 'a::{number_ring,power}"
    6.36 +  and Rep :: "'a::{number_ring} \<Rightarrow> int"
    6.37 +  and Abs :: "int \<Rightarrow> 'a::{number_ring}"
    6.38  begin
    6.39  
    6.40  lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
    6.41 @@ -272,7 +271,7 @@
    6.42    @{typ num1}, since 0 and 1 are not distinct.
    6.43  *}
    6.44  
    6.45 -instantiation num1 :: "{comm_ring,comm_monoid_mult,number,recpower}"
    6.46 +instantiation num1 :: "{comm_ring,comm_monoid_mult,number}"
    6.47  begin
    6.48  
    6.49  lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
    6.50 @@ -284,7 +283,7 @@
    6.51  end
    6.52  
    6.53  instantiation
    6.54 -  bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}"
    6.55 +  bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}"
    6.56  begin
    6.57  
    6.58  definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
    6.59 @@ -299,7 +298,6 @@
    6.60  definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)"
    6.61  definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)"
    6.62  definition "- x = Abs_bit0' (- Rep_bit0 x)"
    6.63 -definition "x ^ k = Abs_bit0' (Rep_bit0 x ^ k)"
    6.64  
    6.65  definition "0 = Abs_bit1 0"
    6.66  definition "1 = Abs_bit1 1"
    6.67 @@ -307,7 +305,6 @@
    6.68  definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)"
    6.69  definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)"
    6.70  definition "- x = Abs_bit1' (- Rep_bit1 x)"
    6.71 -definition "x ^ k = Abs_bit1' (Rep_bit1 x ^ k)"
    6.72  
    6.73  instance ..
    6.74  
    6.75 @@ -326,7 +323,6 @@
    6.76  apply (rule times_bit0_def [unfolded Abs_bit0'_def])
    6.77  apply (rule minus_bit0_def [unfolded Abs_bit0'_def])
    6.78  apply (rule uminus_bit0_def [unfolded Abs_bit0'_def])
    6.79 -apply (rule power_bit0_def [unfolded Abs_bit0'_def])
    6.80  done
    6.81  
    6.82  interpretation bit1:
    6.83 @@ -342,7 +338,6 @@
    6.84  apply (rule times_bit1_def [unfolded Abs_bit1'_def])
    6.85  apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
    6.86  apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
    6.87 -apply (rule power_bit1_def [unfolded Abs_bit1'_def])
    6.88  done
    6.89  
    6.90  instance bit0 :: (finite) "{comm_ring_1,recpower}"
    6.91 @@ -386,9 +381,6 @@
    6.92  lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
    6.93  lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
    6.94  
    6.95 -declare power_Suc [where ?'a="'a::finite bit0", standard, simp]
    6.96 -declare power_Suc [where ?'a="'a::finite bit1", standard, simp]
    6.97 -
    6.98  
    6.99  subsection {* Syntax *}
   6.100  
     7.1 --- a/src/HOL/Library/Polynomial.thy	Wed Apr 22 19:09:19 2009 +0200
     7.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Apr 22 19:09:21 2009 +0200
     7.3 @@ -632,19 +632,7 @@
     7.4    shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
     7.5    by (safe elim!: dvd_smult dvd_smult_cancel)
     7.6  
     7.7 -instantiation poly :: (comm_semiring_1) recpower
     7.8 -begin
     7.9 -
    7.10 -primrec power_poly where
    7.11 -  "(p::'a poly) ^ 0 = 1"
    7.12 -| "(p::'a poly) ^ (Suc n) = p * p ^ n"
    7.13 -
    7.14 -instance
    7.15 -  by default simp_all
    7.16 -
    7.17 -declare power_poly.simps [simp del]
    7.18 -
    7.19 -end
    7.20 +instance poly :: (comm_semiring_1) recpower ..
    7.21  
    7.22  lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
    7.23  by (induct n, simp, auto intro: order_trans degree_mult_le)
     8.1 --- a/src/HOL/Library/Word.thy	Wed Apr 22 19:09:19 2009 +0200
     8.2 +++ b/src/HOL/Library/Word.thy	Wed Apr 22 19:09:21 2009 +0200
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      HOL/Library/Word.thy
     8.5 -    ID:         $Id$
     8.6      Author:     Sebastian Skalberg (TU Muenchen)
     8.7  *)
     8.8  
     8.9 @@ -40,10 +39,8 @@
    8.10      Zero ("\<zero>")
    8.11    | One ("\<one>")
    8.12  
    8.13 -primrec
    8.14 -  bitval :: "bit => nat"
    8.15 -where
    8.16 -  "bitval \<zero> = 0"
    8.17 +primrec bitval :: "bit => nat" where
    8.18 +    "bitval \<zero> = 0"
    8.19    | "bitval \<one> = 1"
    8.20  
    8.21  consts
    8.22 @@ -1531,7 +1528,7 @@
    8.23      show ?thesis
    8.24        apply simp
    8.25        apply (subst power_Suc [symmetric])
    8.26 -      apply (simp del: power_int.simps)
    8.27 +      apply simp
    8.28        done
    8.29    qed
    8.30    finally show ?thesis .
     9.1 --- a/src/HOL/Nat_Numeral.thy	Wed Apr 22 19:09:19 2009 +0200
     9.2 +++ b/src/HOL/Nat_Numeral.thy	Wed Apr 22 19:09:21 2009 +0200
     9.3 @@ -28,9 +28,12 @@
     9.4    "nat (number_of v) = number_of v"
     9.5    unfolding nat_number_of_def ..
     9.6  
     9.7 +context recpower
     9.8 +begin
     9.9 +
    9.10  abbreviation (xsymbols)
    9.11 -  power2 :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
    9.12 -  "x\<twosuperior> == x^2"
    9.13 +  power2 :: "'a \<Rightarrow> 'a"  ("(_\<twosuperior>)" [1000] 999) where
    9.14 +  "x\<twosuperior> \<equiv> x ^ 2"
    9.15  
    9.16  notation (latex output)
    9.17    power2  ("(_\<twosuperior>)" [1000] 999)
    9.18 @@ -38,6 +41,8 @@
    9.19  notation (HTML output)
    9.20    power2  ("(_\<twosuperior>)" [1000] 999)
    9.21  
    9.22 +end
    9.23 +
    9.24  
    9.25  subsection {* Predicate for negative binary numbers *}
    9.26  
    9.27 @@ -397,8 +402,8 @@
    9.28  by (simp add: power_even_eq) 
    9.29  
    9.30  lemma power_minus_even [simp]:
    9.31 -     "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
    9.32 -by (simp add: power_minus1_even power_minus [of a]) 
    9.33 +  "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
    9.34 +  by (simp add: power_minus [of a]) 
    9.35  
    9.36  lemma zero_le_even_power'[simp]:
    9.37       "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
    9.38 @@ -972,4 +977,4 @@
    9.39      Suc_mod_eq_add3_mod [of _ "number_of v", standard]
    9.40  declare Suc_mod_eq_add3_mod_number_of [simp]
    9.41  
    9.42 -end
    9.43 +end
    9.44 \ No newline at end of file
    10.1 --- a/src/HOL/Power.thy	Wed Apr 22 19:09:19 2009 +0200
    10.2 +++ b/src/HOL/Power.thy	Wed Apr 22 19:09:21 2009 +0200
    10.3 @@ -1,24 +1,24 @@
    10.4  (*  Title:      HOL/Power.thy
    10.5 -    ID:         $Id$
    10.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7      Copyright   1997  University of Cambridge
    10.8 -
    10.9  *)
   10.10  
   10.11 -header{*Exponentiation*}
   10.12 +header {* Exponentiation *}
   10.13  
   10.14  theory Power
   10.15  imports Nat
   10.16  begin
   10.17  
   10.18 -class power =
   10.19 -  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "^" 80)
   10.20 +subsection {* Powers for Arbitrary Monoids *}
   10.21 +
   10.22 +class recpower = monoid_mult
   10.23 +begin
   10.24  
   10.25 -subsection{*Powers for Arbitrary Monoids*}
   10.26 +primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where
   10.27 +    power_0: "a ^ 0 = 1"
   10.28 +  | power_Suc: "a ^ Suc n = a * a ^ n"
   10.29  
   10.30 -class recpower = monoid_mult + power +
   10.31 -  assumes power_0 [simp]: "a ^ 0       = 1"
   10.32 -  assumes power_Suc [simp]: "a ^ Suc n = a * (a ^ n)"
   10.33 +end
   10.34  
   10.35  lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
   10.36    by simp
   10.37 @@ -360,24 +360,9 @@
   10.38  done
   10.39  
   10.40  
   10.41 -subsection{*Exponentiation for the Natural Numbers*}
   10.42 -
   10.43 -instantiation nat :: recpower
   10.44 -begin
   10.45 -
   10.46 -primrec power_nat where
   10.47 -  "p ^ 0 = (1\<Colon>nat)"
   10.48 -  | "p ^ (Suc n) = (p\<Colon>nat) * (p ^ n)"
   10.49 +subsection {* Exponentiation for the Natural Numbers *}
   10.50  
   10.51 -instance proof
   10.52 -  fix z n :: nat
   10.53 -  show "z^0 = 1" by simp
   10.54 -  show "z^(Suc n) = z * (z^n)" by simp
   10.55 -qed
   10.56 -
   10.57 -declare power_nat.simps [simp del]
   10.58 -
   10.59 -end
   10.60 +instance nat :: recpower ..
   10.61  
   10.62  lemma of_nat_power:
   10.63    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
   10.64 @@ -391,7 +376,7 @@
   10.65  
   10.66  lemma nat_power_eq_Suc_0_iff [simp]: 
   10.67    "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
   10.68 -by (induct_tac m, auto)
   10.69 +by (induct m, auto)
   10.70  
   10.71  lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
   10.72  by simp
    11.1 --- a/src/HOL/Rational.thy	Wed Apr 22 19:09:19 2009 +0200
    11.2 +++ b/src/HOL/Rational.thy	Wed Apr 22 19:09:21 2009 +0200
    11.3 @@ -156,11 +156,6 @@
    11.4    then show ?thesis by (simp add: mult_rat [symmetric])
    11.5  qed
    11.6  
    11.7 -primrec power_rat
    11.8 -where
    11.9 -  "q ^ 0 = (1\<Colon>rat)"
   11.10 -| "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
   11.11 -
   11.12  instance proof
   11.13    fix q r s :: rat show "(q * r) * s = q * (r * s)" 
   11.14      by (cases q, cases r, cases s) (simp add: eq_rat)
   11.15 @@ -193,15 +188,8 @@
   11.16  next
   11.17    fix q :: rat show "q * 1 = q"
   11.18      by (cases q) (simp add: One_rat_def eq_rat)
   11.19 -next
   11.20 -  fix q :: rat
   11.21 -  fix n :: nat
   11.22 -  show "q ^ 0 = 1" by simp
   11.23 -  show "q ^ (Suc n) = q * (q ^ n)" by simp
   11.24  qed
   11.25  
   11.26 -declare power_rat.simps [simp del]
   11.27 -
   11.28  end
   11.29  
   11.30  lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
   11.31 @@ -222,7 +210,8 @@
   11.32  definition
   11.33    rat_number_of_def [code del]: "number_of w = Fract w 1"
   11.34  
   11.35 -instance by intro_classes (simp add: rat_number_of_def of_int_rat)
   11.36 +instance proof
   11.37 +qed (simp add: rat_number_of_def of_int_rat)
   11.38  
   11.39  end
   11.40  
    12.1 --- a/src/HOL/RealPow.thy	Wed Apr 22 19:09:19 2009 +0200
    12.2 +++ b/src/HOL/RealPow.thy	Wed Apr 22 19:09:21 2009 +0200
    12.3 @@ -12,24 +12,7 @@
    12.4  
    12.5  declare abs_mult_self [simp]
    12.6  
    12.7 -instantiation real :: recpower
    12.8 -begin
    12.9 -
   12.10 -primrec power_real where
   12.11 -  "r ^ 0     = (1\<Colon>real)"
   12.12 -| "r ^ Suc n = (r\<Colon>real) * r ^ n"
   12.13 -
   12.14 -instance proof
   12.15 -  fix z :: real
   12.16 -  fix n :: nat
   12.17 -  show "z^0 = 1" by simp
   12.18 -  show "z^(Suc n) = z * (z^n)" by simp
   12.19 -qed
   12.20 -
   12.21 -declare power_real.simps [simp del]
   12.22 -
   12.23 -end
   12.24 -
   12.25 +instance real :: recpower ..
   12.26  
   12.27  lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
   12.28  by simp
   12.29 @@ -47,7 +30,6 @@
   12.30  
   12.31  lemma realpow_minus_mult [rule_format]:
   12.32       "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
   12.33 -unfolding One_nat_def
   12.34  apply (simp split add: nat_diff_split)
   12.35  done
   12.36