# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1660642784 -3600
# Node ID d7595b12b9ea7f41de025a7b515cd79447082e4f
# Parent  9eeed5c424f9a7c55a29f4b8a070b53a8d7a1ec2
Cleanup of NonstandardAnalysis

diff -r 9eeed5c424f9 -r d7595b12b9ea src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
--- 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