# HG changeset patch # User paulson # Date 1088092322 -7200 # Node ID 6145dd7538d757b8c9d2d4bb11f30dbc30ca68f7 # Parent bc050f23c3f83a93a14968094224cafaac244ac2 replaced monomorphic abs definitions by abs_if diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Complex/Complex.thy Thu Jun 24 17:52:02 2004 +0200 @@ -455,7 +455,7 @@ lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2" apply (induct z, simp add: complex_mod complex_cnj complex_mult) -apply (simp add: power2_eq_square real_abs_def) +apply (simp add: power2_eq_square abs_if linorder_not_less) done lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2" @@ -571,7 +571,7 @@ complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)" -instance complex :: ringpower +instance complex :: recpower proof fix z :: complex fix n :: nat @@ -947,7 +947,7 @@ test "(a*(b*c)) / ((b::complex)) = (uu::complex)"; test "(a*(b*c)) / (d*(b::complex)*(x*a)) = (uu::complex)"; -(*FIXME: what do we do about this?*) +FIXME: what do we do about this? test "a*(b*c)/(y*z) = d*(b::complex)*(x*a)/z"; *) diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Complex/NSComplex.thy Thu Jun 24 17:52:02 2004 +0200 @@ -864,7 +864,7 @@ hcomplexpow_0: "z ^ 0 = 1" hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)" -instance hcomplex :: ringpower +instance hcomplex :: recpower proof fix z :: hcomplex fix n :: nat diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Hyperreal/HyperArith.thy --- a/src/HOL/Hyperreal/HyperArith.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Hyperreal/HyperArith.thy Thu Jun 24 17:52:02 2004 +0200 @@ -86,21 +86,20 @@ declare abs_mult [simp] -lemma hrabs_add_less: "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" -apply (unfold hrabs_def) -apply (simp split add: split_if_asm) -done +lemma hrabs_add_less: + "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" +by (simp add: abs_if split: split_if_asm) text{*used once in NSA*} lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r" by (blast intro!: order_le_less_trans abs_ge_zero) lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x" -by (simp add: hrabs_def) +by (simp add: abs_if) (* Needed in Geom.ML *) lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y" -by (simp add: hrabs_def split add: split_if_asm) +by (simp add: abs_if split add: split_if_asm) lemma hypreal_of_real_hrabs: "abs (hypreal_of_real r) = hypreal_of_real (abs r)" diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Hyperreal/HyperPow.thy --- a/src/HOL/Hyperreal/HyperPow.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Hyperreal/HyperPow.thy Thu Jun 24 17:52:02 2004 +0200 @@ -16,7 +16,7 @@ hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)" -instance hypreal :: ringpower +instance hypreal :: recpower proof fix z :: hypreal fix n :: nat @@ -39,25 +39,21 @@ lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" by simp -lemma hrealpow_two_le: "(0::hypreal) \ r ^ Suc (Suc 0)" +lemma hrealpow_two_le [simp]: "(0::hypreal) \ r ^ Suc (Suc 0)" by (auto simp add: zero_le_mult_iff) -declare hrealpow_two_le [simp] -lemma hrealpow_two_le_add_order: +lemma hrealpow_two_le_add_order [simp]: "(0::hypreal) \ u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" by (simp only: hrealpow_two_le hypreal_le_add_order) -declare hrealpow_two_le_add_order [simp] -lemma hrealpow_two_le_add_order2: +lemma hrealpow_two_le_add_order2 [simp]: "(0::hypreal) \ u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" -apply (simp only: hrealpow_two_le hypreal_le_add_order) -done -declare hrealpow_two_le_add_order2 [simp] +by (simp only: hrealpow_two_le hypreal_le_add_order) lemma hypreal_add_nonneg_eq_0_iff: "[| 0 \ x; 0 \ y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))" -apply arith -done +by arith + text{*FIXME: DELETE THESE*} lemma hypreal_three_squares_add_zero_iff: @@ -78,12 +74,11 @@ lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \ 2 ^ n" by (insert power_increasing [of 0 n "2::hypreal"], simp) -lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n" +lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n" apply (induct_tac "n") apply (auto simp add: hypreal_of_nat_Suc left_distrib) apply (cut_tac n = n in two_hrealpow_ge_one, arith) done -declare two_hrealpow_gt [simp] lemma hrealpow: "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})" @@ -99,11 +94,9 @@ subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*} -lemma hypreal_of_real_power: "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n" -apply (induct_tac "n") -apply (simp_all add: nat_mult_distrib) -done -declare hypreal_of_real_power [simp] +lemma hypreal_of_real_power [simp]: + "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n" +by (induct_tac "n", simp_all add: nat_mult_distrib) lemma power_hypreal_of_real_number_of: "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)" @@ -169,11 +162,10 @@ apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add) done -lemma hyperpow_one: "r pow (1::hypnat) = r" +lemma hyperpow_one [simp]: "r pow (1::hypnat) = r" apply (unfold hypnat_one_def, cases r) apply (auto simp add: hyperpow) done -declare hyperpow_one [simp] lemma hyperpow_two: "r pow ((1::hypnat) + (1::hypnat)) = r * r" @@ -200,57 +192,48 @@ apply (auto intro: power_mono) done -lemma hyperpow_eq_one: "1 pow n = (1::hypreal)" +lemma hyperpow_eq_one [simp]: "1 pow n = (1::hypreal)" apply (cases n) apply (auto simp add: hypreal_one_def hyperpow) done -declare hyperpow_eq_one [simp] -lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)" +lemma hrabs_hyperpow_minus_one [simp]: "abs(-1 pow n) = (1::hypreal)" apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ") apply simp apply (cases n) apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs) done -declare hrabs_hyperpow_minus_one [simp] lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)" apply (cases n, cases r, cases s) apply (auto simp add: hyperpow hypreal_mult power_mult_distrib) done -lemma hyperpow_two_le: "(0::hypreal) \ r pow ((1::hypnat) + (1::hypnat))" +lemma hyperpow_two_le [simp]: "0 \ r pow (1 + 1)" by (auto simp add: hyperpow_two zero_le_mult_iff) -declare hyperpow_two_le [simp] lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)" -by (simp add: hrabs_def hyperpow_two_le) +by (simp add: abs_if hyperpow_two_le linorder_not_less) -lemma hyperpow_two_hrabs: - "abs(x) pow (1 + 1) = x pow (1 + 1)" -apply (simp add: hyperpow_hrabs) -done -declare hyperpow_two_hrabs [simp] +lemma hyperpow_two_hrabs [simp]: "abs(x) pow (1 + 1) = x pow (1 + 1)" +by (simp add: hyperpow_hrabs) -lemma hyperpow_two_gt_one: - "(1::hypreal) < r ==> 1 < r pow (1 + 1)" +lemma hyperpow_two_gt_one: "1 < r ==> 1 < r pow (1 + 1)" apply (auto simp add: hyperpow_two) apply (rule_tac y = "1*1" in order_le_less_trans) apply (rule_tac [2] hypreal_mult_less_mono, auto) done lemma hyperpow_two_ge_one: - "(1::hypreal) \ r ==> 1 \ r pow (1 + 1)" -apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le) -done + "1 \ r ==> 1 \ r pow (1 + 1)" +by (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le) -lemma two_hyperpow_ge_one: "(1::hypreal) \ 2 pow n" +lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \ 2 pow n" apply (rule_tac y = "1 pow n" in order_trans) apply (rule_tac [2] hyperpow_le, auto) done -declare two_hyperpow_ge_one [simp] -lemma hyperpow_minus_one2: +lemma hyperpow_minus_one2 [simp]: "-1 pow ((1 + 1)*n) = (1::hypreal)" apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ") apply simp @@ -258,7 +241,6 @@ apply (auto simp add: nat_mult_2 [symmetric] hyperpow hypnat_add hypreal_minus left_distrib) done -declare hyperpow_minus_one2 [simp] lemma hyperpow_less_le: "[|(0::hypreal) \ r; r \ 1; n < N|] ==> r pow N \ r pow n" @@ -277,18 +259,16 @@ lemma hyperpow_realpow: "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)" -apply (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow) -done +by (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow) -lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \ Reals" -apply (unfold SReal_def) -apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow) -done -declare hyperpow_SReal [simp] +lemma hyperpow_SReal [simp]: + "(hypreal_of_real r) pow (hypnat_of_nat n) \ Reals" +by (simp del: hypreal_of_real_power add: hyperpow_realpow SReal_def) -lemma hyperpow_zero_HNatInfinite: "N \ HNatInfinite ==> (0::hypreal) pow N = 0" + +lemma hyperpow_zero_HNatInfinite [simp]: + "N \ HNatInfinite ==> (0::hypreal) pow N = 0" by (drule HNatInfinite_is_Suc, auto) -declare hyperpow_zero_HNatInfinite [simp] lemma hyperpow_le_le: "[| (0::hypreal) \ r; r \ 1; n \ N |] ==> r pow N \ r pow n" diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Hyperreal/Lim.thy Thu Jun 24 17:52:02 2004 +0200 @@ -1328,7 +1328,7 @@ apply (drule_tac P = "%na. no\na --> ?Q na" and x = "no + n" in spec, auto) apply (subgoal_tac "lim f \ f (no + n) ") apply (induct_tac [2] "no") -apply (auto intro: order_trans simp add: diff_minus real_abs_def) +apply (auto intro: order_trans simp add: diff_minus abs_if) apply (drule_tac no=no and m=n in lemma_f_mono_add) apply (auto simp add: add_commute) done @@ -1660,22 +1660,38 @@ apply (rule_tac [4] x = xb in exI, simp_all) done -(*----------------------------------------------------------------------------*) -(* If f'(x) > 0 then x is locally strictly increasing at the right *) -(*----------------------------------------------------------------------------*) + +subsection{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*} lemma DERIV_left_inc: - "[| DERIV f x :> l; 0 < l |] - ==> \d. 0 < d & (\h. 0 < h & h < d --> f(x) < f(x + h))" -apply (simp add: deriv_def LIM_def) -apply (drule spec, auto) -apply (rule_tac x = s in exI, auto) -apply (subgoal_tac "0 < l*h") - prefer 2 apply (simp add: zero_less_mult_iff) -apply (drule_tac x = h in spec) -apply (simp add: real_abs_def pos_le_divide_eq pos_less_divide_eq - split add: split_if_asm) -done + assumes der: "DERIV f x :> l" + and l: "0 < l" + shows "\d. 0 < d & (\h. 0 < h & h < d --> f(x) < f(x + h))" +proof - + from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]] + have "\s. 0 < s \ + (\z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < l)" + by (simp add: diff_minus) + then obtain s + where s: "0 < s" + and all: "!!z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < l" + by auto + thus ?thesis + proof (intro exI conjI strip) + show "0 h < s" + with all [of h] show "f x < f (x+h)" + proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] + split add: split_if_asm) + assume "~ (f (x+h) - f x) / h < l" and h: "0 < h" + with l + have "0 < (f (x+h) - f x) / h" by arith + thus "f x < f (x+h)" + by (simp add: pos_less_divide_eq h) + qed + qed +qed lemma DERIV_left_dec: assumes der: "DERIV f x :> l" @@ -1696,9 +1712,9 @@ fix h::real assume "0 < h \ h < s" with all [of "-h"] show "f x < f (x-h)" - proof (simp add: real_abs_def pos_less_divide_eq diff_minus [symmetric] + proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] split add: split_if_asm) - assume "~ l \ - ((f (x-h) - f x) / h)" and h: "0 < h" + assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h" with l have "0 < (f (x-h) - f x) / h" by arith thus "f x < f (x-h)" diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Hyperreal/NSA.thy --- a/src/HOL/Hyperreal/NSA.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Hyperreal/NSA.thy Thu Jun 24 17:52:02 2004 +0200 @@ -405,7 +405,7 @@ by auto lemma Infinitesimal_hrabs_iff: "(abs x \ Infinitesimal) = (x \ Infinitesimal)" -by (auto simp add: hrabs_def) +by (auto simp add: abs_if) declare Infinitesimal_hrabs_iff [iff] lemma HFinite_diff_Infinitesimal_hrabs: @@ -845,7 +845,7 @@ lemma SReal_not_Infinitesimal: "[| 0 < y; y \ Reals|] ==> y \ Infinitesimal" apply (simp add: Infinitesimal_def) -apply (auto simp add: hrabs_def) +apply (auto simp add: abs_if) done lemma SReal_minus_not_Infinitesimal: @@ -1324,7 +1324,7 @@ by (auto simp add: hypreal_mult_commute HInfinite_HFinite_not_Infinitesimal_mult) lemma HInfinite_gt_SReal: "[| x \ HInfinite; 0 < x; y \ Reals |] ==> y < x" -by (auto dest!: bspec simp add: HInfinite_def hrabs_def order_less_imp_le) +by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le) lemma HInfinite_gt_zero_gt_one: "[| x \ HInfinite; 0 < x |] ==> 1 < x" by (auto intro: HInfinite_gt_SReal) diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Hyperreal/Series.thy --- a/src/HOL/Hyperreal/Series.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Hyperreal/Series.thy Thu Jun 24 17:52:02 2004 +0200 @@ -506,7 +506,7 @@ apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N) " in exI) apply (rule sums_divide) apply (rule sums_mult) -apply (auto intro!: sums_mult geometric_sums simp add: real_abs_def) +apply (auto intro!: sums_mult geometric_sums simp add: abs_if) done diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Hyperreal/Star.thy --- a/src/HOL/Hyperreal/Star.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Hyperreal/Star.thy Thu Jun 24 17:52:02 2004 +0200 @@ -169,14 +169,11 @@ (* - Prove that hrabs is a nonstandard extension of rabs without + Prove that abs for hypreal is a nonstandard extension of abs for real w/o use of congruence property (proved after this for general - nonstandard extensions of real valued functions). This makes - proof much longer- see comments at end of HREALABS.thy where - we proved a congruence theorem for hrabs. + nonstandard extensions of real valued functions). - NEW!!! No need to prove all the lemmas anymore. Use the ultrafilter - tactic! + Proof now Uses the ultrafilter tactic! *) lemma hrabs_is_starext_rabs: "is_starext abs abs" @@ -185,7 +182,9 @@ apply (rule_tac z = y in eq_Abs_hypreal, auto) apply (rule bexI, rule_tac [2] lemma_hyprel_refl) apply (rule bexI, rule_tac [2] lemma_hyprel_refl) -apply (auto dest!: spec simp add: hypreal_minus hrabs_def hypreal_zero_def hypreal_le_def hypreal_less_def) +apply (auto dest!: spec + simp add: hypreal_minus abs_if hypreal_zero_def + hypreal_le hypreal_less) apply (arith | ultra)+ done @@ -224,6 +223,7 @@ ------------------------------------------*) lemma starfun_mult: "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa" by (cases xa, simp add: starfun hypreal_mult) + declare starfun_mult [symmetric, simp] (*--------------------------------------- diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Import/HOL4Compat.thy --- a/src/HOL/Import/HOL4Compat.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Import/HOL4Compat.thy Thu Jun 24 17:52:02 2004 +0200 @@ -510,10 +510,10 @@ by (simp add: real_of_nat_Suc) lemma abs: "abs (x::real) = (if 0 <= x then x else -x)" - by (simp add: real_abs_def) + by (simp add: abs_if) lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)" - by simp; + by simp constdefs real_gt :: "real => real => bool" diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Integ/IntArith.thy --- a/src/HOL/Integ/IntArith.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Integ/IntArith.thy Thu Jun 24 17:52:02 2004 +0200 @@ -130,7 +130,7 @@ by (simp add: abs_if) lemma abs_power_minus_one [simp]: - "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,ringpower})" + "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})" by (simp add: power_abs) lemma of_int_number_of_eq: @@ -227,7 +227,7 @@ lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)" apply (case_tac "z=0 | w=0") -apply (auto simp add: zabs_def nat_mult_distrib [symmetric] +apply (auto simp add: abs_if nat_mult_distrib [symmetric] nat_mult_distrib_neg [symmetric] mult_less_0_iff) done @@ -318,7 +318,7 @@ apply (case_tac "k = f (n+1) ") apply force apply (erule impE) - apply (simp add: zabs_def split add: split_if_asm) + apply (simp add: abs_if split add: split_if_asm) apply (blast intro: le_SucI) done diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Integ/IntDef.thy Thu Jun 24 17:52:02 2004 +0200 @@ -503,7 +503,7 @@ done lemma abs_int_eq [simp]: "abs (int m) = int m" -by (simp add: zabs_def) +by (simp add: abs_if) text{*This version is proved for all ordered rings, not just integers! It is proved here because attribute @{text arith_split} is not available diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Integ/IntDiv.thy --- a/src/HOL/Integ/IntDiv.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Integ/IntDiv.thy Thu Jun 24 17:52:02 2004 +0200 @@ -1126,7 +1126,7 @@ done lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" - apply (auto simp add: dvd_def zabs_def zmult_int [symmetric]) + apply (auto simp add: dvd_def abs_if zmult_int [symmetric]) apply (rule_tac [3] x = "nat k" in exI) apply (rule_tac [2] x = "-(int k)" in exI) apply (rule_tac x = "nat (-k)" in exI) @@ -1172,7 +1172,7 @@ "p ^ (Suc n) = (p::int) * (p ^ n)" -instance int :: ringpower +instance int :: recpower proof fix z :: int fix n :: nat diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Integ/NatBin.thy --- a/src/HOL/Integ/NatBin.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Integ/NatBin.thy Thu Jun 24 17:52:02 2004 +0200 @@ -256,58 +256,58 @@ We cannot prove general results about the numeral @{term "-1"}, so we have to use @{term "- 1"} instead.*} -lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,ringpower})\ = a * a" +lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\ = a * a" by (simp add: numeral_2_eq_2 Power.power_Suc) -lemma [simp]: "(0::'a::{comm_semiring_1_cancel,ringpower})\ = 0" +lemma [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\ = 0" by (simp add: power2_eq_square) -lemma [simp]: "(1::'a::{comm_semiring_1_cancel,ringpower})\ = 1" +lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\ = 1" by (simp add: power2_eq_square) text{*Squares of literal numerals will be evaluated.*} declare power2_eq_square [of "number_of w", standard, simp] -lemma zero_le_power2 [simp]: "0 \ (a\::'a::{ordered_idom,ringpower})" +lemma zero_le_power2 [simp]: "0 \ (a\::'a::{ordered_idom,recpower})" by (simp add: power2_eq_square zero_le_square) lemma zero_less_power2 [simp]: - "(0 < a\) = (a \ (0::'a::{ordered_idom,ringpower}))" + "(0 < a\) = (a \ (0::'a::{ordered_idom,recpower}))" by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) lemma zero_eq_power2 [simp]: - "(a\ = 0) = (a = (0::'a::{ordered_idom,ringpower}))" + "(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,ringpower})" + "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,ringpower})" + "(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,ringpower})" + "(- a)\ = (a\::'a::{comm_ring_1,recpower})" by (simp add: power2_eq_square) -lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,ringpower})" +lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})" apply (induct_tac "n") apply (auto simp add: power_Suc power_add) done -lemma power_even_eq: "(a::'a::ringpower) ^ (2*n) = (a^n)^2" +lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2" by (simp add: power_mult power_mult_distrib power2_eq_square) 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,ringpower}) ^ (2*n)" + "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)" by (simp add: power_minus1_even power_minus [of a]) lemma zero_le_even_power: - "0 \ (a::'a::{ordered_idom,ringpower}) ^ (2*n)" + "0 \ (a::'a::{ordered_idom,recpower}) ^ (2*n)" proof (induct "n") case 0 show ?case by (simp add: zero_le_one) @@ -320,7 +320,7 @@ qed lemma odd_power_less_zero: - "(a::'a::{ordered_idom,ringpower}) < 0 ==> a ^ Suc(2*n) < 0" + "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0" proof (induct "n") case 0 show ?case by (simp add: Power.power_Suc) @@ -333,7 +333,7 @@ qed lemma odd_0_le_power_imp_0_le: - "0 \ a ^ Suc(2*n) ==> 0 \ (a::'a::{ordered_idom,ringpower})" + "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 @@ -606,10 +606,10 @@ 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,ringpower})" +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})" by (simp add: power_mult); -lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,ringpower})" +lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})" by (simp add: power_mult power_Suc); diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Integ/Parity.thy --- a/src/HOL/Integ/Parity.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Integ/Parity.thy Thu Jun 24 17:52:02 2004 +0200 @@ -233,22 +233,22 @@ subsection {* Powers of negative one *} lemma neg_one_even_odd_power: - "(even x --> (-1::'a::{number_ring,ringpower})^x = 1) & + "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & (odd x --> (-1::'a)^x = -1)" apply (induct_tac x) apply (simp, simp add: power_Suc) done lemma neg_one_even_power [simp]: - "even x ==> (-1::'a::{number_ring,ringpower})^x = 1" + "even x ==> (-1::'a::{number_ring,recpower})^x = 1" by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption) lemma neg_one_odd_power [simp]: - "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1" + "odd x ==> (-1::'a::{number_ring,recpower})^x = -1" by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption) lemma neg_power_if: - "(-x::'a::{comm_ring_1,ringpower}) ^ n = + "(-x::'a::{comm_ring_1,recpower}) ^ n = (if even n then (x ^ n) else -(x ^ n))" by (induct n, simp_all split: split_if_asm add: power_Suc) @@ -256,13 +256,13 @@ subsection {* An Equivalence for @{term "0 \ a^n"} *} lemma even_power_le_0_imp_0: - "a ^ (2*k) \ (0::'a::{ordered_idom,ringpower}) ==> a=0" + "a ^ (2*k) \ (0::'a::{ordered_idom,recpower}) ==> a=0" apply (induct k) apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) done lemma zero_le_power_iff: - "(0 \ a^n) = (0 \ (a::'a::{ordered_idom,ringpower}) | even n)" + "(0 \ a^n) = (0 \ (a::'a::{ordered_idom,recpower}) | even n)" (is "?P n") proof cases assume even: "even n" diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/NumberTheory/EulerFermat.thy --- a/src/HOL/NumberTheory/EulerFermat.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/NumberTheory/EulerFermat.thy Thu Jun 24 17:52:02 2004 +0200 @@ -60,7 +60,7 @@ lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \ z = -1)" -- {* LCP: not sure why this lemma is needed now *} -by (auto simp add: zabs_def) +by (auto simp add: abs_if) text {* \medskip @{text norRRset} *} diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/NumberTheory/Fib.thy --- a/src/HOL/NumberTheory/Fib.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/NumberTheory/Fib.thy Thu Jun 24 17:52:02 2004 +0200 @@ -66,7 +66,8 @@ much easier to prove using integers! *} -lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) = +lemma fib_Cassini: + "int (fib (Suc (Suc n)) * fib n) = (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - 1 else int (fib (Suc n) * fib (Suc n)) + 1)" apply (induct n rule: fib.induct) diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/NumberTheory/IntPrimes.thy --- a/src/HOL/NumberTheory/IntPrimes.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/NumberTheory/IntPrimes.thy Thu Jun 24 17:52:02 2004 +0200 @@ -65,10 +65,10 @@ subsection {* Euclid's Algorithm and GCD *} lemma zgcd_0 [simp]: "zgcd (m, 0) = abs m" - by (simp add: zgcd_def zabs_def) + by (simp add: zgcd_def abs_if) lemma zgcd_0_left [simp]: "zgcd (0, m) = abs m" - by (simp add: zgcd_def zabs_def) + by (simp add: zgcd_def abs_if) lemma zgcd_zminus [simp]: "zgcd (-m, n) = zgcd (m, n)" by (simp add: zgcd_def) @@ -78,7 +78,7 @@ lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)" apply (frule_tac b = n and a = m in pos_mod_sign) - apply (simp del: pos_mod_sign add: zgcd_def zabs_def nat_mod_distrib) + apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib) apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if) apply (frule_tac a = m in pos_mod_bound) apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle) @@ -91,19 +91,19 @@ done lemma zgcd_1 [simp]: "zgcd (m, 1) = 1" - by (simp add: zgcd_def zabs_def) + by (simp add: zgcd_def abs_if) lemma zgcd_0_1_iff [simp]: "(zgcd (0, m) = 1) = (abs m = 1)" - by (simp add: zgcd_def zabs_def) + by (simp add: zgcd_def abs_if) lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m" - by (simp add: zgcd_def zabs_def int_dvd_iff) + by (simp add: zgcd_def abs_if int_dvd_iff) lemma zgcd_zdvd2 [iff]: "zgcd (m, n) dvd n" - by (simp add: zgcd_def zabs_def int_dvd_iff) + by (simp add: zgcd_def abs_if int_dvd_iff) lemma zgcd_greatest_iff: "k dvd zgcd (m, n) = (k dvd m \ k dvd n)" - by (simp add: zgcd_def zabs_def int_dvd_iff dvd_int_iff nat_dvd_iff) + by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff) lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)" by (simp add: zgcd_def gcd_commute) @@ -125,11 +125,11 @@ lemma zgcd_zmult_distrib2: "0 \ k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" by (simp del: minus_mult_right [symmetric] - add: minus_mult_right nat_mult_distrib zgcd_def zabs_def + add: minus_mult_right nat_mult_distrib zgcd_def abs_if mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)" - by (simp add: zabs_def zgcd_zmult_distrib2) + by (simp add: abs_if zgcd_zmult_distrib2) lemma zgcd_self [simp]: "0 \ m ==> zgcd (m, m) = m" by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all) @@ -465,7 +465,7 @@ apply (rule exI) apply (rule exI) apply (subst xzgcda.simps, auto) - apply (simp add: zabs_def) + apply (simp add: abs_if) done lemma xzgcd_correct_aux2: @@ -481,7 +481,7 @@ apply (frule_tac a = "r'" in pos_mod_sign, auto) apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp) apply (subst xzgcda.simps, auto) - apply (simp add: zabs_def) + apply (simp add: abs_if) done lemma xzgcd_correct: diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Real/RealDef.thy Thu Jun 24 17:52:02 2004 +0200 @@ -830,16 +830,16 @@ text{*FIXME: these should go!*} lemma abs_eqI1: "(0::real)\x ==> abs x = x" -by (simp add: real_abs_def) +by (simp add: abs_if) lemma abs_eqI2: "(0::real) < x ==> abs x = x" -by (simp add: real_abs_def) +by (simp add: abs_if) lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x" -by (simp add: real_abs_def linorder_not_less [symmetric]) +by (simp add: abs_if linorder_not_less [symmetric]) lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" -by (simp add: real_abs_def) +by (simp add: abs_if) lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" by (force simp add: Ring_and_Field.abs_less_iff) @@ -849,7 +849,7 @@ (*FIXME: used only once, in SEQ.ML*) lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" -by (simp add: real_abs_def) +by (simp add: abs_if) lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Real/RealPow.thy --- a/src/HOL/Real/RealPow.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Real/RealPow.thy Thu Jun 24 17:52:02 2004 +0200 @@ -17,7 +17,7 @@ realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)" -instance real :: ringpower +instance real :: recpower proof fix z :: real fix n :: nat diff -r bc050f23c3f8 -r 6145dd7538d7 src/HOL/Real/real_arith.ML --- a/src/HOL/Real/real_arith.ML Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/Real/real_arith.ML Thu Jun 24 17:52:02 2004 +0200 @@ -12,8 +12,6 @@ val real_mult_left_mono = read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono; -val real_abs_def = thm "real_abs_def"; - val real_le_def = thm "real_le_def"; val real_diff_def = thm "real_diff_def"; val real_divide_def = thm "real_divide_def";