--- a/src/HOL/Real/Hyperreal/HRealAbs.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HRealAbs.ML Wed Dec 06 12:34:40 2000 +0100
@@ -94,36 +94,36 @@
hypreal_mult,abs_mult]));
qed "hrabs_mult";
-Goal "x~= (0::hypreal) ==> abs(hrinv(x)) = hrinv(abs(x))";
+Goal "x~= (0::hypreal) ==> abs(inverse(x)) = inverse(abs(x))";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs,
- hypreal_hrinv,hypreal_zero_def]));
-by (ultra_tac (claset(),simpset() addsimps [abs_rinv]) 1);
+ hypreal_inverse,hypreal_zero_def]));
+by (ultra_tac (claset(),simpset() addsimps [abs_inverse]) 1);
by (arith_tac 1);
-qed "hrabs_hrinv";
+qed "hrabs_inverse";
(* old version of proof:
Goalw [hrabs_def]
- "x~= (0::hypreal) ==> abs(hrinv(x)) = hrinv(abs(x))";
-by (auto_tac (claset(),simpset() addsimps [hypreal_minus_hrinv]));
+ "x~= (0::hypreal) ==> abs(inverse(x)) = inverse(abs(x))";
+by (auto_tac (claset(),simpset() addsimps [hypreal_minus_inverse]));
by (ALLGOALS(dtac not_hypreal_leE));
by (etac hypreal_less_asym 1);
by (blast_tac (claset() addDs [hypreal_le_imp_less_or_eq,
- hypreal_hrinv_gt_zero]) 1);
-by (dtac (hrinv_not_zero RS not_sym) 1);
-by (rtac (hypreal_hrinv_less_zero RSN (2,hypreal_less_asym)) 1);
+ hypreal_inverse_gt_zero]) 1);
+by (dtac (hreal_inverse_not_zero RS not_sym) 1);
+by (rtac (hypreal_inverse_less_zero RSN (2,hypreal_less_asym)) 1);
by (assume_tac 2);
by (blast_tac (claset() addSDs [hypreal_le_imp_less_or_eq]) 1);
-qed "hrabs_hrinv";
+qed "hrabs_inverse";
*)
val [prem] = goal thy "y ~= (0::hypreal) ==> \
-\ abs(x*hrinv(y)) = abs(x)*hrinv(abs(y))";
+\ abs(x*inverse(y)) = abs(x)*inverse(abs(y))";
by (res_inst_tac [("c1","abs y")] (hypreal_mult_left_cancel RS subst) 1);
by (simp_tac (simpset() addsimps [(hrabs_not_zero_iff RS sym), prem]) 1);
by (simp_tac (simpset() addsimps [(hrabs_mult RS sym), prem,
hrabs_not_zero_iff RS sym] @ hypreal_mult_ac) 1);
-qed "hrabs_mult_hrinv";
+qed "hrabs_mult_inverse";
Goal "abs(x+(y::hypreal)) <= abs x + abs y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Wed Dec 06 12:34:40 2000 +0100
@@ -317,39 +317,39 @@
qed "hypreal_minus_zero_iff";
Addsimps [hypreal_minus_zero_iff];
-(**** hrinv: multiplicative inverse on hypreal ****)
+(**** multiplicative inverse on hypreal ****)
Goalw [congruent_def]
- "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else rinv(X n)})";
+ "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else inverse(X n)})";
by (Auto_tac THEN Ultra_tac 1);
-qed "hypreal_hrinv_congruent";
+qed "hypreal_inverse_congruent";
-Goalw [hrinv_def]
- "hrinv (Abs_hypreal(hyprel^^{%n. X n})) = \
-\ Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else rinv(X n)})";
+Goalw [hypreal_inverse_def]
+ "inverse (Abs_hypreal(hyprel^^{%n. X n})) = \
+\ Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else inverse(X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
by (simp_tac (simpset() addsimps
[hyprel_in_hypreal RS Abs_hypreal_inverse,
- [equiv_hyprel, hypreal_hrinv_congruent] MRS UN_equiv_class]) 1);
-qed "hypreal_hrinv";
+ [equiv_hyprel, hypreal_inverse_congruent] MRS UN_equiv_class]) 1);
+qed "hypreal_inverse";
-Goal "z ~= 0 ==> hrinv (hrinv z) = z";
+Goal "z ~= 0 ==> inverse (inverse (z::hypreal)) = z";
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
by (rotate_tac 1 1);
by (asm_full_simp_tac (simpset() addsimps
- [hypreal_hrinv,hypreal_zero_def] addsplits [split_if]) 1);
-by (ultra_tac (claset() addDs (map rename_numerals [rinv_not_zero,real_rinv_rinv]),
+ [hypreal_inverse,hypreal_zero_def] addsplits [split_if]) 1);
+by (ultra_tac (claset() addDs (map rename_numerals [real_inverse_not_zero,real_inverse_inverse]),
simpset()) 1);
-qed "hypreal_hrinv_hrinv";
+qed "hypreal_inverse_inverse";
-Addsimps [hypreal_hrinv_hrinv];
+Addsimps [hypreal_inverse_inverse];
-Goalw [hypreal_one_def] "hrinv(1hr) = 1hr";
-by (full_simp_tac (simpset() addsimps [hypreal_hrinv,
+Goalw [hypreal_one_def] "inverse(1hr) = 1hr";
+by (full_simp_tac (simpset() addsimps [hypreal_inverse,
real_zero_not_eq_one RS not_sym]
addsplits [split_if]) 1);
-qed "hypreal_hrinv_1";
-Addsimps [hypreal_hrinv_1];
+qed "hypreal_inverse_1";
+Addsimps [hypreal_inverse_1];
(**** hyperreal addition: hypreal_add ****)
@@ -647,86 +647,86 @@
(*** existence of inverse ***)
Goalw [hypreal_one_def,hypreal_zero_def]
- "x ~= 0 ==> x*hrinv(x) = 1hr";
+ "x ~= 0 ==> x*inverse(x) = 1hr";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
+by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse,
hypreal_mult] addsplits [split_if]) 1);
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (blast_tac (claset() addSIs [real_mult_inv_right,
FreeUltrafilterNat_subset]) 1);
-qed "hypreal_mult_hrinv";
+qed "hypreal_mult_inverse";
-Goal "x ~= 0 ==> hrinv(x)*x = 1hr";
-by (asm_simp_tac (simpset() addsimps [hypreal_mult_hrinv,
+Goal "x ~= 0 ==> inverse(x)*x = 1hr";
+by (asm_simp_tac (simpset() addsimps [hypreal_mult_inverse,
hypreal_mult_commute]) 1);
-qed "hypreal_mult_hrinv_left";
+qed "hypreal_mult_inverse_left";
Goal "x ~= 0 ==> EX y. x * y = 1hr";
-by (fast_tac (claset() addDs [hypreal_mult_hrinv]) 1);
-qed "hypreal_hrinv_ex";
+by (fast_tac (claset() addDs [hypreal_mult_inverse]) 1);
+qed "hypreal_inverse_ex";
Goal "x ~= 0 ==> EX y. y * x = 1hr";
-by (fast_tac (claset() addDs [hypreal_mult_hrinv_left]) 1);
-qed "hypreal_hrinv_left_ex";
+by (fast_tac (claset() addDs [hypreal_mult_inverse_left]) 1);
+qed "hypreal_inverse_left_ex";
Goal "x ~= 0 ==> EX! y. x * y = 1hr";
-by (auto_tac (claset() addIs [hypreal_mult_hrinv],simpset()));
+by (auto_tac (claset() addIs [hypreal_mult_inverse],simpset()));
by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
-qed "hypreal_hrinv_ex1";
+qed "hypreal_inverse_ex1";
Goal "x ~= 0 ==> EX! y. y * x = 1hr";
-by (auto_tac (claset() addIs [hypreal_mult_hrinv_left],simpset()));
+by (auto_tac (claset() addIs [hypreal_mult_inverse_left],simpset()));
by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
-qed "hypreal_hrinv_left_ex1";
+qed "hypreal_inverse_left_ex1";
-Goal "[| y~= 0; x * y = 1hr |] ==> x = hrinv y";
-by (forw_inst_tac [("x","y")] hypreal_mult_hrinv_left 1);
-by (res_inst_tac [("x1","y")] (hypreal_hrinv_left_ex1 RS ex1E) 1);
+Goal "[| y~= 0; x * y = 1hr |] ==> x = inverse y";
+by (forw_inst_tac [("x","y")] hypreal_mult_inverse_left 1);
+by (res_inst_tac [("x1","y")] (hypreal_inverse_left_ex1 RS ex1E) 1);
by (assume_tac 1);
by (Blast_tac 1);
-qed "hypreal_mult_inv_hrinv";
+qed "hypreal_mult_inv_inverse";
-Goal "x ~= 0 ==> EX y. x = hrinv y";
-by (forw_inst_tac [("x","x")] hypreal_hrinv_left_ex 1);
+Goal "x ~= 0 ==> EX y. x = inverse (y::hypreal)";
+by (forw_inst_tac [("x","x")] hypreal_inverse_left_ex 1);
by (etac exE 1 THEN
- forw_inst_tac [("x","y")] hypreal_mult_inv_hrinv 1);
+ forw_inst_tac [("x","y")] hypreal_mult_inv_inverse 1);
by (res_inst_tac [("x","y")] exI 2);
by Auto_tac;
qed "hypreal_as_inverse_ex";
Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)";
by Auto_tac;
-by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac) 1);
+by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1);
qed "hypreal_mult_left_cancel";
Goal "(c::hypreal) ~= 0 ==> (a*c=b*c) = (a=b)";
by (Step_tac 1);
-by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac) 1);
+by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1);
qed "hypreal_mult_right_cancel";
-Goalw [hypreal_zero_def] "x ~= 0 ==> hrinv(x) ~= 0";
+Goalw [hypreal_zero_def] "x ~= 0 ==> inverse (x::hypreal) ~= 0";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
+by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse,
hypreal_mult] addsplits [split_if]) 1);
by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
by (ultra_tac (claset() addIs [ccontr]
- addDs [rename_numerals rinv_not_zero],
+ addDs [rename_numerals real_inverse_not_zero],
simpset()) 1);
-qed "hrinv_not_zero";
+qed "hypreal_inverse_not_zero";
-Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
+Addsimps [hypreal_mult_inverse,hypreal_mult_inverse_left];
Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::hypreal)";
by (Step_tac 1);
-by (dres_inst_tac [("f","%z. hrinv x*z")] arg_cong 1);
+by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
qed "hypreal_mult_not_0";
@@ -741,30 +741,30 @@
by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
qed "hypreal_mult_self_not_zero";
-Goal "[| x ~= 0; y ~= 0 |] ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
+Goal "[| x ~= 0; y ~= 0 |] ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)";
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
hypreal_mult_not_0]));
by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0]));
-qed "hrinv_mult_eq";
+qed "inverse_mult_eq";
-Goal "x ~= 0 ==> hrinv(-x) = -hrinv(x)";
+Goal "x ~= 0 ==> inverse(-x) = -inverse(x::hypreal)";
by (rtac (hypreal_mult_right_cancel RS iffD1) 1);
-by (stac hypreal_mult_hrinv_left 2);
+by (stac hypreal_mult_inverse_left 2);
by Auto_tac;
-qed "hypreal_minus_hrinv";
+qed "hypreal_minus_inverse";
Goal "[| x ~= 0; y ~= 0 |] \
-\ ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
+\ ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)";
by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym]));
by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute]));
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
-qed "hypreal_hrinv_distrib";
+qed "hypreal_inverse_distrib";
(*------------------------------------------------------------------
Theorems for ordering
@@ -848,9 +848,7 @@
(*---------------------------------------------------------------------------------
Hyperreals as a linearly ordered field
---------------------------------------------------------------------------------*)
-(*** sum order ***)
-
-(***
+(*** sum order
Goalw [hypreal_zero_def]
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -861,9 +859,9 @@
[hypreal_less_def,hypreal_add]));
by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
qed "hypreal_add_order";
+***)
-(*** mult order ***)
-
+(*** mult order
Goalw [hypreal_zero_def]
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -1160,35 +1158,35 @@
by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
qed "hypreal_of_real_not_zero_iff";
-Goal "r ~= #0 ==> hrinv (hypreal_of_real r) = \
-\ hypreal_of_real (rinv r)";
+Goal "r ~= #0 ==> inverse (hypreal_of_real r) = \
+\ hypreal_of_real (inverse 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);
by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one]));
-qed "hypreal_of_real_hrinv";
+qed "hypreal_of_real_inverse";
-Goal "hypreal_of_real r ~= 0 ==> hrinv (hypreal_of_real r) = \
-\ hypreal_of_real (rinv r)";
-by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_hrinv) 1);
-qed "hypreal_of_real_hrinv2";
+Goal "hypreal_of_real r ~= 0 ==> inverse (hypreal_of_real r) = \
+\ hypreal_of_real (inverse r)";
+by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_inverse) 1);
+qed "hypreal_of_real_inverse2";
Goal "x+x=x*(1hr+1hr)";
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
qed "hypreal_add_self";
-Goal "z ~= 0 ==> x*y = (x*hrinv(z))*(z*y)";
+Goal "(z::hypreal) ~= 0 ==> x*y = (x*inverse(z))*(z*y)";
by (asm_simp_tac (simpset() addsimps hypreal_mult_ac) 1);
qed "lemma_chain";
-Goal "[|x ~= 0; y ~= 0 |] ==> \
-\ hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
-by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
+Goal "[|(x::hypreal) ~= 0; y ~= 0 |] ==> \
+\ inverse(x) + inverse(y) = (x + y)*inverse(x*y)";
+by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_distrib,
hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
by (stac hypreal_mult_assoc 1);
by (rtac (hypreal_mult_left_commute RS subst) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "hypreal_hrinv_add";
+qed "hypreal_inverse_add";
Goal "x = -x ==> x = (0::hypreal)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
--- a/src/HOL/Real/Hyperreal/HyperDef.thy Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.thy Wed Dec 06 12:34:40 2000 +0100
@@ -25,7 +25,7 @@
typedef hypreal = "UNIV//hyprel" (Equiv.quotient_def)
instance
- hypreal :: {ord, zero, plus, times, minus}
+ hypreal :: {ord, zero, plus, times, minus, inverse}
consts
@@ -36,14 +36,19 @@
defs
- hypreal_zero_def "0 == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})"
- hypreal_one_def "1hr == Abs_hypreal(hyprel^^{%n::nat. (#1::real)})"
+ hypreal_zero_def
+ "0 == 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})"
+ omega_def
+ "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})"
(* an infinitesimal number = [<1,1/2,1/3,...>] *)
- epsilon_def "ehr == Abs_hypreal(hyprel^^{%n::nat. rinv(real_of_posnat n)})"
+ epsilon_def
+ "ehr == Abs_hypreal(hyprel^^{%n::nat. inverse (real_of_posnat n)})"
hypreal_minus_def
"- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})"
@@ -51,15 +56,18 @@
hypreal_diff_def
"x - y == x + -(y::hypreal)"
+ hypreal_inverse_def
+ "inverse P == Abs_hypreal(UN X: Rep_hypreal(P).
+ hyprel^^{%n. if X n = #0 then #0 else inverse (X n)})"
+
+ hypreal_divide_def
+ "P / Q::hypreal == P * inverse Q"
+
constdefs
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 = #0 then #0 else rinv(X n)})"
-
(* n::nat --> (n+1)::hypreal *)
hypreal_of_posnat :: nat => hypreal
"hypreal_of_posnat n == (hypreal_of_real(real_of_preal
--- a/src/HOL/Real/Hyperreal/HyperOrd.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperOrd.ML Wed Dec 06 12:34:40 2000 +0100
@@ -54,7 +54,7 @@
val minus_add_distrib = hypreal_minus_add_distrib
val minus_minus = hypreal_minus_minus
val minus_0 = hypreal_minus_zero
- val add_inverses = [hypreal_add_minus, hypreal_add_minus_left];
+ val add_inverses = [hypreal_add_minus, hypreal_add_minus_left]
val cancel_simps = [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]
end;
@@ -197,10 +197,10 @@
qed "hypreal_two_not_zero";
Addsimps [hypreal_two_not_zero];
-Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
+Goal "x*inverse(1hr + 1hr) + x*inverse(1hr + 1hr) = x";
by (stac hypreal_add_self 1);
by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc,
- hypreal_two_not_zero RS hypreal_mult_hrinv_left]) 1);
+ hypreal_two_not_zero RS hypreal_mult_inverse_left]) 1);
qed "hypreal_sum_of_halves";
Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y";
@@ -382,45 +382,45 @@
hypreal_mult_order_trans,hypreal_mult_order],simpset()));
qed "hypreal_mult_le_mono";
-Goal "0 < x ==> 0 < hrinv x";
+Goal "0 < x ==> 0 < inverse (x::hypreal)";
by (EVERY1[rtac ccontr, dtac hypreal_leI]);
by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
-by (dtac (hypreal_not_refl2 RS not_sym RS hrinv_not_zero) 1);
+by (dtac (hypreal_not_refl2 RS not_sym RS hypreal_inverse_not_zero) 1);
by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]);
by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
simpset() addsimps [hypreal_minus_zero_less_iff]));
-qed "hypreal_hrinv_gt_zero";
+qed "hypreal_inverse_gt_zero";
-Goal "x < 0 ==> hrinv x < 0";
+Goal "x < 0 ==> inverse (x::hypreal) < 0";
by (ftac hypreal_not_refl2 1);
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
-by (dtac (hypreal_minus_hrinv RS sym) 1);
-by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero],
+by (dtac (hypreal_minus_inverse RS sym) 1);
+by (auto_tac (claset() addIs [hypreal_inverse_gt_zero],
simpset()));
-qed "hypreal_hrinv_less_zero";
+qed "hypreal_inverse_less_zero";
(* check why this does not work without 2nd substitution anymore! *)
-Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)";
+Goal "x < y ==> x < (x + y)*inverse(1hr + 1hr)";
by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1);
by (dtac (hypreal_add_self RS subst) 1);
-by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS
+by (dtac (hypreal_zero_less_two RS hypreal_inverse_gt_zero RS
hypreal_mult_less_mono1) 1);
by (auto_tac (claset() addDs [hypreal_two_not_zero RS
- (hypreal_mult_hrinv RS subst)],simpset()
+ (hypreal_mult_inverse RS subst)],simpset()
addsimps [hypreal_mult_assoc]));
qed "hypreal_less_half_sum";
(* check why this does not work without 2nd substitution anymore! *)
-Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y";
+Goal "x < y ==> (x + y)*inverse(1hr + 1hr) < y";
by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1);
by (dtac (hypreal_add_self RS subst) 1);
-by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS
+by (dtac (hypreal_zero_less_two RS hypreal_inverse_gt_zero RS
hypreal_mult_less_mono1) 1);
by (auto_tac (claset() addDs [hypreal_two_not_zero RS
- (hypreal_mult_hrinv RS subst)],simpset()
+ (hypreal_mult_inverse RS subst)],simpset()
addsimps [hypreal_mult_assoc]));
qed "hypreal_gt_half_sum";
@@ -584,13 +584,13 @@
(* existence of infinitesimal number also not *)
(* corresponding to any real number *)
-Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
-\ (EX y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
+Goal "{n::nat. x = inverse(real_of_posnat n)} = {} | \
+\ (EX y. {n::nat. x = inverse(real_of_posnat n)} = {y})";
by (Step_tac 1 THEN Step_tac 1);
-by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
+by (auto_tac (claset() addIs [real_of_posnat_inverse_inj],simpset()));
qed "lemma_epsilon_empty_singleton_disj";
-Goal "finite {n::nat. x = rinv(real_of_posnat n)}";
+Goal "finite {n::nat. x = inverse(real_of_posnat n)}";
by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
by Auto_tac;
qed "lemma_finite_epsilon_set";
@@ -608,7 +608,7 @@
Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
by (auto_tac (claset(),
- simpset() addsimps [rename_numerals real_of_posnat_rinv_not_zero]));
+ simpset() addsimps [rename_numerals real_of_posnat_inverse_not_zero]));
qed "hypreal_epsilon_not_zero";
Addsimps [rename_numerals real_of_posnat_not_eq_zero];
@@ -616,10 +616,10 @@
by (Simp_tac 1);
qed "hypreal_omega_not_zero";
-Goal "ehr = hrinv(whr)";
+Goal "ehr = inverse(whr)";
by (asm_full_simp_tac (simpset() addsimps
- [hypreal_hrinv,omega_def,epsilon_def]) 1);
-qed "hypreal_epsilon_hrinv_omega";
+ [hypreal_inverse,omega_def,epsilon_def]) 1);
+qed "hypreal_epsilon_inverse_omega";
(*----------------------------------------------------------------
Another embedding of the naturals in the
@@ -687,45 +687,45 @@
by (simp_tac (simpset() addsimps [hypreal_of_posnat_Suc] @ hypreal_add_ac) 1);
qed "hypreal_of_nat_Suc";
-Goal "0 < r ==> 0 < r*hrinv(1hr+1hr)";
-by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero
+Goal "0 < r ==> 0 < r*inverse(1hr+1hr)";
+by (dtac (hypreal_zero_less_two RS hypreal_inverse_gt_zero
RS hypreal_mult_less_mono1) 1);
by Auto_tac;
qed "hypreal_half_gt_zero";
(* this proof is so much simpler than one for reals!! *)
-Goal "[| 0 < r; r < x |] ==> hrinv x < hrinv r";
+Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_hrinv,
+by (auto_tac (claset(),simpset() addsimps [hypreal_inverse,
hypreal_less,hypreal_zero_def]));
-by (ultra_tac (claset() addIs [real_rinv_less_swap],simpset()) 1);
-qed "hypreal_hrinv_less_swap";
+by (ultra_tac (claset() addIs [real_inverse_less_swap],simpset()) 1);
+qed "hypreal_inverse_less_swap";
-Goal "[| 0 < r; 0 < x|] ==> (r < x) = (hrinv x < hrinv r)";
-by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
-by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
+Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))";
+by (auto_tac (claset() addIs [hypreal_inverse_less_swap],simpset()));
+by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);
by (etac (hypreal_not_refl2 RS not_sym) 1);
-by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1);
+by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);
by (etac (hypreal_not_refl2 RS not_sym) 1);
-by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],
- simpset() addsimps [hypreal_hrinv_gt_zero]));
-qed "hypreal_hrinv_less_iff";
+by (auto_tac (claset() addIs [hypreal_inverse_less_swap],
+ simpset() addsimps [hypreal_inverse_gt_zero]));
+qed "hypreal_inverse_less_iff";
-Goal "[| 0 < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
+Goal "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)";
by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
- hypreal_hrinv_gt_zero]) 1);
-qed "hypreal_mult_hrinv_less_mono1";
+ hypreal_inverse_gt_zero]) 1);
+qed "hypreal_mult_inverse_less_mono1";
-Goal "[| 0 < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
+Goal "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y";
by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
- hypreal_hrinv_gt_zero]) 1);
-qed "hypreal_mult_hrinv_less_mono2";
+ hypreal_inverse_gt_zero]) 1);
+qed "hypreal_mult_inverse_less_mono2";
Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
-by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
+by (forw_inst_tac [("x","x*z")] hypreal_mult_inverse_less_mono1 1);
by (dtac (hypreal_not_refl2 RS not_sym) 2);
-by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
+by (auto_tac (claset() addSDs [hypreal_mult_inverse],
simpset() addsimps hypreal_mult_ac));
qed "hypreal_less_mult_right_cancel";
--- a/src/HOL/Real/Hyperreal/HyperPow.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperPow.ML Wed Dec 06 12:34:40 2000 +0100
@@ -16,13 +16,13 @@
simpset() addsimps [hypreal_zero_not_eq_one RS not_sym]));
qed_spec_mp "hrealpow_not_zero";
-Goal "r ~= (0::hypreal) --> hrinv(r ^ n) = (hrinv r) ^ n";
+Goal "r ~= (0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n";
by (induct_tac "n" 1);
by (Auto_tac);
by (forw_inst_tac [("n","n")] hrealpow_not_zero 1);
-by (auto_tac (claset() addDs [hrinv_mult_eq],
+by (auto_tac (claset() addDs [inverse_mult_eq],
simpset()));
-qed_spec_mp "hrealpow_hrinv";
+qed_spec_mp "hrealpow_inverse";
Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
by (induct_tac "n" 1);
@@ -298,15 +298,15 @@
qed_spec_mp "hyperpow_not_zero";
Goalw [hypreal_zero_def]
- "r ~= (0::hypreal) --> hrinv(r pow n) = (hrinv r) pow n";
+ "r ~= (0::hypreal) --> inverse(r pow n) = (inverse r) pow n";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
- simpset() addsimps [hypreal_hrinv,hyperpow]));
+ simpset() addsimps [hypreal_inverse,hyperpow]));
by (rtac FreeUltrafilterNat_subset 1);
by (auto_tac (claset() addDs [realpow_not_zero]
- addIs [realpow_rinv],simpset()));
-qed "hyperpow_hrinv";
+ addIs [realpow_inverse],simpset()));
+qed "hyperpow_inverse";
Goal "abs r pow n = abs (r pow n)";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
--- a/src/HOL/Real/Hyperreal/Lim.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML Wed Dec 06 12:34:40 2000 +0100
@@ -42,8 +42,8 @@
"[| f -- x --> l; g -- x --> m |] \
\ ==> (%x. f(x) + g(x)) -- x --> (l + m)";
by (Step_tac 1);
-by (REPEAT(dres_inst_tac [("x","r*rinv(#1 + #1)")] spec 1));
-by (dtac (rename_numerals (real_zero_less_two RS real_rinv_gt_zero
+by (REPEAT(dres_inst_tac [("x","r*inverse(#1 + #1)")] spec 1));
+by (dtac (rename_numerals (real_zero_less_two RS real_inverse_gt_zero
RSN (2,real_mult_less_mono2))) 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
@@ -208,16 +208,16 @@
Goal "ALL s. #0 < s --> (EX xa. #0 < abs (xa + - x) & \
\ abs (xa + - x) < s & r <= abs (f xa + -L)) \
\ ==> ALL n::nat. EX xa. #0 < abs (xa + - x) & \
-\ abs(xa + -x) < rinv(real_of_posnat n) & r <= abs(f xa + -L)";
+\ abs(xa + -x) < inverse(real_of_posnat n) & r <= abs(f xa + -L)";
by (Step_tac 1);
-by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_rinv_gt_zero) 1);
+by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
by Auto_tac;
val lemma_LIM = result();
Goal "ALL s. #0 < s --> (EX xa. #0 < abs (xa + - x) & \
\ abs (xa + - x) < s & r <= abs (f xa + -L)) \
\ ==> EX X. ALL n::nat. #0 < abs (X n + - x) & \
-\ abs(X n + -x) < rinv(real_of_posnat n) & r <= abs(f (X n) + -L)";
+\ abs(X n + -x) < inverse(real_of_posnat n) & r <= abs(f (X n) + -L)";
by (dtac lemma_LIM 1);
by (dtac choice 1);
by (Blast_tac 1);
@@ -225,16 +225,16 @@
Goal "{n. f (X n) + - L = Y n} Int \
\ {n. #0 < abs (X n + - x) & \
-\ abs (X n + - x) < rinv (real_of_posnat n) & \
+\ abs (X n + - x) < inverse (real_of_posnat n) & \
\ r <= abs (f (X n) + - L)} <= \
\ {n. r <= abs (Y n)}";
by (Auto_tac);
val lemma_Int = result ();
Goal "!!X. ALL n. #0 < abs (X n + - x) & \
-\ abs (X n + - x) < rinv (real_of_posnat n) & \
+\ abs (X n + - x) < inverse (real_of_posnat n) & \
\ r <= abs (f (X n) + - L) ==> \
-\ ALL n. abs (X n + - x) < rinv (real_of_posnat n)";
+\ ALL n. abs (X n + - x) < inverse (real_of_posnat n)";
by (Auto_tac );
val lemma_simp = result();
@@ -356,28 +356,28 @@
qed "LIM_add_minus2";
(*-----------------------------
- NSLIM_rinv
+ NSLIM_inverse
-----------------------------*)
Goalw [NSLIM_def]
"!!f. [| f -- a --NS> L; \
\ L ~= #0 \
-\ |] ==> (%x. rinv(f(x))) -- a --NS> (rinv L)";
+\ |] ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
by (Step_tac 1);
by (dtac spec 1 THEN auto_tac (claset(),simpset()
addsimps [hypreal_of_real_not_zero_iff RS sym,
- hypreal_of_real_hrinv RS sym]));
+ hypreal_of_real_inverse RS sym]));
by (forward_tac [inf_close_hypreal_of_real_not_zero] 1
THEN assume_tac 1);
-by (auto_tac (claset() addSEs [(starfun_hrinv2 RS subst),
- inf_close_hrinv,hypreal_of_real_HFinite_diff_Infinitesimal],
+by (auto_tac (claset() addSEs [(starfun_inverse2 RS subst),
+ inf_close_inverse,hypreal_of_real_HFinite_diff_Infinitesimal],
simpset()));
-qed "NSLIM_rinv";
+qed "NSLIM_inverse";
Goal "[| f -- a --> L; \
-\ L ~= #0 |] ==> (%x. rinv(f(x))) -- a --> (rinv L)";
+\ L ~= #0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
- NSLIM_rinv]) 1);
-qed "LIM_rinv";
+ NSLIM_inverse]) 1);
+qed "LIM_inverse";
(*------------------------------
NSLIM_zero
@@ -633,14 +633,14 @@
qed "isCont_minus";
Goalw [isCont_def]
- "[| isCont f x; f x ~= #0 |] ==> isCont (%x. rinv (f x)) x";
-by (blast_tac (claset() addIs [LIM_rinv]) 1);
-qed "isCont_rinv";
+ "[| isCont f x; f x ~= #0 |] ==> isCont (%x. inverse (f x)) x";
+by (blast_tac (claset() addIs [LIM_inverse]) 1);
+qed "isCont_inverse";
-Goal "[| isNSCont f x; f x ~= #0 |] ==> isNSCont (%x. rinv (f x)) x";
-by (auto_tac (claset() addIs [isCont_rinv],simpset() addsimps
+Goal "[| isNSCont f x; f x ~= #0 |] ==> isNSCont (%x. inverse (f x)) x";
+by (auto_tac (claset() addIs [isCont_inverse],simpset() addsimps
[isNSCont_isCont_iff]));
-qed "isNSCont_rinv";
+qed "isNSCont_inverse";
Goalw [real_diff_def]
"[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a";
@@ -752,10 +752,10 @@
\ (EX xa y. abs (xa + - y) < s & \
\ r <= abs (f xa + -f y)) ==> \
\ ALL n::nat. EX xa y. \
-\ abs(xa + -y) < rinv(real_of_posnat n) & \
+\ abs(xa + -y) < inverse(real_of_posnat n) & \
\ r <= abs(f xa + -f y)";
by (Step_tac 1);
-by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_rinv_gt_zero) 1);
+by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
by Auto_tac;
val lemma_LIMu = result();
@@ -763,7 +763,7 @@
\ (EX xa y. abs (xa + - y) < s & \
\ r <= abs (f xa + -f y)) ==> \
\ EX X Y. ALL n::nat. \
-\ abs(X n + -(Y n)) < rinv(real_of_posnat n) & \
+\ abs(X n + -(Y n)) < inverse(real_of_posnat n) & \
\ r <= abs(f (X n) + -f (Y n))";
by (dtac lemma_LIMu 1);
by (dtac choice 1);
@@ -772,14 +772,14 @@
by (Blast_tac 1);
val lemma_skolemize_LIM2u = result();
-Goal "ALL n. abs (X n + -Y n) < rinv (real_of_posnat n) & \
+Goal "ALL n. abs (X n + -Y n) < inverse (real_of_posnat n) & \
\ r <= abs (f (X n) + - f(Y n)) ==> \
-\ ALL n. abs (X n + - Y n) < rinv (real_of_posnat n)";
+\ ALL n. abs (X n + - Y n) < inverse (real_of_posnat n)";
by (Auto_tac );
val lemma_simpu = result();
Goal "{n. f (X n) + - f(Y n) = Ya n} Int \
-\ {n. abs (X n + - Y n) < rinv (real_of_posnat n) & \
+\ {n. abs (X n + - Y n) < inverse (real_of_posnat n) & \
\ r <= abs (f (X n) + - f(Y n))} <= \
\ {n. r <= abs (Ya n)}";
by (Auto_tac);
@@ -814,23 +814,23 @@
Derivatives
------------------------------------------------------------------*)
Goalw [deriv_def]
- "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --> D)";
+ "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --> D)";
by (Blast_tac 1);
qed "DERIV_iff";
Goalw [deriv_def]
- "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --NS> D)";
+ "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --NS> D)";
by (simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
qed "DERIV_NS_iff";
Goalw [deriv_def]
"DERIV f x :> D \
-\ ==> (%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --> D";
+\ ==> (%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --> D";
by (Blast_tac 1);
qed "DERIVD";
Goalw [deriv_def] "DERIV f x :> D ==> \
-\ (%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --NS> D";
+\ (%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --NS> D";
by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
qed "NS_DERIVD";
@@ -877,8 +877,8 @@
-------------------------------------------------------*)
Goalw [LIM_def]
- "((%h. (f(a + h) + - f(a))*rinv(h)) -- #0 --> D) = \
-\ ((%x. (f(x) + -f(a))*rinv(x + -a)) -- a --> D)";
+ "((%h. (f(a + h) + - f(a))*inverse(h)) -- #0 --> D) = \
+\ ((%x. (f(x) + -f(a))*inverse(x + -a)) -- a --> D)";
by (Step_tac 1);
by (ALLGOALS(dtac spec));
by (Step_tac 1);
@@ -892,7 +892,7 @@
qed "DERIV_LIM_iff";
Goalw [deriv_def] "(DERIV f x :> D) = \
-\ ((%z. (f(z) + -f(x))*rinv(z + -x)) -- x --> D)";
+\ ((%z. (f(z) + -f(x))*inverse(z + -x)) -- x --> D)";
by (simp_tac (simpset() addsimps [DERIV_LIM_iff]) 1);
qed "DERIV_iff2";
@@ -904,19 +904,19 @@
-------------------------------------------*)
(*--- first equivalence ---*)
Goalw [nsderiv_def,NSLIM_def]
- "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))*rinv(h)) -- #0 --NS> D)";
+ "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --NS> D)";
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero]));
by (dres_inst_tac [("x","xa")] bspec 1);
by (rtac ccontr 3);
by (dres_inst_tac [("x","h")] spec 3);
by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff,
- starfun_mult RS sym,starfun_rinv_hrinv,starfun_add RS sym,
+ starfun_mult RS sym,starfun_inverse_inverse,starfun_add RS sym,
hypreal_of_real_minus,starfun_lambda_cancel]));
qed "NSDERIV_NSLIM_iff";
(*--- second equivalence ---*)
Goal "(NSDERIV f x :> D) = \
-\ ((%z. (f(z) + -f(x))*rinv(z + -x)) -- x --NS> D)";
+\ ((%z. (f(z) + -f(x))*inverse(z + -x)) -- x --NS> D)";
by (full_simp_tac (simpset() addsimps
[NSDERIV_NSLIM_iff,DERIV_LIM_iff,LIM_NSLIM_iff RS sym]) 1);
qed "NSDERIV_NSLIM_iff2";
@@ -926,7 +926,7 @@
"(NSDERIV f x :> D) = \
\ (ALL xa. \
\ xa ~= hypreal_of_real x & xa @= hypreal_of_real x --> \
-\ (*f* (%z. (f z - f x) * rinv (z - x))) xa @= hypreal_of_real D)";
+\ (*f* (%z. (f z - f x) * inverse (z - x))) xa @= hypreal_of_real D)";
by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff2,
NSLIM_def]));
qed "NSDERIV_iff2";
@@ -946,8 +946,8 @@
inf_close_mult1 1);
by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
by (subgoal_tac "(*f* (%z. z - x)) xa ~= (0::hypreal)" 2);
-by (dtac (starfun_hrinv2 RS sym) 2);
-by (auto_tac (claset() addDs [hypreal_mult_hrinv_left],
+by (dtac (starfun_inverse2 RS sym) 2);
+by (auto_tac (claset() addDs [hypreal_mult_inverse_left],
simpset() addsimps [starfun_mult RS sym,
hypreal_mult_assoc,starfun_add RS sym,real_diff_def,
starfun_Id,hypreal_of_real_minus,hypreal_diff_def,
@@ -1072,12 +1072,12 @@
real_minus_mult_eq2 RS sym,real_mult_commute]) 1);
val lemma_nsderiv1 = result();
-Goal "[| (x + y) * hrinv z = hypreal_of_real D + yb; z ~= 0; \
+Goal "[| (x + y) * inverse z = hypreal_of_real D + yb; z ~= 0; \
\ z : Infinitesimal; yb : Infinitesimal |] \
\ ==> x + y @= 0";
by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel
RS iffD2) 1 THEN assume_tac 1);
-by (thin_tac "(x + y) * hrinv z = hypreal_of_real D + yb" 1);
+by (thin_tac "(x + y) * inverse z = hypreal_of_real D + yb" 1);
by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2,
HFinite_add],simpset() addsimps [hypreal_mult_assoc,
mem_infmal_iff RS sym]));
@@ -1090,7 +1090,7 @@
NSLIM_def]) 1 THEN REPEAT(Step_tac 1));
by (auto_tac (claset(),simpset() addsimps [starfun_mult RS sym,
starfun_add RS sym,starfun_lambda_cancel,
- starfun_rinv_hrinv,hypreal_of_real_zero,lemma_nsderiv1]));
+ starfun_inverse_inverse,hypreal_of_real_zero,lemma_nsderiv1]));
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1);
by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
@@ -1208,7 +1208,7 @@
by (forw_inst_tac [("b1","hypreal_of_real(D) + y")]
(hypreal_mult_right_cancel RS iffD2) 1);
by (thin_tac "((*f* f) (hypreal_of_real(x) + h) + \
-\ - hypreal_of_real (f x)) * hrinv h = hypreal_of_real(D) + y" 2);
+\ - hypreal_of_real (f x)) * inverse h = hypreal_of_real(D) + y" 2);
by (assume_tac 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
hypreal_add_mult_distrib]));
@@ -1274,11 +1274,11 @@
\ (*f* g) (hypreal_of_real(x) + xa) @= hypreal_of_real (g x) \
\ |] ==> ((*f* f) ((*f* g) (hypreal_of_real(x) + xa)) \
\ + - hypreal_of_real (f (g x)))* \
-\ hrinv ((*f* g) (hypreal_of_real(x) + xa) + \
+\ inverse ((*f* g) (hypreal_of_real(x) + xa) + \
\ - hypreal_of_real (g x)) @= hypreal_of_real(Da)";
by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff2,
NSLIM_def,starfun_mult RS sym,hypreal_of_real_minus,
- starfun_add RS sym,starfun_hrinv3]));
+ starfun_add RS sym,starfun_inverse3]));
qed "NSDERIVD1";
(*--------------------------------------------------------------
@@ -1290,9 +1290,9 @@
--------------------------------------------------------------*)
Goal "[| NSDERIV g x :> Db; xa: Infinitesimal; xa ~= 0 |] \
\ ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) * \
-\ hrinv xa @= hypreal_of_real(Db)";
+\ inverse xa @= hypreal_of_real(Db)";
by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff,
- NSLIM_def,starfun_mult RS sym,starfun_rinv_hrinv,
+ NSLIM_def,starfun_mult RS sym,starfun_inverse_inverse,
starfun_add RS sym,hypreal_of_real_zero,mem_infmal_iff,
starfun_lambda_cancel,hypreal_of_real_minus]));
qed "NSDERIVD2";
@@ -1307,14 +1307,14 @@
NSLIM_def,hypreal_of_real_zero,mem_infmal_iff RS sym]) 1 THEN Step_tac 1);
by (forw_inst_tac [("f","g")] NSDERIV_inf_close 1);
by (auto_tac (claset(),simpset() addsimps [starfun_add RS sym,
- hypreal_of_real_minus,starfun_rinv_hrinv,hypreal_of_real_mult,
+ hypreal_of_real_minus,starfun_inverse_inverse,hypreal_of_real_mult,
starfun_lambda_cancel2,starfun_o RS sym,starfun_mult RS sym]));
by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
by (dres_inst_tac [("g","g")] NSDERIV_zero 1);
by (auto_tac (claset(),simpset()
addsimps [hypreal_of_real_zero,inf_close_refl]));
by (res_inst_tac [("z1","(*f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"),
- ("y1","hrinv xa")] (lemma_chain RS ssubst) 1);
+ ("y1","inverse xa")] (lemma_chain RS ssubst) 1);
by (etac (hypreal_not_eq_minus_iff RS iffD1) 1);
by (rtac inf_close_mult_hypreal_of_real 1);
by (blast_tac (claset() addIs [NSDERIVD1,
@@ -1345,7 +1345,7 @@
Goal "NSDERIV (%x. x) x :> #1";
by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff,
NSLIM_def,starfun_mult RS sym,starfun_Id,hypreal_of_real_zero,
- starfun_rinv_hrinv,hypreal_of_real_one]
+ starfun_inverse_inverse,hypreal_of_real_one]
@ real_add_ac));
qed "NSDERIV_Id";
Addsimps [NSDERIV_Id];
@@ -1386,16 +1386,16 @@
Power of -1
---------------------------------------------------------------*)
Goalw [nsderiv_def]
- "x ~= #0 ==> NSDERIV (%x. rinv(x)) x :> (- (rinv x ^ 2))";
+ "x ~= #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
by (forward_tac [Infinitesimal_add_not_zero] 1);
-by (auto_tac (claset(),simpset() addsimps [starfun_rinv_hrinv,
- hypreal_of_real_hrinv RS sym,hypreal_of_real_minus,realpow_two,
+by (auto_tac (claset(),simpset() addsimps [starfun_inverse_inverse,
+ hypreal_of_real_inverse RS sym,hypreal_of_real_minus,realpow_two,
hypreal_of_real_mult] delsimps [hypreal_minus_mult_eq1 RS
sym,hypreal_minus_mult_eq2 RS sym]));
by (dtac (hypreal_of_real_not_zero_iff RS iffD2) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_add,
- hrinv_mult_eq RS sym, hypreal_minus_hrinv RS sym]
+by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_add,
+ inverse_mult_eq RS sym, hypreal_minus_inverse RS sym]
@ hypreal_add_ac @ hypreal_mult_ac delsimps [hypreal_minus_mult_eq1 RS
sym,hypreal_minus_mult_eq2 RS sym] ) 1);
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym,
@@ -1405,56 +1405,56 @@
(2,Infinitesimal_HFinite_mult2)) RS
(Infinitesimal_minus_iff RS iffD1)) 1);
by (forw_inst_tac [("x","hypreal_of_real x"),("y","hypreal_of_real x")] hypreal_mult_not_0 1);
-by (res_inst_tac [("y"," hrinv(- hypreal_of_real x * hypreal_of_real x)")] inf_close_trans 2);
-by (rtac hrinv_add_Infinitesimal_inf_close2 2);
+by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] inf_close_trans 2);
+by (rtac inverse_add_Infinitesimal_inf_close2 2);
by (auto_tac (claset() addIs [HFinite_minus_iff RS iffD1]
addSDs [Infinitesimal_minus_iff RS iffD2,
hypreal_of_real_HFinite_diff_Infinitesimal], simpset() addsimps
- [hypreal_minus_hrinv RS sym,hypreal_of_real_mult RS sym]));
-qed "NSDERIV_rinv";
+ [hypreal_minus_inverse RS sym,hypreal_of_real_mult RS sym]));
+qed "NSDERIV_inverse";
-Goal "x ~= #0 ==> DERIV (%x. rinv(x)) x :> (-(rinv x ^ 2))";
-by (asm_simp_tac (simpset() addsimps [NSDERIV_rinv,
+Goal "x ~= #0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
+by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse,
NSDERIV_DERIV_iff RS sym] delsimps [thm "realpow_Suc"]) 1);
-qed "DERIV_rinv";
+qed "DERIV_inverse";
(*--------------------------------------------------------------
Derivative of inverse
-------------------------------------------------------------*)
Goal "[| DERIV f x :> d; f(x) ~= #0 |] \
-\ ==> DERIV (%x. rinv(f x)) x :> (- (d * rinv(f(x) ^ 2)))";
+\ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
by (rtac (real_mult_commute RS subst) 1);
by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1,
- realpow_rinv] delsimps [thm "realpow_Suc",
+ realpow_inverse] delsimps [thm "realpow_Suc",
real_minus_mult_eq1 RS sym]) 1);
by (fold_goals_tac [o_def]);
-by (blast_tac (claset() addSIs [DERIV_chain,DERIV_rinv]) 1);
-qed "DERIV_rinv_fun";
+by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1);
+qed "DERIV_inverse_fun";
Goal "[| NSDERIV f x :> d; f(x) ~= #0 |] \
-\ ==> NSDERIV (%x. rinv(f x)) x :> (- (d * rinv(f(x) ^ 2)))";
+\ ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
- DERIV_rinv_fun] delsimps [thm "realpow_Suc"]) 1);
-qed "NSDERIV_rinv_fun";
+ DERIV_inverse_fun] delsimps [thm "realpow_Suc"]) 1);
+qed "NSDERIV_inverse_fun";
(*--------------------------------------------------------------
Derivative of quotient
-------------------------------------------------------------*)
Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) ~= #0 |] \
-\ ==> DERIV (%y. f(y)*rinv(g y)) x :> (d*g(x) \
-\ + -(e*f(x)))*rinv(g(x) ^ 2)";
-by (dres_inst_tac [("f","g")] DERIV_rinv_fun 1);
+\ ==> DERIV (%y. f(y)*inverse(g y)) x :> (d*g(x) \
+\ + -(e*f(x)))*inverse(g(x) ^ 2)";
+by (dres_inst_tac [("f","g")] DERIV_inverse_fun 1);
by (dtac DERIV_mult 2);
by (REPEAT(assume_tac 1));
by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
- realpow_rinv,real_minus_mult_eq1] @ real_mult_ac delsimps
+ realpow_inverse,real_minus_mult_eq1] @ real_mult_ac delsimps
[thm "realpow_Suc",real_minus_mult_eq1 RS sym,
real_minus_mult_eq2 RS sym]) 1);
qed "DERIV_quotient";
Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) ~= #0 |] \
-\ ==> NSDERIV (%y. f(y)*rinv(g y)) x :> (d*g(x) \
-\ + -(e*f(x)))*rinv(g(x) ^ 2)";
+\ ==> NSDERIV (%y. f(y)*inverse(g y)) x :> (d*g(x) \
+\ + -(e*f(x)))*inverse(g(x) ^ 2)";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
DERIV_quotient] delsimps [thm "realpow_Suc"]) 1);
qed "NSDERIV_quotient";
@@ -1467,7 +1467,7 @@
\ (EX g. (ALL z. f z - f x = g z * (z - x)) & isCont g x & g x = l)";
by (Step_tac 1);
by (res_inst_tac
- [("x","%z. if z = x then l else (f(z) - f(x)) * rinv (z - x)")] exI 1);
+ [("x","%z. if z = x then l else (f(z) - f(x)) * inverse (z - x)")] exI 1);
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
ARITH_PROVE "z ~= x ==> z - x ~= (#0::real)"]));
by (auto_tac (claset(),simpset() addsimps [isCont_iff,DERIV_iff]));
@@ -1486,7 +1486,7 @@
\ ==> NSDERIV f x :> l";
by (auto_tac (claset(),simpset() addsimps [NSDERIV_iff2,starfun_mult
RS sym]));
-by (rtac (starfun_hrinv2 RS subst) 1);
+by (rtac (starfun_inverse2 RS subst) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
starfun_diff RS sym,starfun_Id]));
by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff3 RS sym,
--- a/src/HOL/Real/Hyperreal/Lim.thy Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.thy Wed Dec 06 12:34:40 2000 +0100
@@ -30,12 +30,12 @@
(* differentiation: D is derivative of function f at x *)
deriv:: [real=>real,real,real] => bool ("(DERIV (_)/ (_)/ :> (_))" 60)
- "DERIV f x :> D == ((%h. (f(x + h) + -f(x))*rinv(h)) -- #0 --> D)"
+ "DERIV f x :> D == ((%h. (f(x + h) + -f(x))*inverse(h)) -- #0 --> D)"
nsderiv :: [real=>real,real,real] => bool ("(NSDERIV (_)/ (_)/ :> (_))" 60)
"NSDERIV f x :> D == (ALL h: Infinitesimal - {0}.
((*f* f)(hypreal_of_real x + h) +
- -hypreal_of_real (f x))*hrinv(h) @= hypreal_of_real D)"
+ -hypreal_of_real (f x))*inverse(h) @= hypreal_of_real D)"
differentiable :: [real=>real,real] => bool (infixl 60)
"f differentiable x == (EX D. DERIV f x :> D)"
--- a/src/HOL/Real/Hyperreal/NSA.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NSA.ML Wed Dec 06 12:34:40 2000 +0100
@@ -27,9 +27,9 @@
by (simp_tac (simpset() addsimps [hypreal_of_real_mult]) 1);
qed "SReal_mult";
-Goalw [SReal_def] "[| x: SReal; x ~= 0 |] ==> hrinv x : SReal";
-by (blast_tac (claset() addSDs [hypreal_of_real_hrinv2]) 1);
-qed "SReal_hrinv";
+Goalw [SReal_def] "[| x: SReal; x ~= 0 |] ==> inverse x : SReal";
+by (blast_tac (claset() addSDs [hypreal_of_real_inverse2]) 1);
+qed "SReal_inverse";
Goalw [SReal_def] "x: SReal ==> -x : SReal";
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_minus RS sym]));
@@ -69,8 +69,8 @@
Addsimps [SReal_zero,SReal_two];
-Goal "r : SReal ==> r*hrinv(1hr + 1hr): SReal";
-by (blast_tac (claset() addSIs [SReal_mult,SReal_hrinv,
+Goal "r : SReal ==> r*inverse(1hr + 1hr): SReal";
+by (blast_tac (claset() addSIs [SReal_mult,SReal_inverse,
SReal_two,hypreal_two_not_zero]) 1);
qed "SReal_half";
@@ -331,16 +331,16 @@
by (auto_tac (claset() addSDs [HFiniteD],
simpset() addsimps [Infinitesimal_def]));
by (forward_tac [hrabs_less_gt_zero] 1);
-by (dtac (hypreal_hrinv_gt_zero RSN (2,hypreal_mult_less_mono2)) 1
+by (dtac (hypreal_inverse_gt_zero RSN (2,hypreal_mult_less_mono2)) 1
THEN assume_tac 1);
-by (dtac ((hypreal_not_refl2 RS not_sym) RSN (2,SReal_hrinv)) 1
+by (dtac ((hypreal_not_refl2 RS not_sym) RSN (2,SReal_inverse)) 1
THEN assume_tac 1);
by (dtac SReal_mult 1 THEN assume_tac 1);
-by (thin_tac "hrinv t : SReal" 1);
+by (thin_tac "inverse t : SReal" 1);
by (auto_tac (claset() addSDs [bspec],simpset() addsimps [hrabs_mult]));
by (dtac hrabs_mult_less 1 THEN assume_tac 1);
by (dtac (hypreal_not_refl2 RS not_sym) 1);
-by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
+by (auto_tac (claset() addSDs [hypreal_mult_inverse],
simpset() addsimps [hrabs_mult] @ hypreal_mult_ac));
qed "Infinitesimal_HFinite_mult";
@@ -352,26 +352,26 @@
(*** rather long proof ***)
Goalw [HInfinite_def,Infinitesimal_def]
- "x: HInfinite ==> hrinv x: Infinitesimal";
+ "x: HInfinite ==> inverse x: Infinitesimal";
by (Auto_tac);
-by (eres_inst_tac [("x","hrinv r")] ballE 1);
-by (rtac (hrabs_hrinv RS ssubst) 1);
-by (etac (((hypreal_hrinv_gt_zero RS hypreal_less_trans)
+by (eres_inst_tac [("x","inverse r")] ballE 1);
+by (rtac (hrabs_inverse RS ssubst) 1);
+by (etac (((hypreal_inverse_gt_zero RS hypreal_less_trans)
RS hypreal_not_refl2 RS not_sym) RS (hrabs_not_zero_iff
RS iffD2)) 1 THEN assume_tac 1);
by (forw_inst_tac [("x1","r"),("R3.0","abs x")]
- (hypreal_hrinv_gt_zero RS hypreal_less_trans) 1);
+ (hypreal_inverse_gt_zero RS hypreal_less_trans) 1);
by (assume_tac 1);
by (forw_inst_tac [("s","abs x"),("t","0")]
(hypreal_not_refl2 RS not_sym) 1);
-by (dtac ((hypreal_hrinv_hrinv RS sym) RS subst) 1);
+by (dtac ((hypreal_inverse_inverse RS sym) RS subst) 1);
by (rotate_tac 2 1 THEN assume_tac 1);
-by (dres_inst_tac [("x","abs x")] hypreal_hrinv_gt_zero 1);
-by (rtac (hypreal_hrinv_less_iff RS ssubst) 1);
-by (auto_tac (claset() addSDs [SReal_hrinv],
+by (dres_inst_tac [("x","abs x")] hypreal_inverse_gt_zero 1);
+by (rtac (hypreal_inverse_less_iff RS ssubst) 1);
+by (auto_tac (claset() addSDs [SReal_inverse],
simpset() addsimps [hypreal_not_refl2 RS not_sym,
hypreal_less_not_refl]));
-qed "HInfinite_hrinv_Infinitesimal";
+qed "HInfinite_inverse_Infinitesimal";
Goalw [HInfinite_def]
"[|x: HInfinite;y: HInfinite|] ==> (x*y): HInfinite";
@@ -767,7 +767,7 @@
qed "inf_close_mult_hypreal_of_real";
Goal "!!a. [| a: SReal; a ~= 0; a*x @= 0 |] ==> x @= 0";
-by (dtac (SReal_hrinv RS (SReal_subset_HFinite RS subsetD)) 1);
+by (dtac (SReal_inverse RS (SReal_subset_HFinite RS subsetD)) 1);
by (auto_tac (claset() addDs [inf_close_mult2],
simpset() addsimps [hypreal_mult_assoc RS sym]));
qed "inf_close_SReal_mult_cancel_zero";
@@ -790,7 +790,7 @@
Addsimps [inf_close_mult_SReal_zero_cancel_iff];
Goal "!!a. [| a: SReal; a ~= 0; a* w @= a*z |] ==> w @= z";
-by (dtac (SReal_hrinv RS (SReal_subset_HFinite RS subsetD)) 1);
+by (dtac (SReal_inverse RS (SReal_subset_HFinite RS subsetD)) 1);
by (auto_tac (claset() addDs [inf_close_mult2],
simpset() addsimps [hypreal_mult_assoc RS sym]));
qed "inf_close_SReal_mult_cancel";
@@ -912,7 +912,7 @@
qed "HFinite_diff_Infinitesimal_inf_close";
Goal "[| y ~= 0; y: Infinitesimal; \
-\ x*hrinv(y) : HFinite \
+\ x*inverse(y) : HFinite \
\ |] ==> x : Infinitesimal";
by (dtac Infinitesimal_HFinite_mult2 1);
by (assume_tac 1);
@@ -1201,69 +1201,69 @@
by (fast_tac (claset() addIs [not_HFinite_HInfinite]) 1);
qed "HInfinite_diff_HFinite_Infinitesimal_disj";
-Goal "[| x : HFinite; x ~: Infinitesimal |] ==> hrinv x : HFinite";
-by (cut_inst_tac [("x","hrinv x")] HInfinite_HFinite_disj 1);
-by (forward_tac [not_Infinitesimal_not_zero RS hypreal_hrinv_hrinv] 1);
-by (auto_tac (claset() addSDs [HInfinite_hrinv_Infinitesimal],simpset()));
-qed "HFinite_hrinv";
+Goal "[| x : HFinite; x ~: Infinitesimal |] ==> inverse x : HFinite";
+by (cut_inst_tac [("x","inverse x")] HInfinite_HFinite_disj 1);
+by (forward_tac [not_Infinitesimal_not_zero RS hypreal_inverse_inverse] 1);
+by (auto_tac (claset() addSDs [HInfinite_inverse_Infinitesimal],simpset()));
+qed "HFinite_inverse";
-Goal "x : HFinite - Infinitesimal ==> hrinv x : HFinite";
-by (blast_tac (claset() addIs [HFinite_hrinv]) 1);
-qed "HFinite_hrinv2";
+Goal "x : HFinite - Infinitesimal ==> inverse x : HFinite";
+by (blast_tac (claset() addIs [HFinite_inverse]) 1);
+qed "HFinite_inverse2";
(* stronger statement possible in fact *)
-Goal "x ~: Infinitesimal ==> hrinv(x) : HFinite";
+Goal "x ~: Infinitesimal ==> inverse(x) : HFinite";
by (dtac HInfinite_diff_HFinite_Infinitesimal_disj 1);
-by (blast_tac (claset() addIs [HFinite_hrinv,
- HInfinite_hrinv_Infinitesimal,
+by (blast_tac (claset() addIs [HFinite_inverse,
+ HInfinite_inverse_Infinitesimal,
Infinitesimal_subset_HFinite RS subsetD]) 1);
-qed "Infinitesimal_hrinv_HFinite";
+qed "Infinitesimal_inverse_HFinite";
-Goal "x : HFinite - Infinitesimal ==> hrinv x : HFinite - Infinitesimal";
-by (auto_tac (claset() addIs [Infinitesimal_hrinv_HFinite],simpset()));
+Goal "x : HFinite - Infinitesimal ==> inverse x : HFinite - Infinitesimal";
+by (auto_tac (claset() addIs [Infinitesimal_inverse_HFinite],simpset()));
by (dtac Infinitesimal_HFinite_mult2 1);
by (auto_tac (claset() addSDs [not_Infinitesimal_not_zero,
- hypreal_mult_hrinv],simpset()));
-qed "HFinite_not_Infinitesimal_hrinv";
+ hypreal_mult_inverse],simpset()));
+qed "HFinite_not_Infinitesimal_inverse";
Goal "[| x @= y; y : HFinite - Infinitesimal |] \
-\ ==> hrinv x @= hrinv y";
+\ ==> inverse x @= inverse y";
by (forward_tac [HFinite_diff_Infinitesimal_inf_close] 1);
by (assume_tac 1);
by (forward_tac [not_Infinitesimal_not_zero2] 1);
by (forw_inst_tac [("x","x")] not_Infinitesimal_not_zero2 1);
-by (REPEAT(dtac HFinite_hrinv2 1));
+by (REPEAT(dtac HFinite_inverse2 1));
by (dtac inf_close_mult2 1 THEN assume_tac 1);
by (Auto_tac);
-by (dres_inst_tac [("c","hrinv x")] inf_close_mult1 1
+by (dres_inst_tac [("c","inverse x")] inf_close_mult1 1
THEN assume_tac 1);
by (auto_tac (claset() addIs [inf_close_sym],
simpset() addsimps [hypreal_mult_assoc]));
-qed "inf_close_hrinv";
+qed "inf_close_inverse";
Goal "[| x: HFinite - Infinitesimal; \
-\ h : Infinitesimal |] ==> hrinv(x + h) @= hrinv x";
-by (auto_tac (claset() addIs [inf_close_hrinv,
+\ h : Infinitesimal |] ==> inverse(x + h) @= inverse x";
+by (auto_tac (claset() addIs [inf_close_inverse,
Infinitesimal_add_inf_close_self,inf_close_sym],simpset()));
-qed "hrinv_add_Infinitesimal_inf_close";
+qed "inverse_add_Infinitesimal_inf_close";
Goal "[| x: HFinite - Infinitesimal; \
-\ h : Infinitesimal |] ==> hrinv(h + x) @= hrinv x";
+\ h : Infinitesimal |] ==> inverse(h + x) @= inverse x";
by (rtac (hypreal_add_commute RS subst) 1);
-by (blast_tac (claset() addIs [hrinv_add_Infinitesimal_inf_close]) 1);
-qed "hrinv_add_Infinitesimal_inf_close2";
+by (blast_tac (claset() addIs [inverse_add_Infinitesimal_inf_close]) 1);
+qed "inverse_add_Infinitesimal_inf_close2";
Goal
"[| x: HFinite - Infinitesimal; \
-\ h : Infinitesimal |] ==> hrinv(x + h) + -hrinv x @= h";
+\ h : Infinitesimal |] ==> inverse(x + h) + -inverse x @= h";
by (rtac inf_close_trans2 1);
-by (auto_tac (claset() addIs [hrinv_add_Infinitesimal_inf_close,
+by (auto_tac (claset() addIs [inverse_add_Infinitesimal_inf_close,
inf_close_minus_iff RS iffD1],simpset() addsimps [mem_infmal_iff RS sym]));
-qed "hrinv_add_Infinitesimal_inf_close_Infinitesimal";
+qed "inverse_add_Infinitesimal_inf_close_Infinitesimal";
Goal "(x : Infinitesimal) = (x*x : Infinitesimal)";
by (auto_tac (claset() addIs [Infinitesimal_mult],simpset()));
-by (rtac ccontr 1 THEN forward_tac [Infinitesimal_hrinv_HFinite] 1);
+by (rtac ccontr 1 THEN forward_tac [Infinitesimal_inverse_HFinite] 1);
by (forward_tac [not_Infinitesimal_not_zero] 1);
by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult],
simpset() addsimps [hypreal_mult_assoc]));
@@ -1285,7 +1285,7 @@
Goal "!!a. [| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z";
by (Step_tac 1);
-by (ftac HFinite_hrinv 1 THEN assume_tac 1);
+by (ftac HFinite_inverse 1 THEN assume_tac 1);
by (dtac not_Infinitesimal_not_zero 1);
by (auto_tac (claset() addDs [inf_close_mult2],
simpset() addsimps [hypreal_mult_assoc RS sym]));
@@ -1801,18 +1801,18 @@
val [prem1,prem2] =
goal thy "[| x: HFinite; st x ~= 0 |] \
-\ ==> st(hrinv x) = hrinv (st x)";
+\ ==> st(inverse x) = inverse (st x)";
by (rtac ((prem2 RS hypreal_mult_left_cancel) RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [st_not_zero,
- st_mult RS sym,prem2,st_not_Infinitesimal,HFinite_hrinv,prem1]));
-qed "st_hrinv";
+ st_mult RS sym,prem2,st_not_Infinitesimal,HFinite_inverse,prem1]));
+qed "st_inverse";
val [prem1,prem2,prem3] =
goal thy "[| x: HFinite; y: HFinite; st y ~= 0 |] \
-\ ==> st(x * hrinv y) = (st x) * hrinv (st y)";
+\ ==> st(x * inverse y) = (st x) * inverse (st y)";
by (auto_tac (claset(),simpset() addsimps [st_not_zero,prem3,
- st_mult,prem2,st_not_Infinitesimal,HFinite_hrinv,prem1,st_hrinv]));
-qed "st_mult_hrinv";
+ st_mult,prem2,st_not_Infinitesimal,HFinite_inverse,prem1,st_inverse]));
+qed "st_mult_inverse";
Goal "x: HFinite ==> st(st(x)) = st(x)";
by (blast_tac (claset() addIs [st_HFinite,
@@ -2059,36 +2059,36 @@
(*------------------------------------------------------------------------
Infinitesimals as smaller than 1/n for all n::nat (> 0)
------------------------------------------------------------------------*)
-Goal "(ALL r. 0 < r --> x < r) = (ALL n. x < rinv(real_of_posnat n))";
+Goal "(ALL r. 0 < r --> x < r) = (ALL n. x < inverse(real_of_posnat n))";
by (auto_tac (claset(),simpset() addsimps
- [rename_numerals (real_of_posnat_gt_zero RS real_rinv_gt_zero)]));
+ [rename_numerals (real_of_posnat_gt_zero RS real_inverse_gt_zero)]));
by (blast_tac (claset() addSDs [rename_numerals reals_Archimedean]
addIs [real_less_trans]) 1);
qed "lemma_Infinitesimal";
Goal "(ALL r: SReal. 0 < r --> x < r) = \
-\ (ALL n. x < hrinv(hypreal_of_posnat n))";
+\ (ALL n. x < inverse(hypreal_of_posnat n))";
by (Step_tac 1);
-by (dres_inst_tac [("x","hypreal_of_real (rinv(real_of_posnat n))")] bspec 1);
+by (dres_inst_tac [("x","hypreal_of_real (inverse(real_of_posnat n))")] bspec 1);
by (Full_simp_tac 1);
-by (rtac (real_of_posnat_gt_zero RS real_rinv_gt_zero RS
+by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero RS
(hypreal_of_real_less_iff RS iffD1) RSN(2,impE)) 1);
by (assume_tac 2);
by (asm_full_simp_tac (simpset() addsimps
- [real_not_refl2 RS not_sym RS hypreal_of_real_hrinv RS sym,
+ [real_not_refl2 RS not_sym RS hypreal_of_real_inverse RS sym,
rename_numerals real_of_posnat_gt_zero,hypreal_of_real_zero,
hypreal_of_real_of_posnat]) 1);
by (auto_tac (claset() addSDs [reals_Archimedean],
simpset() addsimps [SReal_iff,hypreal_of_real_zero RS sym]));
by (dtac (hypreal_of_real_less_iff RS iffD1) 1);
by (asm_full_simp_tac (simpset() addsimps
- [real_not_refl2 RS not_sym RS hypreal_of_real_hrinv RS sym,
+ [real_not_refl2 RS not_sym RS hypreal_of_real_inverse RS sym,
rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1);
by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
qed "lemma_Infinitesimal2";
Goalw [Infinitesimal_def]
- "Infinitesimal = {x. ALL n. abs x < hrinv (hypreal_of_posnat n)}";
+ "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_posnat n)}";
by (auto_tac (claset(),simpset() addsimps [lemma_Infinitesimal2]));
qed "Infinitesimal_hypreal_of_posnat_iff";
@@ -2182,8 +2182,8 @@
-----------------------------------------------*)
Goal "ehr : Infinitesimal";
-by (auto_tac (claset() addSIs [HInfinite_hrinv_Infinitesimal,HInfinite_omega],
- simpset() addsimps [hypreal_epsilon_hrinv_omega]));
+by (auto_tac (claset() addSIs [HInfinite_inverse_Infinitesimal,HInfinite_omega],
+ simpset() addsimps [hypreal_epsilon_inverse_omega]));
qed "Infinitesimal_epsilon";
Addsimps [Infinitesimal_epsilon];
@@ -2203,52 +2203,52 @@
that ALL n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
-----------------------------------------------------------------------*)
-Goal "!!u. 0 < u ==> finite {n. u < rinv(real_of_posnat n)}";
-by (asm_simp_tac (simpset() addsimps [real_of_posnat_less_rinv_iff]) 1);
+Goal "!!u. 0 < u ==> finite {n. u < inverse(real_of_posnat n)}";
+by (asm_simp_tac (simpset() addsimps [real_of_posnat_less_inverse_iff]) 1);
by (rtac finite_real_of_posnat_less_real 1);
-qed "finite_rinv_real_of_posnat_gt_real";
+qed "finite_inverse_real_of_posnat_gt_real";
-Goal "{n. u <= rinv(real_of_posnat n)} = \
-\ {n. u < rinv(real_of_posnat n)} Un {n. u = rinv(real_of_posnat n)}";
+Goal "{n. u <= inverse(real_of_posnat n)} = \
+\ {n. u < inverse(real_of_posnat n)} Un {n. u = inverse(real_of_posnat n)}";
by (auto_tac (claset() addDs [real_le_imp_less_or_eq],
simpset() addsimps [real_le_refl,real_less_imp_le]));
qed "lemma_real_le_Un_eq2";
-Goal "!!u. 0 < u ==> finite {n::nat. u = rinv(real_of_posnat n)}";
-by (asm_simp_tac (simpset() addsimps [real_of_posnat_rinv_eq_iff]) 1);
+Goal "!!u. 0 < u ==> finite {n::nat. u = inverse(real_of_posnat n)}";
+by (asm_simp_tac (simpset() addsimps [real_of_posnat_inverse_eq_iff]) 1);
by (auto_tac (claset() addIs [lemma_finite_omega_set RSN
(2,finite_subset)],simpset()));
qed "lemma_finite_omega_set2";
-Goal "!!u. 0 < u ==> finite {n. u <= rinv(real_of_posnat n)}";
+Goal "!!u. 0 < u ==> finite {n. u <= inverse(real_of_posnat n)}";
by (auto_tac (claset(),simpset() addsimps
[lemma_real_le_Un_eq2,lemma_finite_omega_set2,
- finite_rinv_real_of_posnat_gt_real]));
-qed "finite_rinv_real_of_posnat_ge_real";
+ finite_inverse_real_of_posnat_gt_real]));
+qed "finite_inverse_real_of_posnat_ge_real";
Goal "!!u. 0 < u ==> \
-\ {n. u <= rinv(real_of_posnat n)} ~: FreeUltrafilterNat";
+\ {n. u <= inverse(real_of_posnat n)} ~: FreeUltrafilterNat";
by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
- finite_rinv_real_of_posnat_ge_real]) 1);
-qed "rinv_real_of_posnat_ge_real_FreeUltrafilterNat";
+ finite_inverse_real_of_posnat_ge_real]) 1);
+qed "inverse_real_of_posnat_ge_real_FreeUltrafilterNat";
(*--------------------------------------------------------------
- The complement of {n. u <= rinv(real_of_posnat n)} =
- {n. rinv(real_of_posnat n) < u} is in FreeUltrafilterNat
+ The complement of {n. u <= inverse(real_of_posnat n)} =
+ {n. inverse(real_of_posnat n) < u} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
-Goal "- {n. u <= rinv(real_of_posnat n)} = \
-\ {n. rinv(real_of_posnat n) < u}";
+Goal "- {n. u <= inverse(real_of_posnat n)} = \
+\ {n. inverse(real_of_posnat n) < u}";
by (auto_tac (claset() addSDs [real_le_less_trans],
simpset() addsimps [not_real_leE,real_less_not_refl]));
val lemma = result();
Goal "!!u. 0 < u ==> \
-\ {n. rinv(real_of_posnat n) < u} : FreeUltrafilterNat";
-by (cut_inst_tac [("u","u")] rinv_real_of_posnat_ge_real_FreeUltrafilterNat 1);
+\ {n. inverse(real_of_posnat n) < u} : FreeUltrafilterNat";
+by (cut_inst_tac [("u","u")] inverse_real_of_posnat_ge_real_FreeUltrafilterNat 1);
by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
simpset() addsimps [lemma]));
-qed "FreeUltrafilterNat_rinv_real_of_posnat";
+qed "FreeUltrafilterNat_inverse_real_of_posnat";
(*--------------------------------------------------------------
Example where we get a hyperreal from a real sequence
@@ -2261,37 +2261,37 @@
(*-----------------------------------------------------
|X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x|: Infinitesimal
-----------------------------------------------------*)
-Goal "ALL n. abs(X n + -x) < rinv(real_of_posnat n) \
+Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \
\ ==> Abs_hypreal(hyprel^^{X}) + -hypreal_of_real x : Infinitesimal";
by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals
- FreeUltrafilterNat_rinv_real_of_posnat,
+ FreeUltrafilterNat_inverse_real_of_posnat,
FreeUltrafilterNat_all,FreeUltrafilterNat_Int] addIs [real_less_trans,
FreeUltrafilterNat_subset],simpset() addsimps [hypreal_minus,
hypreal_of_real_minus RS sym,hypreal_of_real_def,hypreal_add,
- Infinitesimal_FreeUltrafilterNat_iff,hypreal_hrinv,hypreal_of_real_of_posnat]));
+ Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse,hypreal_of_real_of_posnat]));
qed "real_seq_to_hypreal_Infinitesimal";
-Goal "ALL n. abs(X n + -x) < rinv(real_of_posnat n) \
+Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \
\ ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x";
by (rtac (inf_close_minus_iff RS ssubst) 1);
by (rtac (mem_infmal_iff RS subst) 1);
by (etac real_seq_to_hypreal_Infinitesimal 1);
qed "real_seq_to_hypreal_inf_close";
-Goal "ALL n. abs(x + -X n) < rinv(real_of_posnat n) \
+Goal "ALL n. abs(x + -X n) < inverse(real_of_posnat n) \
\ ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x";
by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel,
real_seq_to_hypreal_inf_close]) 1);
qed "real_seq_to_hypreal_inf_close2";
-Goal "ALL n. abs(X n + -Y n) < rinv(real_of_posnat n) \
+Goal "ALL n. abs(X n + -Y n) < inverse(real_of_posnat n) \
\ ==> Abs_hypreal(hyprel^^{X}) + \
\ -Abs_hypreal(hyprel^^{Y}) : Infinitesimal";
by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals
- FreeUltrafilterNat_rinv_real_of_posnat,
+ FreeUltrafilterNat_inverse_real_of_posnat,
FreeUltrafilterNat_all,FreeUltrafilterNat_Int] addIs [real_less_trans,
FreeUltrafilterNat_subset],simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add,
- hypreal_hrinv,hypreal_of_real_of_posnat]));
+ hypreal_inverse,hypreal_of_real_of_posnat]));
qed "real_seq_to_hypreal_Infinitesimal2";
\ No newline at end of file
--- a/src/HOL/Real/Hyperreal/NatStar.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NatStar.ML Wed Dec 06 12:34:40 2000 +0100
@@ -314,11 +314,11 @@
qed "starfunNat_minus";
Goal "ALL x. f x ~= 0 ==> \
-\ hrinv ((*fNat* f) x) = (*fNat* (%x. rinv (f x))) x";
+\ inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypreal_hrinv]));
-qed "starfunNat_hrinv";
+ hypreal_inverse]));
+qed "starfunNat_inverse";
(*--------------------------------------------------------
extented function has same solution as its standard
@@ -365,13 +365,13 @@
------------------------------------------------------------------*)
Goal
"!!f. (*fNat* f) x ~= 0 ==> \
-\ hrinv ((*fNat* f) x) = (*fNat* (%x. rinv (f x))) x";
+\ inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
addSDs [FreeUltrafilterNat_Compl_mem],
- simpset() addsimps [starfunNat,hypreal_hrinv,
+ simpset() addsimps [starfunNat,hypreal_inverse,
hypreal_zero_def]));
-qed "starfunNat_hrinv2";
+qed "starfunNat_inverse2";
(*-----------------------------------------------------------------
Example of transfer of a property from reals to hyperreals
@@ -449,12 +449,12 @@
qed "starfunNat_real_of_nat";
Goal "N : HNatInfinite \
-\ ==> (*fNat* (%x. rinv (real_of_nat x))) N = hrinv(hypreal_of_hypnat N)";
-by (res_inst_tac [("f1","rinv")] (starfun_stafunNat_o2 RS subst) 1);
+\ ==> (*fNat* (%x. inverse (real_of_nat x))) N = inverse(hypreal_of_hypnat N)";
+by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1);
by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat,
- starfun_rinv_hrinv]));
-qed "starfunNat_rinv_real_of_nat_eq";
+ starfun_inverse_inverse]));
+qed "starfunNat_inverse_real_of_nat_eq";
(*----------------------------------------------------------
Internal functions - some redundancy with *fNat* now
--- a/src/HOL/Real/Hyperreal/SEQ.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML Wed Dec 06 12:34:40 2000 +0100
@@ -11,13 +11,13 @@
-------------------------------------------------------------------------- *)
Goalw [hypnat_omega_def]
- "(*fNat* (%n::nat. rinv(real_of_posnat n))) whn : Infinitesimal";
+ "(*fNat* (%n::nat. inverse(real_of_posnat n))) whn : Infinitesimal";
by (auto_tac (claset(),simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
by (auto_tac (claset(),simpset() addsimps (map rename_numerals)
- [real_of_posnat_gt_zero,real_rinv_gt_zero,abs_eqI2,
- FreeUltrafilterNat_rinv_real_of_posnat]));
+ [real_of_posnat_gt_zero,real_inverse_gt_zero,abs_eqI2,
+ FreeUltrafilterNat_inverse_real_of_posnat]));
qed "SEQ_Infinitesimal";
(*--------------------------------------------------------------------------
@@ -275,46 +275,46 @@
qed "NSLIMSEQ_diff";
(*---------------------------------------------------------------
- Proof is exactly same as that of NSLIM_rinv except
- for starfunNat_hrinv2 --- would not be the case if we
+ Proof is exactly same as that of NSLIM_inverse except
+ for starfunNat_inverse2 --- would not be the case if we
had generalised net theorems for example. Not our
real concern though.
--------------------------------------------------------------*)
Goalw [NSLIMSEQ_def]
"!!X. [| X ----NS> a; a ~= #0 |] \
-\ ==> (%n. rinv(X n)) ----NS> rinv(a)";
+\ ==> (%n. inverse(X n)) ----NS> inverse(a)";
by (Step_tac 1);
by (dtac bspec 1 THEN auto_tac (claset(),simpset()
addsimps [hypreal_of_real_not_zero_iff RS sym,
- hypreal_of_real_hrinv RS sym]));
+ hypreal_of_real_inverse RS sym]));
by (forward_tac [inf_close_hypreal_of_real_not_zero] 1
THEN assume_tac 1);
-by (auto_tac (claset() addSEs [(starfunNat_hrinv2 RS subst),
- inf_close_hrinv,hypreal_of_real_HFinite_diff_Infinitesimal],
+by (auto_tac (claset() addSEs [(starfunNat_inverse2 RS subst),
+ inf_close_inverse,hypreal_of_real_HFinite_diff_Infinitesimal],
simpset()));
-qed "NSLIMSEQ_rinv";
+qed "NSLIMSEQ_inverse";
(*------ Standard version of theorem -------*)
Goal
"!!X. [| X ----> a; a ~= #0 |] \
-\ ==> (%n. rinv(X n)) ----> rinv(a)";
-by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_rinv,
+\ ==> (%n. inverse(X n)) ----> inverse(a)";
+by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_inverse,
LIMSEQ_NSLIMSEQ_iff]) 1);
-qed "LIMSEQ_rinv";
+qed "LIMSEQ_inverse";
(* trivially proved *)
Goal
"!!X. [| X ----NS> a; Y ----NS> b; b ~= #0 |] \
-\ ==> (%n. (X n) * rinv(Y n)) ----NS> a*rinv(b)";
-by (blast_tac (claset() addDs [NSLIMSEQ_rinv,NSLIMSEQ_mult]) 1);
-qed "NSLIMSEQ_mult_rinv";
+\ ==> (%n. (X n) * inverse(Y n)) ----NS> a*inverse(b)";
+by (blast_tac (claset() addDs [NSLIMSEQ_inverse,NSLIMSEQ_mult]) 1);
+qed "NSLIMSEQ_mult_inverse";
(* let's give a standard proof of theorem *)
Goal
"!!X. [| X ----> a; Y ----> b; b ~= #0 |] \
-\ ==> (%n. (X n) * rinv(Y n)) ----> a*rinv(b)";
-by (blast_tac (claset() addDs [LIMSEQ_rinv,LIMSEQ_mult]) 1);
-qed "LIMSEQ_mult_rinv";
+\ ==> (%n. (X n) * inverse(Y n)) ----> a*inverse(b)";
+by (blast_tac (claset() addDs [LIMSEQ_inverse,LIMSEQ_mult]) 1);
+qed "LIMSEQ_mult_inverse";
(*-----------------------------------------------
Uniqueness of limit
@@ -1205,82 +1205,82 @@
(* standard proof seems easier *)
Goalw [LIMSEQ_def]
"ALL y. EX N. ALL n. N <= n --> y < f(n) \
-\ ==> (%n. rinv(f n)) ----> #0";
+\ ==> (%n. inverse(f n)) ----> #0";
by (Step_tac 1 THEN Asm_full_simp_tac 1);
-by (dres_inst_tac [("x","rinv r")] spec 1 THEN Step_tac 1);
+by (dres_inst_tac [("x","inverse r")] spec 1 THEN Step_tac 1);
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
by (dtac spec 1 THEN Auto_tac);
-by (forward_tac [rename_numerals real_rinv_gt_zero] 1);
+by (forward_tac [rename_numerals real_inverse_gt_zero] 1);
by (forward_tac [real_less_trans] 1 THEN assume_tac 1);
-by (forw_inst_tac [("x","f n")] (rename_numerals real_rinv_gt_zero) 1);
+by (forw_inst_tac [("x","f n")] (rename_numerals real_inverse_gt_zero) 1);
by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
-by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
-by (auto_tac (claset() addIs [real_rinv_less_iff RS iffD1], simpset()));
-qed "LIMSEQ_rinv_zero";
+by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
+by (auto_tac (claset() addIs [real_inverse_less_iff RS iffD1], simpset()));
+qed "LIMSEQ_inverse_zero";
Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \
-\ ==> (%n. rinv(f n)) ----NS> #0";
+\ ==> (%n. inverse(f n)) ----NS> #0";
by (asm_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
- LIMSEQ_rinv_zero]) 1);
-qed "NSLIMSEQ_rinv_zero";
+ LIMSEQ_inverse_zero]) 1);
+qed "NSLIMSEQ_inverse_zero";
(*--------------------------------------------------------------
Sequence 1/n --> 0 as n --> infinity
-------------------------------------------------------------*)
-Goal "(%n. rinv(real_of_posnat n)) ----> #0";
-by (rtac LIMSEQ_rinv_zero 1 THEN Step_tac 1);
+Goal "(%n. inverse(real_of_posnat n)) ----> #0";
+by (rtac LIMSEQ_inverse_zero 1 THEN Step_tac 1);
by (cut_inst_tac [("x","y")] reals_Archimedean2 1);
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
by (Step_tac 1 THEN etac (le_imp_less_or_eq RS disjE) 1);
by (dtac (real_of_posnat_less_iff RS iffD2) 1);
by (auto_tac (claset() addEs [real_less_trans], simpset()));
-qed "LIMSEQ_rinv_real_of_posnat";
+qed "LIMSEQ_inverse_real_of_posnat";
-Goal "(%n. rinv(real_of_posnat n)) ----NS> #0";
+Goal "(%n. inverse(real_of_posnat n)) ----NS> #0";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
- LIMSEQ_rinv_real_of_posnat]) 1);
-qed "NSLIMSEQ_rinv_real_of_posnat";
+ LIMSEQ_inverse_real_of_posnat]) 1);
+qed "NSLIMSEQ_inverse_real_of_posnat";
(*--------------------------------------------
Sequence r + 1/n --> r as n --> infinity
now easily proved
--------------------------------------------*)
-Goal "(%n. r + rinv(real_of_posnat n)) ----> r";
-by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_rinv_real_of_posnat]
+Goal "(%n. r + inverse(real_of_posnat n)) ----> r";
+by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat]
MRS LIMSEQ_add] 1);
by (Auto_tac);
-qed "LIMSEQ_rinv_real_of_posnat_add";
+qed "LIMSEQ_inverse_real_of_posnat_add";
-Goal "(%n. r + rinv(real_of_posnat n)) ----NS> r";
+Goal "(%n. r + inverse(real_of_posnat n)) ----NS> r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
- LIMSEQ_rinv_real_of_posnat_add]) 1);
-qed "NSLIMSEQ_rinv_real_of_posnat_add";
+ LIMSEQ_inverse_real_of_posnat_add]) 1);
+qed "NSLIMSEQ_inverse_real_of_posnat_add";
(*--------------
Also...
--------------*)
-Goal "(%n. r + -rinv(real_of_posnat n)) ----> r";
-by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_rinv_real_of_posnat]
+Goal "(%n. r + -inverse(real_of_posnat n)) ----> r";
+by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat]
MRS LIMSEQ_add_minus] 1);
by (Auto_tac);
-qed "LIMSEQ_rinv_real_of_posnat_add_minus";
+qed "LIMSEQ_inverse_real_of_posnat_add_minus";
-Goal "(%n. r + -rinv(real_of_posnat n)) ----NS> r";
+Goal "(%n. r + -inverse(real_of_posnat n)) ----NS> r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
- LIMSEQ_rinv_real_of_posnat_add_minus]) 1);
-qed "NSLIMSEQ_rinv_real_of_posnat_add_minus";
+ LIMSEQ_inverse_real_of_posnat_add_minus]) 1);
+qed "NSLIMSEQ_inverse_real_of_posnat_add_minus";
-Goal "(%n. r*( #1 + -rinv(real_of_posnat n))) ----> r";
+Goal "(%n. r*( #1 + -inverse(real_of_posnat n))) ----> r";
by (cut_inst_tac [("b","#1")] ([LIMSEQ_const,
- LIMSEQ_rinv_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1);
+ LIMSEQ_inverse_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1);
by (Auto_tac);
-qed "LIMSEQ_rinv_real_of_posnat_add_minus_mult";
+qed "LIMSEQ_inverse_real_of_posnat_add_minus_mult";
-Goal "(%n. r*( #1 + -rinv(real_of_posnat n))) ----NS> r";
+Goal "(%n. r*( #1 + -inverse(real_of_posnat n))) ----NS> r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
- LIMSEQ_rinv_real_of_posnat_add_minus_mult]) 1);
-qed "NSLIMSEQ_rinv_real_of_posnat_add_minus_mult";
+ LIMSEQ_inverse_real_of_posnat_add_minus_mult]) 1);
+qed "NSLIMSEQ_inverse_real_of_posnat_add_minus_mult";
(*---------------------------------------------------------------
Real Powers
--- a/src/HOL/Real/Hyperreal/Series.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML Wed Dec 06 12:34:40 2000 +0100
@@ -438,7 +438,7 @@
[rename_numerals (real_eq_minus_iff2 RS sym)]) 1);
qed "real_not_eq_diff";
-Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * rinv(x - #1)";
+Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)";
by (induct_tac "n" 1);
by (Auto_tac);
by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1);
@@ -448,7 +448,7 @@
real_diff_def,real_mult_commute]) 1);
qed "sumr_geometric";
-Goal "abs(x) < #1 ==> (%n. x ^ n) sums rinv(#1 - x)";
+Goal "abs(x) < #1 ==> (%n. x ^ n) sums inverse(#1 - x)";
by (case_tac "x = #1" 1);
by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2],
simpset() addsimps [sumr_geometric,abs_one,sums_def,
@@ -458,7 +458,7 @@
by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_mult 1);
by (dtac real_not_eq_diff 3);
by (auto_tac (claset() addIs [LIMSEQ_const], simpset() addsimps
- [real_minus_rinv RS sym,real_diff_def,real_add_commute,
+ [real_minus_inverse RS sym,real_diff_def,real_add_commute,
rename_numerals LIMSEQ_rabs_realpow_zero2]));
qed "geometric_sums";
@@ -570,18 +570,18 @@
qed "rabs_ratiotest_lemma";
(* lemmas *)
-Goal "#0 < r ==> (x * r ^ n) * rinv (r ^ n) = x";
+Goal "#0 < (r::real) ==> (x * r ^ n) * inverse (r ^ n) = x";
by (auto_tac (claset(),simpset() addsimps
[real_mult_assoc,rename_numerals realpow_not_zero]));
-val lemma_rinv_realpow = result();
+val lemma_inverse_realpow = result();
-Goal "[| c ~= #0; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
-\ ==> ALL n. N <= n --> abs(f(Suc n)) <= (c * c ^ n)* (rinv(c ^ n)*abs(f n))";
+Goal "[| (c::real) ~= #0; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
+\ ==> ALL n. N <= n --> abs(f(Suc n)) <= (c * c ^ n)* (inverse(c ^ n)*abs(f n))";
by (auto_tac (claset(),simpset() addsimps real_mult_ac));
by (res_inst_tac [("z2.1","c ^ n")] (real_mult_left_commute RS subst) 1);
by (auto_tac (claset(),simpset() addsimps [rename_numerals
realpow_not_zero]));
-val lemma_rinv_realpow2 = result();
+val lemma_inverse_realpow2 = result();
Goal "(k::nat) <= l ==> (EX n. l = k + n)";
by (dtac le_imp_less_or_eq 1);
@@ -600,7 +600,7 @@
by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1);
by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
-by (res_inst_tac [("g","%n. (abs (f N)* rinv(c ^ N))*c ^ n")]
+by (res_inst_tac [("g","%n. (abs (f N)* inverse(c ^ N))*c ^ n")]
summable_comparison_test 1);
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
by (dtac (le_Suc_ex_iff RS iffD1) 1);
@@ -612,7 +612,7 @@
by (auto_tac (claset() addIs [real_mult_le_le_mono1],
simpset() addsimps [summable_def, CLAIM_SIMP
"a * (b * c) = b * (a * (c::real))" real_mult_ac]));
-by (res_inst_tac [("x","(abs(f N)*rinv(c ^ N))*rinv(#1 - c)")] exI 1);
+by (res_inst_tac [("x","(abs(f N)*inverse(c ^ N))*inverse(#1 - c)")] exI 1);
by (auto_tac (claset() addSIs [sums_mult,geometric_sums], simpset() addsimps
[abs_eqI2]));
qed "ratio_test";
--- a/src/HOL/Real/Hyperreal/Star.ML Wed Dec 06 12:34:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Star.ML Wed Dec 06 12:34:40 2000 +0100
@@ -355,11 +355,11 @@
(*----------------------------------------------------
Examples: hrabs is nonstandard extension of rabs
- hrinv is nonstandard extension of rinv
+ inverse is nonstandard extension of inverse
---------------------------------------------------*)
(* can be proved easily using theorem "starfun" and *)
-(* properties of ultrafilter as for hrinv below we *)
+(* properties of ultrafilter as for inverse below we *)
(* use the theorem we proved above instead *)
Goal "*f* abs = abs";
@@ -367,54 +367,54 @@
(is_starext_starfun_iff RS iffD1) RS sym) 1);
qed "starfun_rabs_hrabs";
-Goal "!!x. x ~= 0 ==> (*f* rinv) x = hrinv(x)";
+Goal "!!x. x ~= 0 ==> (*f* inverse) x = inverse(x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
- hypreal_hrinv,hypreal_zero_def]));
+ hypreal_inverse,hypreal_zero_def]));
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (auto_tac (claset() addEs [FreeUltrafilterNat_subset],simpset()));
-qed "starfun_rinv_hrinv";
+qed "starfun_inverse_inverse";
(* more specifically *)
-Goal "(*f* rinv) ehr = hrinv (ehr)";
-by (rtac (hypreal_epsilon_not_zero RS starfun_rinv_hrinv) 1);
-qed "starfun_rinv_epsilon";
+Goal "(*f* inverse) ehr = inverse (ehr)";
+by (rtac (hypreal_epsilon_not_zero RS starfun_inverse_inverse) 1);
+qed "starfun_inverse_epsilon";
Goal "ALL x. f x ~= 0 ==> \
-\ hrinv ((*f* f) x) = (*f* (%x. rinv (f x))) x";
+\ inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
- hypreal_hrinv]));
-qed "starfun_hrinv";
+ hypreal_inverse]));
+qed "starfun_inverse";
Goal "(*f* f) x ~= 0 ==> \
-\ hrinv ((*f* f) x) = (*f* (%x. rinv (f x))) x";
+\ inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
addSDs [FreeUltrafilterNat_Compl_mem],
- simpset() addsimps [starfun,hypreal_hrinv,
+ simpset() addsimps [starfun,hypreal_inverse,
hypreal_zero_def]));
-qed "starfun_hrinv2";
+qed "starfun_inverse2";
Goal "a ~= hypreal_of_real b ==> \
-\ (*f* (%z. rinv (z + -b))) a = hrinv(a + -hypreal_of_real b)";
+\ (*f* (%z. inverse (z + -b))) a = inverse(a + -hypreal_of_real b)";
by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
addSDs [FreeUltrafilterNat_Compl_mem],
simpset() addsimps [starfun,hypreal_of_real_def,hypreal_add,
- hypreal_minus,hypreal_hrinv,rename_numerals
+ hypreal_minus,hypreal_inverse,rename_numerals
(real_eq_minus_iff2 RS sym)]));
-qed "starfun_hrinv3";
+qed "starfun_inverse3";
Goal
"!!f. a + hypreal_of_real b ~= 0 ==> \
-\ (*f* (%z. rinv (z + b))) a = hrinv(a + hypreal_of_real b)";
+\ (*f* (%z. inverse (z + b))) a = inverse(a + hypreal_of_real b)";
by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
addSDs [FreeUltrafilterNat_Compl_mem],
simpset() addsimps [starfun,hypreal_of_real_def,hypreal_add,
- hypreal_hrinv,hypreal_zero_def]));
-qed "starfun_hrinv4";
+ hypreal_inverse,hypreal_zero_def]));
+qed "starfun_inverse4";
(*-------------------------------------------------------------
General lemma/theorem needed for proofs in elementary
@@ -471,11 +471,11 @@
move both if possible?
-------------------------------------------------------------------*)
Goal "(x:Infinitesimal) = (EX X:Rep_hypreal(x). \
-\ ALL m. {n. abs(X n) < rinv(real_of_posnat m)}:FreeUltrafilterNat)";
+\ ALL m. {n. abs(X n) < inverse(real_of_posnat m)}:FreeUltrafilterNat)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl],
simpset() addsimps [Infinitesimal_hypreal_of_posnat_iff,
- hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_hrinv,
+ hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_inverse,
hypreal_hrabs,hypreal_less]));
by (dres_inst_tac [("x","n")] spec 1);
by (Fuf_tac 1);
@@ -483,7 +483,7 @@
Goal "(Abs_hypreal(hyprel^^{X}) @= Abs_hypreal(hyprel^^{Y})) = \
\ (ALL m. {n. abs (X n + - Y n) < \
-\ rinv(real_of_posnat m)} : FreeUltrafilterNat)";
+\ inverse(real_of_posnat m)} : FreeUltrafilterNat)";
by (rtac (inf_close_minus_iff RS ssubst) 1);
by (rtac (mem_infmal_iff RS subst) 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_minus,