# HG changeset patch
# User wenzelm
# Date 1482087684 -3600
# Node ID 37ce6ceacbb7359db08c3ae91806e95c75adf9a3
# Parent  86e2f2208a5820ba89e01905c1e5c2b6a706a6b7
misc tuning and modernization;

diff -r 86e2f2208a58 -r 37ce6ceacbb7 src/HOL/Nonstandard_Analysis/CLim.thy
--- a/src/HOL/Nonstandard_Analysis/CLim.thy	Sun Dec 18 16:13:20 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/CLim.thy	Sun Dec 18 20:01:24 2016 +0100
@@ -4,198 +4,178 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-section\<open>Limits, Continuity and Differentiation for Complex Functions\<close>
+section \<open>Limits, Continuity and Differentiation for Complex Functions\<close>
 
 theory CLim
-imports CStar
+  imports CStar
 begin
 
 (*not in simpset?*)
 declare hypreal_epsilon_not_zero [simp]
 
 (*??generalize*)
-lemma lemma_complex_mult_inverse_squared [simp]:
-     "x \<noteq> (0::complex) \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
-by (simp add: numeral_2_eq_2)
+lemma lemma_complex_mult_inverse_squared [simp]: "x \<noteq> 0 \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
+  for x :: complex
+  by (simp add: numeral_2_eq_2)
+
+text \<open>Changing the quantified variable. Install earlier?\<close>
+lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) \<longleftrightarrow> (\<forall>x. P (x - a))"
+  apply auto
+  apply (drule_tac x = "x + a" in spec)
+  apply (simp add: add.assoc)
+  done
 
-text\<open>Changing the quantified variable. Install earlier?\<close>
-lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"
-apply auto 
-apply (drule_tac x="x+a" in spec) 
-apply (simp add: add.assoc) 
-done
+lemma complex_add_minus_iff [simp]: "x + - a = 0 \<longleftrightarrow> x = a"
+  for x a :: complex
+  by (simp add: diff_eq_eq)
 
-lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)"
-by (simp add: diff_eq_eq)
-
-lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)"
-apply auto
-apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto)
-done
+lemma complex_add_eq_0_iff [iff]: "x + y = 0 \<longleftrightarrow> y = - x"
+  for x y :: complex
+  apply auto
+  apply (drule sym [THEN diff_eq_eq [THEN iffD2]])
+  apply auto
+  done
 
 
-subsection\<open>Limit of Complex to Complex Function\<close>
+subsection \<open>Limit of Complex to Complex Function\<close>
+
+lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re L"
+  by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)
 
-lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L)"
-by (simp add: NSLIM_def starfunC_approx_Re_Im_iff 
-              hRe_hcomplex_of_complex)
+lemma NSLIM_Im: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> (\<lambda>x. Im (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im L"
+  by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hIm_hcomplex_of_complex)
 
-lemma NSLIM_Im: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L)"
-by (simp add: NSLIM_def starfunC_approx_Re_Im_iff 
-              hIm_hcomplex_of_complex)
+lemma LIM_Re: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow> Re L"
+  for f :: "'a::real_normed_vector \<Rightarrow> complex"
+  by (simp add: LIM_NSLIM_iff NSLIM_Re)
 
-(** get this result easily now **)
-lemma LIM_Re:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "f \<midarrow>a\<rightarrow> L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow> Re(L)"
-by (simp add: LIM_NSLIM_iff NSLIM_Re)
+lemma LIM_Im: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. Im (f x)) \<midarrow>a\<rightarrow> Im L"
+  for f :: "'a::real_normed_vector \<Rightarrow> complex"
+  by (simp add: LIM_NSLIM_iff NSLIM_Im)
 
-lemma LIM_Im:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "f \<midarrow>a\<rightarrow> L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow> Im(L)"
-by (simp add: LIM_NSLIM_iff NSLIM_Im)
+lemma LIM_cnj: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L"
+  for f :: "'a::real_normed_vector \<Rightarrow> complex"
+  by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
 
