--- a/src/HOL/Deriv.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Deriv.thy Tue Apr 28 19:15:50 2009 +0200
@@ -1,5 +1,4 @@
(* Title : Deriv.thy
- ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
@@ -197,7 +196,7 @@
done
lemma DERIV_power_Suc:
- fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
+ fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
assumes f: "DERIV f x :> D"
shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
proof (induct n)
@@ -211,7 +210,7 @@
qed
lemma DERIV_power:
- fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
+ fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
assumes f: "DERIV f x :> D"
shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
@@ -287,20 +286,20 @@
text{*Power of -1*}
lemma DERIV_inverse:
- fixes x :: "'a::{real_normed_field,recpower}"
+ fixes x :: "'a::{real_normed_field}"
shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
by (drule DERIV_inverse' [OF DERIV_ident]) simp
text{*Derivative of inverse*}
lemma DERIV_inverse_fun:
- fixes x :: "'a::{real_normed_field,recpower}"
+ fixes x :: "'a::{real_normed_field}"
shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
text{*Derivative of quotient*}
lemma DERIV_quotient:
- fixes x :: "'a::{real_normed_field,recpower}"
+ fixes x :: "'a::{real_normed_field}"
shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
by (drule (2) DERIV_divide) (simp add: mult_commute)
@@ -404,7 +403,7 @@
unfolding divide_inverse using prems by simp
lemma differentiable_power [simp]:
- fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"
+ fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
assumes "f differentiable x"
shows "(\<lambda>x. f x ^ n) differentiable x"
by (induct n, simp, simp add: prems)
--- a/src/HOL/Finite_Set.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Finite_Set.thy Tue Apr 28 19:15:50 2009 +0200
@@ -2047,14 +2047,14 @@
apply (auto simp add: algebra_simps)
done
-lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
+lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
apply (erule finite_induct)
apply (auto simp add: power_Suc)
done
lemma setprod_gen_delta:
assumes fS: "finite S"
- shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult, recpower}) * c^ (card S - 1) else c^ card S)"
+ shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult}) * c^ (card S - 1) else c^ card S)"
proof-
let ?f = "(\<lambda>k. if k=a then b k else c)"
{assume a: "a \<notin> S"
--- a/src/HOL/Groebner_Basis.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Groebner_Basis.thy Tue Apr 28 19:15:50 2009 +0200
@@ -164,7 +164,7 @@
end
interpretation class_semiring: gb_semiring
- "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
+ "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
proof qed (auto simp add: algebra_simps power_Suc)
lemmas nat_arith =
@@ -242,7 +242,7 @@
interpretation class_ring: gb_ring "op +" "op *" "op ^"
- "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
+ "0::'a::{comm_semiring_1,number_ring}" 1 "op -" "uminus"
proof qed simp_all
@@ -349,9 +349,9 @@
qed
interpretation class_ringb: ringb
- "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
+ "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
- fix w x y z ::"'a::{idom,recpower,number_ring}"
+ fix w x y z ::"'a::{idom,number_ring}"
assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
hence ynz': "y - z \<noteq> 0" by simp
from p have "w * y + x* z - w*z - x*y = 0" by simp
@@ -471,7 +471,7 @@
subsection{* Groebner Bases for fields *}
interpretation class_fieldgb:
- fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
+ fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
--- a/src/HOL/Int.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Int.thy Tue Apr 28 19:15:50 2009 +0200
@@ -292,9 +292,7 @@
context ring_1
begin
-definition
- of_int :: "int \<Rightarrow> 'a"
-where
+definition of_int :: "int \<Rightarrow> 'a" where
[code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
@@ -330,6 +328,10 @@
lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
by (induct n) auto
+lemma of_int_power:
+ "of_int (z ^ n) = of_int z ^ n"
+ by (induct n) simp_all
+
end
context ordered_idom
@@ -1841,23 +1843,6 @@
qed
-subsection {* Integer Powers *}
-
-lemma of_int_power:
- "of_int (z ^ n) = of_int z ^ n"
- by (induct n) simp_all
-
-lemma zpower_zpower:
- "(x ^ y) ^ z = (x ^ (y * z)::int)"
- by (rule power_mult [symmetric])
-
-lemma int_power:
- "int (m ^ n) = int m ^ n"
- by (rule of_nat_power)
-
-lemmas zpower_int = int_power [symmetric]
-
-
subsection {* Further theorems on numerals *}
subsubsection{*Special Simplification for Constants*}
@@ -2260,4 +2245,14 @@
lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
by (rule zero_le_power_abs)
+lemma zpower_zpower:
+ "(x ^ y) ^ z = (x ^ (y * z)::int)"
+ by (rule power_mult [symmetric])
+
+lemma int_power:
+ "int (m ^ n) = int m ^ n"
+ by (rule of_nat_power)
+
+lemmas zpower_int = int_power [symmetric]
+
end
--- a/src/HOL/Lim.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Lim.thy Tue Apr 28 19:15:50 2009 +0200
@@ -383,7 +383,7 @@
lemmas LIM_of_real = of_real.LIM
lemma LIM_power:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
assumes f: "f -- a --> l"
shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
by (induct n, simp, simp add: LIM_mult f)
@@ -530,7 +530,7 @@
unfolding isCont_def by (rule LIM_of_real)
lemma isCont_power:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
unfolding isCont_def by (rule LIM_power)
--- a/src/HOL/NSA/HDeriv.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/NSA/HDeriv.thy Tue Apr 28 19:15:50 2009 +0200
@@ -1,5 +1,4 @@
(* Title : Deriv.thy
- ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
@@ -345,7 +344,7 @@
(*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
lemma NSDERIV_inverse:
- fixes x :: "'a::{real_normed_field,recpower}"
+ fixes x :: "'a::{real_normed_field}"
shows "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"
apply (simp add: nsderiv_def)
apply (rule ballI, simp, clarify)
@@ -383,7 +382,7 @@
text{*Derivative of inverse*}
lemma NSDERIV_inverse_fun:
- fixes x :: "'a::{real_normed_field,recpower}"
+ fixes x :: "'a::{real_normed_field}"
shows "[| NSDERIV f x :> d; f(x) \<noteq> 0 |]
==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc)
@@ -391,7 +390,7 @@
text{*Derivative of quotient*}
lemma NSDERIV_quotient:
- fixes x :: "'a::{real_normed_field,recpower}"
+ fixes x :: "'a::{real_normed_field}"
shows "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> 0 |]
==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
- (e*f(x))) / (g(x) ^ Suc (Suc 0))"
--- a/src/HOL/NSA/HSEQ.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/NSA/HSEQ.thy Tue Apr 28 19:15:50 2009 +0200
@@ -110,7 +110,7 @@
done
lemma NSLIMSEQ_pow [rule_format]:
- fixes a :: "'a::{real_normed_algebra,recpower}"
+ fixes a :: "'a::{real_normed_algebra,power}"
shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
apply (induct "m")
apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
--- a/src/HOL/NSA/HyperDef.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/NSA/HyperDef.thy Tue Apr 28 19:15:50 2009 +0200
@@ -417,7 +417,7 @@
declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
(*
lemma hrealpow_HFinite:
- fixes x :: "'a::{real_normed_algebra,recpower} star"
+ fixes x :: "'a::{real_normed_algebra,power} star"
shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
apply (induct_tac "n")
apply (auto simp add: power_Suc intro: HFinite_mult)
@@ -438,24 +438,24 @@
by (simp add: hyperpow_def starfun2_star_n)
lemma hyperpow_zero [simp]:
- "\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0"
+ "\<And>n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0"
by transfer simp
lemma hyperpow_not_zero:
- "\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0"
+ "\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0"
by transfer (rule field_power_not_zero)
lemma hyperpow_inverse:
- "\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star)
+ "\<And>r n. r \<noteq> (0::'a::{division_by_zero,field} star)
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
by transfer (rule power_inverse)
-
+
lemma hyperpow_hrabs:
- "\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)"
+ "\<And>r n. abs (r::'a::{ordered_idom} star) pow n = abs (r pow n)"
by transfer (rule power_abs [symmetric])
lemma hyperpow_add:
- "\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)"
+ "\<And>r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)"
by transfer (rule power_add)
lemma hyperpow_one [simp]:
@@ -463,46 +463,46 @@
by transfer (rule power_one_right)
lemma hyperpow_two:
- "\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r"
-by transfer (simp add: power_Suc)
+ "\<And>r. (r::'a::monoid_mult star) pow ((1::hypnat) + (1::hypnat)) = r * r"
+by transfer simp
lemma hyperpow_gt_zero:
- "\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
+ "\<And>r n. (0::'a::{ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
by transfer (rule zero_less_power)
lemma hyperpow_ge_zero:
- "\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
+ "\<And>r n. (0::'a::{ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
by transfer (rule zero_le_power)
lemma hyperpow_le:
- "\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk>
+ "\<And>x y n. \<lbrakk>(0::'a::{ordered_semidom} star) < x; x \<le> y\<rbrakk>
\<Longrightarrow> x pow n \<le> y pow n"
by transfer (rule power_mono [OF _ order_less_imp_le])
lemma hyperpow_eq_one [simp]:
- "\<And>n. 1 pow n = (1::'a::recpower star)"
+ "\<And>n. 1 pow n = (1::'a::monoid_mult star)"
by transfer (rule power_one)
lemma hrabs_hyperpow_minus_one [simp]:
- "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)"
+ "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,ordered_idom} star)"
by transfer (rule abs_power_minus_one)
lemma hyperpow_mult:
- "\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n
+ "\<And>r s n. (r * s::'a::{comm_monoid_mult} star) pow n
= (r pow n) * (s pow n)"
by transfer (rule power_mult_distrib)
lemma hyperpow_two_le [simp]:
- "(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)"
+ "(0::'a::{monoid_mult,ordered_ring_strict} star) \<le> r pow (1 + 1)"
by (auto simp add: hyperpow_two zero_le_mult_iff)
lemma hrabs_hyperpow_two [simp]:
"abs(x pow (1 + 1)) =
- (x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)"
+ (x::'a::{monoid_mult,ordered_ring_strict} star) pow (1 + 1)"
by (simp only: abs_of_nonneg hyperpow_two_le)
lemma hyperpow_two_hrabs [simp]:
- "abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1) = x pow (1 + 1)"
+ "abs(x::'a::{ordered_idom} star) pow (1 + 1) = x pow (1 + 1)"
by (simp add: hyperpow_hrabs)
text{*The precondition could be weakened to @{term "0\<le>x"}*}
@@ -511,11 +511,11 @@
by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
lemma hyperpow_two_gt_one:
- "\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
+ "\<And>r::'a::{ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
by transfer (simp add: power_gt1 del: power_Suc)
lemma hyperpow_two_ge_one:
- "\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
+ "\<And>r::'a::{ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
by transfer (simp add: one_le_power del: power_Suc)
lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
@@ -565,7 +565,7 @@
lemma of_hypreal_hyperpow:
"\<And>x n. of_hypreal (x pow n) =
- (of_hypreal x::'a::{real_algebra_1,recpower} star) pow n"
+ (of_hypreal x::'a::{real_algebra_1} star) pow n"
by transfer (rule of_real_power)
end
--- a/src/HOL/NSA/NSA.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/NSA/NSA.thy Tue Apr 28 19:15:50 2009 +0200
@@ -101,7 +101,7 @@
by transfer (rule norm_mult)
lemma hnorm_hyperpow:
- "\<And>(x::'a::{real_normed_div_algebra,recpower} star) n.
+ "\<And>(x::'a::{real_normed_div_algebra} star) n.
hnorm (x pow n) = hnorm x pow n"
by transfer (rule norm_power)
@@ -304,15 +304,15 @@
unfolding star_one_def by (rule HFinite_star_of)
lemma hrealpow_HFinite:
- fixes x :: "'a::{real_normed_algebra,recpower} star"
+ fixes x :: "'a::{real_normed_algebra,monoid_mult} star"
shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
-apply (induct_tac "n")
+apply (induct n)
apply (auto simp add: power_Suc intro: HFinite_mult)
done
lemma HFinite_bounded:
"[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
-apply (case_tac "x \<le> 0")
+apply (cases "x \<le> 0")
apply (drule_tac y = x in order_trans)
apply (drule_tac [2] order_antisym)
apply (auto simp add: linorder_not_le)
--- a/src/HOL/NSA/NSComplex.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/NSA/NSComplex.thy Tue Apr 28 19:15:50 2009 +0200
@@ -383,7 +383,7 @@
by transfer (rule power_mult_distrib)
lemma hcpow_zero2 [simp]:
- "\<And>n. 0 pow (hSuc n) = (0::'a::{recpower,semiring_0} star)"
+ "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
by transfer (rule power_0_Suc)
lemma hcpow_not_zero [simp,intro]:
--- a/src/HOL/Nat_Numeral.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Tue Apr 28 19:15:50 2009 +0200
@@ -10,6 +10,8 @@
uses ("Tools/nat_simprocs.ML")
begin
+subsection {* Numerals for natural numbers *}
+
text {*
Arithmetic for naturals is reduced to that for the non-negative integers.
*}
@@ -28,7 +30,16 @@
"nat (number_of v) = number_of v"
unfolding nat_number_of_def ..
-context recpower
+
+subsection {* Special case: squares and cubes *}
+
+lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
+ by (simp add: nat_number_of_def)
+
+lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
+ by (simp add: nat_number_of_def)
+
+context power
begin
abbreviation (xsymbols)
@@ -43,6 +54,205 @@
end
+context monoid_mult
+begin
+
+lemma power2_eq_square: "a\<twosuperior> = a * a"
+ by (simp add: numeral_2_eq_2)
+
+lemma power3_eq_cube: "a ^ 3 = a * a * a"
+ by (simp add: numeral_3_eq_3 mult_assoc)
+
+lemma power_even_eq:
+ "a ^ (2*n) = (a ^ n) ^ 2"
+ by (subst OrderedGroup.mult_commute) (simp add: power_mult)
+
+lemma power_odd_eq:
+ "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
+ by (simp add: power_even_eq)
+
+end
+
+context semiring_1
+begin
+
+lemma zero_power2 [simp]: "0\<twosuperior> = 0"
+ by (simp add: power2_eq_square)
+
+lemma one_power2 [simp]: "1\<twosuperior> = 1"
+ by (simp add: power2_eq_square)
+
+end
+
+context comm_ring_1
+begin
+
+lemma power2_minus [simp]:
+ "(- a)\<twosuperior> = a\<twosuperior>"
+ by (simp add: power2_eq_square)
+
+text{*
+ We cannot prove general results about the numeral @{term "-1"},
+ so we have to use @{term "- 1"} instead.
+*}
+
+lemma power_minus1_even [simp]:
+ "(- 1) ^ (2*n) = 1"
+proof (induct n)
+ case 0 show ?case by simp
+next
+ case (Suc n) then show ?case by (simp add: power_add)
+qed
+
+lemma power_minus1_odd:
+ "(- 1) ^ Suc (2*n) = - 1"
+ by simp
+
+lemma power_minus_even [simp]:
+ "(-a) ^ (2*n) = a ^ (2*n)"
+ by (simp add: power_minus [of a])
+
+end
+
+context ordered_ring_strict
+begin
+
+lemma sum_squares_ge_zero:
+ "0 \<le> x * x + y * y"
+ by (intro add_nonneg_nonneg zero_le_square)
+
+lemma not_sum_squares_lt_zero:
+ "\<not> x * x + y * y < 0"
+ by (simp add: not_less sum_squares_ge_zero)
+
+lemma sum_squares_eq_zero_iff:
+ "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+ by (simp add: sum_nonneg_eq_zero_iff)
+
+lemma sum_squares_le_zero_iff:
+ "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+ by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
+
+lemma sum_squares_gt_zero_iff:
+ "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
+proof -
+ have "x * x + y * y \<noteq> 0 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
+ by (simp add: sum_squares_eq_zero_iff)
+ then have "0 \<noteq> x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
+ by auto
+ then show ?thesis
+ by (simp add: less_le sum_squares_ge_zero)
+qed
+
+end
+
+context ordered_semidom
+begin
+
+lemma power2_le_imp_le:
+ "x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
+ unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
+
+lemma power2_less_imp_less:
+ "x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
+ by (rule power_less_imp_less_base)
+
+lemma power2_eq_imp_eq:
+ "x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
+ unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
+
+end
+
+context ordered_idom
+begin
+
+lemma zero_eq_power2 [simp]:
+ "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
+ by (force simp add: power2_eq_square)
+
+lemma zero_le_power2 [simp]:
+ "0 \<le> a\<twosuperior>"
+ by (simp add: power2_eq_square)
+
+lemma zero_less_power2 [simp]:
+ "0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0"
+ by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
+
+lemma power2_less_0 [simp]:
+ "\<not> a\<twosuperior> < 0"
+ by (force simp add: power2_eq_square mult_less_0_iff)
+
+lemma abs_power2 [simp]:
+ "abs (a\<twosuperior>) = a\<twosuperior>"
+ by (simp add: power2_eq_square abs_mult abs_mult_self)
+
+lemma power2_abs [simp]:
+ "(abs a)\<twosuperior> = a\<twosuperior>"
+ by (simp add: power2_eq_square abs_mult_self)
+
+lemma odd_power_less_zero:
+ "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
+proof (induct n)
+ case 0
+ then show ?case by simp
+next
+ case (Suc n)
+ have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
+ by (simp add: mult_ac power_add power2_eq_square)
+ thus ?case
+ by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
+qed
+
+lemma odd_0_le_power_imp_0_le:
+ "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
+ using odd_power_less_zero [of a n]
+ by (force simp add: linorder_not_less [symmetric])
+
+lemma zero_le_even_power'[simp]:
+ "0 \<le> a ^ (2*n)"
+proof (induct n)
+ case 0
+ show ?case by (simp add: zero_le_one)
+next
+ case (Suc n)
+ have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
+ by (simp add: mult_ac power_add power2_eq_square)
+ thus ?case
+ by (simp add: Suc zero_le_mult_iff)
+qed
+
+lemma sum_power2_ge_zero:
+ "0 \<le> x\<twosuperior> + y\<twosuperior>"
+ unfolding power2_eq_square by (rule sum_squares_ge_zero)
+
+lemma not_sum_power2_lt_zero:
+ "\<not> x\<twosuperior> + y\<twosuperior> < 0"
+ unfolding power2_eq_square by (rule not_sum_squares_lt_zero)
+
+lemma sum_power2_eq_zero_iff:
+ "x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+ unfolding power2_eq_square by (rule sum_squares_eq_zero_iff)
+
+lemma sum_power2_le_zero_iff:
+ "x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+ unfolding power2_eq_square by (rule sum_squares_le_zero_iff)
+
+lemma sum_power2_gt_zero_iff:
+ "0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
+ unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
+
+end
+
+lemma power2_sum:
+ fixes x y :: "'a::number_ring"
+ shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
+ by (simp add: ring_distribs power2_eq_square)
+
+lemma power2_diff:
+ fixes x y :: "'a::number_ring"
+ shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
+ by (simp add: ring_distribs power2_eq_square)
+
subsection {* Predicate for negative binary numbers *}
@@ -115,11 +325,6 @@
lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
by (simp add: nat_numeral_1_eq_1)
-lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
-apply (unfold nat_number_of_def)
-apply (rule nat_2)
-done
-
subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
@@ -314,128 +519,10 @@
subsection{*Powers with Numeric Exponents*}
-text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
-We cannot prove general results about the numeral @{term "-1"}, so we have to
-use @{term "- 1"} instead.*}
-
-lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
- by (simp add: numeral_2_eq_2 Power.power_Suc)
-
-lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
- by (simp add: power2_eq_square)
-
-lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
- by (simp add: power2_eq_square)
-
-lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
- apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
- apply (erule ssubst)
- apply (simp add: power_Suc mult_ac)
- apply (unfold nat_number_of_def)
- apply (subst nat_eq_iff)
- apply simp
-done
-
text{*Squares of literal numerals will be evaluated.*}
-lemmas power2_eq_square_number_of =
+lemmas power2_eq_square_number_of [simp] =
power2_eq_square [of "number_of w", standard]
-declare power2_eq_square_number_of [simp]
-
-
-lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
- by (simp add: power2_eq_square)
-
-lemma zero_less_power2[simp]:
- "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
- by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
-
-lemma power2_less_0[simp]:
- fixes a :: "'a::{ordered_idom,recpower}"
- shows "~ (a\<twosuperior> < 0)"
-by (force simp add: power2_eq_square mult_less_0_iff)
-
-lemma zero_eq_power2[simp]:
- "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
- by (force simp add: power2_eq_square mult_eq_0_iff)
-
-lemma abs_power2[simp]:
- "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
- by (simp add: power2_eq_square abs_mult abs_mult_self)
-
-lemma power2_abs[simp]:
- "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
- by (simp add: power2_eq_square abs_mult_self)
-
-lemma power2_minus[simp]:
- "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
- by (simp add: power2_eq_square)
-
-lemma power2_le_imp_le:
- fixes x y :: "'a::{ordered_semidom,recpower}"
- shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
-unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
-lemma power2_less_imp_less:
- fixes x y :: "'a::{ordered_semidom,recpower}"
- shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
-by (rule power_less_imp_less_base)
-
-lemma power2_eq_imp_eq:
- fixes x y :: "'a::{ordered_semidom,recpower}"
- shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
-unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
-
-lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
-proof (induct n)
- case 0 show ?case by simp
-next
- case (Suc n) then show ?case by (simp add: power_Suc power_add)
-qed
-
-lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
- by (simp add: power_Suc)
-
-lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
- by (subst mult_commute) (simp add: power_mult)
-
-lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
- by (simp add: power_even_eq)
-
-lemma power_minus_even [simp]:
- "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
- by (simp add: power_minus [of a])
-
-lemma zero_le_even_power'[simp]:
- "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
-proof (induct "n")
- case 0
- show ?case by (simp add: zero_le_one)
-next
- case (Suc n)
- have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
- by (simp add: mult_ac power_add power2_eq_square)
- thus ?case
- by (simp add: prems zero_le_mult_iff)
-qed
-
-lemma odd_power_less_zero:
- "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
-proof (induct "n")
- case 0
- then show ?case by simp
-next
- case (Suc n)
- have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
- by (simp add: mult_ac power_add power2_eq_square)
- thus ?case
- by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
-qed
-
-lemma odd_0_le_power_imp_0_le:
- "0 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
-apply (insert odd_power_less_zero [of a n])
-apply (force simp add: linorder_not_less [symmetric])
-done
text{*Simprules for comparisons where common factors can be cancelled.*}
lemmas zero_compare_simps =
@@ -621,7 +708,7 @@
text{*For arbitrary rings*}
lemma power_number_of_even:
- fixes z :: "'a::{number_ring,recpower}"
+ fixes z :: "'a::number_ring"
shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
unfolding Let_def nat_number_of_def number_of_Bit0
apply (rule_tac x = "number_of w" in spec, clarify)
@@ -630,7 +717,7 @@
done
lemma power_number_of_odd:
- fixes z :: "'a::{number_ring,recpower}"
+ fixes z :: "'a::number_ring"
shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
then (let w = z ^ (number_of w) in z * w * w) else 1)"
unfolding Let_def nat_number_of_def number_of_Bit1
@@ -697,11 +784,11 @@
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
by (simp add: Let_def)
-lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
-by (simp add: power_mult power_Suc);
+lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})"
+ by (simp only: number_of_Min power_minus1_even)
-lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
-by (simp add: power_mult power_Suc);
+lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring})"
+ by (simp only: number_of_Min power_minus1_odd)
subsection{*Literal arithmetic and @{term of_nat}*}
--- a/src/HOL/NthRoot.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/NthRoot.thy Tue Apr 28 19:15:50 2009 +0200
@@ -565,16 +565,6 @@
lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
by (simp add: power2_eq_square [symmetric])
-lemma power2_sum:
- fixes x y :: "'a::{number_ring,recpower}"
- shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
-by (simp add: ring_distribs power2_eq_square)
-
-lemma power2_diff:
- fixes x y :: "'a::{number_ring,recpower}"
- shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
-by (simp add: ring_distribs power2_eq_square)
-
lemma real_sqrt_sum_squares_triangle_ineq:
"sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
apply (rule power2_le_imp_le, simp)
--- a/src/HOL/OrderedGroup.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Tue Apr 28 19:15:50 2009 +0200
@@ -637,6 +637,27 @@
lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
by (simp add: algebra_simps)
+lemma sum_nonneg_eq_zero_iff:
+ assumes x: "0 \<le> x" and y: "0 \<le> y"
+ shows "(x + y = 0) = (x = 0 \<and> y = 0)"
+proof -
+ have "x + y = 0 \<Longrightarrow> x = 0"
+ proof -
+ from y have "x + 0 \<le> x + y" by (rule add_left_mono)
+ also assume "x + y = 0"
+ finally have "x \<le> 0" by simp
+ then show "x = 0" using x by (rule antisym)
+ qed
+ moreover have "x + y = 0 \<Longrightarrow> y = 0"
+ proof -
+ from x have "0 + y \<le> x + y" by (rule add_right_mono)
+ also assume "x + y = 0"
+ finally have "y \<le> 0" by simp
+ then show "y = 0" using y by (rule antisym)
+ qed
+ ultimately show ?thesis by auto
+qed
+
text{*Legacy - use @{text algebra_simps} *}
lemmas group_simps[noatp] = algebra_simps
--- a/src/HOL/Parity.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Parity.thy Tue Apr 28 19:15:50 2009 +0200
@@ -178,7 +178,7 @@
subsection {* Parity and powers *}
lemma minus_one_even_odd_power:
- "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) &
+ "(even x --> (- 1::'a::{comm_ring_1})^x = 1) &
(odd x --> (- 1::'a)^x = - 1)"
apply (induct x)
apply (rule conjI)
@@ -188,37 +188,37 @@
done
lemma minus_one_even_power [simp]:
- "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1"
+ "even x ==> (- 1::'a::{comm_ring_1})^x = 1"
using minus_one_even_odd_power by blast
lemma minus_one_odd_power [simp]:
- "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1"
+ "odd x ==> (- 1::'a::{comm_ring_1})^x = - 1"
using minus_one_even_odd_power by blast
lemma neg_one_even_odd_power:
- "(even x --> (-1::'a::{number_ring,recpower})^x = 1) &
+ "(even x --> (-1::'a::{number_ring})^x = 1) &
(odd x --> (-1::'a)^x = -1)"
apply (induct x)
apply (simp, simp add: power_Suc)
done
lemma neg_one_even_power [simp]:
- "even x ==> (-1::'a::{number_ring,recpower})^x = 1"
+ "even x ==> (-1::'a::{number_ring})^x = 1"
using neg_one_even_odd_power by blast
lemma neg_one_odd_power [simp]:
- "odd x ==> (-1::'a::{number_ring,recpower})^x = -1"
+ "odd x ==> (-1::'a::{number_ring})^x = -1"
using neg_one_even_odd_power by blast
lemma neg_power_if:
- "(-x::'a::{comm_ring_1,recpower}) ^ n =
+ "(-x::'a::{comm_ring_1}) ^ n =
(if even n then (x ^ n) else -(x ^ n))"
apply (induct n)
apply (simp_all split: split_if_asm add: power_Suc)
done
lemma zero_le_even_power: "even n ==>
- 0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n"
+ 0 <= (x::'a::{ordered_ring_strict,monoid_mult}) ^ n"
apply (simp add: even_nat_equiv_def2)
apply (erule exE)
apply (erule ssubst)
@@ -227,12 +227,12 @@
done
lemma zero_le_odd_power: "odd n ==>
- (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
+ (0 <= (x::'a::{ordered_idom}) ^ n) = (0 <= x)"
apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
done
-lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) =
+lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{ordered_idom}) ^ n) =
(even n | (odd n & 0 <= x))"
apply auto
apply (subst zero_le_odd_power [symmetric])
@@ -240,19 +240,19 @@
apply (erule zero_le_even_power)
done
-lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) =
+lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{ordered_idom}) ^ n) =
(n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
unfolding order_less_le zero_le_power_eq by auto
-lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
+lemma power_less_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n < 0) =
(odd n & x < 0)"
apply (subst linorder_not_le [symmetric])+
apply (subst zero_le_power_eq)
apply auto
done
-lemma power_le_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) =
+lemma power_le_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n <= 0) =
(n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))"
apply (subst linorder_not_less [symmetric])+
apply (subst zero_less_power_eq)
@@ -260,7 +260,7 @@
done
lemma power_even_abs: "even n ==>
- (abs (x::'a::{recpower,ordered_idom}))^n = x^n"
+ (abs (x::'a::{ordered_idom}))^n = x^n"
apply (subst power_abs [symmetric])
apply (simp add: zero_le_even_power)
done
@@ -269,18 +269,18 @@
by (induct n) auto
lemma power_minus_even [simp]: "even n ==>
- (- x)^n = (x^n::'a::{recpower,comm_ring_1})"
+ (- x)^n = (x^n::'a::{comm_ring_1})"
apply (subst power_minus)
apply simp
done
lemma power_minus_odd [simp]: "odd n ==>
- (- x)^n = - (x^n::'a::{recpower,comm_ring_1})"
+ (- x)^n = - (x^n::'a::{comm_ring_1})"
apply (subst power_minus)
apply simp
done
-lemma power_mono_even: fixes x y :: "'a :: {recpower, ordered_idom}"
+lemma power_mono_even: fixes x y :: "'a :: {ordered_idom}"
assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>"
shows "x^n \<le> y^n"
proof -
@@ -292,7 +292,7 @@
lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
-lemma power_mono_odd: fixes x y :: "'a :: {recpower, ordered_idom}"
+lemma power_mono_odd: fixes x y :: "'a :: {ordered_idom}"
assumes "odd n" and "x \<le> y"
shows "x^n \<le> y^n"
proof (cases "y < 0")
@@ -406,11 +406,11 @@
subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
lemma even_power_le_0_imp_0:
- "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"
+ "a ^ (2*k) \<le> (0::'a::{ordered_idom}) ==> a=0"
by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)
lemma zero_le_power_iff[presburger]:
- "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)"
+ "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom}) | even n)"
proof cases
assume even: "even n"
then obtain k where "n = 2*k"
--- a/src/HOL/Rational.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Rational.thy Tue Apr 28 19:15:50 2009 +0200
@@ -90,7 +90,7 @@
and "\<And>a c. Fract 0 a = Fract 0 c"
by (simp_all add: Fract_def)
-instantiation rat :: "{comm_ring_1, recpower}"
+instantiation rat :: comm_ring_1
begin
definition
@@ -185,9 +185,6 @@
by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
next
show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat)
-next
- fix q :: rat show "q * 1 = q"
- by (cases q) (simp add: One_rat_def eq_rat)
qed
end
@@ -656,7 +653,7 @@
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
lemma of_rat_power:
- "(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n"
+ "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n"
by (induct n) (simp_all add: of_rat_mult)
lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
@@ -816,7 +813,7 @@
done
lemma Rats_power [simp]:
- fixes a :: "'a::{field_char_0,recpower}"
+ fixes a :: "'a::field_char_0"
shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
@@ -837,6 +834,8 @@
"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 18:42:26 2009 +0200
+++ b/src/HOL/RealPow.thy Tue Apr 28 19:15:50 2009 +0200
@@ -83,75 +83,6 @@
declare power_real_number_of [of _ "number_of w", standard, simp]
-subsection {* Properties of Squares *}
-
-lemma sum_squares_ge_zero:
- fixes x y :: "'a::ordered_ring_strict"
- shows "0 \<le> x * x + y * y"
-by (intro add_nonneg_nonneg zero_le_square)
-
-lemma not_sum_squares_lt_zero:
- fixes x y :: "'a::ordered_ring_strict"
- shows "\<not> x * x + y * y < 0"
-by (simp add: linorder_not_less sum_squares_ge_zero)
-
-lemma sum_nonneg_eq_zero_iff:
- fixes x y :: "'a::pordered_ab_group_add"
- assumes x: "0 \<le> x" and y: "0 \<le> y"
- shows "(x + y = 0) = (x = 0 \<and> y = 0)"
-proof (auto)
- from y have "x + 0 \<le> x + y" by (rule add_left_mono)
- also assume "x + y = 0"
- finally have "x \<le> 0" by simp
- thus "x = 0" using x by (rule order_antisym)
-next
- from x have "0 + y \<le> x + y" by (rule add_right_mono)
- also assume "x + y = 0"
- finally have "y \<le> 0" by simp
- thus "y = 0" using y by (rule order_antisym)
-qed
-
-lemma sum_squares_eq_zero_iff:
- fixes x y :: "'a::ordered_ring_strict"
- shows "(x * x + y * y = 0) = (x = 0 \<and> y = 0)"
-by (simp add: sum_nonneg_eq_zero_iff)
-
-lemma sum_squares_le_zero_iff:
- fixes x y :: "'a::ordered_ring_strict"
- shows "(x * x + y * y \<le> 0) = (x = 0 \<and> y = 0)"
-by (simp add: order_le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
-
-lemma sum_squares_gt_zero_iff:
- fixes x y :: "'a::ordered_ring_strict"
- shows "(0 < x * x + y * y) = (x \<noteq> 0 \<or> y \<noteq> 0)"
-by (simp add: order_less_le sum_squares_ge_zero sum_squares_eq_zero_iff)
-
-lemma sum_power2_ge_zero:
- fixes x y :: "'a::{ordered_idom,recpower}"
- shows "0 \<le> x\<twosuperior> + y\<twosuperior>"
-unfolding power2_eq_square by (rule sum_squares_ge_zero)
-
-lemma not_sum_power2_lt_zero:
- fixes x y :: "'a::{ordered_idom,recpower}"
- shows "\<not> x\<twosuperior> + y\<twosuperior> < 0"
-unfolding power2_eq_square by (rule not_sum_squares_lt_zero)
-
-lemma sum_power2_eq_zero_iff:
- fixes x y :: "'a::{ordered_idom,recpower}"
- shows "(x\<twosuperior> + y\<twosuperior> = 0) = (x = 0 \<and> y = 0)"
-unfolding power2_eq_square by (rule sum_squares_eq_zero_iff)
-
-lemma sum_power2_le_zero_iff:
- fixes x y :: "'a::{ordered_idom,recpower}"
- shows "(x\<twosuperior> + y\<twosuperior> \<le> 0) = (x = 0 \<and> y = 0)"
-unfolding power2_eq_square by (rule sum_squares_le_zero_iff)
-
-lemma sum_power2_gt_zero_iff:
- fixes x y :: "'a::{ordered_idom,recpower}"
- shows "(0 < x\<twosuperior> + y\<twosuperior>) = (x \<noteq> 0 \<or> y \<noteq> 0)"
-unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
-
-
subsection{* Squares of Reals *}
lemma real_two_squares_add_zero_iff [simp]:
--- a/src/HOL/RealVector.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/RealVector.thy Tue Apr 28 19:15:50 2009 +0200
@@ -259,7 +259,7 @@
by (simp add: divide_inverse)
lemma of_real_power [simp]:
- "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
+ "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n"
by (induct n) simp_all
lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
@@ -389,7 +389,7 @@
done
lemma Reals_power [simp]:
- fixes a :: "'a::{real_algebra_1,recpower}"
+ fixes a :: "'a::{real_algebra_1}"
shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
@@ -613,7 +613,7 @@
by (simp add: divide_inverse norm_mult norm_inverse)
lemma norm_power_ineq:
- fixes x :: "'a::{real_normed_algebra_1,recpower}"
+ fixes x :: "'a::{real_normed_algebra_1}"
shows "norm (x ^ n) \<le> norm x ^ n"
proof (induct n)
case 0 show "norm (x ^ 0) \<le> norm x ^ 0" by simp
@@ -628,7 +628,7 @@
qed
lemma norm_power:
- fixes x :: "'a::{real_normed_div_algebra,recpower}"
+ fixes x :: "'a::{real_normed_div_algebra}"
shows "norm (x ^ n) = norm x ^ n"
by (induct n) (simp_all add: norm_mult)
--- a/src/HOL/SEQ.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/SEQ.thy Tue Apr 28 19:15:50 2009 +0200
@@ -487,7 +487,7 @@
by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
lemma LIMSEQ_pow:
- fixes a :: "'a::{real_normed_algebra,recpower}"
+ fixes a :: "'a::{power, real_normed_algebra}"
shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
@@ -1394,7 +1394,7 @@
qed
lemma LIMSEQ_power_zero:
- fixes x :: "'a::{real_normed_algebra_1,recpower}"
+ fixes x :: "'a::{real_normed_algebra_1}"
shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)
--- a/src/HOL/Series.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Series.thy Tue Apr 28 19:15:50 2009 +0200
@@ -331,7 +331,7 @@
lemmas sumr_geometric = geometric_sum [where 'a = real]
lemma geometric_sums:
- fixes x :: "'a::{real_normed_field,recpower}"
+ fixes x :: "'a::{real_normed_field}"
shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) sums (1 / (1 - x))"
proof -
assume less_1: "norm x < 1"
@@ -348,7 +348,7 @@
qed
lemma summable_geometric:
- fixes x :: "'a::{real_normed_field,recpower}"
+ fixes x :: "'a::{real_normed_field}"
shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
by (rule geometric_sums [THEN sums_summable])
@@ -434,7 +434,7 @@
text{*Summability of geometric series for real algebras*}
lemma complete_algebra_summable_geometric:
- fixes x :: "'a::{real_normed_algebra_1,banach,recpower}"
+ fixes x :: "'a::{real_normed_algebra_1,banach}"
shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
proof (rule summable_comparison_test)
show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n"
--- a/src/HOL/SetInterval.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/SetInterval.thy Tue Apr 28 19:15:50 2009 +0200
@@ -855,7 +855,7 @@
lemma geometric_sum:
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
- (x ^ n - 1) / (x - 1::'a::{field, recpower})"
+ (x ^ n - 1) / (x - 1::'a::{field})"
by (induct "n") (simp_all add:field_simps power_Suc)
subsection {* The formula for arithmetic sums *}
--- a/src/HOL/Transcendental.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Transcendental.thy Tue Apr 28 19:15:50 2009 +0200
@@ -14,7 +14,7 @@
subsection {* Properties of Power Series *}
lemma lemma_realpow_diff:
- fixes y :: "'a::recpower"
+ fixes y :: "'a::monoid_mult"
shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
proof -
assume "p \<le> n"
@@ -23,14 +23,14 @@
qed
lemma lemma_realpow_diff_sumr:
- fixes y :: "'a::{recpower,comm_semiring_0}" shows
+ fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows
"(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =
y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
del: setsum_op_ivl_Suc cong: strong_setsum_cong)
lemma lemma_realpow_diff_sumr2:
- fixes y :: "'a::{recpower,comm_ring}" shows
+ fixes y :: "'a::{comm_ring,monoid_mult}" shows
"x ^ (Suc n) - y ^ (Suc n) =
(x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
apply (induct n, simp)
@@ -56,7 +56,7 @@
x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
lemma powser_insidea:
- fixes x z :: "'a::{real_normed_field,banach,recpower}"
+ fixes x z :: "'a::{real_normed_field,banach}"
assumes 1: "summable (\<lambda>n. f n * x ^ n)"
assumes 2: "norm z < norm x"
shows "summable (\<lambda>n. norm (f n * z ^ n))"
@@ -108,7 +108,7 @@
qed
lemma powser_inside:
- fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows
+ fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows
"[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]
==> summable (%n. f(n) * (z ^ n))"
by (rule powser_insidea [THEN summable_norm_cancel])
@@ -347,7 +347,7 @@
done
lemma lemma_termdiff1:
- fixes z :: "'a :: {recpower,comm_ring}" shows
+ fixes z :: "'a :: {monoid_mult,comm_ring}" shows
"(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
(\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
by(auto simp add: algebra_simps power_add [symmetric] cong: strong_setsum_cong)
@@ -357,7 +357,7 @@
by (simp add: setsum_subtractf)
lemma lemma_termdiff2:
- fixes h :: "'a :: {recpower,field}"
+ fixes h :: "'a :: {field}"
assumes h: "h \<noteq> 0" shows
"((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
@@ -393,7 +393,7 @@
done
lemma lemma_termdiff3:
- fixes h z :: "'a::{real_normed_field,recpower}"
+ fixes h z :: "'a::{real_normed_field}"
assumes 1: "h \<noteq> 0"
assumes 2: "norm z \<le> K"
assumes 3: "norm (z + h) \<le> K"
@@ -433,7 +433,7 @@
qed
lemma lemma_termdiff4:
- fixes f :: "'a::{real_normed_field,recpower} \<Rightarrow>
+ fixes f :: "'a::{real_normed_field} \<Rightarrow>
'b::real_normed_vector"
assumes k: "0 < (k::real)"
assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
@@ -478,7 +478,7 @@
qed
lemma lemma_termdiff5:
- fixes g :: "'a::{recpower,real_normed_field} \<Rightarrow>
+ fixes g :: "'a::{real_normed_field} \<Rightarrow>
nat \<Rightarrow> 'b::banach"
assumes k: "0 < (k::real)"
assumes f: "summable f"
@@ -507,7 +507,7 @@
text{* FIXME: Long proofs*}
lemma termdiffs_aux:
- fixes x :: "'a::{recpower,real_normed_field,banach}"
+ fixes x :: "'a::{real_normed_field,banach}"
assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
assumes 2: "norm x < norm K"
shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
@@ -572,7 +572,7 @@
qed
lemma termdiffs:
- fixes K x :: "'a::{recpower,real_normed_field,banach}"
+ fixes K x :: "'a::{real_normed_field,banach}"
assumes 1: "summable (\<lambda>n. c n * K ^ n)"
assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
@@ -822,11 +822,11 @@
subsection {* Exponential Function *}
definition
- exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where
+ exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
"exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
lemma summable_exp_generic:
- fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
+ fixes x :: "'a::{real_normed_algebra_1,banach}"
defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
shows "summable S"
proof -
@@ -856,7 +856,7 @@
qed
lemma summable_norm_exp:
- fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
+ fixes x :: "'a::{real_normed_algebra_1,banach}"
shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
proof (rule summable_norm_comparison_test [OF exI, rule_format])
show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
@@ -901,7 +901,7 @@
subsubsection {* Properties of the Exponential Function *}
lemma powser_zero:
- fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}"
+ fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
shows "(\<Sum>n. f n * 0 ^ n) = f 0"
proof -
have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
@@ -918,7 +918,7 @@
del: setsum_cl_ivl_Suc)
lemma exp_series_add:
- fixes x y :: "'a::{real_field,recpower}"
+ fixes x y :: "'a::{real_field}"
defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
proof (induct n)
--- a/src/HOL/Word/Num_Lemmas.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy Tue Apr 28 19:15:50 2009 +0200
@@ -45,10 +45,6 @@
apply (simp add: number_of_eq nat_diff_distrib [symmetric])
done
-lemma of_int_power:
- "of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})"
- by (induct n) (auto simp add: power_Suc)
-
lemma zless2: "0 < (2 :: int)" by arith
lemmas zless2p [simp] = zless2 [THEN zero_less_power]
--- a/src/HOL/Word/WordArith.thy Tue Apr 28 18:42:26 2009 +0200
+++ b/src/HOL/Word/WordArith.thy Tue Apr 28 19:15:50 2009 +0200
@@ -790,15 +790,14 @@
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 ..
instance word :: (len0) order ..
-instance word :: (len) recpower
- by (intro_classes) simp_all
-
(* note that iszero_def is only for class comm_semiring_1_cancel,
which requires word length >= 1, ie 'a :: len word *)
lemma zero_bintrunc: