--- 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 \<noteq> #0 ==> x * rinv(x) = #1"
+lemma real_mult_inv_right1: "(x::real) \<noteq> #0 ==> x * inverse x = #1"
by simp
-lemma real_mult_inv_left1: "x \<noteq> #0 ==> rinv(x) * x = #1"
+lemma real_mult_inv_left1: "(x::real) \<noteq> #0 ==> inverse x * x = #1"
by simp
lemma real_le_mult_order1a:
--- 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} \<union> {|f x| * rinv (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
+ {#0} \<union> {|f x| * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> 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 \<in> V" "x \<noteq> 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 \<noteq> #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 \<in> V" "x \<noteq> 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) <= \<parallel>f\<parallel>V,norm"
+ have l: "|f x| * inverse (norm x) <= \<parallel>f\<parallel>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) \<in> B V norm f"
+ show "|f x| * inverse (norm x) \<in> 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 "... <= \<parallel>f\<parallel>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
--- 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 \<noteq> #0" by simp
from a1
- have "- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y) <= xi"
+ have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> 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 \<cdot> y + x0) - h (rinv a \<cdot> y))"
+ hence "a * xi <= a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
by (rule real_mult_less_le_anti [OF lz])
also
- have "... = - a * (p (rinv a \<cdot> y + x0)) - a * (h (rinv a \<cdot> y))"
+ have "... = - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
by (rule real_mult_diff_distrib)
also from lz vs y
- have "- a * (p (rinv a \<cdot> y + x0)) = p (a \<cdot> (rinv a \<cdot> y + x0))"
+ have "- a * (p (inverse a \<cdot> y + x0)) = p (a \<cdot> (inverse a \<cdot> y + x0))"
by (simp add: seminorm_abs_homogenous abs_minus_eqI2)
also from nz vs y have "... = p (y + a \<cdot> x0)"
by (simp add: vs_add_mult_distrib1)
- also from nz vs y have "a * (h (rinv a \<cdot> y)) = h y"
+ also from nz vs y have "a * (h (inverse a \<cdot> y)) = h y"
by (simp add: linearform_mult [symmetric])
finally have "a * xi <= p (y + a \<cdot> x0) - h y" .
@@ -312,23 +312,23 @@
next
assume gz: "#0 < a" hence nz: "a \<noteq> #0" by simp
- from a2 have "xi <= p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y)"
+ from a2 have "xi <= p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> 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 \<cdot> y + x0) - h (rinv a \<cdot> y))"
+ have "a * xi <= a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
by (rule real_mult_less_le_mono)
- also have "... = a * p (rinv a \<cdot> y + x0) - a * h (rinv a \<cdot> y)"
+ also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
by (rule real_mult_diff_distrib2)
also from gz vs y
- have "a * p (rinv a \<cdot> y + x0) = p (a \<cdot> (rinv a \<cdot> y + x0))"
+ have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
by (simp add: seminorm_abs_homogenous abs_eqI2)
also from nz vs y have "... = p (y + a \<cdot> x0)"
by (simp add: vs_add_mult_distrib1)
- also from nz vs y have "a * h (rinv a \<cdot> y) = h y"
+ also from nz vs y have "a * h (inverse a \<cdot> y) = h y"
by (simp add: linearform_mult [symmetric])
finally have "a * xi <= p (y + a \<cdot> x0) - h y" .
--- 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 \<noteq> (#0::real)"
- from h have "rinv a \<cdot> a \<cdot> x' \<in> H"
+ from h have "inverse a \<cdot> a \<cdot> x' \<in> H"
by (rule subspace_mult_closed) (simp!)
- also have "rinv a \<cdot> a \<cdot> x' = x'" by (simp!)
+ also have "inverse a \<cdot> a \<cdot> x' = x'" by (simp!)
finally have "x' \<in> H" .
thus ?thesis by contradiction
qed
--- 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 \<in> V" "a \<cdot> x = 0" "x \<noteq> 0"
assume "a \<noteq> #0"
- have "x = (rinv a * a) \<cdot> x" by (simp!)
- also have "... = rinv a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
- also have "... = rinv a \<cdot> 0" by (simp!)
+ have "x = (inverse a * a) \<cdot> x" by (simp!)
+ also have "... = inverse a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
+ also have "... = inverse a \<cdot> 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 \<in> V" "y \<in> V" "a \<noteq> #0"
have "x = #1 \<cdot> x" by (simp!)
- also have "... = (rinv a * a) \<cdot> x" by (simp!)
- also have "... = rinv a \<cdot> (a \<cdot> x)"
+ also have "... = (inverse a * a) \<cdot> x" by (simp!)
+ also have "... = inverse a \<cdot> (a \<cdot> x)"
by (simp! only: vs_mult_assoc)
also assume ?L
- also have "rinv a \<cdot> ... = y" by (simp!)
+ also have "inverse a \<cdot> ... = y" by (simp!)
finally show ?R .
qed simp
--- 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")]
--- 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);
--- 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]);
--- 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
--- 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)))"
--- 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))";
--- 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";