-lemma LIM_cnj:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "f \<midarrow>a\<rightarrow> L ==> (%x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L"
-by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
-
-lemma LIM_cnj_iff:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "((%x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L) = (f \<midarrow>a\<rightarrow> L)"
-by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
+lemma LIM_cnj_iff: "((\<lambda>x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L) \<longleftrightarrow> f \<midarrow>a\<rightarrow> L"
+  for f :: "'a::real_normed_vector \<Rightarrow> complex"
+  by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
 
 lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
-by transfer (rule refl)
+  by transfer (rule refl)
 
 lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
-by transfer (rule refl)
+  by transfer (rule refl)
 
 lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)"
-by transfer (rule refl)
+  by transfer (rule refl)
 
-text""
-(** another equivalence result **)
-lemma NSCLIM_NSCRLIM_iff:
-   "(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)"
-by (simp add: NSLIM_def starfun_norm
-    approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
+text \<open>Another equivalence result.\<close>
+lemma NSCLIM_NSCRLIM_iff: "f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<lambda>y. cmod (f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0"
+  by (simp add: NSLIM_def starfun_norm
+      approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
 
-(** much, much easier standard proof **)
-lemma CLIM_CRLIM_iff:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "(f \<midarrow>x\<rightarrow> L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow> 0)"
-by (simp add: LIM_eq)
+text \<open>Much, much easier standard proof.\<close>
+lemma CLIM_CRLIM_iff: "f \<midarrow>x\<rightarrow> L \<longleftrightarrow> (\<lambda>y. cmod (f y - L)) \<midarrow>x\<rightarrow> 0"
+  for f :: "'a::real_normed_vector \<Rightarrow> complex"
+  by (simp add: LIM_eq)
 
-(* so this is nicer nonstandard proof *)
-lemma NSCLIM_NSCRLIM_iff2:
-     "(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)"
-by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
+text \<open>So this is nicer nonstandard proof.\<close>
+lemma NSCLIM_NSCRLIM_iff2: "f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<lambda>y. cmod (f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0"
+  by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
 
 lemma NSLIM_NSCRLIM_Re_Im_iff:
-     "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L) &
-                            (%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L))"
-apply (auto intro: NSLIM_Re NSLIM_Im)
-apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
-apply (auto dest!: spec)
-apply (simp add: hcomplex_approx_iff)
-done
+  "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re L \<and> (\<lambda>x. Im (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im L"
+  apply (auto intro: NSLIM_Re NSLIM_Im)
+  apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
+  apply (auto dest!: spec)
+  apply (simp add: hcomplex_approx_iff)
+  done
+
+lemma LIM_CRLIM_Re_Im_iff: "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow> Re L \<and> (\<lambda>x. Im (f x)) \<midarrow>a\<rightarrow> Im L"
+  for f :: "'a::real_normed_vector \<Rightarrow> complex"
+  by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
+
+
+subsection \<open>Continuity\<close>
+
+lemma NSLIM_isContc_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a"
+  by (rule NSLIM_h_iff)
 
-lemma LIM_CRLIM_Re_Im_iff:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "(f \<midarrow>a\<rightarrow> L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow> Re(L) &
-                         (%x. Im(f x)) \<midarrow>a\<rightarrow> Im(L))"
-by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
+
+subsection \<open>Functions from Complex to Reals\<close>
+
+lemma isNSContCR_cmod [simp]: "isNSCont cmod a"
+  by (auto intro: approx_hnorm
+      simp: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] isNSCont_def)
+
+lemma isContCR_cmod [simp]: "isCont cmod a"
+  by (simp add: isNSCont_isCont_iff [symmetric])
+
+lemma isCont_Re: "isCont f a \<Longrightarrow> isCont (\<lambda>x. Re (f x)) a"
+  for f :: "'a::real_normed_vector \<Rightarrow> complex"
+  by (simp add: isCont_def LIM_Re)
+
+lemma isCont_Im: "isCont f a \<Longrightarrow> isCont (\<lambda>x. Im (f x)) a"
+  for f :: "'a::real_normed_vector \<Rightarrow> complex"
+  by (simp add: isCont_def LIM_Im)
 
 
-subsection\<open>Continuity\<close>
-
-lemma NSLIM_isContc_iff:
-     "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
-by (rule NSLIM_h_iff)
-
-subsection\<open>Functions from Complex to Reals\<close>
-
-lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)"
-by (auto intro: approx_hnorm
-         simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] 
-                    isNSCont_def)
+subsection \<open>Differentiation of Natural Number Powers\<close>
 
