# HG changeset patch # User fleuriot # Date 959851347 -7200 # Node ID 9dd0274f76afb155ed8ecd7f22f8a44a41911ef6 # Parent d1bd2144ab5db5e496272d4e07cc45084a28625c Updated files to remove 0r and 1r from theorems in descendant theories of RealBin. Some new theorems added. diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/HahnBanach/Aux.thy --- 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: diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/HahnBanach/FunctionNorm.thy --- 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)"; diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/HahnBanach/HahnBanach.thy --- 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; diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- 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!); diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/HahnBanach/Linearform.thy --- 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 diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/HahnBanach/NormedSpace.thy --- 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!); diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/HahnBanach/Subspace.thy --- 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$ diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/HahnBanach/VectorSpace.thy --- 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); diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/Hyperreal/HyperDef.ML --- 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"; diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/Hyperreal/HyperDef.thy --- 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 diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/RComplete.ML --- 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"; diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/ROOT.ML --- 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]; diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/RealAbs.ML --- 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 abs x = x"; +Goalw [abs_real_def] "(#0::real) 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 y*x y*x y*x y*x abs(x*y) abs(x)*abs(y) 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) 0r (#0::real) 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"; + diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/RealAbs.thy --- 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 diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/RealBin.ML --- 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); + diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/RealOrd.ML --- 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 x<=y"; +by (Auto_tac); +qed "real_mult_le_cancel1"; + +Goalw [real_le_def] "!!(x::real). [| 0r 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 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]; + diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/RealOrd.thy --- 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 diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/RealPow.ML --- 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"; diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/RealPow.thy --- 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