--- a/src/HOL/Nonstandard_Analysis/HLog.thy Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLog.thy Sun Dec 18 23:43:50 2016 +0100
@@ -3,154 +3,134 @@
Copyright: 2000, 2001 University of Edinburgh
*)
-section\<open>Logarithms: Non-Standard Version\<close>
+section \<open>Logarithms: Non-Standard Version\<close>
theory HLog
-imports HTranscendental
+ imports HTranscendental
begin
(* should be in NSA.ML *)
lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
-by (simp add: epsilon_def star_n_zero_num star_n_le)
+ by (simp add: epsilon_def star_n_zero_num star_n_le)
-lemma hpfinite_witness: "\<epsilon> : {x. 0 \<le> x & x : HFinite}"
-by auto
+lemma hpfinite_witness: "\<epsilon> \<in> {x. 0 \<le> x \<and> x \<in> HFinite}"
+ by auto
-definition
- powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
- [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
-
-definition
- hlog :: "[hypreal,hypreal] => hypreal" where
- [transfer_unfold]: "hlog a x = starfun2 log a x"
+definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal" (infixr "powhr" 80)
+ where [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
+
+definition hlog :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"
+ where [transfer_unfold]: "hlog a x = starfun2 log a x"
+
+lemma powhr: "(star_n X) powhr (star_n Y) = star_n (\<lambda>n. (X n) powr (Y n))"
+ by (simp add: powhr_def starfun2_star_n)
-lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
-by (simp add: powhr_def starfun2_star_n)
-
-lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
-by (transfer, simp)
+lemma powhr_one_eq_one [simp]: "\<And>a. 1 powhr a = 1"
+ by transfer simp
-lemma powhr_mult:
- "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
-by (transfer, simp add: powr_mult)
+lemma powhr_mult: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powhr a = (x powhr a) * (y powhr a)"
+ by transfer (simp add: powr_mult)
-lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
-by (transfer, simp)
+lemma powhr_gt_zero [simp]: "\<And>a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
+ by transfer simp
lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
-by transfer simp
-
-lemma powhr_divide:
- "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
-by (transfer, rule powr_divide)
+ by transfer simp
-lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
-by (transfer, rule powr_add)
+lemma powhr_divide: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
+ by transfer (rule powr_divide)
-lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
-by (transfer, rule powr_powr)
+lemma powhr_add: "\<And>a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
+ by transfer (rule powr_add)
-lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
-by (transfer, rule powr_powr_swap)
+lemma powhr_powhr: "\<And>a b x. (x powhr a) powhr b = x powhr (a * b)"
+ by transfer (rule powr_powr)
-lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
-by (transfer, rule powr_minus)
+lemma powhr_powhr_swap: "\<And>a b x. (x powhr a) powhr b = (x powhr b) powhr a"
+ by transfer (rule powr_powr_swap)
-lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
-by (simp add: divide_inverse powhr_minus)
+lemma powhr_minus: "\<And>a x. x powhr (- a) = inverse (x powhr a)"
+ by transfer (rule powr_minus)
-lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
-by (transfer, simp)
+lemma powhr_minus_divide: "x powhr (- a) = 1 / (x powhr a)"
+ by (simp add: divide_inverse powhr_minus)
-lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
-by (transfer, simp)
+lemma powhr_less_mono: "\<And>a b x. a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powhr a < x powhr b"
+ by transfer simp
+
+lemma powhr_less_cancel: "\<And>a b x. x powhr a < x powhr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
+ by transfer simp
-lemma powhr_less_cancel_iff [simp]:
- "1 < x ==> (x powhr a < x powhr b) = (a < b)"
-by (blast intro: powhr_less_cancel powhr_less_mono)
+lemma powhr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a < x powhr b \<longleftrightarrow> a < b"
+ by (blast intro: powhr_less_cancel powhr_less_mono)
-lemma powhr_le_cancel_iff [simp]:
- "1 < x ==> (x powhr a \<le> x powhr b) = (a \<le> b)"
-by (simp add: linorder_not_less [symmetric])
+lemma powhr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a \<le> x powhr b \<longleftrightarrow> a \<le> b"
+ by (simp add: linorder_not_less [symmetric])
-lemma hlog:
- "hlog (star_n X) (star_n Y) =
- star_n (%n. log (X n) (Y n))"
-by (simp add: hlog_def starfun2_star_n)
+lemma hlog: "hlog (star_n X) (star_n Y) = star_n (\<lambda>n. log (X n) (Y n))"
+ by (simp add: hlog_def starfun2_star_n)
-lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
-by (transfer, rule log_ln)
+lemma hlog_starfun_ln: "\<And>x. ( *f* ln) x = hlog (( *f* exp) 1) x"
+ by transfer (rule log_ln)
-lemma powhr_hlog_cancel [simp]:
- "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
-by (transfer, simp)
+lemma powhr_hlog_cancel [simp]: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powhr (hlog a x) = x"
+ by transfer simp
-lemma hlog_powhr_cancel [simp]:
- "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
-by (transfer, simp)
+lemma hlog_powhr_cancel [simp]: "\<And>a y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a (a powhr y) = y"
+ by transfer simp
lemma hlog_mult:
- "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]
- ==> hlog a (x * y) = hlog a x + hlog a y"
-by (transfer, rule log_mult)
+ "\<And>a x y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x * y) = hlog a x + hlog a y"
+ by transfer (rule log_mult)
-lemma hlog_as_starfun:
- "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-by (transfer, simp add: log_def)
+lemma hlog_as_starfun: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
+ by transfer (simp add: log_def)
lemma hlog_eq_div_starfun_ln_mult_hlog:
- "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
- ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
-by (transfer, rule log_eq_div_ln_mult_log)
+ "\<And>a b x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
+ hlog a x = (( *f* ln) b / ( *f* ln) a) * hlog b x"
+ by transfer (rule log_eq_div_ln_mult_log)
-lemma powhr_as_starfun: "!!a x. x powhr a = (if x=0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
- by (transfer, simp add: powr_def)
+lemma powhr_as_starfun: "\<And>a x. x powhr a = (if x = 0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
+ by transfer (simp add: powr_def)
lemma HInfinite_powhr:
- "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;
- 0 < a |] ==> x powhr a : HInfinite"
-apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite
- simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
-done
+ "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> a \<in> HFinite - Infinitesimal \<Longrightarrow> 0 < a \<Longrightarrow> x powhr a \<in> HInfinite"
+ by (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite
+ HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite
+ simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
lemma hlog_hrabs_HInfinite_Infinitesimal:
- "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]
- ==> hlog a \<bar>x\<bar> : Infinitesimal"
-apply (frule HInfinite_gt_zero_gt_one)
-apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
- HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
- simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
- hlog_as_starfun divide_inverse)
-done
+ "x \<in> HFinite - Infinitesimal \<Longrightarrow> a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a \<bar>x\<bar> \<in> Infinitesimal"
+ apply (frule HInfinite_gt_zero_gt_one)
+ apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
+ HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
+ simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
+ hlog_as_starfun divide_inverse)
+ done
-lemma hlog_HInfinite_as_starfun:
- "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-by (rule hlog_as_starfun, auto)
+lemma hlog_HInfinite_as_starfun: "a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
+ by (rule hlog_as_starfun) auto
-lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
-by (transfer, simp)
+lemma hlog_one [simp]: "\<And>a. hlog a 1 = 0"
+ by transfer simp
-lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
-by (transfer, rule log_eq_one)
+lemma hlog_eq_one [simp]: "\<And>a. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a a = 1"
+ by transfer (rule log_eq_one)
-lemma hlog_inverse:
- "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
-apply (rule add_left_cancel [of "hlog a x", THEN iffD1])
-apply (simp add: hlog_mult [symmetric])
-done
+lemma hlog_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> hlog a (inverse x) = - hlog a x"
+ by (rule add_left_cancel [of "hlog a x", THEN iffD1]) (simp add: hlog_mult [symmetric])
-lemma hlog_divide:
- "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
-by (simp add: hlog_mult hlog_inverse divide_inverse)
+lemma hlog_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x / y) = hlog a x - hlog a y"
+ by (simp add: hlog_mult hlog_inverse divide_inverse)
lemma hlog_less_cancel_iff [simp]:
- "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
-by (transfer, simp)
+ "\<And>a x y. 1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a x < hlog a y \<longleftrightarrow> x < y"
+ by transfer simp
-lemma hlog_le_cancel_iff [simp]:
- "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
-by (simp add: linorder_not_less [symmetric])
+lemma hlog_le_cancel_iff [simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a x \<le> hlog a y \<longleftrightarrow> x \<le> y"
+ by (simp add: linorder_not_less [symmetric])
end
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy Sun Dec 18 23:43:50 2016 +0100
@@ -15,434 +15,431 @@
abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
begin
-definition
- NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
+definition NSLIMSEQ :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where
\<comment>\<open>Nonstandard definition of convergence of sequence\<close>
- "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
+ "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
-definition
- nslim :: "(nat => 'a::real_normed_vector) => 'a" where
- \<comment>\<open>Nonstandard definition of limit using choice operator\<close>
- "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
+definition nslim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a"
+ where "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
+ \<comment> \<open>Nonstandard definition of limit using choice operator\<close>
+
-definition
- NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where
- \<comment>\<open>Nonstandard definition of convergence\<close>
- "NSconvergent X = (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
+definition NSconvergent :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
+ where "NSconvergent X \<longleftrightarrow> (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
+ \<comment> \<open>Nonstandard definition of convergence\<close>
-definition
- NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
- \<comment>\<open>Nonstandard definition for bounded sequence\<close>
- "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+definition NSBseq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
+ where "NSBseq X \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite)"
+ \<comment> \<open>Nonstandard definition for bounded sequence\<close>
+
-definition
- NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
- \<comment>\<open>Nonstandard definition\<close>
- "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+definition NSCauchy :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
+ where "NSCauchy X \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+ \<comment> \<open>Nonstandard definition\<close>
+
subsection \<open>Limits of Sequences\<close>
-lemma NSLIMSEQ_iff:
- "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
-by (simp add: NSLIMSEQ_def)
+lemma NSLIMSEQ_iff: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
+ by (simp add: NSLIMSEQ_def)
+
+lemma NSLIMSEQ_I: "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+ by (simp add: NSLIMSEQ_def)
-lemma NSLIMSEQ_I:
- "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
-by (simp add: NSLIMSEQ_def)
+lemma NSLIMSEQ_D: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L"
+ by (simp add: NSLIMSEQ_def)
-lemma NSLIMSEQ_D:
- "\<lbrakk>X \<longlonglongrightarrow>\<^sub>N\<^sub>S L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L"
-by (simp add: NSLIMSEQ_def)
+lemma NSLIMSEQ_const: "(\<lambda>n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k"
+ by (simp add: NSLIMSEQ_def)
-lemma NSLIMSEQ_const: "(%n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k"
-by (simp add: NSLIMSEQ_def)
+lemma NSLIMSEQ_add: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n + Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
+ by (auto intro: approx_add simp add: NSLIMSEQ_def)
-lemma NSLIMSEQ_add:
- "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n + Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
-by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
+lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n + b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
+ by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
-lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n.(f n + b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
-by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
+lemma NSLIMSEQ_mult: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n * Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a * b"
+ for a b :: "'a::real_normed_algebra"
+ by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
-lemma NSLIMSEQ_mult:
- fixes a b :: "'a::real_normed_algebra"
- shows "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n * Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a * b"
-by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
+lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S - a"
+ by (auto simp add: NSLIMSEQ_def)
-lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a"
-by (auto simp add: NSLIMSEQ_def)
+lemma NSLIMSEQ_minus_cancel: "(\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a"
+ by (drule NSLIMSEQ_minus) simp
-lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a ==> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a"
-by (drule NSLIMSEQ_minus, simp)
-
-lemma NSLIMSEQ_diff:
- "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
+lemma NSLIMSEQ_diff: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def)
(* FIXME: delete *)
-lemma NSLIMSEQ_add_minus:
- "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n + -Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + -b"
+lemma NSLIMSEQ_add_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n + - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + - b"
by (simp add: NSLIMSEQ_diff)
-lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n.(f n - b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
-by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
+lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n - b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
+ by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
-lemma NSLIMSEQ_inverse:
- fixes a :: "'a::real_normed_div_algebra"
- shows "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; a ~= 0 |] ==> (%n. inverse(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S inverse(a)"
-by (simp add: NSLIMSEQ_def star_of_approx_inverse)
+lemma NSLIMSEQ_inverse: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S inverse a"
+ for a :: "'a::real_normed_div_algebra"
+ by (simp add: NSLIMSEQ_def star_of_approx_inverse)
-lemma NSLIMSEQ_mult_inverse:
- fixes a b :: "'a::real_normed_field"
- shows
- "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b; b ~= 0 |] ==> (%n. X n / Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a/b"
-by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
+lemma NSLIMSEQ_mult_inverse: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> (\<lambda>n. X n / Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a / b"
+ for a b :: "'a::real_normed_field"
+ by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
-by transfer simp
+ by transfer simp
lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a"
-by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
-
-text\<open>Uniqueness of limit\<close>
-lemma NSLIMSEQ_unique: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; X \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> a = b"
-apply (simp add: NSLIMSEQ_def)
-apply (drule HNatInfinite_whn [THEN [2] bspec])+
-apply (auto dest: approx_trans3)
-done
+ by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
-lemma NSLIMSEQ_pow [rule_format]:
- fixes a :: "'a::{real_normed_algebra,power}"
- shows "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S a) --> ((%n. (X n) ^ m) \<longlonglongrightarrow>\<^sub>N\<^sub>S a ^ m)"
-apply (induct "m")
-apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
-done
+text \<open>Uniqueness of limit.\<close>
+lemma NSLIMSEQ_unique: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> a = b"
+ apply (simp add: NSLIMSEQ_def)
+ apply (drule HNatInfinite_whn [THEN [2] bspec])+
+ apply (auto dest: approx_trans3)
+ done
-text\<open>We can now try and derive a few properties of sequences,
- starting with the limit comparison property for sequences.\<close>
+lemma NSLIMSEQ_pow [rule_format]: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S a) \<longrightarrow> ((\<lambda>n. (X n) ^ m) \<longlonglongrightarrow>\<^sub>N\<^sub>S a ^ m)"
+ for a :: "'a::{real_normed_algebra,power}"
+ by (induct m) (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
+
+text \<open>We can now try and derive a few properties of sequences,
+ starting with the limit comparison property for sequences.\<close>
-lemma NSLIMSEQ_le:
- "[| f \<longlonglongrightarrow>\<^sub>N\<^sub>S l; g \<longlonglongrightarrow>\<^sub>N\<^sub>S m;
- \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
- |] ==> l \<le> (m::real)"
-apply (simp add: NSLIMSEQ_def, safe)
-apply (drule starfun_le_mono)
-apply (drule HNatInfinite_whn [THEN [2] bspec])+
-apply (drule_tac x = whn in spec)
-apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
-apply clarify
-apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
-done
+lemma NSLIMSEQ_le: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> g \<longlonglongrightarrow>\<^sub>N\<^sub>S m \<Longrightarrow> \<exists>N. \<forall>n \<ge> N. f n \<le> g n \<Longrightarrow> l \<le> m"
+ for l m :: real
+ apply (simp add: NSLIMSEQ_def, safe)
+ apply (drule starfun_le_mono)
+ apply (drule HNatInfinite_whn [THEN [2] bspec])+
+ apply (drule_tac x = whn in spec)
+ apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
+ apply clarify
+ apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
+ done
-lemma NSLIMSEQ_le_const: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
-by (erule NSLIMSEQ_le [OF NSLIMSEQ_const], auto)
+lemma NSLIMSEQ_le_const: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. a \<le> X n \<Longrightarrow> a \<le> r"
+ for a r :: real
+ by (erule NSLIMSEQ_le [OF NSLIMSEQ_const]) auto
-lemma NSLIMSEQ_le_const2: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
-by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto)
+lemma NSLIMSEQ_le_const2: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. X n \<le> a \<Longrightarrow> r \<le> a"
+ for a r :: real
+ by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const]) auto
-text\<open>Shift a convergent series by 1:
+text \<open>Shift a convergent series by 1:
By the equivalence between Cauchiness and convergence and because
the successor of an infinite hypernatural is also infinite.\<close>
-lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> (%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
-apply (unfold NSLIMSEQ_def, safe)
-apply (drule_tac x="N + 1" in bspec)
-apply (erule HNatInfinite_add)
-apply (simp add: starfun_shift_one)
-done
+lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> (\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
+ apply (unfold NSLIMSEQ_def)
+ apply safe
+ apply (drule_tac x="N + 1" in bspec)
+ apply (erule HNatInfinite_add)
+ apply (simp add: starfun_shift_one)
+ done
-lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
-apply (unfold NSLIMSEQ_def, safe)
-apply (drule_tac x="N - 1" in bspec)
-apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
-apply (simp add: starfun_shift_one one_le_HNatInfinite)
-done
+lemma NSLIMSEQ_imp_Suc: "(\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
+ apply (unfold NSLIMSEQ_def)
+ apply safe
+ apply (drule_tac x="N - 1" in bspec)
+ apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
+ apply (simp add: starfun_shift_one one_le_HNatInfinite)
+ done
-lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S l)"
-by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
+lemma NSLIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
+ by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
+
subsubsection \<open>Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}\<close>
lemma LIMSEQ_NSLIMSEQ:
- assumes X: "X \<longlonglongrightarrow> L" shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+ assumes X: "X \<longlonglongrightarrow> L"
+ shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
proof (rule NSLIMSEQ_I)
- fix N assume N: "N \<in> HNatInfinite"
+ fix N
+ assume N: "N \<in> HNatInfinite"
have "starfun X N - star_of L \<in> Infinitesimal"
proof (rule InfinitesimalI2)
- fix r::real assume r: "0 < r"
- from LIMSEQ_D [OF X r]
- obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
- hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
+ fix r :: real
+ assume r: "0 < r"
+ from LIMSEQ_D [OF X r] obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
+ then have "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
by transfer
- thus "hnorm (starfun X N - star_of L) < star_of r"
+ then show "hnorm (starfun X N - star_of L) < star_of r"
using N by (simp add: star_of_le_HNatInfinite)
qed
- thus "starfun X N \<approx> star_of L"
- by (unfold approx_def)
+ then show "starfun X N \<approx> star_of L"
+ by (simp only: approx_def)
qed
lemma NSLIMSEQ_LIMSEQ:
- assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" shows "X \<longlonglongrightarrow> L"
+ assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+ shows "X \<longlonglongrightarrow> L"
proof (rule LIMSEQ_I)
- fix r::real assume r: "0 < r"
+ fix r :: real
+ assume r: "0 < r"
have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
proof (intro exI allI impI)
- fix n assume "whn \<le> n"
+ fix n
+ assume "whn \<le> n"
with HNatInfinite_whn have "n \<in> HNatInfinite"
by (rule HNatInfinite_upward_closed)
with X have "starfun X n \<approx> star_of L"
by (rule NSLIMSEQ_D)
- hence "starfun X n - star_of L \<in> Infinitesimal"
- by (unfold approx_def)
- thus "hnorm (starfun X n - star_of L) < star_of r"
+ then have "starfun X n - star_of L \<in> Infinitesimal"
+ by (simp only: approx_def)
+ then show "hnorm (starfun X n - star_of L) < star_of r"
using r by (rule InfinitesimalD2)
qed
- thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
+ then show "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
by transfer
qed
-theorem LIMSEQ_NSLIMSEQ_iff: "(f \<longlonglongrightarrow> L) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
-by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
+theorem LIMSEQ_NSLIMSEQ_iff: "f \<longlonglongrightarrow> L \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+ by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
+
subsubsection \<open>Derived theorems about @{term NSLIMSEQ}\<close>
-text\<open>We prove the NS version from the standard one, since the NS proof
- seems more complicated than the standard one above!\<close>
-lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0)"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
+text \<open>We prove the NS version from the standard one, since the NS proof
+ seems more complicated than the standard one above!\<close>
+lemma NSLIMSEQ_norm_zero: "(\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0 \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+ by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
-lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real))"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
-
-text\<open>Generalization to other limits\<close>
-lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S (l::real) ==> (%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>"
-apply (simp add: NSLIMSEQ_def)
-apply (auto intro: approx_hrabs
- simp add: starfun_abs)
-done
+lemma NSLIMSEQ_rabs_zero: "(\<lambda>n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0 \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real)"
+ by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
-lemma NSLIMSEQ_inverse_zero:
- "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
- ==> (%n. inverse(f n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
+text \<open>Generalization to other limits.\<close>
+lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> (\<lambda>n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>"
+ for l :: real
+ by (simp add: NSLIMSEQ_def) (auto intro: approx_hrabs simp add: starfun_abs)
+
+lemma NSLIMSEQ_inverse_zero: "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f n \<Longrightarrow> (\<lambda>n. inverse (f n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+ by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
-lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)
+lemma NSLIMSEQ_inverse_real_of_nat: "(\<lambda>n. inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+ by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)
-lemma NSLIMSEQ_inverse_real_of_nat_add:
- "(%n. r + inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc)
+lemma NSLIMSEQ_inverse_real_of_nat_add: "(\<lambda>n. r + inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
+ by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc)
-lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
- "(%n. r + -inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
+lemma NSLIMSEQ_inverse_real_of_nat_add_minus: "(\<lambda>n. r + - inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
- "(%n. r*( 1 + -inverse(real(Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
- using LIMSEQ_inverse_real_of_nat_add_minus_mult by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
+ "(\<lambda>n. r * (1 + - inverse (real (Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
+ using LIMSEQ_inverse_real_of_nat_add_minus_mult
+ by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
subsection \<open>Convergence\<close>
-lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L ==> nslim X = L"
-apply (simp add: nslim_def)
-apply (blast intro: NSLIMSEQ_unique)
-done
+lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> nslim X = L"
+ by (simp add: nslim_def) (blast intro: NSLIMSEQ_unique)
lemma lim_nslim_iff: "lim X = nslim X"
-by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
+ by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
-lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
-by (simp add: NSconvergent_def)
+lemma NSconvergentD: "NSconvergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+ by (simp add: NSconvergent_def)
-lemma NSconvergentI: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) ==> NSconvergent X"
-by (auto simp add: NSconvergent_def)
+lemma NSconvergentI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> NSconvergent X"
+ by (auto simp add: NSconvergent_def)
lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
-by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
+ by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
-lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X)"
-by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
+lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X"
+ by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
subsection \<open>Bounded Monotonic Sequences\<close>
-lemma NSBseqD: "[| NSBseq X; N: HNatInfinite |] ==> ( *f* X) N : HFinite"
-by (simp add: NSBseq_def)
+lemma NSBseqD: "NSBseq X \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> ( *f* X) N \<in> HFinite"
+ by (simp add: NSBseq_def)
lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite"
-unfolding Standard_def by auto
+ by (auto simp: Standard_def)
lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite"
-apply (cases "N \<in> HNatInfinite")
-apply (erule (1) NSBseqD)
-apply (rule subsetD [OF Standard_subset_HFinite])
-apply (simp add: HNatInfinite_def Nats_eq_Standard)
-done
+ apply (cases "N \<in> HNatInfinite")
+ apply (erule (1) NSBseqD)
+ apply (rule subsetD [OF Standard_subset_HFinite])
+ apply (simp add: HNatInfinite_def Nats_eq_Standard)
+ done
-lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
-by (simp add: NSBseq_def)
-
-text\<open>The standard definition implies the nonstandard definition\<close>
+lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite \<Longrightarrow> NSBseq X"
+ by (simp add: NSBseq_def)
-lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
-proof (unfold NSBseq_def, safe)
+text \<open>The standard definition implies the nonstandard definition.\<close>
+lemma Bseq_NSBseq: "Bseq X \<Longrightarrow> NSBseq X"
+ unfolding NSBseq_def
+proof safe
assume X: "Bseq X"
- fix N assume N: "N \<in> HNatInfinite"
- from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K" by fast
- hence "\<forall>N. hnorm (starfun X N) \<le> star_of K" by transfer
- hence "hnorm (starfun X N) \<le> star_of K" by simp
- also have "star_of K < star_of (K + 1)" by simp
- finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x" by (rule bexI, simp)
- thus "starfun X N \<in> HFinite" by (simp add: HFinite_def)
+ fix N
+ assume N: "N \<in> HNatInfinite"
+ from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K"
+ by fast
+ then have "\<forall>N. hnorm (starfun X N) \<le> star_of K"
+ by transfer
+ then have "hnorm (starfun X N) \<le> star_of K"
+ by simp
+ also have "star_of K < star_of (K + 1)"
+ by simp
+ finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x"
+ by (rule bexI) simp
+ then show "starfun X N \<in> HFinite"
+ by (simp add: HFinite_def)
qed
-text\<open>The nonstandard definition implies the standard definition\<close>
-
+text \<open>The nonstandard definition implies the standard definition.\<close>
lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
-apply (insert HInfinite_omega)
-apply (simp add: HInfinite_def)
-apply (simp add: order_less_imp_le)
-done
+ using HInfinite_omega
+ by (simp add: HInfinite_def) (simp add: order_less_imp_le)
lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X"
proof (rule ccontr)
let ?n = "\<lambda>K. LEAST n. K < norm (X n)"
assume "NSBseq X"
- hence finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
+ then have finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
by (rule NSBseqD2)
assume "\<not> Bseq X"
- hence "\<forall>K>0. \<exists>n. K < norm (X n)"
+ then have "\<forall>K>0. \<exists>n. K < norm (X n)"
by (simp add: Bseq_def linorder_not_le)
- hence "\<forall>K>0. K < norm (X (?n K))"
+ then have "\<forall>K>0. K < norm (X (?n K))"
by (auto intro: LeastI_ex)
- hence "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
+ then have "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
by transfer
- hence "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
+ then have "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
by simp
- hence "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
+ then have "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
by (simp add: order_less_trans [OF SReal_less_omega])
- hence "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
+ then have "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
by (simp add: HInfinite_def)
with finite show "False"
by (simp add: HFinite_HInfinite_iff)
qed
-text\<open>Equivalence of nonstandard and standard definitions
- for a bounded sequence\<close>
-lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
-by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
+text \<open>Equivalence of nonstandard and standard definitions for a bounded sequence.\<close>
+lemma Bseq_NSBseq_iff: "Bseq X = NSBseq X"
+ by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
-text\<open>A convergent sequence is bounded:
- Boundedness as a necessary condition for convergence.
- The nonstandard version has no existential, as usual\<close>
+text \<open>A convergent sequence is bounded:
+ Boundedness as a necessary condition for convergence.
+ The nonstandard version has no existential, as usual.\<close>
+lemma NSconvergent_NSBseq: "NSconvergent X \<Longrightarrow> NSBseq X"
+ by (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
+ (blast intro: HFinite_star_of approx_sym approx_HFinite)
-lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
-apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
-apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
-done
+text \<open>Standard Version: easily now proved using equivalence of NS and
+ standard definitions.\<close>
-text\<open>Standard Version: easily now proved using equivalence of NS and
- standard definitions\<close>
+lemma convergent_Bseq: "convergent X \<Longrightarrow> Bseq X"
+ for X :: "nat \<Rightarrow> 'b::real_normed_vector"
+ by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
-lemma convergent_Bseq: "convergent X ==> Bseq (X::nat \<Rightarrow> _::real_normed_vector)"
-by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
-subsubsection\<open>Upper Bounds and Lubs of Bounded Sequences\<close>
+subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close>
-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_isUb: "NSBseq X \<Longrightarrow> \<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::real. isLub UNIV {x. \<exists>n. X n = x} U"
-by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
+lemma NSBseq_isLub: "NSBseq X \<Longrightarrow> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
+ by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
+
-subsubsection\<open>A Bounded and Monotonic Sequence Converges\<close>
+subsubsection \<open>A Bounded and Monotonic Sequence Converges\<close>
-text\<open>The best of both worlds: Easier to prove this result as a standard
+text \<open>The best of both worlds: Easier to prove this result as a standard
theorem and then use equivalence to "transfer" it into the
equivalent nonstandard form if needed!\<close>
-lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
-by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
+lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+ by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
-lemma NSBseq_mono_NSconvergent:
- "[| 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])
+lemma NSBseq_mono_NSconvergent: "NSBseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> NSconvergent X"
+ for X :: "nat \<Rightarrow> real"
+ by (auto intro: Bseq_mono_convergent
+ simp: convergent_NSconvergent_iff [symmetric] Bseq_NSBseq_iff [symmetric])
subsection \<open>Cauchy Sequences\<close>
lemma NSCauchyI:
- "(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N)
- \<Longrightarrow> NSCauchy X"
-by (simp add: NSCauchy_def)
+ "(\<And>M N. M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N) \<Longrightarrow> NSCauchy X"
+ by (simp add: NSCauchy_def)
lemma NSCauchyD:
- "\<lbrakk>NSCauchy X; M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk>
- \<Longrightarrow> starfun X M \<approx> starfun X N"
-by (simp add: NSCauchy_def)
+ "NSCauchy X \<Longrightarrow> M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N"
+ by (simp add: NSCauchy_def)
-subsubsection\<open>Equivalence Between NS and Standard\<close>
+
+subsubsection \<open>Equivalence Between NS and Standard\<close>
lemma Cauchy_NSCauchy:
- assumes X: "Cauchy X" shows "NSCauchy X"
+ assumes X: "Cauchy X"
+ shows "NSCauchy X"
proof (rule NSCauchyI)
- fix M assume M: "M \<in> HNatInfinite"
- fix N assume N: "N \<in> HNatInfinite"
+ fix M
+ assume M: "M \<in> HNatInfinite"
+ fix N
+ assume N: "N \<in> HNatInfinite"
have "starfun X M - starfun X N \<in> Infinitesimal"
proof (rule InfinitesimalI2)
- fix r :: real assume r: "0 < r"
- from CauchyD [OF X r]
- obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
- hence "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k.
- hnorm (starfun X m - starfun X n) < star_of r"
+ fix r :: real
+ assume r: "0 < r"
+ from CauchyD [OF X r] obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
+ then have "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k. hnorm (starfun X m - starfun X n) < star_of r"
by transfer
- thus "hnorm (starfun X M - starfun X N) < star_of r"
+ then show "hnorm (starfun X M - starfun X N) < star_of r"
using M N by (simp add: star_of_le_HNatInfinite)
qed
- thus "starfun X M \<approx> starfun X N"
- by (unfold approx_def)
+ then show "starfun X M \<approx> starfun X N"
+ by (simp only: approx_def)
qed
lemma NSCauchy_Cauchy:
- assumes X: "NSCauchy X" shows "Cauchy X"
+ assumes X: "NSCauchy X"
+ shows "Cauchy X"
proof (rule CauchyI)
- fix r::real assume r: "0 < r"
+ fix r :: real
+ assume r: "0 < r"
have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r"
proof (intro exI allI impI)
- fix M assume "whn \<le> M"
+ fix M
+ assume "whn \<le> M"
with HNatInfinite_whn have M: "M \<in> HNatInfinite"
by (rule HNatInfinite_upward_closed)
- fix N assume "whn \<le> N"
+ fix N
+ assume "whn \<le> N"
with HNatInfinite_whn have N: "N \<in> HNatInfinite"
by (rule HNatInfinite_upward_closed)
from X M N have "starfun X M \<approx> starfun X N"
by (rule NSCauchyD)
- hence "starfun X M - starfun X N \<in> Infinitesimal"
- by (unfold approx_def)
- thus "hnorm (starfun X M - starfun X N) < star_of r"
+ then have "starfun X M - starfun X N \<in> Infinitesimal"
+ by (simp only: approx_def)
+ then show "hnorm (starfun X M - starfun X N) < star_of r"
using r by (rule InfinitesimalD2)
qed
- thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
+ then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
by transfer
qed
theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
-by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
+ by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
+
subsubsection \<open>Cauchy Sequences are Bounded\<close>
-text\<open>A Cauchy sequence is bounded -- nonstandard version\<close>
+text \<open>A Cauchy sequence is bounded -- nonstandard version.\<close>
-lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
-by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
+lemma NSCauchy_NSBseq: "NSCauchy X \<Longrightarrow> NSBseq X"
+ by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
+
subsubsection \<open>Cauchy Sequences are Convergent\<close>
-text\<open>Equivalence of Cauchy criterion and convergence:
+text \<open>Equivalence of Cauchy criterion and convergence:
We will prove this using our NS formulation which provides a
much easier proof than using the standard definition. We do not
need to use properties of subsequences such as boundedness,
@@ -453,64 +450,60 @@
since the NS formulations do not involve existential quantifiers.\<close>
lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
-apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe)
-apply (auto intro: approx_trans2)
-done
+ by (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def) (auto intro: approx_trans2)
-lemma real_NSCauchy_NSconvergent:
- fixes X :: "nat \<Rightarrow> real"
- shows "NSCauchy X \<Longrightarrow> NSconvergent X"
-apply (simp add: NSconvergent_def NSLIMSEQ_def)
-apply (frule NSCauchy_NSBseq)
-apply (simp add: NSBseq_def NSCauchy_def)
-apply (drule HNatInfinite_whn [THEN [2] bspec])
-apply (drule HNatInfinite_whn [THEN [2] bspec])
-apply (auto dest!: st_part_Ex simp add: SReal_iff)
-apply (blast intro: approx_trans3)
-done
+lemma real_NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
+ for X :: "nat \<Rightarrow> real"
+ apply (simp add: NSconvergent_def NSLIMSEQ_def)
+ apply (frule NSCauchy_NSBseq)
+ apply (simp add: NSBseq_def NSCauchy_def)
+ apply (drule HNatInfinite_whn [THEN [2] bspec])
+ apply (drule HNatInfinite_whn [THEN [2] bspec])
+ apply (auto dest!: st_part_Ex simp add: SReal_iff)
+ apply (blast intro: approx_trans3)
+ done
-lemma NSCauchy_NSconvergent:
- fixes X :: "nat \<Rightarrow> 'a::banach"
- shows "NSCauchy X \<Longrightarrow> NSconvergent X"
-apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
-apply (erule convergent_NSconvergent_iff [THEN iffD1])
-done
+lemma NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
+ for X :: "nat \<Rightarrow> 'a::banach"
+ apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
+ apply (erule convergent_NSconvergent_iff [THEN iffD1])
+ done
-lemma NSCauchy_NSconvergent_iff:
- fixes X :: "nat \<Rightarrow> 'a::banach"
- shows "NSCauchy X = NSconvergent X"
-by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
+lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
+ for X :: "nat \<Rightarrow> 'a::banach"
+ by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
subsection \<open>Power Sequences\<close>
-text\<open>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
+text \<open>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.\<close>
-text\<open>We now use NS criterion to bring proof of theorem through\<close>
+text \<open>We now use NS criterion to bring proof of theorem through.\<close>
+lemma NSLIMSEQ_realpow_zero: "0 \<le> x \<Longrightarrow> x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+ for x :: real
+ apply (simp add: NSLIMSEQ_def)
+ apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
+ apply (frule NSconvergentD)
+ apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
+ apply (frule HNatInfinite_add_one)
+ apply (drule bspec, assumption)
+ apply (drule bspec, assumption)
+ apply (drule_tac x = "N + 1" in bspec, assumption)
+ apply (simp add: hyperpow_add)
+ apply (drule approx_mult_subst_star_of, assumption)
+ apply (drule approx_trans3, assumption)
+ apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
+ done
-lemma NSLIMSEQ_realpow_zero:
- "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-apply (simp add: NSLIMSEQ_def)
-apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
-apply (frule NSconvergentD)
-apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
-apply (frule HNatInfinite_add_one)
-apply (drule bspec, assumption)
-apply (drule bspec, assumption)
-apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
-apply (simp add: hyperpow_add)
-apply (drule approx_mult_subst_star_of, assumption)
-apply (drule approx_trans3, assumption)
-apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
-done
+lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+ for c :: real
+ by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
-lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
-
-lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
+lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+ for c :: real
+ by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
(***---------------------------------------------------------------
Theorems proved by Harrison in HOL that we do not need
--- a/src/HOL/Nonstandard_Analysis/HSeries.thy Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy Sun Dec 18 23:43:50 2016 +0100
@@ -5,200 +5,177 @@
Converted to Isar and polished by lcp
*)
-section\<open>Finite Summation and Infinite Series for Hyperreals\<close>
+section \<open>Finite Summation and Infinite Series for Hyperreals\<close>
theory HSeries
-imports HSEQ
+ imports HSEQ
begin
-definition
- sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
- "sumhr =
- (%(M,N,f). starfun2 (%m n. sum f {m..<n}) M N)"
+definition sumhr :: "hypnat \<times> hypnat \<times> (nat \<Rightarrow> real) \<Rightarrow> hypreal"
+ where "sumhr = (\<lambda>(M,N,f). starfun2 (\<lambda>m n. sum f {m..<n}) M N)"
+
+definition NSsums :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool" (infixr "NSsums" 80)
+ where "f NSsums s = (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s"
-definition
- NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80) where
- "f NSsums s = (%n. sum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s"
+definition NSsummable :: "(nat \<Rightarrow> real) \<Rightarrow> bool"
+ where "NSsummable f \<longleftrightarrow> (\<exists>s. f NSsums s)"
-definition
- NSsummable :: "(nat=>real) => bool" where
- "NSsummable f = (\<exists>s. f NSsums s)"
+definition NSsuminf :: "(nat \<Rightarrow> real) \<Rightarrow> real"
+ where "NSsuminf f = (THE s. f NSsums s)"
-definition
- NSsuminf :: "(nat=>real) => real" where
- "NSsuminf f = (THE s. f NSsums s)"
+lemma sumhr_app: "sumhr (M, N, f) = ( *f2* (\<lambda>m n. sum f {m..<n})) M N"
+ by (simp add: sumhr_def)
-lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. sum f {m..<n})) M N"
-by (simp add: sumhr_def)
+text \<open>Base case in definition of @{term sumr}.\<close>
+lemma sumhr_zero [simp]: "\<And>m. sumhr (m, 0, f) = 0"
+ unfolding sumhr_app by transfer simp
-text\<open>Base case in definition of @{term sumr}\<close>
-lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0"
-unfolding sumhr_app by transfer simp
-
-text\<open>Recursive case in definition of @{term sumr}\<close>
+text \<open>Recursive case in definition of @{term sumr}.\<close>
lemma sumhr_if:
- "!!m n. sumhr(m,n+1,f) =
- (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)"
-unfolding sumhr_app by transfer simp
+ "\<And>m n. sumhr (m, n + 1, f) = (if n + 1 \<le> m then 0 else sumhr (m, n, f) + ( *f* f) n)"
+ unfolding sumhr_app by transfer simp
+
+lemma sumhr_Suc_zero [simp]: "\<And>n. sumhr (n + 1, n, f) = 0"
+ unfolding sumhr_app by transfer simp
-lemma sumhr_Suc_zero [simp]: "!!n. sumhr (n + 1, n, f) = 0"
-unfolding sumhr_app by transfer simp
+lemma sumhr_eq_bounds [simp]: "\<And>n. sumhr (n, n, f) = 0"
+ unfolding sumhr_app by transfer simp
-lemma sumhr_eq_bounds [simp]: "!!n. sumhr (n,n,f) = 0"
-unfolding sumhr_app by transfer simp
+lemma sumhr_Suc [simp]: "\<And>m. sumhr (m, m + 1, f) = ( *f* f) m"
+ unfolding sumhr_app by transfer simp
-lemma sumhr_Suc [simp]: "!!m. sumhr (m,m + 1,f) = ( *f* f) m"
-unfolding sumhr_app by transfer simp
+lemma sumhr_add_lbound_zero [simp]: "\<And>k m. sumhr (m + k, k, f) = 0"
+ unfolding sumhr_app by transfer simp
-lemma sumhr_add_lbound_zero [simp]: "!!k m. sumhr(m+k,k,f) = 0"
-unfolding sumhr_app by transfer simp
+lemma sumhr_add: "\<And>m n. sumhr (m, n, f) + sumhr (m, n, g) = sumhr (m, n, \<lambda>i. f i + g i)"
+ unfolding sumhr_app by transfer (rule sum.distrib [symmetric])
-lemma sumhr_add:
- "!!m n. sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
-unfolding sumhr_app by transfer (rule sum.distrib [symmetric])
+lemma sumhr_mult: "\<And>m n. hypreal_of_real r * sumhr (m, n, f) = sumhr (m, n, \<lambda>n. r * f n)"
+ unfolding sumhr_app by transfer (rule sum_distrib_left)
-lemma sumhr_mult:
- "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
-unfolding sumhr_app by transfer (rule sum_distrib_left)
+lemma sumhr_split_add: "\<And>n p. n < p \<Longrightarrow> sumhr (0, n, f) + sumhr (n, p, f) = sumhr (0, p, f)"
+ unfolding sumhr_app by transfer (simp add: sum_add_nat_ivl)
-lemma sumhr_split_add:
- "!!n p. n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
-unfolding sumhr_app by transfer (simp add: sum_add_nat_ivl)
+lemma sumhr_split_diff: "n < p \<Longrightarrow> sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n, p, f)"
+ by (drule sumhr_split_add [symmetric, where f = f]) simp
-lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
-by (drule_tac f = f in sumhr_split_add [symmetric], simp)
+lemma sumhr_hrabs: "\<And>m n. \<bar>sumhr (m, n, f)\<bar> \<le> sumhr (m, n, \<lambda>i. \<bar>f i\<bar>)"
+ unfolding sumhr_app by transfer (rule sum_abs)
-lemma sumhr_hrabs: "!!m n. \<bar>sumhr(m,n,f)\<bar> \<le> sumhr(m,n,%i. \<bar>f i\<bar>)"
-unfolding sumhr_app by transfer (rule sum_abs)
-
-text\<open>other general version also needed\<close>
+text \<open>Other general version also needed.\<close>
lemma sumhr_fun_hypnat_eq:
- "(\<forall>r. m \<le> r & r < n --> f r = g r) -->
- sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =
- sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
-unfolding sumhr_app by transfer simp
+ "(\<forall>r. m \<le> r \<and> r < n \<longrightarrow> f r = g r) \<longrightarrow>
+ sumhr (hypnat_of_nat m, hypnat_of_nat n, f) =
+ sumhr (hypnat_of_nat m, hypnat_of_nat n, g)"
+ unfolding sumhr_app by transfer simp
-lemma sumhr_const:
- "!!n. sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
-unfolding sumhr_app by transfer simp
+lemma sumhr_const: "\<And>n. sumhr (0, n, \<lambda>i. r) = hypreal_of_hypnat n * hypreal_of_real r"
+ unfolding sumhr_app by transfer simp
-lemma sumhr_less_bounds_zero [simp]: "!!m n. n < m ==> sumhr(m,n,f) = 0"
-unfolding sumhr_app by transfer simp
+lemma sumhr_less_bounds_zero [simp]: "\<And>m n. n < m \<Longrightarrow> sumhr (m, n, f) = 0"
+ unfolding sumhr_app by transfer simp
-lemma sumhr_minus: "!!m n. sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
-unfolding sumhr_app by transfer (rule sum_negf)
+lemma sumhr_minus: "\<And>m n. sumhr (m, n, \<lambda>i. - f i) = - sumhr (m, n, f)"
+ unfolding sumhr_app by transfer (rule sum_negf)
lemma sumhr_shift_bounds:
- "!!m n. sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) =
- sumhr(m,n,%i. f(i + k))"
-unfolding sumhr_app by transfer (rule sum_shift_bounds_nat_ivl)
+ "\<And>m n. sumhr (m + hypnat_of_nat k, n + hypnat_of_nat k, f) =
+ sumhr (m, n, \<lambda>i. f (i + k))"
+ unfolding sumhr_app by transfer (rule sum_shift_bounds_nat_ivl)
-subsection\<open>Nonstandard Sums\<close>
+subsection \<open>Nonstandard Sums\<close>
-text\<open>Infinite sums are obtained by summing to some infinite hypernatural
- (such as @{term whn})\<close>
-lemma sumhr_hypreal_of_hypnat_omega:
- "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
-by (simp add: sumhr_const)
+text \<open>Infinite sums are obtained by summing to some infinite hypernatural
+ (such as @{term whn}).\<close>
+lemma sumhr_hypreal_of_hypnat_omega: "sumhr (0, whn, \<lambda>i. 1) = hypreal_of_hypnat whn"
+ by (simp add: sumhr_const)
-lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = \<omega> - 1"
-apply (simp add: sumhr_const)
-(* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
-(* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
-apply (unfold star_class_defs omega_def hypnat_omega_def
- of_hypnat_def star_of_def)
-apply (simp add: starfun_star_n starfun2_star_n)
-done
+lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, \<lambda>i. 1) = \<omega> - 1"
+ apply (simp add: sumhr_const)
+ (* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
+ (* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
+ apply (unfold star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def)
+ apply (simp add: starfun_star_n starfun2_star_n)
+ done
-lemma sumhr_minus_one_realpow_zero [simp]:
- "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
-unfolding sumhr_app
-apply transfer
-apply (simp del: power_Suc add: mult_2 [symmetric])
-apply (induct_tac N)
-apply simp_all
-done
+lemma sumhr_minus_one_realpow_zero [simp]: "\<And>N. sumhr (0, N + N, \<lambda>i. (-1) ^ (i + 1)) = 0"
+ unfolding sumhr_app
+ apply transfer
+ apply (simp del: power_Suc add: mult_2 [symmetric])
+ apply (induct_tac N)
+ apply simp_all
+ done
lemma sumhr_interval_const:
- "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
- ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =
- (hypreal_of_nat (na - m) * hypreal_of_real r)"
-unfolding sumhr_app by transfer simp
+ "(\<forall>n. m \<le> Suc n \<longrightarrow> f n = r) \<and> m \<le> na \<Longrightarrow>
+ sumhr (hypnat_of_nat m, hypnat_of_nat na, f) = hypreal_of_nat (na - m) * hypreal_of_real r"
+ unfolding sumhr_app by transfer simp
-lemma starfunNat_sumr: "!!N. ( *f* (%n. sum f {0..<n})) N = sumhr(0,N,f)"
-unfolding sumhr_app by transfer (rule refl)
+lemma starfunNat_sumr: "\<And>N. ( *f* (\<lambda>n. sum f {0..<n})) N = sumhr (0, N, f)"
+ unfolding sumhr_app by transfer (rule refl)
-lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) \<approx> sumhr(0, N, f)
- ==> \<bar>sumhr(M, N, f)\<bar> \<approx> 0"
-apply (cut_tac x = M and y = N in linorder_less_linear)
-apply (auto simp add: approx_refl)
-apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
-apply (auto dest: approx_hrabs
- simp add: sumhr_split_diff)
-done
+lemma sumhr_hrabs_approx [simp]: "sumhr (0, M, f) \<approx> sumhr (0, N, f) \<Longrightarrow> \<bar>sumhr (M, N, f)\<bar> \<approx> 0"
+ using linorder_less_linear [where x = M and y = N]
+ apply auto
+ apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
+ apply (auto dest: approx_hrabs simp add: sumhr_split_diff)
+ done
+
+
+subsection \<open>Infinite sums: Standard and NS theorems\<close>
-(*----------------------------------------------------------------
- infinite sums: Standard and NS theorems
- ----------------------------------------------------------------*)
-lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)"
-by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
+lemma sums_NSsums_iff: "f sums l \<longleftrightarrow> f NSsums l"
+ by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
-lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)"
-by (simp add: summable_def NSsummable_def sums_NSsums_iff)
+lemma summable_NSsummable_iff: "summable f \<longleftrightarrow> NSsummable f"
+ by (simp add: summable_def NSsummable_def sums_NSsums_iff)
-lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)"
-by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
+lemma suminf_NSsuminf_iff: "suminf f = NSsuminf f"
+ by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
-lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f"
-by (simp add: NSsums_def NSsummable_def, blast)
+lemma NSsums_NSsummable: "f NSsums l \<Longrightarrow> NSsummable f"
+ unfolding NSsums_def NSsummable_def by blast
-lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
-apply (simp add: NSsummable_def NSsuminf_def NSsums_def)
-apply (blast intro: theI NSLIMSEQ_unique)
-done
+lemma NSsummable_NSsums: "NSsummable f \<Longrightarrow> f NSsums (NSsuminf f)"
+ unfolding NSsummable_def NSsuminf_def NSsums_def
+ by (blast intro: theI NSLIMSEQ_unique)
-lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
-by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
+lemma NSsums_unique: "f NSsums s \<Longrightarrow> s = NSsuminf f"
+ by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
-lemma NSseries_zero:
- "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sum f {..<n})"
-by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
+lemma NSseries_zero: "\<forall>m. n \<le> Suc m \<longrightarrow> f m = 0 \<Longrightarrow> f NSsums (sum f {..<n})"
+ by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
lemma NSsummable_NSCauchy:
- "NSsummable f =
- (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> \<approx> 0)"
-apply (auto simp add: summable_NSsummable_iff [symmetric]
- summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
- NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
-apply (cut_tac x = M and y = N in linorder_less_linear)
-apply auto
-apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
-apply (rule_tac [2] approx_minus_iff [THEN iffD2])
-apply (auto dest: approx_hrabs_zero_cancel
- simp add: sumhr_split_diff atLeast0LessThan[symmetric])
-done
+ "NSsummable f \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr (M, N, f)\<bar> \<approx> 0)"
+ apply (auto simp add: summable_NSsummable_iff [symmetric]
+ summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
+ NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
+ apply (cut_tac x = M and y = N in linorder_less_linear)
+ apply auto
+ apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
+ apply (rule_tac [2] approx_minus_iff [THEN iffD2])
+ apply (auto dest: approx_hrabs_zero_cancel simp: sumhr_split_diff atLeast0LessThan[symmetric])
+ done
-text\<open>Terms of a convergent series tend to zero\<close>
-lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
-apply (drule bspec, auto)
-apply (drule_tac x = "N + 1 " in bspec)
-apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
-done
+text \<open>Terms of a convergent series tend to zero.\<close>
+lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+ apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
+ apply (drule bspec)
+ apply auto
+ apply (drule_tac x = "N + 1 " in bspec)
+ apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
+ done
-text\<open>Nonstandard comparison test\<close>
-lemma NSsummable_comparison_test:
- "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |] ==> NSsummable f"
-apply (fold summable_NSsummable_iff)
-apply (rule summable_comparison_test, simp, assumption)
-done
+text \<open>Nonstandard comparison test.\<close>
+lemma NSsummable_comparison_test: "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable f"
+ apply (fold summable_NSsummable_iff)
+ apply (rule summable_comparison_test, simp, assumption)
+ done
lemma NSsummable_rabs_comparison_test:
- "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |]
- ==> NSsummable (%k. \<bar>f k\<bar>)"
-apply (rule NSsummable_comparison_test)
-apply (auto)
-done
+ "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable (\<lambda>k. \<bar>f k\<bar>)"
+ by (rule NSsummable_comparison_test) auto
end