# HG changeset patch # User wenzelm # Date 957812222 -7200 # Node ID 4eaa99f0d22395263fc95f6cb3a785a295a147ed # Parent 9ee87bdcba056a53b05f58e16ccac87ad222a318 replaced rabs by overloaded abs; diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/HahnBanach/Aux.thy --- a/src/HOL/Real/HahnBanach/Aux.thy Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/Aux.thy Mon May 08 20:57:02 2000 +0200 @@ -62,13 +62,13 @@ finally; show "?thesis"; .; qed; -lemma rabs_minus_one: "rabs (- 1r) = 1r"; +lemma abs_minus_one: "abs (- 1r) = 1r"; proof -; have "-1r < 0r"; by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one); - hence "rabs (- 1r) = - (- 1r)"; - by (rule rabs_minus_eqI2); + hence "abs (- 1r) = - (- 1r)"; + by (rule abs_minus_eqI2); also; have "... = 1r"; by simp; finally; show ?thesis; .; qed; diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/HahnBanach/FunctionNorm.thy --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon May 08 20:57:02 2000 +0200 @@ -20,14 +20,14 @@ is_continuous :: "['a::{minus, plus} set, 'a => real, 'a => real] => bool" "is_continuous V norm f == - is_linearform V f & (EX c. ALL x:V. rabs (f x) <= c * norm x)"; + is_linearform V f & (EX c. ALL x:V. abs (f x) <= c * norm x)"; lemma continuousI [intro]: - "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |] + "[| is_linearform V f; !! x. x:V ==> abs (f x) <= c * norm x |] ==> is_continuous V norm f"; proof (unfold is_continuous_def, intro exI conjI ballI); - assume r: "!! x. x:V ==> rabs (f x) <= c * norm x"; - fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r); + assume r: "!! x. x:V ==> abs (f x) <= c * norm x"; + fix x; assume "x:V"; show "abs (f x) <= c * norm x"; by (rule r); qed; lemma continuous_linearform [intro??]: @@ -36,7 +36,7 @@ lemma continuous_bounded [intro??]: "is_continuous V norm f - ==> EX c. ALL x:V. rabs (f x) <= c * norm x"; + ==> EX c. ALL x:V. abs (f x) <= c * norm x"; by (unfold is_continuous_def) force; subsection{* The norm of a linear form *}; @@ -66,7 +66,7 @@ constdefs B :: "[ 'a set, 'a => real, 'a => real ] => real set" "B V norm f == - {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= 00 & x:V}"; + {0r} \Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}"; text{* $n$ is the function norm of $f$, iff $n$ is the supremum of $B$. @@ -97,7 +97,7 @@ is_continuous_def Sup_def, elim conjE, rule selectI2EX); assume "is_normed_vectorspace V norm"; assume "is_linearform V f" - and e: "EX c. ALL x:V. rabs (f x) <= c * norm x"; + and e: "EX c. ALL x:V. abs (f x) <= c * norm x"; txt {* The existence of the supremum is shown using the completeness of the reals. Completeness means, that @@ -120,7 +120,7 @@ txt {* We know that $f$ is bounded by some value $c$. *}; - fix c; assume a: "ALL x:V. rabs (f x) <= c * norm x"; + fix c; assume a: "ALL x:V. abs (f x) <= c * norm x"; def b == "max c 0r"; show "?thesis"; @@ -165,13 +165,13 @@ txt {* The thesis follows by a short calculation using the fact that $f$ is bounded. *}; - assume "y = rabs (f x) * rinv (norm x)"; + assume "y = abs (f x) * rinv (norm x)"; also; have "... <= c * norm x * rinv (norm x)"; proof (rule real_mult_le_le_mono2); show "0r <= rinv (norm x)"; by (rule real_less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); - from a; show "rabs (f x) <= c * norm x"; ..; + from a; show "abs (f x) <= c * norm x"; ..; qed; also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc); @@ -208,9 +208,9 @@ elim UnE singletonE CollectE exE conjE); fix x r; assume "x : V" "x ~= 00" - and r: "r = rabs (f x) * rinv (norm x)"; + and r: "r = abs (f x) * rinv (norm x)"; - have ge: "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero); + have ge: "0r <= abs (f x)"; by (simp! only: abs_ge_zero); have "0r <= rinv (norm x)"; by (rule real_less_imp_le, rule real_rinv_gt_zero, rule);(*** proof (rule real_less_imp_le); @@ -243,7 +243,7 @@ lemma norm_fx_le_norm_f_norm_x: "[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |] - ==> rabs (f x) <= function_norm V norm f * norm x"; + ==> abs (f x) <= function_norm V norm f * norm x"; proof -; assume "is_normed_vectorspace V norm" "x:V" and c: "is_continuous V norm f"; @@ -260,16 +260,16 @@ holds $f\ap \zero = 0$. *}; assume "x = 00"; - have "rabs (f x) = rabs (f 00)"; by (simp!); + have "abs (f x) = abs (f 00)"; by (simp!); also; from v continuous_linearform; have "f 00 = 0r"; ..; - also; note rabs_zero; + also; note abs_zero; also; have "0r <= function_norm V norm f * norm x"; proof (rule real_le_mult_order); show "0r <= function_norm V norm f"; ..; show "0r <= norm x"; ..; qed; finally; - show "rabs (f x) <= function_norm V norm f * norm x"; .; + show "abs (f x) <= function_norm V norm f * norm x"; .; next; assume "x ~= 00"; @@ -282,28 +282,28 @@ txt {* For the case $x\neq \zero$ we derive the following fact from the definition of the function norm:*}; - have l: "rabs (f x) * rinv (norm x) <= function_norm V norm f"; + have l: "abs (f x) * rinv (norm x) <= function_norm V norm f"; proof (unfold function_norm_def, rule sup_ub); from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; by (simp! add: is_function_norm_def function_norm_def); - show "rabs (f x) * rinv (norm x) : B V norm f"; + show "abs (f x) * rinv (norm x) : B V norm f"; by (unfold B_def, intro UnI2 CollectI exI [of _ x] conjI, simp); qed; txt {* The thesis now follows by a short calculation: *}; - have "rabs (f x) = rabs (f x) * 1r"; by (simp!); + have "abs (f x) = abs (f x) * 1r"; by (simp!); also; from nz; have "1r = rinv (norm x) * norm x"; by (rule real_mult_inv_left [RS sym]); also; - have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x"; - by (simp! add: real_mult_assoc [of "rabs (f x)"]); + have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x"; + by (simp! add: real_mult_assoc [of "abs (f x)"]); also; have "... <= function_norm V norm f * norm x"; by (rule real_mult_le_le_mono2 [OF n l]); finally; - show "rabs (f x) <= function_norm V norm f * norm x"; .; + show "abs (f x) <= function_norm V norm f * norm x"; .; qed; qed; @@ -316,12 +316,12 @@ lemma fnorm_le_ub: "[| is_normed_vectorspace V norm; is_continuous V norm f; - ALL x:V. rabs (f x) <= c * norm x; 0r <= c |] + ALL x:V. abs (f x) <= c * norm x; 0r <= c |] ==> function_norm V norm f <= c"; proof (unfold function_norm_def); assume "is_normed_vectorspace V norm"; assume c: "is_continuous V norm f"; - assume fb: "ALL x:V. rabs (f x) <= c * norm x" + assume fb: "ALL x:V. abs (f x) <= c * norm x" and "0r <= c"; txt {* Suppose the inequation holds for some $c\geq 0$. @@ -372,10 +372,10 @@ hence rinv_gez: "0r <= rinv (norm x)"; by (rule real_less_imp_le); - assume "y = rabs (f x) * rinv (norm x)"; + assume "y = abs (f x) * rinv (norm x)"; also; from rinv_gez; have "... <= c * norm x * rinv (norm x)"; proof (rule real_mult_le_le_mono2); - show "rabs (f x) <= c * norm x"; by (rule bspec); + show "abs (f x) <= c * norm x"; by (rule bspec); qed; also; have "... <= c"; by (simp add: nz real_mult_assoc); finally; show ?thesis; .; diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/HahnBanach/HahnBanach.thy --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Mon May 08 20:57:02 2000 +0200 @@ -596,25 +596,25 @@ subsection {* Alternative formulation *}; text {* The following alternative formulation of the Hahn-Banach -Theorem\label{rabs-HahnBanach} uses the fact that for a real linear form +Theorem\label{abs-HahnBanach} uses the fact that for a real linear form $f$ and a seminorm $p$ the following inequations are equivalent:\footnote{This was shown in lemma -$\idt{rabs{\dsh}ineq{\dsh}iff}$ (see page \pageref{rabs-ineq-iff}).} +$\idt{abs{\dsh}ineq{\dsh}iff}$ (see page \pageref{abs-ineq-iff}).} \begin{matharray}{ll} \forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ \forall x\in H.\ap h\ap x\leq p\ap x\\ \end{matharray} *}; -theorem rabs_HahnBanach: +theorem abs_HahnBanach: "[| is_vectorspace E; is_subspace F E; is_linearform F f; - is_seminorm E p; ALL x:F. rabs (f x) <= p x |] + is_seminorm E p; ALL x:F. abs (f x) <= p x |] ==> EX g. is_linearform E g & (ALL x:F. g x = f x) - & (ALL x:E. rabs (g x) <= p x)"; + & (ALL x:E. abs (g x) <= p x)"; proof -; assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" - "is_linearform F f" "ALL x:F. rabs (f x) <= p x"; - have "ALL x:F. f x <= p x"; by (rule rabs_ineq_iff [RS iffD1]); + "is_linearform F f" "ALL x:F. abs (f x) <= p x"; + have "ALL x:F. f x <= p x"; by (rule abs_ineq_iff [RS iffD1]); hence "EX g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. g x <= p x)"; by (simp! only: HahnBanach); @@ -622,8 +622,8 @@ proof (elim exE conjE); fix g; assume "is_linearform E g" "ALL x:F. g x = f x" "ALL x:E. g x <= p x"; - hence "ALL x:E. rabs (g x) <= p x"; - by (simp! add: rabs_ineq_iff [OF subspace_refl]); + hence "ALL x:E. abs (g x) <= p x"; + by (simp! add: abs_ineq_iff [OF subspace_refl]); thus ?thesis; by (intro exI conjI); qed; qed; @@ -672,16 +672,16 @@ txt{* $p$ is absolutely homogenous: *}; - show "p (a (*) x) = rabs a * p x"; + show "p (a (*) x) = abs a * p x"; proof -; have "p (a (*) x) = function_norm F norm f * norm (a (*) x)"; by (simp!); - also; have "norm (a (*) x) = rabs a * norm x"; - by (rule normed_vs_norm_rabs_homogenous); - also; have "function_norm F norm f * (rabs a * norm x) - = rabs a * (function_norm F norm f * norm x)"; + also; have "norm (a (*) x) = abs a * norm x"; + by (rule normed_vs_norm_abs_homogenous); + also; have "function_norm F norm f * (abs a * norm x) + = abs a * (function_norm F norm f * norm x)"; by (simp! only: real_mult_left_commute); - also; have "... = rabs a * p x"; by (simp!); + also; have "... = abs a * p x"; by (simp!); finally; show ?thesis; .; qed; @@ -706,10 +706,10 @@ txt{* $f$ is bounded by $p$. *}; - have "ALL x:F. rabs (f x) <= p x"; + have "ALL x:F. abs (f x) <= p x"; proof; fix x; assume "x:F"; - from f_norm; show "rabs (f x) <= p x"; + from f_norm; show "abs (f x) <= p x"; by (simp! add: norm_fx_le_norm_f_norm_x); qed; @@ -721,14 +721,14 @@ with e f q; have "EX g. is_linearform E g & (ALL x:F. g x = f x) - & (ALL x:E. rabs (g x) <= p x)"; - by (simp! add: rabs_HahnBanach); + & (ALL x:E. abs (g x) <= p x)"; + by (simp! add: abs_HahnBanach); thus ?thesis; proof (elim exE conjE); fix g; assume "is_linearform E g" and a: "ALL x:F. g x = f x" - and b: "ALL x:E. rabs (g x) <= p x"; + and b: "ALL x:E. abs (g x) <= p x"; show "EX g. is_linearform E g & is_continuous E norm g @@ -743,7 +743,7 @@ proof; fix x; assume "x:E"; from b [RS bspec, OF this]; - show "rabs (g x) <= function_norm F norm f * norm x"; + show "abs (g x) <= function_norm F norm f * norm x"; by (unfold p_def); qed; @@ -765,10 +765,10 @@ \end{matharray} *}; - have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x"; + have "ALL x:E. abs (g x) <= function_norm F norm f * norm x"; proof; fix x; assume "x:E"; - show "rabs (g x) <= function_norm F norm f * norm x"; + show "abs (g x) <= function_norm F norm f * norm x"; by (simp!); qed; @@ -780,17 +780,17 @@ txt{* The other direction is achieved by a similar argument. *}; - have "ALL x:F. rabs (f x) <= function_norm E norm g * norm x"; + have "ALL x:F. abs (f x) <= function_norm E norm g * norm x"; proof; fix x; assume "x : F"; from a; have "g x = f x"; ..; - hence "rabs (f x) = rabs (g x)"; by simp; + hence "abs (f x) = abs (g x)"; by simp; also; from _ _ g_cont; have "... <= function_norm E norm g * norm x"; proof (rule norm_fx_le_norm_f_norm_x); show "x:E"; ..; qed; - finally; show "rabs (f x) <= function_norm E norm g * norm x"; .; + finally; show "abs (f x) <= function_norm E norm g * norm x"; .; qed; thus "?R <= ?L"; proof (rule fnorm_le_ub [OF f_norm f_cont]); diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon May 08 20:57:02 2000 +0200 @@ -297,7 +297,7 @@ by (rule real_mult_diff_distrib); also; from lz vs y; have "- a * (p (rinv a (*) y + x0)) = p (a (*) (rinv a (*) y + x0))"; - by (simp add: seminorm_rabs_homogenous rabs_minus_eqI2); + by (simp add: seminorm_abs_homogenous abs_minus_eqI2); also; from nz vs y; have "... = p (y + a (*) x0)"; by (simp add: vs_add_mult_distrib1); also; from nz vs y; have "a * (h (rinv a (*) y)) = h y"; @@ -329,7 +329,7 @@ also; from gz vs y; have "a * p (rinv a (*) y + x0) = p (a (*) (rinv a (*) y + x0))"; - by (simp add: seminorm_rabs_homogenous rabs_eqI2); + by (simp add: seminorm_abs_homogenous abs_eqI2); also; from nz vs y; have "... = p (y + a (*) x0)"; by (simp add: vs_add_mult_distrib1); diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Mon May 08 20:57:02 2000 +0200 @@ -638,7 +638,7 @@ text{* \medskip The following lemma is a property of linear forms on real vector spaces. It will be used for the lemma -$\idt{rabs{\dsh}HahnBanach}$ (see page \pageref{rabs-HahnBanach}). \label{rabs-ineq-iff} +$\idt{abs{\dsh}HahnBanach}$ (see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff} For real vector spaces the following inequations are equivalent: \begin{matharray}{ll} \forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ @@ -646,10 +646,10 @@ \end{matharray} *}; -lemma rabs_ineq_iff: +lemma abs_ineq_iff: "[| is_subspace H E; is_vectorspace E; is_seminorm E p; is_linearform H h |] - ==> (ALL x:H. rabs (h x) <= p x) = (ALL x:H. h x <= p x)" + ==> (ALL x:H. abs (h x) <= p x) = (ALL x:H. h x <= p x)" (concl is "?L = ?R"); proof -; assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" @@ -661,7 +661,7 @@ show ?R; proof; fix x; assume x: "x:H"; - have "h x <= rabs (h x)"; by (rule rabs_ge_self); + have "h x <= abs (h x)"; by (rule abs_ge_self); also; from l; have "... <= p x"; ..; finally; show "h x <= p x"; .; qed; @@ -670,7 +670,7 @@ show ?L; proof; fix x; assume "x:H"; - show "!! a b. [| - a <= b; b <= a |] ==> rabs b <= a"; + show "!! a b::real. [| - a <= b; b <= a |] ==> abs b <= a"; by arith; show "- p x <= h x"; proof (rule real_minus_le); diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/HahnBanach/NormedSpace.thy --- a/src/HOL/Real/HahnBanach/NormedSpace.thy Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Mon May 08 20:57:02 2000 +0200 @@ -19,12 +19,12 @@ is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool" "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. 0r <= norm x - & norm (a (*) x) = (rabs a) * (norm x) + & norm (a (*) x) = (abs a) * (norm x) & norm (x + y) <= norm x + norm y"; lemma is_seminormI [intro]: "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x; - !! x a. x:V ==> norm (a (*) x) = (rabs a) * (norm x); + !! x a. x:V ==> norm (a (*) x) = (abs a) * (norm x); !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] ==> is_seminorm V norm"; by (unfold is_seminorm_def, force); @@ -33,9 +33,9 @@ "[| is_seminorm V norm; x:V |] ==> 0r <= norm x"; by (unfold is_seminorm_def, force); -lemma seminorm_rabs_homogenous: +lemma seminorm_abs_homogenous: "[| is_seminorm V norm; x:V |] - ==> norm (a (*) x) = (rabs a) * (norm x)"; + ==> norm (a (*) x) = (abs a) * (norm x)"; by (unfold is_seminorm_def, force); lemma seminorm_subadditive: @@ -52,9 +52,9 @@ by (simp! add: diff_eq2 negate_eq2); also; have "... <= norm x + norm (- 1r (*) y)"; by (simp! add: seminorm_subadditive); - also; have "norm (- 1r (*) y) = rabs (- 1r) * norm y"; - by (rule seminorm_rabs_homogenous); - also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); + also; have "norm (- 1r (*) y) = abs (- 1r) * norm y"; + by (rule seminorm_abs_homogenous); + also; have "abs (- 1r) = 1r"; by (rule abs_minus_one); finally; show "norm (x - y) <= norm x + norm y"; by simp; qed; @@ -64,9 +64,9 @@ proof -; assume "is_seminorm V norm" "x:V" "is_vectorspace V"; have "norm (- x) = norm (- 1r (*) x)"; by (simp! only: negate_eq1); - also; have "... = rabs (- 1r) * norm x"; - by (rule seminorm_rabs_homogenous); - also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); + also; have "... = abs (- 1r) * norm x"; + by (rule seminorm_abs_homogenous); + also; have "abs (- 1r) = 1r"; by (rule abs_minus_one); finally; show "norm (- x) = norm x"; by simp; qed; @@ -142,10 +142,10 @@ finally; show "0r < norm x"; .; qed; -lemma normed_vs_norm_rabs_homogenous [intro??]: +lemma normed_vs_norm_abs_homogenous [intro??]: "[| is_normed_vectorspace V norm; x:V |] - ==> norm (a (*) x) = (rabs a) * (norm x)"; - by (rule seminorm_rabs_homogenous, rule norm_is_seminorm, + ==> norm (a (*) x) = (abs a) * (norm x)"; + by (rule seminorm_abs_homogenous, rule norm_is_seminorm, rule normed_vs_norm); lemma normed_vs_norm_subadditive [intro??]: @@ -170,7 +170,7 @@ proof; fix x y a; presume "x : E"; show "0r <= norm x"; ..; - show "norm (a (*) x) = rabs a * norm x"; ..; + show "norm (a (*) x) = abs a * norm x"; ..; presume "y : E"; show "norm (x + y) <= norm x + norm y"; ..; qed (simp!)+; diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/RealAbs.ML --- a/src/HOL/Real/RealAbs.ML Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/RealAbs.ML Mon May 08 20:57:02 2000 +0200 @@ -9,62 +9,62 @@ Properties of the absolute value function over the reals (adapted version of previously proved theorems about abs) ----------------------------------------------------------------------------*) -Goalw [rabs_def] "rabs r = (if 0r<=r then r else -r)"; +Goalw [abs_real_def] "abs r = (if 0r<=r then r else -r)"; by Auto_tac; -qed "rabs_iff"; +qed "abs_iff"; -Goalw [rabs_def] "rabs 0r = 0r"; +Goalw [abs_real_def] "abs 0r = 0r"; by (rtac (real_le_refl RS if_P) 1); -qed "rabs_zero"; +qed "abs_zero"; -Addsimps [rabs_zero]; +Addsimps [abs_zero]; -Goalw [rabs_def] "rabs 0r = -0r"; +Goalw [abs_real_def] "abs 0r = -0r"; by (Simp_tac 1); -qed "rabs_minus_zero"; +qed "abs_minus_zero"; -Goalw [rabs_def] "0r<=x ==> rabs x = x"; +Goalw [abs_real_def] "0r<=x ==> abs x = x"; by (Asm_simp_tac 1); -qed "rabs_eqI1"; +qed "abs_eqI1"; -Goalw [rabs_def] "0r rabs x = x"; +Goalw [abs_real_def] "0r abs x = x"; by (Asm_simp_tac 1); -qed "rabs_eqI2"; +qed "abs_eqI2"; -Goalw [rabs_def,real_le_def] "x<0r ==> rabs x = -x"; +Goalw [abs_real_def,real_le_def] "x<0r ==> abs x = -x"; by (Asm_simp_tac 1); -qed "rabs_minus_eqI2"; +qed "abs_minus_eqI2"; -Goalw [rabs_def] "x<=0r ==> rabs x = -x"; +Goalw [abs_real_def] "x<=0r ==> abs x = -x"; by (asm_full_simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_minus_eqI1"; +qed "abs_minus_eqI1"; -Goalw [rabs_def] "0r<= rabs x"; +Goalw [abs_real_def] "0r<= abs x"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_ge_zero"; +qed "abs_ge_zero"; -Goalw [rabs_def] "rabs(rabs x)=rabs x"; +Goalw [abs_real_def] "abs(abs x)=abs (x::real)"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_idempotent"; +qed "abs_idempotent"; -Goalw [rabs_def] "(x=0r) = (rabs x = 0r)"; +Goalw [abs_real_def] "(x=0r) = (abs x = 0r)"; by (Full_simp_tac 1); -qed "rabs_zero_iff"; +qed "abs_zero_iff"; -Goal "(x ~= 0r) = (rabs x ~= 0r)"; -by (full_simp_tac (simpset() addsimps [rabs_zero_iff RS sym]) 1); -qed "rabs_not_zero_iff"; +Goal "(x ~= 0r) = (abs x ~= 0r)"; +by (full_simp_tac (simpset() addsimps [abs_zero_iff RS sym]) 1); +qed "abs_not_zero_iff"; -Goalw [rabs_def] "x<=rabs x"; +Goalw [abs_real_def] "x<=abs (x::real)"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_ge_self"; +qed "abs_ge_self"; -Goalw [rabs_def] "-x<=rabs x"; +Goalw [abs_real_def] "-x<=abs (x::real)"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_ge_minus_self"; +qed "abs_ge_minus_self"; (* case splits nightmare *) -Goalw [rabs_def] "rabs(x*y) = (rabs x)*(rabs y)"; +Goalw [abs_real_def] "abs (x * y) = abs x * abs (y::real)"; by (auto_tac (claset(), simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute, real_minus_mult_eq2])); @@ -75,9 +75,9 @@ by (dtac real_mult_less_zero1 5 THEN assume_tac 5); by (auto_tac (claset() addDs [real_less_asym,sym], simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac)); -qed "rabs_mult"; +qed "abs_mult"; -Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))"; +Goalw [abs_real_def] "x~= 0r ==> abs(rinv(x)) = rinv(abs(x))"; by (auto_tac (claset(), simpset() addsimps [real_minus_rinv])); by (ALLGOALS(dtac not_real_leE)); by (etac real_less_asym 1); @@ -86,40 +86,40 @@ by (rtac (real_rinv_less_zero RSN (2,real_less_asym)) 1); by (assume_tac 2); by (blast_tac (claset() addSDs [real_le_imp_less_or_eq]) 1); -qed "rabs_rinv"; +qed "abs_rinv"; -Goal "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))"; -by (asm_simp_tac (simpset() addsimps [rabs_mult, rabs_rinv]) 1); -qed "rabs_mult_rinv"; +Goal "y ~= 0r ==> abs(x*rinv(y)) = abs(x)*rinv(abs(y))"; +by (asm_simp_tac (simpset() addsimps [abs_mult, abs_rinv]) 1); +qed "abs_mult_rinv"; -Goalw [rabs_def] "rabs(x+y) <= rabs x + rabs y"; +Goalw [abs_real_def] "abs(x+y) <= abs x + abs (y::real)"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_triangle_ineq"; +qed "abs_triangle_ineq"; (*Unused, but perhaps interesting as an example*) -Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)"; -by (simp_tac (simpset() addsimps [rabs_triangle_ineq RS order_trans]) 1); -qed "rabs_triangle_ineq_four"; +Goal "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)"; +by (simp_tac (simpset() addsimps [abs_triangle_ineq RS order_trans]) 1); +qed "abs_triangle_ineq_four"; -Goalw [rabs_def] "rabs(-x)=rabs(x)"; +Goalw [abs_real_def] "abs(-x)=abs(x::real)"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_minus_cancel"; +qed "abs_minus_cancel"; -Goalw [rabs_def] "rabs(x + (-y)) = rabs (y + (-x))"; +Goalw [abs_real_def] "abs(x + (-y)) = abs (y + (-(x::real)))"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_minus_add_cancel"; +qed "abs_minus_add_cancel"; -Goalw [rabs_def] "rabs(x + (-y)) <= rabs x + rabs y"; +Goalw [abs_real_def] "abs(x + (-y)) <= abs x + abs (y::real)"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_triangle_minus_ineq"; +qed "abs_triangle_minus_ineq"; -Goalw [rabs_def] "rabs x < r --> rabs y < s --> rabs(x+y) < r+s"; +Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed_spec_mp "rabs_add_less"; +qed_spec_mp "abs_add_less"; -Goalw [rabs_def] "rabs x < r --> rabs y < s --> rabs(x+ (-y)) < r+s"; +Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)"; by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); -qed "rabs_add_minus_less"; +qed "abs_add_minus_less"; (* lemmas manipulating terms *) Goal "(0r*x rabs(x*y) abs(x*y) rabs(x)*rabs(y) abs(x)*abs(y) rabs y <= rabs(x*y)"; -by (cut_inst_tac [("x1","y")] (rabs_ge_zero RS real_le_imp_less_or_eq) 1); +Goal "1r < abs x ==> abs y <= abs(x*y)"; +by (cut_inst_tac [("x1","y")] (abs_ge_zero RS real_le_imp_less_or_eq) 1); by (EVERY1[etac disjE,rtac real_less_imp_le]); by (dres_inst_tac [("W","1r")] real_less_sum_gt_zero 1); -by (forw_inst_tac [("y","rabs x + (-1r)")] real_mult_order 1); +by (forw_inst_tac [("y","abs x + (-1r)")] real_mult_order 1); by (assume_tac 1); by (rtac real_sum_gt_zero_less 1); by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2, - real_mult_commute, rabs_mult]) 1); + real_mult_commute, abs_mult]) 1); by (dtac sym 1); -by (asm_full_simp_tac (simpset() addsimps [rabs_mult]) 1); -qed "rabs_mult_le"; +by (asm_full_simp_tac (simpset() addsimps [abs_mult]) 1); +qed "abs_mult_le"; -Goal "[| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)"; -by (blast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1); -qed "rabs_mult_gt"; +Goal "[| 1r < abs x; r < abs y|] ==> r < abs(x*y)"; +by (blast_tac (HOL_cs addIs [abs_mult_le, real_less_le_trans]) 1); +qed "abs_mult_gt"; -Goal "rabs(x) 0r 0r 0r < k + rabs(x)"; -by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0])); -qed "rabs_add_pos_gt_zero"; +qed "abs_add_minus_interval_iff"; -Goalw [rabs_def] "0r < 1r + rabs(x)"; +Goalw [abs_real_def] "0r < k ==> 0r < k + abs(x)"; +by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0])); +qed "abs_add_pos_gt_zero"; + +Goalw [abs_real_def] "0r < 1r + abs(x)"; by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1])); -qed "rabs_add_one_gt_zero"; -Addsimps [rabs_add_one_gt_zero]; - +qed "abs_add_one_gt_zero"; +Addsimps [abs_add_one_gt_zero]; diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/RealBin.ML --- a/src/HOL/Real/RealBin.ML Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/RealBin.ML Mon May 08 20:57:02 2000 +0200 @@ -110,10 +110,10 @@ Addsimps [le_real_number_of_eq_not_less]; -(** rabs (absolute value) **) +(** abs (absolute value) **) -Goalw [rabs_def] - "rabs (number_of v :: real) = \ +Goalw [abs_real_def] + "abs (number_of v :: real) = \ \ (if neg (number_of v) then number_of (bin_minus v) \ \ else number_of v)"; by (simp_tac @@ -121,9 +121,9 @@ bin_arith_simps@ [minus_real_number_of, zero_eq_numeral_0, le_real_number_of_eq_not_less, less_real_number_of, real_of_int_le_iff]) 1); -qed "rabs_nat_number_of"; +qed "abs_nat_number_of"; -Addsimps [rabs_nat_number_of]; +Addsimps [abs_nat_number_of]; (*** New versions of existing theorems involving 0r, 1r ***) @@ -210,10 +210,10 @@ Addsimprocs [fast_real_arith_simproc] end; -Goalw [rabs_def] - "P(rabs x) = ((#0 <= x --> P x) & (x < #0 --> P(-x)))"; +Goalw [abs_real_def] + "P(abs (x::real)) = ((#0 <= x --> P x) & (x < #0 --> P(-x)))"; by(auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0])); -qed "rabs_split"; +qed "abs_split"; -arith_tac_split_thms := !arith_tac_split_thms @ [rabs_split]; +arith_tac_split_thms := !arith_tac_split_thms @ [abs_split]; diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/RealOrd.thy --- a/src/HOL/Real/RealOrd.thy Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/RealOrd.thy Mon May 08 20:57:02 2000 +0200 @@ -11,8 +11,7 @@ instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le) instance real :: linorder (real_le_linear) -constdefs - rabs :: real => real - "rabs r == if 0r<=r then r else -r" +defs + abs_real_def "abs r == (if 0r <= r then r else -r)" end diff -r 9ee87bdcba05 -r 4eaa99f0d223 src/HOL/Real/RealPow.ML --- a/src/HOL/Real/RealPow.ML Mon May 08 18:20:04 2000 +0200 +++ b/src/HOL/Real/RealPow.ML Mon May 08 20:57:02 2000 +0200 @@ -30,11 +30,11 @@ simpset())); qed_spec_mp "realpow_rinv"; -Goal "rabs r ^ n = rabs (r ^ n)"; +Goal "abs (r::real) ^ n = abs (r ^ n)"; by (induct_tac "n" 1); by (auto_tac (claset(),simpset() addsimps - [rabs_mult,rabs_one])); -qed "realpow_rabs"; + [abs_mult,abs_one])); +qed "realpow_abs"; Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"; by (induct_tac "n" 1); @@ -100,18 +100,18 @@ Addsimps (map (rename_numerals thy) [realpow_zero, realpow_eq_one]); -Goal "rabs(-(1r ^ n)) = 1r"; +Goal "abs(-(1r ^ n)) = 1r"; by (simp_tac (simpset() addsimps - [rabs_minus_cancel,rabs_one]) 1); -qed "rabs_minus_realpow_one"; -Addsimps [rabs_minus_realpow_one]; + [abs_minus_cancel,abs_one]) 1); +qed "abs_minus_realpow_one"; +Addsimps [abs_minus_realpow_one]; -Goal "rabs((-1r) ^ n) = 1r"; +Goal "abs((-1r) ^ n) = 1r"; by (induct_tac "n" 1); -by (auto_tac (claset(),simpset() addsimps [rabs_mult, - rabs_minus_cancel,rabs_one])); -qed "rabs_realpow_minus_one"; -Addsimps [rabs_realpow_minus_one]; +by (auto_tac (claset(),simpset() addsimps [abs_mult, + abs_minus_cancel,abs_one])); +qed "abs_realpow_minus_one"; +Addsimps [abs_realpow_minus_one]; Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"; by (induct_tac "n" 1); @@ -123,16 +123,16 @@ qed "realpow_two_le"; Addsimps [realpow_two_le]; -Goal "rabs(x ^ 2) = x ^ 2"; -by (simp_tac (simpset() addsimps [rabs_eqI1]) 1); -qed "rabs_realpow_two"; -Addsimps [rabs_realpow_two]; +Goal "abs((x::real) ^ 2) = x ^ 2"; +by (simp_tac (simpset() addsimps [abs_eqI1]) 1); +qed "abs_realpow_two"; +Addsimps [abs_realpow_two]; -Goal "rabs(x) ^ 2 = x ^ 2"; +Goal "abs(x::real) ^ 2 = x ^ 2"; by (simp_tac (simpset() addsimps - [realpow_rabs,rabs_eqI1] delsimps [realpow_Suc]) 1); -qed "realpow_two_rabs"; -Addsimps [realpow_two_rabs]; + [realpow_abs,abs_eqI1] delsimps [realpow_Suc]) 1); +qed "realpow_two_abs"; +Addsimps [realpow_two_abs]; Goal "1r < r ==> 1r < r ^ 2"; by (auto_tac (claset(),simpset() addsimps [realpow_two])); @@ -373,5 +373,5 @@ Addsimps (map (rename_numerals thy) [realpow_two_le, realpow_zero_le, - rabs_minus_realpow_one, rabs_realpow_minus_one, + abs_minus_realpow_one, abs_realpow_minus_one, realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);