-lemma isContCR_cmod [simp]: "isCont cmod (a)"
-by (simp add: isNSCont_isCont_iff [symmetric])
-
-lemma isCont_Re:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "isCont f a ==> isCont (%x. Re (f x)) a"
-by (simp add: isCont_def LIM_Re)
-
-lemma isCont_Im:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "isCont f a ==> isCont (%x. Im (f x)) a"
-by (simp add: isCont_def LIM_Im)
+lemma CDERIV_pow [simp]: "DERIV (\<lambda>x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - Suc 0))"
+  apply (induct n)
+   apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
+   apply (auto simp add: distrib_right of_nat_Suc)
+  apply (case_tac "n")
+   apply (auto simp add: ac_simps)
+  done
 
-subsection\<open>Differentiation of Natural Number Powers\<close>
-
-lemma CDERIV_pow [simp]:
-     "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
-apply (induct n)
-apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
-apply (auto simp add: distrib_right of_nat_Suc)
-apply (case_tac "n")
-apply (auto simp add: ac_simps)
-done
+text \<open>Nonstandard version.\<close>
+lemma NSCDERIV_pow: "NSDERIV (\<lambda>x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
+  by (metis CDERIV_pow NSDERIV_DERIV_iff One_nat_def)
 
-text\<open>Nonstandard version\<close>
-lemma NSCDERIV_pow: "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
-    by (metis CDERIV_pow NSDERIV_DERIV_iff One_nat_def)
+text \<open>Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero.\<close>
+lemma NSCDERIV_inverse: "x \<noteq> 0 \<Longrightarrow> NSDERIV (\<lambda>x. inverse x) x :> - (inverse x)\<^sup>2"
+  for x :: complex
+  unfolding numeral_2_eq_2 by (rule NSDERIV_inverse)
 
-text\<open>Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero\<close>
-lemma NSCDERIV_inverse:
-     "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
-unfolding numeral_2_eq_2
-by (rule NSDERIV_inverse)
-
-lemma CDERIV_inverse:
-     "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
-unfolding numeral_2_eq_2
-by (rule DERIV_inverse)
+lemma CDERIV_inverse: "x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse x) x :> - (inverse x)\<^sup>2"
+  for x :: complex
+  unfolding numeral_2_eq_2 by (rule DERIV_inverse)
 
 
-subsection\<open>Derivative of Reciprocals (Function @{term inverse})\<close>
+subsection \<open>Derivative of Reciprocals (Function @{term inverse})\<close>
 
 lemma CDERIV_inverse_fun:
-     "[| DERIV f x :> d; f(x) \<noteq> (0::complex) |]
-      ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))"
-unfolding numeral_2_eq_2
-by (rule DERIV_inverse_fun)
+  "DERIV f x :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse (f x)) x :> - (d * inverse ((f x)\<^sup>2))"
+  for x :: complex
+  unfolding numeral_2_eq_2 by (rule DERIV_inverse_fun)
 
 lemma NSCDERIV_inverse_fun:
-     "[| NSDERIV f x :> d; f(x) \<noteq> (0::complex) |]
-      ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))"
-unfolding numeral_2_eq_2
-by (rule NSDERIV_inverse_fun)
+  "NSDERIV f x :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> NSDERIV (\<lambda>x. inverse (f x)) x :> - (d * inverse ((f x)\<^sup>2))"
+  for x :: complex
+  unfolding numeral_2_eq_2 by (rule NSDERIV_inverse_fun)
 
 
-subsection\<open>Derivative of Quotient\<close>
+subsection \<open>Derivative of Quotient\<close>
 
 lemma CDERIV_quotient:
-     "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |]
-       ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)"
-unfolding numeral_2_eq_2
-by (rule DERIV_quotient)
+  "DERIV f x :> d \<Longrightarrow> DERIV g x :> e \<Longrightarrow> g(x) \<noteq> 0 \<Longrightarrow>
+    DERIV (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x)\<^sup>2"
+  for x :: complex
+  unfolding numeral_2_eq_2 by (rule DERIV_quotient)
 
 lemma NSCDERIV_quotient:
