--- a/src/HOL/Nonstandard_Analysis/HyperNat.thy Tue Apr 30 15:49:15 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy Tue Apr 30 17:03:32 2019 +0100
@@ -154,12 +154,14 @@
lemma hypnat_of_nat_Suc [simp]: "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1"
by transfer simp
-lemma of_nat_eq_add [rule_format]: "\<forall>d::hypnat. of_nat m = of_nat n + d \<longrightarrow> d \<in> range of_nat"
- apply (induct n)
- apply (auto simp add: add.assoc)
- apply (case_tac x)
- apply (auto simp add: add.commute [of 1])
- done
+lemma of_nat_eq_add:
+ fixes d::hypnat
+ shows "of_nat m = of_nat n + d \<Longrightarrow> d \<in> range of_nat"
+proof (induct n arbitrary: d)
+ case (Suc n)
+ then show ?case
+ by (metis Nats_def Nats_eq_Standard Standard_simps(4) hypnat_diff_add_inverse of_nat_in_Nats)
+qed auto
lemma Nats_diff [simp]: "a \<in> Nats \<Longrightarrow> b \<in> Nats \<Longrightarrow> a - b \<in> Nats" for a b :: hypnat
by (simp add: Nats_eq_Standard)
@@ -224,37 +226,22 @@
by (simp add: HNatInfinite_def)
lemma Nats_downward_closed: "x \<in> Nats \<Longrightarrow> y \<le> x \<Longrightarrow> y \<in> Nats" for x y :: hypnat
- apply (simp only: linorder_not_less [symmetric])
- apply (erule contrapos_np)
- apply (drule HNatInfinite_not_Nats_iff [THEN iffD2])
- apply (erule (1) Nats_less_HNatInfinite)
- done
+ using HNatInfinite_not_Nats_iff Nats_le_HNatInfinite by fastforce
lemma HNatInfinite_upward_closed: "x \<in> HNatInfinite \<Longrightarrow> x \<le> y \<Longrightarrow> y \<in> HNatInfinite"
- apply (simp only: HNatInfinite_not_Nats_iff)
- apply (erule contrapos_nn)
- apply (erule (1) Nats_downward_closed)
- done
+ using HNatInfinite_not_Nats_iff Nats_downward_closed by blast
lemma HNatInfinite_add: "x \<in> HNatInfinite \<Longrightarrow> x + y \<in> HNatInfinite"
- apply (erule HNatInfinite_upward_closed)
- apply (rule hypnat_le_add1)
- done
+ using HNatInfinite_upward_closed hypnat_le_add1 by blast
lemma HNatInfinite_add_one: "x \<in> HNatInfinite \<Longrightarrow> x + 1 \<in> HNatInfinite"
by (rule HNatInfinite_add)
-lemma HNatInfinite_diff: "x \<in> HNatInfinite \<Longrightarrow> y \<in> Nats \<Longrightarrow> x - y \<in> HNatInfinite"
- apply (frule (1) Nats_le_HNatInfinite)
- apply (simp only: HNatInfinite_not_Nats_iff)
- apply (erule contrapos_nn)
- apply (drule (1) Nats_add, simp)
- done
+lemma HNatInfinite_diff: "\<lbrakk>x \<in> HNatInfinite; y \<in> Nats\<rbrakk> \<Longrightarrow> x - y \<in> HNatInfinite"
+ by (metis HNatInfinite_not_Nats_iff Nats_add Nats_le_HNatInfinite le_add_diff_inverse)
lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite \<Longrightarrow> \<exists>y. x = y + 1" for x :: hypnat
- apply (rule_tac x = "x - (1::hypnat) " in exI)
- apply (simp add: Nats_le_HNatInfinite)
- done
+ using hypnat_gt_zero_iff2 zero_less_HNatInfinite by blast
subsection \<open>Existence of an infinite hypernatural number\<close>
@@ -308,32 +295,29 @@
text \<open>\<^term>\<open>HNatInfinite = {N. \<forall>n \<in> Nats. n < N}\<close>\<close>
-(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
-lemma HNatInfinite_FreeUltrafilterNat_lemma:
- assumes "\<forall>N::nat. eventually (\<lambda>n. f n \<noteq> N) \<U>"
- shows "eventually (\<lambda>n. N < f n) \<U>"
- apply (induct N)
- using assms
- apply (drule_tac x = 0 in spec, simp)
- using assms
- apply (drule_tac x = "Suc N" in spec)
- apply (auto elim: eventually_elim2)
- done
+text\<open>unused, but possibly interesting\<close>
+lemma HNatInfinite_FreeUltrafilterNat_eventually:
+ assumes "\<And>k::nat. eventually (\<lambda>n. f n \<noteq> k) \<U>"
+ shows "eventually (\<lambda>n. m < f n) \<U>"
+proof (induct m)
+ case 0
+ then show ?case
+ using assms eventually_mono by fastforce
+next
+ case (Suc m)
+ then show ?case
+ using assms [of "Suc m"] eventually_elim2 by fastforce
+qed
lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
- apply (safe intro!: Nats_less_HNatInfinite)
- apply (auto simp add: HNatInfinite_def)
- done
+ using HNatInfinite_def Nats_less_HNatInfinite by auto
subsubsection \<open>Alternative Characterization of \<^term>\<open>HNatInfinite\<close> using Free Ultrafilter\<close>
lemma HNatInfinite_FreeUltrafilterNat:
"star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) \<U>"
- apply (auto simp add: HNatInfinite_iff SHNat_eq)
- apply (drule_tac x="star_of u" in spec, simp)
- apply (simp add: star_of_def star_less_def starP2_star_n)
- done
+ by (metis (full_types) starP2_star_of starP_star_n star_less_def star_of_less_HNatInfinite)
lemma FreeUltrafilterNat_HNatInfinite:
"\<forall>u. eventually (\<lambda>n. u < X n) \<U> \<Longrightarrow> star_n X \<in> HNatInfinite"
--- a/src/HOL/Nonstandard_Analysis/NatStar.thy Tue Apr 30 15:49:15 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/NatStar.thy Tue Apr 30 17:03:32 2019 +0100
@@ -15,33 +15,49 @@
by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
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
+proof -
+ have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<or> x \<in> 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 \<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* (\<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
+proof -
+ have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<and> x \<in> 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 \<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* ((\<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
+proof -
+ have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<notin> 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 \<in> InternalSets \<Longrightarrow> - X \<in> InternalSets"
by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
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
+proof -
+ have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<and> x \<notin> 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 \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X - Y \<in> InternalSets"
by (auto simp add: InternalSets_def starset_n_diff [symmetric])
@@ -59,9 +75,7 @@
by (auto simp add: InternalSets_def starset_starset_n_eq)
lemma InternalSets_UNIV_diff: "X \<in> InternalSets \<Longrightarrow> UNIV - X \<in> InternalSets"
- apply (subgoal_tac "UNIV - X = - X")
- apply (auto intro: InternalSets_Compl)
- done
+ by (simp add: InternalSets_Compl diff_eq)
subsection \<open>Nonstandard Extensions of Functions\<close>
@@ -104,10 +118,7 @@
lemma starfun_inverse_real_of_nat_eq:
"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
+ by (metis of_hypnat_def starfun_inverse2)
text \<open>Internal functions -- some redundancy with \<open>*f*\<close> now.\<close>
@@ -144,10 +155,7 @@
lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
"N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. inverse (real x))) N \<in> Infinitesimal"
- 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
+ using starfun_inverse_real_of_nat_eq by auto
subsection \<open>Nonstandard Characterization of Induction\<close>
@@ -166,23 +174,22 @@
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 \<Longrightarrow> (LEAST n. n \<in> S) \<in> S"
- for S :: "nat set"
- by (erule LeastI)
+lemma nonempty_set_star_has_least_lemma:
+ "\<exists>n\<in>S. \<forall>m\<in>S. n \<le> m" if "S \<noteq> {}" for S :: "nat set"
+proof
+ show "\<forall>m\<in>S. (LEAST n. n \<in> S) \<le> m"
+ by (simp add: Least_le)
+ show "(LEAST n. n \<in> S) \<in> S"
+ by (meson that LeastI_ex equals0I)
+qed
lemma nonempty_set_star_has_least:
"\<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
+ using nonempty_set_star_has_least_lemma by (transfer empty_def)
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
+ 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:
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Tue Apr 30 15:49:15 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Tue Apr 30 17:03:32 2019 +0100
@@ -14,11 +14,8 @@
where "\<U> = (SOME U. freeultrafilter U)"
lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
- apply (unfold FreeUltrafilterNat_def)
- apply (rule someI_ex)
- apply (rule freeultrafilter_Ex)
- apply (rule infinite_UNIV_nat)
- done
+ unfolding FreeUltrafilterNat_def
+ by (simp add: freeultrafilter_Ex someI_ex)
interpretation FreeUltrafilterNat: freeultrafilter \<U>
by (rule freeultrafilter_FreeUltrafilterNat)
@@ -42,16 +39,10 @@
by (cases x) (auto simp: star_n_def star_def elim: quotientE)
lemma all_star_eq: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>X. P (star_n X))"
- apply auto
- apply (rule_tac x = x in star_cases)
- apply simp
- done
+ by (metis star_cases)
lemma ex_star_eq: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>X. P (star_n X))"
- apply auto
- apply (rule_tac x=x in star_cases)
- apply auto
- done
+ by (metis star_cases)
text \<open>Proving that \<^term>\<open>starrel\<close> is an equivalence relation.\<close>
@@ -599,12 +590,16 @@
subsection \<open>Ordering and lattice classes\<close>
instance star :: (order) order
- apply intro_classes
- apply (transfer, rule less_le_not_le)
- apply (transfer, rule order_refl)
- apply (transfer, erule (1) order_trans)
- apply (transfer, erule (1) order_antisym)
- done
+proof
+ show "\<And>x y::'a star. (x < y) = (x \<le> y \<and> \<not> y \<le> x)"
+ by transfer (rule less_le_not_le)
+ show "\<And>x::'a star. x \<le> x"
+ by transfer (rule order_refl)
+ show "\<And>x y z::'a star. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z"
+ by transfer (rule order_trans)
+ show "\<And>x y::'a star. \<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y"
+ by transfer (rule order_antisym)
+qed
instantiation star :: (semilattice_inf) semilattice_inf
begin
@@ -639,16 +634,12 @@
by (intro_classes, transfer, rule linorder_linear)
lemma star_max_def [transfer_unfold]: "max = *f2* max"
- apply (rule ext, rule ext)
- apply (unfold max_def, transfer, fold max_def)
- apply (rule refl)
- done
+ unfolding max_def
+ by (intro ext, transfer, simp)
lemma star_min_def [transfer_unfold]: "min = *f2* min"
- apply (rule ext, rule ext)
- apply (unfold min_def, transfer, fold min_def)
- apply (rule refl)
- done
+ unfolding min_def
+ by (intro ext, transfer, simp)
lemma Standard_max [simp]: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> max x y \<in> Standard"
by (simp add: star_max_def)
@@ -928,10 +919,9 @@
by (erule finite_induct) simp_all
instance star :: (finite) finite
- apply intro_classes
- apply (subst starset_UNIV [symmetric])
- apply (subst starset_finite [OF finite])
- apply (rule finite_imageI [OF finite])
- done
+proof intro_classes
+ show "finite (UNIV::'a star set)"
+ by (metis starset_UNIV finite finite_imageI starset_finite)
+qed
end