farewell to class recpower
authorhaftmann
Wed Apr 29 14:20:26 2009 +0200 (2009-04-29)
changeset 3102153642251a04f
parent 31020 9999a77590c3
child 31022 a438b4516dd3
farewell to class recpower
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy
src/HOL/Int.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Pocklington.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Library/comm_ring.ML
src/HOL/NSA/StarDef.thy
src/HOL/Power.thy
src/HOL/Rational.thy
src/HOL/RealPow.thy
src/HOL/SizeChange/Graphs.thy
src/HOL/SizeChange/Kleene_Algebras.thy
src/HOL/Word/WordArith.thy
src/HOL/ex/Commutative_Ring_Complete.thy
src/HOL/ex/Formal_Power_Series_Examples.thy
src/HOL/ex/Groebner_Examples.thy
src/HOL/ex/Numeral.thy
src/HOL/ex/ReflectionEx.thy
     1.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Tue Apr 28 19:15:50 2009 +0200
     1.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Apr 29 14:20:26 2009 +0200
     1.3 @@ -347,9 +347,6 @@
     1.4      by (simp add: up_divide_def)
     1.5  qed
     1.6  
     1.7 -instance up :: (ring) recpower proof
     1.8 -qed simp_all
     1.9 -
    1.10  (* Further properties of monom *)
    1.11  
    1.12  lemma monom_zero [simp]:
     2.1 --- a/src/HOL/Complex.thy	Tue Apr 28 19:15:50 2009 +0200
     2.2 +++ b/src/HOL/Complex.thy	Wed Apr 29 14:20:26 2009 +0200
     2.3 @@ -157,11 +157,6 @@
     2.4  end
     2.5  
     2.6  
     2.7 -subsection {* Exponentiation *}
     2.8 -
     2.9 -instance complex :: recpower ..
    2.10 -
    2.11 -
    2.12  subsection {* Numerals and Arithmetic *}
    2.13  
    2.14  instantiation complex :: number_ring
     3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue Apr 28 19:15:50 2009 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Apr 29 14:20:26 2009 +0200
     3.3 @@ -639,7 +639,7 @@
     3.4  
     3.5  interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
     3.6   "op <=" "op <"
     3.7 -   "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"
     3.8 +   "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,number_ring}) + y)"
     3.9  proof (unfold_locales, dlo, dlo, auto)
    3.10    fix x y::'a assume lt: "x < y"
    3.11    from  less_half_sum[OF lt] show "x < (x + y) /2" by simp
     4.1 --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Tue Apr 28 19:15:50 2009 +0200
     4.2 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Wed Apr 29 14:20:26 2009 +0200
     4.3 @@ -7,147 +7,147 @@
     4.4  begin
     4.5  
     4.6  lemma
     4.7 -  "\<exists>(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0"
     4.8 +  "\<exists>(y::'a::{ordered_field,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0"
     4.9    by ferrack
    4.10  
    4.11 -lemma "~ (ALL x (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < y --> 10*x < 11*y)"
    4.12 +lemma "~ (ALL x (y::'a::{ordered_field,number_ring, division_by_zero}). x < y --> 10*x < 11*y)"
    4.13    by ferrack
    4.14  
    4.15 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
    4.16 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
    4.17    by ferrack
    4.18  
    4.19 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x ~= y --> x < y"
    4.20 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. x ~= y --> x < y"
    4.21    by ferrack
    4.22  
    4.23 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
    4.24 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
    4.25    by ferrack
    4.26  
    4.27 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
    4.28 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
    4.29    by ferrack
    4.30  
    4.31 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
    4.32 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
    4.33    by ferrack
    4.34  
    4.35 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)"
    4.36 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)"
    4.37    by ferrack
    4.38  
    4.39 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
    4.40 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
    4.41    by ferrack
    4.42  
    4.43 -lemma "EX x. (ALL (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). y < 2 -->  2*(y - x) \<le> 0 )"
    4.44 +lemma "EX x. (ALL (y::'a::{ordered_field,number_ring, division_by_zero}). y < 2 -->  2*(y - x) \<le> 0 )"
    4.45    by ferrack
    4.46  
    4.47 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
    4.48 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
    4.49    by ferrack
    4.50  
    4.51 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0"
    4.52 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0"
    4.53    by ferrack
    4.54  
    4.55 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
    4.56 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
    4.57    by ferrack
    4.58  
    4.59 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)"
    4.60 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)"
    4.61    by ferrack
    4.62  
    4.63 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
    4.64 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
    4.65    by ferrack
    4.66  
    4.67 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
    4.68 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
    4.69    by ferrack
    4.70  
    4.71 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
    4.72 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
    4.73    by ferrack
    4.74  
    4.75 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
    4.76 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
    4.77    by ferrack
    4.78  
    4.79 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )"
    4.80 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )"
    4.81    by ferrack
    4.82  
    4.83 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    4.84 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    4.85    by ferrack
    4.86  
    4.87 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
    4.88 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
    4.89    by ferrack
    4.90  
    4.91 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    4.92 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    4.93    by ferrack
    4.94  
    4.95 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
    4.96 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
    4.97    by ferrack
    4.98  
    4.99 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
   4.100 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
   4.101    by ferrack
   4.102  
   4.103 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
   4.104 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
   4.105    by ferrack
   4.106  
   4.107 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
   4.108 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
   4.109    by ferrack
   4.110  
   4.111 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
   4.112 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
   4.113    by ferrack
   4.114  
   4.115 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
   4.116 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
   4.117    by ferrack
   4.118  
   4.119 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
   4.120 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
   4.121    by ferrack
   4.122  
   4.123 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
   4.124 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
   4.125    by ferrack
   4.126  
   4.127 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   4.128 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   4.129    by ferrack
   4.130  
   4.131 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
   4.132 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
   4.133    by ferrack
   4.134  
   4.135 -lemma "~(ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
   4.136 +lemma "~(ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
   4.137    by ferrack
   4.138  
   4.139 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
   4.140 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
   4.141    by ferrack
   4.142  
   4.143 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
   4.144 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
   4.145    by ferrack
   4.146  
   4.147 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
   4.148 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
   4.149    by ferrack
   4.150  
   4.151 -lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
   4.152 +lemma "EX z. (ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
   4.153    by ferrack
   4.154  
   4.155 -lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
   4.156 +lemma "EX z. (ALL (x::'a::{ordered_field,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
   4.157    by ferrack
   4.158  
   4.159 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
   4.160 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
   4.161    by ferrack
   4.162  
   4.163 -lemma "EX y. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
   4.164 +lemma "EX y. (ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
   4.165    by ferrack
   4.166  
   4.167 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
   4.168 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
   4.169    by ferrack
   4.170  
   4.171 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y).
   4.172 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y).
   4.173    (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
   4.174    by ferrack
   4.175  
   4.176 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y. (EX z > y.
   4.177 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (ALL y. (EX z > y.
   4.178    (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
   4.179    by ferrack
   4.180  
   4.181 -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   4.182 +lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   4.183    by ferrack
   4.184  
   4.185 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
   4.186 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
   4.187    by ferrack
   4.188  
   4.189 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
   4.190 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
   4.191    by ferrack
   4.192  
   4.193 -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
   4.194 +lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
   4.195    by ferrack
   4.196  
   4.197  end
     5.1 --- a/src/HOL/Int.thy	Tue Apr 28 19:15:50 2009 +0200
     5.2 +++ b/src/HOL/Int.thy	Wed Apr 29 14:20:26 2009 +0200
     5.3 @@ -2178,8 +2178,6 @@
     5.4  
     5.5  subsection {* Legacy theorems *}
     5.6  
     5.7 -instance int :: recpower ..
     5.8 -
     5.9  lemmas zminus_zminus = minus_minus [of "z::int", standard]
    5.10  lemmas zminus_0 = minus_zero [where 'a=int]
    5.11  lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
     6.1 --- a/src/HOL/Library/Binomial.thy	Tue Apr 28 19:15:50 2009 +0200
     6.2 +++ b/src/HOL/Library/Binomial.thy	Wed Apr 29 14:20:26 2009 +0200
     6.3 @@ -292,7 +292,7 @@
     6.4  
     6.5  subsection{* Generalized binomial coefficients *}
     6.6  
     6.7 -definition gbinomial :: "'a::{field, recpower,ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
     6.8 +definition gbinomial :: "'a::{field, ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
     6.9    where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
    6.10  
    6.11  lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
    6.12 @@ -420,16 +420,16 @@
    6.13    by (simp add: gbinomial_def)
    6.14   
    6.15  lemma gbinomial_mult_fact:
    6.16 -  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::{field, ring_char_0,recpower}) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
    6.17 +  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::{field, ring_char_0}) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
    6.18    unfolding gbinomial_Suc
    6.19    by (simp_all add: field_simps del: fact_Suc)
    6.20  
    6.21  lemma gbinomial_mult_fact':
    6.22 -  "((a::'a::{field, ring_char_0,recpower}) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
    6.23 +  "((a::'a::{field, ring_char_0}) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
    6.24    using gbinomial_mult_fact[of k a]
    6.25    apply (subst mult_commute) .
    6.26  
    6.27 -lemma gbinomial_Suc_Suc: "((a::'a::{field,recpower, ring_char_0}) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
    6.28 +lemma gbinomial_Suc_Suc: "((a::'a::{field, ring_char_0}) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
    6.29  proof-
    6.30    {assume "k = 0" then have ?thesis by simp}
    6.31    moreover
     7.1 --- a/src/HOL/Library/Commutative_Ring.thy	Tue Apr 28 19:15:50 2009 +0200
     7.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Wed Apr 29 14:20:26 2009 +0200
     7.3 @@ -27,15 +27,15 @@
     7.4  
     7.5  text {* Interpretation functions for the shadow syntax. *}
     7.6  
     7.7 -fun
     7.8 -  Ipol :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
     7.9 +primrec
    7.10 +  Ipol :: "'a::{comm_ring_1} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
    7.11  where
    7.12      "Ipol l (Pc c) = c"
    7.13    | "Ipol l (Pinj i P) = Ipol (drop i l) P"
    7.14    | "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"
    7.15  
    7.16 -fun
    7.17 -  Ipolex :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
    7.18 +primrec
    7.19 +  Ipolex :: "'a::{comm_ring_1} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
    7.20  where
    7.21      "Ipolex l (Pol P) = Ipol l P"
    7.22    | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
    7.23 @@ -54,7 +54,7 @@
    7.24      PX p1 y p2 \<Rightarrow> Pinj x P)"
    7.25  
    7.26  definition
    7.27 -  mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
    7.28 +  mkPX :: "'a::{comm_ring} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
    7.29    "mkPX P i Q = (case P of
    7.30      Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
    7.31      Pinj j R \<Rightarrow> PX P i Q |
    7.32 @@ -63,7 +63,7 @@
    7.33  text {* Defining the basic ring operations on normalized polynomials *}
    7.34  
    7.35  function
    7.36 -  add :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65)
    7.37 +  add :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65)
    7.38  where
    7.39      "Pc a \<oplus> Pc b = Pc (a + b)"
    7.40    | "Pc c \<oplus> Pinj i P = Pinj i (P \<oplus> Pc c)"
    7.41 @@ -90,7 +90,7 @@
    7.42  termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
    7.43  
    7.44  function
    7.45 -  mul :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<otimes>" 70)
    7.46 +  mul :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<otimes>" 70)
    7.47  where
    7.48      "Pc a \<otimes> Pc b = Pc (a * b)"
    7.49    | "Pc c \<otimes> Pinj i P =
    7.50 @@ -122,8 +122,8 @@
    7.51    (auto simp add: mkPinj_def split: pol.split)
    7.52  
    7.53  text {* Negation*}
    7.54 -fun
    7.55 -  neg :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
    7.56 +primrec
    7.57 +  neg :: "'a::{comm_ring} pol \<Rightarrow> 'a pol"
    7.58  where
    7.59      "neg (Pc c) = Pc (-c)"
    7.60    | "neg (Pinj i P) = Pinj i (neg P)"
    7.61 @@ -131,13 +131,13 @@
    7.62  
    7.63  text {* Substraction *}
    7.64  definition
    7.65 -  sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65)
    7.66 +  sub :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65)
    7.67  where
    7.68    "sub P Q = P \<oplus> neg Q"
    7.69  
    7.70  text {* Square for Fast Exponentation *}
    7.71 -fun
    7.72 -  sqr :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
    7.73 +primrec
    7.74 +  sqr :: "'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
    7.75  where
    7.76      "sqr (Pc c) = Pc (c * c)"
    7.77    | "sqr (Pinj i P) = mkPinj i (sqr P)"
    7.78 @@ -146,7 +146,7 @@
    7.79  
    7.80  text {* Fast Exponentation *}
    7.81  fun
    7.82 -  pow :: "nat \<Rightarrow> 'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
    7.83 +  pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
    7.84  where
    7.85      "pow 0 P = Pc 1"
    7.86    | "pow n P = (if even n then pow (n div 2) (sqr P)
    7.87 @@ -161,8 +161,8 @@
    7.88  
    7.89  text {* Normalization of polynomial expressions *}
    7.90  
    7.91 -fun
    7.92 -  norm :: "'a::{comm_ring,recpower} polex \<Rightarrow> 'a pol"
    7.93 +primrec
    7.94 +  norm :: "'a::{comm_ring_1} polex \<Rightarrow> 'a pol"
    7.95  where
    7.96      "norm (Pol P) = P"
    7.97    | "norm (Add P Q) = norm P \<oplus> norm Q"
     8.1 --- a/src/HOL/Library/Euclidean_Space.thy	Tue Apr 28 19:15:50 2009 +0200
     8.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Apr 29 14:20:26 2009 +0200
     8.3 @@ -253,8 +253,6 @@
     8.4    "vector_power x 0 = 1"
     8.5    | "vector_power x (Suc n) = x * vector_power x n"
     8.6  
     8.7 -instance "^" :: (recpower,type) recpower ..
     8.8 -
     8.9  instance "^" :: (semiring,type) semiring
    8.10    apply (intro_classes) by (vector ring_simps)+
    8.11  
    8.12 @@ -2757,7 +2755,7 @@
    8.13  (* Geometric progression.                                                    *)
    8.14  (* ------------------------------------------------------------------------- *)
    8.15  
    8.16 -lemma sum_gp_basic: "((1::'a::{field, recpower}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
    8.17 +lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
    8.18    (is "?lhs = ?rhs")
    8.19  proof-
    8.20    {assume x1: "x = 1" hence ?thesis by simp}
    8.21 @@ -2775,7 +2773,7 @@
    8.22  qed
    8.23  
    8.24  lemma sum_gp_multiplied: assumes mn: "m <= n"
    8.25 -  shows "((1::'a::{field, recpower}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
    8.26 +  shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
    8.27    (is "?lhs = ?rhs")
    8.28  proof-
    8.29    let ?S = "{0..(n - m)}"
    8.30 @@ -2792,7 +2790,7 @@
    8.31      by (simp add: ring_simps power_add[symmetric])
    8.32  qed
    8.33  
    8.34 -lemma sum_gp: "setsum (op ^ (x::'a::{field, recpower})) {m .. n} =
    8.35 +lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
    8.36     (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
    8.37                      else (x^ m - x^ (Suc n)) / (1 - x))"
    8.38  proof-
    8.39 @@ -2808,7 +2806,7 @@
    8.40    ultimately show ?thesis by metis
    8.41  qed
    8.42  
    8.43 -lemma sum_gp_offset: "setsum (op ^ (x::'a::{field,recpower})) {m .. m+n} =
    8.44 +lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
    8.45    (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
    8.46    unfolding sum_gp[of x m "m + n"] power_Suc
    8.47    by (simp add: ring_simps power_add)
     9.1 --- a/src/HOL/Library/Float.thy	Tue Apr 28 19:15:50 2009 +0200
     9.2 +++ b/src/HOL/Library/Float.thy	Wed Apr 29 14:20:26 2009 +0200
     9.3 @@ -443,8 +443,6 @@
     9.4  lemma Ifloat_min: "Ifloat (min x y) = min (Ifloat x) (Ifloat y)" unfolding min_def le_float_def by auto
     9.5  lemma Ifloat_max: "Ifloat (max a b) = max (Ifloat a) (Ifloat b)" unfolding max_def le_float_def by auto
     9.6  
     9.7 -instance float :: recpower ..
     9.8 -
     9.9  lemma float_power: "Ifloat (x ^ n) = Ifloat x ^ n"
    9.10    by (induct n) simp_all
    9.11  
    10.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Apr 28 19:15:50 2009 +0200
    10.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 29 14:20:26 2009 +0200
    10.3 @@ -680,8 +680,6 @@
    10.4  
    10.5  subsection {* Powers*}
    10.6  
    10.7 -instance fps :: (semiring_1) recpower ..
    10.8 -
    10.9  lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
   10.10    by (induct n, auto simp add: expand_fps_eq fps_mult_nth)
   10.11  
   10.12 @@ -701,11 +699,11 @@
   10.13  lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
   10.14    by (induct n, auto simp add: fps_mult_nth)
   10.15  
   10.16 -lemma startsby_power:"a $0 = (v::'a::{comm_ring_1, recpower}) \<Longrightarrow> a^n $0 = v^n"
   10.17 +lemma startsby_power:"a $0 = (v::'a::{comm_ring_1}) \<Longrightarrow> a^n $0 = v^n"
   10.18    by (induct n, auto simp add: fps_mult_nth power_Suc)
   10.19  
   10.20  lemma startsby_zero_power_iff[simp]:
   10.21 -  "a^n $0 = (0::'a::{idom, recpower}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
   10.22 +  "a^n $0 = (0::'a::{idom}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
   10.23  apply (rule iffI)
   10.24  apply (induct n, auto simp add: power_Suc fps_mult_nth)
   10.25  by (rule startsby_zero_power, simp_all)
   10.26 @@ -748,7 +746,7 @@
   10.27    apply (rule startsby_zero_power_prefix[rule_format, OF a0])
   10.28    by arith
   10.29  
   10.30 -lemma startsby_zero_power_nth_same: assumes a0: "a$0 = (0::'a::{recpower, idom})"
   10.31 +lemma startsby_zero_power_nth_same: assumes a0: "a$0 = (0::'a::{idom})"
   10.32    shows "a^n $ n = (a$1) ^ n"
   10.33  proof(induct n)
   10.34    case 0 thus ?case by (simp add: power_0)
   10.35 @@ -769,7 +767,7 @@
   10.36  qed
   10.37  
   10.38  lemma fps_inverse_power:
   10.39 -  fixes a :: "('a::{field, recpower}) fps"
   10.40 +  fixes a :: "('a::{field}) fps"
   10.41    shows "inverse (a^n) = inverse a ^ n"
   10.42  proof-
   10.43    {assume a0: "a$0 = 0"
   10.44 @@ -858,7 +856,7 @@
   10.45  
   10.46  subsection{* The eXtractor series X*}
   10.47  
   10.48 -lemma minus_one_power_iff: "(- (1::'a :: {recpower, comm_ring_1})) ^ n = (if even n then 1 else - 1)"
   10.49 +lemma minus_one_power_iff: "(- (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else - 1)"
   10.50    by (induct n, auto)
   10.51  
   10.52  definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
   10.53 @@ -915,7 +913,7 @@
   10.54    by (simp add: X_power_iff)
   10.55  
   10.56  lemma fps_inverse_X_plus1:
   10.57 -  "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::{recpower, field})) ^ n)" (is "_ = ?r")
   10.58 +  "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::{field})) ^ n)" (is "_ = ?r")
   10.59  proof-
   10.60    have eq: "(1 + X) * ?r = 1"
   10.61      unfolding minus_one_power_iff
   10.62 @@ -1014,7 +1012,7 @@
   10.63  
   10.64  
   10.65  lemma fps_mult_XD_shift:
   10.66 -  "(XD ^^ k) (a:: ('a::{comm_ring_1, recpower}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   10.67 +  "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   10.68    by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
   10.69  
   10.70  subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
   10.71 @@ -1296,7 +1294,7 @@
   10.72    by (cases m, simp_all add: fps_power_nth_Suc del: power_Suc)
   10.73  
   10.74  lemma fps_nth_power_0:
   10.75 -  fixes m :: nat and a :: "('a::{comm_ring_1, recpower}) fps"
   10.76 +  fixes m :: nat and a :: "('a::{comm_ring_1}) fps"
   10.77    shows "(a ^m)$0 = (a$0) ^ m"
   10.78  proof-
   10.79    {assume "m=0" hence ?thesis by simp}
   10.80 @@ -1312,7 +1310,7 @@
   10.81  qed
   10.82  
   10.83  lemma fps_compose_inj_right:
   10.84 -  assumes a0: "a$0 = (0::'a::{recpower,idom})"
   10.85 +  assumes a0: "a$0 = (0::'a::{idom})"
   10.86    and a1: "a$1 \<noteq> 0"
   10.87    shows "(b oo a = c oo a) \<longleftrightarrow> b = c" (is "?lhs \<longleftrightarrow>?rhs")
   10.88  proof-
   10.89 @@ -1353,7 +1351,7 @@
   10.90  subsection {* Radicals *}
   10.91  
   10.92  declare setprod_cong[fundef_cong]
   10.93 -function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field, recpower}) fps \<Rightarrow> nat \<Rightarrow> 'a" where
   10.94 +function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field}) fps \<Rightarrow> nat \<Rightarrow> 'a" where
   10.95    "radical r 0 a 0 = 1"
   10.96  | "radical r 0 a (Suc n) = 0"
   10.97  | "radical r (Suc k) a 0 = r (Suc k) (a$0)"
   10.98 @@ -1441,7 +1439,7 @@
   10.99  qed
  10.100  
  10.101  lemma power_radical:
  10.102 -  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
  10.103 +  fixes a:: "'a ::{field, ring_char_0} fps"
  10.104    assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0"
  10.105    shows "(fps_radical r (Suc k) a) ^ (Suc k) = a"
  10.106  proof-
  10.107 @@ -1502,7 +1500,7 @@
  10.108  
  10.109  lemma radical_unique:
  10.110    assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0"
  10.111 -  and a0: "r (Suc k) (b$0 ::'a::{field, ring_char_0, recpower}) = a$0" and b0: "b$0 \<noteq> 0"
  10.112 +  and a0: "r (Suc k) (b$0 ::'a::{field, ring_char_0}) = a$0" and b0: "b$0 \<noteq> 0"
  10.113    shows "a^(Suc k) = b \<longleftrightarrow> a = fps_radical r (Suc k) b"
  10.114  proof-
  10.115    let ?r = "fps_radical r (Suc k) b"
  10.116 @@ -1597,7 +1595,7 @@
  10.117  
  10.118  lemma radical_power:
  10.119    assumes r0: "r (Suc k) ((a$0) ^ Suc k) = a$0"
  10.120 -  and a0: "(a$0 ::'a::{field, ring_char_0, recpower}) \<noteq> 0"
  10.121 +  and a0: "(a$0 ::'a::{field, ring_char_0}) \<noteq> 0"
  10.122    shows "(fps_radical r (Suc k) (a ^ Suc k)) = a"
  10.123  proof-
  10.124    let ?ak = "a^ Suc k"
  10.125 @@ -1609,7 +1607,7 @@
  10.126  qed
  10.127  
  10.128  lemma fps_deriv_radical:
  10.129 -  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
  10.130 +  fixes a:: "'a ::{field, ring_char_0} fps"
  10.131    assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0"
  10.132    shows "fps_deriv (fps_radical r (Suc k) a) = fps_deriv a / (fps_const (of_nat (Suc k)) * (fps_radical r (Suc k) a) ^ k)"
  10.133  proof-
  10.134 @@ -1630,7 +1628,7 @@
  10.135  qed
  10.136  
  10.137  lemma radical_mult_distrib:
  10.138 -  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
  10.139 +  fixes a:: "'a ::{field, ring_char_0} fps"
  10.140    assumes
  10.141    ra0: "r (k) (a $ 0) ^ k = a $ 0"
  10.142    and rb0: "r (k) (b $ 0) ^ k = b $ 0"
  10.143 @@ -1656,7 +1654,7 @@
  10.144  qed
  10.145  
  10.146  lemma radical_inverse:
  10.147 -  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
  10.148 +  fixes a:: "'a ::{field, ring_char_0} fps"
  10.149    assumes
  10.150    ra0: "r (k) (a $ 0) ^ k = a $ 0"
  10.151    and ria0: "r (k) (inverse (a $ 0)) = inverse (r (k) (a $ 0))"
  10.152 @@ -1698,7 +1696,7 @@
  10.153    by (simp add: fps_divide_def)
  10.154  
  10.155  lemma radical_divide:
  10.156 -  fixes a:: "'a ::{field, ring_char_0, recpower} fps"
  10.157 +  fixes a:: "'a ::{field, ring_char_0} fps"
  10.158    assumes
  10.159        ra0: "r k (a $ 0) ^ k = a $ 0"
  10.160    and rb0: "r k (b $ 0) ^ k = b $ 0"
  10.161 @@ -1818,7 +1816,7 @@
  10.162  subsection{* Compositional inverses *}
  10.163  
  10.164  
  10.165 -fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{recpower,field}" where
  10.166 +fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}" where
  10.167    "compinv a 0 = X$0"
  10.168  | "compinv a (Suc n) = (X$ Suc n - setsum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
  10.169  
  10.170 @@ -1849,7 +1847,7 @@
  10.171  qed
  10.172  
  10.173  
  10.174 -fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{recpower,field}" where
  10.175 +fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}" where
  10.176    "gcompinv b a 0 = b$0"
  10.177  | "gcompinv b a (Suc n) = (b$ Suc n - setsum (\<lambda>i. (gcompinv b a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
  10.178  
  10.179 @@ -2102,7 +2100,7 @@
  10.180  qed
  10.181  
  10.182  lemma fps_inv_deriv:
  10.183 -  assumes a0:"a$0 = (0::'a::{recpower,field})" and a1: "a$1 \<noteq> 0"
  10.184 +  assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \<noteq> 0"
  10.185    shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)"
  10.186  proof-
  10.187    let ?ia = "fps_inv a"
  10.188 @@ -2122,7 +2120,7 @@
  10.189  subsubsection{* Exponential series *}
  10.190  definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
  10.191  
  10.192 -lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, recpower, ring_char_0}) * E a" (is "?l = ?r")
  10.193 +lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, ring_char_0}) * E a" (is "?l = ?r")
  10.194  proof-
  10.195    {fix n
  10.196      have "?l$n = ?r $ n"
  10.197 @@ -2132,7 +2130,7 @@
  10.198  qed
  10.199  
  10.200  lemma E_unique_ODE:
  10.201 -  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::{field, ring_char_0, recpower})"
  10.202 +  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::{field, ring_char_0})"
  10.203    (is "?lhs \<longleftrightarrow> ?rhs")
  10.204  proof-
  10.205    {assume d: ?lhs
  10.206 @@ -2159,7 +2157,7 @@
  10.207  ultimately show ?thesis by blast
  10.208  qed
  10.209  
  10.210 -lemma E_add_mult: "E (a + b) = E (a::'a::{ring_char_0, field, recpower}) * E b" (is "?l = ?r")
  10.211 +lemma E_add_mult: "E (a + b) = E (a::'a::{ring_char_0, field}) * E b" (is "?l = ?r")
  10.212  proof-
  10.213    have "fps_deriv (?r) = fps_const (a+b) * ?r"
  10.214      by (simp add: fps_const_add[symmetric] ring_simps del: fps_const_add)
  10.215 @@ -2171,10 +2169,10 @@
  10.216  lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)"
  10.217    by (simp add: E_def)
  10.218  
  10.219 -lemma E0[simp]: "E (0::'a::{field, recpower}) = 1"
  10.220 +lemma E0[simp]: "E (0::'a::{field}) = 1"
  10.221    by (simp add: fps_eq_iff power_0_left)
  10.222  
  10.223 -lemma E_neg: "E (- a) = inverse (E (a::'a::{ring_char_0, field, recpower}))"
  10.224 +lemma E_neg: "E (- a) = inverse (E (a::'a::{ring_char_0, field}))"
  10.225  proof-
  10.226    from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1"
  10.227      by (simp )
  10.228 @@ -2182,7 +2180,7 @@
  10.229    from fps_inverse_unique[OF th1 th0] show ?thesis by simp
  10.230  qed
  10.231  
  10.232 -lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, recpower, ring_char_0})) = (fps_const a)^n * (E a)"
  10.233 +lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, ring_char_0})) = (fps_const a)^n * (E a)"
  10.234    by (induct n, auto simp add: power_Suc)
  10.235  
  10.236  lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
  10.237 @@ -2195,7 +2193,7 @@
  10.238  lemma X_fps_compose:"X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
  10.239    by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc)
  10.240  
  10.241 -lemma X_compose_E[simp]: "X oo E (a::'a::{field, recpower}) = E a - 1"
  10.242 +lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
  10.243    by (simp add: fps_eq_iff X_fps_compose)
  10.244  
  10.245  lemma LE_compose:
  10.246 @@ -2217,7 +2215,7 @@
  10.247  
  10.248  
  10.249  lemma inverse_one_plus_X:
  10.250 -  "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field, recpower})^n)"
  10.251 +  "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field})^n)"
  10.252    (is "inverse ?l = ?r")
  10.253  proof-
  10.254    have th: "?l * ?r = 1"
  10.255 @@ -2228,11 +2226,11 @@
  10.256    from fps_inverse_unique[OF th' th] show ?thesis .
  10.257  qed
  10.258  
  10.259 -lemma E_power_mult: "(E (c::'a::{field,recpower,ring_char_0}))^n = E (of_nat n * c)"
  10.260 +lemma E_power_mult: "(E (c::'a::{field,ring_char_0}))^n = E (of_nat n * c)"
  10.261    by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
  10.262  
  10.263  subsubsection{* Logarithmic series *}
  10.264 -definition "(L::'a::{field, ring_char_0,recpower} fps)
  10.265 +definition "(L::'a::{field, ring_char_0} fps)
  10.266    = Abs_fps (\<lambda>n. (- 1) ^ Suc n / of_nat n)"
  10.267  
  10.268  lemma fps_deriv_L: "fps_deriv L = inverse (1 + X)"
  10.269 @@ -2243,7 +2241,7 @@
  10.270    by (simp add: L_def)
  10.271  
  10.272  lemma L_E_inv:
  10.273 -  assumes a: "a\<noteq> (0::'a::{field,division_by_zero,ring_char_0,recpower})"
  10.274 +  assumes a: "a\<noteq> (0::'a::{field,division_by_zero,ring_char_0})"
  10.275    shows "L = fps_const a * fps_inv (E a - 1)" (is "?l = ?r")
  10.276  proof-
  10.277    let ?b = "E a - 1"
  10.278 @@ -2267,10 +2265,10 @@
  10.279  
  10.280  subsubsection{* Formal trigonometric functions  *}
  10.281  
  10.282 -definition "fps_sin (c::'a::{field, recpower, ring_char_0}) =
  10.283 +definition "fps_sin (c::'a::{field, ring_char_0}) =
  10.284    Abs_fps (\<lambda>n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))"
  10.285  
  10.286 -definition "fps_cos (c::'a::{field, recpower, ring_char_0}) = Abs_fps (\<lambda>n. if even n then (- 1) ^ (n div 2) * c^n / (of_nat (fact n)) else 0)"
  10.287 +definition "fps_cos (c::'a::{field, ring_char_0}) = Abs_fps (\<lambda>n. if even n then (- 1) ^ (n div 2) * c^n / (of_nat (fact n)) else 0)"
  10.288  
  10.289  lemma fps_sin_deriv:
  10.290    "fps_deriv (fps_sin c) = fps_const c * fps_cos c"
    11.1 --- a/src/HOL/Library/FrechetDeriv.thy	Tue Apr 28 19:15:50 2009 +0200
    11.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Wed Apr 29 14:20:26 2009 +0200
    11.3 @@ -382,7 +382,7 @@
    11.4  subsection {* Powers *}
    11.5  
    11.6  lemma FDERIV_power_Suc:
    11.7 -  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
    11.8 +  fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
    11.9    shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
   11.10   apply (induct n)
   11.11    apply (simp add: power_Suc FDERIV_ident)
   11.12 @@ -392,7 +392,7 @@
   11.13  done
   11.14  
   11.15  lemma FDERIV_power:
   11.16 -  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
   11.17 +  fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
   11.18    shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
   11.19    apply (cases n)
   11.20     apply (simp add: FDERIV_const)
    12.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 28 19:15:50 2009 +0200
    12.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Apr 29 14:20:26 2009 +0200
    12.3 @@ -560,14 +560,14 @@
    12.4    done
    12.5  
    12.6  lemma poly_replicate_append:
    12.7 -  "poly (monom 1 n * p) (x::'a::{recpower, comm_ring_1}) = x^n * poly p x"
    12.8 +  "poly (monom 1 n * p) (x::'a::{comm_ring_1}) = x^n * poly p x"
    12.9    by (simp add: poly_monom)
   12.10  
   12.11  text {* Decomposition of polynomial, skipping zero coefficients
   12.12    after the first.  *}
   12.13  
   12.14  lemma poly_decompose_lemma:
   12.15 - assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
   12.16 + assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{idom}))"
   12.17    shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and>
   12.18                   (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
   12.19  unfolding psize_def
   12.20 @@ -595,7 +595,7 @@
   12.21  
   12.22  lemma poly_decompose:
   12.23    assumes nc: "~constant(poly p)"
   12.24 -  shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
   12.25 +  shows "\<exists>k a q. a\<noteq>(0::'a::{idom}) \<and> k\<noteq>0 \<and>
   12.26                 psize q + k + 1 = psize p \<and>
   12.27                (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
   12.28  using nc
    13.1 --- a/src/HOL/Library/Numeral_Type.thy	Tue Apr 28 19:15:50 2009 +0200
    13.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Apr 29 14:20:26 2009 +0200
    13.3 @@ -216,12 +216,6 @@
    13.4  apply (simp_all add: Rep_simps zmod_simps ring_simps)
    13.5  done
    13.6  
    13.7 -lemma recpower: "OFCLASS('a, recpower_class)"
    13.8 -apply (intro_classes, unfold definitions)
    13.9 -apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc
   13.10 -                     mod_pos_pos_trivial size1)
   13.11 -done
   13.12 -
   13.13  end
   13.14  
   13.15  locale mod_ring = mod_type +
   13.16 @@ -340,11 +334,11 @@
   13.17  apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
   13.18  done
   13.19  
   13.20 -instance bit0 :: (finite) "{comm_ring_1,recpower}"
   13.21 -  by (rule bit0.comm_ring_1 bit0.recpower)+
   13.22 +instance bit0 :: (finite) comm_ring_1
   13.23 +  by (rule bit0.comm_ring_1)+
   13.24  
   13.25 -instance bit1 :: (finite) "{comm_ring_1,recpower}"
   13.26 -  by (rule bit1.comm_ring_1 bit1.recpower)+
   13.27 +instance bit1 :: (finite) comm_ring_1
   13.28 +  by (rule bit1.comm_ring_1)+
   13.29  
   13.30  instantiation bit0 and bit1 :: (finite) number_ring
   13.31  begin
    14.1 --- a/src/HOL/Library/Pocklington.thy	Tue Apr 28 19:15:50 2009 +0200
    14.2 +++ b/src/HOL/Library/Pocklington.thy	Wed Apr 29 14:20:26 2009 +0200
    14.3 @@ -568,7 +568,7 @@
    14.4  
    14.5  lemma nproduct_cmul:
    14.6    assumes fS:"finite S"
    14.7 -  shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult,recpower})* a(m)) S = c ^ (card S) * setprod a S"
    14.8 +  shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S"
    14.9  unfolding setprod_timesf setprod_constant[OF fS, of c] ..
   14.10  
   14.11  lemma coprime_nproduct:
    15.1 --- a/src/HOL/Library/Polynomial.thy	Tue Apr 28 19:15:50 2009 +0200
    15.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Apr 29 14:20:26 2009 +0200
    15.3 @@ -632,8 +632,6 @@
    15.4    shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
    15.5    by (safe elim!: dvd_smult dvd_smult_cancel)
    15.6  
    15.7 -instance poly :: (comm_semiring_1) recpower ..
    15.8 -
    15.9  lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
   15.10  by (induct n, simp, auto intro: order_trans degree_mult_le)
   15.11  
   15.12 @@ -1120,7 +1118,7 @@
   15.13    unfolding one_poly_def by simp
   15.14  
   15.15  lemma poly_monom:
   15.16 -  fixes a x :: "'a::{comm_semiring_1,recpower}"
   15.17 +  fixes a x :: "'a::{comm_semiring_1}"
   15.18    shows "poly (monom a n) x = a * x ^ n"
   15.19    by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
   15.20  
   15.21 @@ -1149,7 +1147,7 @@
   15.22    by (induct p, simp_all, simp add: algebra_simps)
   15.23  
   15.24  lemma poly_power [simp]:
   15.25 -  fixes p :: "'a::{comm_semiring_1,recpower} poly"
   15.26 +  fixes p :: "'a::{comm_semiring_1} poly"
   15.27    shows "poly (p ^ n) x = poly p x ^ n"
   15.28    by (induct n, simp, simp add: power_Suc)
   15.29  
    16.1 --- a/src/HOL/Library/Univ_Poly.thy	Tue Apr 28 19:15:50 2009 +0200
    16.2 +++ b/src/HOL/Library/Univ_Poly.thy	Wed Apr 29 14:20:26 2009 +0200
    16.3 @@ -167,22 +167,9 @@
    16.4      simp_all add: poly_cmult poly_add left_distrib right_distrib mult_ac)
    16.5  qed
    16.6  
    16.7 -class recpower_semiring = semiring + recpower
    16.8 -class recpower_semiring_1 = semiring_1 + recpower
    16.9 -class recpower_semiring_0 = semiring_0 + recpower
   16.10 -class recpower_ring = ring + recpower
   16.11 -class recpower_ring_1 = ring_1 + recpower
   16.12 -subclass (in recpower_ring_1) recpower_ring ..
   16.13 -class recpower_comm_semiring_1 = recpower + comm_semiring_1
   16.14 -class recpower_comm_ring_1 = recpower + comm_ring_1
   16.15 -subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 ..
   16.16 -class recpower_idom = recpower + idom
   16.17 -subclass (in recpower_idom) recpower_comm_ring_1 ..
   16.18  class idom_char_0 = idom + ring_char_0
   16.19 -class recpower_idom_char_0 = recpower + idom_char_0
   16.20 -subclass (in recpower_idom_char_0) recpower_idom ..
   16.21  
   16.22 -lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
   16.23 +lemma (in comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
   16.24  apply (induct "n")
   16.25  apply (auto simp add: poly_cmult poly_mult power_Suc)
   16.26  done
   16.27 @@ -418,7 +405,7 @@
   16.28    finally show ?thesis .
   16.29  qed
   16.30  
   16.31 -lemma (in recpower_idom) poly_exp_eq_zero[simp]:
   16.32 +lemma (in idom) poly_exp_eq_zero[simp]:
   16.33       "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
   16.34  apply (simp only: fun_eq add: all_simps [symmetric])
   16.35  apply (rule arg_cong [where f = All])
   16.36 @@ -437,7 +424,7 @@
   16.37  apply simp
   16.38  done
   16.39  
   16.40 -lemma (in recpower_idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
   16.41 +lemma (in idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
   16.42  by auto
   16.43  
   16.44  text{*A more constructive notion of polynomials being trivial*}
   16.45 @@ -507,7 +494,7 @@
   16.46  done
   16.47  
   16.48  
   16.49 -lemma (in recpower_comm_semiring_1) poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
   16.50 +lemma (in comm_semiring_1) poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
   16.51  apply (auto simp add: le_iff_add)
   16.52  apply (induct_tac k)
   16.53  apply (rule_tac [2] poly_divides_trans)
   16.54 @@ -516,7 +503,7 @@
   16.55  apply (auto simp add: poly_mult fun_eq mult_ac)
   16.56  done
   16.57  
   16.58 -lemma (in recpower_comm_semiring_1) poly_exp_divides: "[| (p %^ n) divides q;  m\<le>n |] ==> (p %^ m) divides q"
   16.59 +lemma (in comm_semiring_1) poly_exp_divides: "[| (p %^ n) divides q;  m\<le>n |] ==> (p %^ m) divides q"
   16.60  by (blast intro: poly_divides_exp poly_divides_trans)
   16.61  
   16.62  lemma (in comm_semiring_0) poly_divides_add:
   16.63 @@ -583,7 +570,7 @@
   16.64  qed
   16.65  
   16.66  
   16.67 -lemma (in recpower_comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
   16.68 +lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
   16.69  by(induct n, auto simp add: poly_mult power_Suc mult_ac)
   16.70  
   16.71  lemma (in comm_semiring_1) divides_left_mult:
   16.72 @@ -600,11 +587,11 @@
   16.73  
   16.74  (* FIXME: Tidy up *)
   16.75  
   16.76 -lemma (in recpower_semiring_1)
   16.77 +lemma (in semiring_1)
   16.78    zero_power_iff: "0 ^ n = (if n = 0 then 1 else 0)"
   16.79    by (induct n, simp_all add: power_Suc)
   16.80  
   16.81 -lemma (in recpower_idom_char_0) poly_order_exists:
   16.82 +lemma (in idom_char_0) poly_order_exists:
   16.83    assumes lp: "length p = d" and p0: "poly p \<noteq> poly []"
   16.84    shows "\<exists>n. ([-a, 1] %^ n) divides p & ~(([-a, 1] %^ (Suc n)) divides p)"
   16.85  proof-
   16.86 @@ -637,7 +624,7 @@
   16.87  lemma (in semiring_1) poly_one_divides[simp]: "[1] divides p"
   16.88  by (simp add: divides_def, auto)
   16.89  
   16.90 -lemma (in recpower_idom_char_0) poly_order: "poly p \<noteq> poly []
   16.91 +lemma (in idom_char_0) poly_order: "poly p \<noteq> poly []
   16.92        ==> EX! n. ([-a, 1] %^ n) divides p &
   16.93                   ~(([-a, 1] %^ (Suc n)) divides p)"
   16.94  apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
   16.95 @@ -652,7 +639,7 @@
   16.96  lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n"
   16.97  by (blast intro: someI2)
   16.98  
   16.99 -lemma (in recpower_idom_char_0) order:
  16.100 +lemma (in idom_char_0) order:
  16.101        "(([-a, 1] %^ n) divides p &
  16.102          ~(([-a, 1] %^ (Suc n)) divides p)) =
  16.103          ((n = order a p) & ~(poly p = poly []))"
  16.104 @@ -662,17 +649,17 @@
  16.105  apply (blast intro!: poly_order [THEN [2] some1_equalityD])
  16.106  done
  16.107  
  16.108 -lemma (in recpower_idom_char_0) order2: "[| poly p \<noteq> poly [] |]
  16.109 +lemma (in idom_char_0) order2: "[| poly p \<noteq> poly [] |]
  16.110        ==> ([-a, 1] %^ (order a p)) divides p &
  16.111                ~(([-a, 1] %^ (Suc(order a p))) divides p)"
  16.112  by (simp add: order del: pexp_Suc)
  16.113  
  16.114 -lemma (in recpower_idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
  16.115 +lemma (in idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
  16.116           ~(([-a, 1] %^ (Suc n)) divides p)
  16.117        |] ==> (n = order a p)"
  16.118  by (insert order [of a n p], auto)
  16.119  
  16.120 -lemma (in recpower_idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
  16.121 +lemma (in idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
  16.122           ~(([-a, 1] %^ (Suc n)) divides p))
  16.123        ==> (n = order a p)"
  16.124  by (blast intro: order_unique)
  16.125 @@ -692,7 +679,7 @@
  16.126  apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
  16.127  done
  16.128  
  16.129 -lemma (in recpower_idom_char_0) order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
  16.130 +lemma (in idom_char_0) order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
  16.131  proof-
  16.132    let ?poly = poly
  16.133    show ?thesis
  16.134 @@ -706,7 +693,7 @@
  16.135  done
  16.136  qed
  16.137  
  16.138 -lemma (in recpower_idom_char_0) order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
  16.139 +lemma (in idom_char_0) order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
  16.140  proof-
  16.141    let ?poly = poly
  16.142    show ?thesis
  16.143 @@ -718,7 +705,7 @@
  16.144  done
  16.145  qed
  16.146  
  16.147 -lemma (in recpower_idom_char_0) order_decomp:
  16.148 +lemma (in idom_char_0) order_decomp:
  16.149       "poly p \<noteq> poly []
  16.150        ==> \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) &
  16.151                  ~([-a, 1] divides q)"
  16.152 @@ -732,7 +719,7 @@
  16.153  
  16.154  text{*Important composition properties of orders.*}
  16.155  lemma order_mult: "poly (p *** q) \<noteq> poly []
  16.156 -      ==> order a (p *** q) = order a p + order (a::'a::{recpower_idom_char_0}) q"
  16.157 +      ==> order a (p *** q) = order a p + order (a::'a::{idom_char_0}) q"
  16.158  apply (cut_tac a = a and p = "p *** q" and n = "order a p + order a q" in order)
  16.159  apply (auto simp add: poly_entire simp del: pmult_Cons)
  16.160  apply (drule_tac a = a in order2)+
  16.161 @@ -753,7 +740,7 @@
  16.162  apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
  16.163  done
  16.164  
  16.165 -lemma (in recpower_idom_char_0) order_mult:
  16.166 +lemma (in idom_char_0) order_mult:
  16.167    assumes pq0: "poly (p *** q) \<noteq> poly []"
  16.168    shows "order a (p *** q) = order a p + order a q"
  16.169  proof-
  16.170 @@ -783,7 +770,7 @@
  16.171  done
  16.172  qed
  16.173  
  16.174 -lemma (in recpower_idom_char_0) order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
  16.175 +lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
  16.176  by (rule order_root [THEN ssubst], auto)
  16.177  
  16.178  lemma (in semiring_1) pmult_one[simp]: "[1] *** p = p" by auto
  16.179 @@ -791,7 +778,7 @@
  16.180  lemma (in semiring_0) poly_Nil_zero: "poly [] = poly [0]"
  16.181  by (simp add: fun_eq)
  16.182  
  16.183 -lemma (in recpower_idom_char_0) rsquarefree_decomp:
  16.184 +lemma (in idom_char_0) rsquarefree_decomp:
  16.185       "[| rsquarefree p; poly p a = 0 |]
  16.186        ==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0"
  16.187  apply (simp add: rsquarefree_def, safe)
  16.188 @@ -999,7 +986,7 @@
  16.189    ultimately show ?case by blast
  16.190  qed
  16.191  
  16.192 -lemma (in recpower_idom_char_0) order_degree:
  16.193 +lemma (in idom_char_0) order_degree:
  16.194    assumes p0: "poly p \<noteq> poly []"
  16.195    shows "order a p \<le> degree p"
  16.196  proof-
    17.1 --- a/src/HOL/Library/comm_ring.ML	Tue Apr 28 19:15:50 2009 +0200
    17.2 +++ b/src/HOL/Library/comm_ring.ML	Wed Apr 29 14:20:26 2009 +0200
    17.3 @@ -65,7 +65,7 @@
    17.4    | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
    17.5  
    17.6  (* reification of the equation *)
    17.7 -val TFree (_, cr_sort) = @{typ "'a :: {comm_ring, recpower}"};
    17.8 +val cr_sort = @{sort "comm_ring_1"};
    17.9  
   17.10  fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
   17.11        if Sign.of_sort thy (T, cr_sort) then
    18.1 --- a/src/HOL/NSA/StarDef.thy	Tue Apr 28 19:15:50 2009 +0200
    18.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Apr 29 14:20:26 2009 +0200
    18.3 @@ -954,8 +954,6 @@
    18.4  
    18.5  subsection {* Power *}
    18.6  
    18.7 -instance star :: (recpower) recpower ..
    18.8 -
    18.9  lemma star_power_def [transfer_unfold]:
   18.10    "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
   18.11  proof (rule eq_reflection, rule ext, rule ext)
    19.1 --- a/src/HOL/Power.thy	Tue Apr 28 19:15:50 2009 +0200
    19.2 +++ b/src/HOL/Power.thy	Wed Apr 29 14:20:26 2009 +0200
    19.3 @@ -419,13 +419,9 @@
    19.4  apply assumption
    19.5  done
    19.6  
    19.7 -class recpower = monoid_mult
    19.8 -
    19.9  
   19.10  subsection {* Exponentiation for the Natural Numbers *}
   19.11  
   19.12 -instance nat :: recpower ..
   19.13 -
   19.14  lemma nat_one_le_power [simp]:
   19.15    "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
   19.16    by (rule one_le_power [of i n, unfolded One_nat_def])
    20.1 --- a/src/HOL/Rational.thy	Tue Apr 28 19:15:50 2009 +0200
    20.2 +++ b/src/HOL/Rational.thy	Wed Apr 29 14:20:26 2009 +0200
    20.3 @@ -834,8 +834,6 @@
    20.4    "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
    20.5    by (rule Rats_cases) auto
    20.6  
    20.7 -instance rat :: recpower ..
    20.8 -
    20.9  
   20.10  subsection {* Implementation of rational numbers as pairs of integers *}
   20.11  
    21.1 --- a/src/HOL/RealPow.thy	Tue Apr 28 19:15:50 2009 +0200
    21.2 +++ b/src/HOL/RealPow.thy	Wed Apr 29 14:20:26 2009 +0200
    21.3 @@ -12,8 +12,6 @@
    21.4  
    21.5  declare abs_mult_self [simp]
    21.6  
    21.7 -instance real :: recpower ..
    21.8 -
    21.9  lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
   21.10  by simp
   21.11  
    22.1 --- a/src/HOL/SizeChange/Graphs.thy	Tue Apr 28 19:15:50 2009 +0200
    22.2 +++ b/src/HOL/SizeChange/Graphs.thy	Wed Apr 29 14:20:26 2009 +0200
    22.3 @@ -228,7 +228,7 @@
    22.4    qed
    22.5  qed
    22.6  
    22.7 -instance graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower}"
    22.8 +instance graph :: (type, monoid_mult) "{semiring_1, idem_add}"
    22.9  proof
   22.10    fix a b c :: "('a, 'b) graph"
   22.11    
    23.1 --- a/src/HOL/SizeChange/Kleene_Algebras.thy	Tue Apr 28 19:15:50 2009 +0200
    23.2 +++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Apr 29 14:20:26 2009 +0200
    23.3 @@ -97,7 +97,7 @@
    23.4    and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
    23.5  
    23.6  class kleene_by_complete_lattice = pre_kleene
    23.7 -  + complete_lattice + recpower + star +
    23.8 +  + complete_lattice + power + star +
    23.9    assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
   23.10  begin
   23.11  
    24.1 --- a/src/HOL/Word/WordArith.thy	Tue Apr 28 19:15:50 2009 +0200
    24.2 +++ b/src/HOL/Word/WordArith.thy	Wed Apr 29 14:20:26 2009 +0200
    24.3 @@ -778,8 +778,6 @@
    24.4    apply (simp add: word_mult_1)
    24.5    done
    24.6  
    24.7 -instance word :: (len0) recpower ..
    24.8 -
    24.9  instance word :: (len0) comm_semiring 
   24.10    by (intro_classes) (simp add : word_left_distrib)
   24.11  
   24.12 @@ -790,8 +788,6 @@
   24.13  instance word :: (len) comm_semiring_1 
   24.14    by (intro_classes) (simp add: lenw1_zero_neq_one)
   24.15  
   24.16 -instance word :: (len) recpower ..
   24.17 -
   24.18  instance word :: (len) comm_ring_1 ..
   24.19  
   24.20  instance word :: (len0) comm_semiring_0 ..
    25.1 --- a/src/HOL/ex/Commutative_Ring_Complete.thy	Tue Apr 28 19:15:50 2009 +0200
    25.2 +++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Apr 29 14:20:26 2009 +0200
    25.3 @@ -1,5 +1,4 @@
    25.4 -(*  ID:         $Id$
    25.5 -    Author:     Bernhard Haeupler
    25.6 +(*  Author:     Bernhard Haeupler
    25.7  
    25.8  This theory is about of the relative completeness of method comm-ring
    25.9  method.  As long as the reified atomic polynomials of type 'a pol are
   25.10 @@ -14,7 +13,7 @@
   25.11  
   25.12  text {* Formalization of normal form *}
   25.13  fun
   25.14 -  isnorm :: "('a::{comm_ring,recpower}) pol \<Rightarrow> bool"
   25.15 +  isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool"
   25.16  where
   25.17      "isnorm (Pc c) \<longleftrightarrow> True"
   25.18    | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
    26.1 --- a/src/HOL/ex/Formal_Power_Series_Examples.thy	Tue Apr 28 19:15:50 2009 +0200
    26.2 +++ b/src/HOL/ex/Formal_Power_Series_Examples.thy	Wed Apr 29 14:20:26 2009 +0200
    26.3 @@ -11,7 +11,7 @@
    26.4  
    26.5  section{* The generalized binomial theorem *}
    26.6  lemma gbinomial_theorem: 
    26.7 -  "((a::'a::{ring_char_0, field, division_by_zero, recpower})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
    26.8 +  "((a::'a::{ring_char_0, field, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
    26.9  proof-
   26.10    from E_add_mult[of a b] 
   26.11    have "(E (a + b)) $ n = (E a * E b)$n" by simp
   26.12 @@ -38,7 +38,7 @@
   26.13    by (simp add: fps_binomial_def)
   26.14  
   26.15  lemma fps_binomial_ODE_unique:
   26.16 -  fixes c :: "'a::{field, recpower,ring_char_0}"
   26.17 +  fixes c :: "'a::{field, ring_char_0}"
   26.18    shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
   26.19    (is "?lhs \<longleftrightarrow> ?rhs")
   26.20  proof-
    27.1 --- a/src/HOL/ex/Groebner_Examples.thy	Tue Apr 28 19:15:50 2009 +0200
    27.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Wed Apr 29 14:20:26 2009 +0200
    27.3 @@ -1,5 +1,4 @@
    27.4  (*  Title:      HOL/ex/Groebner_Examples.thy
    27.5 -    ID:         $Id$
    27.6      Author:     Amine Chaieb, TU Muenchen
    27.7  *)
    27.8  
    27.9 @@ -11,7 +10,7 @@
   27.10  
   27.11  subsection {* Basic examples *}
   27.12  
   27.13 -lemma "3 ^ 3 == (?X::'a::{number_ring,recpower})"
   27.14 +lemma "3 ^ 3 == (?X::'a::{number_ring})"
   27.15    by sring_norm
   27.16  
   27.17  lemma "(x - (-2))^5 == ?X::int"
   27.18 @@ -20,7 +19,7 @@
   27.19  lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
   27.20    by sring_norm
   27.21  
   27.22 -lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring,recpower})"
   27.23 +lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
   27.24    apply (simp only: power_Suc power_0)
   27.25    apply (simp only: comp_arith)
   27.26    oops
   27.27 @@ -47,7 +46,7 @@
   27.28    by algebra
   27.29  
   27.30  lemma
   27.31 -  fixes x::"'a::{idom,recpower,number_ring}"
   27.32 +  fixes x::"'a::{idom,number_ring}"
   27.33    shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
   27.34    by algebra
   27.35  
   27.36 @@ -58,7 +57,7 @@
   27.37    "sq x == x*x"
   27.38  
   27.39  lemma
   27.40 -  fixes x1 :: "'a::{idom,recpower,number_ring}"
   27.41 +  fixes x1 :: "'a::{idom,number_ring}"
   27.42    shows
   27.43    "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
   27.44      sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
   27.45 @@ -68,7 +67,7 @@
   27.46    by (algebra add: sq_def)
   27.47  
   27.48  lemma
   27.49 -  fixes p1 :: "'a::{idom,recpower,number_ring}"
   27.50 +  fixes p1 :: "'a::{idom,number_ring}"
   27.51    shows
   27.52    "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
   27.53     (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
    28.1 --- a/src/HOL/ex/Numeral.thy	Tue Apr 28 19:15:50 2009 +0200
    28.2 +++ b/src/HOL/ex/Numeral.thy	Wed Apr 29 14:20:26 2009 +0200
    28.3 @@ -14,25 +14,19 @@
    28.4  
    28.5  text {* Increment function for type @{typ num} *}
    28.6  
    28.7 -primrec
    28.8 -  inc :: "num \<Rightarrow> num"
    28.9 -where
   28.10 +primrec inc :: "num \<Rightarrow> num" where
   28.11    "inc One = Dig0 One"
   28.12  | "inc (Dig0 x) = Dig1 x"
   28.13  | "inc (Dig1 x) = Dig0 (inc x)"
   28.14  
   28.15  text {* Converting between type @{typ num} and type @{typ nat} *}
   28.16  
   28.17 -primrec
   28.18 -  nat_of_num :: "num \<Rightarrow> nat"
   28.19 -where
   28.20 +primrec nat_of_num :: "num \<Rightarrow> nat" where
   28.21    "nat_of_num One = Suc 0"
   28.22  | "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x"
   28.23  | "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)"
   28.24  
   28.25 -primrec
   28.26 -  num_of_nat :: "nat \<Rightarrow> num"
   28.27 -where
   28.28 +primrec num_of_nat :: "nat \<Rightarrow> num" where
   28.29    "num_of_nat 0 = One"
   28.30  | "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
   28.31  
   28.32 @@ -719,32 +713,32 @@
   28.33     (simp_all add: of_num.simps of_num_plus [symmetric] algebra_simps)
   28.34  
   28.35  lemma of_num_pow:
   28.36 -  "(of_num (pow x y)::'a::{semiring_numeral,recpower}) = of_num x ^ of_num y"
   28.37 +  "(of_num (pow x y)::'a::{semiring_numeral}) = of_num x ^ of_num y"
   28.38  by (induct y)
   28.39     (simp_all add: of_num.simps of_num_square of_num_times [symmetric]
   28.40                    power_Suc power_add)
   28.41  
   28.42  lemma power_of_num [numeral]:
   28.43 -  "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral,recpower})"
   28.44 +  "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral})"
   28.45    by (rule of_num_pow [symmetric])
   28.46  
   28.47  lemma power_zero_of_num [numeral]:
   28.48 -  "0 ^ of_num n = (0::'a::{semiring_0,recpower})"
   28.49 +  "0 ^ of_num n = (0::'a::{semiring_0,power})"
   28.50    using of_num_pos [where n=n and ?'a=nat]
   28.51    by (simp add: power_0_left)
   28.52  
   28.53  lemma power_minus_one_double:
   28.54 -  "(- 1) ^ (n + n) = (1::'a::{ring_1,recpower})"
   28.55 +  "(- 1) ^ (n + n) = (1::'a::{ring_1})"
   28.56    by (induct n) (simp_all add: power_Suc)
   28.57  
   28.58  lemma power_minus_Dig0 [numeral]:
   28.59 -  fixes x :: "'a::{ring_1,recpower}"
   28.60 +  fixes x :: "'a::{ring_1}"
   28.61    shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)"
   28.62    by (subst power_minus)
   28.63       (simp add: of_num.simps power_minus_one_double)
   28.64  
   28.65  lemma power_minus_Dig1 [numeral]:
   28.66 -  fixes x :: "'a::{ring_1,recpower}"
   28.67 +  fixes x :: "'a::{ring_1}"
   28.68    shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))"
   28.69    by (subst power_minus)
   28.70       (simp add: of_num.simps power_Suc power_minus_one_double)
    29.1 --- a/src/HOL/ex/ReflectionEx.thy	Tue Apr 28 19:15:50 2009 +0200
    29.2 +++ b/src/HOL/ex/ReflectionEx.thy	Wed Apr 29 14:20:26 2009 +0200
    29.3 @@ -385,7 +385,7 @@
    29.4    (* An example for equations containing type variables *)	
    29.5  datatype prod = Zero | One | Var nat | Mul prod prod 
    29.6    | Pw prod nat | PNM nat nat prod
    29.7 -consts Iprod :: " prod \<Rightarrow> ('a::{ordered_idom,recpower}) list \<Rightarrow>'a" 
    29.8 +consts Iprod :: " prod \<Rightarrow> ('a::{ordered_idom}) list \<Rightarrow>'a" 
    29.9  primrec
   29.10    "Iprod Zero vs = 0"
   29.11    "Iprod One vs = 1"
   29.12 @@ -397,7 +397,7 @@
   29.13  datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   29.14    | Or sgn sgn | And sgn sgn
   29.15  
   29.16 -consts Isgn :: " sgn \<Rightarrow> ('a::{ordered_idom, recpower}) list \<Rightarrow>bool"
   29.17 +consts Isgn :: " sgn \<Rightarrow> ('a::{ordered_idom}) list \<Rightarrow>bool"
   29.18  primrec 
   29.19    "Isgn Tr vs = True"
   29.20    "Isgn F vs = False"
   29.21 @@ -410,7 +410,7 @@
   29.22  
   29.23  lemmas eqs = Isgn.simps Iprod.simps
   29.24  
   29.25 -lemma "(x::'a::{ordered_idom, recpower})^4 * y * z * y^2 * z^23 > 0"
   29.26 +lemma "(x::'a::{ordered_idom})^4 * y * z * y^2 * z^23 > 0"
   29.27    apply (reify eqs)
   29.28    oops
   29.29