-     "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> (0::complex) |]
-       ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)"
-unfolding numeral_2_eq_2
-by (rule NSDERIV_quotient)
+  "NSDERIV f x :> d \<Longrightarrow> NSDERIV g x :> e \<Longrightarrow> g x \<noteq> (0::complex) \<Longrightarrow>
+    NSDERIV (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x)\<^sup>2"
+  unfolding numeral_2_eq_2 by (rule NSDERIV_quotient)
 
 
-subsection\<open>Caratheodory Formulation of Derivative at a Point: Standard Proof\<close>
+subsection \<open>Caratheodory Formulation of Derivative at a Point: Standard Proof\<close>
 
 lemma CARAT_CDERIVD:
-     "(\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l
-      ==> NSDERIV f x :> l"
-by clarify (rule CARAT_DERIVD)
+  "(\<forall>z. f z - f x = g z * (z - x)) \<and> isNSCont g x \<and> g x = l \<Longrightarrow> NSDERIV f x :> l"
+  by clarify (rule CARAT_DERIVD)
 
 end
diff -r 86e2f2208a58 -r 37ce6ceacbb7 src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Sun Dec 18 16:13:20 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Sun Dec 18 20:01:24 2016 +0100
@@ -4,280 +4,287 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-section\<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close>
+section \<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close>
 
 theory NSPrimes
-imports "~~/src/HOL/Number_Theory/Primes" "../Hyperreal"
+  imports "~~/src/HOL/Number_Theory/Primes" "../Hyperreal"
 begin
 
-text\<open>These can be used to derive an alternative proof of the infinitude of
+text \<open>These can be used to derive an alternative proof of the infinitude of
 primes by considering a property of nonstandard sets.\<close>
 
-definition
-  starprime :: "hypnat set" where
-  [transfer_unfold]: "starprime = ( *s* {p. prime p})"
+definition starprime :: "hypnat set"
+  where [transfer_unfold]: "starprime = *s* {p. prime p}"
 
-definition
-  choicefun :: "'a set => 'a" where
-  "choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
+definition choicefun :: "'a set \<Rightarrow> 'a"
+  where "choicefun E = (SOME x. \<exists>X \<in> Pow E - {{}}. x \<in> X)"
 
-primrec injf_max :: "nat => ('a::{order} set) => 'a"
+primrec injf_max :: "nat \<Rightarrow> 'a::order set \<Rightarrow> 'a"
 where
   injf_max_zero: "injf_max 0 E = choicefun E"
-| injf_max_Suc:  "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})"
-
+| injf_max_Suc: "injf_max (Suc n) E = choicefun ({e. e \<in> E \<and> injf_max n E < e})"
 
-lemma dvd_by_all2:
-  fixes M :: nat
-  shows "\<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N"
-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
+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
 
-lemma dvd_by_all:
-  "\<forall>M::nat. \<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N"
+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
 
-lemma hypnat_of_nat_le_zero_iff [simp]: "(hypnat_of_nat n <= 0) = (n = 0)"
-by (transfer, simp)
+lemma hypnat_of_nat_le_zero_iff [simp]: "hypnat_of_nat n \<le> 0 \<longleftrightarrow> n = 0"
+  by transfer simp
 
-(* Goldblatt: Exercise 5.11(2) - p. 57 *)
-lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m dvd N)"
-by (transfer, rule dvd_by_all)
+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)"
+  by transfer (rule dvd_by_all)
 
 lemmas hdvd_by_all2 = hdvd_by_all [THEN spec]
 
-(* Goldblatt: Exercise 5.11(2) - p. 57 *)
+text \<open>Goldblatt: Exercise 5.11(2) -- p. 57.\<close>
 lemma hypnat_dvd_all_hypnat_of_nat:
