more de-applying
authorpaulson <lp15@cam.ac.uk>
Tue Apr 30 15:49:15 2019 +0100 (6 months ago)
changeset 70218e48c0b5897a6
parent 70217 1f04832cbfcf
child 70219 b21efbf64292
more de-applying
src/HOL/Nonstandard_Analysis/Star.thy
     1.1 --- a/src/HOL/Nonstandard_Analysis/Star.thy	Tue Apr 30 14:42:52 2019 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/Star.thy	Tue Apr 30 15:49:15 2019 +0100
     1.3 @@ -82,10 +82,8 @@
     1.4  text \<open>Nonstandard extension of a function (defined using a
     1.5    constant sequence) as a special case of an internal function.\<close>
     1.6  
     1.7 -lemma starfun_n_starfun: "\<forall>n. F n = f \<Longrightarrow> *fn* F = *f* f"
     1.8 -  apply (drule fun_eq_iff [THEN iffD2])
     1.9 -  apply (simp add: starfun_n_def starfun_def star_of_def)
    1.10 -  done
    1.11 +lemma starfun_n_starfun: "F = (\<lambda>n. f) \<Longrightarrow> *fn* F = *f* f"
    1.12 +  by (simp add: starfun_n_def starfun_def star_of_def)
    1.13  
    1.14  text \<open>Prove that \<open>abs\<close> for hypreal is a nonstandard extension of abs for real w/o
    1.15    use of congruence property (proved after this for general
    1.16 @@ -94,16 +92,13 @@
    1.17    Proof now Uses the ultrafilter tactic!\<close>
    1.18  
    1.19  lemma hrabs_is_starext_rabs: "is_starext abs abs"
    1.20 -  apply (simp add: is_starext_def, safe)
    1.21 -  apply (rule_tac x=x in star_cases)
    1.22 -  apply (rule_tac x=y in star_cases)
    1.23 -  apply (unfold star_n_def, auto)
    1.24 -  apply (rule bexI, rule_tac [2] lemma_starrel_refl)
    1.25 -  apply (rule bexI, rule_tac [2] lemma_starrel_refl)
    1.26 -  apply (fold star_n_def)
    1.27 -  apply (unfold star_abs_def starfun_def star_of_def)
    1.28 -  apply (simp add: Ifun_star_n star_n_eq_iff)
    1.29 -  done
    1.30 +  proof -
    1.31 +  have "\<exists>f\<in>Rep_star (star_n h). \<exists>g\<in>Rep_star (star_n k). (star_n k = \<bar>star_n h\<bar>) = (\<forall>\<^sub>F n in \<U>. (g n::'a) = \<bar>f n\<bar>)"
    1.32 +    for x y :: "'a star" and h k
    1.33 +    by (metis (full_types) Rep_star_star_n star_n_abs star_n_eq_iff)
    1.34 +  then show ?thesis
    1.35 +    unfolding is_starext_def by (metis star_cases)
    1.36 +qed
    1.37  
    1.38  
    1.39  text \<open>Nonstandard extension of functions.\<close>
    1.40 @@ -153,34 +148,32 @@
    1.41  lemma starfun_Id [simp]: "\<And>x. ( *f* (\<lambda>x. x)) x = x"
    1.42    by transfer (rule refl)
    1.43  
    1.44 -text \<open>This is trivial, given \<open>starfun_Id\<close>.\<close>
    1.45 -lemma starfun_Idfun_approx: "x \<approx> star_of a \<Longrightarrow> ( *f* (\<lambda>x. x)) x \<approx> star_of a"
    1.46 -  by (simp only: starfun_Id)
    1.47 -
    1.48  text \<open>The Star-function is a (nonstandard) extension of the function.\<close>
    1.49  lemma is_starext_starfun: "is_starext ( *f* f) f"
    1.50 -  apply (auto simp: is_starext_def)
    1.51 -  apply (rule_tac x = x in star_cases)
    1.52 -  apply (rule_tac x = y in star_cases)
    1.53 -  apply (auto intro!: bexI [OF _ Rep_star_star_n] simp: starfun star_n_eq_iff)
    1.54 -  done
    1.55 +proof -
    1.56 +  have "\<exists>X\<in>Rep_star x. \<exists>Y\<in>Rep_star y. (y = (*f* f) x) = (\<forall>\<^sub>F n in \<U>. Y n = f (X n))"
    1.57 +    for x y
    1.58 +    by (metis (mono_tags) Rep_star_star_n star_cases star_n_eq_iff starfun_star_n)
    1.59 +  then show ?thesis
    1.60 +    by (auto simp: is_starext_def)
    1.61 +qed
    1.62  
    1.63  text \<open>Any nonstandard extension is in fact the Star-function.\<close>
    1.64 -lemma is_starfun_starext: "is_starext F f \<Longrightarrow> F = *f* f"
    1.65 -  apply (simp add: is_starext_def)
    1.66 -  apply (rule ext)
    1.67 -  apply (rule_tac x = x in star_cases)
    1.68 -  apply (drule_tac x = x in spec)
    1.69 -  apply (drule_tac x = "( *f* f) x" in spec)
    1.70 -  apply (auto simp add: starfun_star_n)
    1.71 -  apply (simp add: star_n_eq_iff [symmetric])
    1.72 -  apply (simp add: starfun_star_n [of f, symmetric])
    1.73 -  done
    1.74 +lemma is_starfun_starext:
    1.75 +  assumes "is_starext F f"
    1.76 +  shows "F = *f* f"
    1.77 +  proof -
    1.78 +  have "F x = (*f* f) x"
    1.79 +    if "\<forall>x y. \<exists>X\<in>Rep_star x. \<exists>Y\<in>Rep_star y. (y = F x) = (\<forall>\<^sub>F n in \<U>. Y n = f (X n))" for x
    1.80 +    by (metis that mem_Rep_star_iff star_n_eq_iff starfun_star_n)
    1.81 +  with assms show ?thesis
    1.82 +    by (force simp add: is_starext_def)
    1.83 +qed
    1.84  
    1.85  lemma is_starext_starfun_iff: "is_starext F f \<longleftrightarrow> F = *f* f"
    1.86    by (blast intro: is_starfun_starext is_starext_starfun)
    1.87  
    1.88 -text \<open>Extented function has same solution as its standard version
    1.89 +text \<open>Extended function has same solution as its standard version
    1.90    for real arguments. i.e they are the same for all real arguments.\<close>
    1.91  lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
    1.92    by (rule starfun_star_of)
    1.93 @@ -199,9 +192,7 @@
    1.94    "( *f* f) x \<approx> l \<Longrightarrow> ( *f* g) x \<approx> m \<Longrightarrow> l \<in> HFinite \<Longrightarrow> m \<in> HFinite \<Longrightarrow>
    1.95      ( *f* (\<lambda>x. f x * g x)) x \<approx> l * m"
    1.96    for l m :: "'a::real_normed_algebra star"
    1.97 -  apply (drule (3) approx_mult_HFinite)
    1.98 -  apply (auto intro: approx_HFinite [OF _ approx_sym])
    1.99 -  done
   1.100 +  using approx_mult_HFinite by auto
   1.101  
   1.102  lemma starfun_add_approx: "( *f* f) x \<approx> l \<Longrightarrow> ( *f* g) x \<approx> m \<Longrightarrow> ( *f* (%x. f x + g x)) x \<approx> l + m"
   1.103    by (auto intro: approx_add)
   1.104 @@ -259,35 +250,48 @@
   1.105        star_of_nat_def starfun_star_n star_n_inverse star_n_less)
   1.106  
   1.107  lemma HNatInfinite_inverse_Infinitesimal [simp]:
   1.108 -  "n \<in> HNatInfinite \<Longrightarrow> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
   1.109 -  apply (cases n)
   1.110 -  apply (auto simp: of_hypnat_def starfun_star_n star_n_inverse
   1.111 -    HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
   1.112 -  apply (drule_tac x = "Suc m" in spec)
   1.113 -  apply (auto elim!: eventually_mono)
   1.114 -  done
   1.115 +  assumes "n \<in> HNatInfinite"
   1.116 +  shows "inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
   1.117 +proof (cases n)
   1.118 +  case (star_n X)
   1.119 +  then have *: "\<And>k. \<forall>\<^sub>F n in \<U>. k < X n"
   1.120 +    using HNatInfinite_FreeUltrafilterNat assms by blast
   1.121 +  have "\<forall>\<^sub>F n in \<U>. inverse (real (X n)) < inverse (1 + real m)" for m
   1.122 +    using * [of "Suc m"] by (auto elim!: eventually_mono)
   1.123 +  then show ?thesis
   1.124 +    using star_n by (auto simp: of_hypnat_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff2)
   1.125 +qed
   1.126  
   1.127  lemma approx_FreeUltrafilterNat_iff:
   1.128    "star_n X \<approx> star_n Y \<longleftrightarrow> (\<forall>r>0. eventually (\<lambda>n. norm (X n - Y n) < r) \<U>)"
   1.129 -  apply (subst approx_minus_iff)
   1.130 -  apply (rule mem_infmal_iff [THEN subst])
   1.131 -  apply (simp add: star_n_diff)
   1.132 -  apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
   1.133 -  done
   1.134 +  (is "?lhs = ?rhs")
   1.135 +proof -
   1.136 +  have "?lhs = (star_n X - star_n Y \<approx> 0)"
   1.137 +    using approx_minus_iff by blast
   1.138 +  also have "... = ?rhs"
   1.139 +    by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff mem_infmal_iff star_n_diff)
   1.140 +  finally show ?thesis .
   1.141 +qed
   1.142  
   1.143  lemma approx_FreeUltrafilterNat_iff2:
   1.144    "star_n X \<approx> star_n Y \<longleftrightarrow> (\<forall>m. eventually (\<lambda>n. norm (X n - Y n) < inverse (real (Suc m))) \<U>)"
   1.145 -  apply (subst approx_minus_iff)
   1.146 -  apply (rule mem_infmal_iff [THEN subst])
   1.147 -  apply (simp add: star_n_diff)
   1.148 -  apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2)
   1.149 -  done
   1.150 +  (is "?lhs = ?rhs")
   1.151 +proof -
   1.152 +  have "?lhs = (star_n X - star_n Y \<approx> 0)"
   1.153 +    using approx_minus_iff by blast
   1.154 +  also have "... = ?rhs"
   1.155 +    by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff2 mem_infmal_iff star_n_diff)
   1.156 +  finally show ?thesis .
   1.157 +qed
   1.158  
   1.159  lemma inj_starfun: "inj starfun"
   1.160 -  apply (rule inj_onI)
   1.161 -  apply (rule ext, rule ccontr)
   1.162 -  apply (drule_tac x = "star_n (\<lambda>n. xa)" in fun_cong)
   1.163 -  apply (auto simp add: starfun star_n_eq_iff FreeUltrafilterNat.proper)
   1.164 -  done
   1.165 +proof (rule inj_onI)
   1.166 +  show "\<phi> = \<psi>" if eq: "*f* \<phi> = *f* \<psi>" for \<phi> \<psi> :: "'a \<Rightarrow> 'b"
   1.167 +  proof (rule ext, rule ccontr)
   1.168 +    show False
   1.169 +      if "\<phi> x \<noteq> \<psi> x" for x
   1.170 +      by (metis eq that star_of_inject starfun_eq)
   1.171 +  qed
   1.172 +qed
   1.173  
   1.174  end