# HG changeset patch # User huffman # Date 1176050119 -7200 # Node ID 17644bc9cee41455670842533aaa48a924ea402f # Parent 2f119f54d1500bfc269b7de461a3d5e1b18ff490 rearranged sections diff -r 2f119f54d150 -r 17644bc9cee4 src/HOL/Hyperreal/SEQ.thy --- a/src/HOL/Hyperreal/SEQ.thy Sun Apr 08 17:54:52 2007 +0200 +++ b/src/HOL/Hyperreal/SEQ.thy Sun Apr 08 18:35:19 2007 +0200 @@ -542,6 +542,86 @@ by (simp add: setprod_def LIMSEQ_const) qed +lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b" +by (simp add: LIMSEQ_add LIMSEQ_const) + +(* FIXME: delete *) +lemma LIMSEQ_add_minus: + "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b" +by (simp only: LIMSEQ_add LIMSEQ_minus) + +lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n - b)) ----> a - b" +by (simp add: LIMSEQ_diff LIMSEQ_const) + +lemma LIMSEQ_diff_approach_zero: + "g ----> L ==> (%x. f x - g x) ----> 0 ==> + f ----> L" + apply (drule LIMSEQ_add) + apply assumption + apply simp +done + +lemma LIMSEQ_diff_approach_zero2: + "f ----> L ==> (%x. f x - g x) ----> 0 ==> + g ----> L"; + apply (drule LIMSEQ_diff) + apply assumption + apply simp +done + +text{*A sequence tends to zero iff its abs does*} +lemma LIMSEQ_norm_zero: "((\n. norm (X n)) ----> 0) = (X ----> 0)" +by (simp add: LIMSEQ_def) + +lemma LIMSEQ_rabs_zero: "((%n. \f n\) ----> 0) = (f ----> (0::real))" +by (simp add: LIMSEQ_def) + +lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \f n\) ----> \l\" +by (drule LIMSEQ_norm, simp) + +text{*An unbounded sequence's inverse tends to 0*} + +text{* standard proof seems easier *} +lemma LIMSEQ_inverse_zero: + "\y::real. \N. \n \ 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) +apply (drule spec, auto) +apply (frule positive_imp_inverse_positive) +apply (frule order_less_trans, assumption) +apply (frule_tac a = "f n" in positive_imp_inverse_positive) +apply (simp add: abs_if) +apply (rule_tac t = r in inverse_inverse_eq [THEN subst]) +apply (auto intro: inverse_less_iff_less [THEN iffD2] + simp del: inverse_inverse_eq) +done + +text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} + +lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" +apply (rule LIMSEQ_inverse_zero, safe) +apply (cut_tac x = y in reals_Archimedean2) +apply (safe, rule_tac x = n in exI) +apply (auto simp add: real_of_nat_Suc) +done + +text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to +infinity is now easily proved*} + +lemma LIMSEQ_inverse_real_of_nat_add: + "(%n. r + inverse(real(Suc n))) ----> r" +by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) + +lemma LIMSEQ_inverse_real_of_nat_add_minus: + "(%n. r + -inverse(real(Suc n))) ----> r" +by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) + +lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: + "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" +by (cut_tac b=1 in + LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto) + subsubsection {* Purely nonstandard proofs *} lemma NSLIMSEQ_iff: @@ -620,6 +700,49 @@ apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const) done +text{*We can now try and derive a few properties of sequences, + starting with the limit comparison property for sequences.*} + +lemma NSLIMSEQ_le: + "[| f ----NS> l; g ----NS> m; + \N. \n \ N. f(n) \ g(n) + |] ==> 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 ----NS> (r::real); \n. a \ X n |] ==> a \ r" +by (erule NSLIMSEQ_le [OF NSLIMSEQ_const], auto) + +lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \n. X n \ a |] ==> r \ a" +by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto) + +text{*Shift a convergent series by 1: + By the equivalence between Cauchiness and convergence and because + the successor of an infinite hypernatural is also infinite.*} + +lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> 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_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> 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_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)" +by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc) + subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *} lemma LIMSEQ_NSLIMSEQ: @@ -670,33 +793,63 @@ subsubsection {* Derived theorems about @{term LIMSEQ} *} -lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b" -by (simp add: LIMSEQ_add LIMSEQ_const) +lemma LIMSEQ_le: + "[| f ----> l; g ----> m; \N. \n \ N. f(n) \ g(n) |] + ==> l \ (m::real)" +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le) -(* FIXME: delete *) -lemma LIMSEQ_add_minus: - "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b" -by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus) +lemma LIMSEQ_le_const: "[| X ----> (r::real); \n. a \ X n |] ==> a \ r" +by (erule LIMSEQ_le [OF LIMSEQ_const], auto) -lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n - b)) ----> a - b" -by (simp add: LIMSEQ_diff LIMSEQ_const) +lemma LIMSEQ_le_const2: "[| X ----> (r::real); \n. X n \ a |] ==> r \ a" +by (erule LIMSEQ_le [OF _ LIMSEQ_const], auto) -lemma LIMSEQ_diff_approach_zero: - "g ----> L ==> (%x. f x - g x) ----> 0 ==> - f ----> L" - apply (drule LIMSEQ_add) - apply assumption - apply simp +lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l" +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc) + +lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l" +apply (simp add: LIMSEQ_NSLIMSEQ_iff) +apply (erule NSLIMSEQ_imp_Suc) done -lemma LIMSEQ_diff_approach_zero2: - "f ----> L ==> (%x. f x - g x) ----> 0 ==> - g ----> L"; - apply (drule LIMSEQ_diff) - apply assumption - apply simp +lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)" +by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) + +text{*We prove the NS version from the standard one, since the NS proof + seems more complicated than the standard one above!*} +lemma NSLIMSEQ_norm_zero: "((\n. norm (X n)) ----NS> 0) = (X ----NS> 0)" +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_norm_zero) + +lemma NSLIMSEQ_rabs_zero: "((%n. \f n\) ----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::real) ==> (%n. \f n\) ----NS> \l\" +apply (simp add: NSLIMSEQ_def) +apply (auto intro: approx_hrabs + simp add: starfun_abs) done +lemma NSLIMSEQ_inverse_zero: + "\y::real. \N. \n \ N. y < f(n) + ==> (%n. inverse(f n)) ----NS> 0" +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero) + +lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0" +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat) + +lemma NSLIMSEQ_inverse_real_of_nat_add: + "(%n. r + inverse(real(Suc n))) ----NS> r" +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add) + +lemma NSLIMSEQ_inverse_real_of_nat_add_minus: + "(%n. r + -inverse(real(Suc n))) ----NS> r" +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus) + +lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult: + "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r" +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult) + subsection {* Convergence *} @@ -1209,169 +1362,6 @@ by (fast intro: Cauchy_convergent convergent_Cauchy) -subsection {* More Properties of Sequences *} - -text{*We can now try and derive a few properties of sequences, - starting with the limit comparison property for sequences.*} - -lemma NSLIMSEQ_le: - "[| f ----NS> l; g ----NS> m; - \N. \n \ N. f(n) \ g(n) - |] ==> 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 - -(* standard version *) -lemma LIMSEQ_le: - "[| f ----> l; g ----> m; \N. \n \ N. f(n) \ g(n) |] - ==> l \ (m::real)" -by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le) - -lemma LIMSEQ_le_const: "[| X ----> (r::real); \n. a \ X n |] ==> a \ r" -apply (rule LIMSEQ_le) -apply (rule LIMSEQ_const, auto) -done - -lemma NSLIMSEQ_le_const: "[| X ----NS> (r::real); \n. a \ X n |] ==> a \ r" -by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const) - -lemma LIMSEQ_le_const2: "[| X ----> (r::real); \n. X n \ a |] ==> r \ a" -apply (rule LIMSEQ_le) -apply (rule_tac [2] LIMSEQ_const, auto) -done - -lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \n. X n \ a |] ==> r \ a" -by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2) - -text{*Shift a convergent series by 1: - By the equivalence between Cauchiness and convergence and because - the successor of an infinite hypernatural is also infinite.*} - -lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> 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 - -text{* standard version *} -lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l" -by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc) - -lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> 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 LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l" -apply (simp add: LIMSEQ_NSLIMSEQ_iff) -apply (erule NSLIMSEQ_imp_Suc) -done - -lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)" -by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) - -lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)" -by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc) - -text{*A sequence tends to zero iff its abs does*} -lemma LIMSEQ_norm_zero: "((\n. norm (X n)) ----> 0) = (X ----> 0)" -by (simp add: LIMSEQ_def) - -lemma LIMSEQ_rabs_zero: "((%n. \f n\) ----> 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_norm_zero: "((\n. norm (X n)) ----NS> 0) = (X ----NS> 0)" -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_norm_zero) - -lemma NSLIMSEQ_rabs_zero: "((%n. \f n\) ----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::real) ==> (%n. \f n\) ----NS> \l\" -apply (simp add: NSLIMSEQ_def) -apply (auto intro: approx_hrabs - simp add: starfun_abs) -done - -text{* standard version *} -lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \f n\) ----> \l\" -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: - "\y::real. \N. \n \ 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) -apply (drule spec, auto) -apply (frule positive_imp_inverse_positive) -apply (frule order_less_trans, assumption) -apply (frule_tac a = "f n" in positive_imp_inverse_positive) -apply (simp add: abs_if) -apply (rule_tac t = r in inverse_inverse_eq [THEN subst]) -apply (auto intro: inverse_less_iff_less [THEN iffD2] - simp del: inverse_inverse_eq) -done - -lemma NSLIMSEQ_inverse_zero: - "\y::real. \N. \n \ N. y < f(n) - ==> (%n. inverse(f n)) ----NS> 0" -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero) - -text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} - -lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" -apply (rule LIMSEQ_inverse_zero, safe) -apply (cut_tac x = y in reals_Archimedean2) -apply (safe, rule_tac x = n in exI) -apply (auto simp add: real_of_nat_Suc) -done - -lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0" -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat) - -text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to -infinity is now easily proved*} - -lemma LIMSEQ_inverse_real_of_nat_add: - "(%n. r + inverse(real(Suc n))) ----> r" -by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) - -lemma NSLIMSEQ_inverse_real_of_nat_add: - "(%n. r + inverse(real(Suc n))) ----NS> r" -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add) - -lemma LIMSEQ_inverse_real_of_nat_add_minus: - "(%n. r + -inverse(real(Suc n))) ----> r" -by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) - -lemma NSLIMSEQ_inverse_real_of_nat_add_minus: - "(%n. r + -inverse(real(Suc n))) ----NS> r" -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus) - -lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: - "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" -by (cut_tac b=1 in - LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto) - -lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult: - "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r" -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult) - - subsection {* Power Sequences *} text{*The sequence @{term "x^n"} tends to 0 if @{term "0\x"} and @{term