--- 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;
--- 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; .;
--- 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]);
--- 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);
--- 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);
--- 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!)+;
--- 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<x ==> rabs x = x";
+Goalw [abs_real_def] "0r<x ==> 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<r)=(0r<r)";
@@ -139,69 +139,68 @@
(* proofs lifted from previous older version
FIXME: use a stronger version of real_mult_less_mono *)
-Goal "[| rabs x<r; rabs y<s |] ==> rabs(x*y)<r*s";
-by (simp_tac (simpset() addsimps [rabs_mult]) 1);
+Goal "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::real)";
+by (simp_tac (simpset() addsimps [abs_mult]) 1);
by (rtac real_mult_le_less_trans 1);
-by (rtac rabs_ge_zero 1);
+by (rtac abs_ge_zero 1);
by (assume_tac 1);
-by (blast_tac (HOL_cs addIs [rabs_ge_zero, real_mult_less_mono1,
+by (blast_tac (HOL_cs addIs [abs_ge_zero, real_mult_less_mono1,
real_le_less_trans]) 1);
-by (blast_tac (HOL_cs addIs [rabs_ge_zero, real_mult_order,
+by (blast_tac (HOL_cs addIs [abs_ge_zero, real_mult_order,
real_le_less_trans]) 1);
-qed "rabs_mult_less";
+qed "abs_mult_less";
-Goal "[| rabs x < r; rabs y < s |] ==> rabs(x)*rabs(y)<r*s";
-by (auto_tac (claset() addIs [rabs_mult_less],
- simpset() addsimps [rabs_mult RS sym]));
-qed "rabs_mult_less2";
+Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y)<r*(s::real)";
+by (auto_tac (claset() addIs [abs_mult_less],
+ simpset() addsimps [abs_mult RS sym]));
+qed "abs_mult_less2";
-Goal "1r < rabs x ==> 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)<r ==> 0r<r";
-by (blast_tac (claset() addSIs [real_le_less_trans,rabs_ge_zero]) 1);
-qed "rabs_less_gt_zero";
+Goal "abs(x)<r ==> 0r<r";
+by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1);
+qed "abs_less_gt_zero";
-Goalw [rabs_def] "rabs 1r = 1r";
+Goalw [abs_real_def] "abs 1r = 1r";
by (simp_tac (simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1]) 1);
-qed "rabs_one";
+qed "abs_one";
-Goalw [rabs_def] "rabs x =x | rabs x = -x";
+Goalw [abs_real_def] "abs x =x | abs x = -(x::real)";
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
-qed "rabs_disj";
+qed "abs_disj";
-Goalw [rabs_def] "(rabs x < r) = (-r<x & x<r)";
+Goalw [abs_real_def] "(abs x < r) = (-r<x & x<(r::real))";
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
-qed "rabs_interval_iff";
+qed "abs_interval_iff";
-Goalw [rabs_def] "(rabs x <= r) = (-r<=x & x<=r)";
+Goalw [abs_real_def] "(abs x <= r) = (-r<=x & x<=(r::real))";
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
-qed "rabs_le_interval_iff";
+qed "abs_le_interval_iff";
-Goalw [rabs_def] "(rabs (x + (-y)) < r) = (y + (-r) < x & x < y + r)";
+Goalw [abs_real_def] "(abs (x + (-y)) < r) = (y + (-r) < x & x < y + (r::real))";
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
-qed "rabs_add_minus_interval_iff";
-
-Goalw [rabs_def] "0r < k ==> 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];
--- 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];
--- 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
--- 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]);