generalized types of many constants to work over arbitrary vector spaces;
modified theorems using Rep_star to eliminate existential quantifiers
--- a/src/HOL/Complex/CLim.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Complex/CLim.thy Sat Sep 16 02:40:00 2006 +0200
@@ -126,10 +126,9 @@
apply (rule_tac x = xa in star_cases)
apply (auto simp add: starfun star_n_diff star_of_def star_n_eq_iff
CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
apply (drule_tac x = u in spec, auto)
apply (drule_tac x = s in spec, auto, ultra)
-apply (drule sym, auto)
+apply (auto)
done
lemma eq_Abs_star_ALL: "(\<forall>t. P t) = (\<forall>X. P (star_n X))"
@@ -176,7 +175,7 @@
apply (drule_tac x = X in spec, auto)
apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
apply (simp add: CInfinitesimal_hcmod_iff star_of_def
- Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod, blast)
+ Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod)
apply (drule_tac x = r in spec, clarify)
apply (drule FreeUltrafilterNat_all, ultra)
done
@@ -197,10 +196,9 @@
Infinitesimal_FreeUltrafilterNat_iff
star_of_def star_n_eq_iff
Infinitesimal_approx_minus [symmetric])
-apply (rule bexI [OF _ Rep_star_star_n], safe)
apply (drule_tac x = u in spec, auto)
apply (drule_tac x = s in spec, auto, ultra)
-apply (drule sym, auto)
+apply (auto)
done
lemma lemma_CRLIM:
@@ -242,7 +240,6 @@
apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
apply (simp add: CInfinitesimal_hcmod_iff star_of_def
Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod)
-apply (auto simp add: star_of_def star_n_diff)
apply (drule_tac x = r in spec, clarify)
apply (drule FreeUltrafilterNat_all, ultra)
done
--- a/src/HOL/Complex/NSCA.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy Sat Sep 16 02:40:00 2006 +0200
@@ -656,35 +656,32 @@
lemma hcomplex_capproxD1:
"star_n X @c= star_n Y
==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))"
-apply (auto simp add: approx_FreeUltrafilterNat_iff)
+apply (simp add: approx_FreeUltrafilterNat_iff2, safe)
apply (drule capprox_minus_iff [THEN iffD1])
-apply (auto simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
-apply (drule_tac x = m in spec, ultra)
-apply (rename_tac Z x)
-apply (case_tac "X x")
-apply (case_tac "Y x")
+apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
+apply (drule_tac x = m in spec)
+apply (erule ultra, rule FreeUltrafilterNat_all, clarify)
+apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans)
+apply (case_tac "X n")
+apply (case_tac "Y n")
apply (auto simp add: complex_minus complex_add complex_mod
- simp del: realpow_Suc)
-apply (rule_tac y="abs(Z x)" in order_le_less_trans)
-apply (drule_tac t = "Z x" in sym)
-apply (auto simp del: realpow_Suc)
+ simp del: realpow_Suc)
done
(* same proof *)
lemma hcomplex_capproxD2:
"star_n X @c= star_n Y
==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))"
-apply (auto simp add: approx_FreeUltrafilterNat_iff)
+apply (simp add: approx_FreeUltrafilterNat_iff2, safe)
apply (drule capprox_minus_iff [THEN iffD1])
-apply (auto simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
-apply (drule_tac x = m in spec, ultra)
-apply (rename_tac Z x)
-apply (case_tac "X x")
-apply (case_tac "Y x")
-apply (auto simp add: complex_minus complex_add complex_mod simp del: realpow_Suc)
-apply (rule_tac y="abs(Z x)" in order_le_less_trans)
-apply (drule_tac t = "Z x" in sym)
-apply (auto simp del: realpow_Suc)
+apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
+apply (drule_tac x = m in spec)
+apply (erule ultra, rule FreeUltrafilterNat_all, clarify)
+apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans)
+apply (case_tac "X n")
+apply (case_tac "Y n")
+apply (auto simp add: complex_minus complex_add complex_mod
+ simp del: realpow_Suc)
done
lemma hcomplex_capproxI:
@@ -695,10 +692,8 @@
apply (drule approx_minus_iff [THEN iffD1])
apply (rule capprox_minus_iff [THEN iffD2])
apply (auto simp add: mem_cinfmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_add star_n_minus CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], auto)
apply (drule_tac x = "u/2" in spec)
apply (drule_tac x = "u/2" in spec, auto, ultra)
-apply (drule sym, drule sym)
apply (case_tac "X x")
apply (case_tac "Y x")
apply (auto simp add: complex_minus complex_add complex_mod snd_conv fst_conv numeral_2_eq_2)
@@ -725,9 +720,8 @@
"star_n X \<in> CFinite
==> star_n (%n. Re(X n)) \<in> HFinite"
apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n])
apply (rule_tac x = u in exI, ultra)
-apply (drule sym, case_tac "X x")
+apply (case_tac "X x")
apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
apply (rule ccontr, drule linorder_not_less [THEN iffD1])
apply (drule order_less_le_trans, assumption)
@@ -739,9 +733,8 @@
"star_n X \<in> CFinite
==> star_n (%n. Im(X n)) \<in> HFinite"
apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n])
apply (rule_tac x = u in exI, ultra)
-apply (drule sym, case_tac "X x")
+apply (case_tac "X x")
apply (auto simp add: complex_mod simp del: realpow_Suc)
apply (rule ccontr, drule linorder_not_less [THEN iffD1])
apply (drule order_less_le_trans, assumption)
@@ -753,17 +746,16 @@
star_n (%n. Im(X n)) \<in> HFinite
|] ==> star_n X \<in> CFinite"
apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rename_tac Y Z u v)
-apply (rule bexI [OF _ Rep_star_star_n])
+apply (rename_tac u v)
apply (rule_tac x = "2* (u + v) " in exI)
apply ultra
-apply (drule sym, case_tac "X x")
+apply (case_tac "X x")
apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
apply (subgoal_tac "0 < u")
prefer 2 apply arith
apply (subgoal_tac "0 < v")
prefer 2 apply arith
-apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
+apply (subgoal_tac "sqrt (abs (Re (X x)) ^ 2 + abs (Im (X x)) ^ 2) < 2*u + 2*v")
apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
apply (simp add: power2_eq_square)
done
@@ -1201,7 +1193,6 @@
"\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==>
star_n X - hcomplex_of_complex x \<in> CInfinitesimal"
apply (simp add: star_n_diff CInfinitesimal_hcmod_iff star_of_def Infinitesimal_FreeUltrafilterNat_iff hcmod)
-apply (rule bexI, auto)
apply (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset)
done
--- a/src/HOL/Hyperreal/HTranscendental.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Sat Sep 16 02:40:00 2006 +0200
@@ -362,7 +362,6 @@
lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
apply (cases x)
apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], auto)
apply (rule_tac x = "exp u" in exI)
apply ultra
done
--- a/src/HOL/Hyperreal/HyperDef.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Sat Sep 16 02:40:00 2006 +0200
@@ -188,6 +188,9 @@
lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
by (rule inj_onI, simp)
+lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)"
+by (cases x, simp add: star_n_def)
+
lemma Rep_star_star_n_iff [simp]:
"(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
by (simp add: star_n_def)
--- a/src/HOL/Hyperreal/HyperNat.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Sat Sep 16 02:40:00 2006 +0200
@@ -242,27 +242,20 @@
Free Ultrafilter*}
lemma HNatInfinite_FreeUltrafilterNat:
- "x \<in> HNatInfinite
- ==> \<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}: FreeUltrafilterNat"
-apply (cases x)
-apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
-apply (rule bexI [OF _ Rep_star_star_n], clarify)
-apply (auto simp add: hypnat_of_nat_def star_n_less)
+ "star_n X \<in> HNatInfinite ==> \<forall>u. {n. u < X n}: FreeUltrafilterNat"
+apply (auto simp add: HNatInfinite_iff SHNat_eq)
+apply (drule_tac x="star_of u" in spec, simp)
+apply (simp add: star_of_def star_n_less)
done
lemma FreeUltrafilterNat_HNatInfinite:
- "\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}: FreeUltrafilterNat
- ==> x \<in> HNatInfinite"
-apply (cases x)
-apply (auto simp add: star_n_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
-apply (drule spec, ultra, auto)
-done
+ "\<forall>u. {n. u < X n}: FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
+by (auto simp add: star_n_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
lemma HNatInfinite_FreeUltrafilterNat_iff:
- "(x \<in> HNatInfinite) =
- (\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}: FreeUltrafilterNat)"
-by (blast intro: HNatInfinite_FreeUltrafilterNat
- FreeUltrafilterNat_HNatInfinite)
+ "(star_n X \<in> HNatInfinite) = (\<forall>u. {n. u < X n}: FreeUltrafilterNat)"
+by (rule iffI [OF HNatInfinite_FreeUltrafilterNat
+ FreeUltrafilterNat_HNatInfinite])
lemma HNatInfinite_gt_one [simp]: "x \<in> HNatInfinite ==> (1::hypnat) < x"
by (auto simp add: HNatInfinite_iff)
@@ -370,10 +363,11 @@
lemma HNatInfinite_inverse_Infinitesimal [simp]:
"n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
apply (cases n)
-apply (auto simp add: hypreal_of_hypnat star_n_inverse
- HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
-apply (rule bexI [OF _ Rep_star_star_n], auto)
-apply (drule_tac x = "m + 1" in spec, ultra)
+apply (auto simp add: hypreal_of_hypnat star_n_inverse real_norm_def
+ HNatInfinite_FreeUltrafilterNat_iff
+ Infinitesimal_FreeUltrafilterNat_iff2)
+apply (drule_tac x="Suc m" in spec)
+apply (erule ultra, simp)
done
lemma HNatInfinite_hypreal_of_hypnat_gt_zero:
--- a/src/HOL/Hyperreal/Lim.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Sat Sep 16 02:40:00 2006 +0200
@@ -15,25 +15,24 @@
text{*Standard and Nonstandard Definitions*}
definition
- LIM :: "[real=>real,real,real] => bool"
+ LIM :: "[real => 'a::real_normed_vector, real, 'a] => bool"
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
"f -- a --> L =
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
- --> \<bar>f x + -L\<bar> < r)"
+ --> norm (f x + -L) < r)"
- NSLIM :: "[real=>real,real,real] => bool"
+ NSLIM :: "[real => 'a::real_normed_vector, real, 'a] => bool"
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
- "f -- a --NS> L = (\<forall>x. (x \<noteq> hypreal_of_real a &
- x @= hypreal_of_real a -->
- ( *f* f) x @= hypreal_of_real L))"
+ "f -- a --NS> L =
+ (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
- isCont :: "[real=>real,real] => bool"
+ isCont :: "[real => 'a::real_normed_vector, real] => bool"
"isCont f a = (f -- a --> (f a))"
- isNSCont :: "[real=>real,real] => bool"
+ isNSCont :: "[real => 'a::real_normed_vector, real] => bool"
--{*NS definition dispenses with limit notions*}
- "isNSCont f a = (\<forall>y. y @= hypreal_of_real a -->
- ( *f* f) y @= hypreal_of_real (f a))"
+ "isNSCont f a = (\<forall>y. y @= star_of a -->
+ ( *f* f) y @= star_of (f a))"
deriv:: "[real=>real,real,real] => bool"
--{*Differentiation: D is derivative of function f at x*}
@@ -79,12 +78,17 @@
lemma LIM_eq:
"f -- a --> L =
- (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
+ (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r)"
by (simp add: LIM_def diff_minus)
+lemma LIM_I:
+ "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r)
+ ==> f -- a --> L"
+by (simp add: LIM_eq)
+
lemma LIM_D:
"[| f -- a --> L; 0<r |]
- ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r"
+ ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r"
by (simp add: LIM_eq)
lemma LIM_const [simp]: "(%x. k) -- x --> k"
@@ -93,76 +97,55 @@
lemma LIM_add:
assumes f: "f -- a --> L" and g: "g -- a --> M"
shows "(%x. f x + g(x)) -- a --> (L + M)"
-proof (unfold LIM_eq, clarify)
+proof (rule LIM_I)
fix r :: real
assume r: "0 < r"
from LIM_D [OF f half_gt_zero [OF r]]
obtain fs
where fs: "0 < fs"
- and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x - L\<bar> < r/2"
+ and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> norm (f x - L) < r/2"
by blast
from LIM_D [OF g half_gt_zero [OF r]]
obtain gs
where gs: "0 < gs"
- and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x - M\<bar> < r/2"
+ and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> norm (g x - M) < r/2"
by blast
- show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r"
+ show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm (f x + g x - (L + M)) < r"
proof (intro exI conjI strip)
show "0 < min fs gs" by (simp add: fs gs)
fix x :: real
assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
hence "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
with fs_lt gs_lt
- have "\<bar>f x - L\<bar> < r/2" and "\<bar>g x - M\<bar> < r/2" by blast+
- hence "\<bar>f x - L\<bar> + \<bar>g x - M\<bar> < r" by arith
- thus "\<bar>f x + g x - (L + M)\<bar> < r"
- by (blast intro: abs_diff_triangle_ineq order_le_less_trans)
+ have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+
+ hence "norm (f x - L) + norm (g x - M) < r" by arith
+ thus "norm (f x + g x - (L + M)) < r"
+ by (blast intro: norm_diff_triangle_ineq order_le_less_trans)
qed
qed
+lemma minus_diff_minus:
+ fixes a b :: "'a::ab_group_add"
+ shows "(- a) - (- b) = - (a - b)"
+by simp
+
lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
-apply (simp add: LIM_eq)
-apply (subgoal_tac "\<forall>x. \<bar>- f x + L\<bar> = \<bar>f x - L\<bar>")
-apply (simp_all add: abs_if)
-done
+by (simp only: LIM_eq minus_diff_minus norm_minus_cancel)
lemma LIM_add_minus:
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
-by (blast dest: LIM_add LIM_minus)
+by (intro LIM_add LIM_minus)
lemma LIM_diff:
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
-by (simp add: diff_minus LIM_add_minus)
+by (simp only: diff_minus LIM_add LIM_minus)
lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
-proof (simp add: linorder_neq_iff LIM_eq, elim disjE)
- assume k: "k < L"
- show "\<exists>r>0. \<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
- proof (intro exI conjI strip)
- show "0 < L-k" by (simp add: k compare_rls)
- fix s :: real
- assume s: "0<s"
- { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
- next
- from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
- next
- from s show "~ \<bar>k-L\<bar> < L-k" by (simp add: abs_if) }
- qed
-next
- assume k: "L < k"
- show "\<exists>r>0.\<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
- proof (intro exI conjI strip)
- show "0 < k-L" by (simp add: k compare_rls)
- fix s :: real
- assume s: "0<s"
- { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
- next
- from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
- next
- from s show "~ \<bar>k-L\<bar> < k-L" by (simp add: abs_if) }
- qed
-qed
+apply (simp add: LIM_eq)
+apply (rule_tac x="norm (k - L)" in exI, simp, safe)
+apply (rule_tac x="a + s/2" in exI, simp)
+done
lemma LIM_const_eq: "(%x. k) -- x --> L ==> k = L"
apply (rule ccontr)
@@ -175,31 +158,34 @@
done
lemma LIM_mult_zero:
+ fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
assumes f: "f -- a --> 0" and g: "g -- a --> 0"
shows "(%x. f(x) * g(x)) -- a --> 0"
-proof (simp add: LIM_eq abs_mult, clarify)
+proof (rule LIM_I, simp)
fix r :: real
assume r: "0<r"
from LIM_D [OF f zero_less_one]
obtain fs
where fs: "0 < fs"
- and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x\<bar> < 1"
+ and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> norm (f x) < 1"
by auto
from LIM_D [OF g r]
obtain gs
where gs: "0 < gs"
- and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x\<bar> < r"
+ and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> norm (g x) < r"
by auto
- show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x\<bar> * \<bar>g x\<bar> < r)"
+ show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm (f x * g x) < r)"
proof (intro exI conjI strip)
show "0 < min fs gs" by (simp add: fs gs)
fix x :: real
assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
hence "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
with fs_lt gs_lt
- have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by blast+
- hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less)
- thus "\<bar>f x\<bar> * \<bar>g x\<bar> < r" by simp
+ have "norm (f x) < 1" and "norm (g x) < r" by blast+
+ hence "norm (f x) * norm (g x) < 1*r"
+ by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero])
+ thus "norm (f x * g x) < r"
+ by (simp add: order_le_less_trans [OF norm_mult_ineq])
qed
qed
@@ -223,62 +209,71 @@
text{*Standard and NS definitions of Limit*} (*NEEDS STRUCTURING*)
lemma LIM_NSLIM:
- "f -- x --> L ==> f -- x --NS> L"
-apply (simp add: LIM_def NSLIM_def approx_def)
+ "f -- a --> L ==> f -- a --NS> L"
+apply (simp add: LIM_def NSLIM_def approx_def, safe)
+apply (rule_tac x="x" in star_cases)
+apply (simp add: star_of_def star_n_minus star_n_add starfun)
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac x = xa in star_cases)
-apply (auto simp add: real_add_minus_iff starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
-apply (rule bexI [OF _ Rep_star_star_n], clarify)
+apply (simp add: star_n_eq_iff)
apply (drule_tac x = u in spec, clarify)
apply (drule_tac x = s in spec, clarify)
-apply (subgoal_tac "\<forall>n::nat. (Xa n) \<noteq> x & \<bar>(Xa n) + - x\<bar> < s --> \<bar>f (Xa n) + - L\<bar> < u")
-prefer 2 apply blast
-apply (drule FreeUltrafilterNat_all, ultra)
+apply (simp only: FUFNat.Collect_not [symmetric])
+apply (elim ultra, simp)
done
subsubsection{*Limit: The NS definition implies the standard definition.*}
-lemma lemma_LIM: "\<forall>s>0.\<exists>xa. xa \<noteq> x &
- \<bar>xa + - x\<bar> < s & r \<le> \<bar>f xa + -L\<bar>
- ==> \<forall>n::nat. \<exists>xa. xa \<noteq> x &
- \<bar>xa + -x\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f xa + -L\<bar>"
+lemma lemma_LIM:
+ fixes L :: "'a::real_normed_vector"
+ shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> \<bar>x + - a\<bar> < s \<and> \<not> norm (f x + -L) < r
+ ==> \<forall>n::nat. \<exists>x. x \<noteq> a \<and>
+ \<bar>x + -a\<bar> < inverse(real(Suc n)) \<and> \<not> norm (f x + -L) < r"
apply clarify
apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
done
lemma lemma_skolemize_LIM2:
- "\<forall>s>0.\<exists>xa. xa \<noteq> x & \<bar>xa + - x\<bar> < s & r \<le> \<bar>f xa + -L\<bar>
- ==> \<exists>X. \<forall>n::nat. X n \<noteq> x &
- \<bar>X n + -x\<bar> < inverse(real(Suc n)) & r \<le> abs(f (X n) + -L)"
+ fixes L :: "'a::real_normed_vector"
+ shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> \<bar>x + - a\<bar> < s \<and> \<not> norm (f x + -L) < r
+ ==> \<exists>X. \<forall>n::nat. X n \<noteq> a \<and>
+ \<bar>X n + -a\<bar> < inverse(real(Suc n)) \<and> \<not> norm(f (X n) + -L) < r"
apply (drule lemma_LIM)
apply (drule choice, blast)
done
-lemma lemma_simp: "\<forall>n. X n \<noteq> x &
- \<bar>X n + - x\<bar> < inverse (real(Suc n)) &
- r \<le> abs (f (X n) + - L) ==>
- \<forall>n. \<bar>X n + - x\<bar> < inverse (real(Suc n))"
+lemma FreeUltrafilterNat_most: "\<exists>N. \<forall>n\<ge>N. P n \<Longrightarrow> {n. P n} \<in> \<U>"
+apply (erule exE)
+apply (rule_tac u="{n. N \<le> n}" in FUFNat.subset)
+apply (rule cofinite_mem_FreeUltrafilterNat)
+apply (simp add: Collect_neg_eq [symmetric])
+apply (simp add: linorder_not_le finite_nat_segment)
+apply fast
+done
+
+lemma lemma_simp: "\<forall>n. X n \<noteq> a &
+ \<bar>X n + - a\<bar> < inverse (real(Suc n)) &
+ \<not> norm (f (X n) + - L) < r ==>
+ \<forall>n. \<bar>X n + - a\<bar> < inverse (real(Suc n))"
by auto
text{*NSLIM => LIM*}
-lemma NSLIM_LIM: "f -- x --NS> L ==> f -- x --> L"
+lemma NSLIM_LIM: "f -- a --NS> L ==> f -- a --> L"
apply (simp add: LIM_def NSLIM_def approx_def)
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, clarify)
-apply (rule ccontr, simp)
-apply (simp add: linorder_not_less)
+apply (rule ccontr, simp, clarify)
apply (drule lemma_skolemize_LIM2, safe)
apply (drule_tac x = "star_n X" in spec)
-apply (auto simp add: starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
-apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff star_of_def star_n_minus star_n_add star_n_eq_iff, blast)
-apply (drule spec, drule mp, assumption)
-apply (drule FreeUltrafilterNat_all, ultra)
+apply (drule mp, rule conjI)
+apply (simp add: star_of_def star_n_eq_iff)
+apply (rule real_seq_to_hypreal_Infinitesimal, simp)
+apply (simp add: starfun star_of_def star_n_minus star_n_add)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
+apply (drule spec, drule (1) mp)
+apply simp
done
-
theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
by (blast intro: LIM_NSLIM NSLIM_LIM)
@@ -286,12 +281,15 @@
The properties hold for standard limits as well!*}
lemma NSLIM_mult:
- "[| f -- x --NS> l; g -- x --NS> m |]
+ fixes l m :: "'a::real_normed_algebra"
+ shows "[| f -- x --NS> l; g -- x --NS> m |]
==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
lemma LIM_mult2:
- "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) * g(x)) -- x --> (l * m)"
+ fixes l m :: "'a::real_normed_algebra"
+ shows "[| f -- x --> l; g -- x --> m |]
+ ==> (%x. f(x) * g(x)) -- x --> (l * m)"
by (simp add: LIM_NSLIM_iff NSLIM_mult)
lemma NSLIM_add:
@@ -325,14 +323,18 @@
lemma NSLIM_inverse:
- "[| f -- a --NS> L; L \<noteq> 0 |]
+ fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
+ shows "[| f -- a --NS> L; L \<noteq> 0 |]
==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
apply (simp add: NSLIM_def, clarify)
apply (drule spec)
-apply (auto simp add: hypreal_of_real_approx_inverse)
+apply (auto simp add: star_of_approx_inverse)
done
-lemma LIM_inverse: "[| f -- a --> L; L \<noteq> 0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)"
+lemma LIM_inverse:
+ fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
+ shows "[| f -- a --> L; L \<noteq> 0 |]
+ ==> (%x. inverse(f(x))) -- a --> (inverse L)"
by (simp add: LIM_NSLIM_iff NSLIM_inverse)
@@ -357,19 +359,15 @@
apply (auto simp add: diff_minus add_assoc)
done
-lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"
+lemma NSLIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- x --NS> L)"
apply (simp add: NSLIM_def)
apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
simp add: hypreal_epsilon_not_zero)
done
-lemma NSLIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- x --NS> L)"
-apply (simp add: NSLIM_def)
-apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
-apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
- simp add: hypreal_epsilon_not_zero)
-done
+lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"
+by (rule NSLIM_const_not_eq)
lemma NSLIM_const_eq: "(%x. k) -- x --NS> L ==> k = L"
apply (rule ccontr)
@@ -381,19 +379,24 @@
apply (drule NSLIM_minus)
apply (drule NSLIM_add, assumption)
apply (auto dest!: NSLIM_const_eq [symmetric])
+apply (simp add: diff_def [symmetric])
done
lemma LIM_unique2: "[| f -- x --> L; f -- x --> M |] ==> L = M"
by (simp add: LIM_NSLIM_iff NSLIM_unique)
-lemma NSLIM_mult_zero: "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
+lemma NSLIM_mult_zero:
+ fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
+ shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
by (drule NSLIM_mult, auto)
(* we can use the corresponding thm LIM_mult2 *)
(* for standard definition of limit *)
-lemma LIM_mult_zero2: "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
+lemma LIM_mult_zero2:
+ fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
+ shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
by (drule LIM_mult2, auto)
@@ -472,7 +475,9 @@
by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
text{*mult continuous*}
-lemma isCont_mult: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
+lemma isCont_mult:
+ fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
+ shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
by (auto intro!: starfun_mult_HFinite_approx
simp del: starfun_mult [symmetric]
simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
@@ -492,12 +497,15 @@
by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus)
lemma isCont_inverse:
- "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
+ fixes f :: "real \<Rightarrow> 'a::{real_normed_div_algebra,division_by_zero}"
+ shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
apply (simp add: isCont_def)
apply (blast intro: LIM_inverse)
done
-lemma isNSCont_inverse: "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
+lemma isNSCont_inverse:
+ fixes f :: "real \<Rightarrow> 'a::{real_normed_div_algebra,division_by_zero}"
+ shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
lemma isCont_diff:
@@ -578,17 +586,15 @@
lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f"
apply (simp add: isNSUCont_def isUCont_def approx_def)
+apply (simp add: all_star_eq starfun star_n_minus star_n_add)
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac x = x in star_cases)
-apply (rule_tac x = y in star_cases)
-apply (auto simp add: starfun star_n_minus star_n_add)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
+apply (rename_tac Xa Xb u)
apply (drule_tac x = u in spec, clarify)
apply (drule_tac x = s in spec, clarify)
apply (subgoal_tac "\<forall>n::nat. abs ((Xa n) + - (Xb n)) < s --> abs (f (Xa n) + - f (Xb n)) < u")
prefer 2 apply blast
apply (erule_tac V = "\<forall>x y. \<bar>x + - y\<bar> < s --> \<bar>f x + - f y\<bar> < u" in thin_rl)
-apply (drule FreeUltrafilterNat_all, ultra)
+apply (erule ultra, simp)
done
lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
@@ -615,17 +621,17 @@
lemma isNSUCont_isUCont:
"isNSUCont f ==> isUCont f"
-apply (simp add: isNSUCont_def isUCont_def approx_def)
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
+apply (simp add: isNSUCont_def isUCont_def approx_def, safe)
apply (rule ccontr, simp)
apply (simp add: linorder_not_less)
apply (drule lemma_skolemize_LIM2u, safe)
apply (drule_tac x = "star_n X" in spec)
apply (drule_tac x = "star_n Y" in spec)
-apply (simp add: starfun star_n_minus star_n_add, auto)
-apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus star_n_add, blast)
-apply (drule_tac x = r in spec, clarify)
+apply (drule mp)
+apply (rule real_seq_to_hypreal_Infinitesimal2, simp)
+apply (simp add: all_star_eq starfun star_n_minus star_n_add)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
+apply (drule spec, drule (1) mp)
apply (drule FreeUltrafilterNat_all, ultra)
done
@@ -677,11 +683,6 @@
subsubsection{*Alternative definition for differentiability*}
-lemma LIM_I:
- "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)
- ==> f -- a --> L"
-by (simp add: LIM_eq)
-
lemma DERIV_LIM_iff:
"((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
@@ -695,14 +696,14 @@
and s_lt: "\<forall>x. x \<noteq> 0 & \<bar>x\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r"
by auto
show "\<exists>s. 0 < s \<and>
- (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>(f x - f a) / (x-a) - D\<bar> < r)"
+ (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm ((f x - f a) / (x-a) - D) < r)"
proof (intro exI conjI strip)
show "0 < s" by (rule s)
next
fix x::real
assume "x \<noteq> a \<and> \<bar>x-a\<bar> < s"
with s_lt [THEN spec [where x="x-a"]]
- show "\<bar>(f x - f a) / (x-a) - D\<bar> < r" by auto
+ show "norm ((f x - f a) / (x-a) - D) < r" by auto
qed
next
fix r::real
@@ -714,14 +715,14 @@
and s_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>(f x - f a)/(x-a) - D\<bar> < r"
by auto
show "\<exists>s. 0 < s \<and>
- (\<forall>x. x \<noteq> 0 & \<bar>x - 0\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r)"
+ (\<forall>x. x \<noteq> 0 & \<bar>x - 0\<bar> < s --> norm ((f (a + x) - f a) / x - D) < r)"
proof (intro exI conjI strip)
show "0 < s" by (rule s)
next
fix x::real
assume "x \<noteq> 0 \<and> \<bar>x - 0\<bar> < s"
with s_lt [THEN spec [where x="x+a"]]
- show "\<bar>(f (a + x) - f a) / x - D\<bar> < r" by (auto simp add: add_ac)
+ show "norm ((f (a + x) - f a) / x - D) < r" by (auto simp add: add_ac)
qed
qed
@@ -1236,7 +1237,7 @@
lemma f_inc_g_dec_Beq_f: "[| \<forall>n. f(n) \<le> f(Suc n);
\<forall>n. g(Suc n) \<le> g(n);
\<forall>n. f(n) \<le> g(n) |]
- ==> Bseq f"
+ ==> Bseq (f :: nat \<Rightarrow> real)"
apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
apply (induct_tac "n")
apply (auto intro: order_trans)
@@ -1248,7 +1249,7 @@
lemma f_inc_g_dec_Beq_g: "[| \<forall>n. f(n) \<le> f(Suc n);
\<forall>n. g(Suc n) \<le> g(n);
\<forall>n. f(n) \<le> g(n) |]
- ==> Bseq g"
+ ==> Bseq (g :: nat \<Rightarrow> real)"
apply (subst Bseq_minus_iff [symmetric])
apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f)
apply auto
@@ -1282,7 +1283,7 @@
lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
\<forall>n. g(Suc n) \<le> g(n);
\<forall>n. f(n) \<le> g(n) |]
- ==> \<exists>l m. l \<le> m & ((\<forall>n. f(n) \<le> l) & f ----> l) &
+ ==> \<exists>l m :: real. l \<le> m & ((\<forall>n. f(n) \<le> l) & f ----> l) &
((\<forall>n. m \<le> g(n)) & g ----> m)"
apply (subgoal_tac "monoseq f & monoseq g")
prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc)
@@ -1299,7 +1300,7 @@
\<forall>n. g(Suc n) \<le> g(n);
\<forall>n. f(n) \<le> g(n);
(%n. f(n) - g(n)) ----> 0 |]
- ==> \<exists>l. ((\<forall>n. f(n) \<le> l) & f ----> l) &
+ ==> \<exists>l::real. ((\<forall>n. f(n) \<le> l) & f ----> l) &
((\<forall>n. l \<le> g(n)) & g ----> l)"
apply (drule lemma_nest, auto)
apply (subgoal_tac "l = m")
@@ -1414,7 +1415,7 @@
subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*}
-lemma IVT: "[| f(a) \<le> y; y \<le> f(b);
+lemma IVT: "[| f(a) \<le> (y::real); y \<le> f(b);
a \<le> b;
(\<forall>x. a \<le> x & x \<le> b --> isCont f x) |]
==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
@@ -1441,7 +1442,7 @@
apply (case_tac "x \<le> aa", simp_all)
done
-lemma IVT2: "[| f(b) \<le> y; y \<le> f(a);
+lemma IVT2: "[| f(b) \<le> (y::real); y \<le> f(a);
a \<le> b;
(\<forall>x. a \<le> x & x \<le> b --> isCont f x)
|] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
@@ -1451,13 +1452,13 @@
done
(*HOL style here: object-level formulations*)
-lemma IVT_objl: "(f(a) \<le> y & y \<le> f(b) & a \<le> b &
+lemma IVT_objl: "(f(a) \<le> (y::real) & y \<le> f(b) & a \<le> b &
(\<forall>x. a \<le> x & x \<le> b --> isCont f x))
--> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
apply (blast intro: IVT)
done
-lemma IVT2_objl: "(f(b) \<le> y & y \<le> f(a) & a \<le> b &
+lemma IVT2_objl: "(f(b) \<le> (y::real) & y \<le> f(a) & a \<le> b &
(\<forall>x. a \<le> x & x \<le> b --> isCont f x))
--> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
apply (blast intro: IVT2)
@@ -1467,7 +1468,7 @@
lemma isCont_bounded:
"[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
- ==> \<exists>M. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
+ ==> \<exists>M::real. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M)" in lemma_BOLZANO2)
apply safe
apply simp_all
@@ -1497,7 +1498,7 @@
by (blast intro: reals_complete)
lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
- ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
+ ==> \<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
(\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
in lemma_reals_complete)
@@ -1513,7 +1514,7 @@
lemma isCont_eq_Ub:
assumes le: "a \<le> b"
and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
- shows "\<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
+ shows "\<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
(\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
proof -
from isCont_has_Ub [OF le con]
@@ -1553,7 +1554,7 @@
text{*Same theorem for lower bound*}
lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
- ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
+ ==> \<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
(\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
prefer 2 apply (blast intro: isCont_minus)
@@ -1566,7 +1567,7 @@
text{*Another version.*}
lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
- ==> \<exists>L M. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
+ ==> \<exists>L M::real. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
(\<forall>y. L \<le> y & y \<le> M --> (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))"
apply (frule isCont_eq_Lb)
apply (frule_tac [2] isCont_eq_Ub)
@@ -1925,6 +1926,7 @@
strict maximum at an end point, not in the middle.*}
lemma lemma_isCont_inj:
+ fixes f :: "real \<Rightarrow> real"
assumes d: "0 < d"
and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
@@ -1966,7 +1968,8 @@
text{*Similar version for lower bound.*}
lemma lemma_isCont_inj2:
- "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
+ fixes f g :: "real \<Rightarrow> real"
+ shows "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
apply (insert lemma_isCont_inj
@@ -1978,6 +1981,7 @@
@{text "f[[x - d, x + d]]"} .*}
lemma isCont_inj_range:
+ fixes f :: "real \<Rightarrow> real"
assumes d: "0 < d"
and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
@@ -2205,35 +2209,35 @@
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
proof -
{
- from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r" by (unfold LIM_def)
+ from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (X x + -L) < r" by (unfold LIM_def)
fix S
assume as: "(\<forall>n. S n \<noteq> a) \<and> S ----> a"
then have "S ----> a" by auto
- then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < r))" by (unfold LIMSEQ_def)
+ then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (S n + -a) < r))" by (unfold LIMSEQ_def)
{
fix r
- from Xdef have Xdef2: "0 < r --> (\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by simp
+ from Xdef have Xdef2: "0 < r --> (\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by simp
{
assume rgz: "0 < r"
- from Xdef2 rgz have "\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r" by simp
- then obtain s where sdef: "s > 0 \<and> (\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>X x + -L\<bar> < r)" by auto
- then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>X x + -L\<bar> < r" by auto
+ from Xdef2 rgz have "\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r" by simp
+ then obtain s where sdef: "s > 0 \<and> (\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (X x + -L) < r)" by auto
+ then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (X x + -L) < r" by auto
{
fix n
- from aux have "S n \<noteq> a \<and> \<bar>S n + -a\<bar> < s \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
- with as have imp2: "\<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" by auto
+ from aux have "S n \<noteq> a \<and> \<bar>S n + -a\<bar> < s \<longrightarrow> norm (X (S n) + -L) < r" by simp
+ with as have imp2: "\<bar>S n + -a\<bar> < s --> norm (X (S n) + -L) < r" by auto
}
- hence "\<forall>n. \<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" ..
+ hence "\<forall>n. \<bar>S n + -a\<bar> < s --> norm (X (S n) + -L) < r" ..
moreover
from Sdef sdef have imp1: "\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto
then obtain no where "\<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto
- ultimately have "\<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
- hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by auto
+ ultimately have "\<forall>n. no \<le> n \<longrightarrow> norm (X (S n) + -L) < r" by simp
+ hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> norm (X (S n) + -L) < r" by auto
}
}
- hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X (S n) + -L\<bar> < r))" by simp
+ hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X (S n) + -L) < r))" by simp
hence "(\<lambda>n. X (S n)) ----> L" by (fold LIMSEQ_def)
}
thus ?thesis by simp
@@ -2246,12 +2250,12 @@
shows "X -- a --> L"
proof (rule ccontr)
assume "\<not> (X -- a --> L)"
- hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by (unfold LIM_def)
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by simp
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r)" by (simp add: linorder_not_less)
- then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r))" by auto
+ hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by (unfold LIM_def)
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by simp
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r)" by (simp add: linorder_not_less)
+ then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r))" by auto
- let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
+ let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
have "?F ----> a"
proof -
{
@@ -2270,10 +2274,10 @@
"\<bar>?F n + -a\<bar> < inverse (real (Suc n))"
proof -
from rdef have
- "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
+ "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
by simp
hence
- "(?F n)\<noteq>a \<and> \<bar>(?F n) + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X (?F n) + -L\<bar> \<ge> r"
+ "(?F n)\<noteq>a \<and> \<bar>(?F n) + -a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) + -L) \<ge> r"
by (simp add: some_eq_ex [symmetric])
thus ?thesis by simp
qed
@@ -2291,7 +2295,7 @@
{
fix n
from rdef have
- "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
+ "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
by simp
hence "?F n \<noteq> a" by (simp add: some_eq_ex [symmetric])
}
@@ -2307,15 +2311,15 @@
obtain n where "n = no + 1" by simp
then have nolen: "no \<le> n" by simp
(* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
- from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r)" ..
+ from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r)" ..
- then have "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r" by simp
+ then have "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r" by simp
- hence "\<bar>X (?F n) + -L\<bar> \<ge> r" by (simp add: some_eq_ex [symmetric])
- with nolen have "\<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r" by auto
+ hence "norm (X (?F n) + -L) \<ge> r" by (simp add: some_eq_ex [symmetric])
+ with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> r" by auto
}
- then have "(\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r)" by simp
- with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> e)" by auto
+ then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> r)" by simp
+ with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> e)" by auto
thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
qed
ultimately show False by simp
@@ -2352,26 +2356,26 @@
proof -
have "f -- a --> L" .
hence
- fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>f x + -L\<bar> < r"
+ fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (f x + -L) < r"
by (unfold LIM_def)
{
fix r::real
assume rgz: "0 < r"
- with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s --> \<bar>f x + -L\<bar> < r" by simp
- then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>f x + -L\<bar> < r" by auto
- from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by auto
+ with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s --> norm (f x + -L) < r" by simp
+ then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (f x + -L) < r" by auto
+ from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto
{
fix x::real
- from ax2 have nt: "(x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
+ from ax2 have nt: "(x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" ..
moreover have "((x+c)\<noteq>a) = (x\<noteq>(a-c))" by auto
moreover have "((x+c) + -a) = (x + -(a-c))" by simp
- ultimately have "x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by simp
+ ultimately have "x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by simp
}
- then have "\<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
- with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by auto
+ then have "\<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" ..
+ with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto
}
then have
- "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & \<bar>x + -(a-c)\<bar> < s --> \<bar>f (x+c) + -L\<bar> < r" by simp
+ "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & \<bar>x + -(a-c)\<bar> < s --> norm (f (x+c) + -L) < r" by simp
thus ?thesis by (fold LIM_def)
qed
--- a/src/HOL/Hyperreal/NSA.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Sat Sep 16 02:40:00 2006 +0200
@@ -25,7 +25,8 @@
HInfinite :: "('a::real_normed_vector) star set"
"HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
- approx :: "[hypreal, hypreal] => bool" (infixl "@=" 50)
+ approx :: "['a::real_normed_vector star, 'a star] => bool"
+ (infixl "@=" 50)
--{*the `infinitely close' relation*}
"(x @= y) = ((x + -y) \<in> Infinitesimal)"
@@ -33,10 +34,10 @@
--{*the standard part of a hyperreal*}
"st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
- monad :: "hypreal => hypreal set"
+ monad :: "'a::real_normed_vector star => 'a star set"
"monad x = {y. x @= y}"
- galaxy :: "hypreal => hypreal set"
+ galaxy :: "'a::real_normed_vector star => 'a star set"
"galaxy x = {y. (x + -y) \<in> HFinite}"
const_syntax (xsymbols)
@@ -609,7 +610,7 @@
lemma approx_refl [iff]: "x @= x"
by (simp add: approx_def Infinitesimal_def)
-lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y"
+lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"
by (simp add: add_commute)
lemma approx_sym: "x @= y ==> y @= x"
@@ -689,7 +690,7 @@
lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"
proof (unfold approx_def)
assume inf: "a + - b \<in> Infinitesimal" "c + - d \<in> Infinitesimal"
- have "a + c + - (b + d) = (a + - b) + (c + - d)" by arith
+ have "a + c + - (b + d) = (a + - b) + (c + - d)" by simp
also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add)
finally show "a + c + - (b + d) \<in> Infinitesimal" .
qed
@@ -709,23 +710,38 @@
lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
by (blast intro!: approx_add approx_minus)
-lemma approx_mult1: "[| a @= b; c: HFinite|] ==> a*c @= b*c"
+lemma approx_mult1:
+ fixes a b c :: "'a::real_normed_algebra star"
+ shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"
by (simp add: approx_def Infinitesimal_HFinite_mult minus_mult_left
left_distrib [symmetric]
del: minus_mult_left [symmetric])
-lemma approx_mult2: "[|a @= b; c: HFinite|] ==> c*a @= c*b"
-by (simp add: approx_mult1 mult_commute)
+lemma approx_mult2:
+ fixes a b c :: "'a::real_normed_algebra star"
+ shows "[|a @= b; c: HFinite|] ==> c*a @= c*b"
+by (simp add: approx_def Infinitesimal_HFinite_mult2 minus_mult_right
+ right_distrib [symmetric]
+ del: minus_mult_right [symmetric])
-lemma approx_mult_subst: "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
+lemma approx_mult_subst:
+ fixes u v x y :: "'a::real_normed_algebra star"
+ shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
by (blast intro: approx_mult2 approx_trans)
-lemma approx_mult_subst2: "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
+lemma approx_mult_subst2:
+ fixes u v x y :: "'a::real_normed_algebra star"
+ shows "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
by (blast intro: approx_mult1 approx_trans)
+lemma approx_mult_subst_star_of:
+ fixes u x y :: "'a::real_normed_algebra star"
+ shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v"
+by (auto intro: approx_mult_subst2)
+
lemma approx_mult_subst_SReal:
"[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
-by (auto intro: approx_mult_subst2)
+by (rule approx_mult_subst_star_of)
lemma approx_eq_imp: "a = b ==> a @= b"
by (simp add: approx_def)
@@ -802,51 +818,60 @@
apply (auto simp add: add_assoc)
done
-lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
+lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite"
by (rule approx_sym [THEN [2] approx_HFinite], auto)
+lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
+by (rule approx_star_of_HFinite)
+
lemma approx_mult_HFinite:
- "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
+ fixes a b c d :: "'a::real_normed_algebra star"
+ shows "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
apply (rule approx_trans)
apply (rule_tac [2] approx_mult2)
apply (rule approx_mult1)
prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
done
+lemma approx_mult_star_of:
+ fixes a c :: "'a::real_normed_algebra star"
+ shows "[|a @= star_of b; c @= star_of d |]
+ ==> a*c @= star_of b*star_of d"
+by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
+
lemma approx_mult_hypreal_of_real:
"[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
==> a*c @= hypreal_of_real b*hypreal_of_real d"
-by (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite
- HFinite_hypreal_of_real)
+by (rule approx_mult_star_of)
lemma approx_SReal_mult_cancel_zero:
- "[| a \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
+ "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
done
-lemma approx_mult_SReal1: "[| a \<in> Reals; x @= 0 |] ==> x*a @= 0"
+lemma approx_mult_SReal1: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> x*a @= 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
-lemma approx_mult_SReal2: "[| a \<in> Reals; x @= 0 |] ==> a*x @= 0"
+lemma approx_mult_SReal2: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> a*x @= 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
lemma approx_mult_SReal_zero_cancel_iff [simp]:
- "[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
+ "[|(a::hypreal) \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
lemma approx_SReal_mult_cancel:
- "[| a \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
+ "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
done
lemma approx_SReal_mult_cancel_iff1 [simp]:
- "[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
+ "[| (a::hypreal) \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
intro: approx_SReal_mult_cancel)
-lemma approx_le_bound: "[| z \<le> f; f @= g; g \<le> z |] ==> f @= z"
+lemma approx_le_bound: "[| (z::hypreal) \<le> f; f @= g; g \<le> z |] ==> f @= z"
apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
apply (rule_tac x = "g+y-z" in bexI)
apply (simp (no_asm))
@@ -905,6 +930,10 @@
apply simp
done
+lemma star_of_HFinite_diff_Infinitesimal:
+ "x \<noteq> 0 ==> star_of x \<in> HFinite - Infinitesimal"
+by simp
+
lemma hypreal_of_real_Infinitesimal_iff_0:
"(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
by (rule star_of_Infinitesimal_iff_0)
@@ -920,7 +949,8 @@
apply simp
done
-lemma approx_SReal_not_zero: "[| y \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
+lemma approx_SReal_not_zero:
+ "[| (y::hypreal) \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
done
@@ -958,7 +988,16 @@
subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}
-lemma SReal_approx_iff: "[|x \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
+lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
+apply safe
+apply (simp add: approx_def)
+apply (simp only: star_of_minus [symmetric] star_of_add [symmetric])
+apply (simp only: star_of_Infinitesimal_iff_0)
+apply (simp only: diff_minus [symmetric] right_minus_eq)
+done
+
+lemma SReal_approx_iff:
+ "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
apply auto
apply (simp add: approx_def)
apply (drule_tac x = y in SReal_minus)
@@ -969,23 +1008,31 @@
done
lemma number_of_approx_iff [simp]:
- "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
-by (auto simp add: SReal_approx_iff)
+ "(number_of v @= (number_of w :: 'a::{number,real_normed_vector} star)) =
+ (number_of v = (number_of w :: 'a))"
+apply (unfold star_number_def)
+apply (rule star_of_approx_iff)
+done
(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
-lemma [simp]: "(0 @= number_of w) = ((number_of w :: hypreal) = 0)"
- "(number_of w @= 0) = ((number_of w :: hypreal) = 0)"
- "(1 @= number_of w) = ((number_of w :: hypreal) = 1)"
- "(number_of w @= 1) = ((number_of w :: hypreal) = 1)"
- "~ (0 @= 1)" "~ (1 @= 0)"
-by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1)
+lemma [simp]:
+ "(number_of w @= (0::'a::{number,real_normed_vector} star)) =
+ (number_of w = (0::'a))"
+ "((0::'a::{number,real_normed_vector} star) @= number_of w) =
+ (number_of w = (0::'a))"
+ "(number_of w @= (1::'b::{number,one,real_normed_vector} star)) =
+ (number_of w = (1::'b))"
+ "((1::'b::{number,one,real_normed_vector} star) @= number_of w) =
+ (number_of w = (1::'b))"
+ "~ (0 @= (1::'c::{axclass_0_neq_1,real_normed_vector} star))"
+ "~ (1 @= (0::'c::{axclass_0_neq_1,real_normed_vector} star))"
+apply (unfold star_number_def star_zero_def star_one_def)
+apply (unfold star_of_approx_iff)
+by (auto intro: sym)
-lemma hypreal_of_real_approx_iff [simp]:
+lemma hypreal_of_real_approx_iff:
"(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
-apply auto
-apply (rule inj_hypreal_of_real [THEN injD])
-apply (rule SReal_approx_iff [THEN iffD1], auto)
-done
+by (rule star_of_approx_iff)
lemma hypreal_of_real_approx_number_of_iff [simp]:
"(hypreal_of_real k @= number_of w) = (k = number_of w)"
@@ -998,7 +1045,7 @@
by (simp_all add: hypreal_of_real_approx_iff [symmetric])
lemma approx_unique_real:
- "[| r \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
+ "[| (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
@@ -1171,13 +1218,13 @@
done
lemma st_part_Ex:
- "x \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
+ "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
apply (simp add: approx_def Infinitesimal_def)
apply (drule lemma_st_part_Ex, auto)
done
text{*There is a unique real infinitely close*}
-lemma st_part_Ex1: "x \<in> HFinite ==> EX! t. t \<in> Reals & x @= t"
+lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> Reals & x @= t"
apply (drule st_part_Ex, safe)
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
apply (auto intro!: approx_unique_real)
@@ -1247,6 +1294,8 @@
done
lemma approx_inverse:
+ fixes x y :: "'a::{real_normed_div_algebra,division_by_zero} star"
+ shows
"[| x @= y; y \<in> HFinite - Infinitesimal |]
==> inverse x @= inverse y"
apply (frule HFinite_diff_Infinitesimal_approx, assumption)
@@ -1259,15 +1308,20 @@
done
(*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
+lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
lemmas hypreal_of_real_approx_inverse = hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
lemma inverse_add_Infinitesimal_approx:
+ fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
+ shows
"[| x \<in> HFinite - Infinitesimal;
h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x"
apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
done
lemma inverse_add_Infinitesimal_approx2:
+ fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
+ shows
"[| x \<in> HFinite - Infinitesimal;
h \<in> Infinitesimal |] ==> inverse(h + x) @= inverse x"
apply (rule add_commute [THEN subst])
@@ -1275,6 +1329,8 @@
done
lemma inverse_add_Infinitesimal_approx_Infinitesimal:
+ fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
+ shows
"[| x \<in> HFinite - Infinitesimal;
h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"
apply (rule approx_trans2)
@@ -1305,7 +1361,8 @@
by (auto simp add: HInfinite_HFinite_iff)
lemma approx_HFinite_mult_cancel:
- "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
+ fixes a w z :: "'a::{real_normed_div_algebra,division_by_zero} star"
+ shows "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
apply safe
apply (frule HFinite_inverse, assumption)
apply (drule not_Infinitesimal_not_zero)
@@ -1313,7 +1370,8 @@
done
lemma approx_HFinite_mult_cancel_iff1:
- "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
+ fixes a w z :: "'a::{real_normed_div_algebra,division_by_zero} star"
+ shows "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
lemma HInfinite_HFinite_add_cancel:
@@ -1376,13 +1434,13 @@
apply (simp (no_asm) add: HInfinite_HFinite_iff)
done
-lemma approx_hrabs_disj: "abs x @= x | abs x @= -x"
+lemma approx_hrabs_disj: "abs (x::hypreal) @= x | abs x @= -x"
by (cut_tac x = x in hrabs_disj, auto)
subsection{*Theorems about Monads*}
-lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x) Un monad(-x)"
+lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x::hypreal) Un monad(-x)"
by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x"
@@ -1398,7 +1456,7 @@
apply (simp (no_asm) add: Infinitesimal_monad_zero_iff [symmetric])
done
-lemma monad_zero_hrabs_iff: "(x \<in> monad 0) = (abs x \<in> monad 0)"
+lemma monad_zero_hrabs_iff: "((x::hypreal) \<in> monad 0) = (abs x \<in> monad 0)"
apply (rule_tac x1 = x in hrabs_disj [THEN disjE])
apply (auto simp add: monad_zero_minus_iff [symmetric])
done
@@ -1436,7 +1494,7 @@
done
lemma Infinitesimal_approx_hrabs:
- "[| x @= y; x \<in> Infinitesimal |] ==> abs x @= abs y"
+ "[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> abs x @= abs y"
apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
done
@@ -1449,28 +1507,28 @@
done
lemma Ball_mem_monad_gt_zero:
- "[| 0 < x; x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
+ "[| 0 < (x::hypreal); x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
apply (drule mem_monad_approx [THEN approx_sym])
apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])
apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)
done
lemma Ball_mem_monad_less_zero:
- "[| x < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
+ "[| (x::hypreal) < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
apply (drule mem_monad_approx [THEN approx_sym])
apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])
apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)
done
lemma lemma_approx_gt_zero:
- "[|0 < x; x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
+ "[|0 < (x::hypreal); x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)
lemma lemma_approx_less_zero:
- "[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
+ "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
-theorem approx_hrabs: "x @= y ==> abs x @= abs y"
+theorem approx_hrabs: "(x::hypreal) @= y ==> abs x @= abs y"
apply (case_tac "x \<in> Infinitesimal")
apply (simp add: Infinitesimal_approx_hrabs)
apply (rule linorder_cases [of 0 x])
@@ -1478,20 +1536,21 @@
apply (auto simp add: lemma_approx_less_zero [of x y] abs_of_neg)
done
-lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0"
+lemma approx_hrabs_zero_cancel: "abs(x::hypreal) @= 0 ==> x @= 0"
apply (cut_tac x = x in hrabs_disj)
apply (auto dest: approx_minus)
done
-lemma approx_hrabs_add_Infinitesimal: "e \<in> Infinitesimal ==> abs x @= abs(x+e)"
+lemma approx_hrabs_add_Infinitesimal:
+ "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x+e)"
by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
lemma approx_hrabs_add_minus_Infinitesimal:
- "e \<in> Infinitesimal ==> abs x @= abs(x + -e)"
+ "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x + -e)"
by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
lemma hrabs_add_Infinitesimal_cancel:
- "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+ "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
abs(x+e) = abs(y+e')|] ==> abs x @= abs y"
apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
@@ -1499,7 +1558,7 @@
done
lemma hrabs_add_minus_Infinitesimal_cancel:
- "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+ "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y"
apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
@@ -1857,55 +1916,45 @@
subsection{*Alternative Definitions for @{term HFinite} using Free Ultrafilter*}
-lemma FreeUltrafilterNat_Rep_hypreal:
- "[| X \<in> Rep_star x; Y \<in> Rep_star x |]
- ==> {n. X n = Y n} \<in> FreeUltrafilterNat"
-by (cases x, unfold star_n_def, auto, ultra)
-
lemma HFinite_FreeUltrafilterNat:
- "(x::hypreal) \<in> HFinite
- ==> \<exists>X \<in> Rep_star x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
-apply (cases x)
-apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x]
- star_of_def
- star_n_less SReal_iff star_n_minus)
-apply (rule_tac x=X in bexI)
-apply (rule_tac x=y in exI, ultra)
-apply simp
+ "star_n X \<in> HFinite
+ ==> \<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat"
+apply (auto simp add: HFinite_def SReal_def)
+apply (rule_tac x=r in exI)
+apply (simp add: hnorm_def star_of_def starfun_star_n)
+apply (simp add: star_less_def starP2_star_n)
done
lemma FreeUltrafilterNat_HFinite:
- "\<exists>X \<in> Rep_star x.
- \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
- ==> (x::hypreal) \<in> HFinite"
-apply (cases x)
-apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x])
-apply (rule_tac x = "hypreal_of_real u" in bexI)
-apply (auto simp add: star_n_less SReal_iff star_n_minus star_of_def)
-apply ultra+
+ "\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat
+ ==> star_n X \<in> HFinite"
+apply (auto simp add: HFinite_def mem_Rep_star_iff)
+apply (rule_tac x="star_of u" in bexI)
+apply (simp add: hnorm_def starfun_star_n star_of_def)
+apply (simp add: star_less_def starP2_star_n)
+apply (simp add: SReal_def)
done
lemma HFinite_FreeUltrafilterNat_iff:
- "((x::hypreal) \<in> HFinite) = (\<exists>X \<in> Rep_star x.
- \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
+ "(star_n X \<in> HFinite) = (\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat)"
by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
subsection{*Alternative Definitions for @{term HInfinite} using Free Ultrafilter*}
-lemma lemma_Compl_eq: "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) \<le> u}"
+lemma lemma_Compl_eq: "- {n. u < norm (xa n)} = {n. norm (xa n) \<le> u}"
by auto
-lemma lemma_Compl_eq2: "- {n. abs (xa n) < (u::real)} = {n. u \<le> abs (xa n)}"
+lemma lemma_Compl_eq2: "- {n. norm (xa n) < u} = {n. u \<le> norm (xa n)}"
by auto
lemma lemma_Int_eq1:
- "{n. abs (xa n) \<le> (u::real)} Int {n. u \<le> abs (xa n)}
- = {n. abs(xa n) = u}"
+ "{n. norm (xa n) \<le> u} Int {n. u \<le> norm (xa n)}
+ = {n. norm(xa n) = u}"
by auto
lemma lemma_FreeUltrafilterNat_one:
- "{n. abs (xa n) = u} \<le> {n. abs (xa n) < u + (1::real)}"
+ "{n. norm (xa n) = u} \<le> {n. norm (xa n) < u + (1::real)}"
by auto
(*-------------------------------------
@@ -1913,87 +1962,63 @@
ultrafilter for Infinite numbers!
-------------------------------------*)
lemma FreeUltrafilterNat_const_Finite:
- "[| xa: Rep_star x;
- {n. abs (xa n) = u} \<in> FreeUltrafilterNat
- |] ==> (x::hypreal) \<in> HFinite"
+ "{n. norm (X n) = u} \<in> FreeUltrafilterNat ==> star_n X \<in> HFinite"
apply (rule FreeUltrafilterNat_HFinite)
-apply (rule_tac x = xa in bexI)
apply (rule_tac x = "u + 1" in exI)
-apply (ultra, assumption)
+apply (erule ultra, simp)
done
lemma HInfinite_FreeUltrafilterNat:
- "(x::hypreal) \<in> HInfinite ==> \<exists>X \<in> Rep_star x.
- \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat"
-apply (frule HInfinite_HFinite_iff [THEN iffD1])
-apply (cut_tac x = x in Rep_hypreal_nonempty)
-apply (auto simp del: Rep_hypreal_nonempty simp add: HFinite_FreeUltrafilterNat_iff Bex_def)
-apply (drule spec)+
-apply auto
-apply (drule_tac x = u in spec)
-apply (drule FreeUltrafilterNat_Compl_mem)+
-apply (drule FreeUltrafilterNat_Int, assumption)
-apply (simp add: lemma_Compl_eq lemma_Compl_eq2 lemma_Int_eq1)
-apply (auto dest: FreeUltrafilterNat_const_Finite simp
- add: HInfinite_HFinite_iff [THEN iffD1])
+ "star_n X \<in> HInfinite ==> \<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat"
+apply (drule HInfinite_HFinite_iff [THEN iffD1])
+apply (simp add: HFinite_FreeUltrafilterNat_iff)
+apply (rule allI, drule_tac x="u + 1" in spec)
+apply (drule FreeUltrafilterNat_Compl_mem)
+apply (simp add: Collect_neg_eq [symmetric] linorder_not_less)
+apply (erule ultra, simp)
done
lemma lemma_Int_HI:
- "{n. abs (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. abs (X n) < (u::real)}"
+ "{n. norm (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. norm (X n) < (u::real)}"
by auto
-lemma lemma_Int_HIa: "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}"
+lemma lemma_Int_HIa: "{n. u < norm (X n)} Int {n. norm (X n) < u} = {}"
by (auto intro: order_less_asym)
lemma FreeUltrafilterNat_HInfinite:
- "\<exists>X \<in> Rep_star x. \<forall>u.
- {n. u < abs (X n)} \<in> FreeUltrafilterNat
- ==> (x::hypreal) \<in> HInfinite"
+ "\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat ==> star_n X \<in> HInfinite"
apply (rule HInfinite_HFinite_iff [THEN iffD2])
-apply (safe, drule HFinite_FreeUltrafilterNat, auto)
+apply (safe, drule HFinite_FreeUltrafilterNat, safe)
apply (drule_tac x = u in spec)
-apply (drule FreeUltrafilterNat_Rep_hypreal, assumption)
-apply (drule_tac Y = "{n. X n = Xa n}" in FreeUltrafilterNat_Int, simp)
-apply (drule lemma_Int_HI [THEN [2] FreeUltrafilterNat_subset])
-apply (drule_tac Y = "{n. abs (X n) < u}" in FreeUltrafilterNat_Int)
-apply (auto simp add: lemma_Int_HIa)
+apply ultra
done
lemma HInfinite_FreeUltrafilterNat_iff:
- "((x::hypreal) \<in> HInfinite) = (\<exists>X \<in> Rep_star x.
- \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat)"
+ "(star_n X \<in> HInfinite) = (\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat)"
by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
subsection{*Alternative Definitions for @{term Infinitesimal} using Free Ultrafilter*}
+lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) = (\<forall>x::real. P (star_of x))"
+by (unfold SReal_def, auto)
+
lemma Infinitesimal_FreeUltrafilterNat:
- "(x::hypreal) \<in> Infinitesimal ==> \<exists>X \<in> Rep_star x.
- \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat"
-apply (simp add: Infinitesimal_def)
-apply (auto simp add: abs_less_iff minus_less_iff [of x])
-apply (cases x)
-apply (auto, rule bexI [OF _ Rep_star_star_n], safe)
-apply (drule star_of_less [THEN iffD2])
-apply (drule_tac x = "hypreal_of_real u" in bspec, auto)
-apply (auto simp add: star_n_less star_n_minus star_of_def, ultra)
+ "star_n X \<in> Infinitesimal ==> \<forall>u>0. {n. norm (X n) < u} \<in> \<U>"
+apply (simp add: Infinitesimal_def ball_SReal_eq)
+apply (simp add: hnorm_def starfun_star_n star_of_def)
+apply (simp add: star_less_def starP2_star_n)
done
lemma FreeUltrafilterNat_Infinitesimal:
- "\<exists>X \<in> Rep_star x.
- \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
- ==> (x::hypreal) \<in> Infinitesimal"
-apply (simp add: Infinitesimal_def)
-apply (cases x)
-apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x])
-apply (auto simp add: SReal_iff)
-apply (drule_tac [!] x=y in spec)
-apply (auto simp add: star_n_less star_n_minus star_of_def, ultra+)
+ "\<forall>u>0. {n. norm (X n) < u} \<in> \<U> ==> star_n X \<in> Infinitesimal"
+apply (simp add: Infinitesimal_def ball_SReal_eq)
+apply (simp add: hnorm_def starfun_star_n star_of_def)
+apply (simp add: star_less_def starP2_star_n)
done
lemma Infinitesimal_FreeUltrafilterNat_iff:
- "((x::hypreal) \<in> Infinitesimal) = (\<exists>X \<in> Rep_star x.
- \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
+ "(star_n X \<in> Infinitesimal) = (\<forall>u>0. {n. norm (X n) < u} \<in> \<U>)"
by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
(*------------------------------------------------------------------------
@@ -2028,7 +2053,7 @@
lemma Infinitesimal_hypreal_of_nat_iff:
- "Infinitesimal = {x. \<forall>n. abs x < inverse (hypreal_of_nat (Suc n))}"
+ "Infinitesimal = {x. \<forall>n. hnorm x < inverse (hypreal_of_nat (Suc n))}"
apply (simp add: Infinitesimal_def)
apply (auto simp add: lemma_Infinitesimal2)
done
@@ -2098,11 +2123,9 @@
done
theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
-apply (simp add: omega_def star_n_def)
-apply (auto intro!: FreeUltrafilterNat_HInfinite)
-apply (rule bexI)
-apply (rule_tac [2] lemma_starrel_refl, auto)
-apply (simp (no_asm) add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
+apply (simp add: omega_def)
+apply (rule FreeUltrafilterNat_HInfinite)
+apply (simp (no_asm) add: real_norm_def real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
done
(*-----------------------------------------------
@@ -2202,27 +2225,30 @@
|X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
-----------------------------------------------------*)
lemma real_seq_to_hypreal_Infinitesimal:
- "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
- ==> star_n X + -hypreal_of_real x \<in> Infinitesimal"
+ "\<forall>n. norm(X n + -x) < inverse(real(Suc n))
+ ==> star_n X + -star_of x \<in> Infinitesimal"
apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: star_n_minus star_of_def star_n_add Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)
done
lemma real_seq_to_hypreal_approx:
- "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
- ==> star_n X @= hypreal_of_real x"
+ "\<forall>n. norm(X n + -x) < inverse(real(Suc n))
+ ==> star_n X @= star_of x"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
apply (erule real_seq_to_hypreal_Infinitesimal)
done
lemma real_seq_to_hypreal_approx2:
- "\<forall>n. abs(x + -X n) < inverse(real(Suc n))
- ==> star_n X @= hypreal_of_real x"
-apply (simp add: abs_minus_add_cancel real_seq_to_hypreal_approx)
+ "\<forall>n. norm(x + -X n) < inverse(real(Suc n))
+ ==> star_n X @= star_of x"
+apply (rule real_seq_to_hypreal_approx)
+apply (subst norm_minus_cancel [symmetric])
+apply (simp del: norm_minus_cancel)
+apply (subst add_commute, assumption)
done
lemma real_seq_to_hypreal_Infinitesimal2:
- "\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
+ "\<forall>n. norm(X n + -Y n) < inverse(real(Suc n))
==> star_n X + -star_n Y \<in> Infinitesimal"
by (auto intro!: bexI
dest: FreeUltrafilterNat_inverse_real_of_posnat
--- a/src/HOL/Hyperreal/SEQ.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Sat Sep 16 02:40:00 2006 +0200
@@ -14,13 +14,15 @@
definition
- LIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----> (_))" [60, 60] 60)
+ LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
+ ("((_)/ ----> (_))" [60, 60] 60)
--{*Standard definition of convergence of sequence*}
- "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
+ "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n + -L) < r))"
- NSLIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----NS> (_))" [60, 60] 60)
+ NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
+ ("((_)/ ----NS> (_))" [60, 60] 60)
--{*Nonstandard definition of convergence of sequence*}
- "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
+ "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
lim :: "(nat => real) => real"
--{*Standard definition of limit using choice operator*}
@@ -30,19 +32,19 @@
--{*Nonstandard definition of limit using choice operator*}
"nslim X = (SOME L. (X ----NS> L))"
- convergent :: "(nat => real) => bool"
+ convergent :: "(nat => 'a::real_normed_vector) => bool"
--{*Standard definition of convergence*}
"convergent X = (\<exists>L. (X ----> L))"
- NSconvergent :: "(nat => real) => bool"
+ NSconvergent :: "(nat => 'a::real_normed_vector) => bool"
--{*Nonstandard definition of convergence*}
"NSconvergent X = (\<exists>L. (X ----NS> L))"
- Bseq :: "(nat => real) => bool"
+ Bseq :: "(nat => 'a::real_normed_vector) => bool"
--{*Standard definition for bounded sequence*}
- "Bseq X = (\<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K)"
+ "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
- NSBseq :: "(nat=>real) => bool"
+ NSBseq :: "(nat => 'a::real_normed_vector) => bool"
--{*Nonstandard definition for bounded sequence*}
"NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
@@ -54,15 +56,16 @@
--{*Definition of subsequence*}
"subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
- Cauchy :: "(nat => real) => bool"
+ Cauchy :: "(nat => 'a::real_normed_vector) => bool"
--{*Standard definition of the Cauchy condition*}
- "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e)"
+ "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm((X m) + -(X n)) < e)"
- NSCauchy :: "(nat => real) => bool"
+ NSCauchy :: "(nat => 'a::real_normed_vector) => bool"
--{*Nonstandard definition*}
"NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+declare real_norm_def [simp]
text{* Example of an hypersequence (i.e. an extended standard sequence)
whose term with an hypernatural suffix is an infinitesimal i.e.
@@ -70,9 +73,8 @@
lemma SEQ_Infinitesimal:
"( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
-apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun)
-apply (simp add: star_n_inverse)
-apply (rule bexI [OF _ Rep_star_star_n])
+apply (simp add: hypnat_omega_def starfun star_n_inverse)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
done
@@ -80,28 +82,26 @@
subsection{*LIMSEQ and NSLIMSEQ*}
lemma LIMSEQ_iff:
- "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. \<bar>X n + -L\<bar> < r)"
+ "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n + -L) < r)"
by (simp add: LIMSEQ_def)
lemma NSLIMSEQ_iff:
- "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
+ "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
by (simp add: NSLIMSEQ_def)
text{*LIMSEQ ==> NSLIMSEQ*}
-
lemma LIMSEQ_NSLIMSEQ:
"X ----> L ==> X ----NS> L"
-apply (simp add: LIMSEQ_def NSLIMSEQ_def)
-apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
+apply (simp add: LIMSEQ_def NSLIMSEQ_def, safe)
apply (rule_tac x = N in star_cases)
+apply (simp add: HNatInfinite_FreeUltrafilterNat_iff)
apply (rule approx_minus_iff [THEN iffD2])
apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def
star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
apply (drule_tac x = u in spec, safe)
-apply (drule_tac x = no in spec, fuf)
-apply (blast dest: less_imp_le)
+apply (drule_tac x = no in spec)
+apply (erule ultra, simp add: less_imp_le)
done
@@ -148,29 +148,24 @@
lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n
==> star_n f : HNatInfinite"
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
apply (erule FreeUltrafilterNat_NSLIMSEQ)
done
lemma lemmaLIM:
- "{n. X (f n) + - L = Y n} Int {n. \<bar>Y n\<bar> < r} \<le>
- {n. \<bar>X (f n) + - L\<bar> < r}"
+ "{n. X (f n) + - L = Y n} Int {n. norm (Y n) < r} \<le>
+ {n. norm (X (f n) + - L) < r}"
by auto
lemma lemmaLIM2:
- "{n. \<bar>X (f n) + - L\<bar> < r} Int {n. r \<le> abs (X (f n) + - (L::real))} = {}"
+ "{n. norm (X (f n) + - L) < r} Int {n. r \<le> norm (X (f n) + - L)} = {}"
by auto
-lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
+lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> norm (X (f n) + - L);
( *f* X) (star_n f) +
- - hypreal_of_real L \<approx> 0 |] ==> False"
+ - star_of L \<approx> 0 |] ==> False"
apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rename_tac "Y")
apply (drule_tac x = r in spec, safe)
-apply (drule FreeUltrafilterNat_Int, assumption)
-apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset])
apply (drule FreeUltrafilterNat_all)
-apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl)
apply (drule FreeUltrafilterNat_Int, assumption)
apply (simp add: lemmaLIM2)
done
@@ -179,7 +174,7 @@
apply (simp add: LIMSEQ_def NSLIMSEQ_def)
apply (rule ccontr, simp, safe)
txt{* skolemization step *}
-apply (drule choice, safe)
+apply (drule no_choice, safe)
apply (drule_tac x = "star_n f" in bspec)
apply (drule_tac [2] approx_minus_iff [THEN iffD1])
apply (simp_all add: linorder_not_less)
@@ -217,11 +212,14 @@
by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_add_const)
lemma NSLIMSEQ_mult:
- "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
+ fixes a b :: "'a::real_normed_algebra"
+ shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
by (auto intro!: approx_mult_HFinite
simp add: NSLIMSEQ_def starfun_mult [symmetric])
-lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
+lemma LIMSEQ_mult:
+ fixes a b :: "'a::real_normed_algebra"
+ shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
@@ -266,22 +264,26 @@
text{*Proof is like that of @{text NSLIM_inverse}.*}
lemma NSLIMSEQ_inverse:
- "[| X ----NS> a; a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
-by (simp add: NSLIMSEQ_def starfun_inverse [symmetric]
- hypreal_of_real_approx_inverse)
+ fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
+ shows "[| X ----NS> a; a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
+by (simp add: NSLIMSEQ_def star_of_approx_inverse)
text{*Standard version of theorem*}
lemma LIMSEQ_inverse:
- "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
+ fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
+ shows "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
lemma NSLIMSEQ_mult_inverse:
+ fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
+ shows
"[| X ----NS> a; Y ----NS> b; b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
lemma LIMSEQ_divide:
- "[| X ----> a; Y ----> b; b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
+ fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
+ shows "[| X ----> a; Y ----> b; b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
text{*Uniqueness of limit*}
@@ -316,6 +318,7 @@
qed
lemma LIMSEQ_setprod:
+ fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
proof (cases "finite S")
@@ -455,15 +458,15 @@
subsection{*Bounded Sequence*}
-lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)"
+lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
by (simp add: Bseq_def)
-lemma BseqI: "[| 0 < K; \<forall>n. \<bar>X n\<bar> \<le> K |] ==> Bseq X"
+lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
by (auto simp add: Bseq_def)
lemma lemma_NBseq_def:
- "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) =
- (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
+ "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
+ (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
apply auto
prefer 2 apply force
apply (cut_tac x = K in reals_Archimedean2, clarify)
@@ -473,13 +476,13 @@
done
text{* alternative definition for Bseq *}
-lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
+lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
apply (simp add: Bseq_def)
apply (simp (no_asm) add: lemma_NBseq_def)
done
lemma lemma_NBseq_def2:
- "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
+ "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
apply (subst lemma_NBseq_def, auto)
apply (rule_tac x = "Suc N" in exI)
apply (rule_tac [2] x = N in exI)
@@ -489,7 +492,7 @@
done
(* yet another definition for Bseq *)
-lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
+lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
by (simp add: Bseq_def lemma_NBseq_def2)
lemma NSBseqD: "[| NSBseq X; N: HNatInfinite |] ==> ( *f* X) N : HFinite"
@@ -500,7 +503,7 @@
text{*The standard definition implies the nonstandard definition*}
-lemma lemma_Bseq: "\<forall>n. \<bar>X n\<bar> \<le> K ==> \<forall>n. abs(X((f::nat=>nat) n)) \<le> K"
+lemma lemma_Bseq: "\<forall>n. norm (X n) \<le> K ==> \<forall>n. norm(X((f::nat=>nat) n)) \<le> K"
by auto
lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
@@ -508,7 +511,6 @@
apply (rule_tac x = N in star_cases)
apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff
HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n])
apply (drule_tac f = Xa in lemma_Bseq)
apply (rule_tac x = "K+1" in exI)
apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
@@ -525,23 +527,22 @@
which woulid be useless.*}
lemma lemmaNSBseq:
- "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
- ==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>"
+ "\<forall>K > 0. \<exists>n. K < norm (X n)
+ ==> \<forall>N. \<exists>n. real(Suc N) < norm (X n)"
apply safe
apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
done
-lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
- ==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>"
+lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n::nat. K < norm (X n)
+ ==> \<exists>f. \<forall>N. real(Suc N) < norm (X (f N))"
apply (drule lemmaNSBseq)
-apply (drule choice, blast)
+apply (drule no_choice, blast)
done
lemma real_seq_to_hypreal_HInfinite:
- "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
+ "\<forall>N. real(Suc N) < norm (X (f N))
==> star_n (X o f) : HInfinite"
apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
-apply (rule bexI [OF _ Rep_star_star_n], clarify)
apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
apply (drule FreeUltrafilterNat_all)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
@@ -552,29 +553,28 @@
defined using the skolem function @{term "f::nat=>nat"} above*}
lemma lemma_finite_NSBseq:
- "{n. f n \<le> Suc u & real(Suc n) < \<bar>X (f n)\<bar>} \<le>
- {n. f n \<le> u & real(Suc n) < \<bar>X (f n)\<bar>} Un
- {n. real(Suc n) < \<bar>X (Suc u)\<bar>}"
+ "{n. f n \<le> Suc u & real(Suc n) < norm (X (f n))} \<le>
+ {n. f n \<le> u & real(Suc n) < norm (X (f n))} Un
+ {n. real(Suc n) < norm (X (Suc u))}"
by (auto dest!: le_imp_less_or_eq)
lemma lemma_finite_NSBseq2:
- "finite {n. f n \<le> (u::nat) & real(Suc n) < \<bar>X(f n)\<bar>}"
+ "finite {n. f n \<le> (u::nat) & real(Suc n) < norm (X(f n))}"
apply (induct "u")
apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
-apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset)
+apply (rule_tac B = "{n. real (Suc n) < norm (X 0) }" in finite_subset)
apply (auto intro: finite_real_of_nat_less_real
simp add: real_of_nat_Suc less_diff_eq [symmetric])
done
lemma HNatInfinite_skolem_f:
- "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
+ "\<forall>N. real(Suc N) < norm (X (f N))
==> star_n f : HNatInfinite"
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE])
-apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} =
- {n. f n \<le> u} \<inter> {N. real (Suc N) < \<bar>X (f N)\<bar>}")
+apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < norm (X (f n))} =
+ {n. f n \<le> u} \<inter> {N. real (Suc N) < norm (X (f N))}")
apply (erule ssubst)
apply (auto simp add: linorder_not_less Compl_def)
done
@@ -600,7 +600,7 @@
lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
-apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite)
+apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
done
text{*Standard Version: easily now proved using equivalence of NS and
@@ -624,10 +624,10 @@
\<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
by (blast intro: reals_complete Bseq_isUb)
-lemma NSBseq_isUb: "NSBseq X ==> \<exists>U. isUb UNIV {x. \<exists>n. X n = x} U"
+lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
-lemma NSBseq_isLub: "NSBseq X ==> \<exists>U. isLub UNIV {x. \<exists>n. X n = x} U"
+lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
@@ -686,7 +686,7 @@
text{*A standard proof of the theorem for monotone increasing sequence*}
lemma Bseq_mono_convergent:
- "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent X"
+ "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
apply (simp add: convergent_def)
apply (frule Bseq_isLub, safe)
apply (case_tac "\<exists>m. X m = U", auto)
@@ -705,7 +705,7 @@
text{*Nonstandard version of the theorem*}
lemma NSBseq_mono_NSconvergent:
- "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent X"
+ "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)"
by (auto intro: Bseq_mono_convergent
simp add: convergent_NSconvergent_iff [symmetric]
Bseq_NSBseq_iff [symmetric])
@@ -731,26 +731,31 @@
subsection{*A Few More Equivalence Theorems for Boundedness*}
text{*alternative formulation for boundedness*}
-lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. \<bar>X(n) + -x\<bar> \<le> k)"
+lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
apply (unfold Bseq_def, safe)
-apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI)
+apply (rule_tac [2] x = "k + norm x" in exI)
apply (rule_tac x = K in exI, simp)
apply (rule exI [where x = 0], auto)
-apply (drule_tac x=n in spec, arith)+
+apply (erule order_less_le_trans, simp)
+apply (drule_tac x=n in spec, fold diff_def)
+apply (drule order_trans [OF norm_triangle_ineq2])
+apply simp
done
text{*alternative formulation for boundedness*}
-lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. abs(X(n) + -X(N)) \<le> k)"
+lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
apply safe
apply (simp add: Bseq_def, safe)
-apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
+apply (rule_tac x = "K + norm (X N)" in exI)
apply auto
+apply (erule order_less_le_trans, simp)
apply (rule_tac x = N in exI, safe)
-apply (drule_tac x = n in spec, arith)
+apply (drule_tac x = n in spec)
+apply (rule order_trans [OF norm_triangle_ineq], simp)
apply (auto simp add: Bseq_iff2)
done
-lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
+lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
apply (simp add: Bseq_def)
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
apply (drule_tac x = n in spec, arith)
@@ -769,9 +774,9 @@
done
lemma lemmaCauchy2:
- "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> \<bar>X m + - X n\<bar> < u} Int
+ "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> norm (X m + - X n) < u} Int
{n. M \<le> xa n} Int {n. M \<le> x n} \<le>
- {n. abs (X (xa n) + - X (x n)) < u}"
+ {n. norm (X (xa n) + - X (x n)) < u}"
by blast
lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
@@ -781,7 +786,6 @@
apply (rule approx_minus_iff [THEN iffD2])
apply (rule mem_infmal_iff [THEN iffD1])
apply (auto simp add: starfun star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI, auto)
apply (drule spec, auto)
apply (drule_tac M = M in lemmaCauchy1)
apply (drule_tac M = M in lemmaCauchy1)
@@ -795,23 +799,14 @@
lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
apply (auto simp add: Cauchy_def NSCauchy_def)
apply (rule ccontr, simp)
-apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)
+apply (auto dest!: no_choice HNatInfinite_NSLIMSEQ
+ simp add: all_conj_distrib)
apply (drule bspec, assumption)
apply (drule_tac x = "star_n fa" in bspec);
apply (auto simp add: starfun)
apply (drule approx_minus_iff [THEN iffD1])
apply (drule mem_infmal_iff [THEN iffD2])
apply (auto simp add: star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rename_tac "Y")
-apply (drule_tac x = e in spec, auto)
-apply (drule FreeUltrafilterNat_Int, assumption)
-apply (subgoal_tac "{n. \<bar>X (f n) + - X (fa n)\<bar> < e} \<in> \<U>")
- prefer 2 apply (erule FreeUltrafilterNat_subset, force)
-apply (rule FreeUltrafilterNat_empty [THEN notE])
-apply (subgoal_tac
- "{n. abs (X (f n) + - X (fa n)) < e} Int
- {M. ~ abs (X (f M) + - X (fa M)) < e} = {}")
-apply auto
done
@@ -821,9 +816,13 @@
text{*A Cauchy sequence is bounded -- this is the standard
proof mechanization rather than the nonstandard proof*}
-lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
- ==> \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
-by auto
+lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M + - X n) < (1::real)
+ ==> \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
+apply (clarify, drule spec, drule (1) mp)
+apply (fold diff_def, simp only: norm_minus_commute)
+apply (drule order_le_less_trans [OF norm_triangle_ineq2])
+apply simp
+done
lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
by auto
@@ -842,7 +841,7 @@
done
lemma SUP_rabs_subseq:
- "\<exists>m \<le> M. \<forall>n \<le> M. \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>"
+ "\<exists>m::nat \<le> M. \<forall>n \<le> M. norm (X n) \<le> norm (X m)"
by (rule SUP_subseq)
lemma lemma_Nat_covered:
@@ -853,47 +852,52 @@
lemma lemma_trans1:
- "[| \<forall>n \<le> M. \<bar>(X::nat=>real) n\<bar> \<le> a; a < b |]
- ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
+ "[| \<forall>n \<le> M. norm ((X::nat=>'a::real_normed_vector) n) \<le> a; a < b |]
+ ==> \<forall>n \<le> M. norm (X n) \<le> b"
by (blast intro: order_le_less_trans [THEN order_less_imp_le])
lemma lemma_trans2:
- "[| \<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a; a < b |]
- ==> \<forall>n \<ge> M. \<bar>X n\<bar>\<le> b"
+ "[| \<forall>n \<ge> M. norm ((X::nat=>'a::real_normed_vector) n) < a; a < b |]
+ ==> \<forall>n \<ge> M. norm (X n) \<le> b"
by (blast intro: order_less_trans [THEN order_less_imp_le])
lemma lemma_trans3:
- "[| \<forall>n \<le> M. \<bar>X n\<bar> \<le> a; a = b |]
- ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
+ "[| \<forall>n \<le> M. norm (X n) \<le> a; a = b |]
+ ==> \<forall>n \<le> M. norm (X n) \<le> b"
by auto
-lemma lemma_trans4: "\<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a
- ==> \<forall>n \<ge> M. \<bar>X n\<bar> \<le> a"
+lemma lemma_trans4: "\<forall>n \<ge> M. norm ((X::nat=>'a::real_normed_vector) n) < a
+ ==> \<forall>n \<ge> M. norm (X n) \<le> a"
by (blast intro: order_less_imp_le)
text{*Proof is more involved than outlines sketched by various authors
would suggest*}
+lemma Bseq_Suc_imp_Bseq: "Bseq (\<lambda>n. X (Suc n)) \<Longrightarrow> Bseq X"
+apply (unfold Bseq_def, clarify)
+apply (rule_tac x="max K (norm (X 0))" in exI)
+apply (simp add: order_less_le_trans [OF _ le_maxI1])
+apply (clarify, case_tac "n", simp)
+apply (simp add: order_trans [OF _ le_maxI1])
+done
+
+lemma Bseq_shift_imp_Bseq: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
+apply (induct k, simp_all)
+apply (subgoal_tac "Bseq (\<lambda>n. X (n + k))", simp)
+apply (rule Bseq_Suc_imp_Bseq, simp)
+done
+
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
-apply (simp add: Cauchy_def Bseq_def)
-apply (drule_tac x = 1 in spec)
-apply (erule zero_less_one [THEN [2] impE], safe)
-apply (drule_tac x = M in spec, simp)
+apply (simp add: Cauchy_def)
+apply (drule spec, drule mp, rule zero_less_one, safe)
+apply (drule_tac x="M" in spec, simp)
apply (drule lemmaCauchy)
-apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe)
-apply (cut_tac x = "\<bar>X m\<bar> " and y = "1 + \<bar>X M\<bar> " in linorder_less_linear)
-apply safe
-apply (drule lemma_trans1, assumption)
-apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl)
-apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl)
-apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans])
-apply (drule lemma_trans4)
-apply (drule_tac [2] lemma_trans4)
-apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
-apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
-apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
-apply (auto elim!: lemma_Nat_covered)
+apply (rule_tac k="M" in Bseq_shift_imp_Bseq)
+apply (simp add: Bseq_def)
+apply (rule_tac x="1 + norm (X M)" in exI)
+apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp)
+apply (simp add: order_less_imp_le)
done
text{*A Cauchy sequence is bounded -- nonstandard version*}
@@ -912,7 +916,7 @@
instantiations for his 'espsilon-delta' proof(s) in this case
since the NS formulations do not involve existential quantifiers.*}
-lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
+lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent (X::nat=>real)"
apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
apply (frule NSCauchy_NSBseq)
apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
@@ -923,7 +927,7 @@
done
text{*Standard proof for free*}
-lemma Cauchy_convergent_iff: "Cauchy X = convergent X"
+lemma Cauchy_convergent_iff: "Cauchy X = convergent (X::nat=>real)"
by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
@@ -933,7 +937,7 @@
lemma NSLIMSEQ_le:
"[| f ----NS> l; g ----NS> m;
\<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
- |] ==> l \<le> m"
+ |] ==> l \<le> (m::real)"
apply (simp add: NSLIMSEQ_def, safe)
apply (drule starfun_le_mono)
apply (drule HNatInfinite_whn [THEN [2] bspec])+
@@ -946,23 +950,23 @@
(* standard version *)
lemma LIMSEQ_le:
"[| f ----> l; g ----> m; \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |]
- ==> l \<le> m"
+ ==> l \<le> (m::real)"
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
-lemma LIMSEQ_le_const: "[| X ----> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
+lemma LIMSEQ_le_const: "[| X ----> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
apply (rule LIMSEQ_le)
apply (rule LIMSEQ_const, auto)
done
-lemma NSLIMSEQ_le_const: "[| X ----NS> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
+lemma NSLIMSEQ_le_const: "[| X ----NS> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)
-lemma LIMSEQ_le_const2: "[| X ----> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
+lemma LIMSEQ_le_const2: "[| X ----> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
apply (rule LIMSEQ_le)
apply (rule_tac [2] LIMSEQ_const, auto)
done
-lemma NSLIMSEQ_le_const2: "[| X ----NS> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
+lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)
text{*Shift a convergent series by 1:
@@ -970,12 +974,10 @@
the successor of an infinite hypernatural is also infinite.*}
lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
-apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
-apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
-apply (drule bspec, assumption)
-apply (drule bspec, assumption)
-apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
-apply (blast intro: approx_trans3)
+apply (unfold NSLIMSEQ_def, safe)
+apply (drule_tac x="N + 1" in bspec)
+apply (erule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
+apply (simp add: starfun_shift_one)
done
text{* standard version *}
@@ -983,13 +985,10 @@
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
-apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
-apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
-apply (drule bspec, assumption)
-apply (drule bspec, assumption)
-apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
+apply (unfold NSLIMSEQ_def, safe)
apply (drule_tac x="N - 1" in bspec)
-apply (auto intro: approx_trans3)
+apply (erule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
+apply (simp add: starfun_shift_one)
done
lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
@@ -1004,30 +1003,30 @@
by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
text{*A sequence tends to zero iff its abs does*}
-lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> 0)"
+lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
by (simp add: LIMSEQ_def)
text{*We prove the NS version from the standard one, since the NS proof
seems more complicated than the standard one above!*}
-lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> 0)"
+lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> (0::real))"
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
text{*Generalization to other limits*}
-lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
+lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
apply (simp add: NSLIMSEQ_def)
apply (auto intro: approx_hrabs
simp add: starfun_abs hypreal_of_real_hrabs [symmetric])
done
text{* standard version *}
-lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
+lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)
text{*An unbounded sequence's inverse tends to 0*}
text{* standard proof seems easier *}
lemma LIMSEQ_inverse_zero:
- "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
+ "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
apply (simp add: LIMSEQ_def, safe)
apply (drule_tac x = "inverse r" in spec, safe)
apply (rule_tac x = N in exI, safe)
@@ -1042,7 +1041,7 @@
done
lemma NSLIMSEQ_inverse_zero:
- "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n)
+ "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
==> (%n. inverse(f n)) ----NS> 0"
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
@@ -1090,19 +1089,22 @@
text{* Real Powers*}
lemma NSLIMSEQ_pow [rule_format]:
- "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
+ fixes a :: "'a::{real_normed_algebra,recpower}"
+ shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
apply (induct "m")
-apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
+apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
done
-lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
+lemma LIMSEQ_pow:
+ fixes a :: "'a::{real_normed_algebra,recpower}"
+ shows "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and
also fact that bounded and monotonic sequence converges.*}
-lemma Bseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> Bseq (%n. x ^ n)"
+lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
apply (simp add: Bseq_def)
apply (rule_tac x = 1 in exI)
apply (simp add: power_abs)
@@ -1114,12 +1116,14 @@
apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
done
-lemma convergent_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> convergent (%n. x ^ n)"
+lemma convergent_realpow:
+ "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
text{* We now use NS criterion to bring proof of theorem through *}
-lemma NSLIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----NS> 0"
+lemma NSLIMSEQ_realpow_zero:
+ "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----NS> 0"
apply (simp add: NSLIMSEQ_def)
apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
apply (frule NSconvergentD)
@@ -1135,10 +1139,12 @@
done
text{* standard version *}
-lemma LIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----> 0"
+lemma LIMSEQ_realpow_zero:
+ "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----> 0"
by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
-lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0"
+lemma LIMSEQ_divide_realpow_zero:
+ "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0"
apply (cut_tac a = a and x1 = "inverse x" in
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
apply (auto simp add: divide_inverse power_inverse)
@@ -1147,18 +1153,18 @@
text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
-lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
+lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
-lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
+lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
-lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----> 0"
+lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0"
apply (rule LIMSEQ_rabs_zero [THEN iffD1])
apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
done
-lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----NS> 0"
+lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----NS> 0"
by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
subsection{*Hyperreals and Sequences*}
--- a/src/HOL/Hyperreal/Series.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy Sat Sep 16 02:40:00 2006 +0200
@@ -354,7 +354,7 @@
apply (drule spec, drule (1) mp)
apply (erule exE, rule_tac x="N" in exI, clarify)
apply (rule_tac x="m" and y="n" in linorder_le_cases)
-apply (subst abs_minus_commute)
+apply (subst norm_minus_commute)
apply (simp add: setsum_diff [symmetric])
apply (simp add: setsum_diff [symmetric])
done
--- a/src/HOL/Hyperreal/Star.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/Star.thy Sat Sep 16 02:40:00 2006 +0200
@@ -38,7 +38,7 @@
referee for the JCM Paper: let f(x) be least y such
that Q(x,y)
*)
-lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: nat => nat). \<forall>x. Q x (f x)"
+lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: 'a => nat). \<forall>x. Q x (f x)"
apply (rule_tac x = "%x. LEAST y. Q x y" in exI)
apply (blast intro: LeastI)
done
@@ -146,11 +146,6 @@
apply (simp add: Ifun_star_n star_n_eq_iff)
done
-lemma Rep_star_FreeUltrafilterNat:
- "[| X \<in> Rep_star z; Y \<in> Rep_star z |]
- ==> {n. X n = Y n} : FreeUltrafilterNat"
-by (rule FreeUltrafilterNat_Rep_hypreal)
-
text{*Nonstandard extension of functions*}
lemma starfun:
@@ -213,7 +208,7 @@
(* this is trivial, given starfun_Id *)
lemma starfun_Idfun_approx:
- "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real a"
+ "x @= star_of a ==> ( *f* (%x. x)) x @= star_of a"
by (simp only: starfun_Id)
text{*The Star-function is a (nonstandard) extension of the function*}
@@ -243,10 +238,10 @@
text{*extented function has same solution as its standard
version for real arguments. i.e they are the same
for all real arguments*}
-lemma starfun_eq [simp]: "( *f* f) (star_of a) = star_of (f a)"
-by (transfer, rule refl)
+lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
+by (rule starfun_star_of)
-lemma starfun_approx: "( *f* f) (star_of a) @= hypreal_of_real (f a)"
+lemma starfun_approx: "( *f* f) (star_of a) @= star_of (f a)"
by simp
(* useful for NS definition of derivatives *)
@@ -258,7 +253,9 @@
"( *f* (%h. f(g(x + h)))) x' = ( *f* (f o g)) (star_of x + x')"
by (unfold o_def, rule starfun_lambda_cancel)
-lemma starfun_mult_HFinite_approx: "[| ( *f* f) x @= l; ( *f* g) x @= m;
+lemma starfun_mult_HFinite_approx:
+ fixes l m :: "'a::real_normed_algebra star"
+ shows "[| ( *f* f) x @= l; ( *f* g) x @= m;
l: HFinite; m: HFinite
|] ==> ( *f* (%x. f x * g x)) x @= l * m"
apply (drule (3) approx_mult_HFinite)
@@ -277,10 +274,10 @@
(* use the theorem we proved above instead *)
lemma starfun_rabs_hrabs: "*f* abs = abs"
-by (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
+by (simp only: star_abs_def)
lemma starfun_inverse_inverse [simp]: "( *f* inverse) x = inverse(x)"
-by (unfold star_inverse_def, rule refl)
+by (simp only: star_inverse_def)
lemma starfun_inverse: "!!x. inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
by (transfer, rule refl)
@@ -312,36 +309,40 @@
by its NS extenson. See second NS set extension below.*}
lemma STAR_rabs_add_minus:
"*s* {x. abs (x + - y) < r} =
- {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
+ {x. abs(x + -star_of y) < star_of r}"
by (transfer, rule refl)
lemma STAR_starfun_rabs_add_minus:
"*s* {x. abs (f x + - y) < r} =
- {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
+ {x. abs(( *f* f) x + -star_of y) < star_of r}"
by (transfer, rule refl)
text{*Another characterization of Infinitesimal and one of @= relation.
In this theory since @{text hypreal_hrabs} proved here. Maybe
move both theorems??*}
lemma Infinitesimal_FreeUltrafilterNat_iff2:
- "(x \<in> Infinitesimal) =
- (\<exists>X \<in> Rep_star(x).
- \<forall>m. {n. abs(X n) < inverse(real(Suc m))}
+ "(star_n X \<in> Infinitesimal) =
+ (\<forall>m. {n. norm(X n) < inverse(real(Suc m))}
\<in> FreeUltrafilterNat)"
-apply (cases x)
-apply (auto intro!: bexI lemma_starrel_refl
- simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
- star_n_inverse star_n_abs star_n_less hypreal_of_nat_eq)
-apply (drule_tac x = n in spec, ultra)
+by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
+ hnorm_def star_of_nat_def starfun_star_n
+ star_n_inverse star_n_less hypreal_of_nat_eq)
+
+lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
+ (\<forall>r>0. {n. norm (X n + - Y n) < r} : FreeUltrafilterNat)"
+apply (subst approx_minus_iff)
+apply (rule mem_infmal_iff [THEN subst])
+apply (simp add: star_n_minus star_n_add)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
done
-lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
- (\<forall>m. {n. abs (X n + - Y n) <
+lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
+ (\<forall>m. {n. norm (X n + - Y n) <
inverse(real(Suc m))} : FreeUltrafilterNat)"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
-apply (auto simp add: star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff2)
-apply (drule_tac x = m in spec, ultra)
+apply (simp add: star_n_minus star_n_add)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2)
done
lemma inj_starfun: "inj starfun"
--- a/src/HOL/Hyperreal/Transcendental.thy Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Sat Sep 16 02:40:00 2006 +0200
@@ -2540,7 +2540,8 @@
done
lemma isCont_inv_fun_inv:
- "[| 0 < d;
+ fixes f g :: "real \<Rightarrow> real"
+ shows "[| 0 < d;
\<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;
\<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]
==> \<exists>e. 0 < e &
@@ -2555,7 +2556,7 @@
text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
lemma LIM_fun_gt_zero:
- "[| f -- c --> l; 0 < l |]
+ "[| f -- c --> (l::real); 0 < l |]
==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
apply (auto simp add: LIM_def)
apply (drule_tac x = "l/2" in spec, safe, force)
@@ -2564,7 +2565,7 @@
done
lemma LIM_fun_less_zero:
- "[| f -- c --> l; l < 0 |]
+ "[| f -- c --> (l::real); l < 0 |]
==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
apply (auto simp add: LIM_def)
apply (drule_tac x = "-l/2" in spec, safe, force)
@@ -2574,7 +2575,7 @@
lemma LIM_fun_not_zero:
- "[| f -- c --> l; l \<noteq> 0 |]
+ "[| f -- c --> (l::real); l \<noteq> 0 |]
==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
apply (drule LIM_fun_less_zero)