renamings: real_of_nat, real_of_int -> (overloaded) real
inf_close -> approx
SReal -> Reals
SNat -> Nats
--- a/src/HOL/Hyperreal/HRealAbs.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.ML Tue Jan 16 12:20:52 2001 +0100
@@ -232,7 +232,7 @@
(*------------------------------------------------------------*)
Goalw [hypreal_of_nat_def, hypreal_of_real_def, real_of_nat_def]
- "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real_of_nat m})";
+ "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})";
by Auto_tac;
qed "hypreal_of_nat_iff";
--- a/src/HOL/Hyperreal/HRealAbs.thy Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.thy Tue Jan 16 12:20:52 2001 +0100
@@ -12,6 +12,6 @@
constdefs
hypreal_of_nat :: nat => hypreal
- "hypreal_of_nat n == hypreal_of_real (real_of_nat n)"
+ "hypreal_of_nat (n::nat) == hypreal_of_real (real n)"
end
\ No newline at end of file
--- a/src/HOL/Hyperreal/HSeries.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/HSeries.ML Tue Jan 16 12:20:52 2001 +0100
@@ -191,7 +191,7 @@
qed "sumhr_hypreal_of_hypnat_omega";
Goalw [hypnat_omega_def,hypnat_zero_def,omega_def]
- "sumhr(0, whn, %i. #1) = whr - #1";
+ "sumhr(0, whn, %i. #1) = omega - #1";
by (simp_tac (HOL_ss addsimps
[one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
by (auto_tac (claset(),
@@ -224,12 +224,12 @@
Goal "sumhr (0, M, f) @= sumhr (0, N, f) \
\ ==> abs (sumhr (M, N, f)) @= #0";
by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
-by (auto_tac (claset(), simpset() addsimps [inf_close_refl]));
-by (dtac (inf_close_sym RS (inf_close_minus_iff RS iffD1)) 1);
-by (auto_tac (claset() addDs [inf_close_hrabs],
+by (auto_tac (claset(), simpset() addsimps [approx_refl]));
+by (dtac (approx_sym RS (approx_minus_iff RS iffD1)) 1);
+by (auto_tac (claset() addDs [approx_hrabs],
simpset() addsimps [sumhr_split_add_minus]));
-qed "sumhr_hrabs_inf_close";
-Addsimps [sumhr_hrabs_inf_close];
+qed "sumhr_hrabs_approx";
+Addsimps [sumhr_hrabs_approx];
(*----------------------------------------------------------------
infinite sums: Standard and NS theorems
@@ -276,10 +276,10 @@
NSCauchy_NSconvergent_iff RS sym, NSCauchy_def,
starfunNat_sumr]));
by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
-by (auto_tac (claset(), simpset() addsimps [inf_close_refl]));
-by (rtac ((inf_close_minus_iff RS iffD2) RS inf_close_sym) 1);
-by (rtac (inf_close_minus_iff RS iffD2) 2);
-by (auto_tac (claset() addDs [inf_close_hrabs_zero_cancel],
+by (auto_tac (claset(), simpset() addsimps [approx_refl]));
+by (rtac ((approx_minus_iff RS iffD2) RS approx_sym) 1);
+by (rtac (approx_minus_iff RS iffD2) 2);
+by (auto_tac (claset() addDs [approx_hrabs_zero_cancel],
simpset() addsimps [sumhr_split_add_minus]));
qed "NSsummable_NSCauchy";
@@ -291,7 +291,7 @@
by (dtac bspec 1 THEN Auto_tac);
by (dres_inst_tac [("x","N + 1hn")] bspec 1);
by (auto_tac (claset() addIs [HNatInfinite_add_one,
- inf_close_hrabs_zero_cancel],
+ approx_hrabs_zero_cancel],
simpset() addsimps [rename_numerals hypreal_of_real_zero]));
qed "NSsummable_NSLIMSEQ_zero";
--- a/src/HOL/Hyperreal/HyperDef.thy Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Tue Jan 16 12:20:52 2001 +0100
@@ -29,9 +29,7 @@
consts
- "1hr" :: hypreal ("1hr")
- "whr" :: hypreal ("whr")
- "ehr" :: hypreal ("ehr")
+ "1hr" :: hypreal ("1hr")
defs
@@ -42,14 +40,6 @@
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_nat (Suc n)})"
-
- (* an infinitesimal number = [<1,1/2,1/3,...>] *)
- epsilon_def
- "ehr == Abs_hypreal(hyprel``{%n::nat. inverse (real_of_nat (Suc n))})"
-
hypreal_minus_def
"- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
@@ -68,6 +58,17 @@
hypreal_of_real :: real => hypreal
"hypreal_of_real r == Abs_hypreal(hyprel``{%n::nat. r})"
+ omega :: hypreal (*an infinite number = [<1,2,3,...>] *)
+ "omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
+
+ epsilon :: hypreal (*an infinitesimal number = [<1,1/2,1/3,...>] *)
+ "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
+
+syntax (xsymbols)
+ omega :: hypreal ("\\<omega>")
+ epsilon :: hypreal ("\\<epsilon>")
+
+
defs
hypreal_add_def
--- a/src/HOL/Hyperreal/HyperNat.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.ML Tue Jan 16 12:20:52 2001 +0100
@@ -859,64 +859,64 @@
Addsimps [hypnat_of_nat_not_eq_omega RS not_sym];
(*-----------------------------------------------------------
- Properties of the set SNat of embedded natural numbers
- (cf. set SReal in NSA.thy/NSA.ML)
+ Properties of the set Nats of embedded natural numbers
+ (cf. set Reals in NSA.thy/NSA.ML)
----------------------------------------------------------*)
-(* Infinite hypernatural not in embedded SNat *)
-Goalw [SHNat_def] "whn ~: SNat";
+(* Infinite hypernatural not in embedded Nats *)
+Goalw [SHNat_def] "whn ~: Nats";
by Auto_tac;
qed "SHNAT_omega_not_mem";
Addsimps [SHNAT_omega_not_mem];
(*-----------------------------------------------------------------------
- Closure laws for members of (embedded) set standard naturals SNat
+ Closure laws for members of (embedded) set standard naturals Nats
-----------------------------------------------------------------------*)
Goalw [SHNat_def]
- "!!x::hypnat. [| x: SNat; y: SNat |] ==> x + y: SNat";
+ "!!x::hypnat. [| x: Nats; y: Nats |] ==> x + y: Nats";
by (Step_tac 1);
by (res_inst_tac [("x","N + Na")] exI 1);
by (simp_tac (simpset() addsimps [hypnat_of_nat_add]) 1);
qed "SHNat_add";
Goalw [SHNat_def]
- "!!x::hypnat. [| x: SNat; y: SNat |] ==> x - y: SNat";
+ "!!x::hypnat. [| x: Nats; y: Nats |] ==> x - y: Nats";
by (Step_tac 1);
by (res_inst_tac [("x","N - Na")] exI 1);
by (simp_tac (simpset() addsimps [hypnat_of_nat_minus]) 1);
qed "SHNat_minus";
Goalw [SHNat_def]
- "!!x::hypnat. [| x: SNat; y: SNat |] ==> x * y: SNat";
+ "!!x::hypnat. [| x: Nats; y: Nats |] ==> x * y: Nats";
by (Step_tac 1);
by (res_inst_tac [("x","N * Na")] exI 1);
by (simp_tac (simpset() addsimps [hypnat_of_nat_mult]) 1);
qed "SHNat_mult";
-Goal"!!x::hypnat. [| x + y : SNat; y: SNat |] ==> x: SNat";
+Goal"!!x::hypnat. [| x + y : Nats; y: Nats |] ==> x: Nats";
by (dres_inst_tac [("x","x+y")] SHNat_minus 1);
by Auto_tac;
qed "SHNat_add_cancel";
-Goalw [SHNat_def] "hypnat_of_nat x : SNat";
+Goalw [SHNat_def] "hypnat_of_nat x : Nats";
by (Blast_tac 1);
qed "SHNat_hypnat_of_nat";
Addsimps [SHNat_hypnat_of_nat];
-Goal "hypnat_of_nat 1 : SNat";
+Goal "hypnat_of_nat 1 : Nats";
by (Simp_tac 1);
qed "SHNat_hypnat_of_nat_one";
-Goal "hypnat_of_nat 0 : SNat";
+Goal "hypnat_of_nat 0 : Nats";
by (Simp_tac 1);
qed "SHNat_hypnat_of_nat_zero";
-Goal "1hn : SNat";
+Goal "1hn : Nats";
by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_one,
hypnat_of_nat_one RS sym]) 1);
qed "SHNat_one";
-Goal "(0::hypnat) : SNat";
+Goal "(0::hypnat) : Nats";
by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_zero,
hypnat_of_nat_zero RS sym]) 1);
qed "SHNat_zero";
@@ -924,39 +924,39 @@
Addsimps [SHNat_hypnat_of_nat_one,SHNat_hypnat_of_nat_zero,
SHNat_one,SHNat_zero];
-Goal "1hn + 1hn : SNat";
+Goal "1hn + 1hn : Nats";
by (rtac ([SHNat_one,SHNat_one] MRS SHNat_add) 1);
qed "SHNat_two";
-Goalw [SHNat_def] "{x. hypnat_of_nat x : SNat} = (UNIV::nat set)";
+Goalw [SHNat_def] "{x. hypnat_of_nat x : Nats} = (UNIV::nat set)";
by Auto_tac;
qed "SHNat_UNIV_nat";
-Goalw [SHNat_def] "(x: SNat) = (EX y. x = hypnat_of_nat y)";
+Goalw [SHNat_def] "(x: Nats) = (EX y. x = hypnat_of_nat y)";
by Auto_tac;
qed "SHNat_iff";
-Goalw [SHNat_def] "hypnat_of_nat `(UNIV::nat set) = SNat";
+Goalw [SHNat_def] "hypnat_of_nat `(UNIV::nat set) = Nats";
by Auto_tac;
qed "hypnat_of_nat_image";
-Goalw [SHNat_def] "inv hypnat_of_nat `SNat = (UNIV::nat set)";
+Goalw [SHNat_def] "inv hypnat_of_nat `Nats = (UNIV::nat set)";
by Auto_tac;
by (rtac (inj_hypnat_of_nat RS inv_f_f RS subst) 1);
by (Blast_tac 1);
qed "inv_hypnat_of_nat_image";
Goalw [SHNat_def]
- "[| EX x. x: P; P <= SNat |] ==> EX Q. P = hypnat_of_nat ` Q";
+ "[| EX x. x: P; P <= Nats |] ==> EX Q. P = hypnat_of_nat ` Q";
by (Best_tac 1);
qed "SHNat_hypnat_of_nat_image";
Goalw [SHNat_def]
- "SNat = hypnat_of_nat ` (UNIV::nat set)";
+ "Nats = hypnat_of_nat ` (UNIV::nat set)";
by Auto_tac;
qed "SHNat_hypnat_of_nat_iff";
-Goalw [SHNat_def] "SNat <= (UNIV::hypnat set)";
+Goalw [SHNat_def] "Nats <= (UNIV::hypnat set)";
by Auto_tac;
qed "SHNat_subset_UNIV";
@@ -965,7 +965,7 @@
qed "leSuc_Un_eq";
Goal "finite {n::nat. n <= m}";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
by (auto_tac (claset(),simpset() addsimps [leSuc_Un_eq]));
qed "finite_nat_le_segment";
@@ -977,7 +977,7 @@
Addsimps [lemma_unbounded_set];
Goalw [SHNat_def,hypnat_of_nat_def, hypnat_less_def,hypnat_omega_def]
- "ALL n: SNat. n < whn";
+ "ALL n: Nats. n < whn";
by (Clarify_tac 1);
by (auto_tac (claset() addSIs [exI],simpset()));
qed "hypnat_omega_gt_SHNat";
@@ -1014,66 +1014,64 @@
qed "HNatInfinite_whn";
Addsimps [HNatInfinite_whn];
-Goalw [HNatInfinite_def] "x: SNat ==> x ~: HNatInfinite";
+Goalw [HNatInfinite_def] "x: Nats ==> x ~: HNatInfinite";
by (Simp_tac 1);
qed "SHNat_not_HNatInfinite";
-Goalw [HNatInfinite_def] "x ~: HNatInfinite ==> x: SNat";
+Goalw [HNatInfinite_def] "x ~: HNatInfinite ==> x: Nats";
by (Asm_full_simp_tac 1);
qed "not_HNatInfinite_SHNat";
-Goalw [HNatInfinite_def] "x ~: SNat ==> x: HNatInfinite";
+Goalw [HNatInfinite_def] "x ~: Nats ==> x: HNatInfinite";
by (Simp_tac 1);
qed "not_SHNat_HNatInfinite";
-Goalw [HNatInfinite_def] "x: HNatInfinite ==> x ~: SNat";
+Goalw [HNatInfinite_def] "x: HNatInfinite ==> x ~: Nats";
by (Asm_full_simp_tac 1);
qed "HNatInfinite_not_SHNat";
-Goal "(x: SNat) = (x ~: HNatInfinite)";
+Goal "(x: Nats) = (x ~: HNatInfinite)";
by (blast_tac (claset() addSIs [SHNat_not_HNatInfinite,
not_HNatInfinite_SHNat]) 1);
qed "SHNat_not_HNatInfinite_iff";
-Goal "(x ~: SNat) = (x: HNatInfinite)";
+Goal "(x ~: Nats) = (x: HNatInfinite)";
by (blast_tac (claset() addSIs [not_SHNat_HNatInfinite,
HNatInfinite_not_SHNat]) 1);
qed "not_SHNat_HNatInfinite_iff";
-Goal "x : SNat | x : HNatInfinite";
+Goal "x : Nats | x : HNatInfinite";
by (simp_tac (simpset() addsimps [SHNat_not_HNatInfinite_iff]) 1);
qed "SHNat_HNatInfinite_disj";
(*-------------------------------------------------------------------
Proof of alternative definition for set of Infinite hypernatural
- numbers --- HNatInfinite = {N. ALL n: SNat. n < N}
+ numbers --- HNatInfinite = {N. ALL n: Nats. n < N}
-------------------------------------------------------------------*)
-Goal "!!N (xa::nat=>nat). \
-\ (ALL N. {n. xa n ~= N} : FreeUltrafilterNat) ==> \
-\ ({n. N < xa n} : FreeUltrafilterNat)";
-by (nat_ind_tac "N" 1);
+Goal "ALL N::nat. {n. f n ~= N} : FreeUltrafilterNat \
+\ ==> {n. N < f n} : FreeUltrafilterNat";
+by (induct_tac "N" 1);
by (dres_inst_tac [("x","0")] spec 1);
by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1
THEN dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("x","Suc N")] spec 1);
-by (fuf_tac (claset() addSDs [Suc_leI],simpset() addsimps
- [le_eq_less_or_eq]) 1);
+by (dres_inst_tac [("x","Suc n")] spec 1);
+by (fuf_tac (claset() addSDs [Suc_leI],
+ simpset() addsimps [le_eq_less_or_eq]) 1);
qed "HNatInfinite_FreeUltrafilterNat_lemma";
(*** alternative definition ***)
Goalw [HNatInfinite_def,SHNat_def,hypnat_of_nat_def]
- "HNatInfinite = {N. ALL n:SNat. n < N}";
+ "HNatInfinite = {N. ALL n:Nats. n < N}";
by (Step_tac 1);
-by (dres_inst_tac [("x","Abs_hypnat \
-\ (hypnatrel `` {%n. N})")] bspec 2);
+by (dres_inst_tac [("x","Abs_hypnat (hypnatrel `` {%n. N})")] bspec 2);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [hypnat_less_iff]));
-by (auto_tac (claset() addSIs [exI] addEs
- [HNatInfinite_FreeUltrafilterNat_lemma],
+by (auto_tac (claset() addSIs [exI]
+ addEs [HNatInfinite_FreeUltrafilterNat_lemma],
simpset() addsimps [FreeUltrafilterNat_Compl_iff1,
- CLAIM "- {n. xa n = N} = {n. xa n ~= N}"]));
+ CLAIM "- {n. xa n = N} = {n. xa n ~= N}"]));
qed "HNatInfinite_iff";
(*--------------------------------------------------------------------
@@ -1141,14 +1139,14 @@
by (Asm_full_simp_tac 1);
qed "HNatInfinite_add";
-Goal "[| x: HNatInfinite; y: SNat |] ==> x + y: HNatInfinite";
+Goal "[| x: HNatInfinite; y: Nats |] ==> x + y: HNatInfinite";
by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
by (dres_inst_tac [("x","x + y")] SHNat_minus 1);
by (auto_tac (claset(),simpset() addsimps
[SHNat_not_HNatInfinite_iff]));
qed "HNatInfinite_SHNat_add";
-Goal "[| x: HNatInfinite; y: SNat |] ==> x - y: HNatInfinite";
+Goal "[| x: HNatInfinite; y: Nats |] ==> x - y: HNatInfinite";
by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
by (dres_inst_tac [("x","x - y")] SHNat_add 1);
by (subgoal_tac "y <= x" 2);
@@ -1222,7 +1220,7 @@
Goalw [hypreal_of_hypnat_def]
"hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) = \
-\ Abs_hypreal(hyprel `` {%n. real_of_nat (X n)})";
+\ Abs_hypreal(hyprel `` {%n. real (X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
by (auto_tac (claset()
addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
--- a/src/HOL/Hyperreal/HyperNat.thy Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Tue Jan 16 12:20:52 2001 +0100
@@ -30,26 +30,26 @@
(* hypernaturals as members of the hyperreals; the set is defined as *)
(* the nonstandard extension of set of naturals embedded in the reals *)
HNat :: "hypreal set"
- "HNat == *s* {n. EX no. n = real_of_nat no}"
+ "HNat == *s* {n. EX no::nat. n = real no}"
(* the set of infinite hypernatural numbers *)
HNatInfinite :: "hypnat set"
- "HNatInfinite == {n. n ~: SNat}"
+ "HNatInfinite == {n. n ~: Nats}"
(* explicit embedding of the hypernaturals in the hyperreals *)
hypreal_of_hypnat :: hypnat => hypreal
"hypreal_of_hypnat N == Abs_hypreal(UN X: Rep_hypnat(N).
- hyprel``{%n::nat. real_of_nat (X n)})"
+ hyprel``{%n::nat. real (X n)})"
defs
- (** the overloaded constant "SNat" **)
+ (** the overloaded constant "Nats" **)
(* set of naturals embedded in the hyperreals*)
- SNat_def "SNat == {n. EX N. n = hypreal_of_nat N}"
+ SNat_def "Nats == {n. EX N. n = hypreal_of_nat N}"
(* set of naturals embedded in the hypernaturals*)
- SHNat_def "SNat == {n. EX N. n = hypnat_of_nat N}"
+ SHNat_def "Nats == {n. EX N. n = hypnat_of_nat N}"
(** hypernatural arithmetic **)
--- a/src/HOL/Hyperreal/HyperOrd.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.ML Tue Jan 16 12:20:52 2001 +0100
@@ -386,7 +386,7 @@
Existence of infinite hyperreal number
----------------------------------------------------------------------------*)
-Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
+Goalw [omega_def] "Rep_hypreal(omega) : hypreal";
by (rtac Rep_hypreal 1);
qed "Rep_hypreal_omega";
@@ -394,24 +394,24 @@
(* use assumption that member FreeUltrafilterNat is not finite *)
(* a few lemmas first *)
-Goal "{n::nat. x = real_of_nat n} = {} | \
-\ (EX y. {n::nat. x = real_of_nat n} = {y})";
+Goal "{n::nat. x = real n} = {} | \
+\ (EX y. {n::nat. x = real n} = {y})";
by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
qed "lemma_omega_empty_singleton_disj";
-Goal "finite {n::nat. x = real_of_nat n}";
+Goal "finite {n::nat. x = real n}";
by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
by Auto_tac;
qed "lemma_finite_omega_set";
Goalw [omega_def,hypreal_of_real_def]
- "~ (EX x. hypreal_of_real x = whr)";
+ "~ (EX x. hypreal_of_real x = omega)";
by (auto_tac (claset(),
simpset() addsimps [real_of_nat_Suc, real_diff_eq_eq RS sym,
lemma_finite_omega_set RS FreeUltrafilterNat_finite]));
qed "not_ex_hypreal_of_real_eq_omega";
-Goal "hypreal_of_real x ~= whr";
+Goal "hypreal_of_real x ~= omega";
by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
by Auto_tac;
qed "hypreal_of_real_not_eq_omega";
@@ -419,39 +419,39 @@
(* existence of infinitesimal number also not *)
(* corresponding to any real number *)
-Goal "inverse (real_of_nat x) = inverse (real_of_nat y) ==> x = y";
+Goal "inverse (real (x::nat)) = inverse (real y) ==> x = y";
by (rtac (inj_real_of_nat RS injD) 1);
by (Asm_full_simp_tac 1);
qed "real_of_nat_inverse_inj";
-Goal "{n::nat. x = inverse(real_of_nat(Suc n))} = {} | \
-\ (EX y. {n::nat. x = inverse(real_of_nat(Suc n))} = {y})";
+Goal "{n::nat. x = inverse(real(Suc n))} = {} | \
+\ (EX y. {n::nat. x = inverse(real(Suc n))} = {y})";
by (auto_tac (claset(), simpset() addsimps [inj_real_of_nat RS inj_eq]));
qed "lemma_epsilon_empty_singleton_disj";
-Goal "finite {n::nat. x = inverse(real_of_nat(Suc n))}";
+Goal "finite {n. x = inverse(real(Suc n))}";
by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
by Auto_tac;
qed "lemma_finite_epsilon_set";
Goalw [epsilon_def,hypreal_of_real_def]
- "~ (EX x. hypreal_of_real x = ehr)";
+ "~ (EX x. hypreal_of_real x = epsilon)";
by (auto_tac (claset(),
simpset() addsimps [lemma_finite_epsilon_set RS FreeUltrafilterNat_finite]));
qed "not_ex_hypreal_of_real_eq_epsilon";
-Goal "hypreal_of_real x ~= ehr";
+Goal "hypreal_of_real x ~= epsilon";
by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
by Auto_tac;
qed "hypreal_of_real_not_eq_epsilon";
-Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
+Goalw [epsilon_def,hypreal_zero_def] "epsilon ~= 0";
by Auto_tac;
by (auto_tac (claset(),
simpset() addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym]));
qed "hypreal_epsilon_not_zero";
-Goal "ehr = inverse(whr)";
+Goal "epsilon = inverse(omega)";
by (asm_full_simp_tac (simpset() addsimps
[hypreal_inverse, omega_def, epsilon_def]) 1);
qed "hypreal_epsilon_inverse_omega";
--- a/src/HOL/Hyperreal/HyperPow.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML Tue Jan 16 12:20:52 2001 +0100
@@ -449,7 +449,7 @@
qed "hyperpow_less_le2";
Goal "[| #0 <= r; r < (#1::hypreal); N : HNatInfinite |] \
-\ ==> ALL n: SNat. r pow N <= r pow n";
+\ ==> ALL n: Nats. r pow N <= r pow n";
by (auto_tac (claset() addSIs [hyperpow_less_le],
simpset() addsimps [HNatInfinite_iff]));
qed "hyperpow_SHNat_le";
@@ -460,7 +460,7 @@
qed "hyperpow_realpow";
Goalw [SReal_def]
- "(hypreal_of_real r) pow (hypnat_of_nat n) : SReal";
+ "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals";
by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow]));
qed "hyperpow_SReal";
Addsimps [hyperpow_SReal];
--- a/src/HOL/Hyperreal/Lim.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Tue Jan 16 12:20:52 2001 +0100
@@ -159,7 +159,7 @@
(*--------------------------------------------------------------
Standard and NS definitions of Limit
--------------------------------------------------------------*)
-Goalw [LIM_def,NSLIM_def,inf_close_def]
+Goalw [LIM_def,NSLIM_def,approx_def]
"f -- x --> L ==> f -- x --NS> L";
by (asm_full_simp_tac
(simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1);
@@ -185,7 +185,7 @@
Goal "ALL s. #0 < s --> (EX xa. xa ~= x & \
\ abs (xa + - x) < s & r <= abs (f xa + -L)) \
\ ==> ALL n::nat. EX xa. xa ~= x & \
-\ abs(xa + -x) < inverse(real_of_nat(Suc n)) & r <= abs(f xa + -L)";
+\ abs(xa + -x) < inverse(real(Suc n)) & r <= abs(f xa + -L)";
by (Clarify_tac 1);
by (cut_inst_tac [("n1","n")]
(real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
@@ -195,16 +195,16 @@
Goal "ALL s. #0 < s --> (EX xa. xa ~= x & \
\ abs (xa + - x) < s & r <= abs (f xa + -L)) \
\ ==> EX X. ALL n::nat. X n ~= x & \
-\ abs(X n + -x) < inverse(real_of_nat(Suc n)) & r <= abs(f (X n) + -L)";
+\ abs(X n + -x) < inverse(real(Suc n)) & r <= abs(f (X n) + -L)";
by (dtac lemma_LIM 1);
by (dtac choice 1);
by (Blast_tac 1);
val lemma_skolemize_LIM2 = result();
Goal "ALL n. X n ~= x & \
-\ abs (X n + - x) < inverse (real_of_nat(Suc n)) & \
+\ abs (X n + - x) < inverse (real(Suc n)) & \
\ r <= abs (f (X n) + - L) ==> \
-\ ALL n. abs (X n + - x) < inverse (real_of_nat(Suc n))";
+\ ALL n. abs (X n + - x) < inverse (real(Suc n))";
by (Auto_tac );
val lemma_simp = result();
@@ -212,7 +212,7 @@
NSLIM => LIM
-------------------*)
-Goalw [LIM_def,NSLIM_def,inf_close_def]
+Goalw [LIM_def,NSLIM_def,approx_def]
"f -- x --NS> L ==> f -- x --> L";
by (asm_full_simp_tac
(simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1);
@@ -255,7 +255,7 @@
Goalw [NSLIM_def]
"[| f -- x --NS> l; g -- x --NS> m |] \
\ ==> (%x. f(x) * g(x)) -- x --NS> (l * m)";
-by (auto_tac (claset() addSIs [inf_close_mult_HFinite], simpset()));
+by (auto_tac (claset() addSIs [approx_mult_HFinite], simpset()));
qed "NSLIM_mult";
Goal "[| f -- x --> l; g -- x --> m |] \
@@ -270,7 +270,7 @@
Goalw [NSLIM_def]
"[| f -- x --NS> l; g -- x --NS> m |] \
\ ==> (%x. f(x) + g(x)) -- x --NS> (l + m)";
-by (auto_tac (claset() addSIs [inf_close_add], simpset()));
+by (auto_tac (claset() addSIs [approx_add], simpset()));
qed "NSLIM_add";
Goal "[| f -- x --> l; g -- x --> m |] \
@@ -326,7 +326,7 @@
by (Clarify_tac 1);
by (dtac spec 1);
by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_real_inf_close_inverse]));
+ simpset() addsimps [hypreal_of_real_approx_inverse]));
qed "NSLIM_inverse";
Goal "[| f -- a --> L; \
@@ -362,8 +362,8 @@
--------------------------*)
Goalw [NSLIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --NS> #0)";
by Auto_tac;
-by (res_inst_tac [("x","hypreal_of_real x + ehr")] exI 1);
-by (auto_tac (claset() addIs [Infinitesimal_add_inf_close_self RS inf_close_sym],
+by (res_inst_tac [("x","hypreal_of_real x + epsilon")] exI 1);
+by (auto_tac (claset() addIs [Infinitesimal_add_approx_self RS approx_sym],
simpset() addsimps [rename_numerals hypreal_epsilon_not_zero]));
qed "NSLIM_not_zero";
@@ -423,7 +423,7 @@
NSLIM_self
----------------------------*)
Goalw [NSLIM_def] "(%x. x) -- a --NS> a";
-by (auto_tac (claset() addIs [starfun_Idfun_inf_close],simpset()));
+by (auto_tac (claset() addIs [starfun_Idfun_approx],simpset()));
qed "NSLIM_self";
Goal "(%x. x) -- a --> a";
@@ -507,14 +507,14 @@
by (Step_tac 1);
by (Asm_full_simp_tac 1);
by (rtac ((mem_infmal_iff RS iffD2) RS
- (Infinitesimal_add_inf_close_self RS inf_close_sym)) 1);
-by (rtac (inf_close_minus_iff2 RS iffD1) 4);
+ (Infinitesimal_add_approx_self RS approx_sym)) 1);
+by (rtac (approx_minus_iff2 RS iffD1) 4);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 3);
by (res_inst_tac [("z","x")] eq_Abs_hypreal 2);
by (res_inst_tac [("z","x")] eq_Abs_hypreal 4);
by (auto_tac (claset(),
simpset() addsimps [starfun, hypreal_of_real_def, hypreal_minus,
- hypreal_add, real_add_assoc, inf_close_refl, hypreal_zero_def]));
+ hypreal_add, real_add_assoc, approx_refl, hypreal_zero_def]));
qed "NSLIM_h_iff";
Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- #0 --NS> f a)";
@@ -537,7 +537,7 @@
sum continuous
------------------------*)
Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a";
-by (auto_tac (claset() addIs [inf_close_add],
+by (auto_tac (claset() addIs [approx_add],
simpset() addsimps [isNSCont_isCont_iff RS sym, isNSCont_def]));
qed "isCont_add";
@@ -545,7 +545,7 @@
mult continuous
------------------------*)
Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a";
-by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],
+by (auto_tac (claset() addSIs [starfun_mult_HFinite_approx],
simpset() delsimps [starfun_mult RS sym]
addsimps [isNSCont_isCont_iff RS sym, isNSCont_def]));
qed "isCont_mult";
@@ -600,7 +600,7 @@
Addsimps [isNSCont_const];
Goalw [isNSCont_def] "isNSCont abs a";
-by (auto_tac (claset() addIs [inf_close_hrabs],
+by (auto_tac (claset() addIs [approx_hrabs],
simpset() addsimps [hypreal_of_real_hrabs RS sym,
starfun_rabs_hrabs]));
qed "isNSCont_rabs";
@@ -622,11 +622,11 @@
Goal "[| isNSopen A; ALL x. isNSCont f x |] \
\ ==> isNSopen {x. f x : A}";
by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
-by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
+by (dtac (mem_monad_approx RS approx_sym) 1);
by (dres_inst_tac [("x","a")] spec 1);
by (dtac isNSContD 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
-by (dres_inst_tac [("x","( *f* f) x")] inf_close_mem_monad2 1);
+by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1);
by (blast_tac (claset() addIs [starfun_mem_starset]) 1);
qed "isNSCont_isNSopen";
@@ -634,13 +634,13 @@
"ALL A. isNSopen A --> isNSopen {x. f x : A} \
\ ==> isNSCont f x";
by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
- (inf_close_minus_iff RS iffD2)],simpset() addsimps
+ (approx_minus_iff RS iffD2)],simpset() addsimps
[Infinitesimal_def,SReal_iff]));
by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
by (etac (isNSopen_open_interval RSN (2,impE)) 1);
by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def]));
by (dres_inst_tac [("x","x")] spec 1);
-by (auto_tac (claset() addDs [inf_close_sym RS inf_close_mem_monad],
+by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad],
simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus]));
qed "isNSopen_isNSCont";
@@ -672,7 +672,7 @@
by (Force_tac 1);
qed "isUCont_isCont";
-Goalw [isNSUCont_def,isUCont_def,inf_close_def]
+Goalw [isNSUCont_def,isUCont_def,approx_def]
"isUCont f ==> isNSUCont f";
by (asm_full_simp_tac (simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff]) 1);
@@ -693,7 +693,7 @@
Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s & r <= abs (f z + -f y)) \
\ ==> ALL n::nat. EX z y. \
-\ abs(z + -y) < inverse(real_of_nat(Suc n)) & \
+\ abs(z + -y) < inverse(real(Suc n)) & \
\ r <= abs(f z + -f y)";
by (Clarify_tac 1);
by (cut_inst_tac [("n1","n")]
@@ -703,7 +703,7 @@
Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s & r <= abs (f z + -f y)) \
\ ==> EX X Y. ALL n::nat. \
-\ abs(X n + -(Y n)) < inverse(real_of_nat(Suc n)) & \
+\ abs(X n + -(Y n)) < inverse(real(Suc n)) & \
\ r <= abs(f (X n) + -f (Y n))";
by (dtac lemma_LIMu 1);
by (dtac choice 1);
@@ -712,13 +712,13 @@
by (Blast_tac 1);
val lemma_skolemize_LIM2u = result();
-Goal "ALL n. abs (X n + -Y n) < inverse (real_of_nat(Suc n)) & \
+Goal "ALL n. abs (X n + -Y n) < inverse (real(Suc n)) & \
\ r <= abs (f (X n) + - f(Y n)) ==> \
-\ ALL n. abs (X n + - Y n) < inverse (real_of_nat(Suc n))";
+\ ALL n. abs (X n + - Y n) < inverse (real(Suc n))";
by (Auto_tac );
val lemma_simpu = result();
-Goalw [isNSUCont_def,isUCont_def,inf_close_def]
+Goalw [isNSUCont_def,isUCont_def,approx_def]
"isNSUCont f ==> isUCont f";
by (asm_full_simp_tac (simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff]) 1);
@@ -775,9 +775,9 @@
Goalw [nsderiv_def]
"[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E";
by (cut_facts_tac [Infinitesimal_epsilon, hypreal_epsilon_not_zero] 1);
-by (auto_tac (claset() addSDs [inst "x" "ehr" bspec]
+by (auto_tac (claset() addSDs [inst "x" "epsilon" bspec]
addSIs [inj_hypreal_of_real RS injD]
- addDs [inf_close_trans3],
+ addDs [approx_trans3],
simpset()));
qed "NSDeriv_unique";
@@ -874,13 +874,13 @@
by (dres_inst_tac [("x","u")] spec 1);
by Auto_tac;
by (dres_inst_tac [("c","u - hypreal_of_real x"),("b","hypreal_of_real D")]
- inf_close_mult1 1);
+ approx_mult1 1);
by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
by (subgoal_tac "(*f* (%z. z - x)) u ~= (0::hypreal)" 2);
by (rotate_tac ~1 2);
by (auto_tac (claset(),
simpset() addsimps [real_diff_def, hypreal_diff_def,
- (inf_close_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
+ (approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
Infinitesimal_subset_HFinite RS subsetD]));
qed "NSDERIVD5";
@@ -892,7 +892,7 @@
by (case_tac "h = (0::hypreal)" 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_diff_def]));
by (dres_inst_tac [("x","h")] bspec 1);
-by (dres_inst_tac [("c","h")] inf_close_mult1 2);
+by (dres_inst_tac [("c","h")] approx_mult1 2);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
simpset() addsimps [hypreal_diff_def]));
qed "NSDERIVD4";
@@ -903,7 +903,7 @@
\ hypreal_of_real (f x))@= (hypreal_of_real D) * h)";
by (auto_tac (claset(),simpset() addsimps [nsderiv_def]));
by (rtac ccontr 1 THEN dres_inst_tac [("x","h")] bspec 1);
-by (dres_inst_tac [("c","h")] inf_close_mult1 2);
+by (dres_inst_tac [("c","h")] approx_mult1 2);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
simpset() addsimps [hypreal_mult_assoc, hypreal_diff_def]));
qed "NSDERIVD3";
@@ -923,21 +923,21 @@
"NSDERIV f x :> D ==> isNSCont f x";
by (auto_tac (claset(),simpset() addsimps
[isNSCont_NSLIM_iff,NSLIM_def]));
-by (dtac (inf_close_minus_iff RS iffD1) 1);
+by (dtac (approx_minus_iff RS iffD1) 1);
by (dtac (hypreal_not_eq_minus_iff RS iffD1) 1);
by (dres_inst_tac [("x","-hypreal_of_real x + xa")] bspec 1);
by (asm_full_simp_tac (simpset() addsimps
[hypreal_add_assoc RS sym]) 2);
by (auto_tac (claset(),simpset() addsimps
[mem_infmal_iff RS sym,hypreal_add_commute]));
-by (dres_inst_tac [("c","xa + -hypreal_of_real x")] inf_close_mult1 1);
+by (dres_inst_tac [("c","xa + -hypreal_of_real x")] approx_mult1 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite
RS subsetD],simpset() addsimps [hypreal_mult_assoc]));
by (dres_inst_tac [("x3","D")] (HFinite_hypreal_of_real RSN
(2,Infinitesimal_HFinite_mult) RS (mem_infmal_iff RS iffD1)) 1);
-by (blast_tac (claset() addIs [inf_close_trans,
+by (blast_tac (claset() addIs [approx_trans,
hypreal_mult_commute RS subst,
- (inf_close_minus_iff RS iffD2)]) 1);
+ (approx_minus_iff RS iffD2)]) 1);
qed "NSDERIV_isNSCont";
(* Now Sandard proof *)
@@ -979,7 +979,7 @@
by (auto_tac (claset(),
simpset() addsimps [hypreal_add_divide_distrib]));
by (dres_inst_tac [("b","hypreal_of_real Da"),
- ("d","hypreal_of_real Db")] inf_close_add 1);
+ ("d","hypreal_of_real Db")] approx_add 1);
by (auto_tac (claset(), simpset() addsimps hypreal_add_ac));
qed "NSDERIV_add";
@@ -1024,13 +1024,13 @@
simpset() delsimps [hypreal_times_divide1_eq]
addsimps [hypreal_times_divide1_eq RS sym]));
by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1);
-by (dtac (inf_close_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4);
-by (auto_tac (claset() addSIs [inf_close_add_mono1],
+by (dtac (approx_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4);
+by (auto_tac (claset() addSIs [approx_add_mono1],
simpset() addsimps [hypreal_add_mult_distrib, hypreal_add_mult_distrib2,
hypreal_mult_commute, hypreal_add_assoc]));
by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")]
(hypreal_add_commute RS subst) 1);
-by (auto_tac (claset() addSIs [Infinitesimal_add_inf_close_self2 RS inf_close_sym,
+by (auto_tac (claset() addSIs [Infinitesimal_add_approx_self2 RS approx_sym,
Infinitesimal_add, Infinitesimal_mult,
Infinitesimal_hypreal_of_real_mult,
Infinitesimal_hypreal_of_real_mult2],
@@ -1157,7 +1157,7 @@
[Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps
[hypreal_add_mult_distrib RS sym,mem_infmal_iff RS sym]));
by (etac (Infinitesimal_subset_HFinite RS subsetD) 1);
-qed "increment_inf_close_zero";
+qed "increment_approx_zero";
(*---------------------------------------------------------------
Similarly to the above, the chain rule admits an entirely
@@ -1186,9 +1186,9 @@
by (asm_full_simp_tac (simpset() addsimps
[mem_infmal_iff RS sym]) 1);
by (rtac Infinitesimal_ratio 1);
-by (rtac inf_close_hypreal_of_real_HFinite 3);
+by (rtac approx_hypreal_of_real_HFinite 3);
by Auto_tac;
-qed "NSDERIV_inf_close";
+qed "NSDERIV_approx";
(*---------------------------------------------------------------
from one version of differentiability
@@ -1234,7 +1234,7 @@
\ ==> NSDERIV (f o g) x :> Da * Db";
by (asm_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
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 (forw_inst_tac [("f","g")] NSDERIV_approx 1);
by (auto_tac (claset(),
simpset() addsimps [starfun_lambda_cancel2, starfun_o RS sym]));
by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
@@ -1244,10 +1244,10 @@
by (res_inst_tac [("z1","(*f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"),
("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 (rtac approx_mult_hypreal_of_real 1);
by (fold_tac [hypreal_divide_def]);
by (blast_tac (claset() addIs [NSDERIVD1,
- inf_close_minus_iff RS iffD2]) 1);
+ approx_minus_iff RS iffD2]) 1);
by (blast_tac (claset() addIs [NSDERIVD2]) 1);
qed "NSDERIV_chain";
@@ -1295,7 +1295,7 @@
qed "NSDERIV_cmult_Id";
Addsimps [NSDERIV_cmult_Id];
-Goal "DERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))";
+Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
by (induct_tac "n" 1);
by (dtac (DERIV_Id RS DERIV_mult) 2);
by (auto_tac (claset(),
@@ -1307,7 +1307,7 @@
qed "DERIV_pow";
(* NS version *)
-Goal "NSDERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))";
+Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
qed "NSDERIV_pow";
@@ -1336,8 +1336,8 @@
delsimps [hypreal_minus_mult_eq1 RS sym,
hypreal_minus_mult_eq2 RS sym]) 1);
by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")]
- inf_close_trans 1);
-by (rtac inverse_add_Infinitesimal_inf_close2 1);
+ approx_trans 1);
+by (rtac inverse_add_Infinitesimal_approx2 1);
by (auto_tac (claset() addSDs [hypreal_of_real_HFinite_diff_Infinitesimal],
simpset() addsimps [hypreal_minus_inverse RS sym,
HFinite_minus_iff]));
@@ -1708,8 +1708,8 @@
(* By bisection, function continuous on closed interval is bounded above *)
(*---------------------------------------------------------------------------*)
-Goal "abs (real_of_nat x) = real_of_nat x";
-by (auto_tac (claset() addIs [abs_eqI1],simpset()));
+Goal "abs (real x) = real (x::nat)";
+by (auto_tac (claset() addIs [abs_eqI1], simpset()));
qed "abs_real_of_nat_cancel";
Addsimps [abs_real_of_nat_cancel];
--- a/src/HOL/Hyperreal/NSA.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/NSA.ML Tue Jan 16 12:20:52 2001 +0100
@@ -12,35 +12,35 @@
fun CLAIM str = CLAIM_SIMP str [];
(*--------------------------------------------------------------------
- Closure laws for members of (embedded) set standard real SReal
+ Closure laws for members of (embedded) set standard real Reals
--------------------------------------------------------------------*)
-Goalw [SReal_def] "[| (x::hypreal): SReal; y: SReal |] ==> x + y: SReal";
+Goalw [SReal_def] "[| (x::hypreal): Reals; y: Reals |] ==> x + y: Reals";
by (Step_tac 1);
by (res_inst_tac [("x","r + ra")] exI 1);
by (Simp_tac 1);
qed "SReal_add";
-Goalw [SReal_def] "[| (x::hypreal): SReal; y: SReal |] ==> x * y: SReal";
+Goalw [SReal_def] "[| (x::hypreal): Reals; y: Reals |] ==> x * y: Reals";
by (Step_tac 1);
by (res_inst_tac [("x","r * ra")] exI 1);
by (simp_tac (simpset() addsimps [hypreal_of_real_mult]) 1);
qed "SReal_mult";
-Goalw [SReal_def] "(x::hypreal): SReal ==> inverse x : SReal";
+Goalw [SReal_def] "(x::hypreal): Reals ==> inverse x : Reals";
by (blast_tac (claset() addIs [hypreal_of_real_inverse RS sym]) 1);
qed "SReal_inverse";
-Goal "[| (x::hypreal): SReal; y: SReal |] ==> x/y: SReal";
+Goal "[| (x::hypreal): Reals; y: Reals |] ==> x/y: Reals";
by (asm_simp_tac (simpset() addsimps [SReal_mult,SReal_inverse,
hypreal_divide_def]) 1);
qed "SReal_divide";
-Goalw [SReal_def] "(x::hypreal): SReal ==> -x : SReal";
+Goalw [SReal_def] "(x::hypreal): Reals ==> -x : Reals";
by (blast_tac (claset() addIs [hypreal_of_real_minus RS sym]) 1);
qed "SReal_minus";
-Goal "(-x : SReal) = ((x::hypreal): SReal)";
+Goal "(-x : Reals) = ((x::hypreal): Reals)";
by Auto_tac;
by (etac SReal_minus 2);
by (dtac SReal_minus 1);
@@ -48,68 +48,68 @@
qed "SReal_minus_iff";
Addsimps [SReal_minus_iff];
-Goal "[| (x::hypreal) + y : SReal; y: SReal |] ==> x: SReal";
+Goal "[| (x::hypreal) + y : Reals; y: Reals |] ==> x: Reals";
by (dres_inst_tac [("x","y")] SReal_minus 1);
by (dtac SReal_add 1);
by (assume_tac 1);
by Auto_tac;
qed "SReal_add_cancel";
-Goalw [SReal_def] "(x::hypreal): SReal ==> abs x : SReal";
+Goalw [SReal_def] "(x::hypreal): Reals ==> abs x : Reals";
by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_hrabs]));
qed "SReal_hrabs";
-Goalw [SReal_def] "hypreal_of_real x: SReal";
+Goalw [SReal_def] "hypreal_of_real x: Reals";
by (Blast_tac 1);
qed "SReal_hypreal_of_real";
Addsimps [SReal_hypreal_of_real];
-Goalw [hypreal_number_of_def] "(number_of w ::hypreal) : SReal";
+Goalw [hypreal_number_of_def] "(number_of w ::hypreal) : Reals";
by (rtac SReal_hypreal_of_real 1);
qed "SReal_number_of";
Addsimps [SReal_number_of];
-Goalw [hypreal_divide_def] "r : SReal ==> r/(number_of w::hypreal) : SReal";
+Goalw [hypreal_divide_def] "r : Reals ==> r/(number_of w::hypreal) : Reals";
by (blast_tac (claset() addSIs [SReal_number_of, SReal_mult,
SReal_inverse]) 1);
qed "SReal_divide_number_of";
-(* Infinitesimal ehr not in SReal *)
+(* Infinitesimal epsilon not in Reals *)
-Goalw [SReal_def] "ehr ~: SReal";
+Goalw [SReal_def] "epsilon ~: Reals";
by (auto_tac (claset(),
simpset() addsimps [hypreal_of_real_not_eq_epsilon RS not_sym]));
qed "SReal_epsilon_not_mem";
-Goalw [SReal_def] "whr ~: SReal";
+Goalw [SReal_def] "omega ~: Reals";
by (auto_tac (claset(),
simpset() addsimps [hypreal_of_real_not_eq_omega RS not_sym]));
qed "SReal_omega_not_mem";
-Goalw [SReal_def] "{x. hypreal_of_real x : SReal} = (UNIV::real set)";
+Goalw [SReal_def] "{x. hypreal_of_real x : Reals} = (UNIV::real set)";
by Auto_tac;
qed "SReal_UNIV_real";
-Goalw [SReal_def] "(x: SReal) = (EX y. x = hypreal_of_real y)";
+Goalw [SReal_def] "(x: Reals) = (EX y. x = hypreal_of_real y)";
by Auto_tac;
qed "SReal_iff";
-Goalw [SReal_def] "hypreal_of_real `(UNIV::real set) = SReal";
+Goalw [SReal_def] "hypreal_of_real `(UNIV::real set) = Reals";
by Auto_tac;
qed "hypreal_of_real_image";
-Goalw [SReal_def] "inv hypreal_of_real `SReal = (UNIV::real set)";
+Goalw [SReal_def] "inv hypreal_of_real `Reals = (UNIV::real set)";
by Auto_tac;
by (rtac (inj_hypreal_of_real RS inv_f_f RS subst) 1);
by (Blast_tac 1);
qed "inv_hypreal_of_real_image";
Goalw [SReal_def]
- "[| EX x. x: P; P <= SReal |] ==> EX Q. P = hypreal_of_real ` Q";
+ "[| EX x. x: P; P <= Reals |] ==> EX Q. P = hypreal_of_real ` Q";
by (Best_tac 1);
qed "SReal_hypreal_of_real_image";
-Goal "[| (x::hypreal): SReal; y: SReal; x<y |] ==> EX r: SReal. x<r & r<y";
+Goal "[| (x::hypreal): Reals; y: Reals; x<y |] ==> EX r: Reals. x<r & r<y";
by (auto_tac (claset(), simpset() addsimps [SReal_iff]));
by (dtac real_dense 1 THEN Step_tac 1);
by (res_inst_tac [("x","hypreal_of_real r")] bexI 1);
@@ -117,15 +117,15 @@
qed "SReal_dense";
(*------------------------------------------------------------------
- Completeness of SReal
+ Completeness of Reals
------------------------------------------------------------------*)
-Goal "P <= SReal ==> ((EX x:P. y < x) = \
+Goal "P <= Reals ==> ((EX x:P. y < x) = \
\ (EX X. hypreal_of_real X : P & y < hypreal_of_real X))";
by (blast_tac (claset() addSDs [SReal_iff RS iffD1]) 1);
by (flexflex_tac );
qed "SReal_sup_lemma";
-Goal "[| P <= SReal; EX x. x: P; EX y : SReal. ALL x: P. x < y |] \
+Goal "[| P <= Reals; EX x. x: P; EX y : Reals. ALL x: P. x < y |] \
\ ==> (EX X. X: {w. hypreal_of_real w : P}) & \
\ (EX Y. ALL X: {w. hypreal_of_real w : P}. X < Y)";
by (rtac conjI 1);
@@ -140,13 +140,13 @@
lifting of ub and property of lub
-------------------------------------------------------*)
Goalw [isUb_def,setle_def]
- "(isUb (SReal) (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
+ "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
\ (isUb (UNIV :: real set) Q Y)";
by Auto_tac;
qed "hypreal_of_real_isUb_iff";
Goalw [isLub_def,leastP_def]
- "isLub SReal (hypreal_of_real ` Q) (hypreal_of_real Y) \
+ "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y) \
\ ==> isLub (UNIV :: real set) Q Y";
by (auto_tac (claset() addIs [hypreal_of_real_isUb_iff RS iffD2],
simpset() addsimps [hypreal_of_real_isUb_iff, setge_def]));
@@ -154,7 +154,7 @@
Goalw [isLub_def,leastP_def]
"isLub (UNIV :: real set) Q Y \
-\ ==> isLub SReal (hypreal_of_real ` Q) (hypreal_of_real Y)";
+\ ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)";
by (auto_tac (claset(),
simpset() addsimps [hypreal_of_real_isUb_iff, setge_def]));
by (forw_inst_tac [("x2","x")] (isUbD2a RS (SReal_iff RS iffD1) RS exE) 1);
@@ -163,7 +163,7 @@
by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_isUb_iff]));
qed "hypreal_of_real_isLub2";
-Goal "(isLub SReal (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
+Goal "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
\ (isLub (UNIV :: real set) Q Y)";
by (blast_tac (claset() addIs [hypreal_of_real_isLub1,
hypreal_of_real_isLub2]) 1);
@@ -171,22 +171,22 @@
(* lemmas *)
Goalw [isUb_def]
- "isUb SReal P Y ==> EX Yo. isUb SReal P (hypreal_of_real Yo)";
+ "isUb Reals P Y ==> EX Yo. isUb Reals P (hypreal_of_real Yo)";
by (auto_tac (claset(), simpset() addsimps [SReal_iff]));
qed "lemma_isUb_hypreal_of_real";
Goalw [isLub_def,leastP_def,isUb_def]
- "isLub SReal P Y ==> EX Yo. isLub SReal P (hypreal_of_real Yo)";
+ "isLub Reals P Y ==> EX Yo. isLub Reals P (hypreal_of_real Yo)";
by (auto_tac (claset(), simpset() addsimps [SReal_iff]));
qed "lemma_isLub_hypreal_of_real";
Goalw [isLub_def,leastP_def,isUb_def]
- "EX Yo. isLub SReal P (hypreal_of_real Yo) ==> EX Y. isLub SReal P Y";
+ "EX Yo. isLub Reals P (hypreal_of_real Yo) ==> EX Y. isLub Reals P Y";
by Auto_tac;
qed "lemma_isLub_hypreal_of_real2";
-Goal "[| P <= SReal; EX x. x: P; EX Y. isUb SReal P Y |] \
-\ ==> EX t::hypreal. isLub SReal P t";
+Goal "[| P <= Reals; EX x. x: P; EX Y. isUb Reals P Y |] \
+\ ==> EX t::hypreal. isLub Reals P t";
by (forward_tac [SReal_hypreal_of_real_image] 1);
by (Auto_tac THEN dtac lemma_isUb_hypreal_of_real 1);
by (auto_tac (claset() addSIs [reals_complete, lemma_isLub_hypreal_of_real2],
@@ -209,7 +209,7 @@
by (Simp_tac 1);
qed "HFinite_minus_iff";
-Goalw [SReal_def,HFinite_def] "SReal <= HFinite";
+Goalw [SReal_def,HFinite_def] "Reals <= HFinite";
by Auto_tac;
by (res_inst_tac [("x","#1 + abs(hypreal_of_real r)")] exI 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_hrabs]));
@@ -224,7 +224,7 @@
Addsimps [HFinite_hypreal_of_real];
-Goalw [HFinite_def] "x : HFinite ==> EX t: SReal. abs x < t";
+Goalw [HFinite_def] "x : HFinite ==> EX t: Reals. abs x < t";
by Auto_tac;
qed "HFiniteD";
@@ -251,7 +251,7 @@
Set of infinitesimals is a subring of the hyperreals
------------------------------------------------------------------*)
Goalw [Infinitesimal_def]
- "x : Infinitesimal ==> ALL r: SReal. #0 < r --> abs x < r";
+ "x : Infinitesimal ==> ALL r: Reals. #0 < r --> abs x < r";
by Auto_tac;
qed "InfinitesimalD";
@@ -473,126 +473,126 @@
Infinitely close relation @=
----------------------------------------------------------------------*)
-Goalw [Infinitesimal_def,inf_close_def]
+Goalw [Infinitesimal_def,approx_def]
"x:Infinitesimal = (x @= #0)";
by (Simp_tac 1);
qed "mem_infmal_iff";
-Goalw [inf_close_def]" (x @= y) = (x + -y @= #0)";
+Goalw [approx_def]" (x @= y) = (x + -y @= #0)";
by (Simp_tac 1);
-qed "inf_close_minus_iff";
+qed "approx_minus_iff";
-Goalw [inf_close_def]" (x @= y) = (-y + x @= #0)";
+Goalw [approx_def]" (x @= y) = (-y + x @= #0)";
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "inf_close_minus_iff2";
+qed "approx_minus_iff2";
-Goalw [inf_close_def,Infinitesimal_def] "x @= x";
+Goalw [approx_def,Infinitesimal_def] "x @= x";
by (Simp_tac 1);
-qed "inf_close_refl";
-AddIffs [inf_close_refl];
+qed "approx_refl";
+AddIffs [approx_refl];
-Goalw [inf_close_def] "x @= y ==> y @= x";
+Goalw [approx_def] "x @= y ==> y @= x";
by (rtac (hypreal_minus_distrib1 RS subst) 1);
by (etac (Infinitesimal_minus_iff RS iffD2) 1);
-qed "inf_close_sym";
+qed "approx_sym";
-Goalw [inf_close_def] "[| x @= y; y @= z |] ==> x @= z";
+Goalw [approx_def] "[| x @= y; y @= z |] ==> x @= z";
by (dtac Infinitesimal_add 1);
by (assume_tac 1);
by Auto_tac;
-qed "inf_close_trans";
+qed "approx_trans";
Goal "[| r @= x; s @= x |] ==> r @= s";
-by (blast_tac (claset() addIs [inf_close_sym, inf_close_trans]) 1);
-qed "inf_close_trans2";
+by (blast_tac (claset() addIs [approx_sym, approx_trans]) 1);
+qed "approx_trans2";
Goal "[| x @= r; x @= s|] ==> r @= s";
-by (blast_tac (claset() addIs [inf_close_sym, inf_close_trans]) 1);
-qed "inf_close_trans3";
+by (blast_tac (claset() addIs [approx_sym, approx_trans]) 1);
+qed "approx_trans3";
Goal "(number_of w @= x) = (x @= number_of w)";
-by (blast_tac (claset() addIs [inf_close_sym]) 1);
-qed "number_of_inf_close_reorient";
-Addsimps [number_of_inf_close_reorient];
+by (blast_tac (claset() addIs [approx_sym]) 1);
+qed "number_of_approx_reorient";
+Addsimps [number_of_approx_reorient];
Goal "(x-y : Infinitesimal) = (x @= y)";
by (auto_tac (claset(),
- simpset() addsimps [hypreal_diff_def, inf_close_minus_iff RS sym,
+ simpset() addsimps [hypreal_diff_def, approx_minus_iff RS sym,
mem_infmal_iff]));
-qed "Infinitesimal_inf_close_minus";
+qed "Infinitesimal_approx_minus";
Goalw [monad_def] "(x @= y) = (monad(x)=monad(y))";
-by (auto_tac (claset() addDs [inf_close_sym]
- addSEs [inf_close_trans,equalityCE],
+by (auto_tac (claset() addDs [approx_sym]
+ addSEs [approx_trans,equalityCE],
simpset()));
-qed "inf_close_monad_iff";
+qed "approx_monad_iff";
Goal "[| x: Infinitesimal; y: Infinitesimal |] ==> x @= y";
by (asm_full_simp_tac (simpset() addsimps [mem_infmal_iff]) 1);
-by (blast_tac (claset() addIs [inf_close_trans, inf_close_sym]) 1);
-qed "Infinitesimal_inf_close";
+by (blast_tac (claset() addIs [approx_trans, approx_sym]) 1);
+qed "Infinitesimal_approx";
val prem1::prem2::rest =
-goalw thy [inf_close_def] "[| a @= b; c @= d |] ==> a+c @= b+d";
+goalw thy [approx_def] "[| a @= b; c @= d |] ==> a+c @= b+d";
by (rtac (hypreal_minus_add_distrib RS ssubst) 1);
by (rtac (hypreal_add_assoc RS ssubst) 1);
by (res_inst_tac [("y1","c")] (hypreal_add_left_commute RS subst) 1);
by (rtac (hypreal_add_assoc RS subst) 1);
by (rtac ([prem1,prem2] MRS Infinitesimal_add) 1);
-qed "inf_close_add";
+qed "approx_add";
Goal "a @= b ==> -a @= -b";
-by (rtac ((inf_close_minus_iff RS iffD2) RS inf_close_sym) 1);
-by (dtac (inf_close_minus_iff RS iffD1) 1);
+by (rtac ((approx_minus_iff RS iffD2) RS approx_sym) 1);
+by (dtac (approx_minus_iff RS iffD1) 1);
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "inf_close_minus";
+qed "approx_minus";
Goal "-a @= -b ==> a @= b";
-by (auto_tac (claset() addDs [inf_close_minus], simpset()));
-qed "inf_close_minus2";
+by (auto_tac (claset() addDs [approx_minus], simpset()));
+qed "approx_minus2";
Goal "(-a @= -b) = (a @= b)";
-by (blast_tac (claset() addIs [inf_close_minus,inf_close_minus2]) 1);
-qed "inf_close_minus_cancel";
+by (blast_tac (claset() addIs [approx_minus,approx_minus2]) 1);
+qed "approx_minus_cancel";
-Addsimps [inf_close_minus_cancel];
+Addsimps [approx_minus_cancel];
Goal "[| a @= b; c @= d |] ==> a + -c @= b + -d";
-by (blast_tac (claset() addSIs [inf_close_add,inf_close_minus]) 1);
-qed "inf_close_add_minus";
+by (blast_tac (claset() addSIs [approx_add,approx_minus]) 1);
+qed "approx_add_minus";
-Goalw [inf_close_def] "[| a @= b; c: HFinite|] ==> a*c @= b*c";
+Goalw [approx_def] "[| a @= b; c: HFinite|] ==> a*c @= b*c";
by (asm_full_simp_tac (simpset() addsimps [Infinitesimal_HFinite_mult,
hypreal_minus_mult_eq1,hypreal_add_mult_distrib RS sym]
delsimps [hypreal_minus_mult_eq1 RS sym]) 1);
-qed "inf_close_mult1";
+qed "approx_mult1";
Goal "[|a @= b; c: HFinite|] ==> c*a @= c*b";
-by (asm_simp_tac (simpset() addsimps [inf_close_mult1,hypreal_mult_commute]) 1);
-qed "inf_close_mult2";
+by (asm_simp_tac (simpset() addsimps [approx_mult1,hypreal_mult_commute]) 1);
+qed "approx_mult2";
Goal "[|u @= v*x; x @= y; v: HFinite|] ==> u @= v*y";
-by (fast_tac (claset() addIs [inf_close_mult2,inf_close_trans]) 1);
-qed "inf_close_mult_subst";
+by (fast_tac (claset() addIs [approx_mult2,approx_trans]) 1);
+qed "approx_mult_subst";
Goal "[| u @= x*v; x @= y; v: HFinite |] ==> u @= y*v";
-by (fast_tac (claset() addIs [inf_close_mult1,inf_close_trans]) 1);
-qed "inf_close_mult_subst2";
+by (fast_tac (claset() addIs [approx_mult1,approx_trans]) 1);
+qed "approx_mult_subst2";
Goal "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v";
-by (auto_tac (claset() addIs [inf_close_mult_subst2], simpset()));
-qed "inf_close_mult_subst_SReal";
+by (auto_tac (claset() addIs [approx_mult_subst2], simpset()));
+qed "approx_mult_subst_SReal";
-Goalw [inf_close_def] "a = b ==> a @= b";
+Goalw [approx_def] "a = b ==> a @= b";
by (Asm_simp_tac 1);
-qed "inf_close_eq_imp";
+qed "approx_eq_imp";
Goal "x: Infinitesimal ==> -x @= x";
by (fast_tac (HOL_cs addIs [Infinitesimal_minus_iff RS iffD2,
- mem_infmal_iff RS iffD1,inf_close_trans2]) 1);
-qed "Infinitesimal_minus_inf_close";
+ mem_infmal_iff RS iffD1,approx_trans2]) 1);
+qed "Infinitesimal_minus_approx";
-Goalw [inf_close_def] "(EX y: Infinitesimal. x + -z = y) = (x @= z)";
+Goalw [approx_def] "(EX y: Infinitesimal. x + -z = y) = (x @= z)";
by (Blast_tac 1);
qed "bex_Infinitesimal_iff";
@@ -606,75 +606,75 @@
by (dtac (Infinitesimal_minus_iff RS iffD2) 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib,
hypreal_add_assoc RS sym]));
-qed "Infinitesimal_add_inf_close";
+qed "Infinitesimal_add_approx";
Goal "y: Infinitesimal ==> x @= x + y";
by (rtac (bex_Infinitesimal_iff RS iffD1) 1);
by (dtac (Infinitesimal_minus_iff RS iffD2) 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib,
hypreal_add_assoc RS sym]));
-qed "Infinitesimal_add_inf_close_self";
+qed "Infinitesimal_add_approx_self";
Goal "y: Infinitesimal ==> x @= y + x";
-by (auto_tac (claset() addDs [Infinitesimal_add_inf_close_self],
+by (auto_tac (claset() addDs [Infinitesimal_add_approx_self],
simpset() addsimps [hypreal_add_commute]));
-qed "Infinitesimal_add_inf_close_self2";
+qed "Infinitesimal_add_approx_self2";
Goal "y: Infinitesimal ==> x @= x + -y";
-by (blast_tac (claset() addSIs [Infinitesimal_add_inf_close_self,
+by (blast_tac (claset() addSIs [Infinitesimal_add_approx_self,
Infinitesimal_minus_iff RS iffD2]) 1);
-qed "Infinitesimal_add_minus_inf_close_self";
+qed "Infinitesimal_add_minus_approx_self";
Goal "[| y: Infinitesimal; x+y @= z|] ==> x @= z";
-by (dres_inst_tac [("x","x")] (Infinitesimal_add_inf_close_self RS inf_close_sym) 1);
-by (etac (inf_close_trans3 RS inf_close_sym) 1);
+by (dres_inst_tac [("x","x")] (Infinitesimal_add_approx_self RS approx_sym) 1);
+by (etac (approx_trans3 RS approx_sym) 1);
by (assume_tac 1);
qed "Infinitesimal_add_cancel";
Goal "[| y: Infinitesimal; x @= z + y|] ==> x @= z";
-by (dres_inst_tac [("x","z")] (Infinitesimal_add_inf_close_self2 RS inf_close_sym) 1);
-by (etac (inf_close_trans3 RS inf_close_sym) 1);
+by (dres_inst_tac [("x","z")] (Infinitesimal_add_approx_self2 RS approx_sym) 1);
+by (etac (approx_trans3 RS approx_sym) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-by (etac inf_close_sym 1);
+by (etac approx_sym 1);
qed "Infinitesimal_add_right_cancel";
Goal "d + b @= d + c ==> b @= c";
-by (dtac (inf_close_minus_iff RS iffD1) 1);
+by (dtac (approx_minus_iff RS iffD1) 1);
by (asm_full_simp_tac (simpset() addsimps
- [hypreal_minus_add_distrib,inf_close_minus_iff RS sym]
+ [hypreal_minus_add_distrib,approx_minus_iff RS sym]
@ hypreal_add_ac) 1);
-qed "inf_close_add_left_cancel";
+qed "approx_add_left_cancel";
Goal "b + d @= c + d ==> b @= c";
-by (rtac inf_close_add_left_cancel 1);
+by (rtac approx_add_left_cancel 1);
by (asm_full_simp_tac (simpset() addsimps
[hypreal_add_commute]) 1);
-qed "inf_close_add_right_cancel";
+qed "approx_add_right_cancel";
Goal "b @= c ==> d + b @= d + c";
-by (rtac (inf_close_minus_iff RS iffD2) 1);
+by (rtac (approx_minus_iff RS iffD2) 1);
by (asm_full_simp_tac (simpset() addsimps
- [hypreal_minus_add_distrib,inf_close_minus_iff RS sym]
+ [hypreal_minus_add_distrib,approx_minus_iff RS sym]
@ hypreal_add_ac) 1);
-qed "inf_close_add_mono1";
+qed "approx_add_mono1";
Goal "b @= c ==> b + a @= c + a";
by (asm_simp_tac (simpset() addsimps
- [hypreal_add_commute,inf_close_add_mono1]) 1);
-qed "inf_close_add_mono2";
+ [hypreal_add_commute,approx_add_mono1]) 1);
+qed "approx_add_mono2";
Goal "(a + b @= a + c) = (b @= c)";
-by (fast_tac (claset() addEs [inf_close_add_left_cancel,
- inf_close_add_mono1]) 1);
-qed "inf_close_add_left_iff";
+by (fast_tac (claset() addEs [approx_add_left_cancel,
+ approx_add_mono1]) 1);
+qed "approx_add_left_iff";
-Addsimps [inf_close_add_left_iff];
+Addsimps [approx_add_left_iff];
Goal "(b + a @= c + a) = (b @= c)";
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "inf_close_add_right_iff";
+qed "approx_add_right_iff";
-Addsimps [inf_close_add_right_iff];
+Addsimps [approx_add_right_iff];
Goal "[| x: HFinite; x @= y |] ==> y: HFinite";
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
@@ -683,61 +683,61 @@
RS (HFinite_minus_iff RS iffD2)) 1);
by (dtac HFinite_add 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
-qed "inf_close_HFinite";
+qed "approx_HFinite";
Goal "x @= hypreal_of_real D ==> x: HFinite";
-by (rtac (inf_close_sym RSN (2,inf_close_HFinite)) 1);
+by (rtac (approx_sym RSN (2,approx_HFinite)) 1);
by Auto_tac;
-qed "inf_close_hypreal_of_real_HFinite";
+qed "approx_hypreal_of_real_HFinite";
Goal "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d";
-by (rtac inf_close_trans 1);
-by (rtac inf_close_mult2 2);
-by (rtac inf_close_mult1 1);
-by (blast_tac (claset() addIs [inf_close_HFinite, inf_close_sym]) 2);
+by (rtac approx_trans 1);
+by (rtac approx_mult2 2);
+by (rtac approx_mult1 1);
+by (blast_tac (claset() addIs [approx_HFinite, approx_sym]) 2);
by Auto_tac;
-qed "inf_close_mult_HFinite";
+qed "approx_mult_HFinite";
Goal "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] \
\ ==> a*c @= hypreal_of_real b*hypreal_of_real d";
-by (blast_tac (claset() addSIs [inf_close_mult_HFinite,
- inf_close_hypreal_of_real_HFinite,HFinite_hypreal_of_real]) 1);
-qed "inf_close_mult_hypreal_of_real";
+by (blast_tac (claset() addSIs [approx_mult_HFinite,
+ approx_hypreal_of_real_HFinite,HFinite_hypreal_of_real]) 1);
+qed "approx_mult_hypreal_of_real";
-Goal "[| a: SReal; a ~= #0; a*x @= #0 |] ==> x @= #0";
+Goal "[| a: Reals; a ~= #0; a*x @= #0 |] ==> x @= #0";
by (dtac (SReal_inverse RS (SReal_subset_HFinite RS subsetD)) 1);
-by (auto_tac (claset() addDs [inf_close_mult2],
+by (auto_tac (claset() addDs [approx_mult2],
simpset() addsimps [hypreal_mult_assoc RS sym]));
-qed "inf_close_SReal_mult_cancel_zero";
+qed "approx_SReal_mult_cancel_zero";
(* REM comments: newly added *)
-Goal "[| a: SReal; x @= #0 |] ==> x*a @= #0";
+Goal "[| a: Reals; x @= #0 |] ==> x*a @= #0";
by (auto_tac (claset() addDs [(SReal_subset_HFinite RS subsetD),
- inf_close_mult1], simpset()));
-qed "inf_close_mult_SReal1";
+ approx_mult1], simpset()));
+qed "approx_mult_SReal1";
-Goal "[| a: SReal; x @= #0 |] ==> a*x @= #0";
+Goal "[| a: Reals; x @= #0 |] ==> a*x @= #0";
by (auto_tac (claset() addDs [(SReal_subset_HFinite RS subsetD),
- inf_close_mult2], simpset()));
-qed "inf_close_mult_SReal2";
+ approx_mult2], simpset()));
+qed "approx_mult_SReal2";
-Goal "[|a : SReal; a ~= #0 |] ==> (a*x @= #0) = (x @= #0)";
-by (blast_tac (claset() addIs [inf_close_SReal_mult_cancel_zero,
- inf_close_mult_SReal2]) 1);
-qed "inf_close_mult_SReal_zero_cancel_iff";
-Addsimps [inf_close_mult_SReal_zero_cancel_iff];
+Goal "[|a : Reals; a ~= #0 |] ==> (a*x @= #0) = (x @= #0)";
+by (blast_tac (claset() addIs [approx_SReal_mult_cancel_zero,
+ approx_mult_SReal2]) 1);
+qed "approx_mult_SReal_zero_cancel_iff";
+Addsimps [approx_mult_SReal_zero_cancel_iff];
-Goal "[| a: SReal; a ~= #0; a* w @= a*z |] ==> w @= z";
+Goal "[| a: Reals; a ~= #0; a* w @= a*z |] ==> w @= z";
by (dtac (SReal_inverse RS (SReal_subset_HFinite RS subsetD)) 1);
-by (auto_tac (claset() addDs [inf_close_mult2],
+by (auto_tac (claset() addDs [approx_mult2],
simpset() addsimps [hypreal_mult_assoc RS sym]));
-qed "inf_close_SReal_mult_cancel";
+qed "approx_SReal_mult_cancel";
-Goal "[| a: SReal; a ~= #0|] ==> (a* w @= a*z) = (w @= z)";
-by (auto_tac (claset() addSIs [inf_close_mult2,SReal_subset_HFinite RS subsetD]
- addIs [inf_close_SReal_mult_cancel], simpset()));
-qed "inf_close_SReal_mult_cancel_iff1";
-Addsimps [inf_close_SReal_mult_cancel_iff1];
+Goal "[| a: Reals; a ~= #0|] ==> (a* w @= a*z) = (w @= z)";
+by (auto_tac (claset() addSIs [approx_mult2,SReal_subset_HFinite RS subsetD]
+ addIs [approx_SReal_mult_cancel], simpset()));
+qed "approx_SReal_mult_cancel_iff1";
+Addsimps [approx_SReal_mult_cancel_iff1];
Goal "[| z <= f; f @= g; g <= z |] ==> f @= z";
by (asm_full_simp_tac (simpset() addsimps [bex_Infinitesimal_iff2 RS sym]) 1);
@@ -747,46 +747,46 @@
by (rtac Infinitesimal_interval2 1);
by (rtac Infinitesimal_zero 2);
by Auto_tac;
-qed "inf_close_le_bound";
+qed "approx_le_bound";
(*-----------------------------------------------------------------
Zero is the only infinitesimal that is also a real
-----------------------------------------------------------------*)
Goalw [Infinitesimal_def]
- "[| x: SReal; y: Infinitesimal; #0 < x |] ==> y < x";
+ "[| x: Reals; y: Infinitesimal; #0 < x |] ==> y < x";
by (rtac (hrabs_ge_self RS order_le_less_trans) 1);
by Auto_tac;
qed "Infinitesimal_less_SReal";
-Goal "y: Infinitesimal ==> ALL r: SReal. #0 < r --> y < r";
+Goal "y: Infinitesimal ==> ALL r: Reals. #0 < r --> y < r";
by (blast_tac (claset() addIs [Infinitesimal_less_SReal]) 1);
qed "Infinitesimal_less_SReal2";
Goalw [Infinitesimal_def]
- "[| #0 < y; y: SReal|] ==> y ~: Infinitesimal";
+ "[| #0 < y; y: Reals|] ==> y ~: Infinitesimal";
by (auto_tac (claset(), simpset() addsimps [hrabs_def]));
qed "SReal_not_Infinitesimal";
-Goal "[| y < #0; y : SReal |] ==> y ~: Infinitesimal";
+Goal "[| y < #0; y : Reals |] ==> y ~: Infinitesimal";
by (stac (Infinitesimal_minus_iff RS sym) 1);
by (rtac SReal_not_Infinitesimal 1);
by Auto_tac;
qed "SReal_minus_not_Infinitesimal";
-Goal "SReal Int Infinitesimal = {#0}";
+Goal "Reals Int Infinitesimal = {#0}";
by Auto_tac;
by (cut_inst_tac [("x","x"),("y","#0")] hypreal_linear 1);
by (blast_tac (claset() addDs [SReal_not_Infinitesimal,
SReal_minus_not_Infinitesimal]) 1);
qed "SReal_Int_Infinitesimal_zero";
-Goal "[| x: SReal; x: Infinitesimal|] ==> x = #0";
+Goal "[| x: Reals; x: Infinitesimal|] ==> x = #0";
by (cut_facts_tac [SReal_Int_Infinitesimal_zero] 1);
by (Blast_tac 1);
qed "SReal_Infinitesimal_zero";
-Goal "[| x : SReal; x ~= #0 |] ==> x : HFinite - Infinitesimal";
+Goal "[| x : Reals; x ~= #0 |] ==> x : HFinite - Infinitesimal";
by (auto_tac (claset() addDs [SReal_Infinitesimal_zero,
SReal_subset_HFinite RS subsetD],
simpset()));
@@ -810,21 +810,21 @@
qed "number_of_not_Infinitesimal";
Addsimps [number_of_not_Infinitesimal];
-Goal "[| y: SReal; x @= y; y~= #0 |] ==> x ~= #0";
+Goal "[| y: Reals; x @= y; y~= #0 |] ==> x ~= #0";
by (cut_inst_tac [("x","y")] hypreal_trichotomy 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addDs
- [inf_close_sym RS (mem_infmal_iff RS iffD2),
+ [approx_sym RS (mem_infmal_iff RS iffD2),
SReal_not_Infinitesimal, SReal_minus_not_Infinitesimal]) 1);
-qed "inf_close_SReal_not_zero";
+qed "approx_SReal_not_zero";
Goal "[| x @= y; y : HFinite - Infinitesimal |] \
\ ==> x : HFinite - Infinitesimal";
-by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
+by (auto_tac (claset() addIs [approx_sym RSN (2,approx_HFinite)],
simpset() addsimps [mem_infmal_iff]));
-by (dtac inf_close_trans3 1 THEN assume_tac 1);
-by (blast_tac (claset() addDs [inf_close_sym]) 1);
-qed "HFinite_diff_Infinitesimal_inf_close";
+by (dtac approx_trans3 1 THEN assume_tac 1);
+by (blast_tac (claset() addDs [approx_sym]) 1);
+qed "HFinite_diff_Infinitesimal_approx";
(*The premise y~=0 is essential; otherwise x/y =0 and we lose the
HFinite premise.*)
@@ -837,46 +837,46 @@
(*------------------------------------------------------------------
Standard Part Theorem: Every finite x: R* is infinitely
- close to a unique real number (i.e a member of SReal)
+ close to a unique real number (i.e a member of Reals)
------------------------------------------------------------------*)
(*------------------------------------------------------------------
Uniqueness: Two infinitely close reals are equal
------------------------------------------------------------------*)
-Goal "[|x: SReal; y: SReal|] ==> (x @= y) = (x = y)";
+Goal "[|x: Reals; y: Reals|] ==> (x @= y) = (x = y)";
by Auto_tac;
-by (rewrite_goals_tac [inf_close_def]);
+by (rewrite_goals_tac [approx_def]);
by (dres_inst_tac [("x","y")] SReal_minus 1);
by (dtac SReal_add 1 THEN assume_tac 1);
by (dtac SReal_Infinitesimal_zero 1 THEN assume_tac 1);
by (dtac sym 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff RS sym]) 1);
-qed "SReal_inf_close_iff";
+qed "SReal_approx_iff";
Goal "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))";
-by (rtac SReal_inf_close_iff 1);
+by (rtac SReal_approx_iff 1);
by Auto_tac;
-qed "number_of_inf_close_iff";
-Addsimps [number_of_inf_close_iff];
+qed "number_of_approx_iff";
+Addsimps [number_of_approx_iff];
Goal "(hypreal_of_real k @= hypreal_of_real m) = (k = m)";
by Auto_tac;
by (rtac (inj_hypreal_of_real RS injD) 1);
-by (rtac (SReal_inf_close_iff RS iffD1) 1);
+by (rtac (SReal_approx_iff RS iffD1) 1);
by Auto_tac;
-qed "hypreal_of_real_inf_close_iff";
-Addsimps [hypreal_of_real_inf_close_iff];
+qed "hypreal_of_real_approx_iff";
+Addsimps [hypreal_of_real_approx_iff];
Goal "(hypreal_of_real k @= number_of w) = (k = number_of w)";
-by (stac (hypreal_of_real_inf_close_iff RS sym) 1);
+by (stac (hypreal_of_real_approx_iff RS sym) 1);
by Auto_tac;
-qed "hypreal_of_real_inf_close_number_of_iff";
-Addsimps [hypreal_of_real_inf_close_number_of_iff];
+qed "hypreal_of_real_approx_number_of_iff";
+Addsimps [hypreal_of_real_approx_number_of_iff];
-Goal "[| r: SReal; s: SReal; r @= x; s @= x|] ==> r = s";
-by (blast_tac (claset() addIs [(SReal_inf_close_iff RS iffD1),
- inf_close_trans2]) 1);
-qed "inf_close_unique_real";
+Goal "[| r: Reals; s: Reals; r @= x; s @= x|] ==> r = s";
+by (blast_tac (claset() addIs [(SReal_approx_iff RS iffD1),
+ approx_trans2]) 1);
+qed "approx_unique_real";
(*------------------------------------------------------------------
Existence of unique real infinitely close
@@ -889,25 +889,25 @@
addSDs [isLub_le_isUb]) 1);
qed "hypreal_isLub_unique";
-Goal "x: HFinite ==> EX u. isUb SReal {s. s: SReal & s < x} u";
+Goal "x: HFinite ==> EX u. isUb Reals {s. s: Reals & s < x} u";
by (dtac HFiniteD 1 THEN Step_tac 1);
by (rtac exI 1 THEN rtac isUbI 1 THEN assume_tac 2);
by (auto_tac (claset() addIs [order_less_imp_le,setleI,isUbI,
order_less_trans], simpset() addsimps [hrabs_interval_iff]));
qed "lemma_st_part_ub";
-Goal "x: HFinite ==> EX y. y: {s. s: SReal & s < x}";
+Goal "x: HFinite ==> EX y. y: {s. s: Reals & s < x}";
by (dtac HFiniteD 1 THEN Step_tac 1);
by (dtac SReal_minus 1);
by (res_inst_tac [("x","-t")] exI 1);
by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
qed "lemma_st_part_nonempty";
-Goal "{s. s: SReal & s < x} <= SReal";
+Goal "{s. s: Reals & s < x} <= Reals";
by Auto_tac;
qed "lemma_st_part_subset";
-Goal "x: HFinite ==> EX t. isLub SReal {s. s: SReal & s < x} t";
+Goal "x: HFinite ==> EX t. isLub Reals {s. s: Reals & s < x} t";
by (blast_tac (claset() addSIs [SReal_complete,lemma_st_part_ub,
lemma_st_part_nonempty, lemma_st_part_subset]) 1);
qed "lemma_st_part_lub";
@@ -919,8 +919,8 @@
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc RS sym]));
qed "lemma_hypreal_le_left_cancel";
-Goal "[| x: HFinite; isLub SReal {s. s: SReal & s < x} t; \
-\ r: SReal; #0 < r |] ==> x <= t + r";
+Goal "[| x: HFinite; isLub Reals {s. s: Reals & s < x} t; \
+\ r: Reals; #0 < r |] ==> x <= t + r";
by (forward_tac [isLubD1a] 1);
by (rtac ccontr 1 THEN dtac (linorder_not_le RS iffD2) 1);
by (dres_inst_tac [("x","t")] SReal_add 1 THEN assume_tac 1);
@@ -939,8 +939,8 @@
by (blast_tac (claset() addIs [hypreal_setle_less_trans]) 1);
qed "hypreal_gt_isUb";
-Goal "[| x: HFinite; x < y; y: SReal |] \
-\ ==> isUb SReal {s. s: SReal & s < x} y";
+Goal "[| x: HFinite; x < y; y: Reals |] \
+\ ==> isUb Reals {s. s: Reals & s < x} y";
by (auto_tac (claset() addDs [order_less_trans]
addIs [order_less_imp_le] addSIs [isUbI,setleI], simpset()));
qed "lemma_st_part_gt_ub";
@@ -951,8 +951,8 @@
qed "lemma_minus_le_zero";
Goal "[| x: HFinite; \
-\ isLub SReal {s. s: SReal & s < x} t; \
-\ r: SReal; #0 < r |] \
+\ isLub Reals {s. s: Reals & s < x} t; \
+\ r: Reals; #0 < r |] \
\ ==> t + -r <= x";
by (forward_tac [isLubD1a] 1);
by (rtac ccontr 1 THEN dtac not_hypreal_leE 1);
@@ -969,8 +969,8 @@
qed "lemma_hypreal_le_swap";
Goal "[| x: HFinite; \
-\ isLub SReal {s. s: SReal & s < x} t; \
-\ r: SReal; #0 < r |] \
+\ isLub Reals {s. s: Reals & s < x} t; \
+\ r: Reals; #0 < r |] \
\ ==> x + -t <= r";
by (blast_tac (claset() addSIs [lemma_hypreal_le_swap RS iffD1,
lemma_st_part_le1]) 1);
@@ -981,18 +981,18 @@
qed "lemma_hypreal_le_swap2";
Goal "[| x: HFinite; \
-\ isLub SReal {s. s: SReal & s < x} t; \
-\ r: SReal; #0 < r |] \
+\ isLub Reals {s. s: Reals & s < x} t; \
+\ r: Reals; #0 < r |] \
\ ==> -(x + -t) <= r";
by (blast_tac (claset() addSIs [lemma_hypreal_le_swap2 RS iffD1,
lemma_st_part_le2]) 1);
qed "lemma_st_part2a";
-Goal "(x::hypreal): SReal ==> isUb SReal {s. s: SReal & s < x} x";
+Goal "(x::hypreal): Reals ==> isUb Reals {s. s: Reals & s < x} x";
by (auto_tac (claset() addIs [isUbI, setleI,order_less_imp_le], simpset()));
qed "lemma_SReal_ub";
-Goal "(x::hypreal): SReal ==> isLub SReal {s. s: SReal & s < x} x";
+Goal "(x::hypreal): Reals ==> isLub Reals {s. s: Reals & s < x} x";
by (auto_tac (claset() addSIs [isLubI2,lemma_SReal_ub,setgeI], simpset()));
by (forward_tac [isUbD2a] 1);
by (res_inst_tac [("x","x"),("y","y")] hypreal_linear_less2 1);
@@ -1003,8 +1003,8 @@
qed "lemma_SReal_lub";
Goal "[| x: HFinite; \
-\ isLub SReal {s. s: SReal & s < x} t; \
-\ r: SReal; #0 < r |] \
+\ isLub Reals {s. s: Reals & s < x} t; \
+\ r: Reals; #0 < r |] \
\ ==> x + -t ~= r";
by Auto_tac;
by (forward_tac [isLubD1a RS SReal_minus] 1);
@@ -1015,8 +1015,8 @@
qed "lemma_st_part_not_eq1";
Goal "[| x: HFinite; \
-\ isLub SReal {s. s: SReal & s < x} t; \
-\ r: SReal; #0 < r |] \
+\ isLub Reals {s. s: Reals & s < x} t; \
+\ r: Reals; #0 < r |] \
\ ==> -(x + -t) ~= r";
by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib]));
by (forward_tac [isLubD1a] 1);
@@ -1029,8 +1029,8 @@
qed "lemma_st_part_not_eq2";
Goal "[| x: HFinite; \
-\ isLub SReal {s. s: SReal & s < x} t; \
-\ r: SReal; #0 < r |] \
+\ isLub Reals {s. s: Reals & s < x} t; \
+\ r: Reals; #0 < r |] \
\ ==> abs (x + -t) < r";
by (forward_tac [lemma_st_part1a] 1);
by (forward_tac [lemma_st_part2a] 4);
@@ -1041,8 +1041,8 @@
qed "lemma_st_part_major";
Goal "[| x: HFinite; \
-\ isLub SReal {s. s: SReal & s < x} t |] \
-\ ==> ALL r: SReal. #0 < r --> abs (x + -t) < r";
+\ isLub Reals {s. s: Reals & s < x} t |] \
+\ ==> ALL r: Reals. #0 < r --> abs (x + -t) < r";
by (blast_tac (claset() addSDs [lemma_st_part_major]) 1);
qed "lemma_st_part_major2";
@@ -1050,14 +1050,14 @@
Existence of real and Standard Part Theorem
----------------------------------------------*)
Goal "x: HFinite ==> \
-\ EX t: SReal. ALL r: SReal. #0 < r --> abs (x + -t) < r";
+\ EX t: Reals. ALL r: Reals. #0 < r --> abs (x + -t) < r";
by (forward_tac [lemma_st_part_lub] 1 THEN Step_tac 1);
by (forward_tac [isLubD1a] 1);
by (blast_tac (claset() addDs [lemma_st_part_major2]) 1);
qed "lemma_st_part_Ex";
-Goalw [inf_close_def,Infinitesimal_def]
- "x:HFinite ==> EX t: SReal. x @= t";
+Goalw [approx_def,Infinitesimal_def]
+ "x:HFinite ==> EX t: Reals. x @= t";
by (dtac lemma_st_part_Ex 1);
by Auto_tac;
qed "st_part_Ex";
@@ -1065,11 +1065,11 @@
(*--------------------------------
Unique real infinitely close
-------------------------------*)
-Goal "x:HFinite ==> EX! t. t: SReal & x @= t";
+Goal "x:HFinite ==> EX! t. t: Reals & x @= t";
by (dtac st_part_Ex 1 THEN Step_tac 1);
-by (dtac inf_close_sym 2 THEN dtac inf_close_sym 2
- THEN dtac inf_close_sym 2);
-by (auto_tac (claset() addSIs [inf_close_unique_real], simpset()));
+by (dtac approx_sym 2 THEN dtac approx_sym 2
+ THEN dtac approx_sym 2);
+by (auto_tac (claset() addSIs [approx_unique_real], simpset()));
qed "st_part_Ex1";
(*------------------------------------------------------------------
@@ -1141,43 +1141,43 @@
Goal "[| x @= y; y : HFinite - Infinitesimal |] \
\ ==> inverse x @= inverse y";
-by (forward_tac [HFinite_diff_Infinitesimal_inf_close] 1);
+by (forward_tac [HFinite_diff_Infinitesimal_approx] 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_inverse2 1));
-by (dtac inf_close_mult2 1 THEN assume_tac 1);
+by (dtac approx_mult2 1 THEN assume_tac 1);
by Auto_tac;
-by (dres_inst_tac [("c","inverse x")] inf_close_mult1 1
+by (dres_inst_tac [("c","inverse x")] approx_mult1 1
THEN assume_tac 1);
-by (auto_tac (claset() addIs [inf_close_sym],
+by (auto_tac (claset() addIs [approx_sym],
simpset() addsimps [hypreal_mult_assoc]));
-qed "inf_close_inverse";
+qed "approx_inverse";
(*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
-bind_thm ("hypreal_of_real_inf_close_inverse",
- hypreal_of_real_HFinite_diff_Infinitesimal RSN (2, inf_close_inverse));
+bind_thm ("hypreal_of_real_approx_inverse",
+ hypreal_of_real_HFinite_diff_Infinitesimal RSN (2, approx_inverse));
Goal "[| x: HFinite - Infinitesimal; \
\ h : Infinitesimal |] ==> inverse(x + h) @= inverse x";
-by (auto_tac (claset() addIs [inf_close_inverse, inf_close_sym,
- Infinitesimal_add_inf_close_self],
+by (auto_tac (claset() addIs [approx_inverse, approx_sym,
+ Infinitesimal_add_approx_self],
simpset()));
-qed "inverse_add_Infinitesimal_inf_close";
+qed "inverse_add_Infinitesimal_approx";
Goal "[| x: HFinite - Infinitesimal; \
\ h : Infinitesimal |] ==> inverse(h + x) @= inverse x";
by (rtac (hypreal_add_commute RS subst) 1);
-by (blast_tac (claset() addIs [inverse_add_Infinitesimal_inf_close]) 1);
-qed "inverse_add_Infinitesimal_inf_close2";
+by (blast_tac (claset() addIs [inverse_add_Infinitesimal_approx]) 1);
+qed "inverse_add_Infinitesimal_approx2";
Goal "[| x : HFinite - Infinitesimal; \
\ h : Infinitesimal |] ==> inverse(x + h) + -inverse x @= h";
-by (rtac inf_close_trans2 1);
-by (auto_tac (claset() addIs [inverse_add_Infinitesimal_inf_close],
+by (rtac approx_trans2 1);
+by (auto_tac (claset() addIs [inverse_add_Infinitesimal_approx],
simpset() addsimps [mem_infmal_iff,
- inf_close_minus_iff RS sym]));
-qed "inverse_add_Infinitesimal_inf_close_Infinitesimal";
+ approx_minus_iff RS sym]));
+qed "inverse_add_Infinitesimal_approx_Infinitesimal";
Goal "(x : Infinitesimal) = (x*x : Infinitesimal)";
by (auto_tac (claset() addIs [Infinitesimal_mult], simpset()));
@@ -1205,14 +1205,14 @@
by (Step_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],
+by (auto_tac (claset() addDs [approx_mult2],
simpset() addsimps [hypreal_mult_assoc RS sym]));
-qed "inf_close_HFinite_mult_cancel";
+qed "approx_HFinite_mult_cancel";
Goal "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)";
-by (auto_tac (claset() addIs [inf_close_mult2,
- inf_close_HFinite_mult_cancel], simpset()));
-qed "inf_close_HFinite_mult_cancel_iff1";
+by (auto_tac (claset() addIs [approx_mult2,
+ approx_HFinite_mult_cancel], simpset()));
+qed "approx_HFinite_mult_cancel_iff1";
(*------------------------------------------------------------------
more about absolute value (hrabs)
@@ -1221,7 +1221,7 @@
Goal "abs x @= x | abs x @= -x";
by (cut_inst_tac [("x","x")] hrabs_disj 1);
by Auto_tac;
-qed "inf_close_hrabs_disj";
+qed "approx_hrabs_disj";
(*------------------------------------------------------------------
Theorems about monads
@@ -1233,8 +1233,8 @@
qed "monad_hrabs_Un_subset";
Goal "e : Infinitesimal ==> monad (x+e) = monad x";
-by (fast_tac (claset() addSIs [Infinitesimal_add_inf_close_self RS inf_close_sym,
- inf_close_monad_iff RS iffD1]) 1);
+by (fast_tac (claset() addSIs [Infinitesimal_add_approx_self RS approx_sym,
+ approx_monad_iff RS iffD1]) 1);
qed "Infinitesimal_monad_eq";
Goalw [monad_def] "(u:monad x) = (-u:monad (-x))";
@@ -1242,7 +1242,7 @@
qed "mem_monad_iff";
Goalw [monad_def] "(x:Infinitesimal) = (x:monad #0)";
-by (auto_tac (claset() addIs [inf_close_sym],
+by (auto_tac (claset() addIs [approx_sym],
simpset() addsimps [mem_infmal_iff]));
qed "Infinitesimal_monad_zero_iff";
@@ -1266,36 +1266,36 @@
Goal "x @= y ==> {x,y}<=monad x";
by (Simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps
- [inf_close_monad_iff]) 1);
-qed "inf_close_subset_monad";
+ [approx_monad_iff]) 1);
+qed "approx_subset_monad";
Goal "x @= y ==> {x,y}<=monad y";
-by (dtac inf_close_sym 1);
-by (fast_tac (claset() addDs [inf_close_subset_monad]) 1);
-qed "inf_close_subset_monad2";
+by (dtac approx_sym 1);
+by (fast_tac (claset() addDs [approx_subset_monad]) 1);
+qed "approx_subset_monad2";
Goalw [monad_def] "u:monad x ==> x @= u";
by (Fast_tac 1);
-qed "mem_monad_inf_close";
+qed "mem_monad_approx";
Goalw [monad_def] "x @= u ==> u:monad x";
by (Fast_tac 1);
-qed "inf_close_mem_monad";
+qed "approx_mem_monad";
Goalw [monad_def] "x @= u ==> x:monad u";
-by (blast_tac (claset() addSIs [inf_close_sym]) 1);
-qed "inf_close_mem_monad2";
+by (blast_tac (claset() addSIs [approx_sym]) 1);
+qed "approx_mem_monad2";
Goal "[| x @= y;x:monad #0 |] ==> y:monad #0";
-by (dtac mem_monad_inf_close 1);
-by (fast_tac (claset() addIs [inf_close_mem_monad,inf_close_trans]) 1);
-qed "inf_close_mem_monad_zero";
+by (dtac mem_monad_approx 1);
+by (fast_tac (claset() addIs [approx_mem_monad,approx_trans]) 1);
+qed "approx_mem_monad_zero";
Goal "[| x @= y; x: Infinitesimal |] ==> abs x @= abs y";
by (dtac (Infinitesimal_monad_zero_iff RS iffD1) 1);
-by (blast_tac (claset() addIs [inf_close_mem_monad_zero,
- monad_zero_hrabs_iff RS iffD1, mem_monad_inf_close, inf_close_trans3]) 1);
-qed "Infinitesimal_inf_close_hrabs";
+by (blast_tac (claset() addIs [approx_mem_monad_zero,
+ monad_zero_hrabs_iff RS iffD1, mem_monad_approx, approx_trans3]) 1);
+qed "Infinitesimal_approx_hrabs";
Goal "[| #0 < x; x ~:Infinitesimal; e :Infinitesimal |] ==> e < x";
by (rtac ccontr 1);
@@ -1306,14 +1306,14 @@
qed "less_Infinitesimal_less";
Goal "[| #0 < x; x ~: Infinitesimal; u: monad x |] ==> #0 < u";
-by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
+by (dtac (mem_monad_approx RS approx_sym) 1);
by (etac (bex_Infinitesimal_iff2 RS iffD2 RS bexE) 1);
by (dres_inst_tac [("e","-xa")] less_Infinitesimal_less 1);
by Auto_tac;
qed "Ball_mem_monad_gt_zero";
Goal "[| x < #0; x ~: Infinitesimal; u: monad x |] ==> u < #0";
-by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
+by (dtac (mem_monad_approx RS approx_sym) 1);
by (etac (bex_Infinitesimal_iff RS iffD2 RS bexE) 1);
by (cut_inst_tac [("x","-x"),("e","xa")] less_Infinitesimal_less 1);
by Auto_tac;
@@ -1321,62 +1321,62 @@
Goal "[|#0 < x; x ~: Infinitesimal; x @= y|] ==> #0 < y";
by (blast_tac (claset() addDs [Ball_mem_monad_gt_zero,
- inf_close_subset_monad]) 1);
-qed "lemma_inf_close_gt_zero";
+ approx_subset_monad]) 1);
+qed "lemma_approx_gt_zero";
Goal "[|x < #0; x ~: Infinitesimal; x @= y|] ==> y < #0";
by (blast_tac (claset() addDs [Ball_mem_monad_less_zero,
- inf_close_subset_monad]) 1);
-qed "lemma_inf_close_less_zero";
+ approx_subset_monad]) 1);
+qed "lemma_approx_less_zero";
Goal "[| x @= y; x < #0; x ~: Infinitesimal |] ==> abs x @= abs y";
-by (forward_tac [lemma_inf_close_less_zero] 1);
+by (forward_tac [lemma_approx_less_zero] 1);
by (REPEAT(assume_tac 1));
by (REPEAT(dtac hrabs_minus_eqI2 1));
by Auto_tac;
-qed "inf_close_hrabs1";
+qed "approx_hrabs1";
Goal "[| x @= y; #0 < x; x ~: Infinitesimal |] ==> abs x @= abs y";
-by (forward_tac [lemma_inf_close_gt_zero] 1);
+by (forward_tac [lemma_approx_gt_zero] 1);
by (REPEAT(assume_tac 1));
by (REPEAT(dtac hrabs_eqI2 1));
by Auto_tac;
-qed "inf_close_hrabs2";
+qed "approx_hrabs2";
Goal "x @= y ==> abs x @= abs y";
by (res_inst_tac [("Q","x:Infinitesimal")] (excluded_middle RS disjE) 1);
by (res_inst_tac [("x1","x"),("y1","#0")] (hypreal_linear RS disjE) 1);
-by (auto_tac (claset() addIs [inf_close_hrabs1,inf_close_hrabs2,
- Infinitesimal_inf_close_hrabs], simpset()));
-qed "inf_close_hrabs";
+by (auto_tac (claset() addIs [approx_hrabs1,approx_hrabs2,
+ Infinitesimal_approx_hrabs], simpset()));
+qed "approx_hrabs";
Goal "abs(x) @= #0 ==> x @= #0";
by (cut_inst_tac [("x","x")] hrabs_disj 1);
-by (auto_tac (claset() addDs [inf_close_minus], simpset()));
-qed "inf_close_hrabs_zero_cancel";
+by (auto_tac (claset() addDs [approx_minus], simpset()));
+qed "approx_hrabs_zero_cancel";
Goal "e: Infinitesimal ==> abs x @= abs(x+e)";
-by (fast_tac (claset() addIs [inf_close_hrabs,
- Infinitesimal_add_inf_close_self]) 1);
-qed "inf_close_hrabs_add_Infinitesimal";
+by (fast_tac (claset() addIs [approx_hrabs,
+ Infinitesimal_add_approx_self]) 1);
+qed "approx_hrabs_add_Infinitesimal";
Goal "e: Infinitesimal ==> abs x @= abs(x + -e)";
-by (fast_tac (claset() addIs [inf_close_hrabs,
- Infinitesimal_add_minus_inf_close_self]) 1);
-qed "inf_close_hrabs_add_minus_Infinitesimal";
+by (fast_tac (claset() addIs [approx_hrabs,
+ Infinitesimal_add_minus_approx_self]) 1);
+qed "approx_hrabs_add_minus_Infinitesimal";
Goal "[| e: Infinitesimal; e': Infinitesimal; \
\ abs(x+e) = abs(y+e')|] ==> abs x @= abs y";
-by (dres_inst_tac [("x","x")] inf_close_hrabs_add_Infinitesimal 1);
-by (dres_inst_tac [("x","y")] inf_close_hrabs_add_Infinitesimal 1);
-by (auto_tac (claset() addIs [inf_close_trans2], simpset()));
+by (dres_inst_tac [("x","x")] approx_hrabs_add_Infinitesimal 1);
+by (dres_inst_tac [("x","y")] approx_hrabs_add_Infinitesimal 1);
+by (auto_tac (claset() addIs [approx_trans2], simpset()));
qed "hrabs_add_Infinitesimal_cancel";
Goal "[| e: Infinitesimal; e': Infinitesimal; \
\ abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y";
-by (dres_inst_tac [("x","x")] inf_close_hrabs_add_minus_Infinitesimal 1);
-by (dres_inst_tac [("x","y")] inf_close_hrabs_add_minus_Infinitesimal 1);
-by (auto_tac (claset() addIs [inf_close_trans2], simpset()));
+by (dres_inst_tac [("x","x")] approx_hrabs_add_minus_Infinitesimal 1);
+by (dres_inst_tac [("x","y")] approx_hrabs_add_minus_Infinitesimal 1);
+by (auto_tac (claset() addIs [approx_trans2], simpset()));
qed "hrabs_add_minus_Infinitesimal_cancel";
(* interesting slightly counterintuitive theorem: necessary
@@ -1398,8 +1398,8 @@
Goal "[| x: Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] \
\ ==> abs (hypreal_of_real r + x) < hypreal_of_real y";
by (dres_inst_tac [("x","hypreal_of_real r")]
- inf_close_hrabs_add_Infinitesimal 1);
-by (dtac (inf_close_sym RS (bex_Infinitesimal_iff2 RS iffD2)) 1);
+ approx_hrabs_add_Infinitesimal 1);
+by (dtac (approx_sym RS (bex_Infinitesimal_iff2 RS iffD2)) 1);
by (auto_tac (claset() addSIs [Infinitesimal_add_hypreal_of_real_less],
simpset() addsimps [hypreal_of_real_hrabs]));
qed "Infinitesimal_add_hrabs_hypreal_of_real_less";
@@ -1526,13 +1526,13 @@
Goal "[| y: monad x; #0 < hypreal_of_real e |] \
\ ==> abs (y + -x) < hypreal_of_real e";
-by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
+by (dtac (mem_monad_approx RS approx_sym) 1);
by (dtac (bex_Infinitesimal_iff RS iffD2) 1);
by (auto_tac (claset() addSDs [InfinitesimalD], simpset()));
qed "monad_hrabs_less";
Goal "x: monad (hypreal_of_real a) ==> x: HFinite";
-by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
+by (dtac (mem_monad_approx RS approx_sym) 1);
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
by (step_tac (claset() addSDs
[Infinitesimal_subset_HFinite RS subsetD]) 1);
@@ -1547,23 +1547,23 @@
Goalw [st_def] "x: HFinite ==> st x @= x";
by (forward_tac [st_part_Ex] 1 THEN Step_tac 1);
by (rtac someI2 1);
-by (auto_tac (claset() addIs [inf_close_sym], simpset()));
-qed "st_inf_close_self";
+by (auto_tac (claset() addIs [approx_sym], simpset()));
+qed "st_approx_self";
-Goalw [st_def] "x: HFinite ==> st x: SReal";
+Goalw [st_def] "x: HFinite ==> st x: Reals";
by (forward_tac [st_part_Ex] 1 THEN Step_tac 1);
by (rtac someI2 1);
-by (auto_tac (claset() addIs [inf_close_sym], simpset()));
+by (auto_tac (claset() addIs [approx_sym], simpset()));
qed "st_SReal";
Goal "x: HFinite ==> st x: HFinite";
by (etac (st_SReal RS (SReal_subset_HFinite RS subsetD)) 1);
qed "st_HFinite";
-Goalw [st_def] "x: SReal ==> st x = x";
+Goalw [st_def] "x: Reals ==> st x = x";
by (rtac some_equality 1);
by (fast_tac (claset() addIs [(SReal_subset_HFinite RS subsetD)]) 1);
-by (blast_tac (claset() addDs [SReal_inf_close_iff RS iffD1]) 1);
+by (blast_tac (claset() addDs [SReal_approx_iff RS iffD1]) 1);
qed "st_SReal_eq";
(* should be added to simpset *)
@@ -1572,37 +1572,37 @@
qed "st_hypreal_of_real";
Goal "[| x: HFinite; y: HFinite; st x = st y |] ==> x @= y";
-by (auto_tac (claset() addSDs [st_inf_close_self]
- addSEs [inf_close_trans3], simpset()));
-qed "st_eq_inf_close";
+by (auto_tac (claset() addSDs [st_approx_self]
+ addSEs [approx_trans3], simpset()));
+qed "st_eq_approx";
Goal "[| x: HFinite; y: HFinite; x @= y |] ==> st x = st y";
-by (EVERY1 [forward_tac [st_inf_close_self],
- forw_inst_tac [("x","y")] st_inf_close_self,
+by (EVERY1 [forward_tac [st_approx_self],
+ forw_inst_tac [("x","y")] st_approx_self,
dtac st_SReal,dtac st_SReal]);
-by (fast_tac (claset() addEs [inf_close_trans,
- inf_close_trans2,SReal_inf_close_iff RS iffD1]) 1);
-qed "inf_close_st_eq";
+by (fast_tac (claset() addEs [approx_trans,
+ approx_trans2,SReal_approx_iff RS iffD1]) 1);
+qed "approx_st_eq";
Goal "[| x: HFinite; y: HFinite|] \
\ ==> (x @= y) = (st x = st y)";
-by (blast_tac (claset() addIs [inf_close_st_eq,
- st_eq_inf_close]) 1);
-qed "st_eq_inf_close_iff";
+by (blast_tac (claset() addIs [approx_st_eq,
+ st_eq_approx]) 1);
+qed "st_eq_approx_iff";
-Goal "[| x: SReal; e: Infinitesimal |] ==> st(x + e) = x";
+Goal "[| x: Reals; e: Infinitesimal |] ==> st(x + e) = x";
by (forward_tac [st_SReal_eq RS subst] 1);
by (assume_tac 2);
by (forward_tac [SReal_subset_HFinite RS subsetD] 1);
by (forward_tac [Infinitesimal_subset_HFinite RS subsetD] 1);
by (dtac st_SReal_eq 1);
-by (rtac inf_close_st_eq 1);
+by (rtac approx_st_eq 1);
by (auto_tac (claset() addIs [HFinite_add],
- simpset() addsimps [Infinitesimal_add_inf_close_self
- RS inf_close_sym]));
+ simpset() addsimps [Infinitesimal_add_approx_self
+ RS approx_sym]));
qed "st_Infinitesimal_add_SReal";
-Goal "[| x: SReal; e: Infinitesimal |] \
+Goal "[| x: Reals; e: Infinitesimal |] \
\ ==> st(e + x) = x";
by (rtac (hypreal_add_commute RS subst) 1);
by (blast_tac (claset() addSIs [st_Infinitesimal_add_SReal]) 1);
@@ -1610,8 +1610,8 @@
Goal "x: HFinite ==> \
\ EX e: Infinitesimal. x = st(x) + e";
-by (blast_tac (claset() addSDs [(st_inf_close_self RS
- inf_close_sym),bex_Infinitesimal_iff2 RS iffD2]) 1);
+by (blast_tac (claset() addSDs [(st_approx_self RS
+ approx_sym),bex_Infinitesimal_iff2 RS iffD2]) 1);
qed "HFinite_st_Infinitesimal_add";
Goal "[| x: HFinite; y: HFinite |] \
@@ -1684,7 +1684,7 @@
Goal "x: Infinitesimal ==> st x = #0";
by (rtac (st_number_of RS subst) 1);
-by (rtac inf_close_st_eq 1);
+by (rtac approx_st_eq 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
simpset() addsimps [mem_infmal_iff RS sym]));
qed "st_Infinitesimal";
@@ -1712,8 +1712,8 @@
Addsimps [st_divide];
Goal "x: HFinite ==> st(st(x)) = st(x)";
-by (blast_tac (claset() addIs [st_HFinite, st_inf_close_self,
- inf_close_st_eq]) 1);
+by (blast_tac (claset() addIs [st_HFinite, st_approx_self,
+ approx_st_eq]) 1);
qed "st_idempotent";
Addsimps [st_idempotent];
@@ -1951,16 +1951,16 @@
Infinitesimals as smaller than 1/n for all n::nat (> 0)
------------------------------------------------------------------------*)
-Goal "(ALL r. #0 < r --> x < r) = (ALL n. x < inverse(real_of_nat (Suc n)))";
+Goal "(ALL r. #0 < r --> x < r) = (ALL n. x < inverse(real (Suc n)))";
by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc_gt_zero]));
by (blast_tac (claset() addSDs [reals_Archimedean]
addIs [order_less_trans]) 1);
qed "lemma_Infinitesimal";
-Goal "(ALL r: SReal. #0 < r --> x < r) = \
+Goal "(ALL r: Reals. #0 < r --> x < r) = \
\ (ALL n. x < inverse(hypreal_of_nat (Suc n)))";
by (Step_tac 1);
-by (dres_inst_tac [("x","inverse (hypreal_of_real(real_of_nat (Suc n)))")]
+by (dres_inst_tac [("x","inverse (hypreal_of_real(real (Suc n)))")]
bspec 1);
by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1);
by (rtac (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero RS
@@ -1982,10 +1982,10 @@
qed "Infinitesimal_hypreal_of_nat_iff";
-(*---------------------------------------------------------------------------
- Proof that omega (whr) is an infinite number and
- hence that epsilon (ehr) is an infinitesimal number.
- ---------------------------------------------------------------------------*)
+(*-------------------------------------------------------------------------
+ Proof that omega is an infinite number and
+ hence that epsilon is an infinitesimal number.
+ -------------------------------------------------------------------------*)
Goal "{n. n < Suc m} = {n. n < m} Un {n. n = m}";
by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
qed "Suc_Un_eq";
@@ -1995,15 +1995,15 @@
hence cannot belong to FreeUltrafilterNat
-------------------------------------------*)
Goal "finite {n::nat. n < m}";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
by (auto_tac (claset(), simpset() addsimps [Suc_Un_eq]));
qed "finite_nat_segment";
-Goal "finite {n::nat. real_of_nat n < real_of_nat m}";
+Goal "finite {n::nat. real n < real (m::nat)}";
by (auto_tac (claset() addIs [finite_nat_segment], simpset()));
qed "finite_real_of_nat_segment";
-Goal "finite {n. real_of_nat n < u}";
+Goal "finite {n::nat. real n < u}";
by (cut_inst_tac [("x","u")] reals_Archimedean2 1);
by (Step_tac 1);
by (rtac (finite_real_of_nat_segment RSN (2,finite_subset)) 1);
@@ -2015,41 +2015,41 @@
simpset() addsimps [order_less_imp_le]));
qed "lemma_real_le_Un_eq";
-Goal "finite {n. real_of_nat n <= u}";
+Goal "finite {n::nat. real n <= u}";
by (auto_tac (claset(),
simpset() addsimps [lemma_real_le_Un_eq,lemma_finite_omega_set,
finite_real_of_nat_less_real]));
qed "finite_real_of_nat_le_real";
-Goal "finite {n. abs(real_of_nat n) <= u}";
+Goal "finite {n::nat. abs(real n) <= u}";
by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero,
finite_real_of_nat_le_real]) 1);
qed "finite_rabs_real_of_nat_le_real";
-Goal "{n. abs(real_of_nat n) <= u} ~: FreeUltrafilterNat";
+Goal "{n. abs(real n) <= u} ~: FreeUltrafilterNat";
by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
finite_rabs_real_of_nat_le_real]) 1);
qed "rabs_real_of_nat_le_real_FreeUltrafilterNat";
-Goal "{n. u < real_of_nat n} : FreeUltrafilterNat";
+Goal "{n. u < real n} : FreeUltrafilterNat";
by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
-by (subgoal_tac "- {n. u < real_of_nat n} = {n. real_of_nat n <= u}" 1);
+by (subgoal_tac "- {n::nat. u < real n} = {n. real n <= u}" 1);
by (Force_tac 2);
by (asm_full_simp_tac (simpset() addsimps
[finite_real_of_nat_le_real RS FreeUltrafilterNat_finite]) 1);
qed "FreeUltrafilterNat_nat_gt_real";
(*--------------------------------------------------------------
- The complement of {n. abs(real_of_nat n) <= u} =
- {n. u < abs (real_of_nat n)} is in FreeUltrafilterNat
+ The complement of {n. abs(real n) <= u} =
+ {n. u < abs (real n)} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
-Goal "- {n. real_of_nat n <= u} = {n. u < real_of_nat n}";
+Goal "- {n::nat. real n <= u} = {n. u < real n}";
by (auto_tac (claset() addSDs [order_le_less_trans],
simpset() addsimps [not_real_leE]));
val lemma = result();
-Goal "{n. u < abs (real_of_nat n)} : FreeUltrafilterNat";
+Goal "{n. u < abs (real n)} : FreeUltrafilterNat";
by (cut_inst_tac [("u","u")] rabs_real_of_nat_le_real_FreeUltrafilterNat 1);
by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
simpset() addsimps [lemma]));
@@ -2059,18 +2059,18 @@
Omega is a member of HInfinite
-----------------------------------------------*)
-Goal "hyprel``{%n::nat. real_of_nat (Suc n)} : hypreal";
+Goal "hyprel``{%n::nat. real (Suc n)} : hypreal";
by Auto_tac;
qed "hypreal_omega";
-Goal "{n. u < real_of_nat n} : FreeUltrafilterNat";
+Goal "{n. u < real n} : FreeUltrafilterNat";
by (cut_inst_tac [("u","u")] rabs_real_of_nat_le_real_FreeUltrafilterNat 1);
by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
simpset() addsimps [lemma]));
qed "FreeUltrafilterNat_omega";
-Goalw [omega_def] "whr: HInfinite";
+Goalw [omega_def] "omega: HInfinite";
by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite],
simpset()));
by (rtac bexI 1);
@@ -2084,22 +2084,22 @@
Epsilon is a member of Infinitesimal
-----------------------------------------------*)
-Goal "ehr : Infinitesimal";
+Goal "epsilon : Infinitesimal";
by (auto_tac (claset() addSIs [HInfinite_inverse_Infinitesimal,HInfinite_omega],
simpset() addsimps [hypreal_epsilon_inverse_omega]));
qed "Infinitesimal_epsilon";
Addsimps [Infinitesimal_epsilon];
-Goal "ehr : HFinite";
+Goal "epsilon : HFinite";
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
simpset()));
qed "HFinite_epsilon";
Addsimps [HFinite_epsilon];
-Goal "ehr @= #0";
+Goal "epsilon @= #0";
by (simp_tac (simpset() addsimps [mem_infmal_iff RS sym]) 1);
-qed "epsilon_inf_close_zero";
-Addsimps [epsilon_inf_close_zero];
+qed "epsilon_approx_zero";
+Addsimps [epsilon_approx_zero];
(*------------------------------------------------------------------------
Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given
@@ -2107,7 +2107,7 @@
-----------------------------------------------------------------------*)
Goal "0 < u ==> \
-\ (u < inverse (real_of_nat(Suc n))) = (real_of_nat(Suc n) < inverse u)";
+\ (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)";
by (asm_full_simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1);
by (stac pos_real_less_divide_eq 1);
by (assume_tac 1);
@@ -2116,20 +2116,20 @@
by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1);
qed "real_of_nat_less_inverse_iff";
-Goal "#0 < u ==> finite {n. u < inverse(real_of_nat(Suc n))}";
+Goal "#0 < u ==> finite {n. u < inverse(real(Suc n))}";
by (asm_simp_tac (simpset() addsimps [real_of_nat_less_inverse_iff]) 1);
by (asm_simp_tac (simpset() addsimps [real_of_nat_Suc,
real_less_diff_eq RS sym]) 1);
by (rtac finite_real_of_nat_less_real 1);
qed "finite_inverse_real_of_posnat_gt_real";
-Goal "{n. u <= inverse(real_of_nat(Suc n))} = \
-\ {n. u < inverse(real_of_nat(Suc n))} Un {n. u = inverse(real_of_nat(Suc n))}";
+Goal "{n. u <= inverse(real(Suc n))} = \
+\ {n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}";
by (auto_tac (claset() addDs [order_le_imp_less_or_eq],
simpset() addsimps [order_less_imp_le]));
qed "lemma_real_le_Un_eq2";
-Goal "(inverse (real_of_nat(Suc n)) <= r) = (#1 <= r * real_of_nat(Suc n))";
+Goal "(inverse (real(Suc n)) <= r) = (#1 <= r * real(Suc n))";
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
by (simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1);
by (stac pos_real_less_divide_eq 1);
@@ -2137,44 +2137,44 @@
by (simp_tac (simpset() addsimps [real_mult_commute]) 1);
qed "real_of_nat_inverse_le_iff";
-Goal "(u = inverse (real_of_nat(Suc n))) = (real_of_nat(Suc n) = inverse u)";
+Goal "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)";
by (auto_tac (claset(),
simpset() addsimps [real_inverse_inverse, real_of_nat_Suc_gt_zero,
real_not_refl2 RS not_sym]));
qed "real_of_nat_inverse_eq_iff";
-Goal "finite {n::nat. u = inverse(real_of_nat(Suc n))}";
+Goal "finite {n::nat. u = inverse(real(Suc n))}";
by (asm_simp_tac (simpset() addsimps [real_of_nat_inverse_eq_iff]) 1);
by (cut_inst_tac [("x","inverse u - #1")] lemma_finite_omega_set 1);
by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc,
real_diff_eq_eq RS sym, eq_commute]) 1);
qed "lemma_finite_omega_set2";
-Goal "#0 < u ==> finite {n. u <= inverse(real_of_nat(Suc n))}";
+Goal "#0 < u ==> finite {n. u <= inverse(real(Suc n))}";
by (auto_tac (claset(),
simpset() addsimps [lemma_real_le_Un_eq2,lemma_finite_omega_set2,
finite_inverse_real_of_posnat_gt_real]));
qed "finite_inverse_real_of_posnat_ge_real";
Goal "#0 < u ==> \
-\ {n. u <= inverse(real_of_nat(Suc n))} ~: FreeUltrafilterNat";
+\ {n. u <= inverse(real(Suc n))} ~: FreeUltrafilterNat";
by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
finite_inverse_real_of_posnat_ge_real]) 1);
qed "inverse_real_of_posnat_ge_real_FreeUltrafilterNat";
(*--------------------------------------------------------------
- The complement of {n. u <= inverse(real_of_nat(Suc n))} =
- {n. inverse(real_of_nat(Suc n)) < u} is in FreeUltrafilterNat
+ The complement of {n. u <= inverse(real(Suc n))} =
+ {n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
-Goal "- {n. u <= inverse(real_of_nat(Suc n))} = \
-\ {n. inverse(real_of_nat(Suc n)) < u}";
+Goal "- {n. u <= inverse(real(Suc n))} = \
+\ {n. inverse(real(Suc n)) < u}";
by (auto_tac (claset() addSDs [order_le_less_trans],
simpset() addsimps [not_real_leE]));
val lemma = result();
Goal "#0 < u ==> \
-\ {n. inverse(real_of_nat(Suc n)) < u} : FreeUltrafilterNat";
+\ {n. inverse(real(Suc 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]));
@@ -2191,7 +2191,7 @@
(*-----------------------------------------------------
|X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x|: Infinitesimal
-----------------------------------------------------*)
-Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \
+Goal "ALL n. abs(X n + -x) < inverse(real(Suc n)) \
\ ==> Abs_hypreal(hyprel``{X}) + -hypreal_of_real x : Infinitesimal";
by (auto_tac (claset() addSIs [bexI]
addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat,
@@ -2202,20 +2202,20 @@
Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse]));
qed "real_seq_to_hypreal_Infinitesimal";
-Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \
+Goal "ALL n. abs(X n + -x) < inverse(real(Suc n)) \
\ ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x";
-by (rtac (inf_close_minus_iff RS ssubst) 1);
+by (rtac (approx_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";
+qed "real_seq_to_hypreal_approx";
-Goal "ALL n. abs(x + -X n) < inverse(real_of_nat(Suc n)) \
+Goal "ALL n. abs(x + -X n) < inverse(real(Suc 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";
+ real_seq_to_hypreal_approx]) 1);
+qed "real_seq_to_hypreal_approx2";
-Goal "ALL n. abs(X n + -Y n) < inverse(real_of_nat(Suc n)) \
+Goal "ALL n. abs(X n + -Y n) < inverse(real(Suc n)) \
\ ==> Abs_hypreal(hyprel``{X}) + \
\ -Abs_hypreal(hyprel``{Y}) : Infinitesimal";
by (auto_tac (claset() addSIs [bexI]
--- a/src/HOL/Hyperreal/NSA.thy Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Tue Jan 16 12:20:52 2001 +0100
@@ -10,17 +10,17 @@
constdefs
Infinitesimal :: "hypreal set"
- "Infinitesimal == {x. ALL r: SReal. 0 < r --> abs x < r}"
+ "Infinitesimal == {x. ALL r: Reals. 0 < r --> abs x < r}"
HFinite :: "hypreal set"
- "HFinite == {x. EX r: SReal. abs x < r}"
+ "HFinite == {x. EX r: Reals. abs x < r}"
HInfinite :: "hypreal set"
- "HInfinite == {x. ALL r: SReal. r < abs x}"
+ "HInfinite == {x. ALL r: Reals. r < abs x}"
(* standard part map *)
st :: hypreal => hypreal
- "st == (%x. @r. x : HFinite & r:SReal & r @= x)"
+ "st == (%x. @r. x : HFinite & r:Reals & r @= x)"
monad :: hypreal => hypreal set
"monad x == {y. x @= y}"
@@ -29,17 +29,17 @@
"galaxy x == {y. (x + -y) : HFinite}"
(* infinitely close *)
- inf_close :: "[hypreal, hypreal] => bool" (infixl "@=" 50)
+ approx :: "[hypreal, hypreal] => bool" (infixl "@=" 50)
"x @= y == (x + -y) : Infinitesimal"
defs
(*standard real numbers as a subset of the hyperreals*)
- SReal_def "SReal == {x. EX r. x = hypreal_of_real r}"
+ SReal_def "Reals == {x. EX r. x = hypreal_of_real r}"
syntax (symbols)
- inf_close :: "[hypreal, hypreal] => bool" (infixl "\\<approx>" 50)
+ approx :: "[hypreal, hypreal] => bool" (infixl "\\<approx>" 50)
end
--- a/src/HOL/Hyperreal/NatStar.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML Tue Jan 16 12:20:52 2001 +0100
@@ -122,13 +122,13 @@
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
qed "NatStar_hypreal_of_real_image_subset";
-Goal "SNat <= *sNat* (UNIV:: nat set)";
+Goal "Nats <= *sNat* (UNIV:: nat set)";
by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff,
NatStar_hypreal_of_real_image_subset]) 1);
qed "NatStar_SHNat_subset";
Goalw [starsetNat_def]
- "*sNat* X Int SNat = hypnat_of_nat ` X";
+ "*sNat* X Int Nats = hypnat_of_nat ` X";
by (auto_tac (claset(),
simpset() addsimps
[hypnat_of_nat_def,SHNat_def]));
@@ -325,7 +325,7 @@
Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
by (Auto_tac);
-qed "starfunNat_inf_close";
+qed "starfunNat_approx";
(*-----------------------------------------------------------------
@@ -393,16 +393,16 @@
qed "starfun_pow";
(*-----------------------------------------------------
- hypreal_of_hypnat as NS extension of real_of_nat!
+ hypreal_of_hypnat as NS extension of real (from "nat")!
-------------------------------------------------------*)
-Goal "(*fNat* real_of_nat) = hypreal_of_hypnat";
+Goal "(*fNat* real) = hypreal_of_hypnat";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat]));
qed "starfunNat_real_of_nat";
Goal "N : HNatInfinite \
-\ ==> (*fNat* (%x. inverse(real_of_nat x))) N = inverse(hypreal_of_hypnat N)";
+\ ==> (*fNat* (%x::nat. inverse(real 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(),
--- a/src/HOL/Hyperreal/SEQ.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Tue Jan 16 12:20:52 2001 +0100
@@ -11,7 +11,7 @@
-------------------------------------------------------------------------- *)
Goalw [hypnat_omega_def]
- "(*fNat* (%n::nat. inverse(real_of_nat(Suc n)))) whn : Infinitesimal";
+ "(*fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal";
by (auto_tac (claset(),
simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
@@ -24,47 +24,12 @@
Rules for LIMSEQ and NSLIMSEQ etc.
--------------------------------------------------------------------------*)
-(*** LIMSEQ ***)
-Goalw [LIMSEQ_def]
- "X ----> L ==> \
-\ ALL r. #0 < r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r)";
-by (Asm_simp_tac 1);
-qed "LIMSEQD1";
-
-Goalw [LIMSEQ_def]
- "[| X ----> L; #0 < r|] ==> \
-\ EX no. ALL n. no <= n --> abs(X n + -L) < r";
-by (Asm_simp_tac 1);
-qed "LIMSEQD2";
-
-Goalw [LIMSEQ_def]
- "ALL r. #0 < r --> (EX no. ALL n. \
-\ no <= n --> abs(X n + -L) < r) ==> X ----> L";
-by (Asm_simp_tac 1);
-qed "LIMSEQI";
-
Goalw [LIMSEQ_def]
"(X ----> L) = \
\ (ALL r. #0 <r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r))";
by (Simp_tac 1);
qed "LIMSEQ_iff";
-(*** NSLIMSEQ ***)
-Goalw [NSLIMSEQ_def]
- "X ----NS> L ==> ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L";
-by (Asm_simp_tac 1);
-qed "NSLIMSEQD1";
-
-Goalw [NSLIMSEQ_def]
- "[| X ----NS> L; N: HNatInfinite |] ==> (*fNat* X) N @= hypreal_of_real L";
-by (Asm_simp_tac 1);
-qed "NSLIMSEQD2";
-
-Goalw [NSLIMSEQ_def]
- "ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L ==> X ----NS> L";
-by (Asm_simp_tac 1);
-qed "NSLIMSEQI";
-
Goalw [NSLIMSEQ_def]
"(X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)";
by (Simp_tac 1);
@@ -78,7 +43,7 @@
by (auto_tac (claset(),simpset() addsimps
[HNatInfinite_FreeUltrafilterNat_iff]));
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (rtac (inf_close_minus_iff RS iffD2) 1);
+by (rtac (approx_minus_iff RS iffD2) 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat,
mem_infmal_iff RS sym,hypreal_of_real_def,
hypreal_minus,hypreal_add,
@@ -179,7 +144,7 @@
(* skolemization step *)
by (dtac choice 1 THEN Step_tac 1);
by (dres_inst_tac [("x","Abs_hypnat(hypnatrel``{f})")] bspec 1);
-by (dtac (inf_close_minus_iff RS iffD1) 2);
+by (dtac (approx_minus_iff RS iffD1) 2);
by (fold_tac [real_le_def]);
by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1);
by (blast_tac (claset() addIs [rename_numerals lemmaLIM3]) 1);
@@ -203,7 +168,7 @@
Goalw [NSLIMSEQ_def]
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b";
-by (auto_tac (claset() addIs [inf_close_add],
+by (auto_tac (claset() addIs [approx_add],
simpset() addsimps [starfunNat_add RS sym]));
qed "NSLIMSEQ_add";
@@ -214,7 +179,7 @@
Goalw [NSLIMSEQ_def]
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b";
-by (auto_tac (claset() addSIs [inf_close_mult_HFinite],
+by (auto_tac (claset() addSIs [approx_mult_HFinite],
simpset() addsimps [hypreal_of_real_mult, starfunNat_mult RS sym]));
qed "NSLIMSEQ_mult";
@@ -274,7 +239,7 @@
by (dtac bspec 1);
by (auto_tac (claset(),
simpset() addsimps [starfunNat_inverse RS sym,
- hypreal_of_real_inf_close_inverse]));
+ hypreal_of_real_approx_inverse]));
qed "NSLIMSEQ_inverse";
@@ -301,7 +266,7 @@
Goalw [NSLIMSEQ_def]
"[| X ----NS> a; X ----NS> b |] ==> a = b";
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
-by (auto_tac (claset() addDs [inf_close_trans3], simpset()));
+by (auto_tac (claset() addDs [approx_trans3], simpset()));
qed "NSLIMSEQ_unique";
Goal "[| X ----> a; X ----> b |] ==> a = b";
@@ -367,7 +332,7 @@
------------------------------------------------------------------*)
Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))";
by (auto_tac (claset() addSDs [less_imp_Suc_add], simpset()));
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
by (auto_tac (claset() addIs [less_trans], simpset()));
qed "subseq_Suc_iff";
@@ -421,7 +386,7 @@
qed "BseqI";
Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
-\ (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))";
+\ (EX N. ALL n. abs(X n) <= real(Suc N))";
by Auto_tac;
by (cut_inst_tac [("x","K")] reals_Archimedean2 1);
by (Clarify_tac 1);
@@ -432,12 +397,12 @@
qed "lemma_NBseq_def";
(* alternative definition for Bseq *)
-Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))";
+Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) <= real(Suc N))";
by (simp_tac (simpset() addsimps [lemma_NBseq_def]) 1);
qed "Bseq_iff";
Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
-\ (EX N. ALL n. abs(X n) < real_of_nat(Suc N))";
+\ (EX N. ALL n. abs(X n) < real(Suc N))";
by (stac lemma_NBseq_def 1);
by Auto_tac;
by (res_inst_tac [("x","Suc N")] exI 1);
@@ -449,7 +414,7 @@
qed "lemma_NBseq_def2";
(* yet another definition for Bseq *)
-Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real_of_nat(Suc N))";
+Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real(Suc N))";
by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1);
qed "Bseq_iff1a";
@@ -497,20 +462,20 @@
-------------------------------------------------------------------*)
Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \
-\ ==> ALL N. EX n. real_of_nat(Suc N) < abs (X n)";
+\ ==> ALL N. EX n. real(Suc N) < abs (X n)";
by (Step_tac 1);
by (cut_inst_tac [("n","N")] real_of_nat_Suc_gt_zero 1);
by (Blast_tac 1);
val lemmaNSBseq = result();
Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \
-\ ==> EX f. ALL N. real_of_nat(Suc N) < abs (X (f N))";
+\ ==> EX f. ALL N. real(Suc N) < abs (X (f N))";
by (dtac lemmaNSBseq 1);
by (dtac choice 1);
by (Blast_tac 1);
val lemmaNSBseq2 = result();
-Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
+Goal "ALL N. real(Suc N) < abs (X (f N)) \
\ ==> Abs_hypreal(hyprel``{X o f}) : HInfinite";
by (auto_tac (claset(),
simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def]));
@@ -526,22 +491,22 @@
defined using the skolem function f::nat=>nat above
----------------------------------------------------------------------------*)
-Goal "{n. f n <= Suc u & real_of_nat(Suc n) < abs (X (f n))} <= \
-\ {n. f n <= u & real_of_nat(Suc n) < abs (X (f n))} \
-\ Un {n. real_of_nat(Suc n) < abs (X (Suc u))}";
+Goal "{n. f n <= Suc u & real(Suc n) < abs (X (f n))} <= \
+\ {n. f n <= u & real(Suc n) < abs (X (f n))} \
+\ Un {n. real(Suc n) < abs (X (Suc u))}";
by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
val lemma_finite_NSBseq = result();
-Goal "finite {n. f n <= (u::nat) & real_of_nat(Suc n) < abs(X(f n))}";
+Goal "finite {n. f n <= (u::nat) & real(Suc n) < abs(X(f n))}";
by (induct_tac "u" 1);
-by (res_inst_tac [("B","{n. real_of_nat(Suc n) < abs(X 0)}")] finite_subset 1);
+by (res_inst_tac [("B","{n. real(Suc n) < abs(X 0)}")] finite_subset 1);
by (Force_tac 1);
by (rtac (lemma_finite_NSBseq RS finite_subset) 2);
by (auto_tac (claset() addIs [finite_real_of_nat_less_real],
simpset() addsimps [real_of_nat_Suc, real_less_diff_eq RS sym]));
val lemma_finite_NSBseq2 = result();
-Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
+Goal "ALL N. real(Suc N) < abs (X (f N)) \
\ ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite";
by (auto_tac (claset(),
simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
@@ -554,8 +519,8 @@
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
by (auto_tac (claset(),
simpset() addsimps
- [CLAIM "({n. f n <= u} Int {n. real_of_nat(Suc n) < abs(X(f n))}) = \
-\ {n. f n <= (u::nat) & real_of_nat(Suc n) < abs(X(f n))}",
+ [CLAIM "({n. f n <= u} Int {n. real(Suc n) < abs(X(f n))}) = \
+\ {n. f n <= (u::nat) & real(Suc n) < abs(X(f n))}",
lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite]));
qed "HNatInfinite_skolem_f";
@@ -586,7 +551,7 @@
Goalw [NSconvergent_def,NSBseq_def,NSLIMSEQ_def]
"NSconvergent X ==> NSBseq X";
by (blast_tac (claset() addDs [HFinite_hypreal_of_real RS
- (inf_close_sym RSN (2,inf_close_HFinite))]) 1);
+ (approx_sym RSN (2,approx_HFinite))]) 1);
qed "NSconvergent_NSBseq";
(* standard version - easily now proved using *)
@@ -713,7 +678,7 @@
Bmonoseq_LIMSEQ]) 1);
(* second case *)
by (res_inst_tac [("x","U")] exI 1);
-by (rtac LIMSEQI 1 THEN Step_tac 1);
+by (stac LIMSEQ_iff 1 THEN Step_tac 1);
by (forward_tac [lemma_converg2] 1 THEN assume_tac 1);
by (dtac lemma_converg4 1 THEN Auto_tac);
by (res_inst_tac [("x","m")] exI 1 THEN Step_tac 1);
@@ -814,7 +779,7 @@
by (Step_tac 1);
by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (rtac (inf_close_minus_iff RS iffD2) 1);
+by (rtac (approx_minus_iff RS iffD2) 1);
by (rtac (mem_infmal_iff RS iffD1) 1);
by (auto_tac (claset(),
simpset() addsimps [starfunNat, hypreal_minus,hypreal_add,
@@ -845,7 +810,7 @@
by (dtac bspec 1 THEN assume_tac 1);
by (dres_inst_tac [("x","Abs_hypnat (hypnatrel `` {fa})")] bspec 1
THEN auto_tac (claset(), simpset() addsimps [starfunNat]));
-by (dtac (inf_close_minus_iff RS iffD1) 1);
+by (dtac (approx_minus_iff RS iffD1) 1);
by (dtac (mem_infmal_iff RS iffD2) 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
@@ -996,14 +961,14 @@
"NSCauchy X = NSconvergent X";
by (Step_tac 1);
by (forward_tac [NSCauchy_NSBseq] 1);
-by (auto_tac (claset() addIs [inf_close_trans2],
+by (auto_tac (claset() addIs [approx_trans2],
simpset() addsimps
[NSBseq_def,NSCauchy_def]));
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
by (auto_tac (claset() addSDs [st_part_Ex], simpset()
addsimps [SReal_iff]));
-by (blast_tac (claset() addIs [inf_close_trans3]) 1);
+by (blast_tac (claset() addIs [approx_trans3]) 1);
qed "NSCauchy_NSconvergent_iff";
(* Standard proof for free *)
@@ -1077,7 +1042,7 @@
by (dtac bspec 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1);
-by (blast_tac (claset() addIs [inf_close_trans3]) 1);
+by (blast_tac (claset() addIs [approx_trans3]) 1);
qed "NSLIMSEQ_Suc";
(* standard version *)
@@ -1095,7 +1060,7 @@
by (dtac bspec 1 THEN assume_tac 1);
by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1);
by (rotate_tac 2 1);
-by (auto_tac (claset() addSDs [bspec] addIs [inf_close_trans3],
+by (auto_tac (claset() addSDs [bspec] addIs [approx_trans3],
simpset()));
qed "NSLIMSEQ_imp_Suc";
@@ -1138,7 +1103,7 @@
---------------------------------------*)
Goalw [NSLIMSEQ_def]
"f ----NS> l ==> (%n. abs(f n)) ----NS> abs(l)";
-by (auto_tac (claset() addIs [inf_close_hrabs], simpset()
+by (auto_tac (claset() addIs [approx_hrabs], simpset()
addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym]));
qed "NSLIMSEQ_imp_rabs";
@@ -1178,17 +1143,17 @@
Sequence 1/n --> 0 as n --> infinity
-------------------------------------------------------------*)
-Goal "(%n. inverse(real_of_nat(Suc n))) ----> #0";
+Goal "(%n. inverse(real(Suc 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 (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
-by (subgoal_tac "y < real_of_nat na" 1);
+by (subgoal_tac "y < real na" 1);
by (Asm_simp_tac 1);
by (blast_tac (claset() addIs [order_less_le_trans]) 1);
qed "LIMSEQ_inverse_real_of_nat";
-Goal "(%n. inverse(real_of_nat(Suc n))) ----NS> #0";
+Goal "(%n. inverse(real(Suc n))) ----NS> #0";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
LIMSEQ_inverse_real_of_nat]) 1);
qed "NSLIMSEQ_inverse_real_of_nat";
@@ -1197,13 +1162,13 @@
Sequence r + 1/n --> r as n --> infinity
now easily proved
--------------------------------------------*)
-Goal "(%n. r + inverse(real_of_nat(Suc n))) ----> r";
+Goal "(%n. r + inverse(real(Suc n))) ----> r";
by (cut_facts_tac
[ [LIMSEQ_const,LIMSEQ_inverse_real_of_nat] MRS LIMSEQ_add ] 1);
by Auto_tac;
qed "LIMSEQ_inverse_real_of_posnat_add";
-Goal "(%n. r + inverse(real_of_nat(Suc n))) ----NS> r";
+Goal "(%n. r + inverse(real(Suc n))) ----NS> r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
LIMSEQ_inverse_real_of_posnat_add]) 1);
qed "NSLIMSEQ_inverse_real_of_posnat_add";
@@ -1212,24 +1177,24 @@
Also...
--------------*)
-Goal "(%n. r + -inverse(real_of_nat(Suc n))) ----> r";
+Goal "(%n. r + -inverse(real(Suc n))) ----> r";
by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_nat]
MRS LIMSEQ_add_minus] 1);
by (Auto_tac);
qed "LIMSEQ_inverse_real_of_posnat_add_minus";
-Goal "(%n. r + -inverse(real_of_nat(Suc n))) ----NS> r";
+Goal "(%n. r + -inverse(real(Suc n))) ----NS> r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
LIMSEQ_inverse_real_of_posnat_add_minus]) 1);
qed "NSLIMSEQ_inverse_real_of_posnat_add_minus";
-Goal "(%n. r*( #1 + -inverse(real_of_nat(Suc n)))) ----> r";
+Goal "(%n. r*( #1 + -inverse(real(Suc n)))) ----> r";
by (cut_inst_tac [("b","#1")] ([LIMSEQ_const,
LIMSEQ_inverse_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1);
by (Auto_tac);
qed "LIMSEQ_inverse_real_of_posnat_add_minus_mult";
-Goal "(%n. r*( #1 + -inverse(real_of_nat(Suc n)))) ----NS> r";
+Goal "(%n. r*( #1 + -inverse(real(Suc n)))) ----NS> r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
LIMSEQ_inverse_real_of_posnat_add_minus_mult]) 1);
qed "NSLIMSEQ_inverse_real_of_posnat_add_minus_mult";
@@ -1285,8 +1250,8 @@
by (dtac bspec 1 THEN assume_tac 1);
by (dres_inst_tac [("x","N + 1hn")] bspec 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
-by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
-by (dtac inf_close_trans3 1 THEN assume_tac 1);
+by (dtac approx_mult_subst_SReal 1 THEN assume_tac 1);
+by (dtac approx_trans3 1 THEN assume_tac 1);
by (auto_tac (claset(),
simpset() delsimps [hypreal_of_real_mult]
addsimps [hypreal_of_real_mult RS sym]));
--- a/src/HOL/Hyperreal/Series.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/Series.ML Tue Jan 16 12:20:52 2001 +0100
@@ -65,7 +65,7 @@
by (Auto_tac);
qed_spec_mp "sumr_fun_eq";
-Goal "sumr 0 n (%i. r) = real_of_nat n*r";
+Goal "sumr 0 n (%i. r) = real n * r";
by (induct_tac "n" 1);
by (auto_tac (claset(),
simpset() addsimps [real_add_mult_distrib,real_of_nat_zero,
@@ -73,13 +73,13 @@
qed "sumr_const";
Addsimps [sumr_const];
-Goal "sumr 0 n f + -(real_of_nat n*r) = sumr 0 n (%i. f i + -r)";
+Goal "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)";
by (full_simp_tac (simpset() addsimps [sumr_add RS sym,
real_minus_mult_eq2] delsimps [real_minus_mult_eq2 RS sym]) 1);
qed "sumr_add_mult_const";
Goalw [real_diff_def]
- "sumr 0 n f - (real_of_nat n*r) = sumr 0 n (%i. f i - r)";
+ "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)";
by (full_simp_tac (simpset() addsimps [sumr_add_mult_const]) 1);
qed "sumr_diff_mult_const";
@@ -113,7 +113,7 @@
val Suc_diff_n = result();
Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \
-\ --> sumr m na f = (real_of_nat (na - m) * r)";
+\ --> sumr m na f = (real (na - m) * r)";
by (induct_tac "na" 1);
by (Step_tac 1);
by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2);
@@ -125,7 +125,7 @@
qed_spec_mp "sumr_interval_const";
Goal "(ALL n. m <= n --> f n = r) & m <= na \
-\ --> sumr m na f = (real_of_nat (na - m) * r)";
+\ --> sumr m na f = (real (na - m) * r)";
by (induct_tac "na" 1);
by (Step_tac 1);
by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2);
@@ -226,14 +226,14 @@
qed_spec_mp "sumr_subst";
Goal "(ALL p. m <= p & p < m + n --> (f(p) <= K)) \
-\ --> (sumr m (m + n) f <= (real_of_nat n * K))";
+\ --> (sumr m (m + n) f <= (real n * K))";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_add_le_mono],
simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc]));
qed_spec_mp "sumr_bound";
Goal "(ALL p. 0 <= p & p < n --> (f(p) <= K)) \
-\ --> (sumr 0 n f <= (real_of_nat n * K))";
+\ --> (sumr 0 n f <= (real n * K))";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_add_le_mono],
simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc]));
--- a/src/HOL/Hyperreal/Star.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Hyperreal/Star.ML Tue Jan 16 12:20:52 2001 +0100
@@ -88,7 +88,7 @@
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
qed "STAR_hypreal_of_real_image_subset";
-Goalw [starset_def] "*s* X Int SReal = hypreal_of_real ` X";
+Goalw [starset_def] "*s* X Int Reals = hypreal_of_real ` X";
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,SReal_def]));
by (fold_tac [hypreal_of_real_def]);
by (rtac imageI 1 THEN rtac ccontr 1);
@@ -279,7 +279,7 @@
Goal "x @= hypreal_of_real a ==> (*f* (%x. x)) x @= hypreal_of_real a";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun]));
-qed "starfun_Idfun_inf_close";
+qed "starfun_Idfun_approx";
Goal "(*f* (%x. x)) x = x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -330,7 +330,7 @@
Goal "(*f* f) (hypreal_of_real a) @= hypreal_of_real (f a)";
by (Auto_tac);
-qed "starfun_inf_close";
+qed "starfun_approx";
(* useful for NS definition of derivatives *)
Goal "(*f* (%h. f (x + h))) xa = (*f* f) (hypreal_of_real x + xa)";
@@ -348,16 +348,16 @@
Goal "[| (*f* f) xa @= l; (*f* g) xa @= m; \
\ l: HFinite; m: HFinite \
\ |] ==> (*f* (%x. f x * g x)) xa @= l * m";
-by (dtac inf_close_mult_HFinite 1);
+by (dtac approx_mult_HFinite 1);
by (REPEAT(assume_tac 1));
-by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
+by (auto_tac (claset() addIs [approx_sym RSN (2,approx_HFinite)],
simpset()));
-qed "starfun_mult_HFinite_inf_close";
+qed "starfun_mult_HFinite_approx";
Goal "[| (*f* f) xa @= l; (*f* g) xa @= m \
\ |] ==> (*f* (%x. f x + g x)) xa @= l + m";
-by (auto_tac (claset() addIs [inf_close_add], simpset()));
-qed "starfun_add_inf_close";
+by (auto_tac (claset() addIs [approx_add], simpset()));
+qed "starfun_add_approx";
(*----------------------------------------------------
Examples: hrabs is nonstandard extension of rabs
@@ -457,7 +457,7 @@
-------------------------------------------------------------------*)
Goal "(x:Infinitesimal) = \
\ (EX X:Rep_hypreal(x). \
-\ ALL m. {n. abs(X n) < inverse(real_of_nat(Suc m))} \
+\ ALL m. {n. abs(X n) < inverse(real(Suc m))} \
\ : FreeUltrafilterNat)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl],
@@ -472,15 +472,15 @@
Goal "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) = \
\ (ALL m. {n. abs (X n + - Y n) < \
-\ inverse(real_of_nat(Suc m))} : FreeUltrafilterNat)";
-by (rtac (inf_close_minus_iff RS ssubst) 1);
+\ inverse(real(Suc m))} : FreeUltrafilterNat)";
+by (rtac (approx_minus_iff RS ssubst) 1);
by (rtac (mem_infmal_iff RS subst) 1);
by (auto_tac (claset(),
simpset() addsimps [hypreal_minus, hypreal_add,
Infinitesimal_FreeUltrafilterNat_iff2]));
by (dres_inst_tac [("x","m")] spec 1);
by (Fuf_tac 1);
-qed "inf_close_FreeUltrafilterNat_iff";
+qed "approx_FreeUltrafilterNat_iff";
Goal "inj starfun";
by (rtac injI 1);
--- a/src/HOL/Real/RComplete.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RComplete.ML Tue Jan 16 12:20:52 2001 +0100
@@ -194,37 +194,37 @@
Related: Archimedean property of reals
----------------------------------------------------------------*)
-Goal "#0 < real_of_nat (Suc n)";
-by (res_inst_tac [("y","real_of_nat n")] order_le_less_trans 1);
+Goal "#0 < real (Suc n)";
+by (res_inst_tac [("y","real n")] order_le_less_trans 1);
by (rtac (rename_numerals real_of_nat_ge_zero) 1);
by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1);
qed "real_of_nat_Suc_gt_zero";
-Goal "#0 < x ==> EX n. inverse (real_of_nat(Suc n)) < x";
+Goal "#0 < x ==> EX n. inverse (real(Suc n)) < x";
by (rtac ccontr 1);
-by (subgoal_tac "ALL n. x * real_of_nat (Suc n) <= #1" 1);
+by (subgoal_tac "ALL n. x * real (Suc n) <= #1" 1);
by (asm_full_simp_tac
(simpset() addsimps [linorder_not_less, real_inverse_eq_divide]) 2);
by (Clarify_tac 2);
by (dres_inst_tac [("x","n")] spec 2);
-by (dres_inst_tac [("k","real_of_nat (Suc n)")] (real_mult_le_mono1) 2);
+by (dres_inst_tac [("k","real (Suc n)")] (real_mult_le_mono1) 2);
by (rtac real_of_nat_ge_zero 2);
by (asm_full_simp_tac (simpset()
addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym,
real_mult_commute]) 2);
by (subgoal_tac "isUb (UNIV::real set) \
-\ {z. EX n. z = x*(real_of_nat (Suc n))} #1" 1);
-by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_nat (Suc n))}" 1);
+\ {z. EX n. z = x*(real (Suc n))} #1" 1);
+by (subgoal_tac "EX X. X : {z. EX n. z = x*(real (Suc n))}" 1);
by (dtac reals_complete 1);
by (auto_tac (claset() addIs [isUbI,setleI],simpset()));
-by (subgoal_tac "ALL m. x*(real_of_nat(Suc m)) <= t" 1);
+by (subgoal_tac "ALL m. x*(real(Suc m)) <= t" 1);
by (asm_full_simp_tac (simpset() addsimps
[real_of_nat_Suc, real_add_mult_distrib2]) 1);
by (blast_tac (claset() addIs [isLubD2]) 2);
by (asm_full_simp_tac
(simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1);
by (subgoal_tac "isUb (UNIV::real set) \
-\ {z. EX n. z = x*(real_of_nat (Suc n))} (t + (-x))" 1);
+\ {z. EX n. z = x*(real (Suc n))} (t + (-x))" 1);
by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1);
by (auto_tac (claset(),
@@ -233,7 +233,7 @@
(*There must be other proofs, e.g. Suc of the largest integer in the
cut representing x*)
-Goal "EX n. (x::real) < real_of_nat n";
+Goal "EX n. (x::real) < real (n::nat)";
by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1);
by (res_inst_tac [("x","0")] exI 1);
by (res_inst_tac [("x","1")] exI 2);
@@ -244,7 +244,7 @@
by (forw_inst_tac [("y","inverse x")]
(rename_numerals real_mult_less_mono1) 1);
by Auto_tac;
-by (dres_inst_tac [("y","#1"),("z","real_of_nat (Suc n)")]
+by (dres_inst_tac [("y","#1"),("z","real (Suc n)")]
(rotate_prems 1 real_mult_less_mono2) 1);
by (auto_tac (claset(),
simpset() addsimps [real_of_nat_Suc_gt_zero,
--- a/src/HOL/Real/RealAbs.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealAbs.ML Tue Jan 16 12:20:52 2001 +0100
@@ -213,7 +213,7 @@
qed "real_0_less_abs_iff";
Addsimps [real_0_less_abs_iff];
-Goal "abs (real_of_nat x) = real_of_nat x";
+Goal "abs (real x) = real (x::nat)";
by (auto_tac (claset() addIs [abs_eqI1],
simpset() addsimps [rename_numerals real_of_nat_ge_zero]));
qed "abs_real_of_nat_cancel";
--- a/src/HOL/Real/RealBin.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealBin.ML Tue Jan 16 12:20:52 2001 +0100
@@ -6,9 +6,9 @@
Binary arithmetic for the reals (integer literals only).
*)
-(** real_of_int (coercion from int to real) **)
+(** real (coercion from int to real) **)
-Goal "real_of_int (number_of w) = number_of w";
+Goal "real (number_of w :: int) = number_of w";
by (simp_tac (simpset() addsimps [real_number_of_def]) 1);
qed "real_number_of";
Addsimps [real_number_of];
@@ -156,15 +156,15 @@
Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
-(** real_of_nat **)
+(** real from type "nat" **)
-Goal "(#0 < real_of_nat n) = (0<n)";
+Goal "(#0 < real (n::nat)) = (0<n)";
by (simp_tac (HOL_ss addsimps [real_of_nat_less_iff,
rename_numerals real_of_nat_zero RS sym]) 1);
qed "zero_less_real_of_nat_iff";
AddIffs [zero_less_real_of_nat_iff];
-Goal "(#0 <= real_of_nat n) = (0<=n)";
+Goal "(#0 <= real (n::nat)) = (0<=n)";
by (simp_tac (HOL_ss addsimps [real_of_nat_le_iff,
rename_numerals real_of_nat_zero RS sym]) 1);
qed "zero_le_real_of_nat_iff";
@@ -197,7 +197,7 @@
(*"neg" is used in rewrite rules for binary comparisons*)
-Goal "real_of_nat (number_of v :: nat) = \
+Goal "real (number_of v :: nat) = \
\ (if neg (number_of v) then #0 \
\ else (number_of v :: real))";
by (simp_tac
--- a/src/HOL/Real/RealBin.thy Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealBin.thy Tue Jan 16 12:20:52 2001 +0100
@@ -15,7 +15,7 @@
defs
real_number_of_def
- "number_of v == real_of_int (number_of v)"
- (*::bin=>real ::bin=>int*)
+ "number_of v == real (number_of v :: int)"
+ (*::bin=>real ::bin=>int*)
end
--- a/src/HOL/Real/RealDef.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealDef.ML Tue Jan 16 12:20:52 2001 +0100
@@ -5,6 +5,9 @@
Description : The reals
*)
+(*Ensures that Blast_tac can cope with real*)
+Blast.overloaded ("RealDef.real", domain_type);
+
(*** Proving that realrel is an equivalence relation ***)
Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
@@ -43,66 +46,61 @@
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
qed "realrelE";
-AddSIs [realrelI];
-AddSEs [realrelE];
-
Goal "(x,x): realrel";
-by (pair_tac "x" 1);
-by (rtac realrelI 1);
-by (rtac refl 1);
+by (case_tac "x" 1);
+by (asm_simp_tac (simpset() addsimps [realrel_def]) 1);
qed "realrel_refl";
Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV realrel";
-by (fast_tac (claset() addSIs [realrel_refl]
- addSEs [sym, preal_trans_lemma]) 1);
+by (fast_tac (claset() addSIs [realrelI, realrel_refl]
+ addSEs [sym, realrelE, preal_trans_lemma]) 1);
qed "equiv_realrel";
(* (realrel `` {x} = realrel `` {y}) = ((x,y) : realrel) *)
bind_thm ("equiv_realrel_iff",
[equiv_realrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
-Goalw [real_def,realrel_def,quotient_def] "realrel``{(x,y)}:real";
+Goalw [REAL_def,realrel_def,quotient_def] "realrel``{(x,y)}: REAL";
by (Blast_tac 1);
qed "realrel_in_real";
-Goal "inj_on Abs_real real";
+Goal "inj_on Abs_REAL REAL";
by (rtac inj_on_inverseI 1);
-by (etac Abs_real_inverse 1);
-qed "inj_on_Abs_real";
+by (etac Abs_REAL_inverse 1);
+qed "inj_on_Abs_REAL";
-Addsimps [equiv_realrel_iff,inj_on_Abs_real RS inj_on_iff,
- realrel_iff, realrel_in_real, Abs_real_inverse];
+Addsimps [equiv_realrel_iff,inj_on_Abs_REAL RS inj_on_iff,
+ realrel_iff, realrel_in_real, Abs_REAL_inverse];
Addsimps [equiv_realrel RS eq_equiv_class_iff];
bind_thm ("eq_realrelD", equiv_realrel RSN (2,eq_equiv_class));
-Goal "inj(Rep_real)";
+Goal "inj Rep_REAL";
by (rtac inj_inverseI 1);
-by (rtac Rep_real_inverse 1);
-qed "inj_Rep_real";
+by (rtac Rep_REAL_inverse 1);
+qed "inj_Rep_REAL";
(** real_of_preal: the injection from preal to real **)
Goal "inj(real_of_preal)";
by (rtac injI 1);
by (rewtac real_of_preal_def);
-by (dtac (inj_on_Abs_real RS inj_onD) 1);
+by (dtac (inj_on_Abs_REAL RS inj_onD) 1);
by (REPEAT (rtac realrel_in_real 1));
by (dtac eq_equiv_class 1);
by (rtac equiv_realrel 1);
by (Blast_tac 1);
-by Safe_tac;
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [realrel_def]) 1);
qed "inj_real_of_preal";
val [prem] = Goal
- "(!!x y. z = Abs_real(realrel``{(x,y)}) ==> P) ==> P";
+ "(!!x y. z = Abs_REAL(realrel``{(x,y)}) ==> P) ==> P";
by (res_inst_tac [("x1","z")]
- (rewrite_rule [real_def] Rep_real RS quotientE) 1);
-by (dres_inst_tac [("f","Abs_real")] arg_cong 1);
-by (res_inst_tac [("p","x")] PairE 1);
+ (rewrite_rule [REAL_def] Rep_REAL RS quotientE) 1);
+by (dres_inst_tac [("f","Abs_REAL")] arg_cong 1);
+by (case_tac "x" 1);
by (rtac prem 1);
-by (asm_full_simp_tac (simpset() addsimps [Rep_real_inverse]) 1);
-qed "eq_Abs_real";
+by (asm_full_simp_tac (simpset() addsimps [Rep_REAL_inverse]) 1);
+qed "eq_Abs_REAL";
(**** real_minus: additive inverse on real ****)
@@ -113,15 +111,14 @@
qed "real_minus_congruent";
Goalw [real_minus_def]
- "- (Abs_real(realrel``{(x,y)})) = Abs_real(realrel `` {(y,x)})";
-by (res_inst_tac [("f","Abs_real")] arg_cong 1);
-by (simp_tac (simpset() addsimps
- [realrel_in_real RS Abs_real_inverse,
- [equiv_realrel, real_minus_congruent] MRS UN_equiv_class]) 1);
+ "- (Abs_REAL(realrel``{(x,y)})) = Abs_REAL(realrel `` {(y,x)})";
+by (res_inst_tac [("f","Abs_REAL")] arg_cong 1);
+by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_REAL_inverse,
+ [equiv_realrel, real_minus_congruent] MRS UN_equiv_class]) 1);
qed "real_minus";
Goal "- (- z) = (z::real)";
-by (res_inst_tac [("z","z")] eq_Abs_real 1);
+by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
by (asm_simp_tac (simpset() addsimps [real_minus]) 1);
qed "real_minus_minus";
@@ -140,7 +137,7 @@
Addsimps [real_minus_zero];
Goal "(-x = 0) = (x = (0::real))";
-by (res_inst_tac [("z","x")] eq_Abs_real 1);
+by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
by (auto_tac (claset(),
simpset() addsimps [real_zero_def, real_minus] @ preal_add_ac));
qed "real_minus_zero_iff";
@@ -151,7 +148,7 @@
Goalw [congruent2_def]
"congruent2 realrel (%p1 p2. \
\ (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)";
-by (Clarify_tac 1);
+by (clarify_tac (claset() addSEs [realrelE]) 1);
by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
@@ -159,22 +156,22 @@
qed "real_add_congruent2";
Goalw [real_add_def]
- "Abs_real(realrel``{(x1,y1)}) + Abs_real(realrel``{(x2,y2)}) = \
-\ Abs_real(realrel``{(x1+x2, y1+y2)})";
+ "Abs_REAL(realrel``{(x1,y1)}) + Abs_REAL(realrel``{(x2,y2)}) = \
+\ Abs_REAL(realrel``{(x1+x2, y1+y2)})";
by (simp_tac (simpset() addsimps
[[equiv_realrel, real_add_congruent2] MRS UN_equiv_class2]) 1);
qed "real_add";
Goal "(z::real) + w = w + z";
-by (res_inst_tac [("z","z")] eq_Abs_real 1);
-by (res_inst_tac [("z","w")] eq_Abs_real 1);
+by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","w")] eq_Abs_REAL 1);
by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1);
qed "real_add_commute";
Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_real 1);
-by (res_inst_tac [("z","z2")] eq_Abs_real 1);
-by (res_inst_tac [("z","z3")] eq_Abs_real 1);
+by (res_inst_tac [("z","z1")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","z2")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","z3")] eq_Abs_REAL 1);
by (asm_simp_tac (simpset() addsimps [real_add, preal_add_assoc]) 1);
qed "real_add_assoc";
@@ -189,7 +186,7 @@
bind_thms ("real_add_ac", [real_add_assoc,real_add_commute,real_add_left_commute]);
Goalw [real_of_preal_def,real_zero_def] "(0::real) + z = z";
-by (res_inst_tac [("z","z")] eq_Abs_real 1);
+by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
qed "real_add_zero_left";
Addsimps [real_add_zero_left];
@@ -200,7 +197,7 @@
Addsimps [real_add_zero_right];
Goalw [real_zero_def] "z + (-z) = (0::real)";
-by (res_inst_tac [("z","z")] eq_Abs_real 1);
+by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
by (asm_full_simp_tac (simpset() addsimps [real_minus,
real_add, preal_add_commute]) 1);
qed "real_add_minus";
@@ -253,8 +250,8 @@
qed "real_as_add_inverse_ex";
Goal "-(x + y) = (-x) + (- y :: real)";
-by (res_inst_tac [("z","x")] eq_Abs_real 1);
-by (res_inst_tac [("z","y")] eq_Abs_real 1);
+by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","y")] eq_Abs_REAL 1);
by (auto_tac (claset(),simpset() addsimps [real_minus,real_add]));
qed "real_minus_add_distrib";
@@ -310,23 +307,23 @@
qed "real_mult_congruent2";
Goalw [real_mult_def]
- "Abs_real((realrel``{(x1,y1)})) * Abs_real((realrel``{(x2,y2)})) = \
-\ Abs_real(realrel `` {(x1*x2+y1*y2,x1*y2+x2*y1)})";
+ "Abs_REAL((realrel``{(x1,y1)})) * Abs_REAL((realrel``{(x2,y2)})) = \
+\ Abs_REAL(realrel `` {(x1*x2+y1*y2,x1*y2+x2*y1)})";
by (simp_tac (simpset() addsimps
[[equiv_realrel, real_mult_congruent2] MRS UN_equiv_class2]) 1);
qed "real_mult";
Goal "(z::real) * w = w * z";
-by (res_inst_tac [("z","z")] eq_Abs_real 1);
-by (res_inst_tac [("z","w")] eq_Abs_real 1);
+by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","w")] eq_Abs_REAL 1);
by (asm_simp_tac
(simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1);
qed "real_mult_commute";
Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_real 1);
-by (res_inst_tac [("z","z2")] eq_Abs_real 1);
-by (res_inst_tac [("z","z3")] eq_Abs_real 1);
+by (res_inst_tac [("z","z1")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","z2")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","z3")] eq_Abs_REAL 1);
by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @
preal_add_ac @ preal_mult_ac) 1);
qed "real_mult_assoc";
@@ -342,7 +339,7 @@
[real_mult_assoc, real_mult_commute, real_mult_left_commute]);
Goalw [real_one_def,pnat_one_def] "1r * z = z";
-by (res_inst_tac [("z","z")] eq_Abs_real 1);
+by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
by (asm_full_simp_tac
(simpset() addsimps [real_mult,
preal_add_mult_distrib2,preal_mult_1_right]
@@ -358,7 +355,7 @@
Addsimps [real_mult_1_right];
Goalw [real_zero_def,pnat_one_def] "0 * z = (0::real)";
-by (res_inst_tac [("z","z")] eq_Abs_real 1);
+by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult,
preal_add_mult_distrib2,preal_mult_1_right]
@ preal_mult_ac @ preal_add_ac) 1);
@@ -371,8 +368,8 @@
Addsimps [real_mult_0_right, real_mult_0];
Goal "-(x * y) = (-x) * (y::real)";
-by (res_inst_tac [("z","x")] eq_Abs_real 1);
-by (res_inst_tac [("z","y")] eq_Abs_real 1);
+by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","y")] eq_Abs_REAL 1);
by (auto_tac (claset(),
simpset() addsimps [real_minus,real_mult]
@ preal_mult_ac @ preal_add_ac));
@@ -419,9 +416,9 @@
qed "real_add_assoc_swap";
Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)";
-by (res_inst_tac [("z","z1")] eq_Abs_real 1);
-by (res_inst_tac [("z","z2")] eq_Abs_real 1);
-by (res_inst_tac [("z","w")] eq_Abs_real 1);
+by (res_inst_tac [("z","z1")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","z2")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","w")] eq_Abs_REAL 1);
by (asm_simp_tac
(simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @
preal_add_ac @ preal_mult_ac) 1);
@@ -451,20 +448,20 @@
(*** existence of inverse ***)
(** lemma -- alternative definition of 0 **)
-Goalw [real_zero_def] "0 = Abs_real (realrel `` {(x, x)})";
+Goalw [real_zero_def] "0 = Abs_REAL (realrel `` {(x, x)})";
by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
qed "real_zero_iff";
Goalw [real_zero_def,real_one_def]
"!!(x::real). x ~= 0 ==> EX y. x*y = 1r";
-by (res_inst_tac [("z","x")] eq_Abs_real 1);
+by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
simpset() addsimps [real_zero_iff RS sym]));
-by (res_inst_tac [("x","Abs_real (realrel `` \
+by (res_inst_tac [("x","Abs_REAL (realrel `` \
\ {(preal_of_prat(prat_of_pnat 1p),pinv(D)+\
\ preal_of_prat(prat_of_pnat 1p))})")] exI 1);
-by (res_inst_tac [("x","Abs_real (realrel `` \
+by (res_inst_tac [("x","Abs_REAL (realrel `` \
\ {(pinv(D)+preal_of_prat(prat_of_pnat 1p),\
\ preal_of_prat(prat_of_pnat 1p))})")] exI 2);
by (auto_tac (claset(),
@@ -651,7 +648,7 @@
qed "preal_lemma_for_not_refl";
Goal "~ (R::real) < R";
-by (res_inst_tac [("z","R")] eq_Abs_real 1);
+by (res_inst_tac [("z","R")] eq_Abs_REAL 1);
by (auto_tac (claset(),simpset() addsimps [real_less_def]));
by (dtac preal_lemma_for_not_refl 1);
by (assume_tac 1);
@@ -677,9 +674,9 @@
(** heavy re-writing involved*)
Goal "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
-by (res_inst_tac [("z","R1")] eq_Abs_real 1);
-by (res_inst_tac [("z","R2")] eq_Abs_real 1);
-by (res_inst_tac [("z","R3")] eq_Abs_real 1);
+by (res_inst_tac [("z","R1")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","R2")] eq_Abs_REAL 1);
+by (res_inst_tac [("z","R3")] eq_Abs_REAL 1);
by (auto_tac (claset(),simpset() addsimps [real_less_def]));
by (REPEAT(rtac exI 1));
by (EVERY[rtac conjI 1, rtac conjI 2]);
@@ -716,13 +713,13 @@
Goalw [real_of_preal_def]
"!!(x::preal). y < x ==> \
-\ EX m. Abs_real (realrel `` {(x,y)}) = real_of_preal m";
+\ EX m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m";
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
simpset() addsimps preal_add_ac));
qed "real_of_preal_ExI";
Goalw [real_of_preal_def]
- "!!(x::preal). EX m. Abs_real (realrel `` {(x,y)}) = \
+ "!!(x::preal). EX m. Abs_REAL (realrel `` {(x,y)}) = \
\ real_of_preal m ==> y < x";
by (auto_tac (claset(),
simpset() addsimps
@@ -731,14 +728,14 @@
[preal_add_assoc RS sym,preal_self_less_add_left]) 1);
qed "real_of_preal_ExD";
-Goal "(EX m. Abs_real (realrel `` {(x,y)}) = real_of_preal m) = (y < x)";
+Goal "(EX m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m) = (y < x)";
by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1);
qed "real_of_preal_iff";
(*** Gleason prop 9-4.4 p 127 ***)
Goalw [real_of_preal_def,real_zero_def]
"EX m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)";
-by (res_inst_tac [("z","x")] eq_Abs_real 1);
+by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
--- a/src/HOL/Real/RealDef.thy Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealDef.thy Tue Jan 16 12:20:52 2001 +0100
@@ -12,9 +12,10 @@
constdefs
realrel :: "((preal * preal) * (preal * preal)) set"
- "realrel == {p. ? x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+ "realrel == {p. EX x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
-typedef real = "UNIV//realrel" (Equiv.quotient_def)
+typedef (REAL)
+ real = "UNIV//realrel" (Equiv.quotient_def)
instance
@@ -25,20 +26,23 @@
(*Overloaded constants denoting the Nat and Real subsets of enclosing
types such as hypreal and complex*)
- SNat, SReal :: "'a set"
+ Nats, Reals :: "'a set"
+ (*overloaded constant for injecting other types into "real"*)
+ real :: 'a => real
+
defs
real_zero_def
- "0 == Abs_real(realrel``{(preal_of_prat(prat_of_pnat 1p),
+ "0 == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1p),
preal_of_prat(prat_of_pnat 1p))})"
real_one_def
- "1r == Abs_real(realrel``{(preal_of_prat(prat_of_pnat 1p) +
+ "1r == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1p) +
preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
real_minus_def
- "- R == Abs_real(UN (x,y):Rep_real(R). realrel``{(y,x)})"
+ "- R == Abs_REAL(UN (x,y):Rep_REAL(R). realrel``{(y,x)})"
real_diff_def
"R - (S::real) == R + - S"
@@ -51,36 +55,39 @@
constdefs
+ (** these don't use the overloaded real because users don't see them **)
+
real_of_preal :: preal => real
"real_of_preal m ==
- Abs_real(realrel``{(m+preal_of_prat(prat_of_pnat 1p),
+ Abs_REAL(realrel``{(m+preal_of_prat(prat_of_pnat 1p),
preal_of_prat(prat_of_pnat 1p))})"
real_of_posnat :: nat => real
"real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
- real_of_nat :: nat => real
- "real_of_nat n == real_of_posnat n + (-1r)"
defs
+ (*overloaded*)
+ real_of_nat_def "real n == real_of_posnat n + (-1r)"
+
real_add_def
- "P+Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
+ "P+Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
(%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)"
real_mult_def
- "P*Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
+ "P*Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
(%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)})
p2) p1)"
real_less_def
"P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
- (x1,y1):Rep_real(P) & (x2,y2):Rep_real(Q)"
+ (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)"
real_le_def
"P <= (Q::real) == ~(Q < P)"
syntax (symbols)
- SReal :: "'a set" ("\\<real>")
- SNat :: "'a set" ("\\<nat>")
+ Reals :: "'a set" ("\\<real>")
+ Nats :: "'a set" ("\\<nat>")
end
--- a/src/HOL/Real/RealInt.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealInt.ML Tue Jan 16 12:20:52 2001 +0100
@@ -16,16 +16,16 @@
qed "real_of_int_congruent";
Goalw [real_of_int_def]
- "real_of_int (Abs_Integ (intrel `` {(i, j)})) = \
-\ Abs_real(realrel `` \
+ "real (Abs_Integ (intrel `` {(i, j)})) = \
+\ Abs_REAL(realrel `` \
\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))})";
-by (res_inst_tac [("f","Abs_real")] arg_cong 1);
-by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_real_inverse,
+by (res_inst_tac [("f","Abs_REAL")] arg_cong 1);
+by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_REAL_inverse,
[equiv_intrel, real_of_int_congruent] MRS UN_equiv_class]) 1);
qed "real_of_int";
-Goal "inj(real_of_int)";
+Goal "inj(real :: int => real)";
by (rtac injI 1);
by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
@@ -35,75 +35,76 @@
prat_of_pnat_add RS sym,pnat_of_nat_add]));
qed "inj_real_of_int";
-Goalw [int_def,real_zero_def] "real_of_int (int 0) = 0";
+Goalw [int_def,real_zero_def] "real (int 0) = 0";
by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
qed "real_of_int_zero";
-Goalw [int_def,real_one_def] "real_of_int (int 1) = 1r";
+Goalw [int_def,real_one_def] "real (int 1) = 1r";
by (auto_tac (claset(),
simpset() addsimps [real_of_int,
preal_of_prat_add RS sym,pnat_two_eq,
prat_of_pnat_add RS sym,pnat_one_iff RS sym]));
qed "real_of_int_one";
-Goal "real_of_int x + real_of_int y = real_of_int (x + y)";
+Goal "real (x::int) + real y = real (x + y)";
by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
-by (auto_tac (claset(),simpset() addsimps [real_of_int,
- preal_of_prat_add RS sym,prat_of_pnat_add RS sym,
- zadd,real_add,pnat_of_nat_add] @ pnat_add_ac));
+by (auto_tac (claset(),
+ simpset() addsimps [real_of_int, preal_of_prat_add RS sym,
+ prat_of_pnat_add RS sym, zadd,real_add,
+ pnat_of_nat_add] @ pnat_add_ac));
qed "real_of_int_add";
Addsimps [real_of_int_add RS sym];
-Goal "-real_of_int x = real_of_int (-x)";
+Goal "-real (x::int) = real (-x)";
by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
by (auto_tac (claset(), simpset() addsimps [real_of_int, real_minus,zminus]));
qed "real_of_int_minus";
Addsimps [real_of_int_minus RS sym];
Goalw [zdiff_def,real_diff_def]
- "real_of_int x - real_of_int y = real_of_int (x - y)";
+ "real (x::int) - real y = real (x - y)";
by (simp_tac (HOL_ss addsimps [real_of_int_add, real_of_int_minus]) 1);
qed "real_of_int_diff";
Addsimps [real_of_int_diff RS sym];
-Goal "real_of_int x * real_of_int y = real_of_int (x * y)";
+Goal "real (x::int) * real y = real (x * y)";
by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
by (auto_tac (claset(),
simpset() addsimps [real_of_int, real_mult,zmult,
- preal_of_prat_mult RS sym,pnat_of_nat_mult,
- prat_of_pnat_mult RS sym,preal_of_prat_add RS sym,
- prat_of_pnat_add RS sym,pnat_of_nat_add] @ mult_ac @add_ac
- @ pnat_add_ac));
+ preal_of_prat_mult RS sym,pnat_of_nat_mult,
+ prat_of_pnat_mult RS sym,preal_of_prat_add RS sym,
+ prat_of_pnat_add RS sym,pnat_of_nat_add] @
+ mult_ac @ add_ac @ pnat_add_ac));
qed "real_of_int_mult";
Addsimps [real_of_int_mult RS sym];
-Goal "real_of_int (int (Suc n)) = real_of_int (int n) + 1r";
-by (simp_tac (simpset() addsimps [real_of_int_one RS sym,
- zadd_int] @ zadd_ac) 1);
+Goal "real (int (Suc n)) = real (int n) + 1r";
+by (simp_tac (simpset() addsimps [real_of_int_one RS sym, zadd_int] @
+ zadd_ac) 1);
qed "real_of_int_Suc";
(* relating two of the embeddings *)
-Goal "real_of_int (int n) = real_of_nat n";
+Goal "real (int n) = real n";
by (induct_tac "n" 1);
-by (ALLGOALS (simp_tac (HOL_ss addsimps [real_of_int_zero,
- real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc])));
+by (ALLGOALS (simp_tac (HOL_ss addsimps [real_of_int_zero, real_of_nat_zero,
+ real_of_int_Suc,real_of_nat_Suc])));
by (Simp_tac 1);
qed "real_of_int_real_of_nat";
-Goal "~neg z ==> real_of_nat (nat z) = real_of_int z";
+Goal "~neg z ==> real (nat z) = real z";
by (asm_simp_tac (simpset() addsimps [not_neg_nat,
real_of_int_real_of_nat RS sym]) 1);
qed "real_of_nat_real_of_int";
-Goal "(real_of_int x = 0) = (x = int 0)";
+Goal "(real x = 0) = (x = int 0)";
by (auto_tac (claset() addIs [inj_real_of_int RS injD],
HOL_ss addsimps [real_of_int_zero]));
qed "real_of_int_zero_cancel";
Addsimps [real_of_int_zero_cancel];
-Goal "real_of_int x < real_of_int y ==> x < y";
+Goal "real (x::int) < real y ==> x < y";
by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
by (auto_tac (claset(),
simpset() addsimps [zle_iff_zadd, real_of_int_add RS sym,
@@ -111,24 +112,24 @@
linorder_not_le RS sym]));
qed "real_of_int_less_cancel";
-Goal "(real_of_int x = real_of_int y) = (x = y)";
+Goal "(real (x::int) = real y) = (x = y)";
by (blast_tac (claset() addSDs [inj_real_of_int RS injD]) 1);
qed "real_of_int_eq_iff";
AddIffs [real_of_int_eq_iff];
-Goal "x < y ==> (real_of_int x < real_of_int y)";
+Goal "x < y ==> (real (x::int) < real y)";
by (full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
by (auto_tac (claset() addSDs [real_of_int_less_cancel],
simpset() addsimps [order_le_less]));
qed "real_of_int_less_mono";
-Goal "(real_of_int x < real_of_int y) = (x < y)";
-by (blast_tac (claset() addIs [real_of_int_less_cancel,
- real_of_int_less_mono]) 1);
+Goal "(real (x::int) < real y) = (x < y)";
+by (blast_tac (claset() addDs [real_of_int_less_cancel]
+ addIs [real_of_int_less_mono]) 1);
qed "real_of_int_less_iff";
AddIffs [real_of_int_less_iff];
-Goal "(real_of_int x <= real_of_int y) = (x <= y)";
+Goal "(real (x::int) <= real y) = (x <= y)";
by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
qed "real_of_int_le_iff";
Addsimps [real_of_int_le_iff];
--- a/src/HOL/Real/RealInt.thy Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealInt.thy Tue Jan 16 12:20:52 2001 +0100
@@ -7,11 +7,11 @@
RealInt = RealOrd +
-constdefs
- real_of_int :: int => real
- "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ``
- {(preal_of_prat(prat_of_pnat(pnat_of_nat i)),
- preal_of_prat(prat_of_pnat(pnat_of_nat j)))})"
-
+defs
+ (*overloaded*)
+ real_of_int_def
+ "real z == Abs_REAL(UN (i,j): Rep_Integ z. realrel ``
+ {(preal_of_prat(prat_of_pnat(pnat_of_nat i)),
+ preal_of_prat(prat_of_pnat(pnat_of_nat j)))})"
end
--- a/src/HOL/Real/RealOrd.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealOrd.ML Tue Jan 16 12:20:52 2001 +0100
@@ -302,45 +302,45 @@
by (etac (inj_pnat_of_nat RS injD) 1);
qed "inj_real_of_posnat";
-Goalw [real_of_nat_def] "real_of_nat 0 = 0";
+Goalw [real_of_nat_def] "real (0::nat) = 0";
by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
qed "real_of_nat_zero";
-Goalw [real_of_nat_def] "real_of_nat 1 = 1r";
+Goalw [real_of_nat_def] "real (1::nat) = 1r";
by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1);
qed "real_of_nat_one";
Addsimps [real_of_nat_zero, real_of_nat_one];
Goalw [real_of_nat_def]
- "real_of_nat (m + n) = real_of_nat m + real_of_nat n";
+ "real (m + n) = real (m::nat) + real n";
by (simp_tac (simpset() addsimps
[real_of_posnat_add,real_add_assoc RS sym]) 1);
qed "real_of_nat_add";
Addsimps [real_of_nat_add];
(*Not for addsimps: often the LHS is used to represent a positive natural*)
-Goalw [real_of_nat_def] "real_of_nat (Suc n) = real_of_nat n + 1r";
+Goalw [real_of_nat_def] "real (Suc n) = real n + 1r";
by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1);
qed "real_of_nat_Suc";
Goalw [real_of_nat_def, real_of_posnat_def]
- "(real_of_nat n < real_of_nat m) = (n < m)";
+ "(real (n::nat) < real m) = (n < m)";
by Auto_tac;
qed "real_of_nat_less_iff";
AddIffs [real_of_nat_less_iff];
-Goal "(real_of_nat n <= real_of_nat m) = (n <= m)";
+Goal "(real (n::nat) <= real m) = (n <= m)";
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
qed "real_of_nat_le_iff";
AddIffs [real_of_nat_le_iff];
-Goal "inj real_of_nat";
+Goal "inj (real :: nat => real)";
by (rtac injI 1);
by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD],
simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
qed "inj_real_of_nat";
-Goal "0 <= real_of_nat n";
+Goal "0 <= real (n::nat)";
by (induct_tac "n" 1);
by (auto_tac (claset(),
simpset () addsimps [real_of_nat_Suc]));
@@ -350,7 +350,7 @@
qed "real_of_nat_ge_zero";
AddIffs [real_of_nat_ge_zero];
-Goal "real_of_nat (m * n) = real_of_nat m * real_of_nat n";
+Goal "real (m * n) = real (m::nat) * real n";
by (induct_tac "m" 1);
by (auto_tac (claset(),
simpset() addsimps [real_of_nat_Suc,
@@ -358,33 +358,23 @@
qed "real_of_nat_mult";
Addsimps [real_of_nat_mult];
-Goal "(real_of_nat n = real_of_nat m) = (n = m)";
+Goal "(real (n::nat) = real m) = (n = m)";
by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
qed "real_of_nat_eq_cancel";
Addsimps [real_of_nat_eq_cancel];
-Goal "n <= m --> real_of_nat (m - n) = real_of_nat m + (-real_of_nat n)";
+Goal "n <= m --> real (m - n) = real (m::nat) - real n";
by (induct_tac "m" 1);
by (auto_tac (claset(),
- simpset() addsimps [Suc_diff_le, le_Suc_eq, real_of_nat_Suc,
- real_of_nat_zero] @ real_add_ac));
-qed_spec_mp "real_of_nat_minus";
+ simpset() addsimps [real_diff_def, Suc_diff_le, le_Suc_eq,
+ real_of_nat_Suc, real_of_nat_zero] @ real_add_ac));
+qed_spec_mp "real_of_nat_diff";
-Goalw [real_diff_def]
- "n < m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n";
-by (auto_tac (claset() addIs [real_of_nat_minus], simpset()));
-qed "real_of_nat_diff";
-
-Goalw [real_diff_def]
- "n <= m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n";
-by (etac real_of_nat_minus 1);
-qed "real_of_nat_diff2";
-
-Goal "(real_of_nat n = 0) = (n = 0)";
+Goal "(real (n::nat) = 0) = (n = 0)";
by (auto_tac (claset() addIs [inj_real_of_nat RS injD], simpset()));
qed "real_of_nat_zero_iff";
-Goal "neg z ==> real_of_nat (nat z) = 0";
+Goal "neg z ==> real (nat z) = 0";
by (asm_simp_tac (simpset() addsimps [neg_nat, real_of_nat_zero]) 1);
qed "real_of_nat_neg_int";
Addsimps [real_of_nat_neg_int];
--- a/src/HOL/Real/RealPow.ML Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealPow.ML Tue Jan 16 12:20:52 2001 +0100
@@ -133,7 +133,7 @@
by (auto_tac (claset() addIs [order_less_imp_le], simpset()));
qed "two_realpow_ge_one";
-Goal "real_of_nat n < #2 ^ n";
+Goal "real (n::nat) < #2 ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
by (stac real_mult_2 1);
@@ -319,13 +319,13 @@
realpow_not_zero] @ real_mult_ac));
qed "realpow_diff";
-Goal "real_of_nat (m) ^ n = real_of_nat (m ^ n)";
+Goal "real (m::nat) ^ n = real (m ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset(),
simpset() addsimps [real_of_nat_one, real_of_nat_mult]));
qed "realpow_real_of_nat";
-Goal "#0 < real_of_nat (2 ^ n)";
+Goal "#0 < real (2 ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset(),
simpset() addsimps [real_of_nat_mult, real_zero_less_mult_iff]));