--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Mon Aug 15 21:57:55 2022 +0100
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Tue Aug 16 10:39:44 2022 +0100
@@ -26,12 +26,17 @@
lemma dvd_by_all2: "\<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N"
for M :: nat
- apply (induct M)
- apply auto
- apply (rule_tac x = "N * Suc M" in exI)
- apply auto
- apply (metis dvdI dvd_add_times_triv_left_iff dvd_add_triv_right_iff dvd_refl dvd_trans le_Suc_eq mult_Suc_right)
- done
+proof (induct M)
+ case 0
+ then show ?case
+ by auto
+next
+ case (Suc M)
+ then obtain N where "N>0" and "\<And>m. 0 < m \<and> m \<le> M \<Longrightarrow> m dvd N"
+ by metis
+ then show ?case
+ by (metis nat_0_less_mult_iff zero_less_Suc dvd_mult dvd_mult2 dvd_refl le_Suc_eq)
+qed
lemma dvd_by_all: "\<forall>M::nat. \<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N"
using dvd_by_all2 by blast
@@ -40,22 +45,13 @@
by transfer simp
text \<open>Goldblatt: Exercise 5.11(2) -- p. 57.\<close>
-lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N \<and> (\<forall>m::hypnat. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N)"
+lemma hdvd_by_all [rule_format]: "\<forall>M. \<exists>N. 0 < N \<and> (\<forall>m::hypnat. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N)"
by transfer (rule dvd_by_all)
-lemmas hdvd_by_all2 = hdvd_by_all [THEN spec]
-
text \<open>Goldblatt: Exercise 5.11(2) -- p. 57.\<close>
lemma hypnat_dvd_all_hypnat_of_nat:
"\<exists>N::hypnat. 0 < N \<and> (\<forall>n \<in> - {0::nat}. hypnat_of_nat n dvd N)"
- apply (cut_tac hdvd_by_all)
- apply (drule_tac x = whn in spec)
- apply auto
- apply (rule exI)
- apply auto
- apply (drule_tac x = "hypnat_of_nat n" in spec)
- apply (auto simp add: linorder_not_less)
- done
+ by (metis Compl_iff gr0I hdvd_by_all hypnat_of_nat_le_whn singletonI star_of_0_less)
text \<open>The nonstandard extension of the set prime numbers consists of precisely
@@ -74,50 +70,12 @@
by (rule starset_finite)
-subsection \<open>Another characterization of infinite set of natural numbers\<close>
-
-lemma finite_nat_set_bounded: "finite N \<Longrightarrow> \<exists>n::nat. \<forall>i \<in> N. i < n"
- apply (erule_tac F = N in finite_induct)
- apply auto
- apply (rule_tac x = "Suc n + x" in exI)
- apply auto
- done
-
-lemma finite_nat_set_bounded_iff: "finite N \<longleftrightarrow> (\<exists>n::nat. \<forall>i \<in> N. i < n)"
- by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite)
-
-lemma not_finite_nat_set_iff: "\<not> finite N \<longleftrightarrow> (\<forall>n::nat. \<exists>i \<in> N. n \<le> i)"
- by (auto simp add: finite_nat_set_bounded_iff not_less)
-
-lemma bounded_nat_set_is_finite2: "\<forall>i::nat \<in> N. i \<le> n \<Longrightarrow> finite N"
- apply (rule finite_subset)
- apply (rule_tac [2] finite_atMost)
- apply auto
- done
-
-lemma finite_nat_set_bounded2: "finite N \<Longrightarrow> \<exists>n::nat. \<forall>i \<in> N. i \<le> n"
- apply (erule_tac F = N in finite_induct)
- apply auto
- apply (rule_tac x = "n + x" in exI)
- apply auto
- done
-
-lemma finite_nat_set_bounded_iff2: "finite N \<longleftrightarrow> (\<exists>n::nat. \<forall>i \<in> N. i \<le> n)"
- by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2)
-
-lemma not_finite_nat_set_iff2: "\<not> finite N \<longleftrightarrow> (\<forall>n::nat. \<exists>i \<in> N. n < i)"
- by (auto simp add: finite_nat_set_bounded_iff2 not_le)
-
subsection \<open>An injective function cannot define an embedded natural number\<close>
lemma lemma_infinite_set_singleton:
"\<forall>m n. m \<noteq> n \<longrightarrow> f n \<noteq> f m \<Longrightarrow> {n. f n = N} = {} \<or> (\<exists>m. {n. f n = N} = {m})"
- apply auto
- apply (drule_tac x = x in spec, auto)
- apply (subgoal_tac "\<forall>n. f n = f x \<longleftrightarrow> x = n")
- apply auto
- done
+ by (metis (mono_tags) is_singletonI' is_singleton_the_elem mem_Collect_eq)
lemma inj_fun_not_hypnat_in_SHNat:
fixes f :: "nat \<Rightarrow> nat"
@@ -143,10 +101,7 @@
qed
lemma range_subset_mem_starsetNat: "range f \<subseteq> A \<Longrightarrow> starfun f whn \<in> *s* A"
- apply (rule_tac x="whn" in spec)
- apply transfer
- apply auto
- done
+ by (metis STAR_subset_closed UNIV_I image_eqI starset_UNIV starset_image)
text \<open>
Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360.
@@ -162,68 +117,53 @@
by auto
lemma choicefun_mem_set [simp]: "E \<noteq> {} \<Longrightarrow> choicefun E \<in> E"
- apply (unfold choicefun_def)
- apply (rule lemmaPow3 [THEN someI2_ex], auto)
- done
+ unfolding choicefun_def
+ by (force intro: lemmaPow3 [THEN someI2_ex])
lemma injf_max_mem_set: "E \<noteq>{} \<Longrightarrow> \<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> injf_max n E \<in> E"
- apply (induct n)
- apply force
- apply (simp add: choicefun_def)
- apply (rule lemmaPow3 [THEN someI2_ex], auto)
- done
+proof (induct n)
+ case 0
+ then show ?case by force
+next
+ case (Suc n)
+ then show ?case
+ apply (simp add: choicefun_def)
+ apply (rule lemmaPow3 [THEN someI2_ex], auto)
+ done
+qed
lemma injf_max_order_preserving: "\<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> injf_max n E < injf_max (Suc n) E"
- apply (simp add: choicefun_def)
- apply (rule lemmaPow3 [THEN someI2_ex])
- apply auto
- done
+ by (metis (no_types, lifting) choicefun_mem_set empty_iff injf_max.simps(2) mem_Collect_eq)
-lemma injf_max_order_preserving2: "\<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> \<forall>n m. m < n \<longrightarrow> injf_max m E < injf_max n E"
- apply (rule allI)
- apply (induct_tac n)
- apply auto
- apply (simp add: choicefun_def)
- apply (rule lemmaPow3 [THEN someI2_ex])
- apply (auto simp add: less_Suc_eq)
- apply (drule_tac x = m in spec)
- apply (drule subsetD)
- apply auto
- done
+lemma injf_max_order_preserving2:
+ assumes "m < n" and E: "\<forall>x. \<exists>y \<in> E. x < y"
+ shows "injf_max m E < injf_max n E"
+ using \<open>m < n\<close>
+proof (induction n arbitrary: m)
+ case 0 then show ?case by auto
+next
+ case (Suc n)
+ then show ?case
+ by (metis E injf_max_order_preserving less_Suc_eq order_less_trans)
+qed
+
lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> inj (\<lambda>n. injf_max n E)"
- apply (rule inj_onI)
- apply (rule ccontr)
- apply auto
- apply (drule injf_max_order_preserving2)
- apply (metis antisym_conv3 order_less_le)
- done
+ by (metis injf_max_order_preserving2 linorder_injI order_less_irrefl)
lemma infinite_set_has_order_preserving_inj:
"E \<noteq> {} \<Longrightarrow> \<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> \<exists>f. range f \<subseteq> E \<and> inj f \<and> (\<forall>m. f m < f (Suc m))"
for E :: "'a::order set" and f :: "nat \<Rightarrow> 'a"
- apply (rule_tac x = "\<lambda>n. injf_max n E" in exI)
- apply safe
- apply (rule injf_max_mem_set)
- apply (rule_tac [3] inj_injf_max)
- apply (rule_tac [4] injf_max_order_preserving)
- apply auto
- done
+ by (metis image_subsetI inj_injf_max injf_max_mem_set injf_max_order_preserving)
text \<open>Only need the existence of an injective function from \<open>N\<close> to \<open>A\<close> for proof.\<close>
-lemma hypnat_infinite_has_nonstandard: "\<not> finite A \<Longrightarrow> hypnat_of_nat ` A < ( *s* A)"
- apply auto
- apply (subgoal_tac "A \<noteq> {}")
- prefer 2 apply force
- apply (drule infinite_set_has_order_preserving_inj)
- apply (erule not_finite_nat_set_iff2 [THEN iffD1])
- apply auto
- apply (drule inj_fun_not_hypnat_in_SHNat)
- apply (drule range_subset_mem_starsetNat)
- apply (auto simp add: SHNat_eq)
- done
+lemma hypnat_infinite_has_nonstandard:
+ assumes "infinite A"
+ shows "hypnat_of_nat ` A < ( *s* A)"
+ by (metis assms IntE NatStar_hypreal_of_real_Int STAR_star_of_image_subset psubsetI
+ infinite_iff_countable_subset inj_fun_not_hypnat_in_SHNat range_subset_mem_starsetNat)
lemma starsetNat_eq_hypnat_of_nat_image_finite: "*s* A = hypnat_of_nat ` A \<Longrightarrow> finite A"
by (metis hypnat_infinite_has_nonstandard less_irrefl)
@@ -231,24 +171,19 @@
lemma finite_starsetNat_iff: "*s* A = hypnat_of_nat ` A \<longleftrightarrow> finite A"
by (blast intro!: starsetNat_eq_hypnat_of_nat_image_finite NatStar_hypnat_of_nat)
-lemma hypnat_infinite_has_nonstandard_iff: "\<not> finite A \<longleftrightarrow> hypnat_of_nat ` A < *s* A"
- apply (rule iffI)
- apply (blast intro!: hypnat_infinite_has_nonstandard)
- apply (auto simp add: finite_starsetNat_iff [symmetric])
- done
+lemma hypnat_infinite_has_nonstandard_iff: "infinite A \<longleftrightarrow> hypnat_of_nat ` A < *s* A"
+ by (metis finite_starsetNat_iff hypnat_infinite_has_nonstandard nless_le)
subsection \<open>Existence of Infinitely Many Primes: a Nonstandard Proof\<close>
-lemma lemma_not_dvd_hypnat_one [simp]: "\<not> (\<forall>n \<in> - {0}. hypnat_of_nat n dvd 1)"
- apply auto
- apply (rule_tac x = 2 in bexI)
- apply transfer
- apply auto
- done
-
-lemma lemma_not_dvd_hypnat_one2 [simp]: "\<exists>n \<in> - {0}. \<not> hypnat_of_nat n dvd 1"
- using lemma_not_dvd_hypnat_one by (auto simp del: lemma_not_dvd_hypnat_one)
+lemma lemma_not_dvd_hypnat_one [simp]: "\<exists>n \<in> - {0}. \<not> hypnat_of_nat n dvd 1"
+proof -
+ have "\<not> hypnat_of_nat 2 dvd 1"
+ by transfer auto
+ then show ?thesis
+ by (metis ComplI singletonD zero_neq_numeral)
+qed
lemma hypnat_add_one_gt_one: "\<And>N::hypnat. 0 < N \<Longrightarrow> 1 < N + 1"
by transfer simp
@@ -272,17 +207,16 @@
by transfer simp
text \<open>Already proved as \<open>primes_infinite\<close>, but now using non-standard naturals.\<close>
-theorem not_finite_prime: "\<not> finite {p::nat. prime p}"
- apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
- using hypnat_dvd_all_hypnat_of_nat
- apply clarify
- apply (drule hypnat_add_one_gt_one)
- apply (drule hyperprime_factor_exists)
- apply clarify
- apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
- apply (force simp: starprime_def)
- apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime
- imageE insert_iff mem_Collect_eq not_prime_0)
- done
+theorem not_finite_prime: "infinite {p::nat. prime p}"
+proof -
+ obtain N k where N: "\<forall>n\<in>- {0}. hypnat_of_nat n dvd N" "k\<in>starprime" "k dvd N + 1"
+ by (meson hyperprime_factor_exists hypnat_add_one_gt_one hypnat_dvd_all_hypnat_of_nat)
+ then have "k \<noteq> 1"
+ using \<open>k \<in> starprime\<close> by force
+ then have "k \<notin> hypnat_of_nat ` {p. prime p}"
+ using N dvd_add_right_iff hdvd_one_eq_one not_prime_0 by blast
+ then show ?thesis
+ by (metis \<open>k \<in> starprime\<close> finite_starsetNat_iff starprime_def)
+qed
end