# HG changeset patch # User bauerg # Date 976102480 -3600 # Node ID 352f6f209775b3b2fccba42568459f2ef3226541 # Parent e3229a37d53f2082871ab6b16561af829d1fc17d converted rinv and hrinv to inverse; diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/HRealAbs.ML --- 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); diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/HyperDef.ML --- 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); diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/HyperDef.thy --- 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 diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/HyperOrd.ML --- 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"; diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/HyperPow.ML --- 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); diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/Lim.ML --- 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, diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/Lim.thy --- 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)" diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/NSA.ML --- 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 ==> [] - 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 diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/NatStar.ML --- 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 diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/SEQ.ML --- 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 diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/Series.ML --- 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"; diff -r e3229a37d53f -r 352f6f209775 src/HOL/Real/Hyperreal/Star.ML --- 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,