--- a/src/HOL/Hyperreal/HRealAbs.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.ML Thu Jan 04 10:23:01 2001 +0100
@@ -204,3 +204,52 @@
"abs (hypreal_of_real r) = hypreal_of_real (abs r)";
by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs]));
qed "hypreal_of_real_hrabs";
+
+
+(*----------------------------------------------------------------------------
+ Embedding of the naturals in the hyperreals
+ ----------------------------------------------------------------------------*)
+
+Goalw [hypreal_of_nat_def]
+ "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)";
+by (simp_tac (simpset() addsimps [hypreal_of_real_add, real_of_nat_add]) 1);
+qed "hypreal_of_nat_add";
+
+Goalw [hypreal_of_nat_def]
+ "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
+by (auto_tac (claset() addIs [hypreal_add_less_mono1], simpset()));
+qed "hypreal_of_nat_less_iff";
+Addsimps [hypreal_of_nat_less_iff RS sym];
+
+(*------------------------------------------------------------*)
+(* naturals embedded in hyperreals *)
+(* is a hyperreal c.f. NS extension *)
+(*------------------------------------------------------------*)
+
+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})";
+by Auto_tac;
+qed "hypreal_of_nat_iff";
+
+Goal "inj hypreal_of_nat";
+by (simp_tac (simpset() addsimps [inj_on_def, hypreal_of_nat_def]) 1);
+qed "inj_hypreal_of_nat";
+
+Goalw [hypreal_of_nat_def]
+ "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr";
+by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1);
+qed "hypreal_of_nat_Suc";
+
+(*"neg" is used in rewrite rules for binary comparisons*)
+Goal "hypreal_of_nat (number_of v :: nat) = \
+\ (if neg (number_of v) then #0 \
+\ else (number_of v :: hypreal))";
+by (simp_tac (simpset() addsimps [hypreal_of_nat_def]) 1);
+qed "hypreal_of_nat_number_of";
+Addsimps [hypreal_of_nat_number_of];
+
+Goal "hypreal_of_nat 0 = #0";
+by (simp_tac (simpset() delsimps [numeral_0_eq_0]
+ addsimps [numeral_0_eq_0 RS sym]) 1);
+qed "hypreal_of_nat_zero";
+Addsimps [hypreal_of_nat_zero];
--- a/src/HOL/Hyperreal/HRealAbs.thy Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.thy Thu Jan 04 10:23:01 2001 +0100
@@ -9,4 +9,9 @@
defs
hrabs_def "abs r == if (0::hypreal) <=r then r else -r"
+constdefs
+
+ hypreal_of_nat :: nat => hypreal
+ "hypreal_of_nat n == hypreal_of_real (real_of_nat n)"
+
end
\ No newline at end of file
--- a/src/HOL/Hyperreal/HSeries.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HSeries.ML Thu Jan 04 10:23:01 2001 +0100
@@ -195,7 +195,7 @@
by (simp_tac (HOL_ss addsimps
[one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypreal_diff, real_of_nat_def]));
+ simpset() addsimps [sumhr, hypreal_diff, real_of_nat_Suc]));
qed "sumhr_hypreal_omega_minus_one";
Goalw [hypnat_zero_def, hypnat_omega_def]
@@ -211,8 +211,8 @@
\ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \
\ (hypreal_of_nat (na - m) * hypreal_of_real r)";
by (auto_tac (claset() addSDs [sumr_interval_const],
- simpset() addsimps [sumhr,hypreal_of_nat_real_of_nat,
- hypreal_of_real_def,hypreal_mult]));
+ simpset() addsimps [sumhr,hypreal_of_nat_def,
+ hypreal_of_real_def, hypreal_mult]));
qed "sumhr_interval_const";
Goalw [hypnat_zero_def]
--- a/src/HOL/Hyperreal/HyperBin.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HyperBin.ML Thu Jan 04 10:23:01 2001 +0100
@@ -172,15 +172,6 @@
hypreal_add_number_of_diff1, hypreal_add_number_of_diff2];
-(*"neg" is used in rewrite rules for binary comparisons*)
-Goal "hypreal_of_nat (number_of v :: nat) = \
-\ (if neg (number_of v) then #0 \
-\ else (number_of v :: hypreal))";
-by (simp_tac (simpset() addsimps [hypreal_of_nat_real_of_nat]) 1);
-qed "hypreal_of_nat_number_of";
-Addsimps [hypreal_of_nat_number_of];
-
-
(**** Simprocs for numeric literals ****)
(** Combining of literal coefficients in sums of products **)
--- a/src/HOL/Hyperreal/HyperDef.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HyperDef.ML Thu Jan 04 10:23:01 2001 +0100
@@ -1227,49 +1227,6 @@
qed "hypreal_minus_eq_cancel";
Addsimps [hypreal_minus_eq_cancel];
-Goal "x < x + 1hr";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_add, hypreal_one_def,hypreal_less]));
-qed "hypreal_less_self_add_one";
-Addsimps [hypreal_less_self_add_one];
-
-(*??DELETE MOST OF THE FOLLOWING??*)
-Goal "((x::hypreal) + x = y + y) = (x = y)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add]));
-by (ALLGOALS(Ultra_tac));
-qed "hypreal_add_self_cancel";
-Addsimps [hypreal_add_self_cancel];
-
-Goal "(y = x + - y + x) = (y = (x::hypreal))";
-by Auto_tac;
-by (dres_inst_tac [("x1","y")]
- (hypreal_add_right_cancel RS iffD2) 1);
-by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
-qed "hypreal_add_self_minus_cancel";
-Addsimps [hypreal_add_self_minus_cancel];
-
-Goal "(y = x + (- y + x)) = (y = (x::hypreal))";
-by (asm_full_simp_tac (simpset() addsimps
- [hypreal_add_assoc RS sym])1);
-qed "hypreal_add_self_minus_cancel2";
-Addsimps [hypreal_add_self_minus_cancel2];
-
-(* of course, can prove this by "transfer" as well *)
-Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))";
-by Auto_tac;
-by (dres_inst_tac [("x1","z")]
- (hypreal_add_right_cancel RS iffD2) 1);
-by (asm_full_simp_tac (simpset() addsimps
- [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
- delsimps [hypreal_minus_add_distrib]) 1);
-by (asm_full_simp_tac (simpset() addsimps
- [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1);
-qed "hypreal_add_self_minus_cancel3";
-Addsimps [hypreal_add_self_minus_cancel3];
-
Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))";
by (rtac hypreal_less_minus_iff2 1);
qed "hypreal_less_eq_diff";
--- a/src/HOL/Hyperreal/HyperDef.thy Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Thu Jan 04 10:23:01 2001 +0100
@@ -44,11 +44,11 @@
(* an infinite number = [<1,2,3,...>] *)
omega_def
- "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})"
+ "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_posnat n)})"
+ "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)})"
@@ -67,14 +67,6 @@
hypreal_of_real :: real => hypreal
"hypreal_of_real r == Abs_hypreal(hyprel^^{%n::nat. r})"
-
- (* n::nat --> (n+1)::hypreal *)
- hypreal_of_posnat :: nat => hypreal
- "hypreal_of_posnat n == (hypreal_of_real(real_of_preal
- (preal_of_prat(prat_of_pnat(pnat_of_nat n)))))"
-
- hypreal_of_nat :: nat => hypreal
- "hypreal_of_nat n == hypreal_of_posnat n + -1hr"
defs
--- a/src/HOL/Hyperreal/HyperNat.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.ML Thu Jan 04 10:23:01 2001 +0100
@@ -41,7 +41,7 @@
AddSEs [hypnatrelE];
Goalw [hypnatrel_def] "(x,x): hypnatrel";
-by (Auto_tac);
+by Auto_tac;
qed "hypnatrel_refl";
Goalw [hypnatrel_def] "(x,y): hypnatrel --> (y,x):hypnatrel";
@@ -50,7 +50,7 @@
Goalw [hypnatrel_def]
"(x,y): hypnatrel --> (y,z):hypnatrel --> (x,z):hypnatrel";
-by (Auto_tac);
+by Auto_tac;
by (Fuf_tac 1);
qed_spec_mp "hypnatrel_trans";
@@ -87,7 +87,7 @@
Goalw [hypnatrel_def] "x: hypnatrel ^^ {x}";
by (Step_tac 1);
-by (Auto_tac);
+by Auto_tac;
qed "lemma_hypnatrel_refl";
Addsimps [lemma_hypnatrel_refl];
@@ -100,7 +100,7 @@
Goal "Rep_hypnat x ~= {}";
by (cut_inst_tac [("x","x")] Rep_hypnat 1);
-by (Auto_tac);
+by Auto_tac;
qed "Rep_hypnat_nonempty";
Addsimps [Rep_hypnat_nonempty];
@@ -117,7 +117,7 @@
by (rtac equiv_hypnatrel 1);
by (Fast_tac 1);
by (rtac ccontr 1 THEN rotate_tac 1 1);
-by (Auto_tac);
+by Auto_tac;
qed "inj_hypnat_of_nat";
val [prem] = Goal
@@ -376,7 +376,7 @@
(*** (hypnat) one and zero are distinct ***)
Goalw [hypnat_zero_def,hypnat_one_def] "(0::hypnat) ~= 1hn";
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_zero_not_eq_one";
Addsimps [hypnat_zero_not_eq_one];
Addsimps [hypnat_zero_not_eq_one RS not_sym];
@@ -404,7 +404,7 @@
qed "hypnat_less_iff";
Goalw [hypnat_less_def]
- "!!P. [| {n. X n < Y n} : FreeUltrafilterNat; \
+ "[| {n. X n < Y n} : FreeUltrafilterNat; \
\ X : Rep_hypnat(P); \
\ Y : Rep_hypnat(Q) |] ==> P < (Q::hypnat)";
by (Fast_tac 1);
@@ -416,11 +416,11 @@
\ !!X. X : Rep_hypnat(R1) ==> P; \
\ !!Y. Y : Rep_hypnat(R2) ==> P |] \
\ ==> P";
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_lessE";
Goalw [hypnat_less_def]
- "!!R1. R1 < (R2::hypnat) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
+ "R1 < (R2::hypnat) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
\ X : Rep_hypnat(R1) & \
\ Y : Rep_hypnat(R2))";
by (Fast_tac 1);
@@ -437,7 +437,7 @@
Goalw [hypnat_less_def,hypnat_zero_def] "~ n<(0::hypnat)";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (Auto_tac);
+by Auto_tac;
by (Fuf_empty_tac 1);
qed "hypnat_not_less0";
AddIffs [hypnat_not_less0];
@@ -460,9 +460,9 @@
by (res_inst_tac [("z","R3")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [hypnat_less_def]));
by (res_inst_tac [("x","X")] exI 1);
-by (Auto_tac);
+by Auto_tac;
by (res_inst_tac [("x","Ya")] exI 1);
-by (Auto_tac);
+by Auto_tac;
by (Fuf_tac 1);
qed "hypnat_less_trans";
@@ -530,12 +530,12 @@
Goalw [hypnatrel_def] "EX x. x: hypnatrel ^^ {%n. 0}";
by (res_inst_tac [("x","%n. 0")] exI 1);
by (Step_tac 1);
-by (Auto_tac);
+by Auto_tac;
qed "lemma_hypnatrel_0_mem";
(* linearity is actually proved further down! *)
-Goalw [hypnat_zero_def,
- hypnat_less_def]"(0::hypnat) < x | x = 0 | x < 0";
+Goalw [hypnat_zero_def, hypnat_less_def]
+ "(0::hypnat) < x | x = 0 | x < 0";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (Auto_tac );
by (REPEAT(Step_tac 1));
@@ -543,29 +543,28 @@
by (Fuf_tac 1);
qed "hypnat_trichotomy";
-Goal "!!x. [| (0::hypnat) < x ==> P; \
-\ x = 0 ==> P; \
-\ x < 0 ==> P |] ==> P";
+Goal "!!P. [| (0::hypnat) < x ==> P; \
+\ x = 0 ==> P; \
+\ x < 0 ==> P |] ==> P";
by (cut_inst_tac [("x","x")] hypnat_trichotomy 1);
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_trichotomyE";
-(*------------------------------------------------------------------------------
+(*----------------------------------------------------------------------------
More properties of <
- ------------------------------------------------------------------------------*)
+ ----------------------------------------------------------------------------*)
Goal "!!(A::hypnat). A < B ==> A + C < B + C";
by (res_inst_tac [("z","A")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","B")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","C")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [hypnat_less_def,hypnat_add]));
+by (auto_tac (claset(), simpset() addsimps [hypnat_less_def,hypnat_add]));
by (REPEAT(Step_tac 1));
by (Fuf_tac 1);
qed "hypnat_add_less_mono1";
Goal "!!(A::hypnat). A < B ==> C + A < C + B";
by (auto_tac (claset() addIs [hypnat_add_less_mono1],
- simpset() addsimps [hypnat_add_commute]));
+ simpset() addsimps [hypnat_add_commute]));
qed "hypnat_add_less_mono2";
Goal "!!k l::hypnat. [|i<j; k<l |] ==> i + k < j + l";
@@ -598,16 +597,27 @@
by (Fuf_tac 1);
qed "hypnat_linear";
-Goal
- "!!(x::hypnat). [| x < y ==> P; x = y ==> P; \
-\ y < x ==> P |] ==> P";
+Goal "!!(x::hypnat). [| x < y ==> P; x = y ==> P; \
+\ y < x ==> P |] ==> P";
by (cut_inst_tac [("x","x"),("y","y")] hypnat_linear 1);
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_linear_less2";
-(*------------------------------------------------------------------------------
+Goal "((w::hypnat) ~= z) = (w<z | z<w)";
+by (cut_facts_tac [hypnat_linear] 1);
+by Auto_tac;
+qed "hypnat_neq_iff";
+
+(* Axiom 'order_less_le' of class 'order': *)
+Goal "(w::hypnat) < z = (w <= z & w ~= z)";
+by (simp_tac (simpset() addsimps [hypnat_le_def, hypnat_neq_iff]) 1);
+by (blast_tac (claset() addIs [hypnat_less_asym]) 1);
+qed "hypnat_less_le";
+
+(*----------------------------------------------------------------------------
Properties of <=
- ------------------------------------------------------------------------------*)
+ ----------------------------------------------------------------------------*)
+
(*------ hypnat le iff nat le a.e ------*)
Goalw [hypnat_le_def,le_def]
"(Abs_hypnat(hypnatrel^^{%n. X n}) <= \
@@ -620,25 +630,8 @@
(*---------------------------------------------------------*)
(*---------------------------------------------------------*)
-Goalw [hypnat_le_def] "!!w. ~(w < z) ==> z <= (w::hypnat)";
-by (assume_tac 1);
-qed "hypnat_leI";
-Goalw [hypnat_le_def] "!!w. z<=w ==> ~(w<(z::hypnat))";
-by (assume_tac 1);
-qed "hypnat_leD";
-
-val hypnat_leE = make_elim hypnat_leD;
-
-Goal "!!w. (~(w < z)) = (z <= (w::hypnat))";
-by (fast_tac (claset() addSIs [hypnat_leI,hypnat_leD]) 1);
-qed "hypnat_less_le_iff";
-
-Goalw [hypnat_le_def] "!!z. ~ z <= w ==> w<(z::hypnat)";
-by (Fast_tac 1);
-qed "not_hypnat_leE";
-
-Goalw [hypnat_le_def] "!!z. z < w ==> z <= (w::hypnat)";
+Goalw [hypnat_le_def] "z < w ==> z <= (w::hypnat)";
by (fast_tac (claset() addEs [hypnat_less_asym]) 1);
qed "hypnat_less_imp_le";
@@ -647,59 +640,53 @@
by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1);
qed "hypnat_le_imp_less_or_eq";
-Goalw [hypnat_le_def] "!!z. z<w | z=w ==> z <=(w::hypnat)";
+Goalw [hypnat_le_def] "z<w | z=w ==> z <=(w::hypnat)";
by (cut_facts_tac [hypnat_linear] 1);
-by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1);
+by (blast_tac (claset() addDs [hypnat_less_irrefl,hypnat_less_asym]) 1);
qed "hypnat_less_or_eq_imp_le";
Goal "(x <= (y::hypnat)) = (x < y | x=y)";
-by (REPEAT(ares_tac [iffI, hypnat_less_or_eq_imp_le, hypnat_le_imp_less_or_eq] 1));
-qed "hypnat_le_eq_less_or_eq";
+by (REPEAT(ares_tac [iffI, hypnat_less_or_eq_imp_le,
+ hypnat_le_imp_less_or_eq] 1));
+qed "hypnat_le_less";
+
+(* Axiom 'linorder_linear' of class 'linorder': *)
+Goal "(z::hypnat) <= w | w <= z";
+by (simp_tac (simpset() addsimps [hypnat_le_less]) 1);
+by (cut_facts_tac [hypnat_linear] 1);
+by (Blast_tac 1);
+qed "hypnat_le_linear";
Goal "w <= (w::hypnat)";
-by (simp_tac (simpset() addsimps [hypnat_le_eq_less_or_eq]) 1);
+by (simp_tac (simpset() addsimps [hypnat_le_less]) 1);
qed "hypnat_le_refl";
Addsimps [hypnat_le_refl];
-val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::hypnat)";
-by (dtac hypnat_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [hypnat_less_trans]) 1);
-qed "hypnat_le_less_trans";
-
-Goal "!! (i::hypnat). [| i < j; j <= k |] ==> i < k";
-by (dtac hypnat_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [hypnat_less_trans]) 1);
-qed "hypnat_less_le_trans";
-
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::hypnat)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::hypnat)";
by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
- rtac hypnat_less_or_eq_imp_le, fast_tac (claset() addIs [hypnat_less_trans])]);
+ rtac hypnat_less_or_eq_imp_le,
+ fast_tac (claset() addIs [hypnat_less_trans])]);
qed "hypnat_le_trans";
-Goal "!!z. [| z <= w; w <= z |] ==> z = (w::hypnat)";
+Goal "[| z <= w; w <= z |] ==> z = (w::hypnat)";
by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym])]);
qed "hypnat_le_anti_sym";
-Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::hypnat)";
-by (rtac not_hypnat_leE 1);
-by (fast_tac (claset() addDs [hypnat_le_imp_less_or_eq]) 1);
-qed "not_less_not_eq_hypnat_less";
-
-Goal "!!x. [| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x * y";
+Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x * y";
by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [hypnat_mult_order,
- hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl]));
+by (auto_tac (claset() addIs [hypnat_mult_order, hypnat_less_imp_le],
+ simpset() addsimps [hypnat_le_refl]));
qed "hypnat_le_mult_order";
Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def]
"(0::hypnat) < 1hn";
by (res_inst_tac [("x","%n. 0")] exI 1);
by (res_inst_tac [("x","%n. 1")] exI 1);
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_zero_less_one";
-Goal "!!x. [| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x + y";
+Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x + y";
by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
by (auto_tac (claset() addIs [hypnat_add_order,
hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl]));
@@ -752,7 +739,7 @@
Goal "(x::hypnat) < x + 1hn";
by (cut_facts_tac [hypnat_zero_less_one
RS hypnat_add_less_mono2] 1);
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_add_one_self_less";
Addsimps [hypnat_add_one_self_less];
@@ -816,7 +803,7 @@
Goalw [hypnat_le_def,le_def]
"(z1 <= z2) = (hypnat_of_nat z1 <= hypnat_of_nat z2)";
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_of_nat_le_iff";
Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat 1 = 1hn";
@@ -837,8 +824,8 @@
by (full_simp_tac (simpset() addsimps [hypnat_of_nat_zero_iff]) 1);
qed "hypnat_of_nat_not_zero_iff";
-goalw HyperNat.thy [hypnat_of_nat_def,hypnat_one_def]
- "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1hn";
+Goalw [hypnat_of_nat_def,hypnat_one_def]
+ "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1hn";
by (auto_tac (claset(),simpset() addsimps [hypnat_add]));
qed "hypnat_of_nat_Suc";
@@ -847,7 +834,7 @@
---------------------------------------------------------------------------------*)
Goal "hypnatrel^^{%n::nat. n} : hypnat";
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_omega";
Goalw [hypnat_omega_def] "Rep_hypnat(whn) : hypnat";
@@ -867,111 +854,110 @@
Goal "hypnat_of_nat x ~= whn";
by (cut_facts_tac [not_ex_hypnat_of_nat_eq_omega] 1);
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_of_nat_not_eq_omega";
Addsimps [hypnat_of_nat_not_eq_omega RS not_sym];
(*-----------------------------------------------------------
- Properties of the set SHNat of embedded natural numbers
+ Properties of the set SNat of embedded natural numbers
(cf. set SReal in NSA.thy/NSA.ML)
----------------------------------------------------------*)
-(* Infinite hypernatural not in embedded SHNat *)
-Goalw [SHNat_def] "whn ~: SHNat";
-by (Auto_tac);
+(* Infinite hypernatural not in embedded SNat *)
+Goalw [SHNat_def] "whn ~: SNat";
+by Auto_tac;
qed "SHNAT_omega_not_mem";
Addsimps [SHNAT_omega_not_mem];
(*-----------------------------------------------------------------------
- Closure laws for members of (embedded) set standard naturals SHNat
+ Closure laws for members of (embedded) set standard naturals SNat
-----------------------------------------------------------------------*)
Goalw [SHNat_def]
- "!!x. [| x: SHNat; y: SHNat |] ==> x + y: SHNat";
+ "!!x::hypnat. [| x: SNat; y: SNat |] ==> x + y: SNat";
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. [| x: SHNat; y: SHNat |] ==> x - y: SHNat";
+ "!!x::hypnat. [| x: SNat; y: SNat |] ==> x - y: SNat";
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. [| x: SHNat; y: SHNat |] ==> x * y: SHNat";
+ "!!x::hypnat. [| x: SNat; y: SNat |] ==> x * y: SNat";
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. [| x + y : SHNat; y: SHNat |] ==> x: SHNat";
+Goal"!!x::hypnat. [| x + y : SNat; y: SNat |] ==> x: SNat";
by (dres_inst_tac [("x","x+y")] SHNat_minus 1);
-by (Auto_tac);
+by Auto_tac;
qed "SHNat_add_cancel";
-Goalw [SHNat_def] "hypnat_of_nat x : SHNat";
+Goalw [SHNat_def] "hypnat_of_nat x : SNat";
by (Blast_tac 1);
qed "SHNat_hypnat_of_nat";
Addsimps [SHNat_hypnat_of_nat];
-Goal "hypnat_of_nat 1 : SHNat";
+Goal "hypnat_of_nat 1 : SNat";
by (Simp_tac 1);
qed "SHNat_hypnat_of_nat_one";
-Goal "hypnat_of_nat 0 : SHNat";
+Goal "hypnat_of_nat 0 : SNat";
by (Simp_tac 1);
qed "SHNat_hypnat_of_nat_zero";
-Goal "1hn : SHNat";
+Goal "1hn : SNat";
by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_one,
hypnat_of_nat_one RS sym]) 1);
qed "SHNat_one";
-Goal "0 : SHNat";
+Goal "(0::hypnat) : SNat";
by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_zero,
- hypnat_of_nat_zero RS sym]) 1);
+ hypnat_of_nat_zero RS sym]) 1);
qed "SHNat_zero";
Addsimps [SHNat_hypnat_of_nat_one,SHNat_hypnat_of_nat_zero,
SHNat_one,SHNat_zero];
-Goal "1hn + 1hn : SHNat";
+Goal "1hn + 1hn : SNat";
by (rtac ([SHNat_one,SHNat_one] MRS SHNat_add) 1);
qed "SHNat_two";
-Goalw [SHNat_def] "{x. hypnat_of_nat x : SHNat} = (UNIV::nat set)";
-by (Auto_tac);
+Goalw [SHNat_def] "{x. hypnat_of_nat x : SNat} = (UNIV::nat set)";
+by Auto_tac;
qed "SHNat_UNIV_nat";
-Goalw [SHNat_def] "(x: SHNat) = (EX y. x = hypnat_of_nat y)";
-by (Auto_tac);
+Goalw [SHNat_def] "(x: SNat) = (EX y. x = hypnat_of_nat y)";
+by Auto_tac;
qed "SHNat_iff";
-Goalw [SHNat_def] "hypnat_of_nat ``(UNIV::nat set) = SHNat";
-by (Auto_tac);
+Goalw [SHNat_def] "hypnat_of_nat ``(UNIV::nat set) = SNat";
+by Auto_tac;
qed "hypnat_of_nat_image";
-Goalw [SHNat_def] "inv hypnat_of_nat ``SHNat = (UNIV::nat set)";
-by (Auto_tac);
+Goalw [SHNat_def] "inv hypnat_of_nat ``SNat = (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]
- "!!P. [| EX x. x: P; P <= SHNat |] ==> \
-\ EX Q. P = hypnat_of_nat `` Q";
+ "[| EX x. x: P; P <= SNat |] ==> EX Q. P = hypnat_of_nat `` Q";
by (Best_tac 1);
qed "SHNat_hypnat_of_nat_image";
Goalw [SHNat_def]
- "SHNat = hypnat_of_nat `` (UNIV::nat set)";
-by (Auto_tac);
+ "SNat = hypnat_of_nat `` (UNIV::nat set)";
+by Auto_tac;
qed "SHNat_hypnat_of_nat_iff";
-Goalw [SHNat_def] "SHNat <= (UNIV::hypnat set)";
-by (Auto_tac);
+Goalw [SHNat_def] "SNat <= (UNIV::hypnat set)";
+by Auto_tac;
qed "SHNat_subset_UNIV";
Goal "{n. n <= Suc m} = {n. n <= m} Un {n. n = Suc m}";
@@ -990,9 +976,8 @@
qed "lemma_unbounded_set";
Addsimps [lemma_unbounded_set];
-Goalw [SHNat_def,hypnat_of_nat_def,
- hypnat_less_def,hypnat_omega_def]
- "ALL n: SHNat. n < whn";
+Goalw [SHNat_def,hypnat_of_nat_def, hypnat_less_def,hypnat_omega_def]
+ "ALL n: SNat. n < whn";
by (Clarify_tac 1);
by (auto_tac (claset() addSIs [exI],simpset()));
qed "hypnat_omega_gt_SHNat";
@@ -1000,7 +985,7 @@
Goal "hypnat_of_nat n < whn";
by (cut_facts_tac [hypnat_omega_gt_SHNat] 1);
by (dres_inst_tac [("x","hypnat_of_nat n")] bspec 1);
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_of_nat_less_whn";
Addsimps [hypnat_of_nat_less_whn];
@@ -1011,13 +996,13 @@
Goal "0 < whn";
by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_zero_less_hypnat_omega";
Addsimps [hypnat_zero_less_hypnat_omega];
Goal "1hn < whn";
by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
-by (Auto_tac);
+by Auto_tac;
qed "hypnat_one_less_hypnat_omega";
Addsimps [hypnat_one_less_hypnat_omega];
@@ -1025,43 +1010,43 @@
Theorems about infinite hypernatural numbers -- HNatInfinite
-------------------------------------------------------------------------*)
Goalw [HNatInfinite_def,SHNat_def] "whn : HNatInfinite";
-by (Auto_tac);
+by Auto_tac;
qed "HNatInfinite_whn";
Addsimps [HNatInfinite_whn];
-Goalw [HNatInfinite_def] "!!x. x: SHNat ==> x ~: HNatInfinite";
+Goalw [HNatInfinite_def] "x: SNat ==> x ~: HNatInfinite";
by (Simp_tac 1);
qed "SHNat_not_HNatInfinite";
-Goalw [HNatInfinite_def] "!!x. x ~: HNatInfinite ==> x: SHNat";
+Goalw [HNatInfinite_def] "x ~: HNatInfinite ==> x: SNat";
by (Asm_full_simp_tac 1);
qed "not_HNatInfinite_SHNat";
-Goalw [HNatInfinite_def] "!!x. x ~: SHNat ==> x: HNatInfinite";
+Goalw [HNatInfinite_def] "x ~: SNat ==> x: HNatInfinite";
by (Simp_tac 1);
qed "not_SHNat_HNatInfinite";
-Goalw [HNatInfinite_def] "!!x. x: HNatInfinite ==> x ~: SHNat";
+Goalw [HNatInfinite_def] "x: HNatInfinite ==> x ~: SNat";
by (Asm_full_simp_tac 1);
qed "HNatInfinite_not_SHNat";
-Goal "(x: SHNat) = (x ~: HNatInfinite)";
+Goal "(x: SNat) = (x ~: HNatInfinite)";
by (blast_tac (claset() addSIs [SHNat_not_HNatInfinite,
not_HNatInfinite_SHNat]) 1);
qed "SHNat_not_HNatInfinite_iff";
-Goal "(x ~: SHNat) = (x: HNatInfinite)";
+Goal "(x ~: SNat) = (x: HNatInfinite)";
by (blast_tac (claset() addSIs [not_SHNat_HNatInfinite,
HNatInfinite_not_SHNat]) 1);
qed "not_SHNat_HNatInfinite_iff";
-Goal "x : SHNat | x : HNatInfinite";
+Goal "x : SNat | 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: SHNat. n < N}
+ numbers --- HNatInfinite = {N. ALL n: SNat. n < N}
-------------------------------------------------------------------*)
Goal "!!N (xa::nat=>nat). \
\ (ALL N. {n. xa n ~= N} : FreeUltrafilterNat) ==> \
@@ -1078,7 +1063,7 @@
(*** alternative definition ***)
Goalw [HNatInfinite_def,SHNat_def,hypnat_of_nat_def]
- "HNatInfinite = {N. ALL n:SHNat. n < N}";
+ "HNatInfinite = {N. ALL n:SNat. n < N}";
by (Step_tac 1);
by (dres_inst_tac [("x","Abs_hypnat \
\ (hypnatrel ^^ {%n. N})")] bspec 2);
@@ -1094,8 +1079,8 @@
(*--------------------------------------------------------------------
Alternative definition for HNatInfinite using Free ultrafilter
--------------------------------------------------------------------*)
-Goal "!!x. x : HNatInfinite ==> EX X: Rep_hypnat x. \
-\ ALL u. {n. u < X n}: FreeUltrafilterNat";
+Goal "x : HNatInfinite ==> EX X: Rep_hypnat x. \
+\ ALL u. {n. u < X n}: FreeUltrafilterNat";
by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
@@ -1108,26 +1093,25 @@
by (Fuf_tac 1);
qed "HNatInfinite_FreeUltrafilterNat";
-Goal "!!x. EX X: Rep_hypnat x. \
-\ ALL u. {n. u < X n}: FreeUltrafilterNat \
-\ ==> x: HNatInfinite";
+Goal "EX X: Rep_hypnat x. ALL u. {n. u < X n}: FreeUltrafilterNat \
+\ ==> x: HNatInfinite";
by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
by (rtac exI 1 THEN Auto_tac);
qed "FreeUltrafilterNat_HNatInfinite";
-Goal "!!x. (x : HNatInfinite) = (EX X: Rep_hypnat x. \
+Goal "(x : HNatInfinite) = (EX X: Rep_hypnat x. \
\ ALL u. {n. u < X n}: FreeUltrafilterNat)";
by (blast_tac (claset() addIs [HNatInfinite_FreeUltrafilterNat,
FreeUltrafilterNat_HNatInfinite]) 1);
qed "HNatInfinite_FreeUltrafilterNat_iff";
-Goal "!!x. x : HNatInfinite ==> 1hn < x";
+Goal "x : HNatInfinite ==> 1hn < x";
by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
qed "HNatInfinite_gt_one";
Addsimps [HNatInfinite_gt_one];
-Goal "!!x. 0 ~: HNatInfinite";
+Goal "0 ~: HNatInfinite";
by (auto_tac (claset(),simpset()
addsimps [HNatInfinite_iff]));
by (dres_inst_tac [("a","1hn")] equals0D 1);
@@ -1135,11 +1119,11 @@
qed "zero_not_mem_HNatInfinite";
Addsimps [zero_not_mem_HNatInfinite];
-Goal "!!x. x : HNatInfinite ==> x ~= 0";
-by (Auto_tac);
+Goal "x : HNatInfinite ==> x ~= 0";
+by Auto_tac;
qed "HNatInfinite_not_eq_zero";
-Goal "!!x. x : HNatInfinite ==> 1hn <= x";
+Goal "x : HNatInfinite ==> 1hn <= x";
by (blast_tac (claset() addIs [hypnat_less_imp_le,
HNatInfinite_gt_one]) 1);
qed "HNatInfinite_ge_one";
@@ -1148,7 +1132,7 @@
(*--------------------------------------------------
Closure Rules
--------------------------------------------------*)
-Goal "!!x. [| x: HNatInfinite; y: HNatInfinite |] \
+Goal "[| x: HNatInfinite; y: HNatInfinite |] \
\ ==> x + y: HNatInfinite";
by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
by (dtac bspec 1 THEN assume_tac 1);
@@ -1157,16 +1141,14 @@
by (Asm_full_simp_tac 1);
qed "HNatInfinite_add";
-Goal "!!x. [| x: HNatInfinite; y: SHNat |] \
-\ ==> x + y: HNatInfinite";
+Goal "[| x: HNatInfinite; y: SNat |] ==> 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 HyperNat.thy "!!x. [| x: HNatInfinite; y: SHNat |] \
-\ ==> x - y: HNatInfinite";
+Goal "[| x: HNatInfinite; y: SNat |] ==> 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);
@@ -1176,23 +1158,21 @@
simpset() addsimps [not_SHNat_HNatInfinite_iff,HNatInfinite_iff]));
qed "HNatInfinite_SHNat_diff";
-Goal
- "!!x. x: HNatInfinite ==> x + 1hn: HNatInfinite";
+Goal "x: HNatInfinite ==> x + 1hn: HNatInfinite";
by (auto_tac (claset() addIs [HNatInfinite_SHNat_add],
simpset()));
qed "HNatInfinite_add_one";
-Goal
- "!!x. x: HNatInfinite ==> x - 1hn: HNatInfinite";
+Goal "x: HNatInfinite ==> x - 1hn: HNatInfinite";
by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
by (dres_inst_tac [("x","x - 1hn"),("y","1hn")] SHNat_add 1);
by (auto_tac (claset(),simpset() addsimps
[not_SHNat_HNatInfinite_iff RS sym]));
qed "HNatInfinite_minus_one";
-Goal "!!x. x : HNatInfinite ==> EX y. x = y + 1hn";
+Goal "x : HNatInfinite ==> EX y. x = y + 1hn";
by (res_inst_tac [("x","x - 1hn")] exI 1);
-by (Auto_tac);
+by Auto_tac;
qed "HNatInfinite_is_Suc";
(*---------------------------------------------------------------
@@ -1200,23 +1180,21 @@
Obtained using the NS extension of the naturals
--------------------------------------------------------------*)
-Goalw [HNat_def,starset_def,
- hypreal_of_posnat_def,hypreal_of_real_def]
- "hypreal_of_posnat N : HNat";
-by (Auto_tac);
+Goalw [HNat_def,starset_def, hypreal_of_nat_def,hypreal_of_real_def]
+ "hypreal_of_nat N : HNat";
+by Auto_tac;
by (Ultra_tac 1);
-by (res_inst_tac [("x","Suc N")] exI 1);
-by (dtac sym 1 THEN auto_tac (claset(),simpset()
- addsimps [real_of_preal_real_of_nat_Suc]));
-qed "HNat_hypreal_of_posnat";
-Addsimps [HNat_hypreal_of_posnat];
+by (res_inst_tac [("x","N")] exI 1);
+by Auto_tac;
+qed "HNat_hypreal_of_nat";
+Addsimps [HNat_hypreal_of_nat];
Goalw [HNat_def,starset_def]
"[| x: HNat; y: HNat |] ==> x + y: HNat";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
- simpset() addsimps [hypreal_add]));
+ simpset() addsimps [hypreal_add]));
by (Ultra_tac 1);
by (dres_inst_tac [("t","Y xb")] sym 1);
by (auto_tac (claset(),simpset() addsimps [real_of_nat_add RS sym]));
@@ -1236,10 +1214,10 @@
(*---------------------------------------------------------------
Embedding of the hypernaturals into the hyperreal
--------------------------------------------------------------*)
-(*** A lemma that should have been derived a long time ago! ***)
+
Goal "(Ya : hyprel ^^{%n. f(n)}) = \
-\ ({n. f n = Ya n} : FreeUltrafilterNat)";
-by (Auto_tac);
+\ ({n. f n = Ya n} : FreeUltrafilterNat)";
+by Auto_tac;
qed "lemma_hyprel_FUFN";
Goalw [hypreal_of_hypnat_def]
@@ -1255,8 +1233,7 @@
by (rtac injI 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_of_hypnat,real_of_nat_eq_cancel]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat]));
qed "inj_hypreal_of_hypnat";
Goal "(hypreal_of_hypnat n = hypreal_of_hypnat m) = (n = m)";
@@ -1326,7 +1303,7 @@
Addsimps [hypnat_not_all_eq_zero];
Goal "n ~= 0 ==> (n <= 1hn) = (n = 1hn)";
-by (auto_tac (claset(),simpset() addsimps [hypnat_le_eq_less_or_eq]));
+by (auto_tac (claset(), simpset() addsimps [hypnat_le_less]));
qed "hypnat_le_one_eq_one";
Addsimps [hypnat_le_one_eq_one];
--- a/src/HOL/Hyperreal/HyperNat.thy Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Thu Jan 04 10:23:01 2001 +0100
@@ -21,29 +21,12 @@
"1hn" :: hypnat ("1hn")
"whn" :: hypnat ("whn")
-defs
-
- hypnat_zero_def "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})"
- hypnat_one_def "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})"
-
- (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
- hypnat_omega_def "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})"
-
-
constdefs
(* embedding the naturals in the hypernaturals *)
hypnat_of_nat :: nat => hypnat
"hypnat_of_nat m == Abs_hypnat(hypnatrel^^{%n::nat. m})"
- (* set of naturals embedded in the hypernaturals*)
- SHNat :: "hypnat set"
- "SHNat == {n. EX N. n = hypnat_of_nat N}"
-
- (* embedding the naturals in the hyperreals*)
- SNat :: "hypreal set"
- "SNat == {n. EX N. n = hypreal_of_nat N}"
-
(* 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"
@@ -51,7 +34,7 @@
(* the set of infinite hypernatural numbers *)
HNatInfinite :: "hypnat set"
- "HNatInfinite == {n. n ~: SHNat}"
+ "HNatInfinite == {n. n ~: SNat}"
(* explicit embedding of the hypernaturals in the hyperreals *)
hypreal_of_hypnat :: hypnat => hypreal
@@ -59,6 +42,23 @@
hyprel^^{%n::nat. real_of_nat (X n)})"
defs
+
+ (** the overloaded constant "SNat" **)
+
+ (* set of naturals embedded in the hyperreals*)
+ SNat_def "SNat == {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}"
+
+ (** hypernatural arithmetic **)
+
+ hypnat_zero_def "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})"
+ hypnat_one_def "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})"
+
+ (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
+ hypnat_omega_def "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})"
+
hypnat_add_def
"P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
hypnatrel^^{%n::nat. X n + Y n})"
--- a/src/HOL/Hyperreal/HyperOrd.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.ML Thu Jan 04 10:23:01 2001 +0100
@@ -102,22 +102,22 @@
qed "hypreal_lt_zero_iff";
Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)";
-by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_lt_zero_iff RS sym]));
qed "hypreal_ge_zero_iff";
Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)";
-by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_gt_zero_iff RS sym]));
qed "hypreal_le_zero_iff";
Goalw [hypreal_zero_def]
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_less_def,hypreal_add]));
-by (auto_tac (claset() addSIs [exI],simpset() addsimps
- [hypreal_less_def,hypreal_add]));
-by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_less_def,hypreal_add]));
+by (auto_tac (claset() addSIs [exI],
+ simpset() addsimps [hypreal_less_def,hypreal_add]));
+by (ultra_tac (claset() addIs [real_add_order], simpset()) 1);
qed "hypreal_add_order";
Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y";
@@ -130,8 +130,8 @@
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSIs [exI],simpset() addsimps
- [hypreal_less_def,hypreal_mult]));
+by (auto_tac (claset() addSIs [exI],
+ simpset() addsimps [hypreal_less_def,hypreal_mult]));
by (ultra_tac (claset() addIs [rename_numerals real_mult_order],
simpset()) 1);
qed "hypreal_mult_order";
@@ -142,31 +142,6 @@
by (Asm_full_simp_tac 1);
qed "hypreal_mult_less_zero1";
-Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y";
-by (REPEAT(dtac order_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [hypreal_mult_order, order_less_imp_le],
- simpset()));
-qed "hypreal_le_mult_order";
-
-
-Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y";
-by (rtac hypreal_less_or_eq_imp_le 1);
-by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
-by Auto_tac;
-by (dtac order_le_imp_less_or_eq 1);
-by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
-qed "hypreal_mult_le_zero1";
-
-Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)";
-by (rtac hypreal_less_or_eq_imp_le 1);
-by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
-by Auto_tac;
-by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
-by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
-by (blast_tac (claset() addDs [hypreal_mult_order]
- addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
-qed "hypreal_mult_le_zero";
-
Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)";
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
by (dtac hypreal_mult_order 1 THEN assume_tac 1);
@@ -181,22 +156,6 @@
simpset() addsimps [real_zero_less_one, FreeUltrafilterNat_Nat_set]));
qed "hypreal_zero_less_one";
-Goal "1hr < 1hr + 1hr";
-by (rtac (hypreal_less_minus_iff RS iffD2) 1);
-by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
- hypreal_add_assoc]) 1);
-qed "hypreal_one_less_two";
-
-Goal "0 < 1hr + 1hr";
-by (rtac ([hypreal_zero_less_one,
- hypreal_one_less_two] MRS order_less_trans) 1);
-qed "hypreal_zero_less_two";
-
-Goal "1hr + 1hr ~= 0";
-by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
-qed "hypreal_two_not_zero";
-Addsimps [hypreal_two_not_zero];
-
Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y";
by (REPEAT(dtac order_le_imp_less_or_eq 1));
by (auto_tac (claset() addIs [hypreal_add_order, order_less_imp_le],
@@ -232,9 +191,9 @@
by (dtac hypreal_add_order 1 THEN assume_tac 1);
by (thin_tac "0 < y2 + - z2" 1);
by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
- delsimps [hypreal_minus_add_distrib]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
+ delsimps [hypreal_minus_add_distrib]));
qed "hypreal_add_less_mono";
Goal "(q1::hypreal) <= q2 ==> x + q1 <= x + q2";
@@ -322,7 +281,7 @@
Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z";
by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac order_le_imp_less_or_eq]);
-by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
+by (auto_tac (claset() addIs [hypreal_mult_less_mono1], simpset()));
qed "hypreal_mult_le_less_mono1";
Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y";
@@ -397,12 +356,6 @@
by (blast_tac (claset() addDs [hypreal_mult_zero_disj]) 1);
qed "hypreal_mult_is_0";
-Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
-by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_add_nonneg_eq_0_iff,
- hypreal_mult_is_0]) 1);
-qed "hypreal_squares_add_zero_iff";
-Addsimps [hypreal_squares_add_zero_iff];
-
Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order,
hypreal_add_nonneg_eq_0_iff, hypreal_mult_is_0]) 1);
@@ -435,58 +388,8 @@
(*----------------------------------------------------------------------------
- Embedding of the naturals in the hyperreals
+ Existence of infinite hyperreal number
----------------------------------------------------------------------------*)
-Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
-by (full_simp_tac (simpset() addsimps
- [pnat_one_iff RS sym,real_of_preal_def]) 1);
-by (fold_tac [real_one_def]);
-by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
-qed "hypreal_of_posnat_one";
-
-Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
-by (full_simp_tac (simpset() addsimps
- [real_of_preal_def,
- rename_numerals (real_one_def RS meta_eq_to_obj_eq),
- hypreal_add,hypreal_of_real_def,pnat_two_eq,
- hypreal_one_def, real_add,
- prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @
- pnat_add_ac) 1);
-qed "hypreal_of_posnat_two";
-
-(*FIXME: delete this and all posnat*)
-Goalw [hypreal_of_posnat_def]
- "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
-\ hypreal_of_posnat (n1 + n2) + 1hr";
-by (full_simp_tac (HOL_ss addsimps [hypreal_of_posnat_one RS sym,
- hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
- preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
-qed "hypreal_of_posnat_add";
-
-Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
-by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
-by (rtac (hypreal_of_posnat_add RS subst) 1);
-by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
-qed "hypreal_of_posnat_add_one";
-
-Goalw [real_of_posnat_def,hypreal_of_posnat_def]
- "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
-by (rtac refl 1);
-qed "hypreal_of_real_of_posnat";
-
-Goalw [hypreal_of_posnat_def]
- "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
-by Auto_tac;
-qed "hypreal_of_posnat_less_iff";
-
-Addsimps [hypreal_of_posnat_less_iff RS sym];
-(*---------------------------------------------------------------------------------
- Existence of infinite hyperreal number
- ---------------------------------------------------------------------------------*)
-
-Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
-by Auto_tac;
-qed "hypreal_omega";
Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
by (rtac Rep_hypreal 1);
@@ -496,20 +399,21 @@
(* use assumption that member FreeUltrafilterNat is not finite *)
(* a few lemmas first *)
-Goal "{n::nat. x = real_of_posnat n} = {} | \
-\ (EX y. {n::nat. x = real_of_posnat n} = {y})";
-by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
+Goal "{n::nat. x = real_of_nat n} = {} | \
+\ (EX y. {n::nat. x = real_of_nat 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_posnat n}";
+Goal "finite {n::nat. x = real_of_nat 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)";
-by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set
- RS FreeUltrafilterNat_finite]));
+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";
@@ -520,21 +424,25 @@
(* existence of infinitesimal number also not *)
(* corresponding to any real number *)
-Goal "{n::nat. x = inverse(real_of_posnat n)} = {} | \
-\ (EX y. {n::nat. x = inverse(real_of_posnat n)} = {y})";
-by (Step_tac 1 THEN Step_tac 1);
-by (auto_tac (claset() addIs [real_of_posnat_inverse_inj],simpset()));
+Goal "inverse (real_of_nat x) = inverse (real_of_nat 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})";
+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_posnat n)}";
+Goal "finite {n::nat. x = inverse(real_of_nat(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)";
-by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set
- RS FreeUltrafilterNat_finite]));
+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";
@@ -543,96 +451,28 @@
qed "hypreal_of_real_not_eq_epsilon";
Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
+by Auto_tac;
by (auto_tac (claset(),
- simpset() addsimps [rename_numerals real_of_posnat_not_eq_zero]));
+ simpset() addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym]));
qed "hypreal_epsilon_not_zero";
-Addsimps [rename_numerals real_of_posnat_not_eq_zero];
-Goalw [omega_def,hypreal_zero_def] "whr ~= 0";
-by (Simp_tac 1);
-qed "hypreal_omega_not_zero";
-
Goal "ehr = inverse(whr)";
by (asm_full_simp_tac (simpset() addsimps
[hypreal_inverse, omega_def, epsilon_def]) 1);
qed "hypreal_epsilon_inverse_omega";
-(*----------------------------------------------------------------
- Another embedding of the naturals in the
- hyperreals (see hypreal_of_posnat)
- ----------------------------------------------------------------*)
-Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0";
-by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
-qed "hypreal_of_nat_zero";
-
-Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
-by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
- hypreal_add_assoc]) 1);
-qed "hypreal_of_nat_one";
-
-Goalw [hypreal_of_nat_def]
- "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)";
-by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
-by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
- hypreal_add_assoc RS sym]) 1);
-qed "hypreal_of_nat_add";
-
-Goal "hypreal_of_nat 2 = 1hr + 1hr";
-by (simp_tac (simpset() addsimps [hypreal_of_nat_one
- RS sym,hypreal_of_nat_add]) 1);
-qed "hypreal_of_nat_two";
-
-Goalw [hypreal_of_nat_def]
- "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
-by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
-qed "hypreal_of_nat_less_iff";
-Addsimps [hypreal_of_nat_less_iff RS sym];
-
-(*------------------------------------------------------------*)
-(* naturals embedded in hyperreals *)
-(* is a hyperreal c.f. NS extension *)
-(*------------------------------------------------------------*)
-
-Goalw [hypreal_of_nat_def,real_of_nat_def]
- "hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
- hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
-qed "hypreal_of_nat_iff";
-
-Goal "inj hypreal_of_nat";
-by (rtac injI 1);
-by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
- simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
- real_add_right_cancel,inj_real_of_nat RS injD]));
-qed "inj_hypreal_of_nat";
-
-Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
- real_of_posnat_def,hypreal_one_def,real_of_nat_def]
- "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
-by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
-qed "hypreal_of_nat_real_of_nat";
-
-Goal "hypreal_of_posnat (Suc n) = hypreal_of_posnat n + 1hr";
-by (stac (hypreal_of_posnat_add_one RS sym) 1);
-by (Simp_tac 1);
-qed "hypreal_of_posnat_Suc";
-
-Goalw [hypreal_of_nat_def]
- "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr";
-by (simp_tac (simpset() addsimps [hypreal_of_posnat_Suc] @ hypreal_add_ac) 1);
-qed "hypreal_of_nat_Suc";
(* this proof is so much simpler than one for reals!! *)
Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_inverse,
- hypreal_less,hypreal_zero_def]));
-by (ultra_tac (claset() addIs [real_inverse_less_swap],simpset()) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_inverse, hypreal_less,hypreal_zero_def]));
+by (ultra_tac (claset() addIs [real_inverse_less_swap], simpset()) 1);
qed "hypreal_inverse_less_swap";
Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))";
-by (auto_tac (claset() addIs [hypreal_inverse_less_swap],simpset()));
+by (auto_tac (claset() addIs [hypreal_inverse_less_swap], simpset()));
by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);
by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);
by (rtac hypreal_inverse_less_swap 1);
--- a/src/HOL/Hyperreal/HyperPow.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML Thu Jan 04 10:23:01 2001 +0100
@@ -3,6 +3,7 @@
Copyright : 1998 University of Cambridge
Description : Natural Powers of hyperreals theory
+Exponentials on the hyperreals
*)
Goal "(#0::hypreal) ^ (Suc n) = 0";
@@ -136,15 +137,13 @@
Goal "(#1::hypreal) <= #2 ^ n";
by (res_inst_tac [("y","#1 ^ n")] order_trans 1);
by (rtac hrealpow_le 2);
-by (auto_tac (claset() addIs [order_less_imp_le],
- simpset() addsimps [hypreal_zero_less_one, hypreal_one_less_two]));
+by Auto_tac;
qed "two_hrealpow_ge_one";
Goal "hypreal_of_nat n < #2 ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero,
- hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one]));
+ simpset() addsimps [hypreal_of_nat_Suc, hypreal_add_mult_distrib]));
by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1);
by (arith_tac 1);
qed "two_hrealpow_gt";
@@ -189,9 +188,9 @@
Goal "(x + (y::hypreal)) ^ 2 = \
\ x ^ 2 + y ^ 2 + (hypreal_of_nat 2)*x*y";
-by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
- hypreal_add_mult_distrib,hypreal_of_nat_two]
- @ hypreal_add_ac @ hypreal_mult_ac) 1);
+by (simp_tac (simpset() addsimps
+ [hypreal_add_mult_distrib2, hypreal_add_mult_distrib,
+ hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1);
qed "hrealpow_sum_square_expand";
(*---------------------------------------------------------------
@@ -391,8 +390,7 @@
Goal "(#1::hypreal) <= #2 pow n";
by (res_inst_tac [("y","#1 pow n")] order_trans 1);
by (rtac hyperpow_le 2);
-by (auto_tac (claset() addIs [order_less_imp_le],
- simpset() addsimps [hypreal_zero_less_one, hypreal_one_less_two]));
+by Auto_tac;
qed "two_hyperpow_ge_one";
Addsimps [two_hyperpow_ge_one];
@@ -455,7 +453,7 @@
qed "hyperpow_less_le2";
Goal "[| #0 <= r; r < (#1::hypreal); N : HNatInfinite |] \
-\ ==> ALL n:SHNat. r pow N <= r pow n";
+\ ==> ALL n: SNat. r pow N <= r pow n";
by (auto_tac (claset() addSIs [hyperpow_less_le],
simpset() addsimps [HNatInfinite_iff]));
qed "hyperpow_SHNat_le";
@@ -493,18 +491,16 @@
qed "hyperpow_Suc_le_self2";
Goalw [Infinitesimal_def]
- "[| x : Infinitesimal; 0 < N |] ==> (abs x) pow N <= abs x";
+ "[| x : Infinitesimal; 0 < N |] ==> abs (x pow N) <= abs x";
by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2],
- simpset() addsimps [hyperpow_hrabs RS sym,
- hypnat_gt_zero_iff2, hrabs_ge_zero,
- hypreal_zero_less_one]));
+ simpset() addsimps [hyperpow_hrabs RS sym,
+ hypnat_gt_zero_iff2, hrabs_ge_zero]));
qed "lemma_Infinitesimal_hyperpow";
Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal";
by (rtac hrabs_le_Infinitesimal 1);
-by (dtac Infinitesimal_hrabs 1);
-by (auto_tac (claset() addSIs [lemma_Infinitesimal_hyperpow],
- simpset() addsimps [hyperpow_hrabs RS sym]));
+by (rtac lemma_Infinitesimal_hyperpow 2);
+by Auto_tac;
qed "Infinitesimal_hyperpow";
Goalw [hypnat_of_nat_def]
--- a/src/HOL/Hyperreal/HyperPow.thy Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy Thu Jan 04 10:23:01 2001 +0100
@@ -6,6 +6,16 @@
HyperPow = HRealAbs + HyperNat + RealPow +
+(** First: hypnat is linearly ordered **)
+
+instance hypnat :: order (hypnat_le_refl,hypnat_le_trans,hypnat_le_anti_sym,
+ hypnat_less_le)
+instance hypnat :: linorder (hypnat_le_linear)
+
+instance hypnat :: plus_ac0(hypnat_add_commute,hypnat_add_assoc,
+ hypnat_add_zero_left)
+
+
instance hypreal :: {power}
consts hpowr :: "[hypreal,nat] => hypreal"
--- a/src/HOL/Hyperreal/Lim.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Thu Jan 04 10:23:01 2001 +0100
@@ -5,7 +5,6 @@
differentiation of real=>real functions
*)
-
fun ARITH_PROVE str = prove_goal thy str
(fn prems => [cut_facts_tac prems 1,arith_tac 1]);
@@ -28,12 +27,9 @@
LIM_add
---------------*)
Goalw [LIM_def]
- "[| f -- x --> l; g -- x --> m |] \
-\ ==> (%x. f(x) + g(x)) -- x --> (l + m)";
-by (Step_tac 1);
+ "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)";
+by (Clarify_tac 1);
by (REPEAT(dres_inst_tac [("x","r/#2")] spec 1));
-by (dtac (rename_numerals (real_zero_less_two RS real_inverse_gt_zero
- RSN (2,real_mult_less_mono2))) 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
by (res_inst_tac [("R1.0","s"),("R2.0","sa")]
@@ -189,26 +185,26 @@
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_posnat n) & r <= abs(f xa + -L)";
-by (Step_tac 1);
+\ abs(xa + -x) < inverse(real_of_nat(Suc n)) & r <= abs(f xa + -L)";
+by (Clarify_tac 1);
by (cut_inst_tac [("n1","n")]
- (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
+ (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
by Auto_tac;
val lemma_LIM = result();
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_posnat n) & r <= abs(f (X n) + -L)";
+\ abs(X n + -x) < inverse(real_of_nat(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_posnat n) & \
+\ abs (X n + - x) < inverse (real_of_nat(Suc n)) & \
\ r <= abs (f (X n) + - L) ==> \
-\ ALL n. abs (X n + - x) < inverse (real_of_posnat n)";
+\ ALL n. abs (X n + - x) < inverse (real_of_nat(Suc n))";
by (Auto_tac );
val lemma_simp = result();
@@ -217,7 +213,7 @@
-------------------*)
Goalw [LIM_def,NSLIM_def,inf_close_def]
- "f -- x --NS> L ==> f -- x --> L";
+ "f -- x --NS> L ==> f -- x --> L";
by (asm_full_simp_tac
(simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1);
by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]);
@@ -697,16 +693,17 @@
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_posnat n) & \
+\ abs(z + -y) < inverse(real_of_nat(Suc n)) & \
\ r <= abs(f z + -f y)";
-by (Step_tac 1);
-by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
+by (Clarify_tac 1);
+by (cut_inst_tac [("n1","n")]
+ (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
by Auto_tac;
val lemma_LIMu = result();
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_posnat n) & \
+\ abs(X n + -(Y n)) < inverse(real_of_nat(Suc n)) & \
\ r <= abs(f (X n) + -f (Y n))";
by (dtac lemma_LIMu 1);
by (dtac choice 1);
@@ -715,9 +712,9 @@
by (Blast_tac 1);
val lemma_skolemize_LIM2u = result();
-Goal "ALL n. abs (X n + -Y n) < inverse (real_of_posnat n) & \
+Goal "ALL n. abs (X n + -Y n) < inverse (real_of_nat(Suc n)) & \
\ r <= abs (f (X n) + - f(Y n)) ==> \
-\ ALL n. abs (X n + - Y n) < inverse (real_of_posnat n)";
+\ ALL n. abs (X n + - Y n) < inverse (real_of_nat(Suc n))";
by (Auto_tac );
val lemma_simpu = result();
@@ -1301,17 +1298,17 @@
Goal "DERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))";
by (induct_tac "n" 1);
by (dtac (DERIV_Id RS DERIV_mult) 2);
-by (auto_tac (claset(),simpset() addsimps
- [real_add_mult_distrib]));
+by (auto_tac (claset(),
+ simpset() addsimps [real_of_nat_Suc, real_add_mult_distrib]));
by (case_tac "0 < n" 1);
by (dres_inst_tac [("x","x")] realpow_minus_mult 1);
-by (auto_tac (claset(),simpset() addsimps
- [real_mult_assoc,real_add_commute]));
+by (auto_tac (claset(),
+ simpset() addsimps [real_mult_assoc, real_add_commute]));
qed "DERIV_pow";
(* NS version *)
Goal "NSDERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))";
-by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,DERIV_pow]) 1);
+by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
qed "NSDERIV_pow";
(*---------------------------------------------------------------
--- a/src/HOL/Hyperreal/NSA.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/NSA.ML Thu Jan 04 10:23:01 2001 +0100
@@ -228,13 +228,10 @@
by Auto_tac;
qed "HFiniteD";
-Goalw [HFinite_def] "x : HFinite ==> abs x : HFinite";
+Goalw [HFinite_def] "(abs x : HFinite) = (x : HFinite)";
by (auto_tac (claset(), simpset() addsimps [hrabs_idempotent]));
-qed "HFinite_hrabs";
-
-Goalw [HFinite_def,Bex_def] "x ~: HFinite ==> abs x ~: HFinite";
-by (auto_tac (claset(), simpset() addsimps [hrabs_idempotent]));
-qed "not_HFinite_hrabs";
+qed "HFinite_hrabs_iff";
+AddIffs [HFinite_hrabs_iff];
Goal "number_of w : HFinite";
by (rtac (SReal_number_of RS (SReal_subset_HFinite RS subsetD)) 1);
@@ -389,23 +386,13 @@
by Auto_tac;
qed "not_Infinitesimal_not_zero2";
-Goal "x : Infinitesimal ==> abs x : Infinitesimal";
-by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
-by Auto_tac;
-qed "Infinitesimal_hrabs";
-
-Goal "x ~: Infinitesimal ==> abs x ~: Infinitesimal";
-by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
-by Auto_tac;
-qed "not_Infinitesimal_hrabs";
-
-Goal "abs x : Infinitesimal ==> x : Infinitesimal";
-by (rtac ccontr 1);
-by (blast_tac (claset() addDs [not_Infinitesimal_hrabs]) 1);
-qed "hrabs_Infinitesimal_Infinitesimal";
+Goal "(abs x : Infinitesimal) = (x : Infinitesimal)";
+by (auto_tac (claset(), simpset() addsimps [hrabs_def]));
+qed "Infinitesimal_hrabs_iff";
+AddIffs [Infinitesimal_hrabs_iff];
Goal "x : HFinite - Infinitesimal ==> abs x : HFinite - Infinitesimal";
-by (fast_tac (set_cs addSEs [HFinite_hrabs,not_Infinitesimal_hrabs]) 1);
+by (Blast_tac 1);
qed "HFinite_diff_Infinitesimal_hrabs";
Goalw [Infinitesimal_def]
@@ -417,8 +404,7 @@
Goal "[| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
by (blast_tac (claset() addDs [order_le_imp_less_or_eq]
- addIs [hrabs_Infinitesimal_Infinitesimal,
- hrabs_less_Infinitesimal]) 1);
+ addIs [hrabs_less_Infinitesimal]) 1);
qed "hrabs_le_Infinitesimal";
Goalw [Infinitesimal_def]
@@ -1091,8 +1077,7 @@
------------------------------------------------------------------*)
Goalw [HFinite_def,HInfinite_def] "HFinite Int HInfinite = {}";
-by (auto_tac (claset() addIs [hypreal_less_irrefl]
- addDs [order_less_trans,bspec],
+by (auto_tac (claset() addIs [hypreal_less_irrefl] addDs [order_less_trans],
simpset()));
qed "HFinite_Int_HInfinite_empty";
Addsimps [HFinite_Int_HInfinite_empty];
@@ -1102,15 +1087,10 @@
by Auto_tac;
qed "HFinite_not_HInfinite";
-val [prem] = goalw thy [HInfinite_def] "x~: HFinite ==> x: HInfinite";
-by (cut_facts_tac [prem] 1);
-by (Clarify_tac 1);
-by (auto_tac (claset() addSDs [spec],
- simpset() addsimps [HFinite_def,Bex_def]));
-by (dtac hypreal_leI 1);
-by (dtac order_le_imp_less_or_eq 1);
-by (auto_tac (claset() addSDs [SReal_subset_HFinite RS subsetD],
- simpset() addsimps [prem,hrabs_idempotent,prem RS not_HFinite_hrabs]));
+Goalw [HInfinite_def, HFinite_def] "x~: HFinite ==> x: HInfinite";
+by Auto_tac;
+by (dres_inst_tac [("x","r + #1")] bspec 1);
+by (auto_tac (claset(), simpset() addsimps [SReal_add]));
qed "not_HFinite_HInfinite";
Goal "x : HInfinite | x : HFinite";
@@ -1325,22 +1305,19 @@
simpset()));
qed "less_Infinitesimal_less";
-Goal "[| #0 < x; x ~: Infinitesimal|] ==> ALL u: monad x. #0 < u";
-by (Step_tac 1);
+Goal "[| #0 < x; x ~: Infinitesimal; u: monad x |] ==> #0 < u";
by (dtac (mem_monad_inf_close RS inf_close_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|] ==> ALL u: monad x. u < #0";
-by (Step_tac 1);
+Goal "[| x < #0; x ~: Infinitesimal; u: monad x |] ==> u < #0";
by (dtac (mem_monad_inf_close RS inf_close_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;
qed "Ball_mem_monad_less_zero";
-(*??GET RID OF QUANTIFIERS ABOVE??*)
Goal "[|#0 < x; x ~: Infinitesimal; x @= y|] ==> #0 < y";
by (blast_tac (claset() addDs [Ball_mem_monad_gt_zero,
@@ -1352,16 +1329,14 @@
inf_close_subset_monad]) 1);
qed "lemma_inf_close_less_zero";
-Goal "[| x @= y; x < #0; x ~: Infinitesimal |] \
-\ ==> abs x @= abs y";
+Goal "[| x @= y; x < #0; x ~: Infinitesimal |] ==> abs x @= abs y";
by (forward_tac [lemma_inf_close_less_zero] 1);
by (REPEAT(assume_tac 1));
by (REPEAT(dtac hrabs_minus_eqI2 1));
by Auto_tac;
qed "inf_close_hrabs1";
-Goal "[| x @= y; #0 < x; x ~: Infinitesimal |] \
-\ ==> abs x @= abs y";
+Goal "[| x @= y; #0 < x; x ~: Infinitesimal |] ==> abs x @= abs y";
by (forward_tac [lemma_inf_close_gt_zero] 1);
by (REPEAT(assume_tac 1));
by (REPEAT(dtac hrabs_eqI2 1));
@@ -1975,42 +1950,42 @@
(*------------------------------------------------------------------------
Infinitesimals as smaller than 1/n for all n::nat (> 0)
------------------------------------------------------------------------*)
-Goal "(ALL r. #0 < r --> x < r) = (ALL n. x < inverse(real_of_posnat n))";
-by (auto_tac (claset(),
- simpset() addsimps [rename_numerals real_of_posnat_gt_zero]));
-by (blast_tac (claset() addSDs [rename_numerals reals_Archimedean]
+
+Goal "(ALL r. #0 < r --> x < r) = (ALL n. x < inverse(real_of_nat (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) = \
-\ (ALL n. x < inverse(hypreal_of_posnat n))";
+\ (ALL n. x < inverse(hypreal_of_nat (Suc n)))";
by (Step_tac 1);
-by (dres_inst_tac [("x","inverse (hypreal_of_real(real_of_posnat n))")]
+by (dres_inst_tac [("x","inverse (hypreal_of_real(real_of_nat (Suc n)))")]
bspec 1);
by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1);
-by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero RS
+by (rtac (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero RS
(hypreal_of_real_less_iff RS iffD2) RSN(2,impE)) 1);
by (assume_tac 2);
by (asm_full_simp_tac (simpset() addsimps
- [rename_numerals real_of_posnat_gt_zero, hypreal_of_real_zero,
- hypreal_of_real_of_posnat]) 1);
+ [real_of_nat_Suc_gt_zero, hypreal_of_real_zero, hypreal_of_nat_def]) 1);
by (auto_tac (claset() addSDs [reals_Archimedean],
simpset() addsimps [SReal_iff,hypreal_of_real_zero RS sym]));
by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
by (asm_full_simp_tac (simpset() addsimps
- [rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1);
+ [real_of_nat_Suc_gt_zero, hypreal_of_nat_def])1);
by (blast_tac (claset() addIs [order_less_trans]) 1);
qed "lemma_Infinitesimal2";
Goalw [Infinitesimal_def]
- "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_posnat n)}";
+ "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_nat (Suc n))}";
by (auto_tac (claset(), simpset() addsimps [lemma_Infinitesimal2]));
-qed "Infinitesimal_hypreal_of_posnat_iff";
+qed "Infinitesimal_hypreal_of_nat_iff";
+
-(*-----------------------------------------------------------------------------
- Actual proof that omega (whr) is an infinite number and
+(*---------------------------------------------------------------------------
+ Proof that omega (whr) is an infinite number and
hence that epsilon (ehr) 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";
@@ -2024,72 +1999,85 @@
by (auto_tac (claset(), simpset() addsimps [Suc_Un_eq]));
qed "finite_nat_segment";
-Goal "finite {n::nat. real_of_posnat n < real_of_posnat m}";
+Goal "finite {n::nat. real_of_nat n < real_of_nat m}";
by (auto_tac (claset() addIs [finite_nat_segment], simpset()));
-qed "finite_real_of_posnat_segment";
+qed "finite_real_of_nat_segment";
-Goal "finite {n. real_of_posnat n < u}";
+Goal "finite {n. real_of_nat n < u}";
by (cut_inst_tac [("x","u")] reals_Archimedean2 1);
by (Step_tac 1);
-by (rtac (finite_real_of_posnat_segment RSN (2,finite_subset)) 1);
+by (rtac (finite_real_of_nat_segment RSN (2,finite_subset)) 1);
by (auto_tac (claset() addDs [order_less_trans], simpset()));
-qed "finite_real_of_posnat_less_real";
+qed "finite_real_of_nat_less_real";
-Goal "{n. real_of_posnat n <= u} = \
-\ {n. real_of_posnat n < u} Un {n. u = real_of_posnat n}";
+Goal "{n. f n <= u} = {n. f n < u} Un {n. u = (f n :: real)}";
by (auto_tac (claset() addDs [order_le_imp_less_or_eq],
simpset() addsimps [order_less_imp_le]));
qed "lemma_real_le_Un_eq";
-Goal "finite {n. real_of_posnat n <= u}";
-by (auto_tac (claset(), simpset() addsimps
- [lemma_real_le_Un_eq,lemma_finite_omega_set,
- finite_real_of_posnat_less_real]));
-qed "finite_real_of_posnat_le_real";
+Goal "finite {n. real_of_nat 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_posnat n) <= u}";
-by (full_simp_tac (simpset() addsimps [rename_numerals
- real_of_posnat_gt_zero,abs_eqI2,
- finite_real_of_posnat_le_real]) 1);
-qed "finite_rabs_real_of_posnat_le_real";
+Goal "finite {n. abs(real_of_nat 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_posnat n) <= u} ~: FreeUltrafilterNat";
+Goal "{n. abs(real_of_nat n) <= u} ~: FreeUltrafilterNat";
by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
- finite_rabs_real_of_posnat_le_real]) 1);
-qed "rabs_real_of_posnat_le_real_FreeUltrafilterNat";
+ finite_rabs_real_of_nat_le_real]) 1);
+qed "rabs_real_of_nat_le_real_FreeUltrafilterNat";
-Goal "{n. u < real_of_posnat n} : FreeUltrafilterNat";
+Goal "{n. u < real_of_nat n} : FreeUltrafilterNat";
by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
-by (auto_tac (claset(), simpset() addsimps
- [CLAIM_SIMP "- {n. u < real_of_posnat n} = \
-\ {n. real_of_posnat n <= u}"
- [real_le_def],finite_real_of_posnat_le_real
- RS FreeUltrafilterNat_finite]));
+by (subgoal_tac "- {n. u < real_of_nat n} = {n. real_of_nat 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_posnat n) <= u} =
- {n. u < abs (real_of_posnat n)} is in FreeUltrafilterNat
+ The complement of {n. abs(real_of_nat n) <= u} =
+ {n. u < abs (real_of_nat n)} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
-Goal "- {n. abs (real_of_posnat n) <= u} = \
-\ {n. u < abs (real_of_posnat n)}";
+Goal "- {n. real_of_nat n <= u} = {n. u < real_of_nat n}";
by (auto_tac (claset() addSDs [order_le_less_trans],
simpset() addsimps [not_real_leE]));
val lemma = result();
-Goal "{n. u < abs (real_of_posnat n)} : FreeUltrafilterNat";
-by (cut_inst_tac [("u","u")] rabs_real_of_posnat_le_real_FreeUltrafilterNat 1);
+Goal "{n. u < abs (real_of_nat 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]));
+ simpset() addsimps [lemma]));
qed "FreeUltrafilterNat_omega";
(*-----------------------------------------------
Omega is a member of HInfinite
-----------------------------------------------*)
+
+Goal "hyprel^^{%n::nat. real_of_nat (Suc n)} : hypreal";
+by Auto_tac;
+qed "hypreal_omega";
+
+
+Goal "{n. u < real_of_nat 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";
-by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite,
- lemma_hyprel_refl,FreeUltrafilterNat_omega], simpset()));
+by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite],
+ simpset()));
+by (rtac bexI 1);
+by (rtac lemma_hyprel_refl 2);
+by Auto_tac;
+by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym,
+ FreeUltrafilterNat_omega]) 1);
qed "HInfinite_omega";
(*-----------------------------------------------
@@ -2118,48 +2106,75 @@
that ALL n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
-----------------------------------------------------------------------*)
-Goal "#0 < u ==> finite {n. u < inverse(real_of_posnat n)}";
-by (asm_simp_tac (simpset() addsimps [real_of_posnat_less_inverse_iff]) 1);
-by (rtac finite_real_of_posnat_less_real 1);
+Goal "0 < u ==> \
+\ (u < inverse (real_of_nat(Suc n))) = (real_of_nat(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);
+by (stac pos_real_less_divide_eq 1);
+by (simp_tac (simpset() addsimps [real_mult_commute]) 2);
+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))}";
+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_posnat n)} = \
-\ {n. u < inverse(real_of_posnat n)} Un {n. u = inverse(real_of_posnat n)}";
+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))}";
by (auto_tac (claset() addDs [order_le_imp_less_or_eq],
simpset() addsimps [order_less_imp_le]));
qed "lemma_real_le_Un_eq2";
-Goal "#0 < u ==> finite {n::nat. u = inverse(real_of_posnat n)}";
-by (asm_simp_tac (simpset() addsimps [real_of_posnat_inverse_eq_iff]) 1);
-by (auto_tac (claset() addIs [lemma_finite_omega_set RSN
- (2,finite_subset)], simpset()));
+Goal "(inverse (real_of_nat(Suc n)) <= r) = (#1 <= r * real_of_nat(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);
+by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1);
+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)";
+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))}";
+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_posnat n)}";
+Goal "#0 < u ==> finite {n. u <= inverse(real_of_nat(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_posnat n)} ~: FreeUltrafilterNat";
+\ {n. u <= inverse(real_of_nat(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_posnat n)} =
- {n. inverse(real_of_posnat n) < u} is in FreeUltrafilterNat
+ The complement of {n. u <= inverse(real_of_nat(Suc n))} =
+ {n. inverse(real_of_nat(Suc n)) < u} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
-Goal "- {n. u <= inverse(real_of_posnat n)} = \
-\ {n. inverse(real_of_posnat n) < u}";
+Goal "- {n. u <= inverse(real_of_nat(Suc n))} = \
+\ {n. inverse(real_of_nat(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_posnat n) < u} : FreeUltrafilterNat";
+\ {n. inverse(real_of_nat(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]));
@@ -2176,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_posnat n) \
+Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(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,
@@ -2184,24 +2199,23 @@
addIs [order_less_trans, FreeUltrafilterNat_subset],
simpset() addsimps [hypreal_minus,
hypreal_of_real_def,hypreal_add,
- Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse,
- hypreal_of_real_of_posnat]));
+ Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse]));
qed "real_seq_to_hypreal_Infinitesimal";
-Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \
+Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \
\ ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x";
by (rtac (inf_close_minus_iff RS ssubst) 1);
by (rtac (mem_infmal_iff RS subst) 1);
by (etac real_seq_to_hypreal_Infinitesimal 1);
qed "real_seq_to_hypreal_inf_close";
-Goal "ALL n. abs(x + -X n) < inverse(real_of_posnat n) \
+Goal "ALL n. abs(x + -X n) < inverse(real_of_nat(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";
-Goal "ALL n. abs(X n + -Y n) < inverse(real_of_posnat n) \
+Goal "ALL n. abs(X n + -Y n) < inverse(real_of_nat(Suc n)) \
\ ==> Abs_hypreal(hyprel^^{X}) + \
\ -Abs_hypreal(hyprel^^{Y}) : Infinitesimal";
by (auto_tac (claset() addSIs [bexI]
@@ -2211,5 +2225,5 @@
addIs [order_less_trans, FreeUltrafilterNat_subset],
simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add,
- hypreal_inverse,hypreal_of_real_of_posnat]));
+ hypreal_inverse]));
qed "real_seq_to_hypreal_Infinitesimal2";
--- a/src/HOL/Hyperreal/NatStar.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML Thu Jan 04 10:23:01 2001 +0100
@@ -122,13 +122,13 @@
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
qed "NatStar_hypreal_of_real_image_subset";
-Goal "SHNat <= *sNat* (UNIV:: nat set)";
+Goal "SNat <= *sNat* (UNIV:: nat set)";
by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff,
- NatStar_hypreal_of_real_image_subset]) 1);
+ NatStar_hypreal_of_real_image_subset]) 1);
qed "NatStar_SHNat_subset";
Goalw [starsetNat_def]
- "*sNat* X Int SHNat = hypnat_of_nat `` X";
+ "*sNat* X Int SNat = hypnat_of_nat `` X";
by (auto_tac (claset(),
simpset() addsimps
[hypnat_of_nat_def,SHNat_def]));
--- a/src/HOL/Hyperreal/NatStar.thy Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy Thu Jan 04 10:23:01 2001 +0100
@@ -5,7 +5,7 @@
sets of reals, and nat=>real, nat=>nat functions
*)
-NatStar = HyperNat + RealPow + HyperPow +
+NatStar = RealPow + HyperPow +
constdefs
--- a/src/HOL/Hyperreal/SEQ.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Thu Jan 04 10:23:01 2001 +0100
@@ -11,14 +11,13 @@
-------------------------------------------------------------------------- *)
Goalw [hypnat_omega_def]
- "(*fNat* (%n::nat. inverse(real_of_posnat n))) whn : Infinitesimal";
+ "(*fNat* (%n::nat. inverse(real_of_nat(Suc n)))) whn : Infinitesimal";
by (auto_tac (claset(),
simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
by (auto_tac (claset(),
- simpset() addsimps (map rename_numerals)
- [real_of_posnat_gt_zero,real_inverse_gt_zero,abs_eqI2,
- FreeUltrafilterNat_inverse_real_of_posnat]));
+ simpset() addsimps [real_of_nat_Suc_gt_zero, abs_eqI2,
+ FreeUltrafilterNat_inverse_real_of_posnat]));
qed "SEQ_Infinitesimal";
(*--------------------------------------------------------------------------
@@ -423,45 +422,46 @@
qed "BseqI";
Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
-\ (EX N. ALL n. abs(X n) <= real_of_posnat N)";
-by (auto_tac (claset(),simpset() addsimps
- (map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero]));
-by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1);
-by (blast_tac (claset() addIs [order_le_less_trans, order_less_imp_le]) 1);
-by (auto_tac (claset(),simpset() addsimps [real_of_posnat_def]));
+\ (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))";
+by Auto_tac;
+by (Force_tac 2);
+by (cut_inst_tac [("x","K")] reals_Archimedean2 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("x","n")] exI 1);
+by (Clarify_tac 1);
+by (dres_inst_tac [("x","na")] spec 1);
+by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
qed "lemma_NBseq_def";
(* alternative definition for Bseq *)
-Goalw [Bseq_def]
- "Bseq X = (EX N. ALL n. abs(X n) <= real_of_posnat N)";
+Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) <= real_of_nat(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_posnat N)";
-by (auto_tac (claset(),simpset() addsimps
- (map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero]));
-by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1);
-by (blast_tac (claset() addIs [order_less_trans, order_le_less_trans]) 1);
-by (auto_tac (claset() addIs [order_less_imp_le],
- simpset() addsimps [real_of_posnat_def]));
+\ (EX N. ALL n. abs(X n) < real_of_nat(Suc N))";
+by (stac lemma_NBseq_def 1);
+by Auto_tac;
+by (res_inst_tac [("x","Suc N")] exI 1);
+by (res_inst_tac [("x","N")] exI 2);
+by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
+by (blast_tac (claset() addIs [order_less_imp_le]) 2);
+by (dres_inst_tac [("x","n")] spec 1);
+by (Asm_simp_tac 1);
qed "lemma_NBseq_def2";
(* yet another definition for Bseq *)
-Goalw [Bseq_def]
- "Bseq X = (EX N. ALL n. abs(X n) < real_of_posnat N)";
+Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real_of_nat(Suc N))";
by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1);
qed "Bseq_iff1a";
Goalw [NSBseq_def]
- "[| NSBseq X; N: HNatInfinite |] \
-\ ==> (*fNat* X) N : HFinite";
+ "[| NSBseq X; N: HNatInfinite |] ==> (*fNat* X) N : HFinite";
by (Blast_tac 1);
qed "NSBseqD";
Goalw [NSBseq_def]
- "ALL N: HNatInfinite. (*fNat* X) N : HFinite \
-\ ==> NSBseq X";
+ "ALL N: HNatInfinite. (*fNat* X) N : HFinite ==> NSBseq X";
by (assume_tac 1);
qed "NSBseqI";
@@ -469,17 +469,16 @@
Standard definition ==> NS definition
----------------------------------------------------------*)
(* a few lemmas *)
-Goal "ALL n. abs(X n) <= K ==> \
-\ ALL n. abs(X((f::nat=>nat) n)) <= K";
+Goal "ALL n. abs(X n) <= K ==> ALL n. abs(X((f::nat=>nat) n)) <= K";
by (Auto_tac);
val lemma_Bseq = result();
Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X";
by (Step_tac 1);
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- HFinite_FreeUltrafilterNat_iff,
- HNatInfinite_FreeUltrafilterNat_iff]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat, HFinite_FreeUltrafilterNat_iff,
+ HNatInfinite_FreeUltrafilterNat_iff]));
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2]);
by (dres_inst_tac [("f","Xa")] lemma_Bseq 1);
by (res_inst_tac [("x","K+#1")] exI 1);
@@ -500,79 +499,77 @@
-------------------------------------------------------------------*)
Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \
-\ ==> ALL N. EX n. real_of_posnat N < abs (X n)";
+\ ==> ALL N. EX n. real_of_nat(Suc N) < abs (X n)";
by (Step_tac 1);
-by (cut_inst_tac [("n","N")] (rename_numerals real_of_posnat_gt_zero) 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_posnat N < abs (X (f N))";
+\ ==> EX f. ALL N. real_of_nat(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_posnat N < abs (X (f N)) \
+Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
\ ==> Abs_hypreal(hyprel^^{X o f}) : HInfinite";
-by (auto_tac (claset(),simpset() addsimps
- [HInfinite_FreeUltrafilterNat_iff,o_def]));
-by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2,
- Step_tac 1]);
+by (auto_tac (claset(),
+ simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def]));
+by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1);
-by (blast_tac (claset() addDs [FreeUltrafilterNat_all, FreeUltrafilterNat_Int]
- addIs [order_less_trans, FreeUltrafilterNat_subset]) 1);
+by (dtac FreeUltrafilterNat_all 1);
+by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1);
+by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
qed "real_seq_to_hypreal_HInfinite";
-(*--------------------------------------------------------------------------------
+(*-----------------------------------------------------------------------------
Now prove that we can get out an infinite hypernatural as well
defined using the skolem function f::nat=>nat above
- --------------------------------------------------------------------------------*)
+ ----------------------------------------------------------------------------*)
-Goal "{n. f n <= Suc u & real_of_posnat n < abs (X (f n))} <= \
-\ {n. f n <= u & real_of_posnat n < abs (X (f n))} \
-\ Un {n. real_of_posnat n < abs (X (Suc u))}";
-by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_imp_le],
- simpset() addsimps [less_Suc_eq]));
+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))}";
+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_posnat n < abs(X(f n))}";
+Goal "finite {n. f n <= (u::nat) & real_of_nat(Suc n) < abs(X(f n))}";
by (induct_tac "u" 1);
-by (rtac (CLAIM "{n. f n <= (0::nat) & real_of_posnat n < abs (X (f n))} <= \
-\ {n. real_of_posnat n < abs (X 0)}"
- RS finite_subset) 1);
-by (rtac finite_real_of_posnat_less_real 1);
-by (rtac (lemma_finite_NSBseq RS finite_subset) 1);
-by (auto_tac (claset() addIs [finite_real_of_posnat_less_real], simpset()));
+by (res_inst_tac [("B","{n. real_of_nat(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_posnat N < abs (X (f N)) \
+Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
\ ==> Abs_hypnat(hypnatrel^^{f}) : HNatInfinite";
-by (auto_tac (claset(),simpset() addsimps
- [HNatInfinite_FreeUltrafilterNat_iff]));
-by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2,
- Step_tac 1]);
+by (auto_tac (claset(),
+ simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
+by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
by (asm_full_simp_tac (simpset() addsimps
[CLAIM_SIMP "- {n. u < (f::nat=>nat) n} \
\ = {n. f n <= u}" [le_def]]) 1);
by (dtac FreeUltrafilterNat_all 1);
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
-by (auto_tac (claset(),simpset() addsimps
- [CLAIM "({n. f n <= u} Int {n. real_of_posnat n < abs(X(f n))}) = \
-\ {n. f n <= (u::nat) & real_of_posnat n < abs(X(f n))}",
+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))}",
lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite]));
qed "HNatInfinite_skolem_f";
Goalw [Bseq_def,NSBseq_def]
"NSBseq X ==> Bseq X";
by (rtac ccontr 1);
-by (auto_tac (claset(),simpset() addsimps [real_le_def]));
+by (auto_tac (claset(), simpset() addsimps [real_le_def]));
by (dtac lemmaNSBseq2 1 THEN Step_tac 1);
by (forw_inst_tac [("X","X"),("f","f")] real_seq_to_hypreal_HInfinite 1);
by (dtac (HNatInfinite_skolem_f RSN (2,bspec)) 1 THEN assume_tac 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- o_def,HFinite_HInfinite_iff]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat, o_def,HFinite_HInfinite_iff]));
qed "NSBseq_Bseq";
(*----------------------------------------------------------------------
@@ -805,7 +802,7 @@
by (auto_tac (claset(),
simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
by (dres_inst_tac [("x","M")] spec 1);
-by (ultra_tac (claset(),simpset() addsimps [less_imp_le]) 1);
+by (ultra_tac (claset(), simpset() addsimps [less_imp_le]) 1);
val lemmaCauchy1 = result();
Goal "{n. ALL m n. M <= m & M <= (n::nat) --> abs (X m + - X n) < u} Int \
@@ -821,8 +818,9 @@
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (rtac (inf_close_minus_iff RS iffD2) 1);
by (rtac (mem_infmal_iff RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypreal_minus,hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat, hypreal_minus,hypreal_add,
+ Infinitesimal_FreeUltrafilterNat_iff]));
by (EVERY[rtac bexI 1, Auto_tac]);
by (dtac spec 1 THEN Auto_tac);
by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
@@ -841,17 +839,17 @@
Goalw [Cauchy_def,NSCauchy_def]
"NSCauchy X ==> Cauchy X";
by (EVERY1[Step_tac, rtac ccontr,Asm_full_simp_tac]);
-by (dtac choice 1 THEN auto_tac (claset(),simpset()
- addsimps [all_conj_distrib]));
-by (dtac choice 1 THEN step_tac (claset() addSDs
- [all_conj_distrib RS iffD1]) 1);
+by (dtac choice 1 THEN
+ auto_tac (claset(), simpset() addsimps [all_conj_distrib]));
+by (dtac choice 1 THEN
+ step_tac (claset() addSDs [all_conj_distrib RS iffD1]) 1);
by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1));
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]));
+ THEN auto_tac (claset(), simpset() addsimps [starfunNat]));
by (dtac (inf_close_minus_iff RS iffD1) 1);
by (dtac (mem_infmal_iff RS iffD2) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
+by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac);
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
@@ -1076,8 +1074,8 @@
Goal "f ----NS> l ==> (%n. f(Suc n)) ----NS> l";
by (forward_tac [NSconvergentI RS
(NSCauchy_NSconvergent_iff RS iffD2)] 1);
-by (auto_tac (claset(),simpset() addsimps [NSCauchy_def,
- NSLIMSEQ_def,starfunNat_shift_one]));
+by (auto_tac (claset(),
+ simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
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);
@@ -1093,8 +1091,8 @@
Goal "(%n. f(Suc n)) ----NS> l ==> f ----NS> l";
by (forward_tac [NSconvergentI RS
(NSCauchy_NSconvergent_iff RS iffD2)] 1);
-by (auto_tac (claset(),simpset() addsimps [NSCauchy_def,
- NSLIMSEQ_def,starfunNat_shift_one]));
+by (auto_tac (claset(),
+ simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
by (dtac bspec 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1);
@@ -1181,31 +1179,33 @@
(*--------------------------------------------------------------
Sequence 1/n --> 0 as n --> infinity
-------------------------------------------------------------*)
-Goal "(%n. inverse(real_of_posnat n)) ----> #0";
+
+Goal "(%n. inverse(real_of_nat(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 (Step_tac 1 THEN etac (le_imp_less_or_eq RS disjE) 1);
-by (dtac (real_of_posnat_less_iff RS iffD2) 1);
-by (auto_tac (claset() addEs [order_less_trans], simpset()));
-qed "LIMSEQ_inverse_real_of_posnat";
+by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
+by (subgoal_tac "y < real_of_nat 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_posnat n)) ----NS> #0";
+Goal "(%n. inverse(real_of_nat(Suc n))) ----NS> #0";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
- LIMSEQ_inverse_real_of_posnat]) 1);
-qed "NSLIMSEQ_inverse_real_of_posnat";
+ LIMSEQ_inverse_real_of_nat]) 1);
+qed "NSLIMSEQ_inverse_real_of_nat";
(*--------------------------------------------
Sequence r + 1/n --> r as n --> infinity
now easily proved
--------------------------------------------*)
-Goal "(%n. r + inverse(real_of_posnat n)) ----> r";
-by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat]
- MRS LIMSEQ_add] 1);
-by (Auto_tac);
+Goal "(%n. r + inverse(real_of_nat(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_posnat n)) ----NS> r";
+Goal "(%n. r + inverse(real_of_nat(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";
@@ -1214,24 +1214,24 @@
Also...
--------------*)
-Goal "(%n. r + -inverse(real_of_posnat n)) ----> r";
-by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat]
- MRS LIMSEQ_add_minus] 1);
+Goal "(%n. r + -inverse(real_of_nat(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_posnat n)) ----NS> r";
+Goal "(%n. r + -inverse(real_of_nat(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_posnat n))) ----> r";
+Goal "(%n. r*( #1 + -inverse(real_of_nat(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_posnat n))) ----NS> r";
+Goal "(%n. r*( #1 + -inverse(real_of_nat(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";
@@ -1349,8 +1349,9 @@
"X ----NS> #0 ==> Abs_hypreal(hyprel^^{X}) : Infinitesimal";
by (dres_inst_tac [("x","whn")] bspec 1);
by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_omega_def,
- mem_infmal_iff RS sym,starfunNat,hypreal_of_real_zero]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypnat_omega_def, mem_infmal_iff RS sym,
+ starfunNat,hypreal_of_real_zero]));
qed "NSLIMSEQ_zero_Infinitesimal_hypreal";
(***---------------------------------------------------------------
@@ -1366,3 +1367,5 @@
Goal "subseq f ==> n <= f(n)";
Goal "subseq f ==> EX n. N1 <= n & N2 <= f(n)";
---------------------------------------------------------------***)
+
+
--- a/src/HOL/Hyperreal/Series.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/Series.ML Thu Jan 04 10:23:01 2001 +0100
@@ -67,8 +67,9 @@
Goal "sumr 0 n (%i. r) = real_of_nat n*r";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps
- [real_add_mult_distrib,real_of_nat_zero]));
+by (auto_tac (claset(),
+ simpset() addsimps [real_add_mult_distrib,real_of_nat_zero,
+ real_of_nat_Suc]));
qed "sumr_const";
Addsimps [sumr_const];
@@ -118,10 +119,9 @@
by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2);
by (Step_tac 1);
by (dres_inst_tac [("x","n")] spec 3);
-by (auto_tac (claset() addSDs [le_imp_less_or_eq],
- simpset()));
-by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib,
- Suc_diff_n]) 1);
+by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
+by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib, Suc_diff_n,
+ real_of_nat_Suc]) 1);
qed_spec_mp "sumr_interval_const";
Goal "(ALL n. m <= n --> f n = r) & m <= na \
@@ -133,20 +133,14 @@
by (dres_inst_tac [("x","n")] spec 3);
by (auto_tac (claset() addSDs [le_imp_less_or_eq],
simpset()));
-by (asm_simp_tac (simpset() addsimps [Suc_diff_n,
- real_add_mult_distrib]) 1);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_n, real_add_mult_distrib,
+ real_of_nat_Suc]) 1);
qed_spec_mp "sumr_interval_const2";
-Goal "(m <= n)= (m < Suc n)";
-by (Auto_tac);
-qed "le_eq_less_Suc";
-
-Goal "(ALL n. m <= n --> #0 <= f n) & m < na \
-\ --> sumr 0 m f <= sumr 0 na f";
-by (induct_tac "na" 1);
+Goal "(ALL n. m <= n --> #0 <= f n) & m < k --> sumr 0 m f <= sumr 0 k f";
+by (induct_tac "k" 1);
by (Step_tac 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps
- [le_eq_less_Suc RS sym])));
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le])));
by (ALLGOALS(dres_inst_tac [("x","n")] spec));
by (Step_tac 1);
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
@@ -235,14 +229,14 @@
\ --> (sumr m (m + n) f <= (real_of_nat n * K))";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_add_le_mono],
- simpset() addsimps [real_add_mult_distrib]));
+ 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))";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_add_le_mono],
- simpset() addsimps [real_add_mult_distrib]));
+ simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc]));
qed_spec_mp "sumr_bound2";
Goal "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f";
@@ -543,14 +537,13 @@
(*-------------------------------------------------------------------
The ratio test
-------------------------------------------------------------------*)
+
Goal "[| c <= #0; abs x <= c * abs y |] ==> x = (#0::real)";
by (dtac order_le_imp_less_or_eq 1);
-by Auto_tac;
-by (dres_inst_tac [("x1","y")]
- (abs_ge_zero RS rename_numerals real_mult_le_zero) 1);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
-by (dtac order_trans 1 THEN assume_tac 1);
-by (TRYALL(arith_tac));
+by Auto_tac;
+by (subgoal_tac "#0 <= c * abs y" 1);
+by (arith_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [real_0_le_mult_iff]) 1);
qed "rabs_ratiotest_lemma";
(* lemmas *)
@@ -599,9 +592,9 @@
qed "ratio_test";
-(*----------------------------------------------------------------------------*)
-(* Differentiation of finite sum *)
-(*----------------------------------------------------------------------------*)
+(*--------------------------------------------------------------------------*)
+(* Differentiation of finite sum *)
+(*--------------------------------------------------------------------------*)
Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \
\ --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)";
--- a/src/HOL/Hyperreal/Star.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/Star.ML Thu Jan 04 10:23:01 2001 +0100
@@ -451,25 +451,28 @@
qed "STAR_starfun_rabs_add_minus";
(*-------------------------------------------------------------------
- Another charaterization of Infinitesimal and one of @= relation.
+ Another characterization of Infinitesimal and one of @= relation.
In this theory since hypreal_hrabs proved here. (To Check:) Maybe
move both if possible?
-------------------------------------------------------------------*)
Goal "(x:Infinitesimal) = \
\ (EX X:Rep_hypreal(x). \
-\ ALL m. {n. abs(X n) < inverse(real_of_posnat m)}:FreeUltrafilterNat)";
+\ ALL m. {n. abs(X n) < inverse(real_of_nat(Suc m))} \
+\ : FreeUltrafilterNat)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl],
- simpset() addsimps [Infinitesimal_hypreal_of_posnat_iff,
- hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_inverse,
- hypreal_hrabs,hypreal_less]));
+ simpset() addsimps [Infinitesimal_hypreal_of_nat_iff,
+ hypreal_of_real_def,hypreal_inverse,
+ hypreal_hrabs,hypreal_less, hypreal_of_nat_def]));
+by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero,
+ real_not_refl2 RS not_sym]) 1) ;
by (dres_inst_tac [("x","n")] spec 1);
by (Fuf_tac 1);
qed "Infinitesimal_FreeUltrafilterNat_iff2";
Goal "(Abs_hypreal(hyprel^^{X}) @= Abs_hypreal(hyprel^^{Y})) = \
\ (ALL m. {n. abs (X n + - Y n) < \
-\ inverse(real_of_posnat m)} : FreeUltrafilterNat)";
+\ inverse(real_of_nat(Suc m))} : FreeUltrafilterNat)";
by (rtac (inf_close_minus_iff RS ssubst) 1);
by (rtac (mem_infmal_iff RS subst) 1);
by (auto_tac (claset(),
@@ -485,8 +488,3 @@
by (dres_inst_tac [("x","Abs_hypreal(hyprel ^^{%n. xa})")] fun_cong 1);
by (auto_tac (claset(),simpset() addsimps [starfun]));
qed "inj_starfun";
-
-
-
-
-
--- a/src/HOL/Real/RComplete.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Real/RComplete.ML Thu Jan 04 10:23:01 2001 +0100
@@ -194,51 +194,61 @@
Related: Archimedean property of reals
----------------------------------------------------------------*)
-Goal "#0 < x ==> EX n. inverse (real_of_posnat n) < x";
-by (stac real_of_posnat_inverse_Ex_iff 1);
-by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
-by (fold_tac [real_le_def]);
+Goal "#0 < real_of_nat (Suc n)";
+by (res_inst_tac [("y","real_of_nat 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";
+by (rtac ccontr 1);
+by (subgoal_tac "ALL n. x * real_of_nat (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 [("z","real_of_nat (Suc n)")]
+ (rotate_prems 1 real_mult_le_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_posnat n)} #1" 1);
-by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1);
+\ {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);
by (dtac reals_complete 1);
by (auto_tac (claset() addIs [isUbI,setleI],simpset()));
-by (subgoal_tac "ALL m. x*(real_of_posnat(Suc m)) <= t" 1);
+by (subgoal_tac "ALL m. x*(real_of_nat(Suc m)) <= t" 1);
by (asm_full_simp_tac (simpset() addsimps
- [real_of_posnat_Suc,real_add_mult_distrib2]) 1);
+ [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_posnat n)} (t + (-x))" 1);
+\ {z. EX n. z = x*(real_of_nat (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 (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2);
-by (auto_tac (claset() addDs [order_le_less_trans,
- real_minus_zero_less_iff2 RS iffD2],
- simpset() addsimps [real_add_assoc RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [real_of_nat_Suc,real_add_mult_distrib2]));
qed "reals_Archimedean";
-Goal "EX n. (x::real) < real_of_posnat n";
+(*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";
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","0")] exI 2);
+by (res_inst_tac [("x","1")] exI 2);
by (auto_tac (claset() addEs [order_less_trans],
- simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
+ simpset() addsimps [real_of_nat_one]));
by (ftac ((rename_numerals real_inverse_gt_zero) RS reals_Archimedean) 1);
-by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
+by (Step_tac 1 THEN res_inst_tac [("x","Suc n")] exI 1);
by (forw_inst_tac [("y","inverse x")]
(rename_numerals real_mult_less_mono1) 1);
-by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
-by (dres_inst_tac [("n1","n"),("y","#1")]
- (real_of_posnat_gt_zero RS real_mult_less_mono2) 1);
+by Auto_tac;
+by (dres_inst_tac [("y","#1"),("z","real_of_nat (Suc n)")]
+ (rotate_prems 1 real_mult_less_mono2) 1);
by (auto_tac (claset(),
- simpset() addsimps [rename_numerals real_of_posnat_gt_zero,
+ simpset() addsimps [real_of_nat_Suc_gt_zero,
real_not_refl2 RS not_sym,
real_mult_assoc RS sym]));
qed "reals_Archimedean2";
-
-
-
-
-
--- a/src/HOL/Real/RealArith0.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Real/RealArith0.ML Thu Jan 04 10:23:01 2001 +0100
@@ -86,6 +86,11 @@
qed "real_divide_eq_0_iff";
Addsimps [real_divide_eq_0_iff];
+Goal "h ~= (#0::real) ==> h/h = #1";
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_inv_left]) 1);
+qed "real_divide_self_eq";
+Addsimps [real_divide_self_eq];
+
(**** Factor cancellation theorems for "real" ****)
@@ -524,6 +529,25 @@
by (asm_simp_tac (simpset() addsimps [min_def]) 1);
qed "real_lbound_gt_zero";
+Goal "(inverse x = inverse y) = (x = (y::real))";
+by (case_tac "x=#0 | y=#0" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [real_inverse_eq_divide,
+ rename_numerals DIVISION_BY_ZERO]));
+by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
+by (Asm_full_simp_tac 1);
+qed "real_inverse_eq_iff";
+Addsimps [real_inverse_eq_iff];
+
+Goal "(z/x = z/y) = (z = #0 | x = (y::real))";
+by (case_tac "x=#0 | y=#0" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [rename_numerals DIVISION_BY_ZERO]));
+by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
+by Auto_tac;
+qed "real_divide_eq_iff";
+Addsimps [real_divide_eq_iff];
+
(*** General rewrites to improve automation, like those for type "int" ***)
--- a/src/HOL/Real/RealDef.thy Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Real/RealDef.thy Thu Jan 04 10:23:01 2001 +0100
@@ -23,9 +23,10 @@
consts
"1r" :: real ("1r")
- (*Overloaded constant: denotes the Real subset of enclosing types such as
- hypreal and complex*)
- SReal :: "'a set"
+ (*Overloaded constants denoting the Nat and Real subsets of enclosing
+ types such as hypreal and complex*)
+ SNat, SReal :: "'a set"
+
defs
@@ -80,5 +81,6 @@
syntax (symbols)
SReal :: "'a set" ("\\<real>")
+ SNat :: "'a set" ("\\<nat>")
end
--- a/src/HOL/Real/RealOrd.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Real/RealOrd.ML Thu Jan 04 10:23:01 2001 +0100
@@ -142,24 +142,6 @@
simpset()));
qed "real_less_le_mult_order";
-Goal "[| x <= 0; y <= 0 |] ==> (0::real) <= x * y";
-by (rtac real_less_or_eq_imp_le 1);
-by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
-by Auto_tac;
-by (dtac order_le_imp_less_or_eq 1);
-by (auto_tac (claset() addDs [real_mult_less_zero1],simpset()));
-qed "real_mult_le_zero1";
-
-Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::real)";
-by (rtac real_less_or_eq_imp_le 1);
-by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
-by Auto_tac;
-by (dtac (real_minus_zero_less_iff RS iffD2) 1);
-by (rtac (real_minus_zero_less_iff RS subst) 1);
-by (blast_tac (claset() addDs [real_mult_order]
- addIs [real_minus_mult_eq2 RS ssubst]) 1);
-qed "real_mult_le_zero";
-
Goal "[| 0 < x; y < 0 |] ==> x*y < (0::real)";
by (dtac (real_minus_zero_less_iff RS iffD2) 1);
by (dtac real_mult_order 1 THEN assume_tac 1);
@@ -281,11 +263,6 @@
by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
qed "real_le_minus_iff";
Addsimps [real_le_minus_iff];
-
-Goal "0 <= 1r";
-by (rtac (real_zero_less_one RS order_less_imp_le) 1);
-qed "real_zero_le_one";
-Addsimps [real_zero_le_one];
Goal "(0::real) <= x*x";
by (res_inst_tac [("R2.0","0"),("R1.0","x")] real_linear_less2 1);
@@ -300,19 +277,18 @@
----------------------------------------------------------------------------*)
Goalw [real_of_posnat_def] "real_of_posnat 0 = 1r";
-by (full_simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def]) 1);
-by (fold_tac [real_one_def]);
-by (rtac refl 1);
+by (simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def,
+ symmetric real_one_def]) 1);
qed "real_of_posnat_one";
Goalw [real_of_posnat_def] "real_of_posnat 1 = 1r + 1r";
-by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
- pnat_two_eq,real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym
- ] @ pnat_add_ac) 1);
+by (simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
+ pnat_two_eq,real_add,prat_of_pnat_add RS sym,
+ preal_of_prat_add RS sym] @ pnat_add_ac) 1);
qed "real_of_posnat_two";
Goalw [real_of_posnat_def]
- "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r";
+ "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r";
by (full_simp_tac (simpset() addsimps [real_of_posnat_one RS sym,
real_of_posnat_def,real_of_preal_add RS sym,preal_of_prat_add RS sym,
prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
@@ -338,40 +314,96 @@
by (etac (inj_pnat_of_nat RS injD) 1);
qed "inj_real_of_posnat";
-Goalw [real_of_posnat_def] "0 < real_of_posnat n";
-by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
-by (Blast_tac 1);
-qed "real_of_posnat_gt_zero";
+Goalw [real_of_nat_def] "real_of_nat 0 = 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";
+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";
+by (simp_tac (simpset() addsimps
+ [real_of_posnat_add,real_add_assoc RS sym]) 1);
+qed "real_of_nat_add";
-Goal "real_of_posnat n ~= 0";
-by (rtac (real_of_posnat_gt_zero RS real_not_refl2 RS not_sym) 1);
-qed "real_of_posnat_not_eq_zero";
-Addsimps[real_of_posnat_not_eq_zero];
+(*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";
+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)";
+by Auto_tac;
+qed "real_of_nat_less_iff";
+AddIffs [real_of_nat_less_iff];
-Goal "1r <= real_of_posnat n";
-by (simp_tac (simpset() addsimps [real_of_posnat_one RS sym]) 1);
+Goal "(real_of_nat n <= real_of_nat 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";
+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";
by (induct_tac "n" 1);
by (auto_tac (claset(),
- simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
- real_of_posnat_gt_zero, order_less_imp_le]));
-qed "real_of_posnat_less_one";
-Addsimps [real_of_posnat_less_one];
+ simpset () addsimps [real_of_nat_Suc]));
+by (dtac real_add_le_less_mono 1);
+by (rtac real_zero_less_one 1);
+by (asm_full_simp_tac (simpset() addsimps [order_less_imp_le]) 1);
+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";
+by (induct_tac "m" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [real_of_nat_add, real_of_nat_Suc,
+ real_add_mult_distrib, real_add_commute]));
+qed "real_of_nat_mult";
+
+Goal "(real_of_nat n = real_of_nat 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 "inverse (real_of_posnat n) ~= 0";
-by (rtac ((real_of_posnat_gt_zero RS
- real_not_refl2 RS not_sym) RS real_inverse_not_zero) 1);
-qed "real_of_posnat_inverse_not_zero";
-Addsimps [real_of_posnat_inverse_not_zero];
+Goal "n <= m --> real_of_nat (m - n) = real_of_nat m + (-real_of_nat 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";
+
+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";
-Goal "inverse (real_of_posnat x) = inverse (real_of_posnat y) ==> x = y";
-by (rtac (inj_real_of_posnat RS injD) 1);
-by (res_inst_tac [("n2","x")]
- (real_of_posnat_inverse_not_zero RS real_mult_left_cancel RS iffD1) 1);
-by (full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS
- real_not_refl2 RS not_sym) RS real_mult_inv_left]) 1);
-by (asm_full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS
- real_not_refl2 RS not_sym)]) 1);
-qed "real_of_posnat_inverse_inj";
+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)";
+by (auto_tac (claset() addIs [inj_real_of_nat RS injD], simpset()));
+qed "real_of_nat_zero_iff";
+Addsimps [real_of_nat_zero_iff];
+
+Goal "neg z ==> real_of_nat (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];
+
+
+(*----------------------------------------------------------------------------
+ inverse, etc.
+ ----------------------------------------------------------------------------*)
Goal "0 < x ==> 0 < inverse (x::real)";
by (EVERY1[rtac ccontr, dtac real_leI]);
@@ -392,40 +424,6 @@
by (auto_tac (claset() addIs [real_inverse_gt_zero], simpset()));
qed "real_inverse_less_zero";
-Goal "0 < inverse (real_of_posnat n)";
-by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
-qed "real_of_posnat_inverse_gt_zero";
-Addsimps [real_of_posnat_inverse_gt_zero];
-
-Goal "real_of_preal (preal_of_prat (prat_of_pnat (pnat_of_nat N))) = \
-\ real_of_nat (Suc N)";
-by (simp_tac (simpset() addsimps [real_of_nat_def,real_of_posnat_Suc,
- real_add_assoc,(real_of_posnat_def RS meta_eq_to_obj_eq) RS sym]) 1);
-qed "real_of_preal_real_of_nat_Suc";
-
-Goal "x+x = x*(1r+1r)";
-by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
-qed "real_add_self";
-
-Goal "x < x + 1r";
-by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
-by (full_simp_tac (simpset() addsimps [real_zero_less_one,
- real_add_assoc, real_add_left_commute]) 1);
-qed "real_self_less_add_one";
-
-Goal "1r < 1r + 1r";
-by (rtac real_self_less_add_one 1);
-qed "real_one_less_two";
-
-Goal "0 < 1r + 1r";
-by (rtac ([real_zero_less_one, real_one_less_two] MRS order_less_trans) 1);
-qed "real_zero_less_two";
-
-Goal "1r + 1r ~= 0";
-by (rtac (real_zero_less_two RS real_not_refl2 RS not_sym) 1);
-qed "real_two_not_zero";
-Addsimps [real_two_not_zero];
-
Goal "[| (0::real) < z; x < y |] ==> x*z < y*z";
by (rotate_tac 1 1);
by (dtac real_less_sum_gt_zero 1);
@@ -550,66 +548,6 @@
by (auto_tac (claset() addIs [real_mult_self_le], simpset()));
qed "real_mult_self_le2";
-Goal "(EX n. inverse (real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
-by (Step_tac 1);
-by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero
- RS real_mult_less_mono1) 1);
-by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS
- real_inverse_gt_zero RS real_mult_less_mono1) 2);
-by (auto_tac (claset(),
- simpset() addsimps [(real_of_posnat_gt_zero RS
- real_not_refl2 RS not_sym),
- real_mult_assoc]));
-qed "real_of_posnat_inverse_Ex_iff";
-
-Goal "(inverse(real_of_posnat n) < r) = (1r < r * real_of_posnat n)";
-by (Step_tac 1);
-by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero
- RS real_mult_less_mono1) 1);
-by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS
- real_inverse_gt_zero RS real_mult_less_mono1) 2);
-by (auto_tac (claset(), simpset() addsimps [real_mult_assoc]));
-qed "real_of_posnat_inverse_iff";
-
-Goal "(inverse (real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)";
-by (Step_tac 1);
-by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS
- order_less_imp_le RS real_mult_le_le_mono1) 1);
-by (dres_inst_tac [("n3","n")] (real_of_posnat_gt_zero RS
- real_inverse_gt_zero RS order_less_imp_le RS
- real_mult_le_le_mono1) 2);
-by (auto_tac (claset(), simpset() addsimps real_mult_ac));
-qed "real_of_posnat_inverse_le_iff";
-
-Goalw [real_of_posnat_def] "(real_of_posnat n < real_of_posnat m) = (n < m)";
-by Auto_tac;
-qed "real_of_posnat_less_iff";
-
-Addsimps [real_of_posnat_less_iff];
-
-Goal "0 < u ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse u)";
-by (Step_tac 1);
-by (res_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS
- real_inverse_gt_zero RS real_mult_less_cancel1) 1);
-by (res_inst_tac [("x1","u")] ( real_inverse_gt_zero
- RS real_mult_less_cancel1) 2);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_posnat_gt_zero,
- real_not_refl2 RS not_sym]));
-by (res_inst_tac [("z","u")] real_mult_less_cancel2 1);
-by (res_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS
- real_mult_less_cancel2) 3);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_posnat_gt_zero,
- real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
-qed "real_of_posnat_less_inverse_iff";
-
-Goal "0 < u ==> (u = inverse (real_of_posnat n)) = (real_of_posnat n = inverse u)";
-by (auto_tac (claset(),
- simpset() addsimps [real_inverse_inverse, real_of_posnat_gt_zero,
- real_not_refl2 RS not_sym]));
-qed "real_of_posnat_inverse_eq_iff";
-
Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)";
by (ftac order_less_trans 1 THEN assume_tac 1);
by (ftac real_inverse_gt_zero 1);
@@ -625,65 +563,14 @@
not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1);
qed "real_inverse_less_swap";
-Goal "r < r + inverse (real_of_posnat n)";
-by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
-by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
-qed "real_add_inverse_real_of_posnat_less";
-Addsimps [real_add_inverse_real_of_posnat_less];
-
-Goal "r <= r + inverse (real_of_posnat n)";
-by (rtac order_less_imp_le 1);
-by (Simp_tac 1);
-qed "real_add_inverse_real_of_posnat_le";
-Addsimps [real_add_inverse_real_of_posnat_le];
-
-Goal "r + (-inverse (real_of_posnat n)) < r";
-by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
-by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym,
- real_minus_zero_less_iff2]) 1);
-qed "real_add_minus_inverse_real_of_posnat_less";
-Addsimps [real_add_minus_inverse_real_of_posnat_less];
-
-Goal "r + (-inverse (real_of_posnat n)) <= r";
-by (rtac order_less_imp_le 1);
-by (Simp_tac 1);
-qed "real_add_minus_inverse_real_of_posnat_le";
-Addsimps [real_add_minus_inverse_real_of_posnat_le];
-
-Goal "0 < r ==> r*(1r + (-inverse (real_of_posnat n))) < r";
-by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
-by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
-by (auto_tac (claset() addIs [real_mult_order],
- simpset() addsimps [real_add_assoc RS sym,
- real_minus_zero_less_iff2]));
-qed "real_mult_less_self";
-
-Goal "0 <= 1r + (-inverse (real_of_posnat n))";
-by (res_inst_tac [("C","inverse (real_of_posnat n)")] real_le_add_right_cancel 1);
-by (simp_tac (simpset() addsimps [real_add_assoc,
- real_of_posnat_inverse_le_iff]) 1);
-qed "real_add_one_minus_inverse_ge_zero";
-
-Goal "0 < r ==> 0 <= r*(1r + (-inverse (real_of_posnat n)))";
-by (dtac (real_add_one_minus_inverse_ge_zero RS real_mult_le_less_mono1) 1);
-by Auto_tac;
-qed "real_mult_add_one_minus_ge_zero";
-
Goal "(x*y = 0) = (x = 0 | y = (0::real))";
by Auto_tac;
by (blast_tac (claset() addIs [ccontr] addDs [real_mult_not_zero]) 1);
qed "real_mult_is_0";
AddIffs [real_mult_is_0];
-Goal "[| 0 <= x * y; 0 < x |] ==> (0::real) <= y";
-by (ftac real_inverse_gt_zero 1);
-by (dres_inst_tac [("x","inverse x")] real_less_le_mult_order 1);
-by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2);
-by (auto_tac (claset(),
- simpset() addsimps [real_mult_assoc RS sym]));
-qed "real_mult_ge_zero_cancel";
-
-Goal "[|x ~= 0; y ~= 0 |] ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))";
+Goal "[| x ~= 0; y ~= 0 |] \
+\ ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))";
by (asm_full_simp_tac (simpset() addsimps
[real_inverse_distrib,real_add_mult_distrib,
real_mult_assoc RS sym]) 1);
@@ -753,90 +640,3 @@
linorder_not_less RS sym]));
qed "real_mult_le_zero_iff";
-
-(*----------------------------------------------------------------------------
- Another embedding of the naturals in the reals (see real_of_posnat)
- ----------------------------------------------------------------------------*)
-Goalw [real_of_nat_def] "real_of_nat 0 = 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";
-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";
-by (simp_tac (simpset() addsimps
- [real_of_posnat_add,real_add_assoc RS sym]) 1);
-qed "real_of_nat_add";
-
-Goalw [real_of_nat_def] "real_of_nat (Suc n) = real_of_nat n + 1r";
-by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1);
-qed "real_of_nat_Suc";
-Addsimps [real_of_nat_Suc];
-
-Goalw [real_of_nat_def] "(real_of_nat n < real_of_nat m) = (n < m)";
-by Auto_tac;
-qed "real_of_nat_less_iff";
-
-AddIffs [real_of_nat_less_iff];
-
-Goal "inj real_of_nat";
-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";
-
-Goalw [real_of_nat_def] "0 <= real_of_nat n";
-by (res_inst_tac [("C","1r")] real_le_add_right_cancel 1);
-by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
-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";
-by (induct_tac "m" 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_nat_add,
- real_add_mult_distrib, real_add_commute]));
-qed "real_of_nat_mult";
-
-Goal "(real_of_nat n = real_of_nat m) = (n = m)";
-by (auto_tac (claset() addDs [inj_real_of_nat RS injD],
- simpset()));
-qed "real_of_nat_eq_cancel";
-
-Goal "n <= m --> real_of_nat (m - n) = real_of_nat m + (-real_of_nat 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";
-
-(* 05/00 *)
-Goal "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_minus2";
-
-Goalw [real_diff_def]
- "n < m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n";
-by (etac real_of_nat_minus2 1);
-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)";
-by (auto_tac (claset() addIs [inj_real_of_nat RS injD], simpset()));
-qed "real_of_nat_zero_iff";
-AddIffs [real_of_nat_zero_iff];
-
-Goal "neg z ==> real_of_nat (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 Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Real/RealPow.ML Thu Jan 04 10:23:01 2001 +0100
@@ -146,16 +146,15 @@
Goal "(#1::real) <= #2 ^ n";
by (res_inst_tac [("y","#1 ^ n")] order_trans 1);
by (rtac realpow_le 2);
-by (auto_tac (claset() addIs [order_less_imp_le],simpset()));
+by (auto_tac (claset() addIs [order_less_imp_le], simpset()));
qed "two_realpow_ge_one";
Goal "real_of_nat n < #2 ^ n";
by (induct_tac "n" 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
by (stac real_mult_2 1);
by (rtac real_add_less_le_mono 1);
-by (auto_tac (claset(),
- simpset() addsimps [two_realpow_ge_one]));
+by (auto_tac (claset(), simpset() addsimps [two_realpow_ge_one]));
qed "two_realpow_gt";
Addsimps [two_realpow_gt,two_realpow_ge_one];