-     "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) dvd N)"
-apply (cut_tac hdvd_by_all)
-apply (drule_tac x = whn in spec, auto)
-apply (rule exI, auto)
-apply (drule_tac x = "hypnat_of_nat n" in spec)
-apply (auto simp add: linorder_not_less)
-done
+  "\<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
 
 
-text\<open>The nonstandard extension of the set prime numbers consists of precisely
-those hypernaturals exceeding 1 that have no nontrivial factors\<close>
+text \<open>The nonstandard extension of the set prime numbers consists of precisely
+  those hypernaturals exceeding 1 that have no nontrivial factors.\<close>
 
-(* Goldblatt: Exercise 5.11(3a) - p 57  *)
-lemma starprime:
-  "starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
-by (transfer, auto simp add: prime_nat_iff)
+text \<open>Goldblatt: Exercise 5.11(3a) -- p 57.\<close>
+lemma starprime: "starprime = {p. 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)}"
+  by transfer (auto simp add: prime_nat_iff)
 
-(* Goldblatt Exercise 5.11(3b) - p 57  *)
-lemma hyperprime_factor_exists [rule_format]:
-  "!!n. 1 < n ==> (\<exists>k \<in> starprime. k dvd n)"
-by (transfer, simp add: prime_factor_nat)
+text \<open>Goldblatt Exercise 5.11(3b) -- p 57.\<close>
+lemma hyperprime_factor_exists: "\<And>n. 1 < n \<Longrightarrow> \<exists>k \<in> starprime. k dvd n"
+  by transfer (simp add: prime_factor_nat)
 
-(* Goldblatt Exercise 3.10(1) - p. 29 *)
-lemma NatStar_hypnat_of_nat: "finite A ==> *s* A = hypnat_of_nat ` A"
-by (rule starset_finite)
+text \<open>Goldblatt Exercise 3.10(1) -- p. 29.\<close>
+lemma NatStar_hypnat_of_nat: "finite A \<Longrightarrow> *s* A = hypnat_of_nat ` A"
+  by (rule starset_finite)
 
 
-subsection\<open>Another characterization of infinite set of natural numbers\<close>
+subsection \<open>Another characterization of infinite set of natural numbers\<close>
 
-lemma finite_nat_set_bounded: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<(n::nat))"
-apply (erule_tac F = N in finite_induct, auto)
-apply (rule_tac x = "Suc n + x" in exI, auto)
-done
+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 = (\<exists>n. (\<forall>i \<in> N. i<(n::nat)))"
-by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite)
+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: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n <= (i::nat))"
-by (auto simp add: finite_nat_set_bounded_iff not_less)
+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 \<in> N. i<=(n::nat)) ==> finite N"
-apply (rule finite_subset)
- apply (rule_tac [2] finite_atMost, auto)
-done
+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 ==> \<exists>n. (\<forall>i \<in> N. i<=(n::nat))"
-apply (erule_tac F = N in finite_induct, auto)
-apply (rule_tac x = "n + x" in exI, 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 = (\<exists>n. (\<forall>i \<in> N. i<=(n::nat)))"
-by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2)
+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: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n < (i::nat))"
-by (auto simp add: finite_nat_set_bounded_iff2 not_le)
+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>
+subsection \<open>An injective function cannot define an embedded natural number\<close>
 
-lemma lemma_infinite_set_singleton: "\<forall>m n. m \<noteq> n --> f n \<noteq> f m
-      ==>  {n. f n = N} = {} |  (\<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) = (x = n) ")
-apply auto
-done
+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
 
 lemma inj_fun_not_hypnat_in_SHNat:
-  assumes inj_f: "inj (f::nat=>nat)"
+  fixes f :: "nat \<Rightarrow> nat"
+  assumes inj_f: "inj f"
   shows "starfun f whn \<notin> Nats"
 proof
   from inj_f have inj_f': "inj (starfun f)"
     by (transfer inj_on_def Ball_def UNIV_def)
   assume "starfun f whn \<in> Nats"
   then obtain N where N: "starfun f whn = hypnat_of_nat N"
