# HG changeset patch # User haftmann # Date 1240938950 -7200 # Node ID 9999a77590c368bcd203f32d3f194b49a81da082 # Parent 69a476d6fea6351450c34964541c5170a099eeff# Parent 0a38079e789b1f1aafbbad342e7034e25012fedb merged diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/Deriv.thy --- 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 \ 'a::{real_normed_field,recpower}" + fixes f :: "'a \ 'a::{real_normed_field}" assumes f: "DERIV f x :> D" shows "DERIV (\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 \ 'a::{real_normed_field,recpower}" + fixes f :: "'a \ 'a::{real_normed_field}" assumes f: "DERIV f x :> D" shows "DERIV (\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 \ 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) \ 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) \ 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} \ 'a" + fixes f :: "'a::{real_normed_field} \ 'a" assumes "f differentiable x" shows "(\x. f x ^ n) differentiable x" by (induct n, simp, simp add: prems) diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/Finite_Set.thy --- 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 ==> (\x\ A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)" +lemma setprod_constant: "finite A ==> (\x\ 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 (\k. if k=a then b k else c) S = (if a \ S then (b a ::'a::{comm_monoid_mult, recpower}) * c^ (card S - 1) else c^ card S)" + shows "setprod (\k. if k=a then b k else c) S = (if a \ S then (b a ::'a::{comm_monoid_mult}) * c^ (card S - 1) else c^ card S)" proof- let ?f = "(\k. if k=a then b k else c)" {assume a: "a \ S" diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/Groebner_Basis.thy --- 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 \ z" hence ynz': "y - z \ 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" diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/Int.thy --- 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 \ 'a" -where +definition of_int :: "int \ 'a" where [code del]: "of_int z = contents (\(i, j) \ 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) \ 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 diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/Lim.thy --- 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 \ 'b::{recpower,real_normed_algebra}" + fixes f :: "'a::real_normed_vector \ 'b::{power,real_normed_algebra}" assumes f: "f -- a --> l" shows "(\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 \ 'b::{recpower,real_normed_algebra}" + fixes f :: "'a::real_normed_vector \ 'b::{power,real_normed_algebra}" shows "isCont f a \ isCont (\x. f x ^ n) a" unfolding isCont_def by (rule LIM_power) diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/NSA/HDeriv.thy --- 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 \ 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 \ 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) \ 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) \ 0 |] ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))" diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/NSA/HSEQ.thy --- 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) diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/NSA/HyperDef.thy --- 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 \ HFinite ==> x ^ n \ 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]: - "\n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0" + "\n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0" by transfer simp lemma hyperpow_not_zero: - "\r n. r \ (0::'a::{recpower,field} star) ==> r pow n \ 0" + "\r n. r \ (0::'a::{field} star) ==> r pow n \ 0" by transfer (rule field_power_not_zero) lemma hyperpow_inverse: - "\r n. r \ (0::'a::{recpower,division_by_zero,field} star) + "\r n. r \ (0::'a::{division_by_zero,field} star) \ inverse (r pow n) = (inverse r) pow n" by transfer (rule power_inverse) - + lemma hyperpow_hrabs: - "\r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)" + "\r n. abs (r::'a::{ordered_idom} star) pow n = abs (r pow n)" by transfer (rule power_abs [symmetric]) lemma hyperpow_add: - "\r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)" + "\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: - "\r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r" -by transfer (simp add: power_Suc) + "\r. (r::'a::monoid_mult star) pow ((1::hypnat) + (1::hypnat)) = r * r" +by transfer simp lemma hyperpow_gt_zero: - "\r n. (0::'a::{recpower,ordered_semidom} star) < r \ 0 < r pow n" + "\r n. (0::'a::{ordered_semidom} star) < r \ 0 < r pow n" by transfer (rule zero_less_power) lemma hyperpow_ge_zero: - "\r n. (0::'a::{recpower,ordered_semidom} star) \ r \ 0 \ r pow n" + "\r n. (0::'a::{ordered_semidom} star) \ r \ 0 \ r pow n" by transfer (rule zero_le_power) lemma hyperpow_le: - "\x y n. \(0::'a::{recpower,ordered_semidom} star) < x; x \ y\ + "\x y n. \(0::'a::{ordered_semidom} star) < x; x \ y\ \ x pow n \ y pow n" by transfer (rule power_mono [OF _ order_less_imp_le]) lemma hyperpow_eq_one [simp]: - "\n. 1 pow n = (1::'a::recpower star)" + "\n. 1 pow n = (1::'a::monoid_mult star)" by transfer (rule power_one) lemma hrabs_hyperpow_minus_one [simp]: - "\n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)" + "\n. abs(-1 pow n) = (1::'a::{number_ring,ordered_idom} star)" by transfer (rule abs_power_minus_one) lemma hyperpow_mult: - "\r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n + "\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) \ r pow (1 + 1)" + "(0::'a::{monoid_mult,ordered_ring_strict} star) \ 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\x"}*} @@ -511,11 +511,11 @@ by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) lemma hyperpow_two_gt_one: - "\r::'a::{recpower,ordered_semidom} star. 1 < r \ 1 < r pow (1 + 1)" + "\r::'a::{ordered_semidom} star. 1 < r \ 1 < r pow (1 + 1)" by transfer (simp add: power_gt1 del: power_Suc) lemma hyperpow_two_ge_one: - "\r::'a::{recpower,ordered_semidom} star. 1 \ r \ 1 \ r pow (1 + 1)" + "\r::'a::{ordered_semidom} star. 1 \ r \ 1 \ r pow (1 + 1)" by transfer (simp add: one_le_power del: power_Suc) lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \ 2 pow n" @@ -565,7 +565,7 @@ lemma of_hypreal_hyperpow: "\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 diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/NSA/NSA.thy --- 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: - "\(x::'a::{real_normed_div_algebra,recpower} star) n. + "\(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 \ HFinite ==> x ^ n \ HFinite" -apply (induct_tac "n") +apply (induct n) apply (auto simp add: power_Suc intro: HFinite_mult) done lemma HFinite_bounded: "[|(x::hypreal) \ HFinite; y \ x; 0 \ y |] ==> y \ HFinite" -apply (case_tac "x \ 0") +apply (cases "x \ 0") apply (drule_tac y = x in order_trans) apply (drule_tac [2] order_antisym) apply (auto simp add: linorder_not_le) diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/NSA/NSComplex.thy --- 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]: - "\n. 0 pow (hSuc n) = (0::'a::{recpower,semiring_0} star)" + "\n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)" by transfer (rule power_0_Suc) lemma hcpow_not_zero [simp,intro]: diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/Nat_Numeral.thy --- 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\ = 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\ = 0" + by (simp add: power2_eq_square) + +lemma one_power2 [simp]: "1\ = 1" + by (simp add: power2_eq_square) + +end + +context comm_ring_1 +begin + +lemma power2_minus [simp]: + "(- a)\ = a\" + 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 \ x * x + y * y" + by (intro add_nonneg_nonneg zero_le_square) + +lemma not_sum_squares_lt_zero: + "\ 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 \ x = 0 \ y = 0" + by (simp add: sum_nonneg_eq_zero_iff) + +lemma sum_squares_le_zero_iff: + "x * x + y * y \ 0 \ x = 0 \ 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 \ x \ 0 \ y \ 0" +proof - + have "x * x + y * y \ 0 \ x \ 0 \ y \ 0" + by (simp add: sum_squares_eq_zero_iff) + then have "0 \ x * x + y * y \ x \ 0 \ y \ 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\ \ y\ \ 0 \ y \ x \ y" + unfolding numeral_2_eq_2 by (rule power_le_imp_le_base) + +lemma power2_less_imp_less: + "x\ < y\ \ 0 \ y \ x < y" + by (rule power_less_imp_less_base) + +lemma power2_eq_imp_eq: + "x\ = y\ \ 0 \ x \ 0 \ y \ 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\ = 0 \ a = 0" + by (force simp add: power2_eq_square) + +lemma zero_le_power2 [simp]: + "0 \ a\" + by (simp add: power2_eq_square) + +lemma zero_less_power2 [simp]: + "0 < a\ \ a \ 0" + by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) + +lemma power2_less_0 [simp]: + "\ a\ < 0" + by (force simp add: power2_eq_square mult_less_0_iff) + +lemma abs_power2 [simp]: + "abs (a\) = a\" + by (simp add: power2_eq_square abs_mult abs_mult_self) + +lemma power2_abs [simp]: + "(abs a)\ = a\" + by (simp add: power2_eq_square abs_mult_self) + +lemma odd_power_less_zero: + "a < 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: Suc mult_less_0_iff mult_neg_neg) +qed + +lemma odd_0_le_power_imp_0_le: + "0 \ a ^ Suc (2*n) \ 0 \ a" + using odd_power_less_zero [of a n] + by (force simp add: linorder_not_less [symmetric]) + +lemma zero_le_even_power'[simp]: + "0 \ 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 \ x\ + y\" + unfolding power2_eq_square by (rule sum_squares_ge_zero) + +lemma not_sum_power2_lt_zero: + "\ x\ + y\ < 0" + unfolding power2_eq_square by (rule not_sum_squares_lt_zero) + +lemma sum_power2_eq_zero_iff: + "x\ + y\ = 0 \ x = 0 \ y = 0" + unfolding power2_eq_square by (rule sum_squares_eq_zero_iff) + +lemma sum_power2_le_zero_iff: + "x\ + y\ \ 0 \ x = 0 \ y = 0" + unfolding power2_eq_square by (rule sum_squares_le_zero_iff) + +lemma sum_power2_gt_zero_iff: + "0 < x\ + y\ \ x \ 0 \ y \ 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)\ = x\ + y\ + 2 * x * y" + by (simp add: ring_distribs power2_eq_square) + +lemma power2_diff: + fixes x y :: "'a::number_ring" + shows "(x - y)\ = x\ + y\ - 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)\ = a * a" - by (simp add: numeral_2_eq_2 Power.power_Suc) - -lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\ = 0" - by (simp add: power2_eq_square) - -lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\ = 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 \ (a\::'a::{ordered_idom,recpower})" - by (simp add: power2_eq_square) - -lemma zero_less_power2[simp]: - "(0 < a\) = (a \ (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\ < 0)" -by (force simp add: power2_eq_square mult_less_0_iff) - -lemma zero_eq_power2[simp]: - "(a\ = 0) = (a = (0::'a::{ordered_idom,recpower}))" - by (force simp add: power2_eq_square mult_eq_0_iff) - -lemma abs_power2[simp]: - "abs(a\) = (a\::'a::{ordered_idom,recpower})" - by (simp add: power2_eq_square abs_mult abs_mult_self) - -lemma power2_abs[simp]: - "(abs a)\ = (a\::'a::{ordered_idom,recpower})" - by (simp add: power2_eq_square abs_mult_self) - -lemma power2_minus[simp]: - "(- a)\ = (a\::'a::{comm_ring_1,recpower})" - by (simp add: power2_eq_square) - -lemma power2_le_imp_le: - fixes x y :: "'a::{ordered_semidom,recpower}" - shows "\x\ \ y\; 0 \ y\ \ x \ 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 "\x\ < y\; 0 \ y\ \ x < y" -by (rule power_less_imp_less_base) - -lemma power2_eq_imp_eq: - fixes x y :: "'a::{ordered_semidom,recpower}" - shows "\x\ = y\; 0 \ x; 0 \ y\ \ 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 \ (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 \ a ^ Suc(2*n) ==> 0 \ (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}*} diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/NthRoot.thy --- 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 \ 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)\ = x\ + y\ + 2 * x * y" -by (simp add: ring_distribs power2_eq_square) - -lemma power2_diff: - fixes x y :: "'a::{number_ring,recpower}" - shows "(x - y)\ = x\ + y\ - 2 * x * y" -by (simp add: ring_distribs power2_eq_square) - lemma real_sqrt_sum_squares_triangle_ineq: "sqrt ((a + c)\ + (b + d)\) \ sqrt (a\ + b\) + sqrt (c\ + d\)" apply (rule power2_le_imp_le, simp) diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/OrderedGroup.thy --- 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 \ b \ a - b \ 0" by (simp add: algebra_simps) +lemma sum_nonneg_eq_zero_iff: + assumes x: "0 \ x" and y: "0 \ y" + shows "(x + y = 0) = (x = 0 \ y = 0)" +proof - + have "x + y = 0 \ x = 0" + proof - + from y have "x + 0 \ x + y" by (rule add_left_mono) + also assume "x + y = 0" + finally have "x \ 0" by simp + then show "x = 0" using x by (rule antisym) + qed + moreover have "x + y = 0 \ y = 0" + proof - + from x have "0 + y \ x + y" by (rule add_right_mono) + also assume "x + y = 0" + finally have "y \ 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 diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/Parity.thy --- 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 "\x\ \ \y\" shows "x^n \ y^n" proof - @@ -292,7 +292,7 @@ lemma odd_pos: "odd (n::nat) \ 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 \ y" shows "x^n \ y^n" proof (cases "y < 0") @@ -406,11 +406,11 @@ subsection {* An Equivalence for @{term [source] "0 \ a^n"} *} lemma even_power_le_0_imp_0: - "a ^ (2*k) \ (0::'a::{ordered_idom,recpower}) ==> a=0" + "a ^ (2*k) \ (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 \ a^n) = (0 \ (a::'a::{ordered_idom,recpower}) | even n)" + "(0 \ a^n) = (0 \ (a::'a::{ordered_idom}) | even n)" proof cases assume even: "even n" then obtain k where "n = 2*k" diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/Rational.thy --- 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 "\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) \ 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 \ Rats \ a ^ n \ Rats" apply (auto simp add: Rats_def) apply (rule range_eqI) @@ -837,6 +834,8 @@ "q \ \ \ (\r. P (of_rat r)) \ P q" by (rule Rats_cases) auto +instance rat :: recpower .. + subsection {* Implementation of rational numbers as pairs of integers *} diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/RealPow.thy --- 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 \ 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 "\ 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 \ x" and y: "0 \ y" - shows "(x + y = 0) = (x = 0 \ y = 0)" -proof (auto) - from y have "x + 0 \ x + y" by (rule add_left_mono) - also assume "x + y = 0" - finally have "x \ 0" by simp - thus "x = 0" using x by (rule order_antisym) -next - from x have "0 + y \ x + y" by (rule add_right_mono) - also assume "x + y = 0" - finally have "y \ 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 \ 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 \ 0) = (x = 0 \ 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 \ 0 \ y \ 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 \ x\ + y\" -unfolding power2_eq_square by (rule sum_squares_ge_zero) - -lemma not_sum_power2_lt_zero: - fixes x y :: "'a::{ordered_idom,recpower}" - shows "\ x\ + y\ < 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\ + y\ = 0) = (x = 0 \ 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\ + y\ \ 0) = (x = 0 \ 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\ + y\) = (x \ 0 \ y \ 0)" -unfolding power2_eq_square by (rule sum_squares_gt_zero_iff) - - subsection{* Squares of Reals *} lemma real_two_squares_add_zero_iff [simp]: diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/RealVector.thy --- 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 \ Reals \ a ^ n \ 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) \ norm x ^ n" proof (induct n) case 0 show "norm (x ^ 0) \ 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) diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/SEQ.thy --- 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 \ (\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 \ (\n. x ^ n) ----> 0" apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le) diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/Series.thy --- 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 \ (\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 \ summable (\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 \ summable (\n. x ^ n)" proof (rule summable_comparison_test) show "\N. \n\N. norm (x ^ n) \ norm x ^ n" diff -r 69a476d6fea6 -r 9999a77590c3 src/HOL/SetInterval.thy --- 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 ==> (\i=0.. n \ y ^ (Suc n - p) = (y ^ (n - p)) * y" proof - assume "p \ 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 "(\p=0..p=0..p=0..z\ < \x\"}.*} lemma powser_insidea: - fixes x z :: "'a::{real_normed_field,banach,recpower}" + fixes x z :: "'a::{real_normed_field,banach}" assumes 1: "summable (\n. f n * x ^ n)" assumes 2: "norm z < norm x" shows "summable (\n. norm (f n * z ^ n))" @@ -108,7 +108,7 @@ qed lemma powser_inside: - fixes f :: "nat \ 'a::{real_normed_field,banach,recpower}" shows + fixes f :: "nat \ '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 "(\p=0..p=0.. 0" shows "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) = h * (\p=0..< n - Suc 0. \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 \ 0" assumes 2: "norm z \ K" assumes 3: "norm (z + h) \ K" @@ -433,7 +433,7 @@ qed lemma lemma_termdiff4: - fixes f :: "'a::{real_normed_field,recpower} \ + fixes f :: "'a::{real_normed_field} \ 'b::real_normed_vector" assumes k: "0 < (k::real)" assumes le: "\h. \h \ 0; norm h < k\ \ norm (f h) \ K * norm h" @@ -478,7 +478,7 @@ qed lemma lemma_termdiff5: - fixes g :: "'a::{recpower,real_normed_field} \ + fixes g :: "'a::{real_normed_field} \ nat \ '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 (\n. diffs (diffs c) n * K ^ n)" assumes 2: "norm x < norm K" shows "(\h. \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 (\n. c n * K ^ n)" assumes 2: "summable (\n. (diffs c) n * K ^ n)" assumes 3: "summable (\n. (diffs (diffs c)) n * K ^ n)" @@ -822,11 +822,11 @@ subsection {* Exponential Function *} definition - exp :: "'a \ 'a::{recpower,real_normed_field,banach}" where + exp :: "'a \ 'a::{real_normed_field,banach}" where "exp x = (\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 \ \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 (\n. norm (x ^ n /\<^sub>R real (fact n)))" proof (rule summable_norm_comparison_test [OF exI, rule_format]) show "summable (\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 \ 'a::{real_normed_algebra_1,recpower}" + fixes f :: "nat \ 'a::{real_normed_algebra_1}" shows "(\