--- 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";
*)
--- 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
--- 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)"
--- 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) \<le> r ^ Suc (Suc 0)"
+lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> 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) \<le> 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) \<le> 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 \<le> x; 0 \<le> 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) \<le> 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) \<le> r pow ((1::hypnat) + (1::hypnat))"
+lemma hyperpow_two_le [simp]: "0 \<le> 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) \<le> r ==> 1 \<le> r pow (1 + 1)"
-apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
-done
+ "1 \<le> r ==> 1 \<le> 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) \<le> 2 pow n"
+lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 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) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> 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) \<in> 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) \<in> Reals"
+by (simp del: hypreal_of_real_power add: hyperpow_realpow SReal_def)
-lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
+
+lemma hyperpow_zero_HNatInfinite [simp]:
+ "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
by (drule HNatInfinite_is_Suc, auto)
-declare hyperpow_zero_HNatInfinite [simp]
lemma hyperpow_le_le:
"[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
--- 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\<le>na --> ?Q na" and x = "no + n" in spec, auto)
apply (subgoal_tac "lim f \<le> 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 |]
- ==> \<exists>d. 0 < d & (\<forall>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 "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
+proof -
+ from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
+ have "\<exists>s. 0 < s \<and>
+ (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
+ by (simp add: diff_minus)
+ then obtain s
+ where s: "0 < s"
+ and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
+ by auto
+ thus ?thesis
+ proof (intro exI conjI strip)
+ show "0<s" .
+ fix h::real
+ assume "0 < h \<and> 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 \<and> 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 \<le> - ((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)"
--- 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 \<in> Infinitesimal) = (x \<in> 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 \<in> Reals|] ==> y \<notin> 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 \<in> HInfinite; 0 < x; y \<in> 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 \<in> HInfinite; 0 < x |] ==> 1 < x"
by (auto intro: HInfinite_gt_SReal)
--- 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
--- 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]
(*---------------------------------------
--- 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"
--- 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
--- 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
--- 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
--- 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})\<twosuperior> = a * a"
+lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = a * a"
by (simp add: numeral_2_eq_2 Power.power_Suc)
-lemma [simp]: "(0::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = 0"
+lemma [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
by (simp add: power2_eq_square)
-lemma [simp]: "(1::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = 1"
+lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 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 \<le> (a\<twosuperior>::'a::{ordered_idom,ringpower})"
+lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
by (simp add: power2_eq_square zero_le_square)
lemma zero_less_power2 [simp]:
- "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,ringpower}))"
+ "(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 zero_eq_power2 [simp]:
- "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,ringpower}))"
+ "(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,ringpower})"
+ "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,ringpower})"
+ "(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,ringpower})"
+ "(- a)\<twosuperior> = (a\<twosuperior>::'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 \<le> (a::'a::{ordered_idom,ringpower}) ^ (2*n)"
+ "0 \<le> (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 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,ringpower})"
+ "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
@@ -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);
--- 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 \<le> a^n"} *}
lemma even_power_le_0_imp_0:
- "a ^ (2*k) \<le> (0::'a::{ordered_idom,ringpower}) ==> a=0"
+ "a ^ (2*k) \<le> (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 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,ringpower}) | even n)"
+ "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)"
(is "?P n")
proof cases
assume even: "even n"
--- 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 \<or> 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} *}
--- 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)
--- 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 \<and> 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 \<le> 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 \<le> 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:
--- 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)\<le>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)
--- 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
--- 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";