--- a/src/HOL/Algebra/poly/UnivPoly2.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Wed Apr 29 14:20:26 2009 +0200
@@ -347,9 +347,6 @@
by (simp add: up_divide_def)
qed
-instance up :: (ring) recpower proof
-qed simp_all
-
(* Further properties of monom *)
lemma monom_zero [simp]:
--- a/src/HOL/Complex.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Complex.thy Wed Apr 29 14:20:26 2009 +0200
@@ -157,11 +157,6 @@
end
-subsection {* Exponentiation *}
-
-instance complex :: recpower ..
-
-
subsection {* Numerals and Arithmetic *}
instantiation complex :: number_ring
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Apr 29 14:20:26 2009 +0200
@@ -639,7 +639,7 @@
interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
"op <=" "op <"
- "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"
+ "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,number_ring}) + y)"
proof (unfold_locales, dlo, dlo, auto)
fix x y::'a assume lt: "x < y"
from less_half_sum[OF lt] show "x < (x + y) /2" by simp
--- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Wed Apr 29 14:20:26 2009 +0200
@@ -7,147 +7,147 @@
begin
lemma
- "\<exists>(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0"
+ "\<exists>(y::'a::{ordered_field,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0"
by ferrack
-lemma "~ (ALL x (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < y --> 10*x < 11*y)"
+lemma "~ (ALL x (y::'a::{ordered_field,number_ring, division_by_zero}). x < y --> 10*x < 11*y)"
by ferrack
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
by ferrack
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x ~= y --> x < y"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. x ~= y --> x < y"
by ferrack
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
by ferrack
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
by ferrack
-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)"
+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)"
by ferrack
-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)"
+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)"
by ferrack
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
by ferrack
-lemma "EX x. (ALL (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \<le> 0 )"
+lemma "EX x. (ALL (y::'a::{ordered_field,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \<le> 0 )"
by ferrack
-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)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
by ferrack
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0"
by ferrack
-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"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
by ferrack
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)"
by ferrack
-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"
+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"
by ferrack
-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))"
+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))"
by ferrack
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
by ferrack
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
by ferrack
-lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )"
+lemma "ALL (x::'a::{ordered_field,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )"
by ferrack
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
by ferrack
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
by ferrack
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
by ferrack
-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))"
+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))"
by ferrack
-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))"
+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))"
by ferrack
-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))"
+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))"
by ferrack
-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) ))"
+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) ))"
by ferrack
-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))"
+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))"
by ferrack
-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"
+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"
by ferrack
-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"
+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"
by ferrack
-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)"
+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)"
by ferrack
-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)"
+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)"
by ferrack
-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)"
+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)"
by ferrack
-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))"
+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))"
by ferrack
-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)"
+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)"
by ferrack
-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))"
+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))"
by ferrack
-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)"
+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)"
by ferrack
-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))"
+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))"
by ferrack
-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))"
+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))"
by ferrack
-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))"
+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))"
by ferrack
-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)))"
+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)))"
by ferrack
-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))"
+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))"
by ferrack
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y).
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y).
(ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
by ferrack
-lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y. (EX z > y.
+lemma "EX (x::'a::{ordered_field,number_ring, division_by_zero}). (ALL y. (EX z > y.
(ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
by ferrack
-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)"
+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)"
by ferrack
-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)))"
+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)))"
by ferrack
-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)))"
+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)))"
by ferrack
-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)))"
+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)))"
by ferrack
end
--- a/src/HOL/Int.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Int.thy Wed Apr 29 14:20:26 2009 +0200
@@ -2178,8 +2178,6 @@
subsection {* Legacy theorems *}
-instance int :: recpower ..
-
lemmas zminus_zminus = minus_minus [of "z::int", standard]
lemmas zminus_0 = minus_zero [where 'a=int]
lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
--- a/src/HOL/Library/Binomial.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Binomial.thy Wed Apr 29 14:20:26 2009 +0200
@@ -292,7 +292,7 @@
subsection{* Generalized binomial coefficients *}
-definition gbinomial :: "'a::{field, recpower,ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
+definition gbinomial :: "'a::{field, ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
@@ -420,16 +420,16 @@
by (simp add: gbinomial_def)
lemma gbinomial_mult_fact:
- "(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})"
+ "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::{field, ring_char_0}) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
unfolding gbinomial_Suc
by (simp_all add: field_simps del: fact_Suc)
lemma gbinomial_mult_fact':
- "((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})"
+ "((a::'a::{field, ring_char_0}) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
using gbinomial_mult_fact[of k a]
apply (subst mult_commute) .
-lemma gbinomial_Suc_Suc: "((a::'a::{field,recpower, ring_char_0}) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
+lemma gbinomial_Suc_Suc: "((a::'a::{field, ring_char_0}) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
proof-
{assume "k = 0" then have ?thesis by simp}
moreover
--- a/src/HOL/Library/Commutative_Ring.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Commutative_Ring.thy Wed Apr 29 14:20:26 2009 +0200
@@ -27,15 +27,15 @@
text {* Interpretation functions for the shadow syntax. *}
-fun
- Ipol :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
+primrec
+ Ipol :: "'a::{comm_ring_1} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
where
"Ipol l (Pc c) = c"
| "Ipol l (Pinj i P) = Ipol (drop i l) P"
| "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"
-fun
- Ipolex :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
+primrec
+ Ipolex :: "'a::{comm_ring_1} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
where
"Ipolex l (Pol P) = Ipol l P"
| "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
@@ -54,7 +54,7 @@
PX p1 y p2 \<Rightarrow> Pinj x P)"
definition
- mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
+ mkPX :: "'a::{comm_ring} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
"mkPX P i Q = (case P of
Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
Pinj j R \<Rightarrow> PX P i Q |
@@ -63,7 +63,7 @@
text {* Defining the basic ring operations on normalized polynomials *}
function
- add :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65)
+ add :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65)
where
"Pc a \<oplus> Pc b = Pc (a + b)"
| "Pc c \<oplus> Pinj i P = Pinj i (P \<oplus> Pc c)"
@@ -90,7 +90,7 @@
termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
function
- mul :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<otimes>" 70)
+ mul :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<otimes>" 70)
where
"Pc a \<otimes> Pc b = Pc (a * b)"
| "Pc c \<otimes> Pinj i P =
@@ -122,8 +122,8 @@
(auto simp add: mkPinj_def split: pol.split)
text {* Negation*}
-fun
- neg :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
+primrec
+ neg :: "'a::{comm_ring} pol \<Rightarrow> 'a pol"
where
"neg (Pc c) = Pc (-c)"
| "neg (Pinj i P) = Pinj i (neg P)"
@@ -131,13 +131,13 @@
text {* Substraction *}
definition
- sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65)
+ sub :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65)
where
"sub P Q = P \<oplus> neg Q"
text {* Square for Fast Exponentation *}
-fun
- sqr :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
+primrec
+ sqr :: "'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
where
"sqr (Pc c) = Pc (c * c)"
| "sqr (Pinj i P) = mkPinj i (sqr P)"
@@ -146,7 +146,7 @@
text {* Fast Exponentation *}
fun
- pow :: "nat \<Rightarrow> 'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
+ pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
where
"pow 0 P = Pc 1"
| "pow n P = (if even n then pow (n div 2) (sqr P)
@@ -161,8 +161,8 @@
text {* Normalization of polynomial expressions *}
-fun
- norm :: "'a::{comm_ring,recpower} polex \<Rightarrow> 'a pol"
+primrec
+ norm :: "'a::{comm_ring_1} polex \<Rightarrow> 'a pol"
where
"norm (Pol P) = P"
| "norm (Add P Q) = norm P \<oplus> norm Q"
--- a/src/HOL/Library/Euclidean_Space.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Wed Apr 29 14:20:26 2009 +0200
@@ -253,8 +253,6 @@
"vector_power x 0 = 1"
| "vector_power x (Suc n) = x * vector_power x n"
-instance "^" :: (recpower,type) recpower ..
-
instance "^" :: (semiring,type) semiring
apply (intro_classes) by (vector ring_simps)+
@@ -2757,7 +2755,7 @@
(* Geometric progression. *)
(* ------------------------------------------------------------------------- *)
-lemma sum_gp_basic: "((1::'a::{field, recpower}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
+lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
(is "?lhs = ?rhs")
proof-
{assume x1: "x = 1" hence ?thesis by simp}
@@ -2775,7 +2773,7 @@
qed
lemma sum_gp_multiplied: assumes mn: "m <= n"
- shows "((1::'a::{field, recpower}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
+ shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
(is "?lhs = ?rhs")
proof-
let ?S = "{0..(n - m)}"
@@ -2792,7 +2790,7 @@
by (simp add: ring_simps power_add[symmetric])
qed
-lemma sum_gp: "setsum (op ^ (x::'a::{field, recpower})) {m .. n} =
+lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
(if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
else (x^ m - x^ (Suc n)) / (1 - x))"
proof-
@@ -2808,7 +2806,7 @@
ultimately show ?thesis by metis
qed
-lemma sum_gp_offset: "setsum (op ^ (x::'a::{field,recpower})) {m .. m+n} =
+lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
(if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
unfolding sum_gp[of x m "m + n"] power_Suc
by (simp add: ring_simps power_add)
--- a/src/HOL/Library/Float.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Float.thy Wed Apr 29 14:20:26 2009 +0200
@@ -443,8 +443,6 @@
lemma Ifloat_min: "Ifloat (min x y) = min (Ifloat x) (Ifloat y)" unfolding min_def le_float_def by auto
lemma Ifloat_max: "Ifloat (max a b) = max (Ifloat a) (Ifloat b)" unfolding max_def le_float_def by auto
-instance float :: recpower ..
-
lemma float_power: "Ifloat (x ^ n) = Ifloat x ^ n"
by (induct n) simp_all
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Apr 29 14:20:26 2009 +0200
@@ -680,8 +680,6 @@
subsection {* Powers*}
-instance fps :: (semiring_1) recpower ..
-
lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
by (induct n, auto simp add: expand_fps_eq fps_mult_nth)
@@ -701,11 +699,11 @@
lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
by (induct n, auto simp add: fps_mult_nth)
-lemma startsby_power:"a $0 = (v::'a::{comm_ring_1, recpower}) \<Longrightarrow> a^n $0 = v^n"
+lemma startsby_power:"a $0 = (v::'a::{comm_ring_1}) \<Longrightarrow> a^n $0 = v^n"
by (induct n, auto simp add: fps_mult_nth power_Suc)
lemma startsby_zero_power_iff[simp]:
- "a^n $0 = (0::'a::{idom, recpower}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
+ "a^n $0 = (0::'a::{idom}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
apply (rule iffI)
apply (induct n, auto simp add: power_Suc fps_mult_nth)
by (rule startsby_zero_power, simp_all)
@@ -748,7 +746,7 @@
apply (rule startsby_zero_power_prefix[rule_format, OF a0])
by arith
-lemma startsby_zero_power_nth_same: assumes a0: "a$0 = (0::'a::{recpower, idom})"
+lemma startsby_zero_power_nth_same: assumes a0: "a$0 = (0::'a::{idom})"
shows "a^n $ n = (a$1) ^ n"
proof(induct n)
case 0 thus ?case by (simp add: power_0)
@@ -769,7 +767,7 @@
qed
lemma fps_inverse_power:
- fixes a :: "('a::{field, recpower}) fps"
+ fixes a :: "('a::{field}) fps"
shows "inverse (a^n) = inverse a ^ n"
proof-
{assume a0: "a$0 = 0"
@@ -858,7 +856,7 @@
subsection{* The eXtractor series X*}
-lemma minus_one_power_iff: "(- (1::'a :: {recpower, comm_ring_1})) ^ n = (if even n then 1 else - 1)"
+lemma minus_one_power_iff: "(- (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else - 1)"
by (induct n, auto)
definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
@@ -915,7 +913,7 @@
by (simp add: X_power_iff)
lemma fps_inverse_X_plus1:
- "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::{recpower, field})) ^ n)" (is "_ = ?r")
+ "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::{field})) ^ n)" (is "_ = ?r")
proof-
have eq: "(1 + X) * ?r = 1"
unfolding minus_one_power_iff
@@ -1014,7 +1012,7 @@
lemma fps_mult_XD_shift:
- "(XD ^^ k) (a:: ('a::{comm_ring_1, recpower}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
+ "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
@@ -1296,7 +1294,7 @@
by (cases m, simp_all add: fps_power_nth_Suc del: power_Suc)
lemma fps_nth_power_0:
- fixes m :: nat and a :: "('a::{comm_ring_1, recpower}) fps"
+ fixes m :: nat and a :: "('a::{comm_ring_1}) fps"
shows "(a ^m)$0 = (a$0) ^ m"
proof-
{assume "m=0" hence ?thesis by simp}
@@ -1312,7 +1310,7 @@
qed
lemma fps_compose_inj_right:
- assumes a0: "a$0 = (0::'a::{recpower,idom})"
+ assumes a0: "a$0 = (0::'a::{idom})"
and a1: "a$1 \<noteq> 0"
shows "(b oo a = c oo a) \<longleftrightarrow> b = c" (is "?lhs \<longleftrightarrow>?rhs")
proof-
@@ -1353,7 +1351,7 @@
subsection {* Radicals *}
declare setprod_cong[fundef_cong]
-function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field, recpower}) fps \<Rightarrow> nat \<Rightarrow> 'a" where
+function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field}) fps \<Rightarrow> nat \<Rightarrow> 'a" where
"radical r 0 a 0 = 1"
| "radical r 0 a (Suc n) = 0"
| "radical r (Suc k) a 0 = r (Suc k) (a$0)"
@@ -1441,7 +1439,7 @@
qed
lemma power_radical:
- fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+ fixes a:: "'a ::{field, ring_char_0} fps"
assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0"
shows "(fps_radical r (Suc k) a) ^ (Suc k) = a"
proof-
@@ -1502,7 +1500,7 @@
lemma radical_unique:
assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0"
- and a0: "r (Suc k) (b$0 ::'a::{field, ring_char_0, recpower}) = a$0" and b0: "b$0 \<noteq> 0"
+ and a0: "r (Suc k) (b$0 ::'a::{field, ring_char_0}) = a$0" and b0: "b$0 \<noteq> 0"
shows "a^(Suc k) = b \<longleftrightarrow> a = fps_radical r (Suc k) b"
proof-
let ?r = "fps_radical r (Suc k) b"
@@ -1597,7 +1595,7 @@
lemma radical_power:
assumes r0: "r (Suc k) ((a$0) ^ Suc k) = a$0"
- and a0: "(a$0 ::'a::{field, ring_char_0, recpower}) \<noteq> 0"
+ and a0: "(a$0 ::'a::{field, ring_char_0}) \<noteq> 0"
shows "(fps_radical r (Suc k) (a ^ Suc k)) = a"
proof-
let ?ak = "a^ Suc k"
@@ -1609,7 +1607,7 @@
qed
lemma fps_deriv_radical:
- fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+ fixes a:: "'a ::{field, ring_char_0} fps"
assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0"
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)"
proof-
@@ -1630,7 +1628,7 @@
qed
lemma radical_mult_distrib:
- fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+ fixes a:: "'a ::{field, ring_char_0} fps"
assumes
ra0: "r (k) (a $ 0) ^ k = a $ 0"
and rb0: "r (k) (b $ 0) ^ k = b $ 0"
@@ -1656,7 +1654,7 @@
qed
lemma radical_inverse:
- fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+ fixes a:: "'a ::{field, ring_char_0} fps"
assumes
ra0: "r (k) (a $ 0) ^ k = a $ 0"
and ria0: "r (k) (inverse (a $ 0)) = inverse (r (k) (a $ 0))"
@@ -1698,7 +1696,7 @@
by (simp add: fps_divide_def)
lemma radical_divide:
- fixes a:: "'a ::{field, ring_char_0, recpower} fps"
+ fixes a:: "'a ::{field, ring_char_0} fps"
assumes
ra0: "r k (a $ 0) ^ k = a $ 0"
and rb0: "r k (b $ 0) ^ k = b $ 0"
@@ -1818,7 +1816,7 @@
subsection{* Compositional inverses *}
-fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{recpower,field}" where
+fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}" where
"compinv a 0 = X$0"
| "compinv a (Suc n) = (X$ Suc n - setsum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
@@ -1849,7 +1847,7 @@
qed
-fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{recpower,field}" where
+fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}" where
"gcompinv b a 0 = b$0"
| "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"
@@ -2102,7 +2100,7 @@
qed
lemma fps_inv_deriv:
- assumes a0:"a$0 = (0::'a::{recpower,field})" and a1: "a$1 \<noteq> 0"
+ assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \<noteq> 0"
shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)"
proof-
let ?ia = "fps_inv a"
@@ -2122,7 +2120,7 @@
subsubsection{* Exponential series *}
definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
-lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, recpower, ring_char_0}) * E a" (is "?l = ?r")
+lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, ring_char_0}) * E a" (is "?l = ?r")
proof-
{fix n
have "?l$n = ?r $ n"
@@ -2132,7 +2130,7 @@
qed
lemma E_unique_ODE:
- "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::{field, ring_char_0, recpower})"
+ "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::{field, ring_char_0})"
(is "?lhs \<longleftrightarrow> ?rhs")
proof-
{assume d: ?lhs
@@ -2159,7 +2157,7 @@
ultimately show ?thesis by blast
qed
-lemma E_add_mult: "E (a + b) = E (a::'a::{ring_char_0, field, recpower}) * E b" (is "?l = ?r")
+lemma E_add_mult: "E (a + b) = E (a::'a::{ring_char_0, field}) * E b" (is "?l = ?r")
proof-
have "fps_deriv (?r) = fps_const (a+b) * ?r"
by (simp add: fps_const_add[symmetric] ring_simps del: fps_const_add)
@@ -2171,10 +2169,10 @@
lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)"
by (simp add: E_def)
-lemma E0[simp]: "E (0::'a::{field, recpower}) = 1"
+lemma E0[simp]: "E (0::'a::{field}) = 1"
by (simp add: fps_eq_iff power_0_left)
-lemma E_neg: "E (- a) = inverse (E (a::'a::{ring_char_0, field, recpower}))"
+lemma E_neg: "E (- a) = inverse (E (a::'a::{ring_char_0, field}))"
proof-
from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1"
by (simp )
@@ -2182,7 +2180,7 @@
from fps_inverse_unique[OF th1 th0] show ?thesis by simp
qed
-lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, recpower, ring_char_0})) = (fps_const a)^n * (E a)"
+lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, ring_char_0})) = (fps_const a)^n * (E a)"
by (induct n, auto simp add: power_Suc)
lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
@@ -2195,7 +2193,7 @@
lemma X_fps_compose:"X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc)
-lemma X_compose_E[simp]: "X oo E (a::'a::{field, recpower}) = E a - 1"
+lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
by (simp add: fps_eq_iff X_fps_compose)
lemma LE_compose:
@@ -2217,7 +2215,7 @@
lemma inverse_one_plus_X:
- "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field, recpower})^n)"
+ "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field})^n)"
(is "inverse ?l = ?r")
proof-
have th: "?l * ?r = 1"
@@ -2228,11 +2226,11 @@
from fps_inverse_unique[OF th' th] show ?thesis .
qed
-lemma E_power_mult: "(E (c::'a::{field,recpower,ring_char_0}))^n = E (of_nat n * c)"
+lemma E_power_mult: "(E (c::'a::{field,ring_char_0}))^n = E (of_nat n * c)"
by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
subsubsection{* Logarithmic series *}
-definition "(L::'a::{field, ring_char_0,recpower} fps)
+definition "(L::'a::{field, ring_char_0} fps)
= Abs_fps (\<lambda>n. (- 1) ^ Suc n / of_nat n)"
lemma fps_deriv_L: "fps_deriv L = inverse (1 + X)"
@@ -2243,7 +2241,7 @@
by (simp add: L_def)
lemma L_E_inv:
- assumes a: "a\<noteq> (0::'a::{field,division_by_zero,ring_char_0,recpower})"
+ assumes a: "a\<noteq> (0::'a::{field,division_by_zero,ring_char_0})"
shows "L = fps_const a * fps_inv (E a - 1)" (is "?l = ?r")
proof-
let ?b = "E a - 1"
@@ -2267,10 +2265,10 @@
subsubsection{* Formal trigonometric functions *}
-definition "fps_sin (c::'a::{field, recpower, ring_char_0}) =
+definition "fps_sin (c::'a::{field, ring_char_0}) =
Abs_fps (\<lambda>n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))"
-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)"
+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)"
lemma fps_sin_deriv:
"fps_deriv (fps_sin c) = fps_const c * fps_cos c"
--- a/src/HOL/Library/FrechetDeriv.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy Wed Apr 29 14:20:26 2009 +0200
@@ -382,7 +382,7 @@
subsection {* Powers *}
lemma FDERIV_power_Suc:
- fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
+ fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
apply (induct n)
apply (simp add: power_Suc FDERIV_ident)
@@ -392,7 +392,7 @@
done
lemma FDERIV_power:
- fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
+ fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
apply (cases n)
apply (simp add: FDERIV_const)
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed Apr 29 14:20:26 2009 +0200
@@ -560,14 +560,14 @@
done
lemma poly_replicate_append:
- "poly (monom 1 n * p) (x::'a::{recpower, comm_ring_1}) = x^n * poly p x"
+ "poly (monom 1 n * p) (x::'a::{comm_ring_1}) = x^n * poly p x"
by (simp add: poly_monom)
text {* Decomposition of polynomial, skipping zero coefficients
after the first. *}
lemma poly_decompose_lemma:
- assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
+ assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{idom}))"
shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and>
(\<forall>z. poly p z = z^k * poly (pCons a q) z)"
unfolding psize_def
@@ -595,7 +595,7 @@
lemma poly_decompose:
assumes nc: "~constant(poly p)"
- shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
+ shows "\<exists>k a q. a\<noteq>(0::'a::{idom}) \<and> k\<noteq>0 \<and>
psize q + k + 1 = psize p \<and>
(\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
using nc
--- a/src/HOL/Library/Numeral_Type.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Wed Apr 29 14:20:26 2009 +0200
@@ -216,12 +216,6 @@
apply (simp_all add: Rep_simps zmod_simps ring_simps)
done
-lemma recpower: "OFCLASS('a, recpower_class)"
-apply (intro_classes, unfold definitions)
-apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc
- mod_pos_pos_trivial size1)
-done
-
end
locale mod_ring = mod_type +
@@ -340,11 +334,11 @@
apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
done
-instance bit0 :: (finite) "{comm_ring_1,recpower}"
- by (rule bit0.comm_ring_1 bit0.recpower)+
+instance bit0 :: (finite) comm_ring_1
+ by (rule bit0.comm_ring_1)+
-instance bit1 :: (finite) "{comm_ring_1,recpower}"
- by (rule bit1.comm_ring_1 bit1.recpower)+
+instance bit1 :: (finite) comm_ring_1
+ by (rule bit1.comm_ring_1)+
instantiation bit0 and bit1 :: (finite) number_ring
begin
--- a/src/HOL/Library/Pocklington.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Pocklington.thy Wed Apr 29 14:20:26 2009 +0200
@@ -568,7 +568,7 @@
lemma nproduct_cmul:
assumes fS:"finite S"
- shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult,recpower})* a(m)) S = c ^ (card S) * setprod a S"
+ shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S"
unfolding setprod_timesf setprod_constant[OF fS, of c] ..
lemma coprime_nproduct:
--- a/src/HOL/Library/Polynomial.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy Wed Apr 29 14:20:26 2009 +0200
@@ -632,8 +632,6 @@
shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
by (safe elim!: dvd_smult dvd_smult_cancel)
-instance poly :: (comm_semiring_1) recpower ..
-
lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
by (induct n, simp, auto intro: order_trans degree_mult_le)
@@ -1120,7 +1118,7 @@
unfolding one_poly_def by simp
lemma poly_monom:
- fixes a x :: "'a::{comm_semiring_1,recpower}"
+ fixes a x :: "'a::{comm_semiring_1}"
shows "poly (monom a n) x = a * x ^ n"
by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
@@ -1149,7 +1147,7 @@
by (induct p, simp_all, simp add: algebra_simps)
lemma poly_power [simp]:
- fixes p :: "'a::{comm_semiring_1,recpower} poly"
+ fixes p :: "'a::{comm_semiring_1} poly"
shows "poly (p ^ n) x = poly p x ^ n"
by (induct n, simp, simp add: power_Suc)
--- a/src/HOL/Library/Univ_Poly.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Wed Apr 29 14:20:26 2009 +0200
@@ -167,22 +167,9 @@
simp_all add: poly_cmult poly_add left_distrib right_distrib mult_ac)
qed
-class recpower_semiring = semiring + recpower
-class recpower_semiring_1 = semiring_1 + recpower
-class recpower_semiring_0 = semiring_0 + recpower
-class recpower_ring = ring + recpower
-class recpower_ring_1 = ring_1 + recpower
-subclass (in recpower_ring_1) recpower_ring ..
-class recpower_comm_semiring_1 = recpower + comm_semiring_1
-class recpower_comm_ring_1 = recpower + comm_ring_1
-subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 ..
-class recpower_idom = recpower + idom
-subclass (in recpower_idom) recpower_comm_ring_1 ..
class idom_char_0 = idom + ring_char_0
-class recpower_idom_char_0 = recpower + idom_char_0
-subclass (in recpower_idom_char_0) recpower_idom ..
-lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
+lemma (in comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
apply (induct "n")
apply (auto simp add: poly_cmult poly_mult power_Suc)
done
@@ -418,7 +405,7 @@
finally show ?thesis .
qed
-lemma (in recpower_idom) poly_exp_eq_zero[simp]:
+lemma (in idom) poly_exp_eq_zero[simp]:
"(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
apply (simp only: fun_eq add: all_simps [symmetric])
apply (rule arg_cong [where f = All])
@@ -437,7 +424,7 @@
apply simp
done
-lemma (in recpower_idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
+lemma (in idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
by auto
text{*A more constructive notion of polynomials being trivial*}
@@ -507,7 +494,7 @@
done
-lemma (in recpower_comm_semiring_1) poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
+lemma (in comm_semiring_1) poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
apply (auto simp add: le_iff_add)
apply (induct_tac k)
apply (rule_tac [2] poly_divides_trans)
@@ -516,7 +503,7 @@
apply (auto simp add: poly_mult fun_eq mult_ac)
done
-lemma (in recpower_comm_semiring_1) poly_exp_divides: "[| (p %^ n) divides q; m\<le>n |] ==> (p %^ m) divides q"
+lemma (in comm_semiring_1) poly_exp_divides: "[| (p %^ n) divides q; m\<le>n |] ==> (p %^ m) divides q"
by (blast intro: poly_divides_exp poly_divides_trans)
lemma (in comm_semiring_0) poly_divides_add:
@@ -583,7 +570,7 @@
qed
-lemma (in recpower_comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
+lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
by(induct n, auto simp add: poly_mult power_Suc mult_ac)
lemma (in comm_semiring_1) divides_left_mult:
@@ -600,11 +587,11 @@
(* FIXME: Tidy up *)
-lemma (in recpower_semiring_1)
+lemma (in semiring_1)
zero_power_iff: "0 ^ n = (if n = 0 then 1 else 0)"
by (induct n, simp_all add: power_Suc)
-lemma (in recpower_idom_char_0) poly_order_exists:
+lemma (in idom_char_0) poly_order_exists:
assumes lp: "length p = d" and p0: "poly p \<noteq> poly []"
shows "\<exists>n. ([-a, 1] %^ n) divides p & ~(([-a, 1] %^ (Suc n)) divides p)"
proof-
@@ -637,7 +624,7 @@
lemma (in semiring_1) poly_one_divides[simp]: "[1] divides p"
by (simp add: divides_def, auto)
-lemma (in recpower_idom_char_0) poly_order: "poly p \<noteq> poly []
+lemma (in idom_char_0) poly_order: "poly p \<noteq> poly []
==> EX! n. ([-a, 1] %^ n) divides p &
~(([-a, 1] %^ (Suc n)) divides p)"
apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
@@ -652,7 +639,7 @@
lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n"
by (blast intro: someI2)
-lemma (in recpower_idom_char_0) order:
+lemma (in idom_char_0) order:
"(([-a, 1] %^ n) divides p &
~(([-a, 1] %^ (Suc n)) divides p)) =
((n = order a p) & ~(poly p = poly []))"
@@ -662,17 +649,17 @@
apply (blast intro!: poly_order [THEN [2] some1_equalityD])
done
-lemma (in recpower_idom_char_0) order2: "[| poly p \<noteq> poly [] |]
+lemma (in idom_char_0) order2: "[| poly p \<noteq> poly [] |]
==> ([-a, 1] %^ (order a p)) divides p &
~(([-a, 1] %^ (Suc(order a p))) divides p)"
by (simp add: order del: pexp_Suc)
-lemma (in recpower_idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
+lemma (in idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
~(([-a, 1] %^ (Suc n)) divides p)
|] ==> (n = order a p)"
by (insert order [of a n p], auto)
-lemma (in recpower_idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
+lemma (in idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
~(([-a, 1] %^ (Suc n)) divides p))
==> (n = order a p)"
by (blast intro: order_unique)
@@ -692,7 +679,7 @@
apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
done
-lemma (in recpower_idom_char_0) order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
+lemma (in idom_char_0) order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
proof-
let ?poly = poly
show ?thesis
@@ -706,7 +693,7 @@
done
qed
-lemma (in recpower_idom_char_0) order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
+lemma (in idom_char_0) order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
proof-
let ?poly = poly
show ?thesis
@@ -718,7 +705,7 @@
done
qed
-lemma (in recpower_idom_char_0) order_decomp:
+lemma (in idom_char_0) order_decomp:
"poly p \<noteq> poly []
==> \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) &
~([-a, 1] divides q)"
@@ -732,7 +719,7 @@
text{*Important composition properties of orders.*}
lemma order_mult: "poly (p *** q) \<noteq> poly []
- ==> order a (p *** q) = order a p + order (a::'a::{recpower_idom_char_0}) q"
+ ==> order a (p *** q) = order a p + order (a::'a::{idom_char_0}) q"
apply (cut_tac a = a and p = "p *** q" and n = "order a p + order a q" in order)
apply (auto simp add: poly_entire simp del: pmult_Cons)
apply (drule_tac a = a in order2)+
@@ -753,7 +740,7 @@
apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
done
-lemma (in recpower_idom_char_0) order_mult:
+lemma (in idom_char_0) order_mult:
assumes pq0: "poly (p *** q) \<noteq> poly []"
shows "order a (p *** q) = order a p + order a q"
proof-
@@ -783,7 +770,7 @@
done
qed
-lemma (in recpower_idom_char_0) order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
+lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
by (rule order_root [THEN ssubst], auto)
lemma (in semiring_1) pmult_one[simp]: "[1] *** p = p" by auto
@@ -791,7 +778,7 @@
lemma (in semiring_0) poly_Nil_zero: "poly [] = poly [0]"
by (simp add: fun_eq)
-lemma (in recpower_idom_char_0) rsquarefree_decomp:
+lemma (in idom_char_0) rsquarefree_decomp:
"[| rsquarefree p; poly p a = 0 |]
==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0"
apply (simp add: rsquarefree_def, safe)
@@ -999,7 +986,7 @@
ultimately show ?case by blast
qed
-lemma (in recpower_idom_char_0) order_degree:
+lemma (in idom_char_0) order_degree:
assumes p0: "poly p \<noteq> poly []"
shows "order a p \<le> degree p"
proof-
--- a/src/HOL/Library/comm_ring.ML Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/comm_ring.ML Wed Apr 29 14:20:26 2009 +0200
@@ -65,7 +65,7 @@
| reif_polex T vs t = polex_pol T $ reif_pol T vs t;
(* reification of the equation *)
-val TFree (_, cr_sort) = @{typ "'a :: {comm_ring, recpower}"};
+val cr_sort = @{sort "comm_ring_1"};
fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
if Sign.of_sort thy (T, cr_sort) then
--- a/src/HOL/NSA/StarDef.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/NSA/StarDef.thy Wed Apr 29 14:20:26 2009 +0200
@@ -954,8 +954,6 @@
subsection {* Power *}
-instance star :: (recpower) recpower ..
-
lemma star_power_def [transfer_unfold]:
"(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
proof (rule eq_reflection, rule ext, rule ext)
--- a/src/HOL/Power.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Power.thy Wed Apr 29 14:20:26 2009 +0200
@@ -419,13 +419,9 @@
apply assumption
done
-class recpower = monoid_mult
-
subsection {* Exponentiation for the Natural Numbers *}
-instance nat :: recpower ..
-
lemma nat_one_le_power [simp]:
"Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
by (rule one_le_power [of i n, unfolded One_nat_def])
--- a/src/HOL/Rational.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Rational.thy Wed Apr 29 14:20:26 2009 +0200
@@ -834,8 +834,6 @@
"q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
by (rule Rats_cases) auto
-instance rat :: recpower ..
-
subsection {* Implementation of rational numbers as pairs of integers *}
--- a/src/HOL/RealPow.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/RealPow.thy Wed Apr 29 14:20:26 2009 +0200
@@ -12,8 +12,6 @@
declare abs_mult_self [simp]
-instance real :: recpower ..
-
lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
by simp
--- a/src/HOL/SizeChange/Graphs.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/SizeChange/Graphs.thy Wed Apr 29 14:20:26 2009 +0200
@@ -228,7 +228,7 @@
qed
qed
-instance graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower}"
+instance graph :: (type, monoid_mult) "{semiring_1, idem_add}"
proof
fix a b c :: "('a, 'b) graph"
--- a/src/HOL/SizeChange/Kleene_Algebras.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/SizeChange/Kleene_Algebras.thy Wed Apr 29 14:20:26 2009 +0200
@@ -97,7 +97,7 @@
and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
class kleene_by_complete_lattice = pre_kleene
- + complete_lattice + recpower + star +
+ + complete_lattice + power + star +
assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
begin
--- a/src/HOL/Word/WordArith.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Word/WordArith.thy Wed Apr 29 14:20:26 2009 +0200
@@ -778,8 +778,6 @@
apply (simp add: word_mult_1)
done
-instance word :: (len0) recpower ..
-
instance word :: (len0) comm_semiring
by (intro_classes) (simp add : word_left_distrib)
@@ -790,8 +788,6 @@
instance word :: (len) comm_semiring_1
by (intro_classes) (simp add: lenw1_zero_neq_one)
-instance word :: (len) recpower ..
-
instance word :: (len) comm_ring_1 ..
instance word :: (len0) comm_semiring_0 ..
--- a/src/HOL/ex/Commutative_Ring_Complete.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy Wed Apr 29 14:20:26 2009 +0200
@@ -1,5 +1,4 @@
-(* ID: $Id$
- Author: Bernhard Haeupler
+(* Author: Bernhard Haeupler
This theory is about of the relative completeness of method comm-ring
method. As long as the reified atomic polynomials of type 'a pol are
@@ -14,7 +13,7 @@
text {* Formalization of normal form *}
fun
- isnorm :: "('a::{comm_ring,recpower}) pol \<Rightarrow> bool"
+ isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool"
where
"isnorm (Pc c) \<longleftrightarrow> True"
| "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
--- a/src/HOL/ex/Formal_Power_Series_Examples.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/Formal_Power_Series_Examples.thy Wed Apr 29 14:20:26 2009 +0200
@@ -11,7 +11,7 @@
section{* The generalized binomial theorem *}
lemma gbinomial_theorem:
- "((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))"
+ "((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))"
proof-
from E_add_mult[of a b]
have "(E (a + b)) $ n = (E a * E b)$n" by simp
@@ -38,7 +38,7 @@
by (simp add: fps_binomial_def)
lemma fps_binomial_ODE_unique:
- fixes c :: "'a::{field, recpower,ring_char_0}"
+ fixes c :: "'a::{field, ring_char_0}"
shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
(is "?lhs \<longleftrightarrow> ?rhs")
proof-
--- a/src/HOL/ex/Groebner_Examples.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy Wed Apr 29 14:20:26 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Groebner_Examples.thy
- ID: $Id$
Author: Amine Chaieb, TU Muenchen
*)
@@ -11,7 +10,7 @@
subsection {* Basic examples *}
-lemma "3 ^ 3 == (?X::'a::{number_ring,recpower})"
+lemma "3 ^ 3 == (?X::'a::{number_ring})"
by sring_norm
lemma "(x - (-2))^5 == ?X::int"
@@ -20,7 +19,7 @@
lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int"
by sring_norm
-lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring,recpower})"
+lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
apply (simp only: power_Suc power_0)
apply (simp only: comp_arith)
oops
@@ -47,7 +46,7 @@
by algebra
lemma
- fixes x::"'a::{idom,recpower,number_ring}"
+ fixes x::"'a::{idom,number_ring}"
shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0"
by algebra
@@ -58,7 +57,7 @@
"sq x == x*x"
lemma
- fixes x1 :: "'a::{idom,recpower,number_ring}"
+ fixes x1 :: "'a::{idom,number_ring}"
shows
"(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) +
@@ -68,7 +67,7 @@
by (algebra add: sq_def)
lemma
- fixes p1 :: "'a::{idom,recpower,number_ring}"
+ fixes p1 :: "'a::{idom,number_ring}"
shows
"(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
(sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
--- a/src/HOL/ex/Numeral.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/Numeral.thy Wed Apr 29 14:20:26 2009 +0200
@@ -14,25 +14,19 @@
text {* Increment function for type @{typ num} *}
-primrec
- inc :: "num \<Rightarrow> num"
-where
+primrec inc :: "num \<Rightarrow> num" where
"inc One = Dig0 One"
| "inc (Dig0 x) = Dig1 x"
| "inc (Dig1 x) = Dig0 (inc x)"
text {* Converting between type @{typ num} and type @{typ nat} *}
-primrec
- nat_of_num :: "num \<Rightarrow> nat"
-where
+primrec nat_of_num :: "num \<Rightarrow> nat" where
"nat_of_num One = Suc 0"
| "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x"
| "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)"
-primrec
- num_of_nat :: "nat \<Rightarrow> num"
-where
+primrec num_of_nat :: "nat \<Rightarrow> num" where
"num_of_nat 0 = One"
| "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
@@ -719,32 +713,32 @@
(simp_all add: of_num.simps of_num_plus [symmetric] algebra_simps)
lemma of_num_pow:
- "(of_num (pow x y)::'a::{semiring_numeral,recpower}) = of_num x ^ of_num y"
+ "(of_num (pow x y)::'a::{semiring_numeral}) = of_num x ^ of_num y"
by (induct y)
(simp_all add: of_num.simps of_num_square of_num_times [symmetric]
power_Suc power_add)
lemma power_of_num [numeral]:
- "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral,recpower})"
+ "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral})"
by (rule of_num_pow [symmetric])
lemma power_zero_of_num [numeral]:
- "0 ^ of_num n = (0::'a::{semiring_0,recpower})"
+ "0 ^ of_num n = (0::'a::{semiring_0,power})"
using of_num_pos [where n=n and ?'a=nat]
by (simp add: power_0_left)
lemma power_minus_one_double:
- "(- 1) ^ (n + n) = (1::'a::{ring_1,recpower})"
+ "(- 1) ^ (n + n) = (1::'a::{ring_1})"
by (induct n) (simp_all add: power_Suc)
lemma power_minus_Dig0 [numeral]:
- fixes x :: "'a::{ring_1,recpower}"
+ fixes x :: "'a::{ring_1}"
shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)"
by (subst power_minus)
(simp add: of_num.simps power_minus_one_double)
lemma power_minus_Dig1 [numeral]:
- fixes x :: "'a::{ring_1,recpower}"
+ fixes x :: "'a::{ring_1}"
shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))"
by (subst power_minus)
(simp add: of_num.simps power_Suc power_minus_one_double)
--- a/src/HOL/ex/ReflectionEx.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/ex/ReflectionEx.thy Wed Apr 29 14:20:26 2009 +0200
@@ -385,7 +385,7 @@
(* An example for equations containing type variables *)
datatype prod = Zero | One | Var nat | Mul prod prod
| Pw prod nat | PNM nat nat prod
-consts Iprod :: " prod \<Rightarrow> ('a::{ordered_idom,recpower}) list \<Rightarrow>'a"
+consts Iprod :: " prod \<Rightarrow> ('a::{ordered_idom}) list \<Rightarrow>'a"
primrec
"Iprod Zero vs = 0"
"Iprod One vs = 1"
@@ -397,7 +397,7 @@
datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F
| Or sgn sgn | And sgn sgn
-consts Isgn :: " sgn \<Rightarrow> ('a::{ordered_idom, recpower}) list \<Rightarrow>bool"
+consts Isgn :: " sgn \<Rightarrow> ('a::{ordered_idom}) list \<Rightarrow>bool"
primrec
"Isgn Tr vs = True"
"Isgn F vs = False"
@@ -410,7 +410,7 @@
lemmas eqs = Isgn.simps Iprod.simps
-lemma "(x::'a::{ordered_idom, recpower})^4 * y * z * y^2 * z^23 > 0"
+lemma "(x::'a::{ordered_idom})^4 * y * z * y^2 * z^23 > 0"
apply (reify eqs)
oops