merged

--- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Thu May 02 14:43:19 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Thu May 02 15:40:57 2019 +0100
@@ -201,45 +201,36 @@
 text \<open>Existence of infinite number not corresponding to any real number.
   Use assumption that member \<^term>\<open>\<U>\<close> is not finite.\<close>
 
-text \<open>A few lemmas first.\<close>
-
-lemma lemma_omega_empty_singleton_disj:
-  "{n::nat. x = real n} = {} \<or> (\<exists>y. {n::nat. x = real n} = {y})"
-  by force
-
-lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
-  using lemma_omega_empty_singleton_disj [of x] by auto
-
-lemma not_ex_hypreal_of_real_eq_omega: "\<nexists>x. hypreal_of_real x = \<omega>"
-  apply (simp add: omega_def star_of_def star_n_eq_iff)
-  apply clarify
-  apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE])
-  apply (erule eventually_mono)
-  apply auto
-  done
-
 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> \<omega>"
-  using not_ex_hypreal_of_real_eq_omega by auto
+proof -
+  have False if "\<forall>\<^sub>F n in \<U>. x = 1 + real n" for x
+  proof -
+    have "finite {n::nat. x = 1 + real n}"
+      by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute nat_le_linear nat_le_real_less)
+    then show False
+      using FreeUltrafilterNat.finite that by blast
+  qed
+  then show ?thesis
+    by (auto simp add: omega_def star_of_def star_n_eq_iff)
+qed
 
 text \<open>Existence of infinitesimal number also not corresponding to any real number.\<close>
 
-lemma lemma_epsilon_empty_singleton_disj:
-  "{n::nat. x = inverse(real(Suc n))} = {} \<or> (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
-  by auto
-
-lemma lemma_finite_epsilon_set: "finite {n. x = inverse (real (Suc n))}"
-  using lemma_epsilon_empty_singleton_disj [of x] by auto
-
-lemma not_ex_hypreal_of_real_eq_epsilon: "\<nexists>x. hypreal_of_real x = \<epsilon>"
-  by (auto simp: epsilon_def star_of_def star_n_eq_iff
-      lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite] simp del: of_nat_Suc)
-
 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> \<epsilon>"
-  using not_ex_hypreal_of_real_eq_epsilon by auto
+proof -
+  have False if "\<forall>\<^sub>F n in \<U>. x = inverse (1 + real n)" for x
+  proof -
+    have "finite {n::nat. x = inverse (1 + real n)}"
+      by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute inverse_inverse_eq linear nat_le_real_less of_nat_Suc) 
+    then show False
+      using FreeUltrafilterNat.finite that by blast
+  qed
+  then show ?thesis
+    by (auto simp: epsilon_def star_of_def star_n_eq_iff)
+qed
 
 lemma hypreal_epsilon_not_zero: "\<epsilon> \<noteq> 0"
-  by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff FreeUltrafilterNat.proper
-      del: star_of_zero)
+  using hypreal_of_real_not_eq_epsilon by force
 
 lemma hypreal_epsilon_inverse_omega: "\<epsilon> = inverse \<omega>"
   by (simp add: epsilon_def omega_def star_n_inverse)
@@ -248,25 +239,6 @@
   by (simp add: hypreal_epsilon_inverse_omega)
 
 
-subsection \<open>Absolute Value Function for the Hyperreals\<close>
-
-lemma hrabs_add_less: "\<bar>x\<bar> < r \<Longrightarrow> \<bar>y\<bar> < s \<Longrightarrow> \<bar>x + y\<bar> < r + s"
-  for x y r s :: hypreal
-  by (simp add: abs_if split: if_split_asm)
-
-lemma hrabs_less_gt_zero: "\<bar>x\<bar> < r \<Longrightarrow> 0 < r"
-  for x r :: hypreal
-  by (blast intro!: order_le_less_trans abs_ge_zero)
-
-lemma hrabs_disj: "\<bar>x\<bar> = x \<or> \<bar>x\<bar> = -x"
-  for x :: "'a::abs_if"
-  by (simp add: abs_if)
-
-lemma hrabs_add_lemma_disj: "y + - x + (y + - z) = \<bar>x + - z\<bar> \<Longrightarrow> y = z \<or> x = y"
-  for x y z :: hypreal
-  by (simp add: abs_if split: if_split_asm)
-
-
 subsection \<open>Embedding the Naturals into the Hyperreals\<close>
 
 abbreviation hypreal_of_nat :: "nat \<Rightarrow> hypreal"
@@ -425,18 +397,9 @@
 lemma hyperpow_two_le [simp]: "\<And>r. (0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow 2"
   by (auto simp add: hyperpow_two zero_le_mult_iff)
 
-lemma hrabs_hyperpow_two [simp]:
-  "\<bar>x pow 2\<bar> = (x::'a::{monoid_mult,linordered_ring_strict} star) pow 2"
-  by (simp only: abs_of_nonneg hyperpow_two_le)
-
 lemma hyperpow_two_hrabs [simp]: "\<bar>x::'a::linordered_idom star\<bar> pow 2 = x pow 2"
   by (simp add: hyperpow_hrabs)
 
-text \<open>The precondition could be weakened to \<^term>\<open>0\<le>x\<close>.\<close>
-lemma hypreal_mult_less_mono: "u < v \<Longrightarrow> x < y \<Longrightarrow> 0 < v \<Longrightarrow> 0 < x \<Longrightarrow> u * x < v * y"
-  for u v x y :: hypreal
-  by (simp add: mult_strict_mono order_less_imp_le)
-
 lemma hyperpow_two_gt_one: "\<And>r::'a::linordered_semidom star. 1 < r \<Longrightarrow> 1 < r pow 2"
   by transfer simp
 