-    by (auto simp add: Nats_def)
-  hence "\<exists>n. starfun f n = hypnat_of_nat N" ..
-  hence "\<exists>n. f n = N" by transfer
-  then obtain n where n: "f n = N" ..
-  hence "starfun f (hypnat_of_nat n) = hypnat_of_nat N"
+    by (auto simp: Nats_def)
+  then have "\<exists>n. starfun f n = hypnat_of_nat N" ..
+  then have "\<exists>n. f n = N" by transfer
+  then obtain n where "f n = N" ..
+  then have "starfun f (hypnat_of_nat n) = hypnat_of_nat N"
     by transfer
   with N have "starfun f whn = starfun f (hypnat_of_nat n)"
     by simp
   with inj_f' have "whn = hypnat_of_nat n"
     by (rule injD)
-  thus "False"
+  then show False
     by (simp add: whn_neq_hypnat_of_nat)
 qed
 
-lemma range_subset_mem_starsetNat:
-   "range f <= A ==> starfun f whn \<in> *s* A"
-apply (rule_tac x="whn" in spec)
-apply (transfer, auto)
-done
+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
+
+text \<open>
+  Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360.
 
-(*--------------------------------------------------------------------------------*)
-(* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360                 *)
-(* Let E be a nonvoid ordered set with no maximal elements (note: effectively an  *)
-(* infinite set if we take E = N (Nats)). Then there exists an order-preserving   *)
-(* injection from N to E. Of course, (as some doofus will undoubtedly point out!  *)
-(* :-)) can use notion of least element in proof (i.e. no need for choice) if     *)
-(* dealing with nats as we have well-ordering property                            *)
-(*--------------------------------------------------------------------------------*)
+  Let \<open>E\<close> be a nonvoid ordered set with no maximal elements (note: effectively an
+  infinite set if we take \<open>E = N\<close> (Nats)). Then there exists an order-preserving
+  injection from \<open>N\<close> to \<open>E\<close>. Of course, (as some doofus will undoubtedly point out!
+  :-)) can use notion of least element in proof (i.e. no need for choice) if
+  dealing with nats as we have well-ordering property.
+\<close>
 
-lemma lemmaPow3: "E \<noteq> {} ==> \<exists>x. \<exists>X \<in> (Pow E - {{}}). x: X"
-by auto
+lemma lemmaPow3: "E \<noteq> {} \<Longrightarrow> \<exists>x. \<exists>X \<in> Pow E - {{}}. x \<in> X"
+  by auto
 
-lemma choicefun_mem_set [simp]: "E \<noteq> {} ==> choicefun E \<in> E"
-apply (unfold choicefun_def)
-apply (rule lemmaPow3 [THEN someI2_ex], auto)
-done
+lemma choicefun_mem_set [simp]: "E \<noteq> {} \<Longrightarrow> choicefun E \<in> E"
+  apply (unfold choicefun_def)
+  apply (rule lemmaPow3 [THEN someI2_ex], auto)
+  done
 
-lemma injf_max_mem_set: "[| E \<noteq>{}; \<forall>x. \<exists>y \<in> E. x < y |] ==> injf_max n E \<in> E"
-apply (induct_tac "n", force)
-apply (simp (no_asm) add: choicefun_def)
-apply (rule lemmaPow3 [THEN someI2_ex], auto)
-done
+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
 
-lemma injf_max_order_preserving: "\<forall>x. \<exists>y \<in> E. x < y ==> injf_max n E < injf_max (Suc n) E"
-apply (simp (no_asm) add: choicefun_def)
-apply (rule lemmaPow3 [THEN someI2_ex], auto)
-done
+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
 
-lemma injf_max_order_preserving2: "\<forall>x. \<exists>y \<in> E. x < y
-      ==> \<forall>n m. m < n --> injf_max m E < injf_max n E"
-apply (rule allI)
-apply (induct_tac "n", auto)
-apply (simp (no_asm) 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, auto)
-apply (drule_tac x = "injf_max m E" in order_less_trans, auto)
-done
+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
+  apply (drule_tac x = "injf_max m E" in order_less_trans)
+   apply auto
+  done
 
-lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y ==> inj (%n. injf_max n E)"
-apply (rule inj_onI)
-apply (rule ccontr, auto)
-apply (drule injf_max_order_preserving2)
-apply (metis linorder_antisym_conv3 order_less_le)
-done
+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 linorder_antisym_conv3 order_less_le)
+  done
 
 lemma infinite_set_has_order_preserving_inj:
