--- a/src/HOL/Nonstandard_Analysis/NatStar.thy Mon Oct 31 16:26:36 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/NatStar.thy Tue Nov 01 00:44:24 2016 +0100
@@ -5,237 +5,198 @@
Converted to Isar and polished by lcp
*)
-section\<open>Star-transforms for the Hypernaturals\<close>
+section \<open>Star-transforms for the Hypernaturals\<close>
theory NatStar
-imports Star
+ 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)
+ by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
-lemma starset_n_Un: "*sn* (%n. (A n) Un (B n)) = *sn* A Un *sn* B"
-apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
-apply (rule_tac x=whn in spec, transfer, simp)
-done
+lemma starset_n_Un: "*sn* (\<lambda>n. (A n) \<union> (B n)) = *sn* A \<union> *sn* B"
+ apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
+ apply (rule_tac x=whn in spec, transfer, simp)
+ done
-lemma InternalSets_Un:
- "[| X \<in> InternalSets; Y \<in> InternalSets |]
- ==> (X Un Y) \<in> InternalSets"
-by (auto simp add: InternalSets_def starset_n_Un [symmetric])
+lemma InternalSets_Un: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<union> Y \<in> InternalSets"
+ by (auto simp add: InternalSets_def starset_n_Un [symmetric])
-lemma starset_n_Int:
- "*sn* (%n. (A n) Int (B n)) = *sn* A Int *sn* B"
-apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
-apply (rule_tac x=whn in spec, transfer, simp)
-done
+lemma starset_n_Int: "*sn* (\<lambda>n. A n \<inter> B n) = *sn* A \<inter> *sn* B"
+ apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
+ apply (rule_tac x=whn in spec, transfer, simp)
+ done
-lemma InternalSets_Int:
- "[| X \<in> InternalSets; Y \<in> InternalSets |]
- ==> (X Int Y) \<in> InternalSets"
-by (auto simp add: InternalSets_def starset_n_Int [symmetric])
+lemma InternalSets_Int: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<inter> Y \<in> InternalSets"
+ by (auto simp add: InternalSets_def starset_n_Int [symmetric])
-lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
-apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
-apply (rule_tac x=whn in spec, transfer, simp)
-done
+lemma starset_n_Compl: "*sn* ((\<lambda>n. - A n)) = - ( *sn* A)"
+ apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
+ apply (rule_tac x=whn in spec, transfer, simp)
+ done
-lemma InternalSets_Compl: "X \<in> InternalSets ==> -X \<in> InternalSets"
-by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
+lemma InternalSets_Compl: "X \<in> InternalSets \<Longrightarrow> - X \<in> 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"
-apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
-apply (rule_tac x=whn in spec, transfer, simp)
-done
+lemma starset_n_diff: "*sn* (\<lambda>n. (A n) - (B n)) = *sn* A - *sn* B"
+ apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
+ apply (rule_tac x=whn in spec, transfer, simp)
+ done
-lemma InternalSets_diff:
- "[| X \<in> InternalSets; Y \<in> InternalSets |]
- ==> (X - Y) \<in> InternalSets"
-by (auto simp add: InternalSets_def starset_n_diff [symmetric])
+lemma InternalSets_diff: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X - Y \<in> InternalSets"
+ by (auto simp add: InternalSets_def starset_n_diff [symmetric])
lemma NatStar_SHNat_subset: "Nats \<le> *s* (UNIV:: nat set)"
-by simp
+ by simp
-lemma NatStar_hypreal_of_real_Int:
- "*s* X Int Nats = hypnat_of_nat ` X"
-by (auto simp add: SHNat_eq)
+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 starset_starset_n_eq: "*s* X = *sn* (\<lambda>n. X)"
+ by (simp add: starset_n_starset)
lemma InternalSets_starset_n [simp]: "( *s* X) \<in> InternalSets"
-by (auto simp add: InternalSets_def starset_starset_n_eq)
+ by (auto simp add: InternalSets_def starset_starset_n_eq)
-lemma InternalSets_UNIV_diff:
- "X \<in> InternalSets ==> UNIV - X \<in> InternalSets"
-apply (subgoal_tac "UNIV - X = - X")
-by (auto intro: InternalSets_Compl)
+lemma InternalSets_UNIV_diff: "X \<in> InternalSets \<Longrightarrow> UNIV - X \<in> InternalSets"
+ apply (subgoal_tac "UNIV - X = - X")
+ apply (auto intro: InternalSets_Compl)
+ done
-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>
+subsection \<open>Nonstandard Extensions of Functions\<close>
-lemma starfun_le_mono:
- "\<forall>n. N \<le> n --> f n \<le> g n
- ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n \<le> ( *f* g) n"
-by transfer
+text \<open>Example of transfer of a property from reals to hyperreals
+ --- used for limit comparison of sequences.\<close>
+
+lemma starfun_le_mono: "\<forall>n. N \<le> n \<longrightarrow> f n \<le> g n \<Longrightarrow>
+ \<forall>n. hypnat_of_nat N \<le> n \<longrightarrow> ( *f* f) n \<le> ( *f* g) n"
+ by transfer
-(*****----- and another -----*****)
+text \<open>And another:\<close>
lemma starfun_less_mono:
- "\<forall>n. N \<le> n --> f n < g n
- ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n < ( *f* g) n"
-by transfer
+ "\<forall>n. N \<le> n \<longrightarrow> f n < g n \<Longrightarrow> \<forall>n. hypnat_of_nat N \<le> n \<longrightarrow> ( *f* f) n < ( *f* g) n"
+ by transfer
-text\<open>Nonstandard extension when we increment the argument by one\<close>
+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)
+lemma starfun_shift_one: "\<And>N. ( *f* (\<lambda>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. \<bar>f n\<bar>)) N = \<bar>( *f* f) N\<bar>"
-by (transfer, rule refl)
+text \<open>Nonstandard extension with absolute value.\<close>
+lemma starfun_abs: "\<And>N. ( *f* (\<lambda>n. \<bar>f n\<bar>)) N = \<bar>( *f* f) N\<bar>"
+ by transfer (rule refl)
-text\<open>The hyperpow function as a nonstandard extension of realpow\<close>
-
-lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
-by (transfer, rule refl)
+text \<open>The \<open>hyperpow\<close> function as a nonstandard extension of \<open>realpow\<close>.\<close>
+lemma starfun_pow: "\<And>N. ( *f* (\<lambda>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_pow2: "\<And>N. ( *f* (\<lambda>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)
+lemma starfun_pow3: "\<And>R. ( *f* (\<lambda>r. r ^ n)) R = R pow hypnat_of_nat n"
+ by transfer (rule refl)
-text\<open>The @{term hypreal_of_hypnat} function as a nonstandard extension of
- @{term real_of_nat}\<close>
-
+text \<open>The @{term hypreal_of_hypnat} function as a nonstandard extension of
+ @{term real_of_nat}.\<close>
lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
-by transfer (simp add: fun_eq_iff)
+ by transfer (simp add: fun_eq_iff)
lemma starfun_inverse_real_of_nat_eq:
- "N \<in> HNatInfinite
- ==> ( *f* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)"
-apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
-apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
-apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat starfun_inverse_inverse)
-done
+ "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x::nat. inverse (real x))) N = inverse (hypreal_of_hypnat N)"
+ apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
+ apply (subgoal_tac "hypreal_of_hypnat N \<noteq> 0")
+ apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
+ done
-text\<open>Internal functions - some redundancy with *f* now\<close>
+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: "( *fn* f) (star_n X) = star_n (\<lambda>n. f n (X n))"
+ by (simp add: starfun_n_def Ifun_star_n)
-lemma starfun_n_mult:
- "( *fn* f) z * ( *fn* g) z = ( *fn* (% i x. f i x * g i x)) z"
-apply (cases z)
-apply (simp add: starfun_n star_n_mult)
-done
+text \<open>Multiplication: \<open>( *fn) x ( *gn) = *(fn x gn)\<close>\<close>
-text\<open>Addition: \<open>( *fn) + ( *gn) = *(fn + gn)\<close>\<close>
+lemma starfun_n_mult: "( *fn* f) z * ( *fn* g) z = ( *fn* (\<lambda>i x. f i x * g i x)) z"
+ by (cases z) (simp add: starfun_n star_n_mult)
-lemma starfun_n_add:
- "( *fn* f) z + ( *fn* g) z = ( *fn* (%i x. f i x + g i x)) z"
-apply (cases z)
-apply (simp add: starfun_n star_n_add)
-done
+text \<open>Addition: \<open>( *fn) + ( *gn) = *(fn + gn)\<close>\<close>
+lemma starfun_n_add: "( *fn* f) z + ( *fn* g) z = ( *fn* (\<lambda>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"
-apply (cases z)
-apply (simp add: starfun_n star_n_minus star_n_add)
-done
+text \<open>Subtraction: \<open>( *fn) - ( *gn) = *(fn + - gn)\<close>\<close>
+lemma starfun_n_add_minus: "( *fn* f) z + -( *fn* g) z = ( *fn* (\<lambda>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) o ( *gn) = *(fn o gn)\<close>\<close>
+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"
-apply (cases z)
-apply (simp add: starfun_n star_of_def)
-done
+lemma starfun_n_const_fun [simp]: "( *fn* (\<lambda>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"
-apply (cases x)
-apply (simp add: starfun_n star_n_minus)
-done
+lemma starfun_n_minus: "- ( *fn* f) x = ( *fn* (\<lambda>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_n_eq [simp]: "( *fn* f) (star_of n) = star_n (\<lambda>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 starfun_eq_iff: "(( *f* f) = ( *f* g)) \<longleftrightarrow> f = g"
+ by transfer (rule refl)
lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
- "N \<in> HNatInfinite ==> ( *f* (%x. inverse (real x))) N \<in> Infinitesimal"
-apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
-apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
-apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
-done
+ "N \<in> HNatInfinite \<Longrightarrow> ( *f* (%x. inverse (real x))) N \<in> Infinitesimal"
+ apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
+ apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
+ apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
+ done
-subsection\<open>Nonstandard Characterization of Induction\<close>
+subsection \<open>Nonstandard Characterization of Induction\<close>
lemma hypnat_induct_obj:
- "!!n. (( *p* P) (0::hypnat) &
- (\<forall>n. ( *p* P)(n) --> ( *p* P)(n + 1)))
- --> ( *p* P)(n)"
-by (transfer, induct_tac n, auto)
+ "\<And>n. (( *p* P) (0::hypnat) \<and> (\<forall>n. ( *p* P) n \<longrightarrow> ( *p* P) (n + 1))) \<longrightarrow> ( *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)
+ "\<And>n. ( *p* P) (0::hypnat) \<Longrightarrow> (\<And>n. ( *p* P) n \<Longrightarrow> ( *p* P) (n + 1)) \<Longrightarrow> ( *p* P) n"
+ by transfer (induct_tac n, auto)
lemma starP2_eq_iff: "( *p2* (op =)) = (op =)"
-by transfer (rule refl)
+ by transfer (rule refl)
-lemma starP2_eq_iff2: "( *p2* (%x y. x = y)) X Y = (X = Y)"
-by (simp add: starP2_eq_iff)
+lemma starP2_eq_iff2: "( *p2* (\<lambda>x y. x = y)) X Y \<longleftrightarrow> X = Y"
+ by (simp add: starP2_eq_iff)
-lemma nonempty_nat_set_Least_mem:
- "c \<in> (S :: nat set) ==> (LEAST n. n \<in> S) \<in> S"
-by (erule LeastI)
+lemma nonempty_nat_set_Least_mem: "c \<in> S \<Longrightarrow> (LEAST n. n \<in> S) \<in> S"
+ for S :: "nat set"
+ by (erule LeastI)
lemma nonempty_set_star_has_least:
- "!!S::nat set star. Iset S \<noteq> {} ==> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m"
-apply (transfer empty_def)
-apply (rule_tac x="LEAST n. n \<in> S" in bexI)
-apply (simp add: Least_le)
-apply (rule LeastI_ex, auto)
-done
+ "\<And>S::nat set star. Iset S \<noteq> {} \<Longrightarrow> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m"
+ apply (transfer empty_def)
+ apply (rule_tac x="LEAST n. n \<in> S" in bexI)
+ apply (simp add: Least_le)
+ apply (rule LeastI_ex, auto)
+ done
-lemma nonempty_InternalNatSet_has_least:
- "[| (S::hypnat set) \<in> InternalSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
-apply (clarsimp simp add: InternalSets_def starset_n_def)
-apply (erule nonempty_set_star_has_least)
-done
+lemma nonempty_InternalNatSet_has_least: "S \<in> InternalSets \<Longrightarrow> S \<noteq> {} \<Longrightarrow> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
+ for S :: "hypnat set"
+ apply (clarsimp simp add: InternalSets_def starset_n_def)
+ apply (erule nonempty_set_star_has_least)
+ done
-text\<open>Goldblatt page 129 Thm 11.3.2\<close>
+text \<open>Goldblatt, page 129 Thm 11.3.2.\<close>
lemma internal_induct_lemma:
- "!!X::nat set star. [| (0::hypnat) \<in> Iset X; \<forall>n. n \<in> Iset X --> n + 1 \<in> Iset X |]
- ==> Iset X = (UNIV:: hypnat set)"
-apply (transfer UNIV_def)
-apply (rule equalityI [OF subset_UNIV subsetI])
-apply (induct_tac x, auto)
-done
+ "\<And>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 \<in> InternalSets; (0::hypnat) \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |]
- ==> X = (UNIV:: hypnat set)"
-apply (clarsimp simp add: InternalSets_def starset_n_def)
-apply (erule (1) internal_induct_lemma)
-done
-
+ "X \<in> InternalSets \<Longrightarrow> (0::hypnat) \<in> X \<Longrightarrow> \<forall>n. n \<in> X \<longrightarrow> n + 1 \<in> X \<Longrightarrow> X = (UNIV:: hypnat set)"
+ apply (clarsimp simp add: InternalSets_def starset_n_def)
+ apply (erule (1) internal_induct_lemma)
+ done
end