Updated files to remove 0r and 1r from theorems in descendant theories
of RealBin. Some new theorems added.
--- a/src/HOL/Real/HahnBanach/Aux.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Thu Jun 01 11:22:27 2000 +0200
@@ -53,58 +53,83 @@
text_raw {* \medskip *};
text{* Some lemmas for the reals. *};
-lemma real_add_minus_eq: "x - y = 0r ==> x = y";
-proof -;
- assume "x - y = 0r";
- have "x + - y = 0r"; by (simp!);
- hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
- also; have "... = y"; by simp;
- finally; show "?thesis"; .;
-qed;
+lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y";
+ by simp;
+
+lemma abs_minus_one: "abs (- (#1::real)) = #1";
+ by simp;
+
-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 "abs (- 1r) = - (- 1r)";
- by (rule abs_minus_eqI2);
- also; have "... = 1r"; by simp;
- finally; show ?thesis; .;
+lemma real_mult_le_le_mono1a:
+ "[| (#0::real) <= z; x <= y |] ==> z * x <= z * y";
+proof -;
+ assume "(#0::real) <= z" "x <= y";
+ hence "x < y | x = y"; by (force simp add: order_le_less);
+ thus ?thesis;
+ proof (elim disjE);
+ assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono2) simp;
+ next;
+ assume "x = y"; thus ?thesis;; by simp;
+ qed;
qed;
lemma real_mult_le_le_mono2:
- "[| 0r <= z; x <= y |] ==> x * z <= y * z";
+ "[| (#0::real) <= z; x <= y |] ==> x * z <= y * z";
proof -;
- assume "0r <= z" "x <= y";
+ assume "(#0::real) <= z" "x <= y";
hence "x < y | x = y"; by (force simp add: order_le_less);
thus ?thesis;
proof (elim disjE);
- assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono1);
+ assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono1) simp;
next;
- assume "x = y"; thus ?thesis;; by simp;
+ assume "x = y"; thus ?thesis;; by simp;
qed;
qed;
lemma real_mult_less_le_anti:
- "[| z < 0r; x <= y |] ==> z * y <= z * x";
+ "[| z < (#0::real); x <= y |] ==> z * y <= z * x";
proof -;
- assume "z < 0r" "x <= y";
- hence "0r < - z"; by simp;
- hence "0r <= - z"; by (rule real_less_imp_le);
- hence "(- z) * x <= (- z) * y";
- by (rule real_mult_le_le_mono1);
- hence "- (z * x) <= - (z * y)";
- by (simp only: real_minus_mult_eq1);
+ assume "z < (#0::real)" "x <= y";
+ hence "(#0::real) < - z"; by simp;
+ hence "(#0::real) <= - z"; by (rule real_less_imp_le);
+ hence "x * (- z) <= y * (- z)";
+ by (rule real_mult_le_le_mono2);
+ hence "- (x * z) <= - (y * z)";
+ by (simp only: real_minus_mult_eq2);
+ thus ?thesis; by (simp only: real_mult_commute);
+qed;
+
+lemma real_mult_less_le_mono:
+ "[| (#0::real) < z; x <= y |] ==> z * x <= z * y";
+proof -;
+ assume "(#0::real) < z" "x <= y";
+ have "(#0::real) <= z"; by (rule real_less_imp_le);
+ hence "x * z <= y * z";
+ by (rule real_mult_le_le_mono2);
+ thus ?thesis; by (simp only: real_mult_commute);
+qed;
+
+lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x";
+proof -;
+ assume "#0 < x";
+ have "0r < x"; by simp;
+ hence "0r < rinv x"; by (rule real_rinv_gt_zero);
thus ?thesis; by simp;
qed;
-lemma real_mult_less_le_mono:
- "[| 0r < z; x <= y |] ==> z * x <= z * y";
-proof -;
- assume "0r < z" "x <= y";
- have "0r <= z"; by (rule real_less_imp_le);
- thus ?thesis; by (rule real_mult_le_le_mono1);
+lemma real_mult_inv_right1: "x ~= #0 ==> x*rinv(x) = #1";
+ by simp;
+
+lemma real_mult_inv_left1: "x ~= #0 ==> rinv(x)*x = #1";
+ by simp;
+
+lemma real_le_mult_order1a:
+ "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y";
+proof -;
+ assume "#0 <= x" "#0 <= y";
+ have "[|0r <= x; 0r <= y|] ==> 0r <= x * y";
+ by (rule real_le_mult_order);
+ thus ?thesis; by (simp!);
qed;
lemma real_mult_diff_distrib:
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Jun 01 11:22:27 2000 +0200
@@ -66,7 +66,7 @@
constdefs
B :: "[ 'a set, 'a => real, 'a => real ] => real set"
"B V norm f ==
- {0r} \Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x:V}";
+ {(#0::real)} \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$.
@@ -84,7 +84,7 @@
function_norm :: " ['a set, 'a => real, 'a => real] => real"
"function_norm V norm f == Sup UNIV (B V norm f)";
-lemma B_not_empty: "0r : B V norm f";
+lemma B_not_empty: "(#0::real) : B V norm f";
by (unfold B_def, force);
text {* The following lemma states that every continuous linear form
@@ -110,7 +110,7 @@
show "EX X. X : B V norm f";
proof (intro exI);
- show "0r : (B V norm f)"; by (unfold B_def, force);
+ show "(#0::real) : (B V norm f)"; by (unfold B_def, force);
qed;
txt {* Then we have to show that $B$ is bounded: *};
@@ -121,7 +121,7 @@
txt {* We know that $f$ is bounded by some value $c$. *};
fix c; assume a: "ALL x:V. abs (f x) <= c * norm x";
- def b == "max c 0r";
+ def b == "max c (#0::real)";
show "?thesis";
proof (intro exI isUbI setleI ballI, unfold B_def,
@@ -132,7 +132,7 @@
Due to the definition of $B$ there are two cases for
$y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *};
- fix y; assume "y = 0r";
+ fix y; assume "y = (#0::real)";
show "y <= b"; by (simp! add: le_max2);
txt{* The second case is
@@ -143,22 +143,22 @@
fix x y;
assume "x:V" "x ~= 00"; (***
- have ge: "0r <= rinv (norm x)";
+ have ge: "(#0::real) <= rinv (norm x)";
by (rule real_less_imp_le, rule real_rinv_gt_zero,
rule normed_vs_norm_gt_zero); (***
proof (rule real_less_imp_le);
- show "0r < rinv (norm x)";
+ show "(#0::real) < rinv (norm x)";
proof (rule real_rinv_gt_zero);
- show "0r < norm x"; ..;
+ show "(#0::real) < norm x"; ..;
qed;
qed; ***)
- have nz: "norm x ~= 0r";
+ have nz: "norm x ~= (#0::real)";
by (rule not_sym, rule lt_imp_not_eq,
rule normed_vs_norm_gt_zero); (***
proof (rule not_sym);
- show "0r ~= norm x";
+ show "(#0::real) ~= norm x";
proof (rule lt_imp_not_eq);
- show "0r < norm x"; ..;
+ show "(#0::real) < norm x"; ..;
qed;
qed; ***)***)
@@ -168,16 +168,16 @@
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,
+ show "(#0::real) <= rinv (norm x)";
+ by (rule real_less_imp_le, rule real_rinv_gt_zero1,
rule normed_vs_norm_gt_zero);
from a; show "abs (f x) <= c * norm x"; ..;
qed;
also; have "... = c * (norm x * rinv (norm x))";
by (rule real_mult_assoc);
- also; have "(norm x * rinv (norm x)) = 1r";
- proof (rule real_mult_inv_right);
- show nz: "norm x ~= 0r";
+ also; have "(norm x * rinv (norm x)) = (#1::real)";
+ proof (rule real_mult_inv_right1);
+ show nz: "norm x ~= (#0::real)";
by (rule not_sym, rule lt_imp_not_eq,
rule normed_vs_norm_gt_zero);
qed;
@@ -192,7 +192,7 @@
lemma fnorm_ge_zero [intro??]:
"[| is_continuous V norm f; is_normed_vectorspace V norm|]
- ==> 0r <= function_norm V norm f";
+ ==> (#0::real) <= function_norm V norm f";
proof -;
assume c: "is_continuous V norm f"
and n: "is_normed_vectorspace V norm";
@@ -203,24 +203,24 @@
show ?thesis;
proof (unfold function_norm_def, rule sup_ub1);
- show "ALL x:(B V norm f). 0r <= x";
+ show "ALL x:(B V norm f). (#0::real) <= x";
proof (intro ballI, unfold B_def,
elim UnE singletonE CollectE exE conjE);
fix x r;
assume "x : V" "x ~= 00"
and r: "r = abs (f x) * rinv (norm x)";
- 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);(***
+ have ge: "(#0::real) <= abs (f x)"; by (simp! only: abs_ge_zero);
+ have "(#0::real) <= rinv (norm x)";
+ by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule);(***
proof (rule real_less_imp_le);
- show "0r < rinv (norm x)";
+ show "(#0::real) < rinv (norm x)";
proof (rule real_rinv_gt_zero);
- show "0r < norm x"; ..;
+ show "(#0::real) < norm x"; ..;
qed;
qed; ***)
- with ge; show "0r <= r";
- by (simp only: r, rule real_le_mult_order);
+ with ge; show "(#0::real) <= r";
+ by (simp only: r, rule real_le_mult_order1a);
qed (simp!);
txt {* Since $f$ is continuous the function norm exists: *};
@@ -231,7 +231,7 @@
txt {* $B$ is non-empty by construction: *};
- show "0r : B V norm f"; by (rule B_not_empty);
+ show "(#0::real) : B V norm f"; by (rule B_not_empty);
qed;
qed;
@@ -261,22 +261,22 @@
assume "x = 00";
have "abs (f x) = abs (f 00)"; by (simp!);
- also; from v continuous_linearform; have "f 00 = 0r"; ..;
+ also; from v continuous_linearform; have "f 00 = (#0::real)"; ..;
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"; ..;
+ also; have "(#0::real) <= function_norm V norm f * norm x";
+ proof (rule real_le_mult_order1a);
+ show "(#0::real) <= function_norm V norm f"; ..;
+ show "(#0::real) <= norm x"; ..;
qed;
finally;
show "abs (f x) <= function_norm V norm f * norm x"; .;
next;
assume "x ~= 00";
- have n: "0r <= norm x"; ..;
- have nz: "norm x ~= 0r";
+ have n: "(#0::real) <= norm x"; ..;
+ have nz: "norm x ~= (#0::real)";
proof (rule lt_imp_not_eq [RS not_sym]);
- show "0r < norm x"; ..;
+ show "(#0::real) < norm x"; ..;
qed;
txt {* For the case $x\neq \zero$ we derive the following
@@ -294,9 +294,9 @@
txt {* The thesis now follows by a short calculation: *};
- 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]);
+ have "abs (f x) = abs (f x) * (#1::real)"; by (simp!);
+ also; from nz; have "(#1::real) = rinv (norm x) * norm x";
+ by (rule real_mult_inv_left1 [RS sym]);
also;
have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x";
by (simp! add: real_mult_assoc [of "abs (f x)"]);
@@ -316,13 +316,13 @@
lemma fnorm_le_ub:
"[| is_normed_vectorspace V norm; is_continuous V norm f;
- ALL x:V. abs (f x) <= c * norm x; 0r <= c |]
+ ALL x:V. abs (f x) <= c * norm x; (#0::real) <= 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. abs (f x) <= c * norm x"
- and "0r <= c";
+ and "(#0::real) <= c";
txt {* Suppose the inequation holds for some $c\geq 0$.
If $c$ is an upper bound of $B$, then $c$ is greater
@@ -347,7 +347,7 @@
txt {* The first case for $y\in B$ is $y=0$. *};
- assume "y = 0r";
+ assume "y = (#0::real)";
show "y <= c"; by (force!);
txt{* The second case is
@@ -358,18 +358,18 @@
fix x;
assume "x : V" "x ~= 00";
- have lz: "0r < norm x";
+ have lz: "(#0::real) < norm x";
by (simp! add: normed_vs_norm_gt_zero);
- have nz: "norm x ~= 0r";
+ have nz: "norm x ~= (#0::real)";
proof (rule not_sym);
- from lz; show "0r ~= norm x";
+ from lz; show "(#0::real) ~= norm x";
by (simp! add: order_less_imp_not_eq);
qed;
- from lz; have "0r < rinv (norm x)";
- by (simp! add: real_rinv_gt_zero);
- hence rinv_gez: "0r <= rinv (norm x)";
+ from lz; have "(#0::real) < rinv (norm x)";
+ by (simp! add: real_rinv_gt_zero1);
+ hence rinv_gez: "(#0::real) <= rinv (norm x)";
by (rule real_less_imp_le);
assume "y = abs (f x) * rinv (norm x)";
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Jun 01 11:22:27 2000 +0200
@@ -206,7 +206,7 @@
proof (rule graph_extI);
fix t; assume "t:H";
have "(SOME (y, a). t = y + a (*) x0 & y : H)
- = (t,0r)";
+ = (t,#0)";
by (rule decomp_H0_H [OF _ _ _ _ _ x0]);
thus "h t = h0 t"; by (simp! add: Let_def);
next;
@@ -261,11 +261,11 @@
proof (rule graph_extI);
fix x; assume "x:F";
have "f x = h x"; ..;
- also; have " ... = h x + 0r * xi"; by simp;
- also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
+ also; have " ... = h x + #0 * xi"; by simp;
+ also; have "... = (let (y,a) = (x, #0) in h y + a * xi)";
by (simp add: Let_def);
also; have
- "(x, 0r) = (SOME (y, a). x = y + a (*) x0 & y : H)";
+ "(x, #0) = (SOME (y, a). x = y + a (*) x0 & y : H)";
by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+;
also; have
"(let (y,a) = (SOME (y,a). x = y + a (*) x0 & y : H)
@@ -480,7 +480,7 @@
have "graph H h <= graph H0 h0";
proof (rule graph_extI);
fix t; assume "t:H";
- have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,0r)";
+ have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,#0)";
by (rule decomp_H0_H, rule x0);
thus "h t = h0 t"; by (simp! add: Let_def);
next;
@@ -541,11 +541,11 @@
proof (rule graph_extI);
fix x; assume "x:F";
have "f x = h x"; ..;
- also; have " ... = h x + 0r * xi"; by simp;
- also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
+ also; have " ... = h x + #0 * xi"; by simp;
+ also; have "... = (let (y,a) = (x, #0) in h y + a * xi)";
by (simp add: Let_def);
also; have
- "(x, 0r) = (SOME (y, a). x = y + a ( * ) x0 & y : H)";
+ "(x, #0) = (SOME (y, a). x = y + a ( * ) x0 & y : H)";
by (rule decomp_H0_H [RS sym], rule x0) (simp!)+;
also; have
"(let (y,a) = (SOME (y,a). x = y + a ( * ) x0 & y : H)
@@ -664,10 +664,10 @@
txt{* $p$ is positive definite: *};
- show "0r <= p x";
- proof (unfold p_def, rule real_le_mult_order);
- from _ f_norm; show "0r <= function_norm F norm f"; ..;
- show "0r <= norm x"; ..;
+ show "#0 <= p x";
+ proof (unfold p_def, rule real_le_mult_order1a);
+ from _ f_norm; show "#0 <= function_norm F norm f"; ..;
+ show "#0 <= norm x"; ..;
qed;
txt{* $p$ is absolutely homogenous: *};
@@ -693,8 +693,8 @@
by (simp!);
also;
have "... <= function_norm F norm f * (norm x + norm y)";
- proof (rule real_mult_le_le_mono1);
- from _ f_norm; show "0r <= function_norm F norm f"; ..;
+ proof (rule real_mult_le_le_mono1a);
+ from _ f_norm; show "#0 <= function_norm F norm f"; ..;
show "norm (x + y) <= norm x + norm y"; ..;
qed;
also; have "... = function_norm F norm f * norm x
@@ -774,7 +774,7 @@
with _ g_cont; show "?L <= ?R";
proof (rule fnorm_le_ub);
- from f_cont f_norm; show "0r <= function_norm F norm f"; ..;
+ from f_cont f_norm; show "#0 <= function_norm F norm f"; ..;
qed;
txt{* The other direction is achieved by a similar
@@ -794,7 +794,7 @@
qed;
thus "?R <= ?L";
proof (rule fnorm_le_ub [OF f_norm f_cont]);
- from g_cont; show "0r <= function_norm E norm g"; ..;
+ from g_cont; show "#0 <= function_norm E norm g"; ..;
qed;
qed;
qed;
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Jun 01 11:22:27 2000 +0200
@@ -275,14 +275,14 @@
also; have "... <= p (y + a (*) x0)";
proof (rule linorder_linear_split);
- assume z: "a = 0r";
+ assume z: "a = (#0::real)";
with vs y a; show ?thesis; by simp;
txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$
taken as $y/a$: *};
next;
- assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
+ assume lz: "a < #0"; hence nz: "a ~= #0"; by simp;
from a1;
have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi";
by (rule bspec) (simp!);
@@ -312,7 +312,7 @@
taken as $y/a$: *};
next;
- assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
+ assume gz: "#0 < a"; hence nz: "a ~= #0"; by simp;
from a2;
have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)";
by (rule bspec) (simp!);
--- a/src/HOL/Real/HahnBanach/Linearform.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Thu Jun 01 11:22:27 2000 +0200
@@ -35,8 +35,8 @@
==> f (- x) = - f x";
proof -;
assume "is_linearform V f" "is_vectorspace V" "x:V";
- have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1);
- also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
+ have "f (- x) = f ((- (#1::real)) (*) x)"; by (simp! add: negate_eq1);
+ also; have "... = (- #1) * (f x)"; by (rule linearform_mult);
also; have "... = - (f x)"; by (simp!);
finally; show ?thesis; .;
qed;
@@ -56,14 +56,14 @@
text{* Every linear form yields $0$ for the $\zero$ vector.*};
lemma linearform_zero [intro??, simp]:
- "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r";
+ "[| is_vectorspace V; is_linearform V f |] ==> f 00 = (#0::real)";
proof -;
assume "is_vectorspace V" "is_linearform V f";
have "f 00 = f (00 - 00)"; by (simp!);
also; have "... = f 00 - f 00";
by (rule linearform_diff) (simp!)+;
- also; have "... = 0r"; by simp;
- finally; show "f 00 = 0r"; .;
+ also; have "... = (#0::real)"; by simp;
+ finally; show "f 00 = (#0::real)"; .;
qed;
end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Thu Jun 01 11:22:27 2000 +0200
@@ -18,19 +18,19 @@
constdefs
is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
"is_seminorm V norm == ALL x: V. ALL y:V. ALL a.
- 0r <= norm x
+ (#0::real) <= 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 y a. [| x:V; y:V|] ==> (#0::real) <= 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);
lemma seminorm_ge_zero [intro??]:
- "[| is_seminorm V norm; x:V |] ==> 0r <= norm x";
+ "[| is_seminorm V norm; x:V |] ==> (#0::real) <= norm x";
by (unfold is_seminorm_def, force);
lemma seminorm_abs_homogenous:
@@ -48,13 +48,13 @@
==> norm (x - y) <= norm x + norm y";
proof -;
assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V";
- have "norm (x - y) = norm (x + - 1r (*) y)";
- by (simp! add: diff_eq2 negate_eq2);
- also; have "... <= norm x + norm (- 1r (*) y)";
+ have "norm (x - y) = norm (x + - (#1::real) (*) y)";
+ by (simp! add: diff_eq2 negate_eq2a);
+ also; have "... <= norm x + norm (- (#1::real) (*) y)";
by (simp! add: seminorm_subadditive);
- also; have "norm (- 1r (*) y) = abs (- 1r) * norm y";
+ also; have "norm (- (#1::real) (*) y) = abs (- (#1::real)) * norm y";
by (rule seminorm_abs_homogenous);
- also; have "abs (- 1r) = 1r"; by (rule abs_minus_one);
+ also; have "abs (- (#1::real)) = (#1::real)"; by (rule abs_minus_one);
finally; show "norm (x - y) <= norm x + norm y"; by simp;
qed;
@@ -63,10 +63,10 @@
==> norm (- x) = norm x";
proof -;
assume "is_seminorm V norm" "x:V" "is_vectorspace V";
- have "norm (- x) = norm (- 1r (*) x)"; by (simp! only: negate_eq1);
- also; have "... = abs (- 1r) * norm x";
+ have "norm (- x) = norm (- (#1::real) (*) x)"; by (simp! only: negate_eq1);
+ also; have "... = abs (- (#1::real)) * norm x";
by (rule seminorm_abs_homogenous);
- also; have "abs (- 1r) = 1r"; by (rule abs_minus_one);
+ also; have "abs (- (#1::real)) = (#1::real)"; by (rule abs_minus_one);
finally; show "norm (- x) = norm x"; by simp;
qed;
@@ -79,10 +79,10 @@
constdefs
is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
"is_norm V norm == ALL x: V. is_seminorm V norm
- & (norm x = 0r) = (x = 00)";
+ & (norm x = (#0::real)) = (x = 00)";
lemma is_normI [intro]:
- "ALL x: V. is_seminorm V norm & (norm x = 0r) = (x = 00)
+ "ALL x: V. is_seminorm V norm & (norm x = (#0::real)) = (x = 00)
==> is_norm V norm"; by (simp only: is_norm_def);
lemma norm_is_seminorm [intro??]:
@@ -90,11 +90,11 @@
by (unfold is_norm_def, force);
lemma norm_zero_iff:
- "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = 00)";
+ "[| is_norm V norm; x:V |] ==> (norm x = (#0::real)) = (x = 00)";
by (unfold is_norm_def, force);
lemma norm_ge_zero [intro??]:
- "[|is_norm V norm; x:V |] ==> 0r <= norm x";
+ "[|is_norm V norm; x:V |] ==> (#0::real) <= norm x";
by (unfold is_norm_def is_seminorm_def, force);
@@ -124,22 +124,22 @@
by (unfold is_normed_vectorspace_def, elim conjE);
lemma normed_vs_norm_ge_zero [intro??]:
- "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
+ "[| is_normed_vectorspace V norm; x:V |] ==> (#0::real) <= norm x";
by (unfold is_normed_vectorspace_def, rule, elim conjE);
lemma normed_vs_norm_gt_zero [intro??]:
- "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> 0r < norm x";
+ "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> (#0::real) < norm x";
proof (unfold is_normed_vectorspace_def, elim conjE);
assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm";
- have "0r <= norm x"; ..;
- also; have "0r ~= norm x";
+ have "(#0::real) <= norm x"; ..;
+ also; have "(#0::real) ~= norm x";
proof;
- presume "norm x = 0r";
+ presume "norm x = (#0::real)";
also; have "?this = (x = 00)"; by (rule norm_zero_iff);
finally; have "x = 00"; .;
thus "False"; by contradiction;
qed (rule sym);
- finally; show "0r < norm x"; .;
+ finally; show "(#0::real) < norm x"; .;
qed;
lemma normed_vs_norm_abs_homogenous [intro??]:
@@ -169,14 +169,14 @@
show "is_seminorm F norm";
proof;
fix x y a; presume "x : E";
- show "0r <= norm x"; ..;
+ show "(#0::real) <= norm x"; ..;
show "norm (a (*) x) = abs a * norm x"; ..;
presume "y : E";
show "norm (x + y) <= norm x + norm y"; ..;
qed (simp!)+;
fix x; assume "x : F";
- show "(norm x = 0r) = (x = 00)";
+ show "(norm x = (#0::real)) = (x = 00)";
proof (rule norm_zero_iff);
show "is_norm E norm"; ..;
qed (simp!);
--- a/src/HOL/Real/HahnBanach/Subspace.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Thu Jun 01 11:22:27 2000 +0200
@@ -87,7 +87,7 @@
show "00 : U"; ..;
show "ALL x:U. ALL a. a (*) x : U"; by (simp!);
show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
- show "ALL x:U. - x = -1r (*) x"; by (simp! add: negate_eq1);
+ show "ALL x:U. - x = -#1 (*) x"; by (simp! add: negate_eq1);
show "ALL x:U. ALL y:U. x - y = x + - y";
by (simp! add: diff_eq1);
qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
@@ -152,7 +152,7 @@
lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
proof (unfold lin_def, intro CollectI exI conjI);
assume "is_vectorspace V" "x:V";
- show "x = 1r (*) x"; by (simp!);
+ show "x = #1 (*) x"; by (simp!);
qed simp;
text {* Any linear closure is a subspace. *};
@@ -163,7 +163,7 @@
assume "is_vectorspace V" "x:V";
show "00 : lin x";
proof (unfold lin_def, intro CollectI exI conjI);
- show "00 = 0r (*) x"; by (simp!);
+ show "00 = (#0::real) (*) x"; by (simp!);
qed simp;
show "lin x <= V";
@@ -379,9 +379,9 @@
fix a; assume "x = a (*) x0";
show ?thesis;
proof cases;
- assume "a = 0r"; show ?thesis; by (simp!);
+ assume "a = (#0::real)"; show ?thesis; by (simp!);
next;
- assume "a ~= 0r";
+ assume "a ~= (#0::real)";
from h; have "rinv a (*) a (*) x0 : H";
by (rule subspace_mult_closed) (simp!);
also; have "rinv a (*) a (*) x0 = x0"; by (simp!);
@@ -419,15 +419,15 @@
lemma decomp_H0_H:
"[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
x0 ~= 00 |]
- ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, 0r)";
+ ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))";
proof (rule, unfold split_paired_all);
assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
"x0 ~= 00";
have h: "is_vectorspace H"; ..;
fix y a; presume t1: "t = y + a (*) x0" and "y:H";
- have "y = t & a = 0r";
+ have "y = t & a = (#0::real)";
by (rule decomp_H0) (assumption | (simp!))+;
- thus "(y, a) = (t, 0r)"; by (simp!);
+ thus "(y, a) = (t, (#0::real))"; by (simp!);
qed (simp!)+;
text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Thu Jun 01 11:22:27 2000 +0200
@@ -29,7 +29,7 @@
(***
constdefs
negate :: "'a => 'a" ("- _" [100] 100)
- "- x == (- 1r) ( * ) x"
+ "- x == (- (#1::real)) ( * ) x"
diff :: "'a => 'a => 'a" (infixl "-" 68)
"x - y == x + - y";
***)
@@ -59,8 +59,8 @@
& a (*) (x + y) = a (*) x + a (*) y
& (a + b) (*) x = a (*) x + b (*) x
& (a * b) (*) x = a (*) b (*) x
- & 1r (*) x = x
- & - x = (- 1r) (*) x
+ & (#1::real) (*) x = x
+ & - x = (- (#1::real)) (*) x
& x - y = x + - y)";
text_raw {* \medskip *};
@@ -77,8 +77,8 @@
ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y;
ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x;
ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x;
- ALL x:V. 1r (*) x = x;
- ALL x:V. - x = (- 1r) (*) x;
+ ALL x:V. (#1::real) (*) x = x;
+ ALL x:V. - x = (- (#1::real)) (*) x;
ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V";
proof (unfold is_vectorspace_def, intro conjI ballI allI);
fix x y z;
@@ -91,7 +91,7 @@
text {* The corresponding destruction rules are: *};
lemma negate_eq1:
- "[| is_vectorspace V; x:V |] ==> - x = (- 1r) (*) x";
+ "[| is_vectorspace V; x:V |] ==> - x = (- (#1::real)) (*) x";
by (unfold is_vectorspace_def) simp;
lemma diff_eq1:
@@ -99,7 +99,11 @@
by (unfold is_vectorspace_def) simp;
lemma negate_eq2:
- "[| is_vectorspace V; x:V |] ==> (- 1r) (*) x = - x";
+ "[| is_vectorspace V; x:V |] ==> (- (#1::real)) (*) x = - x";
+ by (unfold is_vectorspace_def) simp;
+
+lemma negate_eq2a:
+ "[| is_vectorspace V; x:V |] ==> ((#-1::real)) (*) x = - x";
by (unfold is_vectorspace_def) simp;
lemma diff_eq2:
@@ -201,7 +205,7 @@
by (simp only: vs_mult_assoc);
lemma vs_mult_1 [simp]:
- "[| is_vectorspace V; x:V |] ==> 1r (*) x = x";
+ "[| is_vectorspace V; x:V |] ==> (#1::real) (*) x = x";
by (unfold is_vectorspace_def) simp;
lemma vs_diff_mult_distrib1:
@@ -230,15 +234,15 @@
text{* Further derived laws: *};
lemma vs_mult_zero_left [simp]:
- "[| is_vectorspace V; x:V |] ==> 0r (*) x = 00";
+ "[| is_vectorspace V; x:V |] ==> (#0::real) (*) x = 00";
proof -;
assume "is_vectorspace V" "x:V";
- have "0r (*) x = (1r - 1r) (*) x"; by (simp only: real_diff_self);
- also; have "... = (1r + - 1r) (*) x"; by simp;
- also; have "... = 1r (*) x + (- 1r) (*) x";
+ have "(#0::real) (*) x = ((#1::real) - (#1::real)) (*) x"; by simp;
+ also; have "... = ((#1::real) + - (#1::real)) (*) x"; by simp;
+ also; have "... = (#1::real) (*) x + (- (#1::real)) (*) x";
by (rule vs_add_mult_distrib2);
- also; have "... = x + (- 1r) (*) x"; by (simp!);
- also; have "... = x + - x"; by (simp! add: negate_eq2);;
+ also; have "... = x + (- (#1::real)) (*) x"; by (simp!);
+ also; have "... = x + - x"; by (simp! add: negate_eq2a);;
also; have "... = x - x"; by (simp! add: diff_eq2);
also; have "... = 00"; by (simp!);
finally; show ?thesis; .;
@@ -354,25 +358,25 @@
by (simp add: real_mult_commute);
lemma vs_mult_zero_uniq :
- "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = 0r";
+ "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = (#0::real)";
proof (rule classical);
assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00";
- assume "a ~= 0r";
+ assume "a ~= (#0::real)";
have "x = (rinv a * a) (*) x"; by (simp!);
also; have "... = rinv a (*) (a (*) x)"; by (rule vs_mult_assoc);
also; have "... = rinv a (*) 00"; by (simp!);
also; have "... = 00"; by (simp!);
finally; have "x = 00"; .;
- thus "a = 0r"; by contradiction;
+ thus "a = (#0::real)"; by contradiction;
qed;
lemma vs_mult_left_cancel:
- "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==>
+ "[| is_vectorspace V; x:V; y:V; a ~= (#0::real) |] ==>
(a (*) x = a (*) y) = (x = y)"
(concl is "?L = ?R");
proof;
- assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
- have "x = 1r (*) x"; by (simp!);
+ assume "is_vectorspace V" "x:V" "y:V" "a ~= (#0::real)";
+ have "x = (#1::real) (*) x"; by (simp!);
also; have "... = (rinv a * a) (*) x"; by (simp!);
also; have "... = rinv a (*) (a (*) x)";
by (simp! only: vs_mult_assoc);
@@ -390,7 +394,7 @@
by (simp! add: vs_diff_mult_distrib2);
also; assume ?L; hence "a (*) x - b (*) x = 00"; by (simp!);
finally; have "(a - b) (*) x = 00"; .;
- hence "a - b = 0r"; by (simp! add: vs_mult_zero_uniq);
+ hence "a - b = (#0::real)"; by (simp! add: vs_mult_zero_uniq);
thus "a = b"; by (rule real_add_minus_eq);
qed simp; (***
@@ -404,7 +408,7 @@
assume l: ?L;
show "a = b";
proof (rule real_add_minus_eq);
- show "a - b = 0r";
+ show "a - b = (#0::real)";
proof (rule vs_mult_zero_uniq);
have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
by (simp! add: vs_diff_mult_distrib2);
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Thu Jun 01 11:22:27 2000 +0200
@@ -327,7 +327,7 @@
(**** hrinv: multiplicative inverse on hypreal ****)
Goalw [congruent_def]
- "congruent hyprel (%X. hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})";
+ "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else rinv(X n)})";
by (Auto_tac THEN Ultra_tac 1);
qed "hypreal_hrinv_congruent";
@@ -336,7 +336,7 @@
Goalw [hrinv_def]
"hrinv (Abs_hypreal(hyprel^^{%n. X n})) = \
-\ Abs_hypreal(hyprel ^^ {%n. if X n = 0r then 0r else rinv(X n)})";
+\ Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else rinv(X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
by (simp_tac (simpset() addsimps
[hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_hrinv_ize UN_equiv_class]) 1);
@@ -347,7 +347,8 @@
by (rotate_tac 1 1);
by (asm_full_simp_tac (simpset() addsimps
[hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1);
-by (ultra_tac (claset() addDs [rinv_not_zero,real_rinv_rinv],simpset()) 1);
+by (ultra_tac (claset() addDs (map (full_rename_numerals thy)
+ [rinv_not_zero,real_rinv_rinv]),simpset()) 1);
qed "hypreal_hrinv_hrinv";
Addsimps [hypreal_hrinv_hrinv];
@@ -718,7 +719,7 @@
hypreal_mult] setloop (split_tac [expand_if])) 1);
by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
by (ultra_tac (claset() addIs [ccontr] addDs
- [rinv_not_zero],simpset()) 1);
+ [full_rename_numerals thy rinv_not_zero],simpset()) 1);
qed "hrinv_not_zero";
Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
@@ -861,15 +862,16 @@
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSIs [exI],simpset() addsimps
[hypreal_less_def,hypreal_mult]));
-by (ultra_tac (claset() addIs [real_mult_order],simpset()) 1);
+by (ultra_tac (claset() addIs [rename_numerals thy
+ real_mult_order],simpset()) 1);
qed "hypreal_mult_order";
(*---------------------------------------------------------------------------------
Trichotomy of the hyperreals
--------------------------------------------------------------------------------*)
-Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. 0r}";
-by (res_inst_tac [("x","%n. 0r")] exI 1);
+Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. #0}";
+by (res_inst_tac [("x","%n. #0")] exI 1);
by (Step_tac 1);
by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
qed "lemma_hyprel_0r_mem";
@@ -1153,8 +1155,8 @@
qed "hypreal_mult_less_zero";
Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0hr < 1hr";
-by (res_inst_tac [("x","%n. 0r")] exI 1);
-by (res_inst_tac [("x","%n. 1r")] exI 1);
+by (res_inst_tac [("x","%n. #0")] exI 1);
+by (res_inst_tac [("x","%n. #1")] exI 1);
by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
FreeUltrafilterNat_Nat_set]));
qed "hypreal_zero_less_one";
@@ -1326,25 +1328,25 @@
simpset()));
qed "hypreal_hrinv_less_zero";
-Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real 1r = 1hr";
+Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real #1 = 1hr";
by (Step_tac 1);
qed "hypreal_of_real_one";
-Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real 0r = 0hr";
+Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real #0 = 0hr";
by (Step_tac 1);
qed "hypreal_of_real_zero";
-Goal "(hypreal_of_real r = 0hr) = (r = 0r)";
+Goal "(hypreal_of_real r = 0hr) = (r = #0)";
by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
simpset() addsimps [hypreal_of_real_def,
hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
qed "hypreal_of_real_zero_iff";
-Goal "(hypreal_of_real r ~= 0hr) = (r ~= 0r)";
+Goal "(hypreal_of_real r ~= 0hr) = (r ~= #0)";
by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
qed "hypreal_of_real_not_zero_iff";
-Goal "r ~= 0r ==> hrinv (hypreal_of_real r) = \
+Goal "r ~= #0 ==> hrinv (hypreal_of_real r) = \
\ hypreal_of_real (rinv r)";
by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
@@ -1665,6 +1667,7 @@
qed "hypreal_three_squares_add_zero_iff";
Addsimps [hypreal_three_squares_add_zero_iff];
+Addsimps [rename_numerals thy real_le_square];
Goal "(x::hypreal)*x <= x*x + y*y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
@@ -1679,7 +1682,7 @@
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps
[hypreal_mult,hypreal_add,hypreal_le,
- real_le_add_order]));
+ rename_numerals thy real_le_add_order]));
qed "hypreal_self_le_add_pos2";
Addsimps [hypreal_self_le_add_pos2];
@@ -1690,13 +1693,15 @@
by (full_simp_tac (simpset() addsimps
[pnat_one_iff RS sym,real_of_preal_def]) 1);
by (fold_tac [real_one_def]);
-by (rtac hypreal_of_real_one 1);
+by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
qed "hypreal_of_posnat_one";
Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
-by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
- hypreal_one_def,hypreal_add,hypreal_of_real_def,pnat_two_eq,
- real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ pnat_add_ac) 1);
+by (full_simp_tac (simpset() addsimps [real_of_preal_def,
+ rename_numerals thy (real_one_def RS meta_eq_to_obj_eq),
+ hypreal_add,hypreal_of_real_def,pnat_two_eq,hypreal_one_def,
+ real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @
+ pnat_add_ac) 1);
qed "hypreal_of_posnat_two";
Goalw [hypreal_of_posnat_def]
@@ -1788,9 +1793,10 @@
Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0hr";
by (auto_tac (claset(),simpset() addsimps
- [real_of_posnat_rinv_not_zero]));
+ [rename_numerals thy real_of_posnat_rinv_not_zero]));
qed "hypreal_epsilon_not_zero";
+Addsimps [rename_numerals thy real_of_posnat_not_eq_zero];
Goalw [omega_def,hypreal_zero_def] "whr ~= 0hr";
by (Simp_tac 1);
qed "hypreal_omega_not_zero";
--- a/src/HOL/Real/Hyperreal/HyperDef.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.thy Thu Jun 01 11:22:27 2000 +0200
@@ -5,7 +5,7 @@
Description : Construction of hyperreals using ultrafilters
*)
-HyperDef = Filter + RealBin +
+HyperDef = Filter + Real +
consts
@@ -37,8 +37,8 @@
defs
- hypreal_zero_def "0hr == Abs_hypreal(hyprel^^{%n::nat. 0r})"
- hypreal_one_def "1hr == Abs_hypreal(hyprel^^{%n::nat. 1r})"
+ hypreal_zero_def "0hr == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})"
+ hypreal_one_def "1hr == Abs_hypreal(hyprel^^{%n::nat. (#1::real)})"
(* an infinite number = [<1,2,3,...>] *)
omega_def "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})"
@@ -54,19 +54,19 @@
constdefs
- hypreal_of_real :: real => hypreal ("&# _" [80] 80)
+ hypreal_of_real :: real => hypreal
"hypreal_of_real r == Abs_hypreal(hyprel^^{%n::nat. r})"
hrinv :: hypreal => hypreal
"hrinv(P) == Abs_hypreal(UN X: Rep_hypreal(P).
- hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})"
+ hyprel^^{%n. if X n = #0 then #0 else rinv(X n)})"
(* n::nat --> (n+1)::hypreal *)
- hypreal_of_posnat :: nat => hypreal ("&&# _" [80] 80)
+ hypreal_of_posnat :: nat => hypreal
"hypreal_of_posnat n == (hypreal_of_real(real_of_preal
(preal_of_prat(prat_of_pnat(pnat_of_nat n)))))"
- hypreal_of_nat :: nat => hypreal ("&&## _" [80] 80)
+ hypreal_of_nat :: nat => hypreal
"hypreal_of_nat n == hypreal_of_posnat n + -1hr"
defs
--- a/src/HOL/Real/RComplete.ML Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RComplete.ML Thu Jun 01 11:22:27 2000 +0200
@@ -14,23 +14,25 @@
previously in Real.ML.
---------------------------------------------------------*)
(*a few lemmas*)
-Goal "! x:P. 0r < x ==> \
+Goal "! x:P. #0 < x ==> \
\ ((? x:P. y < x) = (? X. real_of_preal X : P & \
\ y < real_of_preal X))";
-by (blast_tac (claset() addSDs [bspec,
+by (blast_tac (claset() addSDs [bspec,rename_numerals thy
real_gt_zero_preal_Ex RS iffD1]) 1);
qed "real_sup_lemma1";
-Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
+Goal "[| ! x:P. #0 < x; ? x. x: P; ? y. !x: P. x < y |] \
\ ==> (? X. X: {w. real_of_preal w : P}) & \
\ (? Y. !X: {w. real_of_preal w : P}. X < Y)";
by (rtac conjI 1);
-by (blast_tac (claset() addDs [bspec, real_gt_zero_preal_Ex RS iffD1]) 1);
+by (blast_tac (claset() addDs [bspec, rename_numerals thy
+ real_gt_zero_preal_Ex RS iffD1]) 1);
by Auto_tac;
by (dtac bspec 1 THEN assume_tac 1);
by (ftac bspec 1 THEN assume_tac 1);
by (dtac real_less_trans 1 THEN assume_tac 1);
-by (dtac (real_gt_zero_preal_Ex RS iffD1) 1 THEN etac exE 1);
+by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1
+ THEN etac exE 1);
by (res_inst_tac [("x","ya")] exI 1);
by Auto_tac;
by (dres_inst_tac [("x","real_of_preal X")] bspec 1 THEN assume_tac 1);
@@ -41,18 +43,21 @@
Completeness of Positive Reals
-------------------------------------------------------------*)
-(* Supremum property for the set of positive reals *)
-(* FIXME: long proof - can be improved - need only have
- one case split *) (* will do for now *)
-Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
+(**
+ Supremum property for the set of positive reals
+ FIXME: long proof - should be improved - need
+ only have one case split
+**)
+
+Goal "[| ! x:P. (#0::real) < x; ? x. x: P; ? y. !x: P. x < y |] \
\ ==> (? S. !y. (? x: P. y < x) = (y < S))";
by (res_inst_tac
[("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1);
by Auto_tac;
by (ftac real_sup_lemma2 1 THEN Auto_tac);
-by (case_tac "0r < ya" 1);
-by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
-by (dtac real_less_all_real2 2);
+by (case_tac "#0 < ya" 1);
+by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
+by (dtac (full_rename_numerals thy real_less_all_real2) 2);
by Auto_tac;
by (rtac (preal_complete RS spec RS iffD1) 1);
by Auto_tac;
@@ -60,16 +65,15 @@
by Auto_tac;
(* second part *)
by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
-by (case_tac "0r < ya" 1);
-by (auto_tac (claset() addSDs [real_less_all_real2,
- real_gt_zero_preal_Ex RS iffD1],simpset()));
+by (case_tac "#0 < ya" 1);
+by (auto_tac (claset() addSDs (map (full_rename_numerals
+ thy) [real_less_all_real2,real_gt_zero_preal_Ex RS iffD1]),
+ simpset()));
by (ftac real_sup_lemma2 2 THEN Auto_tac);
by (ftac real_sup_lemma2 1 THEN Auto_tac);
by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
by (Blast_tac 3);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
+by (ALLGOALS(Blast_tac));
qed "posreal_complete";
(*--------------------------------------------------------
@@ -91,17 +95,19 @@
Completeness theorem for the positive reals(again)
----------------------------------------------------------------*)
-Goal "[| ALL x: S. 0r < x; \
+Goal "[| ALL x: S. #0 < x; \
\ EX x. x: S; \
\ EX u. isUb (UNIV::real set) S u \
\ |] ==> EX t. isLub (UNIV::real set) S t";
-by (res_inst_tac [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def]));
+by (res_inst_tac
+ [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1);
+by (auto_tac (claset(), simpset() addsimps
+ [isLub_def,leastP_def,isUb_def]));
by (auto_tac (claset() addSIs [setleI,setgeI]
- addSDs [real_gt_zero_preal_Ex RS iffD1],
- simpset()));
+ addSDs [(rename_numerals thy real_gt_zero_preal_Ex)
+ RS iffD1],simpset()));
by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
-by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
+by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff]));
by (rtac preal_psup_leI2a 1);
by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1);
@@ -111,7 +117,7 @@
by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1);
by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1);
by (ftac isUbD2 1);
-by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
+by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex],
simpset() addsimps [real_of_preal_le_iff]));
by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1]
@@ -122,63 +128,49 @@
(*-------------------------------
Lemmas
-------------------------------*)
-Goal "! y : {z. ? x: P. z = x + (-xa) + 1r} Int {x. 0r < x}. 0r < y";
+Goal "! y : {z. ? x: P. z = x + (-xa) + #1} Int {x. #0 < x}. #0 < y";
by Auto_tac;
qed "real_sup_lemma3";
Goal "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))";
-by (simp_tac (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
- real_add_ac) 1);
+by (Auto_tac);
qed "lemma_le_swap2";
-Goal "[| 0r < x + (-X) + 1r; x < xa |] ==> 0r < xa + (-X) + 1r";
-by (dtac real_add_less_mono 1);
-by (assume_tac 1);
-by (dres_inst_tac [("C","-x"),("A","0r + x")] real_add_less_mono2 1);
-by (asm_full_simp_tac
- (simpset() addsimps [real_add_zero_right, real_add_assoc RS sym,
- real_add_minus_left,real_add_zero_left]) 1);
+Goal "[| #0 < (x::real) + (-X) + #1; x < xa |] ==> #0 < xa + (-X) + #1";
+by (Auto_tac);
qed "lemma_real_complete1";
-Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa + (-X) + 1r <= S";
-by (dtac real_less_imp_le 1);
-by (dtac real_add_le_mono 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
+Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa + (-X) + #1 <= S";
+by (Auto_tac);
qed "lemma_real_complete2";
-Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa <= S + X + (-1r)"; (**)
-by (rtac (lemma_le_swap2 RS iffD2) 1);
-by (etac lemma_real_complete2 1);
-by (assume_tac 1);
+Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa <= S + X + (-#1)"; (**)
+by (Auto_tac);
qed "lemma_real_complete2a";
-Goal "[| x + (-X) + 1r <= S; xa <= x |] ==> xa <= S + X + (-1r)";
-by (rotate_tac 1 1);
-by (etac (real_le_imp_less_or_eq RS disjE) 1);
-by (blast_tac (claset() addIs [lemma_real_complete2a]) 1);
-by (blast_tac (claset() addIs [(lemma_le_swap2 RS iffD2)]) 1);
+Goal "[| (x::real) + (-X) + #1 <= S; xa <= x |] ==> xa <= S + X + (-#1)";
+by (Auto_tac);
qed "lemma_real_complete2b";
-(*------------------------------------
+(*----------------------------------------------------------
reals Completeness (again!)
- ------------------------------------*)
+ ----------------------------------------------------------*)
Goal "[| EX X. X: S; EX Y. isUb (UNIV::real set) S Y |] \
\ ==> EX t. isLub (UNIV :: real set) S t";
by (Step_tac 1);
-by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + 1r} \
-\ Int {x. 0r < x}" 1);
-by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + 1r} \
-\ Int {x. 0r < x}) (Y + (-X) + 1r)" 1);
+by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + #1} \
+\ Int {x. #0 < x}" 1);
+by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + #1} \
+\ Int {x. #0 < x}) (Y + (-X) + #1)" 1);
by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1);
by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac,
Step_tac]);
-by (res_inst_tac [("x","t + X + (-1r)")] exI 1);
+by (res_inst_tac [("x","t + X + (-#1)")] exI 1);
by (rtac isLubI2 1);
by (rtac setgeI 2 THEN Step_tac 2);
-by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + 1r} \
-\ Int {x. 0r < x}) (y + (-X) + 1r)" 2);
-by (dres_inst_tac [("y","(y + (- X) + 1r)")] isLub_le_isUb 2
+by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + #1} \
+\ Int {x. #0 < x}) (y + (-X) + #1)" 2);
+by (dres_inst_tac [("y","(y + (- X) + #1)")] isLub_le_isUb 2
THEN assume_tac 2);
by (full_simp_tac
(simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
@@ -202,21 +194,19 @@
addIs [real_add_le_mono1]) 1);
by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI]
addIs [real_add_le_mono1]) 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_add_assoc RS sym,
- real_zero_less_one]));
+by (Auto_tac);
qed "reals_complete";
(*----------------------------------------------------------------
Related: Archimedean property of reals
----------------------------------------------------------------*)
-Goal "0r < x ==> EX n. rinv(real_of_posnat n) < x";
+Goal "#0 < x ==> EX n. rinv(real_of_posnat n) < x";
by (stac real_of_posnat_rinv_Ex_iff 1);
by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
by (fold_tac [real_le_def]);
by (subgoal_tac "isUb (UNIV::real set) \
-\ {z. EX n. z = x*(real_of_posnat n)} 1r" 1);
+\ {z. EX n. z = x*(real_of_posnat n)} #1" 1);
by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1);
by (dtac reals_complete 1);
by (auto_tac (claset() addIs [isUbI,setleI],simpset()));
@@ -237,19 +227,22 @@
qed "reals_Archimedean";
Goal "EX n. (x::real) < real_of_posnat n";
-by (res_inst_tac [("R1.0","x"),("R2.0","0r")] real_linear_less2 1);
+by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1);
by (res_inst_tac [("x","0")] exI 1);
by (res_inst_tac [("x","0")] exI 2);
by (auto_tac (claset() addEs [real_less_trans],
simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
-by (forward_tac [(real_rinv_gt_zero RS reals_Archimedean)] 1);
+by (forward_tac [((full_rename_numerals thy real_rinv_gt_zero)
+ RS reals_Archimedean)] 1);
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
-by (forw_inst_tac [("y","rinv x")] real_mult_less_mono1 1);
+by (forw_inst_tac [("y","rinv x")]
+ (full_rename_numerals thy real_mult_less_mono1) 1);
by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
-by (dres_inst_tac [("n1","n"),("y","1r")]
+by (dres_inst_tac [("n1","n"),("y","#1")]
(real_of_posnat_less_zero RS real_mult_less_mono2) 1);
by (auto_tac (claset(),
- simpset() addsimps [real_of_posnat_less_zero,
+ simpset() addsimps [rename_numerals thy
+ real_of_posnat_less_zero,
real_not_refl2 RS not_sym,
real_mult_assoc RS sym]));
qed "reals_Archimedean2";
--- a/src/HOL/Real/ROOT.ML Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/ROOT.ML Thu Jun 01 11:22:27 2000 +0200
@@ -12,7 +12,3 @@
use "simproc.ML";
time_use_thy "Real";
time_use_thy "Hyperreal/HyperDef";
-
-(*FIXME: move to RealBin and eliminate all references to 0r, 1r in
- descendant theories*)
-Addsimps [zero_eq_numeral_0, one_eq_numeral_1];
--- a/src/HOL/Real/RealAbs.ML Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RealAbs.ML Thu Jun 01 11:22:27 2000 +0200
@@ -5,53 +5,76 @@
Description : Absolute value function for the reals
*)
+
+(** abs (absolute value) **)
+
+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
+ (simpset_of Int.thy addsimps
+ 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 "abs_nat_number_of";
+
+Addsimps [abs_nat_number_of];
+
+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 "abs_split";
+
+arith_tac_split_thms := !arith_tac_split_thms @ [abs_split];
+
(*----------------------------------------------------------------------------
Properties of the absolute value function over the reals
(adapted version of previously proved theorems about abs)
----------------------------------------------------------------------------*)
-Goalw [abs_real_def] "abs r = (if 0r<=r then r else -r)";
+
+Goalw [abs_real_def] "abs (r::real) = (if #0<=r then r else -r)";
by Auto_tac;
qed "abs_iff";
-Goalw [abs_real_def] "abs 0r = 0r";
-by (rtac (real_le_refl RS if_P) 1);
+Goalw [abs_real_def] "abs #0 = (#0::real)";
+by Auto_tac;
qed "abs_zero";
-
Addsimps [abs_zero];
-Goalw [abs_real_def] "abs 0r = -0r";
+Goalw [abs_real_def] "abs (#0::real) = -#0";
by (Simp_tac 1);
qed "abs_minus_zero";
-Goalw [abs_real_def] "0r<=x ==> abs x = x";
+Goalw [abs_real_def] "(#0::real)<=x ==> abs x = x";
by (Asm_simp_tac 1);
qed "abs_eqI1";
-Goalw [abs_real_def] "0r<x ==> abs x = x";
+Goalw [abs_real_def] "(#0::real)<x ==> abs x = x";
by (Asm_simp_tac 1);
qed "abs_eqI2";
-Goalw [abs_real_def,real_le_def] "x<0r ==> abs x = -x";
+Goalw [abs_real_def,real_le_def] "x<(#0::real) ==> abs x = -x";
by (Asm_simp_tac 1);
qed "abs_minus_eqI2";
-Goalw [abs_real_def] "x<=0r ==> abs x = -x";
-by (asm_full_simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
+Goalw [abs_real_def] "x<=(#0::real) ==> abs x = -x";
+by (Asm_simp_tac 1);
qed "abs_minus_eqI1";
-Goalw [abs_real_def] "0r<= abs x";
-by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
+Goalw [abs_real_def] "(#0::real)<= abs x";
+by (Simp_tac 1);
qed "abs_ge_zero";
Goalw [abs_real_def] "abs(abs x)=abs (x::real)";
-by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
+by (Simp_tac 1);
qed "abs_idempotent";
-Goalw [abs_real_def] "(x=0r) = (abs x = 0r)";
+Goalw [abs_real_def] "(x=(#0::real)) = (abs x = #0)";
by (Full_simp_tac 1);
qed "abs_zero_iff";
-Goal "(x ~= 0r) = (abs x ~= 0r)";
+Goal "(x ~= (#0::real)) = (abs x ~= #0)";
by (full_simp_tac (simpset() addsimps [abs_zero_iff RS sym]) 1);
qed "abs_not_zero_iff";
@@ -68,32 +91,32 @@
by (auto_tac (claset(),
simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute,
real_minus_mult_eq2]));
-by (blast_tac (claset() addDs [real_le_mult_order]) 1);
+by (blast_tac (claset() addDs [full_rename_numerals thy real_le_mult_order]) 1);
by (auto_tac (claset() addSDs [not_real_leE], simpset()));
-by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]);
-by (EVERY[dtac real_mult_le_zero 3, assume_tac 3, dtac real_le_anti_sym 3]);
-by (dtac real_mult_less_zero1 5 THEN assume_tac 5);
+by (EVERY1[dtac (full_rename_numerals thy real_mult_le_zero),
+ assume_tac, dtac real_le_anti_sym]);
+by (EVERY[dtac (full_rename_numerals thy real_mult_le_zero) 3,
+ assume_tac 3, dtac real_le_anti_sym 3]);
+by (dtac (full_rename_numerals thy 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 "abs_mult";
-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);
-by (blast_tac (claset() addDs [real_le_imp_less_or_eq, real_rinv_gt_zero]) 1);
-by (dtac (rinv_not_zero RS not_sym) 1);
-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);
+Goalw [abs_real_def] "x~= (#0::real) ==> abs(rinv(x)) = rinv(abs(x))";
+by (auto_tac (claset(), simpset() addsimps [real_le_less] @
+ (map (full_rename_numerals thy) [real_minus_rinv,
+ real_rinv_gt_zero])));
+by (etac (full_rename_numerals thy (real_rinv_less_zero
+ RSN (2,real_less_asym))) 1);
+by (arith_tac 1);
qed "abs_rinv";
-Goal "y ~= 0r ==> abs(x*rinv(y)) = abs(x)*rinv(abs(y))";
+Goal "y ~= #0 ==> 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 [abs_real_def] "abs(x+y) <= abs x + abs (y::real)";
-by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
+by (Simp_tac 1);
qed "abs_triangle_ineq";
(*Unused, but perhaps interesting as an example*)
@@ -102,52 +125,49 @@
qed "abs_triangle_ineq_four";
Goalw [abs_real_def] "abs(-x)=abs(x::real)";
-by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
+by (Simp_tac 1);
qed "abs_minus_cancel";
Goalw [abs_real_def] "abs(x + (-y)) = abs (y + (-(x::real)))";
-by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
+by (Simp_tac 1);
qed "abs_minus_add_cancel";
Goalw [abs_real_def] "abs(x + (-y)) <= abs x + abs (y::real)";
-by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
+by (Simp_tac 1);
qed "abs_triangle_minus_ineq";
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);
+by (Simp_tac 1);
qed_spec_mp "abs_add_less";
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);
+by (Simp_tac 1);
qed "abs_add_minus_less";
(* lemmas manipulating terms *)
-Goal "(0r*x<r)=(0r<r)";
+Goal "((#0::real)*x<r)=(#0<r)";
by (Simp_tac 1);
qed "real_mult_0_less";
-Goal "[| 0r<y; x<r; y*r<t*s |] ==> y*x<t*s";
-by (blast_tac (claset() addSIs [real_mult_less_mono2]
- addIs [real_less_trans]) 1);
+Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s";
+by (blast_tac (claset() addSIs [full_rename_numerals thy
+ real_mult_less_mono2] addIs [real_less_trans]) 1);
qed "real_mult_less_trans";
-Goal "[| 0r<=y; x<r; y*r<t*s; 0r<t*s|] ==> y*x<t*s";
+Goal "[| (#0::real)<=y; x<r; y*r<t*s; #0<t*s|] ==> y*x<t*s";
by (dtac real_le_imp_less_or_eq 1);
by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2,
real_mult_less_trans]) 1);
qed "real_mult_le_less_trans";
-(* proofs lifted from previous older version
- FIXME: use a stronger version of real_mult_less_mono *)
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 abs_ge_zero 1);
by (assume_tac 1);
-by (blast_tac (HOL_cs addIs [abs_ge_zero, real_mult_less_mono1,
- real_le_less_trans]) 1);
-by (blast_tac (HOL_cs addIs [abs_ge_zero, real_mult_order,
- real_le_less_trans]) 1);
+by (rtac (full_rename_numerals thy real_mult_order) 2);
+by (auto_tac (claset() addSIs [real_mult_less_mono1,
+ abs_ge_zero] addIs [real_le_less_trans],simpset()));
qed "abs_mult_less";
Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y)<r*(s::real)";
@@ -155,52 +175,112 @@
simpset() addsimps [abs_mult RS sym]));
qed "abs_mult_less2";
-Goal "1r < abs x ==> abs y <= abs(x*y)";
+Goal "(#1::real) < 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","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, abs_mult]) 1);
-by (dtac sym 1);
-by (asm_full_simp_tac (simpset() addsimps [abs_mult]) 1);
+by (dres_inst_tac [("W","#1")] real_less_sum_gt_zero 1);
+by (forw_inst_tac [("y","abs x + (-#1)")] (full_rename_numerals thy
+ real_mult_order) 1);
+by (rtac real_sum_gt_zero_less 2);
+by (asm_full_simp_tac (simpset()
+ addsimps [real_add_mult_distrib2,
+ real_mult_commute, abs_mult]) 2);
+by (dtac sym 2);
+by (auto_tac (claset(),simpset() addsimps [abs_mult]));
qed "abs_mult_le";
-Goal "[| 1r < abs x; r < abs y|] ==> r < abs(x*y)";
+Goal "[| (#1::real) < 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 "abs(x)<r ==> 0r<r";
+Goal "abs(x)<r ==> (#0::real)<r";
by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1);
qed "abs_less_gt_zero";
-Goalw [abs_real_def] "abs 1r = 1r";
-by (simp_tac (simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1]) 1);
+Goalw [abs_real_def] "abs #1 = (#1::real)";
+by (Simp_tac 1);
qed "abs_one";
+Goalw [abs_real_def] "abs (-#1) = (#1::real)";
+by (Simp_tac 1);
+qed "abs_minus_one";
+Addsimps [abs_minus_one];
+
Goalw [abs_real_def] "abs x =x | abs x = -(x::real)";
-by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
+by Auto_tac;
qed "abs_disj";
Goalw [abs_real_def] "(abs x < r) = (-r<x & x<(r::real))";
-by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
+by Auto_tac;
qed "abs_interval_iff";
Goalw [abs_real_def] "(abs x <= r) = (-r<=x & x<=(r::real))";
-by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
+by Auto_tac;
qed "abs_le_interval_iff";
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]));
+by Auto_tac;
qed "abs_add_minus_interval_iff";
-Goalw [abs_real_def] "0r < k ==> 0r < k + abs(x)";
-by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
+Goalw [abs_real_def] "(#0::real) < k ==> #0 < k + abs(x)";
+by Auto_tac;
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]));
+Goalw [abs_real_def] "(#0::real) < #1 + abs(x)";
+by Auto_tac;
qed "abs_add_one_gt_zero";
Addsimps [abs_add_one_gt_zero];
+
+(* 05/2000 *)
+Goalw [abs_real_def] "~ abs x < (#0::real)";
+by Auto_tac;
+qed "abs_not_less_zero";
+Addsimps [abs_not_less_zero];
+
+Goal "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)";
+by (auto_tac (claset() addIs [abs_triangle_ineq RS real_le_less_trans],
+ simpset()));
+qed "abs_circle";
+
+Goalw [abs_real_def] "(abs x <= (#0::real)) = (x = #0)";
+by Auto_tac;
+qed "abs_le_zero_iff";
+Addsimps [abs_le_zero_iff];
+
+Goal "abs (real_of_nat x) = real_of_nat x";
+by (auto_tac (claset() addIs [abs_eqI1],simpset()
+ addsimps [rename_numerals thy real_of_nat_ge_zero]));
+qed "abs_real_of_nat_cancel";
+Addsimps [abs_real_of_nat_cancel];
+
+Goal "~ abs(x) + (#1::real) < x";
+by (rtac real_leD 1);
+by (auto_tac (claset() addIs [abs_ge_self RS real_le_trans],simpset()));
+qed "abs_add_one_not_less_self";
+Addsimps [abs_add_one_not_less_self];
+
+(* used in vector theory *)
+Goal "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)";
+by (auto_tac (claset() addSIs [(abs_triangle_ineq
+ RS real_le_trans),real_add_left_le_mono1],
+ simpset() addsimps [real_add_assoc]));
+qed "abs_triangle_ineq_three";
+
+Goalw [abs_real_def] "abs(x - y) < y ==> (#0::real) < y";
+by (case_tac "#0 <= x - y" 1);
+by (Auto_tac);
+qed "abs_diff_less_imp_gt_zero";
+
+Goalw [abs_real_def] "abs(x - y) < x ==> (#0::real) < x";
+by (case_tac "#0 <= x - y" 1);
+by (Auto_tac);
+qed "abs_diff_less_imp_gt_zero2";
+
+Goal "abs(x - y) < y ==> (#0::real) < x";
+by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
+qed "abs_diff_less_imp_gt_zero3";
+
+Goal "abs(x - y) < -y ==> x < (#0::real)";
+by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
+qed "abs_diff_less_imp_gt_zero4";
+
--- a/src/HOL/Real/RealAbs.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RealAbs.thy Thu Jun 01 11:22:27 2000 +0200
@@ -7,4 +7,8 @@
RealAbs = RealBin +
+
+defs
+ abs_real_def "abs r == (if (#0::real) <= r then r else -r)"
+
end
--- a/src/HOL/Real/RealBin.ML Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RealBin.ML Thu Jun 01 11:22:27 2000 +0200
@@ -109,23 +109,6 @@
Addsimps [le_real_number_of_eq_not_less];
-
-(** abs (absolute value) **)
-
-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
- (simpset_of Int.thy addsimps
- 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 "abs_nat_number_of";
-
-Addsimps [abs_nat_number_of];
-
-
(*** New versions of existing theorems involving 0r, 1r ***)
Goal "- #1 = (#-1::real)";
@@ -209,11 +192,12 @@
in
Addsimprocs [fast_real_arith_simproc]
end;
+
-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 "abs_split";
+Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
-arith_tac_split_thms := !arith_tac_split_thms @ [abs_split];
+(* added by jdf *)
+fun full_rename_numerals thy th =
+ asm_full_simplify real_numeral_ss (change_theory thy th);
+
--- a/src/HOL/Real/RealOrd.ML Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RealOrd.ML Thu Jun 01 11:22:27 2000 +0200
@@ -1,7 +1,6 @@
(* Title: HOL/Real/Real.ML
ID: $Id$
- Author: Lawrence C. Paulson
- Jacques D. Fleuriot
+ Author: Jacques D. Fleuriot and Lawrence C. Paulson
Copyright: 1998 University of Cambridge
Description: Type "real" is a linear order
*)
@@ -434,6 +433,26 @@
Addsimps [real_mult_less_iff1,real_mult_less_iff2];
+(* 05/00 *)
+Goalw [real_le_def] "[| 0r<z; x*z<=y*z |] ==> x<=y";
+by (Auto_tac);
+qed "real_mult_le_cancel1";
+
+Goalw [real_le_def] "!!(x::real). [| 0r<z; z*x<=z*y |] ==> x<=y";
+by (Auto_tac);
+qed "real_mult_le_cancel2";
+
+Goalw [real_le_def] "0r < z ==> (x*z <= y*z) = (x <= y)";
+by (Auto_tac);
+qed "real_mult_le_cancel_iff1";
+
+Goalw [real_le_def] "0r < z ==> (z*x <= z*y) = (x <= y)";
+by (Auto_tac);
+qed "real_mult_le_cancel_iff2";
+
+Addsimps [real_mult_le_cancel_iff1,real_mult_le_cancel_iff2];
+
+
Goal "[| 0r<=z; x<y |] ==> x*z<=y*z";
by (EVERY1 [rtac real_less_or_eq_imp_le, dtac real_le_imp_less_or_eq]);
by (auto_tac (claset() addIs [real_mult_less_mono1],simpset()));
@@ -720,6 +739,34 @@
by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "real_rinv_add";
+(* 05/00 *)
+Goal "(0r <= -R) = (R <= 0r)";
+by (auto_tac (claset() addDs [sym],
+ simpset() addsimps [real_le_less]));
+qed "real_minus_zero_le_iff";
+
+Goal "(-R <= 0r) = (0r <= R)";
+by (auto_tac (claset(),simpset() addsimps
+ [real_minus_zero_less_iff2,real_le_less]));
+qed "real_minus_zero_le_iff2";
+
+Goal "-(x*x) <= 0r";
+by (simp_tac (simpset() addsimps [real_minus_zero_le_iff2]) 1);
+qed "real_minus_squre_le_zero";
+Addsimps [real_minus_squre_le_zero];
+
+Goal "x * x + y * y = 0r ==> x = 0r";
+by (dtac real_add_minus_eq_minus 1);
+by (cut_inst_tac [("x","x")] real_le_square 1);
+by (Auto_tac THEN dtac real_le_anti_sym 1);
+by (auto_tac (claset() addDs [real_mult_zero_disj],simpset()));
+qed "real_sum_squares_cancel";
+
+Goal "x * x + y * y = 0r ==> y = 0r";
+by (res_inst_tac [("y","x")] real_sum_squares_cancel 1);
+by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
+qed "real_sum_squares_cancel2";
+
(*----------------------------------------------------------------------------
Another embedding of the naturals in the reals (see real_of_posnat)
----------------------------------------------------------------------------*)
@@ -780,3 +827,27 @@
simpset() addsimps [Suc_diff_le, le_Suc_eq, real_of_nat_Suc,
real_of_nat_zero] @ real_add_ac));
qed_spec_mp "real_of_nat_minus";
+
+(* 05/00 *)
+Goal "n2 < n1 ==> real_of_nat (n1 - n2) = \
+\ real_of_nat n1 + -real_of_nat n2";
+by (auto_tac (claset() addIs [real_of_nat_minus],simpset()));
+qed "real_of_nat_minus2";
+
+Goalw [real_diff_def] "n2 < n1 ==> real_of_nat (n1 - n2) = \
+\ real_of_nat n1 - real_of_nat n2";
+by (etac real_of_nat_minus2 1);
+qed "real_of_nat_diff";
+
+Goalw [real_diff_def] "n2 <= n1 ==> real_of_nat (n1 - n2) = \
+\ real_of_nat n1 - real_of_nat n2";
+by (etac real_of_nat_minus 1);
+qed "real_of_nat_diff2";
+
+Goal "(real_of_nat n ~= 0r) = (n ~= 0)";
+by (auto_tac (claset() addIs [inj_real_of_nat RS injD],
+ simpset() addsimps [real_of_nat_zero RS sym]
+ delsimps [neq0_conv]));
+qed "real_of_nat_not_zero_iff";
+Addsimps [real_of_nat_not_zero_iff];
+
--- a/src/HOL/Real/RealOrd.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RealOrd.thy Thu Jun 01 11:22:27 2000 +0200
@@ -1,7 +1,6 @@
-(* Title: Real/RealOrd.thy
- ID: $Id$
- Author: Lawrence C. Paulson
- Jacques D. Fleuriot
+(* Title: Real/RealOrd.thy
+ ID: $Id$
+ Author: Jacques D. Fleuriot and Lawrence C. Paulson
Copyright: 1998 University of Cambridge
Description: Type "real" is a linear order
*)
@@ -11,7 +10,4 @@
instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
instance real :: linorder (real_le_linear)
-defs
- abs_real_def "abs r == (if 0r <= r then r else -r)"
-
end
--- a/src/HOL/Real/RealPow.ML Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RealPow.ML Thu Jun 01 11:22:27 2000 +0200
@@ -3,31 +3,30 @@
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : Natural Powers of reals theory
-
*)
-Goal "0r ^ (Suc n) = 0r";
+Goal "(#0::real) ^ (Suc n) = #0";
by (Auto_tac);
qed "realpow_zero";
Addsimps [realpow_zero];
-Goal "r ~= 0r --> r ^ n ~= 0r";
+Goal "r ~= (#0::real) --> r ^ n ~= #0";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_mult_not_zeroE],
simpset() addsimps [real_zero_not_eq_one RS not_sym]));
qed_spec_mp "realpow_not_zero";
-Goal "r ^ n = 0r ==> r = 0r";
-by (blast_tac (claset() addIs [ccontr]
- addDs [realpow_not_zero]) 1);
+Goal "r ^ n = (#0::real) ==> r = #0";
+by (rtac ccontr 1);
+by (auto_tac (claset() addDs [realpow_not_zero],simpset()));
qed "realpow_zero_zero";
-Goal "r ~= 0r --> rinv(r ^ n) = (rinv r) ^ n";
+Goal "r ~= #0 --> rinv(r ^ n) = (rinv r) ^ n";
by (induct_tac "n" 1);
by (Auto_tac);
by (forw_inst_tac [("n","n")] realpow_not_zero 1);
-by (auto_tac (claset() addDs [real_rinv_distrib],
- simpset()));
+by (auto_tac (claset() addDs [full_rename_numerals
+ thy real_rinv_distrib],simpset()));
qed_spec_mp "realpow_rinv";
Goal "abs (r::real) ^ n = abs (r ^ n)";
@@ -50,63 +49,58 @@
by (Simp_tac 1);
qed "realpow_two";
-Goal "0r < r --> 0r <= r ^ n";
+Goal "(#0::real) < r --> #0 <= r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addDs [real_less_imp_le]
- addIs [real_le_mult_order],simpset()));
+ addIs [rename_numerals thy real_le_mult_order],simpset()));
qed_spec_mp "realpow_ge_zero";
-Goal "0r < r --> 0r < r ^ n";
+Goal "(#0::real) < r --> #0 < r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [real_mult_order],
+by (auto_tac (claset() addIs [rename_numerals thy real_mult_order],
simpset() addsimps [real_zero_less_one]));
qed_spec_mp "realpow_gt_zero";
-Goal "0r <= r --> 0r <= r ^ n";
+Goal "(#0::real) <= r --> #0 <= r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [real_le_mult_order],
+by (auto_tac (claset() addIs [rename_numerals thy real_le_mult_order],
simpset()));
qed_spec_mp "realpow_ge_zero2";
-Goal "0r < x & x <= y --> x ^ n <= y ^ n";
+Goal "(#0::real) < x & x <= y --> x ^ n <= y ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addSIs [real_mult_le_mono],
simpset()));
by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
qed_spec_mp "realpow_le";
-Goal "0r <= x & x <= y --> x ^ n <= y ^ n";
+Goal "(#0::real) <= x & x <= y --> x ^ n <= y ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addSIs [real_mult_le_mono4],
simpset()));
by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1);
qed_spec_mp "realpow_le2";
-Goal "0r < x & x < y & 0 < n --> x ^ n < y ^ n";
+Goal "(#0::real) < x & x < y & 0 < n --> x ^ n < y ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [real_mult_less_mono,
- gr0I] addDs [realpow_gt_zero],simpset()));
+by (auto_tac (claset() addIs [full_rename_numerals thy
+ real_mult_less_mono, gr0I] addDs [realpow_gt_zero],
+ simpset()));
qed_spec_mp "realpow_less";
-Goal "1r ^ n = 1r";
+Goal "#1 ^ n = (#1::real)";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_eq_one";
Addsimps [realpow_eq_one];
-(** New versions using #0 and #1 instead of 0r and 1r
- REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
-
-Addsimps (map (rename_numerals thy) [realpow_zero, realpow_eq_one]);
-
-
-Goal "abs(-(1r ^ n)) = 1r";
+Goal "abs(-(#1 ^ n)) = (#1::real)";
by (simp_tac (simpset() addsimps
[abs_minus_cancel,abs_one]) 1);
qed "abs_minus_realpow_one";
Addsimps [abs_minus_realpow_one];
-Goal "abs((-1r) ^ n) = 1r";
+Goal "abs((-#1) ^ n) = (#1::real)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [abs_mult,
abs_minus_cancel,abs_one]));
@@ -118,13 +112,15 @@
by (auto_tac (claset(),simpset() addsimps real_mult_ac));
qed "realpow_mult";
-Goal "0r <= r ^ 2";
-by (simp_tac (simpset() addsimps [realpow_two]) 1);
+Goal "(#0::real) <= r ^ 2";
+by (simp_tac (simpset() addsimps [rename_numerals
+ thy real_le_square]) 1);
qed "realpow_two_le";
Addsimps [realpow_two_le];
Goal "abs((x::real) ^ 2) = x ^ 2";
-by (simp_tac (simpset() addsimps [abs_eqI1]) 1);
+by (simp_tac (simpset() addsimps [abs_eqI1,
+ rename_numerals thy real_le_square]) 1);
qed "abs_realpow_two";
Addsimps [abs_realpow_two];
@@ -134,222 +130,221 @@
qed "realpow_two_abs";
Addsimps [realpow_two_abs];
-Goal "1r < r ==> 1r < r ^ 2";
-by (auto_tac (claset(),simpset() addsimps [realpow_two]));
-by (cut_facts_tac [real_zero_less_one] 1);
-by (forw_inst_tac [("R1.0","0r")] real_less_trans 1);
+Goal "(#1::real) < r ==> #1 < r ^ 2";
+by Auto_tac;
+by (cut_facts_tac [rename_numerals thy real_zero_less_one] 1);
+by (forw_inst_tac [("R1.0","#0")] real_less_trans 1);
by (assume_tac 1);
-by (dres_inst_tac [("z","r"),("x","1r")] real_mult_less_mono1 1);
+by (dres_inst_tac [("z","r"),("x","#1")] (full_rename_numerals thy
+ real_mult_less_mono1) 1);
by (auto_tac (claset() addIs [real_less_trans],simpset()));
qed "realpow_two_gt_one";
-Goal "1r < r --> 1r <= r ^ n";
+Goal "(#1::real) < r --> #1 <= r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
simpset()));
-by (dtac (real_zero_less_one RS real_mult_less_mono) 1);
+by (dtac (full_rename_numerals thy (real_zero_less_one
+ RS real_mult_less_mono)) 1);
+by (dtac sym 4);
by (auto_tac (claset() addSIs [real_less_imp_le],
simpset() addsimps [real_zero_less_one]));
qed_spec_mp "realpow_ge_one";
-Goal "1r < r ==> 1r < r ^ (Suc n)";
+Goal "(#1::real) < r ==> #1 < r ^ (Suc n)";
by (forw_inst_tac [("n","n")] realpow_ge_one 1);
by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
by (dtac sym 2);
-by (forward_tac [real_zero_less_one RS real_less_trans] 1);
-by (dres_inst_tac [("y","r ^ n")] real_mult_less_mono2 1);
+by (forward_tac [full_rename_numerals thy
+ (real_zero_less_one RS real_less_trans)] 1);
+by (dres_inst_tac [("y","r ^ n")] (full_rename_numerals thy
+ real_mult_less_mono2) 1);
+by (assume_tac 1);
by (auto_tac (claset() addDs [real_less_trans],
simpset()));
qed "realpow_Suc_gt_one";
-Goal "1r <= r ==> 1r <= r ^ n";
+Goal "(#1::real) <= r ==> #1 <= r ^ n";
by (dtac real_le_imp_less_or_eq 1);
by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
qed "realpow_ge_one2";
-Goal "0r < r ==> 0r < r ^ Suc n";
+Goal "(#0::real) < r ==> #0 < r ^ Suc n";
by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
by (forw_inst_tac [("n1","n")]
((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
- addIs [real_mult_order],simpset()));
+ addIs [rename_numerals thy real_mult_order],simpset()));
qed "realpow_Suc_gt_zero";
-Goal "0r <= r ==> 0r <= r ^ Suc n";
+Goal "(#0::real) <= r ==> #0 <= r ^ Suc n";
by (etac (real_le_imp_less_or_eq RS disjE) 1);
by (etac (realpow_ge_zero) 1);
+by (dtac sym 1);
by (Asm_simp_tac 1);
qed "realpow_Suc_ge_zero";
Goal "(#1::real) <= #2 ^ n";
by (res_inst_tac [("j","#1 ^ n")] real_le_trans 1);
by (rtac realpow_le 2);
-by (auto_tac (claset() addIs [real_less_imp_le],
- simpset() addsimps [zero_eq_numeral_0]));
+by (auto_tac (claset() addIs [real_less_imp_le],simpset()));
qed "two_realpow_ge_one";
Goal "real_of_nat n < #2 ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(),
- simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1,
- real_mult_2,
+ simpset() addsimps [real_mult_2,
real_of_nat_Suc, real_of_nat_zero,
real_add_less_le_mono, two_realpow_ge_one]));
qed "two_realpow_gt";
Addsimps [two_realpow_gt,two_realpow_ge_one];
-Goal "(-1r) ^ (2*n) = 1r";
+Goal "(-#1) ^ (2*n) = (#1::real)";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_minus_one";
Addsimps [realpow_minus_one];
-Goal "(-1r) ^ (n + n) = 1r";
+Goal "(-#1) ^ (n + n) = (#1::real)";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_minus_one2";
Addsimps [realpow_minus_one2];
-Goal "(-1r) ^ Suc (n + n) = -1r";
+Goal "(-#1) ^ Suc (n + n) = -(#1::real)";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_minus_one_odd";
Addsimps [realpow_minus_one_odd];
-Goal "(-1r) ^ Suc (Suc (n + n)) = 1r";
+Goal "(-#1) ^ Suc (Suc (n + n)) = (#1::real)";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_minus_one_even";
Addsimps [realpow_minus_one_even];
-Goal "0r < r & r < 1r --> r ^ Suc n < r ^ n";
+Goal "(#0::real) < r & r < (#1::real) --> r ^ Suc n < r ^ n";
by (induct_tac "n" 1);
by (Auto_tac);
qed_spec_mp "realpow_Suc_less";
-Goal "0r <= r & r < 1r --> r ^ Suc n <= r ^ n";
+Goal "#0 <= r & r < (#1::real) --> r ^ Suc n <= r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_less_imp_le] addSDs
[real_le_imp_less_or_eq],simpset()));
qed_spec_mp "realpow_Suc_le";
-Goal "0r <= 0r ^ n";
+Goal "(#0::real) <= #0 ^ n";
by (case_tac "n" 1);
by (Auto_tac);
qed "realpow_zero_le";
Addsimps [realpow_zero_le];
-Goal "0r < r & r < 1r --> r ^ Suc n <= r ^ n";
+Goal "#0 < r & r < (#1::real) --> r ^ Suc n <= r ^ n";
by (blast_tac (claset() addSIs [real_less_imp_le,
realpow_Suc_less]) 1);
qed_spec_mp "realpow_Suc_le2";
-Goal "[| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n";
+Goal "[| #0 <= r; r < (#1::real) |] ==> r ^ Suc n <= r ^ n";
by (etac (real_le_imp_less_or_eq RS disjE) 1);
by (rtac realpow_Suc_le2 1);
by (Auto_tac);
qed "realpow_Suc_le3";
-Goal "0r <= r & r < 1r & n < N --> r ^ N <= r ^ n";
+Goal "#0 <= r & r < (#1::real) & n < N --> r ^ N <= r ^ n";
by (induct_tac "N" 1);
by (Auto_tac);
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
-by (ALLGOALS(dtac real_mult_le_mono3));
+by (ALLGOALS(dtac (full_rename_numerals thy real_mult_le_mono3)));
by (REPEAT(assume_tac 1));
by (REPEAT(assume_tac 3));
by (auto_tac (claset(),simpset() addsimps
[less_Suc_eq]));
qed_spec_mp "realpow_less_le";
-Goal "[| 0r <= r; r < 1r; n <= N |] ==> r ^ N <= r ^ n";
+Goal "[| #0 <= r; r < (#1::real); n <= N |] ==> r ^ N <= r ^ n";
by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [realpow_less_le],
simpset()));
qed "realpow_le_le";
-Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n <= r";
+Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n <= r";
by (dres_inst_tac [("n","1"),("N","Suc n")]
(real_less_imp_le RS realpow_le_le) 1);
by (Auto_tac);
qed "realpow_Suc_le_self";
-Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n < 1r";
+Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n < #1";
by (blast_tac (claset() addIs [realpow_Suc_le_self,
real_le_less_trans]) 1);
qed "realpow_Suc_less_one";
-Goal "1r <= r --> r ^ n <= r ^ Suc n";
+Goal "(#1::real) <= r --> r ^ n <= r ^ Suc n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addSIs [real_mult_le_le_mono1],simpset()));
-by (rtac ccontr 1 THEN dtac not_real_leE 1);
-by (dtac real_le_less_trans 1 THEN assume_tac 1);
-by (etac (real_zero_less_one RS real_less_asym) 1);
+by Auto_tac;
qed_spec_mp "realpow_le_Suc";
-Goal "1r < r --> r ^ n < r ^ Suc n";
+Goal "(#1::real) < r --> r ^ n < r ^ Suc n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addSIs [real_mult_less_mono2],simpset()));
-by (rtac ccontr 1 THEN dtac real_leI 1);
-by (dtac real_less_le_trans 1 THEN assume_tac 1);
-by (etac (real_zero_less_one RS real_less_asym) 1);
+by Auto_tac;
qed_spec_mp "realpow_less_Suc";
-Goal "1r < r --> r ^ n <= r ^ Suc n";
+Goal "(#1::real) < r --> r ^ n <= r ^ Suc n";
by (blast_tac (claset() addSIs [real_less_imp_le,
realpow_less_Suc]) 1);
qed_spec_mp "realpow_le_Suc2";
-Goal "1r < r & n < N --> r ^ n <= r ^ N";
+Goal "(#1::real) < r & n < N --> r ^ n <= r ^ N";
by (induct_tac "N" 1);
by (Auto_tac);
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
-by (ALLGOALS(dtac real_mult_self_le));
+by (ALLGOALS(dtac (full_rename_numerals thy real_mult_self_le)));
by (assume_tac 1);
by (assume_tac 2);
by (auto_tac (claset() addIs [real_le_trans],
simpset() addsimps [less_Suc_eq]));
qed_spec_mp "realpow_gt_ge";
-Goal "1r <= r & n < N --> r ^ n <= r ^ N";
+Goal "(#1::real) <= r & n < N --> r ^ n <= r ^ N";
by (induct_tac "N" 1);
by (Auto_tac);
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
-by (ALLGOALS(dtac real_mult_self_le2));
+by (ALLGOALS(dtac (full_rename_numerals thy real_mult_self_le2)));
by (assume_tac 1);
by (assume_tac 2);
by (auto_tac (claset() addIs [real_le_trans],
simpset() addsimps [less_Suc_eq]));
qed_spec_mp "realpow_gt_ge2";
-Goal "[| 1r < r; n <= N |] ==> r ^ n <= r ^ N";
+Goal "[| (#1::real) < r; n <= N |] ==> r ^ n <= r ^ N";
by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [realpow_gt_ge],simpset()));
qed "realpow_ge_ge";
-Goal "[| 1r <= r; n <= N |] ==> r ^ n <= r ^ N";
+Goal "[| (#1::real) <= r; n <= N |] ==> r ^ n <= r ^ N";
by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [realpow_gt_ge2],simpset()));
qed "realpow_ge_ge2";
-Goal "1r < r ==> r <= r ^ Suc n";
+Goal "(#1::real) < r ==> r <= r ^ Suc n";
by (dres_inst_tac [("n","1"),("N","Suc n")]
realpow_ge_ge 1);
by (Auto_tac);
qed_spec_mp "realpow_Suc_ge_self";
-Goal "1r <= r ==> r <= r ^ Suc n";
+Goal "(#1::real) <= r ==> r <= r ^ Suc n";
by (dres_inst_tac [("n","1"),("N","Suc n")]
realpow_ge_ge2 1);
by (Auto_tac);
qed_spec_mp "realpow_Suc_ge_self2";
-Goal "[| 1r < r; 0 < n |] ==> r <= r ^ n";
+Goal "[| (#1::real) < r; 0 < n |] ==> r <= r ^ n";
by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
by (auto_tac (claset() addSIs
[realpow_Suc_ge_self],simpset()));
qed "realpow_ge_self";
-Goal "[| 1r <= r; 0 < n |] ==> r <= r ^ n";
+Goal "[| (#1::real) <= r; 0 < n |] ==> r <= r ^ n";
by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
qed "realpow_ge_self2";
@@ -361,17 +356,107 @@
qed_spec_mp "realpow_minus_mult";
Addsimps [realpow_minus_mult];
-Goal "r ~= 0r ==> r * rinv(r) ^ 2 = rinv r";
+Goal "r ~= #0 ==> r * rinv(r) ^ 2 = rinv r";
by (asm_simp_tac (simpset() addsimps [realpow_two,
real_mult_assoc RS sym]) 1);
qed "realpow_two_mult_rinv";
Addsimps [realpow_two_mult_rinv];
+(* 05/00 *)
+Goal "(-x) ^ 2 = (x::real) ^ 2";
+by (Simp_tac 1);
+qed "realpow_two_minus";
+Addsimps [realpow_two_minus];
-(** New versions using #0 and #1 instead of 0r and 1r
- REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
+Goal "(x::real) ^ 2 + - (y ^ 2) = (x + -y) * (x + y)";
+by (simp_tac (simpset() addsimps [real_add_mult_distrib2,
+ real_add_mult_distrib, real_minus_mult_eq2 RS sym]
+ @ real_mult_ac) 1);
+qed "realpow_two_add_minus";
+
+goalw RealPow.thy [real_diff_def]
+ "(x::real) ^ 2 - y ^ 2 = (x - y) * (x + y)";
+by (simp_tac (simpset() addsimps [realpow_two_add_minus]
+ delsimps [realpow_Suc]) 1);
+qed "realpow_two_diff";
+
+goalw RealPow.thy [real_diff_def]
+ "((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)";
+by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
+by (dtac (rename_numerals thy ((real_eq_minus_iff RS iffD1)
+ RS sym)) 1);
+by (auto_tac (claset() addSDs [full_rename_numerals thy
+ real_mult_zero_disj] addDs [full_rename_numerals thy
+ real_add_minus_eq_minus], simpset() addsimps
+ [realpow_two_add_minus] delsimps [realpow_Suc]));
+qed "realpow_two_disj";
+
+(* used in Transc *)
+Goal "!!x. [|x ~= #0; m <= n |] ==> \
+\ x ^ (n - m) = x ^ n * rinv(x ^ m)";
+by (auto_tac (claset(),simpset() addsimps [le_eq_less_or_eq,
+ less_iff_Suc_add,realpow_add,
+ realpow_not_zero] @ real_mult_ac));
+qed "realpow_diff";
+
+Goal "real_of_nat (m) ^ n = real_of_nat (m ^ n)";
+by (induct_tac "n" 1);
+by (auto_tac (claset(),simpset() addsimps [real_of_nat_one,
+ real_of_nat_mult]));
+qed "realpow_real_of_nat";
-Addsimps (map (rename_numerals thy)
- [realpow_two_le, realpow_zero_le,
- abs_minus_realpow_one, abs_realpow_minus_one,
- realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);
+Goal "#0 < real_of_nat (2 ^ n)";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addSIs [full_rename_numerals thy real_mult_order],
+ simpset() addsimps [real_of_nat_mult RS sym,real_of_nat_one]));
+by (simp_tac (simpset() addsimps [rename_numerals thy
+ (real_of_nat_zero RS sym)]) 1);
+qed "realpow_real_of_nat_two_pos";
+Addsimps [realpow_real_of_nat_two_pos];
+
+(* FIXME: annoyingly long proof! *)
+Goal "(#0::real) <= x & #0 <= y & x ^ Suc n <= y ^ Suc n --> x <= y";
+by (induct_tac "n" 1);
+by (Auto_tac);
+by (dtac not_real_leE 1);
+by (auto_tac (claset() addDs [real_less_asym],
+ simpset() addsimps [real_le_less]));
+by (forw_inst_tac [("r","y")]
+ (full_rename_numerals thy real_rinv_less_swap) 1);
+by (rtac real_linear_less2 2);
+by (rtac real_linear_less2 5);
+by (dtac (full_rename_numerals thy
+ ((real_not_refl2 RS not_sym) RS real_mult_not_zero)) 9);
+by (Auto_tac);
+by (forw_inst_tac [("t","#0")] (real_not_refl2 RS not_sym) 1);
+by (forward_tac [full_rename_numerals thy real_rinv_gt_zero] 1);
+by (forw_inst_tac [("t","#0")] (real_not_refl2 RS not_sym) 3);
+by (dtac (full_rename_numerals thy real_rinv_gt_zero) 3);
+by (dtac (full_rename_numerals thy real_mult_less_zero) 3);
+by (forw_inst_tac [("x","(y * y ^ n)"),("r1.0","y")]
+ (full_rename_numerals thy real_mult_less_mono) 2);
+by (dres_inst_tac [("x","x * (x * x ^ n)"),("r1.0","rinv x")]
+ (full_rename_numerals thy real_mult_less_mono) 1);
+by (Auto_tac);
+by (auto_tac (claset() addIs (map (full_rename_numerals thy )
+ [real_mult_order,realpow_gt_zero]),
+ simpset() addsimps [real_mult_assoc
+ RS sym,real_not_refl2 RS not_sym]));
+qed_spec_mp "realpow_increasing";
+
+Goal "(#0::real) <= x & #0 <= y & x ^ Suc n = y ^ Suc n --> x = y";
+by (induct_tac "n" 1);
+by (Auto_tac);
+by (res_inst_tac [("R1.0","x"),("R2.0","y")]
+ real_linear_less2 1);
+by (auto_tac (claset() addDs [real_less_asym],
+ simpset() addsimps [real_le_less]));
+by (dres_inst_tac [("n","Suc(Suc n)")]
+ (conjI RSN(2,conjI RS realpow_less)) 1);
+by (dres_inst_tac [("n","Suc(Suc n)"),("x","y")]
+ (conjI RSN(2,conjI RS realpow_less)) 5);
+by (EVERY[dtac sym 4, dtac not_sym 4, rtac sym 4]);
+by (auto_tac (claset() addDs [real_not_refl2 RS not_sym,
+ full_rename_numerals thy real_mult_not_zero]
+ addIs [ccontr],simpset()));
+qed_spec_mp "realpow_Suc_cancel_eq";
--- a/src/HOL/Real/RealPow.thy Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RealPow.thy Thu Jun 01 11:22:27 2000 +0200
@@ -11,7 +11,7 @@
instance real :: {power}
primrec (realpow)
- realpow_0 "r ^ 0 = 1r"
+ realpow_0 "r ^ 0 = #1"
realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
end