-     "[| (E::('a::{order} set)) \<noteq> {}; \<forall>x. \<exists>y \<in> E. x < y |]
-      ==> \<exists>f. range f <= E & inj (f::nat => 'a) & (\<forall>m. f m < f(Suc m))"
-apply (rule_tac x = "%n. injf_max n E" in exI, safe)
-apply (rule injf_max_mem_set)
-apply (rule_tac [3] inj_injf_max)
-apply (rule_tac [4] injf_max_order_preserving, auto)
-done
+  "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
 
-text\<open>Only need the existence of an injective function from N to A for proof\<close>
 
-lemma hypnat_infinite_has_nonstandard:
-     "~ finite A ==> 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], auto)
-apply (drule inj_fun_not_hypnat_in_SHNat)
-apply (drule range_subset_mem_starsetNat)
-apply (auto simp add: SHNat_eq)
-done
+text \<open>Only need the existence of an injective function from \<open>N\<close> to \<open>A\<close> for proof.\<close>
 
-lemma starsetNat_eq_hypnat_of_nat_image_finite: "*s* A =  hypnat_of_nat ` A ==> finite A"
-by (metis hypnat_infinite_has_nonstandard less_irrefl)
+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 finite_starsetNat_iff: "( *s* A = hypnat_of_nat ` A) = (finite A)"
-by (blast intro!: starsetNat_eq_hypnat_of_nat_image_finite NatStar_hypnat_of_nat)
+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)
+
+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: "(~ finite A) = (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: "\<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
 
-subsection\<open>Existence of Infinitely Many Primes: a Nonstandard Proof\<close>
 
-lemma lemma_not_dvd_hypnat_one [simp]: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n dvd 1)"
-apply auto
-apply (rule_tac x = 2 in bexI)
-apply (transfer, auto)
-done
+subsection \<open>Existence of Infinitely Many Primes: a Nonstandard Proof\<close>
 
-lemma lemma_not_dvd_hypnat_one2 [simp]: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n dvd 1"
-apply (cut_tac lemma_not_dvd_hypnat_one)
-apply (auto simp del: lemma_not_dvd_hypnat_one)
-done
+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 hypnat_add_one_gt_one:
-    "!!N. 0 < N ==> 1 < (N::hypnat) + 1"
-by (transfer, simp)
+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 hypnat_add_one_gt_one: "\<And>N::hypnat. 0 < N \<Longrightarrow> 1 < N + 1"
+  by transfer simp
 
 lemma hypnat_of_nat_zero_not_prime [simp]: "hypnat_of_nat 0 \<notin> starprime"
-by (transfer, simp)
+  by transfer simp
 
-lemma hypnat_zero_not_prime [simp]:
-   "0 \<notin> starprime"
-by (cut_tac hypnat_of_nat_zero_not_prime, simp)
+lemma hypnat_zero_not_prime [simp]: "0 \<notin> starprime"
+  using hypnat_of_nat_zero_not_prime by simp
 
 lemma hypnat_of_nat_one_not_prime [simp]: "hypnat_of_nat 1 \<notin> starprime"
-by (transfer, simp)
+  by transfer simp
 
 lemma hypnat_one_not_prime [simp]: "1 \<notin> starprime"
-by (cut_tac hypnat_of_nat_one_not_prime, simp)
+  using hypnat_of_nat_one_not_prime by simp
 
-lemma hdvd_diff: "!!k m n :: hypnat. [| k dvd m; k dvd n |] ==> k dvd (m - n)"
-by (transfer, rule dvd_diff_nat)
+lemma hdvd_diff: "\<And>k m n :: hypnat. k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)"
+  by transfer (rule dvd_diff_nat)
 
-lemma hdvd_one_eq_one:
-  "\<And>x::hypnat. is_unit x \<Longrightarrow> x = 1"
+lemma hdvd_one_eq_one: "\<And>x::hypnat. is_unit x \<Longrightarrow> x = 1"
   by transfer simp
 
-text\<open>Already proved as \<open>primes_infinite\<close>, but now using non-standard naturals.\<close>
-theorem not_finite_prime: "~ 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 add: 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
+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
 
 end