# HG changeset patch # User bauerg # Date 976102452 -3600 # Node ID e3229a37d53f2082871ab6b16561af829d1fc17d # Parent fe12dc60bc3cfb5fc2691fd1199f29d49c26d1c5 converted rinv to inverse; diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/HahnBanach/Aux.thy --- a/src/HOL/Real/HahnBanach/Aux.thy Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/HahnBanach/Aux.thy Wed Dec 06 12:34:12 2000 +0100 @@ -95,18 +95,18 @@ thus ?thesis by (simp only: real_mult_commute) qed -lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x" +lemma real_inverse_gt_zero1: "#0 < (x::real) ==> #0 < inverse x" proof - assume "#0 < x" have "0 < x" by simp - hence "0 < rinv x" by (rule real_rinv_gt_zero) + hence "0 < inverse x" by (rule real_inverse_gt_zero) thus ?thesis by simp qed -lemma real_mult_inv_right1: "x \ #0 ==> x * rinv(x) = #1" +lemma real_mult_inv_right1: "(x::real) \ #0 ==> x * inverse x = #1" by simp -lemma real_mult_inv_left1: "x \ #0 ==> rinv(x) * x = #1" +lemma real_mult_inv_left1: "(x::real) \ #0 ==> inverse x * x = #1" by simp lemma real_le_mult_order1a: diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/HahnBanach/FunctionNorm.thy --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Wed Dec 06 12:34:12 2000 +0100 @@ -66,7 +66,7 @@ constdefs B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set" "B V norm f == - {#0} \ {|f x| * rinv (norm x) | x. x \ 0 \ x \ V}" + {#0} \ {|f x| * inverse (norm x) | x. x \ 0 \ x \ V}" text{* $n$ is the function norm of $f$, iff $n$ is the supremum of $B$. @@ -146,12 +146,12 @@ fix x y assume "x \ V" "x \ 0" (*** - have ge: "#0 <= rinv (norm x)"; - by (rule real_less_imp_le, rule real_rinv_gt_zero, + have ge: "#0 <= inverse (norm x)"; + by (rule real_less_imp_le, rule real_inverse_gt_zero, rule normed_vs_norm_gt_zero); ( *** proof (rule real_less_imp_le); - show "#0 < rinv (norm x)"; - proof (rule real_rinv_gt_zero); + show "#0 < inverse (norm x)"; + proof (rule real_inverse_gt_zero); show "#0 < norm x"; ..; qed; qed; *** ) @@ -168,17 +168,17 @@ txt {* The thesis follows by a short calculation using the fact that $f$ is bounded. *} - assume "y = |f x| * rinv (norm x)" - also have "... <= c * norm x * rinv (norm x)" + assume "y = |f x| * inverse (norm x)" + also have "... <= c * norm x * inverse (norm x)" proof (rule real_mult_le_le_mono2) - show "#0 <= rinv (norm x)" - by (rule real_less_imp_le, rule real_rinv_gt_zero1, + show "#0 <= inverse (norm x)" + by (rule real_less_imp_le, rule real_inverse_gt_zero1, rule normed_vs_norm_gt_zero) from a show "|f x| <= c * norm x" .. qed - also have "... = c * (norm x * rinv (norm x))" + also have "... = c * (norm x * inverse (norm x))" by (rule real_mult_assoc) - also have "(norm x * rinv (norm x)) = (#1::real)" + also have "(norm x * inverse (norm x)) = (#1::real)" proof (rule real_mult_inv_right1) show nz: "norm x \ #0" by (rule not_sym, rule lt_imp_not_eq, @@ -211,14 +211,14 @@ elim UnE singletonE CollectE exE conjE) fix x r assume "x \ V" "x \ 0" - and r: "r = |f x| * rinv (norm x)" + and r: "r = |f x| * inverse (norm x)" have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero) - have "#0 <= rinv (norm x)" - by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(*** + have "#0 <= inverse (norm x)" + by (rule real_less_imp_le, rule real_inverse_gt_zero1, rule)(*** proof (rule real_less_imp_le); - show "#0 < rinv (norm x)"; - proof (rule real_rinv_gt_zero); + show "#0 < inverse (norm x)"; + proof (rule real_inverse_gt_zero); show "#0 < norm x"; ..; qed; qed; ***) @@ -282,12 +282,12 @@ txt {* For the case $x\neq \zero$ we derive the following fact from the definition of the function norm:*} - have l: "|f x| * rinv (norm x) <= \f\V,norm" + have l: "|f x| * inverse (norm x) <= \f\V,norm" proof (unfold function_norm_def, rule sup_ub) from ex_fnorm [OF _ c] show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" by (simp! add: is_function_norm_def function_norm_def) - show "|f x| * rinv (norm x) \ B V norm f" + show "|f x| * inverse (norm x) \ B V norm f" by (unfold B_def, intro UnI2 CollectI exI [of _ x] conjI, simp) qed @@ -295,9 +295,9 @@ txt {* The thesis now follows by a short calculation: *} have "|f x| = |f x| * #1" by (simp!) - also from nz have "#1 = rinv (norm x) * norm x" + also from nz have "#1 = inverse (norm x) * norm x" by (simp add: real_mult_inv_left1) - also have "|f x| * ... = |f x| * rinv (norm x) * norm x" + also have "|f x| * ... = |f x| * inverse (norm x) * norm x" by (simp! add: real_mult_assoc) also from n l have "... <= \f\V,norm * norm x" by (simp add: real_mult_le_le_mono2) @@ -365,13 +365,13 @@ by (simp! add: order_less_imp_not_eq) qed - from lz have "#0 < rinv (norm x)" - by (simp! add: real_rinv_gt_zero1) - hence rinv_gez: "#0 <= rinv (norm x)" + from lz have "#0 < inverse (norm x)" + by (simp! add: real_inverse_gt_zero1) + hence inverse_gez: "#0 <= inverse (norm x)" by (rule real_less_imp_le) - assume "y = |f x| * rinv (norm x)" - also from rinv_gez have "... <= c * norm x * rinv (norm x)" + assume "y = |f x| * inverse (norm x)" + also from inverse_gez have "... <= c * norm x * inverse (norm x)" proof (rule real_mult_le_le_mono2) show "|f x| <= c * norm x" by (rule bspec) qed diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Wed Dec 06 12:34:12 2000 +0100 @@ -284,22 +284,22 @@ next assume lz: "a < #0" hence nz: "a \ #0" by simp from a1 - have "- p (rinv a \ y + x0) - h (rinv a \ y) <= xi" + have "- p (inverse a \ y + x0) - h (inverse a \ y) <= xi" by (rule bspec) (simp!) txt {* The thesis for this case now follows by a short calculation. *} - hence "a * xi <= a * (- p (rinv a \ y + x0) - h (rinv a \ y))" + hence "a * xi <= a * (- p (inverse a \ y + x0) - h (inverse a \ y))" by (rule real_mult_less_le_anti [OF lz]) also - have "... = - a * (p (rinv a \ y + x0)) - a * (h (rinv a \ y))" + have "... = - a * (p (inverse a \ y + x0)) - a * (h (inverse a \ y))" by (rule real_mult_diff_distrib) also from lz vs y - have "- a * (p (rinv a \ y + x0)) = p (a \ (rinv a \ y + x0))" + have "- a * (p (inverse a \ y + x0)) = p (a \ (inverse a \ y + x0))" by (simp add: seminorm_abs_homogenous abs_minus_eqI2) also from nz vs y have "... = p (y + a \ x0)" by (simp add: vs_add_mult_distrib1) - also from nz vs y have "a * (h (rinv a \ y)) = h y" + also from nz vs y have "a * (h (inverse a \ y)) = h y" by (simp add: linearform_mult [symmetric]) finally have "a * xi <= p (y + a \ x0) - h y" . @@ -312,23 +312,23 @@ next assume gz: "#0 < a" hence nz: "a \ #0" by simp - from a2 have "xi <= p (rinv a \ y + x0) - h (rinv a \ y)" + from a2 have "xi <= p (inverse a \ y + x0) - h (inverse a \ y)" by (rule bspec) (simp!) txt {* The thesis for this case follows by a short calculation: *} with gz - have "a * xi <= a * (p (rinv a \ y + x0) - h (rinv a \ y))" + have "a * xi <= a * (p (inverse a \ y + x0) - h (inverse a \ y))" by (rule real_mult_less_le_mono) - also have "... = a * p (rinv a \ y + x0) - a * h (rinv a \ y)" + also have "... = a * p (inverse a \ y + x0) - a * h (inverse a \ y)" by (rule real_mult_diff_distrib2) also from gz vs y - have "a * p (rinv a \ y + x0) = p (a \ (rinv a \ y + x0))" + have "a * p (inverse a \ y + x0) = p (a \ (inverse a \ y + x0))" by (simp add: seminorm_abs_homogenous abs_eqI2) also from nz vs y have "... = p (y + a \ x0)" by (simp add: vs_add_mult_distrib1) - also from nz vs y have "a * h (rinv a \ y) = h y" + also from nz vs y have "a * h (inverse a \ y) = h y" by (simp add: linearform_mult [symmetric]) finally have "a * xi <= p (y + a \ x0) - h y" . diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/HahnBanach/Subspace.thy --- a/src/HOL/Real/HahnBanach/Subspace.thy Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/HahnBanach/Subspace.thy Wed Dec 06 12:34:12 2000 +0100 @@ -382,9 +382,9 @@ assume "a = (#0::real)" show ?thesis by (simp!) next assume "a \ (#0::real)" - from h have "rinv a \ a \ x' \ H" + from h have "inverse a \ a \ x' \ H" by (rule subspace_mult_closed) (simp!) - also have "rinv a \ a \ x' = x'" by (simp!) + also have "inverse a \ a \ x' = x'" by (simp!) finally have "x' \ H" . thus ?thesis by contradiction qed diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/HahnBanach/VectorSpace.thy --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Dec 06 12:34:12 2000 +0100 @@ -348,9 +348,9 @@ proof (rule classical) assume "is_vectorspace V" "x \ V" "a \ x = 0" "x \ 0" assume "a \ #0" - have "x = (rinv a * a) \ x" by (simp!) - also have "... = rinv a \ (a \ x)" by (rule vs_mult_assoc) - also have "... = rinv a \ 0" by (simp!) + have "x = (inverse a * a) \ x" by (simp!) + also have "... = inverse a \ (a \ x)" by (rule vs_mult_assoc) + also have "... = inverse a \ 0" by (simp!) also have "... = 0" by (simp!) finally have "x = 0" . thus "a = #0" by contradiction @@ -363,11 +363,11 @@ proof assume "is_vectorspace V" "x \ V" "y \ V" "a \ #0" have "x = #1 \ x" by (simp!) - also have "... = (rinv a * a) \ x" by (simp!) - also have "... = rinv a \ (a \ x)" + also have "... = (inverse a * a) \ x" by (simp!) + also have "... = inverse a \ (a \ x)" by (simp! only: vs_mult_assoc) also assume ?L - also have "rinv a \ ... = y" by (simp!) + also have "inverse a \ ... = y" by (simp!) finally show ?R . qed simp diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/RComplete.ML --- a/src/HOL/Real/RComplete.ML Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/RComplete.ML Wed Dec 06 12:34:12 2000 +0100 @@ -202,8 +202,8 @@ Related: Archimedean property of reals ----------------------------------------------------------------*) -Goal "#0 < x ==> EX n. rinv(real_of_posnat n) < x"; -by (stac real_of_posnat_rinv_Ex_iff 1); +Goal "#0 < x ==> EX n. inverse (real_of_posnat n) < x"; +by (stac real_of_posnat_inverse_Ex_iff 1); by (EVERY1[rtac ccontr, Asm_full_simp_tac]); by (fold_tac [real_le_def]); by (subgoal_tac "isUb (UNIV::real set) \ @@ -233,9 +233,9 @@ 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 (ftac ((rename_numerals real_rinv_gt_zero) RS reals_Archimedean) 1); +by (ftac ((rename_numerals real_inverse_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")] +by (forw_inst_tac [("y","inverse x")] (rename_numerals real_mult_less_mono1) 1); by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym])); by (dres_inst_tac [("n1","n"),("y","#1")] diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/RealAbs.ML --- a/src/HOL/Real/RealAbs.ML Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/RealAbs.ML Wed Dec 06 12:34:12 2000 +0100 @@ -90,17 +90,17 @@ simpset() addsimps [real_0_le_mult_iff])); qed "abs_mult"; -Goalw [abs_real_def] "x~= (#0::real) ==> abs(rinv(x)) = rinv(abs(x))"; +Goalw [abs_real_def] "x~= (#0::real) ==> abs(inverse(x)) = inverse(abs(x))"; by (auto_tac (claset(), simpset() addsimps [real_le_less] @ - (map rename_numerals [real_minus_rinv, real_rinv_gt_zero]))); -by (etac (rename_numerals (real_rinv_less_zero RSN (2,real_less_asym))) 1); + (map rename_numerals [real_minus_inverse, real_inverse_gt_zero]))); +by (etac (rename_numerals (real_inverse_less_zero RSN (2,real_less_asym))) 1); by (arith_tac 1); -qed "abs_rinv"; +qed "abs_inverse"; -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"; +Goal "y ~= #0 ==> abs (x * inverse y) = (abs x) * inverse (abs (y::real))"; +by (asm_simp_tac (simpset() addsimps [abs_mult, abs_inverse]) 1); +qed "abs_mult_inverse"; Goalw [abs_real_def] "abs(x+y) <= abs x + abs (y::real)"; by (Simp_tac 1); diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/RealBin.ML --- a/src/HOL/Real/RealBin.ML Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/RealBin.ML Wed Dec 06 12:34:12 2000 +0100 @@ -134,7 +134,7 @@ real_add_zero_left, real_add_zero_right, real_diff_0, real_diff_0_right, real_mult_0_right, real_mult_0, real_mult_1_right, real_mult_1, - real_mult_minus_1_right, real_mult_minus_1, real_rinv_1, + real_mult_minus_1_right, real_mult_minus_1, real_inverse_1, real_minus_zero_less_iff]); AddIffs (map rename_numerals [real_mult_is_0, real_0_is_mult]); diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/RealDef.ML --- a/src/HOL/Real/RealDef.ML Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/RealDef.ML Wed Dec 06 12:34:12 2000 +0100 @@ -493,27 +493,27 @@ real_mult_inv_right_ex]) 1); qed "real_mult_inv_left_ex"; -Goalw [rinv_def] "x ~= 0 ==> rinv(x)*x = 1r"; +Goalw [real_inverse_def] "x ~= 0 ==> inverse(x)*x = 1r"; by (ftac real_mult_inv_left_ex 1); by (Step_tac 1); by (rtac someI2 1); by Auto_tac; qed "real_mult_inv_left"; -Goal "x ~= 0 ==> x*rinv(x) = 1r"; +Goal "x ~= 0 ==> x*inverse(x) = 1r"; by (auto_tac (claset() addIs [real_mult_commute RS subst], simpset() addsimps [real_mult_inv_left])); qed "real_mult_inv_right"; Goal "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)"; by Auto_tac; -by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1); +by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); qed "real_mult_left_cancel"; Goal "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)"; by (Step_tac 1); -by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1); +by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); qed "real_mult_right_cancel"; @@ -526,53 +526,53 @@ by Auto_tac; qed "real_mult_right_cancel_ccontr"; -Goalw [rinv_def] "x ~= 0 ==> rinv(x) ~= 0"; +Goalw [real_inverse_def] "x ~= 0 ==> inverse(x::real) ~= 0"; by (ftac real_mult_inv_left_ex 1); by (etac exE 1); by (rtac someI2 1); by (auto_tac (claset(), simpset() addsimps [real_mult_0, real_zero_not_eq_one])); -qed "rinv_not_zero"; +qed "real_inverse_not_zero"; Addsimps [real_mult_inv_left,real_mult_inv_right]; Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)"; by (Step_tac 1); -by (dres_inst_tac [("f","%z. rinv x*z")] arg_cong 1); +by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1); by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1); qed "real_mult_not_zero"; bind_thm ("real_mult_not_zeroE",real_mult_not_zero RS notE); -Goal "x ~= 0 ==> rinv(rinv x) = x"; -by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1); -by (etac rinv_not_zero 1); -by (auto_tac (claset() addDs [rinv_not_zero],simpset())); -qed "real_rinv_rinv"; +Goal "x ~= 0 ==> inverse(inverse (x::real)) = x"; +by (res_inst_tac [("c1","inverse x")] (real_mult_right_cancel RS iffD1) 1); +by (etac real_inverse_not_zero 1); +by (auto_tac (claset() addDs [real_inverse_not_zero],simpset())); +qed "real_inverse_inverse"; -Goalw [rinv_def] "rinv(1r) = 1r"; +Goalw [real_inverse_def] "inverse(1r) = 1r"; by (cut_facts_tac [real_zero_not_eq_one RS not_sym RS real_mult_inv_left_ex] 1); by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one RS not_sym])); -qed "real_rinv_1"; -Addsimps [real_rinv_1]; +qed "real_inverse_1"; +Addsimps [real_inverse_1]; -Goal "x ~= 0 ==> rinv(-x) = -rinv(x)"; +Goal "x ~= 0 ==> inverse(-x) = -inverse(x::real)"; by (res_inst_tac [("c1","-x")] (real_mult_right_cancel RS iffD1) 1); by (stac real_mult_inv_left 2); by Auto_tac; -qed "real_minus_rinv"; +qed "real_minus_inverse"; -Goal "[| x ~= 0; y ~= 0 |] ==> rinv(x*y) = rinv(x)*rinv(y)"; +Goal "[| x ~= 0; y ~= 0 |] ==> inverse(x*y) = inverse(x)*inverse(y::real)"; by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1); by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1); by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym])); by (res_inst_tac [("c1","y")] (real_mult_left_cancel RS iffD1) 1); by (auto_tac (claset(),simpset() addsimps [real_mult_left_commute])); by (asm_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1); -qed "real_rinv_distrib"; +qed "real_inverse_distrib"; (*--------------------------------------------------------- Theorems for ordering diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/RealDef.thy Wed Dec 06 12:34:12 2000 +0100 @@ -15,7 +15,7 @@ instance - real :: {ord, zero, plus, times, minus} + real :: {ord, zero, plus, times, minus, inverse} consts @@ -24,17 +24,24 @@ defs real_zero_def - "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p), + "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p), preal_of_prat(prat_of_pnat 1p))})" real_one_def - "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + + "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})" real_minus_def - "- R == Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})" + "- R == Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})" + + real_diff_def + "R - (S::real) == R + - S" - real_diff_def "x - y == x + (- y :: real)" + real_inverse_def + "inverse (R::real) == (@S. R ~= 0 & S*R = 1r)" + real_divide_def + "R / (S::real) == R * inverse S" + constdefs real_of_preal :: preal => real @@ -42,9 +49,6 @@ Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p), preal_of_prat(prat_of_pnat 1p))})" - rinv :: real => real - "rinv(R) == (@S. R ~= 0 & S*R = 1r)" - real_of_posnat :: nat => real "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))" diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/RealOrd.ML --- a/src/HOL/Real/RealOrd.ML Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/RealOrd.ML Wed Dec 06 12:34:12 2000 +0100 @@ -53,7 +53,7 @@ val minus_add_distrib = real_minus_add_distrib val minus_minus = real_minus_minus val minus_0 = real_minus_zero - val add_inverses = [real_add_minus, real_add_minus_left]; + val add_inverses = [real_add_minus, real_add_minus_left] val cancel_simps = [real_add_minus_cancel, real_minus_add_cancel] end; @@ -388,45 +388,45 @@ qed "real_of_posnat_less_one"; Addsimps [real_of_posnat_less_one]; -Goal "rinv(real_of_posnat n) ~= 0"; +Goal "inverse (real_of_posnat n) ~= 0"; by (rtac ((real_of_posnat_gt_zero RS - real_not_refl2 RS not_sym) RS rinv_not_zero) 1); -qed "real_of_posnat_rinv_not_zero"; -Addsimps [real_of_posnat_rinv_not_zero]; + real_not_refl2 RS not_sym) RS real_inverse_not_zero) 1); +qed "real_of_posnat_inverse_not_zero"; +Addsimps [real_of_posnat_inverse_not_zero]; -Goal "rinv(real_of_posnat x) = rinv(real_of_posnat y) ==> x = y"; +Goal "inverse (real_of_posnat x) = inverse (real_of_posnat y) ==> x = y"; by (rtac (inj_real_of_posnat RS injD) 1); by (res_inst_tac [("n2","x")] - (real_of_posnat_rinv_not_zero RS real_mult_left_cancel RS iffD1) 1); + (real_of_posnat_inverse_not_zero RS real_mult_left_cancel RS iffD1) 1); by (full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS real_not_refl2 RS not_sym) RS real_mult_inv_left]) 1); by (asm_full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS real_not_refl2 RS not_sym)]) 1); -qed "real_of_posnat_rinv_inj"; +qed "real_of_posnat_inverse_inj"; -Goal "0 < x ==> 0 < rinv x"; +Goal "0 < x ==> 0 < inverse (x::real)"; by (EVERY1[rtac ccontr, dtac real_leI]); by (forward_tac [real_minus_zero_less_iff2 RS iffD2] 1); by (forward_tac [real_not_refl2 RS not_sym] 1); -by (dtac (real_not_refl2 RS not_sym RS rinv_not_zero) 1); +by (dtac (real_not_refl2 RS not_sym RS real_inverse_not_zero) 1); by (EVERY1[dtac real_le_imp_less_or_eq, Step_tac]); by (dtac real_mult_less_zero1 1 THEN assume_tac 1); by (auto_tac (claset() addIs [real_zero_less_one RS real_less_asym], simpset())); -qed "real_rinv_gt_zero"; +qed "real_inverse_gt_zero"; -Goal "x < 0 ==> rinv x < 0"; +Goal "x < 0 ==> inverse (x::real) < 0"; by (ftac real_not_refl2 1); by (dtac (real_minus_zero_less_iff RS iffD2) 1); by (rtac (real_minus_zero_less_iff RS iffD1) 1); -by (dtac (real_minus_rinv RS sym) 1); -by (auto_tac (claset() addIs [real_rinv_gt_zero], simpset())); -qed "real_rinv_less_zero"; +by (dtac (real_minus_inverse RS sym) 1); +by (auto_tac (claset() addIs [real_inverse_gt_zero], simpset())); +qed "real_inverse_less_zero"; -Goal "0 < rinv(real_of_posnat n)"; -by (rtac (real_of_posnat_gt_zero RS real_rinv_gt_zero) 1); -qed "real_of_posnat_rinv_gt_zero"; -Addsimps [real_of_posnat_rinv_gt_zero]; +Goal "0 < inverse (real_of_posnat n)"; +by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1); +qed "real_of_posnat_inverse_gt_zero"; +Addsimps [real_of_posnat_inverse_gt_zero]; Goal "real_of_preal (preal_of_prat (prat_of_pnat (pnat_of_nat N))) = \ \ real_of_nat (Suc N)"; @@ -459,7 +459,7 @@ Addsimps [real_two_not_zero]; -Goal "x*rinv(1r + 1r) + x*rinv(1r + 1r) = x"; +Goal "x * inverse (1r + 1r) + x * inverse(1r + 1r) = x"; by (stac real_add_self 1); by (full_simp_tac (simpset() addsimps [real_mult_assoc]) 1); qed "real_sum_of_halves"; @@ -473,12 +473,12 @@ real_mult_commute ]) 1); qed "real_mult_less_mono1"; -Goal "[| (0::real) < z; x < y |] ==> z*x < z*y"; +Goal "[| (0::real) < z; x < y |] ==> z * x < z * y"; by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_less_mono1]) 1); qed "real_mult_less_mono2"; -Goal "[| (0::real) < z; x*z < y*z |] ==> x < y"; -by (forw_inst_tac [("x","x*z")] (real_rinv_gt_zero +Goal "[| (0::real) < z; x * z < y * z |] ==> x < y"; +by (forw_inst_tac [("x","x*z")] (real_inverse_gt_zero RS real_mult_less_mono1) 1); by (auto_tac (claset(), simpset() addsimps @@ -614,18 +614,18 @@ simpset() addsimps [real_le_refl])); qed "real_mult_self_le2"; -Goal "x < y ==> x < (x + y)*rinv(1r + 1r)"; +Goal "x < y ==> x < (x + y) * inverse (1r + 1r)"; by (dres_inst_tac [("C","x")] real_add_less_mono2 1); by (dtac (real_add_self RS subst) 1); -by (dtac (real_zero_less_two RS real_rinv_gt_zero RS +by (dtac (real_zero_less_two RS real_inverse_gt_zero RS real_mult_less_mono1) 1); by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc]) 1); qed "real_less_half_sum"; -Goal "x < y ==> (x + y)*rinv(1r + 1r) < y"; +Goal "x < y ==> (x + y) * inverse (1r + 1r) < y"; by (dtac real_add_less_mono1 1); by (dtac (real_add_self RS subst) 1); -by (dtac (real_zero_less_two RS real_rinv_gt_zero RS +by (dtac (real_zero_less_two RS real_inverse_gt_zero RS real_mult_less_mono1) 1); by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc]) 1); qed "real_gt_half_sum"; @@ -634,36 +634,36 @@ by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1); qed "real_dense"; -Goal "(EX n. rinv(real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)"; +Goal "(EX n. inverse (real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)"; by (Step_tac 1); by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_mult_less_mono1) 1); by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS - real_rinv_gt_zero RS real_mult_less_mono1) 2); + real_inverse_gt_zero RS real_mult_less_mono1) 2); by (auto_tac (claset(), simpset() addsimps [(real_of_posnat_gt_zero RS real_not_refl2 RS not_sym), real_mult_assoc])); -qed "real_of_posnat_rinv_Ex_iff"; +qed "real_of_posnat_inverse_Ex_iff"; -Goal "(rinv(real_of_posnat n) < r) = (1r < r * real_of_posnat n)"; +Goal "(inverse(real_of_posnat n) < r) = (1r < r * real_of_posnat n)"; by (Step_tac 1); by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_mult_less_mono1) 1); by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS - real_rinv_gt_zero RS real_mult_less_mono1) 2); + real_inverse_gt_zero RS real_mult_less_mono1) 2); by (auto_tac (claset(), simpset() addsimps [real_mult_assoc])); -qed "real_of_posnat_rinv_iff"; +qed "real_of_posnat_inverse_iff"; -Goal "(rinv(real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)"; +Goal "(inverse (real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)"; by (Step_tac 1); by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS real_less_imp_le RS real_mult_le_le_mono1) 1); by (dres_inst_tac [("n3","n")] (real_of_posnat_gt_zero RS - real_rinv_gt_zero RS real_less_imp_le RS + real_inverse_gt_zero RS real_less_imp_le RS real_mult_le_le_mono1) 2); by (auto_tac (claset(), simpset() addsimps real_mult_ac)); -qed "real_of_posnat_rinv_le_iff"; +qed "real_of_posnat_inverse_le_iff"; Goalw [real_of_posnat_def] "(real_of_posnat n < real_of_posnat m) = (n < m)"; by Auto_tac; @@ -671,11 +671,11 @@ Addsimps [real_of_posnat_less_iff]; -Goal "0 < u ==> (u < rinv (real_of_posnat n)) = (real_of_posnat n < rinv(u))"; +Goal "0 < u ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse u)"; by (Step_tac 1); by (res_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS - real_rinv_gt_zero RS real_mult_less_cancel1) 1); -by (res_inst_tac [("x1","u")] ( real_rinv_gt_zero + real_inverse_gt_zero RS real_mult_less_cancel1) 1); +by (res_inst_tac [("x1","u")] ( real_inverse_gt_zero RS real_mult_less_cancel1) 2); by (auto_tac (claset(), simpset() addsimps [real_of_posnat_gt_zero, @@ -686,65 +686,65 @@ by (auto_tac (claset(), simpset() addsimps [real_of_posnat_gt_zero, real_not_refl2 RS not_sym,real_mult_assoc RS sym])); -qed "real_of_posnat_less_rinv_iff"; +qed "real_of_posnat_less_inverse_iff"; -Goal "0 < u ==> (u = rinv(real_of_posnat n)) = (real_of_posnat n = rinv u)"; +Goal "0 < u ==> (u = inverse (real_of_posnat n)) = (real_of_posnat n = inverse u)"; by (auto_tac (claset(), - simpset() addsimps [real_rinv_rinv, real_of_posnat_gt_zero, + simpset() addsimps [real_inverse_inverse, real_of_posnat_gt_zero, real_not_refl2 RS not_sym])); -qed "real_of_posnat_rinv_eq_iff"; +qed "real_of_posnat_inverse_eq_iff"; -Goal "[| 0 < r; r < x |] ==> rinv x < rinv r"; +Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"; by (ftac real_less_trans 1 THEN assume_tac 1); -by (ftac real_rinv_gt_zero 1); -by (forw_inst_tac [("x","x")] real_rinv_gt_zero 1); -by (forw_inst_tac [("x","r"),("z","rinv r")] real_mult_less_mono1 1); +by (ftac real_inverse_gt_zero 1); +by (forw_inst_tac [("x","x")] real_inverse_gt_zero 1); +by (forw_inst_tac [("x","r"),("z","inverse r")] real_mult_less_mono1 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS not_sym RS real_mult_inv_right]) 1); -by (ftac real_rinv_gt_zero 1); -by (forw_inst_tac [("x","1r"),("z","rinv x")] real_mult_less_mono2 1); +by (ftac real_inverse_gt_zero 1); +by (forw_inst_tac [("x","1r"),("z","inverse x")] real_mult_less_mono2 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1); -qed "real_rinv_less_swap"; +qed "real_inverse_less_swap"; -Goal "[| 0 < r; 0 < x|] ==> (r < x) = (rinv x < rinv r)"; -by (auto_tac (claset() addIs [real_rinv_less_swap],simpset())); -by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1); +Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::real))"; +by (auto_tac (claset() addIs [real_inverse_less_swap],simpset())); +by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1); by (etac (real_not_refl2 RS not_sym) 1); -by (res_inst_tac [("t","x")] (real_rinv_rinv RS subst) 1); +by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1); by (etac (real_not_refl2 RS not_sym) 1); -by (auto_tac (claset() addIs [real_rinv_less_swap], - simpset() addsimps [real_rinv_gt_zero])); -qed "real_rinv_less_iff"; +by (auto_tac (claset() addIs [real_inverse_less_swap], + simpset() addsimps [real_inverse_gt_zero])); +qed "real_inverse_less_iff"; -Goal "r < r + rinv(real_of_posnat n)"; +Goal "r < r + inverse (real_of_posnat n)"; by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1); by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); -qed "real_add_rinv_real_of_posnat_less"; -Addsimps [real_add_rinv_real_of_posnat_less]; +qed "real_add_inverse_real_of_posnat_less"; +Addsimps [real_add_inverse_real_of_posnat_less]; -Goal "r <= r + rinv(real_of_posnat n)"; +Goal "r <= r + inverse (real_of_posnat n)"; by (rtac real_less_imp_le 1); by (Simp_tac 1); -qed "real_add_rinv_real_of_posnat_le"; -Addsimps [real_add_rinv_real_of_posnat_le]; +qed "real_add_inverse_real_of_posnat_le"; +Addsimps [real_add_inverse_real_of_posnat_le]; -Goal "r + (-rinv(real_of_posnat n)) < r"; +Goal "r + (-inverse (real_of_posnat n)) < r"; by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1); by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym, real_minus_zero_less_iff2]) 1); -qed "real_add_minus_rinv_real_of_posnat_less"; -Addsimps [real_add_minus_rinv_real_of_posnat_less]; +qed "real_add_minus_inverse_real_of_posnat_less"; +Addsimps [real_add_minus_inverse_real_of_posnat_less]; -Goal "r + (-rinv(real_of_posnat n)) <= r"; +Goal "r + (-inverse (real_of_posnat n)) <= r"; by (rtac real_less_imp_le 1); by (Simp_tac 1); -qed "real_add_minus_rinv_real_of_posnat_le"; -Addsimps [real_add_minus_rinv_real_of_posnat_le]; +qed "real_add_minus_inverse_real_of_posnat_le"; +Addsimps [real_add_minus_inverse_real_of_posnat_le]; -Goal "0 < r ==> r*(1r + (-rinv(real_of_posnat n))) < r"; +Goal "0 < r ==> r*(1r + (-inverse (real_of_posnat n))) < r"; by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1); by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1); by (auto_tac (claset() addIs [real_mult_order], @@ -752,14 +752,14 @@ real_minus_zero_less_iff2])); qed "real_mult_less_self"; -Goal "0 <= 1r + (-rinv(real_of_posnat n))"; -by (res_inst_tac [("C","rinv(real_of_posnat n)")] real_le_add_right_cancel 1); +Goal "0 <= 1r + (-inverse (real_of_posnat n))"; +by (res_inst_tac [("C","inverse (real_of_posnat n)")] real_le_add_right_cancel 1); by (simp_tac (simpset() addsimps [real_add_assoc, - real_of_posnat_rinv_le_iff]) 1); -qed "real_add_one_minus_rinv_ge_zero"; + real_of_posnat_inverse_le_iff]) 1); +qed "real_add_one_minus_inverse_ge_zero"; -Goal "0 < r ==> 0 <= r*(1r + (-rinv(real_of_posnat n)))"; -by (dtac (real_add_one_minus_rinv_ge_zero RS real_mult_le_less_mono1) 1); +Goal "0 < r ==> 0 <= r*(1r + (-inverse (real_of_posnat n)))"; +by (dtac (real_add_one_minus_inverse_ge_zero RS real_mult_le_less_mono1) 1); by Auto_tac; qed "real_mult_add_one_minus_ge_zero"; @@ -788,22 +788,22 @@ qed "real_mult_eq_self_zero2"; Addsimps [real_mult_eq_self_zero2]; -Goal "[| 0 <= x*y; 0 < x |] ==> (0::real) <= y"; -by (ftac real_rinv_gt_zero 1); -by (dres_inst_tac [("x","rinv x")] real_less_le_mult_order 1); +Goal "[| 0 <= x * y; 0 < x |] ==> (0::real) <= y"; +by (ftac real_inverse_gt_zero 1); +by (dres_inst_tac [("x","inverse x")] real_less_le_mult_order 1); by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2); by (auto_tac (claset(), simpset() addsimps [real_mult_assoc RS sym])); qed "real_mult_ge_zero_cancel"; -Goal "[|x ~= 0; y ~= 0 |] ==> rinv(x) + rinv(y) = (x + y)*rinv(x*y)"; +Goal "[|x ~= 0; y ~= 0 |] ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))"; by (asm_full_simp_tac (simpset() addsimps - [real_rinv_distrib,real_add_mult_distrib, + [real_inverse_distrib,real_add_mult_distrib, real_mult_assoc RS sym]) 1); by (stac real_mult_assoc 1); by (rtac (real_mult_left_commute RS subst) 1); by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1); -qed "real_rinv_add"; +qed "real_inverse_add"; (* 05/00 *) Goal "(0 <= -R) = (R <= (0::real))"; diff -r fe12dc60bc3c -r e3229a37d53f src/HOL/Real/RealPow.ML --- a/src/HOL/Real/RealPow.ML Wed Dec 06 12:28:52 2000 +0100 +++ b/src/HOL/Real/RealPow.ML Wed Dec 06 12:34:12 2000 +0100 @@ -20,13 +20,13 @@ by (auto_tac (claset() addDs [realpow_not_zero], simpset())); qed "realpow_zero_zero"; -Goal "r ~= #0 --> rinv(r ^ n) = (rinv r) ^ n"; +Goal "(r::real) ~= #0 --> inverse (r ^ n) = (inverse 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 [rename_numerals real_rinv_distrib], +by (auto_tac (claset() addDs [rename_numerals real_inverse_distrib], simpset())); -qed_spec_mp "realpow_rinv"; +qed_spec_mp "realpow_inverse"; Goal "abs (r::real) ^ n = abs (r ^ n)"; by (induct_tac "n" 1); @@ -360,11 +360,11 @@ qed_spec_mp "realpow_minus_mult"; Addsimps [realpow_minus_mult]; -Goal "r ~= #0 ==> r * rinv(r) ^ 2 = rinv r"; +Goal "r ~= #0 ==> r * inverse r ^ 2 = inverse (r::real)"; by (asm_simp_tac (simpset() addsimps [realpow_two, real_mult_assoc RS sym]) 1); -qed "realpow_two_mult_rinv"; -Addsimps [realpow_two_mult_rinv]; +qed "realpow_two_mult_inverse"; +Addsimps [realpow_two_mult_inverse]; (* 05/00 *) Goal "(-x) ^ 2 = (x::real) ^ 2"; @@ -393,7 +393,7 @@ qed "realpow_two_disj"; (* used in Transc *) -Goal "[|x ~= #0; m <= n |] ==> x ^ (n - m) = x ^ n * rinv(x ^ m)"; +Goal "[|(x::real) ~= #0; m <= n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"; by (auto_tac (claset(), simpset() addsimps [le_eq_less_or_eq, less_iff_Suc_add,realpow_add, @@ -414,11 +414,11 @@ Addsimps [realpow_real_of_nat_two_pos]; -(*** REALORD.ML, AFTER real_rinv_less_iff ***) -Goal "[| 0 < r; 0 < x|] ==> (rinv x <= rinv r) = (r <= x)"; +(*** REALORD.ML, AFTER real_inverse_less_iff ***) +Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))"; by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, - real_rinv_less_iff]) 1); -qed "real_rinv_le_iff"; + real_inverse_less_iff]) 1); +qed "real_inverse_le_iff"; Goal "(#0::real) <= x --> #0 <= y --> x ^ Suc n <= y ^ Suc n --> x <= y"; by (induct_tac "n" 1); @@ -427,12 +427,12 @@ by (auto_tac (claset(), simpset() addsimps [inst "x" "#0" order_le_less, real_mult_le_0_iff])); -by (subgoal_tac "rinv x * (x * (x * x ^ n)) <= rinv y * (y * (y * y ^ n))" 1); +by (subgoal_tac "inverse x * (x * (x * x ^ n)) <= inverse y * (y * (y * y ^ n))" 1); by (rtac real_mult_le_mono 2); by (asm_full_simp_tac (simpset() addsimps [realpow_ge_zero, real_0_le_mult_iff]) 4); -by (asm_full_simp_tac (simpset() addsimps [real_rinv_le_iff]) 3); +by (asm_full_simp_tac (simpset() addsimps [real_inverse_le_iff]) 3); by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1); -by (rtac real_rinv_gt_zero 1); +by (rtac real_inverse_gt_zero 1); by Auto_tac; qed_spec_mp "realpow_increasing";