@@ -444,10 +407,7 @@
   by transfer (rule one_le_power)
 
 lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
-  apply (rule_tac y = "1 pow n" in order_trans)
-   apply (rule_tac [2] hyperpow_le)
-    apply auto
-  done
+  by (metis hyperpow_eq_one hyperpow_le one_le_numeral zero_less_one)
 
 lemma hyperpow_minus_one2 [simp]: "\<And>n. (- 1) pow (2 * n) = (1::hypreal)"
   by transfer (rule power_minus1_even)
@@ -469,14 +429,10 @@
   by (drule HNatInfinite_is_Suc, auto)
 
 lemma hyperpow_le_le: "(0::hypreal) \<le> r \<Longrightarrow> r \<le> 1 \<Longrightarrow> n \<le> N \<Longrightarrow> r pow N \<le> r pow n"
-  apply (drule order_le_less [of n, THEN iffD1])
-  apply (auto intro: hyperpow_less_le)
-  done
+  by (metis hyperpow_less_le le_less)
 
 lemma hyperpow_Suc_le_self2: "(0::hypreal) \<le> r \<Longrightarrow> r < 1 \<Longrightarrow> r pow (n + (1::hypnat)) \<le> r"
-  apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
-    apply auto
-  done
+  by (metis hyperpow_less_le hyperpow_one hypnat_add_self_le le_less)
 
 lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n"
   by transfer (rule refl)

--- a/src/HOL/Nonstandard_Analysis/NSA.thy	Thu May 02 14:43:19 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Thu May 02 15:40:57 2019 +0100
@@ -964,8 +964,8 @@
       then obtain r where "y < r" "r < x"
         using dense by blast
       then show ?thesis
-        using isUbD [OF that] apply (simp add: )
-        by (meson SReal_dense \<open>y \<in> \<real>\<close> assms greater not_le)
+        using isUbD [OF that]
+        by simp (meson SReal_dense \<open>y \<in> \<real>\<close> assms greater not_le)
     qed auto
   qed
   with assms show ?thesis
@@ -1161,14 +1161,14 @@
 
 lemma approx_hrabs_disj: "\<bar>x\<bar> \<approx> x \<or> \<bar>x\<bar> \<approx> -x"
   for x :: hypreal
-  using hrabs_disj [of x] by auto
+  by (simp add: abs_if)
 
 
 subsection \<open>Theorems about Monads\<close>
 
 lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad x \<union> monad (- x)"
   for x :: hypreal
-  by (rule hrabs_disj [of x, THEN disjE]) auto
+  by (simp add: abs_if)
 
 lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal \<Longrightarrow> monad (x + e) = monad x"
   by (fast intro!: Infinitesimal_add_approx_self [THEN approx_sym] approx_monad_iff [THEN iffD1])
@@ -1184,7 +1184,7 @@
 
 lemma monad_zero_hrabs_iff: "x \<in> monad 0 \<longleftrightarrow> \<bar>x\<bar> \<in> monad 0"
   for x :: hypreal
-  by (rule hrabs_disj [of x, THEN disjE]) (auto simp: monad_zero_minus_iff [symmetric])
+  using Infinitesimal_monad_zero_iff by blast
 
 lemma mem_monad_self [simp]: "x \<in> monad x"
   by (simp add: monad_def)
@@ -1240,7 +1240,7 @@
 
 lemma approx_hrabs_zero_cancel: "\<bar>x\<bar> \<approx> 0 \<Longrightarrow> x \<approx> 0"
   for x :: hypreal
-  using hrabs_disj [of x] by (auto dest: approx_minus)
+  using mem_infmal_iff by blast
 
 lemma approx_hrabs_add_Infinitesimal: "e \<in> Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>x + e\<bar>"
   for e x :: hypreal
@@ -1614,25 +1614,21 @@
     by auto
 qed
 
-lemma lemma_real_le_Un_eq2:
-  "{n. u \<le> inverse(real(Suc n))} =
-    {n. u < inverse(real(Suc n))} \<union> {n. u = inverse(real(Suc n))}"
-  by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
-
-lemma finite_inverse_real_of_posnat_ge_real: "0 < u \<Longrightarrow> finite {n. u \<le> inverse (real (Suc n))}"
-  by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real
-      simp del: of_nat_Suc)
+lemma finite_inverse_real_of_posnat_ge_real:
+  assumes "0 < u"
+  shows "finite {n. u \<le> inverse (real (Suc n))}"
+proof -
+  have "\<forall>na. u \<le> inverse (1 + real na) \<longrightarrow> na \<le> ceiling (inverse u)"
+    by (metis add.commute add1_zle_eq assms ceiling_mono ceiling_of_nat dual_order.order_iff_strict inverse_inverse_eq le_imp_inverse_le semiring_1_class.of_nat_simps(2))
+  then show ?thesis
+    apply (auto simp add: finite_nat_set_iff_bounded_le)
+    by (meson assms inverse_positive_iff_positive le_nat_iff less_imp_le zero_less_ceiling)
+qed
 
 lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
   "0 < u \<Longrightarrow> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) \<U>"
   by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)
 
-text \<open>The complement of \<open>{n. u \<le> inverse(real(Suc n))} = {n. inverse (real (Suc n)) < u}\<close>
-  is in \<open>\<U>\<close> by property of (free) ultrafilters.\<close>
-lemma Compl_le_inverse_eq: "- {n. u \<le> inverse(real(Suc n))} = {n. inverse(real(Suc n)) < u}"
-  by (auto dest!: order_le_less_trans simp add: linorder_not_le)
-
-
 lemma FreeUltrafilterNat_inverse_real_of_posnat:
   "0 < u \<Longrightarrow> eventually (\<lambda>n. inverse(real(Suc n)) < u) \<U>"
   by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)