merged
authorpaulson
Thu May 02 15:40:57 2019 +0100 (6 months ago)
changeset 70233778366b0f519
parent 70231 cdbc8d92c349
parent 70232 d19266b7465f
child 70234 4e0834322981
child 70235 b0680d8b0608
merged
     1.1 --- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Thu May 02 14:43:19 2019 +0200
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Thu May 02 15:40:57 2019 +0100
     1.3 @@ -201,45 +201,36 @@
     1.4  text \<open>Existence of infinite number not corresponding to any real number.
     1.5    Use assumption that member \<^term>\<open>\<U>\<close> is not finite.\<close>
     1.6  
     1.7 -text \<open>A few lemmas first.\<close>
     1.8 -
     1.9 -lemma lemma_omega_empty_singleton_disj:
    1.10 -  "{n::nat. x = real n} = {} \<or> (\<exists>y. {n::nat. x = real n} = {y})"
    1.11 -  by force
    1.12 -
    1.13 -lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
    1.14 -  using lemma_omega_empty_singleton_disj [of x] by auto
    1.15 -
    1.16 -lemma not_ex_hypreal_of_real_eq_omega: "\<nexists>x. hypreal_of_real x = \<omega>"
    1.17 -  apply (simp add: omega_def star_of_def star_n_eq_iff)
    1.18 -  apply clarify
    1.19 -  apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE])
    1.20 -  apply (erule eventually_mono)
    1.21 -  apply auto
    1.22 -  done
    1.23 -
    1.24  lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> \<omega>"
    1.25 -  using not_ex_hypreal_of_real_eq_omega by auto
    1.26 +proof -
    1.27 +  have False if "\<forall>\<^sub>F n in \<U>. x = 1 + real n" for x
    1.28 +  proof -
    1.29 +    have "finite {n::nat. x = 1 + real n}"
    1.30 +      by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute nat_le_linear nat_le_real_less)
    1.31 +    then show False
    1.32 +      using FreeUltrafilterNat.finite that by blast
    1.33 +  qed
    1.34 +  then show ?thesis
    1.35 +    by (auto simp add: omega_def star_of_def star_n_eq_iff)
    1.36 +qed
    1.37  
    1.38  text \<open>Existence of infinitesimal number also not corresponding to any real number.\<close>
    1.39  
    1.40 -lemma lemma_epsilon_empty_singleton_disj:
    1.41 -  "{n::nat. x = inverse(real(Suc n))} = {} \<or> (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
    1.42 -  by auto
    1.43 -
    1.44 -lemma lemma_finite_epsilon_set: "finite {n. x = inverse (real (Suc n))}"
    1.45 -  using lemma_epsilon_empty_singleton_disj [of x] by auto
    1.46 -
    1.47 -lemma not_ex_hypreal_of_real_eq_epsilon: "\<nexists>x. hypreal_of_real x = \<epsilon>"
    1.48 -  by (auto simp: epsilon_def star_of_def star_n_eq_iff
    1.49 -      lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite] simp del: of_nat_Suc)
    1.50 -
    1.51  lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> \<epsilon>"
    1.52 -  using not_ex_hypreal_of_real_eq_epsilon by auto
    1.53 +proof -
    1.54 +  have False if "\<forall>\<^sub>F n in \<U>. x = inverse (1 + real n)" for x
    1.55 +  proof -
    1.56 +    have "finite {n::nat. x = inverse (1 + real n)}"
    1.57 +      by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute inverse_inverse_eq linear nat_le_real_less of_nat_Suc) 
    1.58 +    then show False
    1.59 +      using FreeUltrafilterNat.finite that by blast
    1.60 +  qed
    1.61 +  then show ?thesis
    1.62 +    by (auto simp: epsilon_def star_of_def star_n_eq_iff)
    1.63 +qed
    1.64  
    1.65  lemma hypreal_epsilon_not_zero: "\<epsilon> \<noteq> 0"
    1.66 -  by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff FreeUltrafilterNat.proper
    1.67 -      del: star_of_zero)
    1.68 +  using hypreal_of_real_not_eq_epsilon by force
    1.69  
    1.70  lemma hypreal_epsilon_inverse_omega: "\<epsilon> = inverse \<omega>"
    1.71    by (simp add: epsilon_def omega_def star_n_inverse)
    1.72 @@ -248,25 +239,6 @@
    1.73    by (simp add: hypreal_epsilon_inverse_omega)
    1.74  
    1.75  
    1.76 -subsection \<open>Absolute Value Function for the Hyperreals\<close>
    1.77 -
    1.78 -lemma hrabs_add_less: "\<bar>x\<bar> < r \<Longrightarrow> \<bar>y\<bar> < s \<Longrightarrow> \<bar>x + y\<bar> < r + s"
    1.79 -  for x y r s :: hypreal
    1.80 -  by (simp add: abs_if split: if_split_asm)
    1.81 -
    1.82 -lemma hrabs_less_gt_zero: "\<bar>x\<bar> < r \<Longrightarrow> 0 < r"
    1.83 -  for x r :: hypreal
    1.84 -  by (blast intro!: order_le_less_trans abs_ge_zero)
    1.85 -
    1.86 -lemma hrabs_disj: "\<bar>x\<bar> = x \<or> \<bar>x\<bar> = -x"
    1.87 -  for x :: "'a::abs_if"
    1.88 -  by (simp add: abs_if)
    1.89 -
    1.90 -lemma hrabs_add_lemma_disj: "y + - x + (y + - z) = \<bar>x + - z\<bar> \<Longrightarrow> y = z \<or> x = y"
    1.91 -  for x y z :: hypreal
    1.92 -  by (simp add: abs_if split: if_split_asm)
    1.93 -
    1.94 -
    1.95  subsection \<open>Embedding the Naturals into the Hyperreals\<close>
    1.96  
    1.97  abbreviation hypreal_of_nat :: "nat \<Rightarrow> hypreal"
    1.98 @@ -425,18 +397,9 @@
    1.99  lemma hyperpow_two_le [simp]: "\<And>r. (0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow 2"
   1.100    by (auto simp add: hyperpow_two zero_le_mult_iff)
   1.101  
   1.102 -lemma hrabs_hyperpow_two [simp]:
   1.103 -  "\<bar>x pow 2\<bar> = (x::'a::{monoid_mult,linordered_ring_strict} star) pow 2"
   1.104 -  by (simp only: abs_of_nonneg hyperpow_two_le)
   1.105 -
   1.106  lemma hyperpow_two_hrabs [simp]: "\<bar>x::'a::linordered_idom star\<bar> pow 2 = x pow 2"
   1.107    by (simp add: hyperpow_hrabs)
   1.108  
   1.109 -text \<open>The precondition could be weakened to \<^term>\<open>0\<le>x\<close>.\<close>
   1.110 -lemma hypreal_mult_less_mono: "u < v \<Longrightarrow> x < y \<Longrightarrow> 0 < v \<Longrightarrow> 0 < x \<Longrightarrow> u * x < v * y"
   1.111 -  for u v x y :: hypreal
   1.112 -  by (simp add: mult_strict_mono order_less_imp_le)
   1.113 -
   1.114  lemma hyperpow_two_gt_one: "\<And>r::'a::linordered_semidom star. 1 < r \<Longrightarrow> 1 < r pow 2"
   1.115    by transfer simp
   1.116  
   1.117 @@ -444,10 +407,7 @@
   1.118    by transfer (rule one_le_power)
   1.119  
   1.120  lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
   1.121 -  apply (rule_tac y = "1 pow n" in order_trans)
   1.122 -   apply (rule_tac [2] hyperpow_le)
   1.123 -    apply auto
   1.124 -  done
   1.125 +  by (metis hyperpow_eq_one hyperpow_le one_le_numeral zero_less_one)
   1.126  
   1.127  lemma hyperpow_minus_one2 [simp]: "\<And>n. (- 1) pow (2 * n) = (1::hypreal)"
   1.128    by transfer (rule power_minus1_even)
   1.129 @@ -469,14 +429,10 @@
   1.130    by (drule HNatInfinite_is_Suc, auto)
   1.131  
   1.132  lemma hyperpow_le_le: "(0::hypreal) \<le> r \<Longrightarrow> r \<le> 1 \<Longrightarrow> n \<le> N \<Longrightarrow> r pow N \<le> r pow n"
   1.133 -  apply (drule order_le_less [of n, THEN iffD1])
   1.134 -  apply (auto intro: hyperpow_less_le)
   1.135 -  done
   1.136 +  by (metis hyperpow_less_le le_less)
   1.137  
   1.138  lemma hyperpow_Suc_le_self2: "(0::hypreal) \<le> r \<Longrightarrow> r < 1 \<Longrightarrow> r pow (n + (1::hypnat)) \<le> r"
   1.139 -  apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
   1.140 -    apply auto
   1.141 -  done
   1.142 +  by (metis hyperpow_less_le hyperpow_one hypnat_add_self_le le_less)
   1.143  
   1.144  lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n"
   1.145    by transfer (rule refl)
     2.1 --- a/src/HOL/Nonstandard_Analysis/NSA.thy	Thu May 02 14:43:19 2019 +0200
     2.2 +++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Thu May 02 15:40:57 2019 +0100
     2.3 @@ -964,8 +964,8 @@
     2.4        then obtain r where "y < r" "r < x"
     2.5          using dense by blast
     2.6        then show ?thesis
     2.7 -        using isUbD [OF that] apply (simp add: )
     2.8 -        by (meson SReal_dense \<open>y \<in> \<real>\<close> assms greater not_le)
     2.9 +        using isUbD [OF that]
    2.10 +        by simp (meson SReal_dense \<open>y \<in> \<real>\<close> assms greater not_le)
    2.11      qed auto
    2.12    qed
    2.13    with assms show ?thesis
    2.14 @@ -1161,14 +1161,14 @@
    2.15  
    2.16  lemma approx_hrabs_disj: "\<bar>x\<bar> \<approx> x \<or> \<bar>x\<bar> \<approx> -x"
    2.17    for x :: hypreal
    2.18 -  using hrabs_disj [of x] by auto
    2.19 +  by (simp add: abs_if)
    2.20  
    2.21  
    2.22  subsection \<open>Theorems about Monads\<close>
    2.23  
    2.24  lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad x \<union> monad (- x)"
    2.25    for x :: hypreal
    2.26 -  by (rule hrabs_disj [of x, THEN disjE]) auto
    2.27 +  by (simp add: abs_if)
    2.28  
    2.29  lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal \<Longrightarrow> monad (x + e) = monad x"
    2.30    by (fast intro!: Infinitesimal_add_approx_self [THEN approx_sym] approx_monad_iff [THEN iffD1])
    2.31 @@ -1184,7 +1184,7 @@
    2.32  
    2.33  lemma monad_zero_hrabs_iff: "x \<in> monad 0 \<longleftrightarrow> \<bar>x\<bar> \<in> monad 0"
    2.34    for x :: hypreal
    2.35 -  by (rule hrabs_disj [of x, THEN disjE]) (auto simp: monad_zero_minus_iff [symmetric])
    2.36 +  using Infinitesimal_monad_zero_iff by blast
    2.37  
    2.38  lemma mem_monad_self [simp]: "x \<in> monad x"
    2.39    by (simp add: monad_def)
    2.40 @@ -1240,7 +1240,7 @@
    2.41  
    2.42  lemma approx_hrabs_zero_cancel: "\<bar>x\<bar> \<approx> 0 \<Longrightarrow> x \<approx> 0"
    2.43    for x :: hypreal
    2.44 -  using hrabs_disj [of x] by (auto dest: approx_minus)
    2.45 +  using mem_infmal_iff by blast
    2.46  
    2.47  lemma approx_hrabs_add_Infinitesimal: "e \<in> Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>x + e\<bar>"
    2.48    for e x :: hypreal
    2.49 @@ -1614,25 +1614,21 @@
    2.50      by auto
    2.51  qed
    2.52  
    2.53 -lemma lemma_real_le_Un_eq2:
    2.54 -  "{n. u \<le> inverse(real(Suc n))} =
    2.55 -    {n. u < inverse(real(Suc n))} \<union> {n. u = inverse(real(Suc n))}"
    2.56 -  by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
    2.57 -
    2.58 -lemma finite_inverse_real_of_posnat_ge_real: "0 < u \<Longrightarrow> finite {n. u \<le> inverse (real (Suc n))}"
    2.59 -  by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real
    2.60 -      simp del: of_nat_Suc)
    2.61 +lemma finite_inverse_real_of_posnat_ge_real:
    2.62 +  assumes "0 < u"
    2.63 +  shows "finite {n. u \<le> inverse (real (Suc n))}"
    2.64 +proof -
    2.65 +  have "\<forall>na. u \<le> inverse (1 + real na) \<longrightarrow> na \<le> ceiling (inverse u)"
    2.66 +    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))
    2.67 +  then show ?thesis
    2.68 +    apply (auto simp add: finite_nat_set_iff_bounded_le)
    2.69 +    by (meson assms inverse_positive_iff_positive le_nat_iff less_imp_le zero_less_ceiling)
    2.70 +qed
    2.71  
    2.72  lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
    2.73    "0 < u \<Longrightarrow> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) \<U>"
    2.74    by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)
    2.75  
    2.76 -text \<open>The complement of \<open>{n. u \<le> inverse(real(Suc n))} = {n. inverse (real (Suc n)) < u}\<close>
    2.77 -  is in \<open>\<U>\<close> by property of (free) ultrafilters.\<close>
    2.78 -lemma Compl_le_inverse_eq: "- {n. u \<le> inverse(real(Suc n))} = {n. inverse(real(Suc n)) < u}"
    2.79 -  by (auto dest!: order_le_less_trans simp add: linorder_not_le)
    2.80 -
    2.81 -
    2.82  lemma FreeUltrafilterNat_inverse_real_of_posnat:
    2.83    "0 < u \<Longrightarrow> eventually (\<lambda>n. inverse(real(Suc n)) < u) \<U>"
    2.84    by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)