(* Title: HOL/Nonstandard_Analysis/NatStar.thy
Author: Jacques D. Fleuriot
Copyright: 1998 University of Cambridge
Converted to Isar and polished by lcp
*)
section \<open>Star-transforms for the Hypernaturals\<close>
theory NatStar
imports Star
begin
lemma star_n_eq_starfun_whn: "star_n X = ( *f* X) whn"
by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
lemma starset_n_Un: "*sn* (\n. (A n) \ (B n)) = *sn* A \ *sn* B"
proof -
have "\N. Iset ((*f* (\n. {x. x \ A n \ x \ B n})) N) =
{x. x \<in> Iset ((*f* A) N) \<or> x \<in> Iset ((*f* B) N)}"
by transfer simp
then show ?thesis
by (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
qed
lemma InternalSets_Un: "X \ InternalSets \ Y \ InternalSets \ X \ Y \ InternalSets"
by (auto simp add: InternalSets_def starset_n_Un [symmetric])
lemma starset_n_Int: "*sn* (\n. A n \ B n) = *sn* A \ *sn* B"
proof -
have "\N. Iset ((*f* (\n. {x. x \ A n \ x \ B n})) N) =
{x. x \<in> Iset ((*f* A) N) \<and> x \<in> Iset ((*f* B) N)}"
by transfer simp
then show ?thesis
by (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
qed
lemma InternalSets_Int: "X \ InternalSets \ Y \ InternalSets \ X \ Y \ InternalSets"
by (auto simp add: InternalSets_def starset_n_Int [symmetric])
lemma starset_n_Compl: "*sn* ((\n. - A n)) = - ( *sn* A)"
proof -
have "\N. Iset ((*f* (\n. {x. x \ A n})) N) =
{x. x \<notin> Iset ((*f* A) N)}"
by transfer simp
then show ?thesis
by (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
qed
lemma InternalSets_Compl: "X \ InternalSets \ - X \ InternalSets"
by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
lemma starset_n_diff: "*sn* (\n. (A n) - (B n)) = *sn* A - *sn* B"
proof -
have "\N. Iset ((*f* (\n. {x. x \ A n \ x \ B n})) N) =
{x. x \<in> Iset ((*f* A) N) \<and> x \<notin> Iset ((*f* B) N)}"
by transfer simp
then show ?thesis
by (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
qed
lemma InternalSets_diff: "X \ InternalSets \ Y \ InternalSets \ X - Y \ InternalSets"
by (auto simp add: InternalSets_def starset_n_diff [symmetric])
lemma NatStar_SHNat_subset: "Nats \ *s* (UNIV:: nat set)"
by simp
lemma NatStar_hypreal_of_real_Int: "*s* X Int Nats = hypnat_of_nat ` X"
by (auto simp add: SHNat_eq)
lemma starset_starset_n_eq: "*s* X = *sn* (\n. X)"
by (simp add: starset_n_starset)
lemma InternalSets_starset_n [simp]: "( *s* X) \ InternalSets"
by (auto simp add: InternalSets_def starset_starset_n_eq)
lemma InternalSets_UNIV_diff: "X \ InternalSets \ UNIV - X \ InternalSets"
by (simp add: InternalSets_Compl diff_eq)
subsection \<open>Nonstandard Extensions of Functions\<close>
text \<open>Example of transfer of a property from reals to hyperreals
--- used for limit comparison of sequences.\<close>
lemma starfun_le_mono: "\n. N \ n \ f n \ g n \
\<forall>n. hypnat_of_nat N \<le> n \<longrightarrow> ( *f* f) n \<le> ( *f* g) n"
by transfer
text \<open>And another:\<close>
lemma starfun_less_mono:
"\n. N \ n \ f n < g n \ \n. hypnat_of_nat N \ n \ ( *f* f) n < ( *f* g) n"
by transfer
text \<open>Nonstandard extension when we increment the argument by one.\<close>
lemma starfun_shift_one: "\N. ( *f* (\n. f (Suc n))) N = ( *f* f) (N + (1::hypnat))"
by transfer simp
text \<open>Nonstandard extension with absolute value.\<close>
lemma starfun_abs: "\N. ( *f* (\n. \f n\)) N = \( *f* f) N\"
by transfer (rule refl)
text \<open>The \<open>hyperpow\<close> function as a nonstandard extension of \<open>realpow\<close>.\<close>
lemma starfun_pow: "\N. ( *f* (\n. r ^ n)) N = hypreal_of_real r pow N"
by transfer (rule refl)
lemma starfun_pow2: "\N. ( *f* (\n. X n ^ m)) N = ( *f* X) N pow hypnat_of_nat m"
by transfer (rule refl)
lemma starfun_pow3: "\R. ( *f* (\r. r ^ n)) R = R pow hypnat_of_nat n"
by transfer (rule refl)
text \<open>The \<^term>\<open>hypreal_of_hypnat\<close> function as a nonstandard extension of
\<^term>\<open>real_of_nat\<close>.\<close>
lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
by transfer (simp add: fun_eq_iff)
lemma starfun_inverse_real_of_nat_eq:
"N \ HNatInfinite \ ( *f* (\x::nat. inverse (real x))) N = inverse (hypreal_of_hypnat N)"
by (metis of_hypnat_def starfun_inverse2)
text \<open>Internal functions -- some redundancy with \<open>*f*\<close> now.\<close>
lemma starfun_n: "( *fn* f) (star_n X) = star_n (\n. f n (X n))"
by (simp add: starfun_n_def Ifun_star_n)
text \<open>Multiplication: \<open>( *fn) x ( *gn) = *(fn x gn)\<close>\<close>
lemma starfun_n_mult: "( *fn* f) z * ( *fn* g) z = ( *fn* (\i x. f i x * g i x)) z"
by (cases z) (simp add: starfun_n star_n_mult)
text \<open>Addition: \<open>( *fn) + ( *gn) = *(fn + gn)\<close>\<close>
lemma starfun_n_add: "( *fn* f) z + ( *fn* g) z = ( *fn* (\i x. f i x + g i x)) z"
by (cases z) (simp add: starfun_n star_n_add)
text \<open>Subtraction: \<open>( *fn) - ( *gn) = *(fn + - gn)\<close>\<close>
lemma starfun_n_add_minus: "( *fn* f) z + -( *fn* g) z = ( *fn* (\i x. f i x + -g i x)) z"
by (cases z) (simp add: starfun_n star_n_minus star_n_add)
text \<open>Composition: \<open>( *fn) \<circ> ( *gn) = *(fn \<circ> gn)\<close>\<close>
lemma starfun_n_const_fun [simp]: "( *fn* (\i x. k)) z = star_of k"
by (cases z) (simp add: starfun_n star_of_def)
lemma starfun_n_minus: "- ( *fn* f) x = ( *fn* (\i x. - (f i) x)) x"
by (cases x) (simp add: starfun_n star_n_minus)
lemma starfun_n_eq [simp]: "( *fn* f) (star_of n) = star_n (\i. f i n)"
by (simp add: starfun_n star_of_def)
lemma starfun_eq_iff: "(( *f* f) = ( *f* g)) \ f = g"
by transfer (rule refl)
lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
"N \ HNatInfinite \ ( *f* (\x. inverse (real x))) N \ Infinitesimal"
using starfun_inverse_real_of_nat_eq by auto
subsection \<open>Nonstandard Characterization of Induction\<close>
lemma hypnat_induct_obj:
"\n. (( *p* P) (0::hypnat) \ (\n. ( *p* P) n \ ( *p* P) (n + 1))) \ ( *p* P) n"
by transfer (induct_tac n, auto)
lemma hypnat_induct:
"\n. ( *p* P) (0::hypnat) \ (\n. ( *p* P) n \ ( *p* P) (n + 1)) \ ( *p* P) n"
by transfer (induct_tac n, auto)
lemma starP2_eq_iff: "( *p2* (=)) = (=)"
by transfer (rule refl)
lemma starP2_eq_iff2: "( *p2* (\x y. x = y)) X Y \ X = Y"
by (simp add: starP2_eq_iff)
lemma nonempty_set_star_has_least_lemma:
"\n\S. \m\S. n \ m" if "S \ {}" for S :: "nat set"
proof
show "\m\S. (LEAST n. n \ S) \ m"
by (simp add: Least_le)
show "(LEAST n. n \ S) \ S"
by (meson that LeastI_ex equals0I)
qed
lemma nonempty_set_star_has_least:
"\S::nat set star. Iset S \ {} \ \n \ Iset S. \m \ Iset S. n \ m"
using nonempty_set_star_has_least_lemma by (transfer empty_def)
lemma nonempty_InternalNatSet_has_least: "S \ InternalSets \ S \ {} \ \n \ S. \m \ S. n \ m"
for S :: "hypnat set"
by (force simp add: InternalSets_def starset_n_def dest!: nonempty_set_star_has_least)
text \<open>Goldblatt, page 129 Thm 11.3.2.\<close>
lemma internal_induct_lemma:
"\X::nat set star.
(0::hypnat) \<in> Iset X \<Longrightarrow> \<forall>n. n \<in> Iset X \<longrightarrow> n + 1 \<in> Iset X \<Longrightarrow> Iset X = (UNIV:: hypnat set)"
apply (transfer UNIV_def)
apply (rule equalityI [OF subset_UNIV subsetI])
apply (induct_tac x, auto)
done
lemma internal_induct:
"X \ InternalSets \ (0::hypnat) \ X \ \n. n \ X \ n + 1 \ X \ X = (UNIV:: hypnat set)"
apply (clarsimp simp add: InternalSets_def starset_n_def)
apply (erule (1) internal_induct_lemma)
done
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
