src/HOL/Limits.thy
changeset 44081 730f7cced3a6
parent 44079 bcc60791b7b9
child 44194 0639898074ae
     1.1 --- a/src/HOL/Limits.thy	Mon Aug 08 18:36:32 2011 -0700
     1.2 +++ b/src/HOL/Limits.thy	Mon Aug 08 19:26:53 2011 -0700
     1.3 @@ -8,263 +8,262 @@
     1.4  imports RealVector
     1.5  begin
     1.6  
     1.7 -subsection {* Nets *}
     1.8 +subsection {* Filters *}
     1.9  
    1.10  text {*
    1.11 -  A net is now defined simply as a filter on a set.
    1.12 -  The definition also allows non-proper filters.
    1.13 +  This definition also allows non-proper filters.
    1.14  *}
    1.15  
    1.16  locale is_filter =
    1.17 -  fixes net :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.18 -  assumes True: "net (\<lambda>x. True)"
    1.19 -  assumes conj: "net (\<lambda>x. P x) \<Longrightarrow> net (\<lambda>x. Q x) \<Longrightarrow> net (\<lambda>x. P x \<and> Q x)"
    1.20 -  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> net (\<lambda>x. P x) \<Longrightarrow> net (\<lambda>x. Q x)"
    1.21 +  fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.22 +  assumes True: "F (\<lambda>x. True)"
    1.23 +  assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
    1.24 +  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
    1.25  
    1.26 -typedef (open) 'a net =
    1.27 -  "{net :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter net}"
    1.28 +typedef (open) 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
    1.29  proof
    1.30 -  show "(\<lambda>x. True) \<in> ?net" by (auto intro: is_filter.intro)
    1.31 +  show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
    1.32  qed
    1.33  
    1.34 -lemma is_filter_Rep_net: "is_filter (Rep_net net)"
    1.35 -using Rep_net [of net] by simp
    1.36 +lemma is_filter_Rep_filter: "is_filter (Rep_filter A)"
    1.37 +  using Rep_filter [of A] by simp
    1.38  
    1.39 -lemma Abs_net_inverse':
    1.40 -  assumes "is_filter net" shows "Rep_net (Abs_net net) = net"
    1.41 -using assms by (simp add: Abs_net_inverse)
    1.42 +lemma Abs_filter_inverse':
    1.43 +  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
    1.44 +  using assms by (simp add: Abs_filter_inverse)
    1.45  
    1.46  
    1.47  subsection {* Eventually *}
    1.48  
    1.49 -definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
    1.50 -  "eventually P net \<longleftrightarrow> Rep_net net P"
    1.51 +definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.52 +  where "eventually P A \<longleftrightarrow> Rep_filter A P"
    1.53  
    1.54 -lemma eventually_Abs_net:
    1.55 -  assumes "is_filter net" shows "eventually P (Abs_net net) = net P"
    1.56 -unfolding eventually_def using assms by (simp add: Abs_net_inverse)
    1.57 +lemma eventually_Abs_filter:
    1.58 +  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
    1.59 +  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
    1.60  
    1.61 -lemma expand_net_eq:
    1.62 -  shows "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
    1.63 -unfolding Rep_net_inject [symmetric] fun_eq_iff eventually_def ..
    1.64 +lemma filter_eq_iff:
    1.65 +  shows "A = B \<longleftrightarrow> (\<forall>P. eventually P A = eventually P B)"
    1.66 +  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
    1.67  
    1.68 -lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
    1.69 -unfolding eventually_def
    1.70 -by (rule is_filter.True [OF is_filter_Rep_net])
    1.71 +lemma eventually_True [simp]: "eventually (\<lambda>x. True) A"
    1.72 +  unfolding eventually_def
    1.73 +  by (rule is_filter.True [OF is_filter_Rep_filter])
    1.74  
    1.75 -lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P net"
    1.76 +lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P A"
    1.77  proof -
    1.78    assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
    1.79 -  thus "eventually P net" by simp
    1.80 +  thus "eventually P A" by simp
    1.81  qed
    1.82  
    1.83  lemma eventually_mono:
    1.84 -  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
    1.85 -unfolding eventually_def
    1.86 -by (rule is_filter.mono [OF is_filter_Rep_net])
    1.87 +  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P A \<Longrightarrow> eventually Q A"
    1.88 +  unfolding eventually_def
    1.89 +  by (rule is_filter.mono [OF is_filter_Rep_filter])
    1.90  
    1.91  lemma eventually_conj:
    1.92 -  assumes P: "eventually (\<lambda>x. P x) net"
    1.93 -  assumes Q: "eventually (\<lambda>x. Q x) net"
    1.94 -  shows "eventually (\<lambda>x. P x \<and> Q x) net"
    1.95 -using assms unfolding eventually_def
    1.96 -by (rule is_filter.conj [OF is_filter_Rep_net])
    1.97 +  assumes P: "eventually (\<lambda>x. P x) A"
    1.98 +  assumes Q: "eventually (\<lambda>x. Q x) A"
    1.99 +  shows "eventually (\<lambda>x. P x \<and> Q x) A"
   1.100 +  using assms unfolding eventually_def
   1.101 +  by (rule is_filter.conj [OF is_filter_Rep_filter])
   1.102  
   1.103  lemma eventually_mp:
   1.104 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
   1.105 -  assumes "eventually (\<lambda>x. P x) net"
   1.106 -  shows "eventually (\<lambda>x. Q x) net"
   1.107 +  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) A"
   1.108 +  assumes "eventually (\<lambda>x. P x) A"
   1.109 +  shows "eventually (\<lambda>x. Q x) A"
   1.110  proof (rule eventually_mono)
   1.111    show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
   1.112 -  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) net"
   1.113 +  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) A"
   1.114      using assms by (rule eventually_conj)
   1.115  qed
   1.116  
   1.117  lemma eventually_rev_mp:
   1.118 -  assumes "eventually (\<lambda>x. P x) net"
   1.119 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
   1.120 -  shows "eventually (\<lambda>x. Q x) net"
   1.121 +  assumes "eventually (\<lambda>x. P x) A"
   1.122 +  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) A"
   1.123 +  shows "eventually (\<lambda>x. Q x) A"
   1.124  using assms(2) assms(1) by (rule eventually_mp)
   1.125  
   1.126  lemma eventually_conj_iff:
   1.127 -  "eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net"
   1.128 -by (auto intro: eventually_conj elim: eventually_rev_mp)
   1.129 +  "eventually (\<lambda>x. P x \<and> Q x) A \<longleftrightarrow> eventually P A \<and> eventually Q A"
   1.130 +  by (auto intro: eventually_conj elim: eventually_rev_mp)
   1.131  
   1.132  lemma eventually_elim1:
   1.133 -  assumes "eventually (\<lambda>i. P i) net"
   1.134 +  assumes "eventually (\<lambda>i. P i) A"
   1.135    assumes "\<And>i. P i \<Longrightarrow> Q i"
   1.136 -  shows "eventually (\<lambda>i. Q i) net"
   1.137 -using assms by (auto elim!: eventually_rev_mp)
   1.138 +  shows "eventually (\<lambda>i. Q i) A"
   1.139 +  using assms by (auto elim!: eventually_rev_mp)
   1.140  
   1.141  lemma eventually_elim2:
   1.142 -  assumes "eventually (\<lambda>i. P i) net"
   1.143 -  assumes "eventually (\<lambda>i. Q i) net"
   1.144 +  assumes "eventually (\<lambda>i. P i) A"
   1.145 +  assumes "eventually (\<lambda>i. Q i) A"
   1.146    assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
   1.147 -  shows "eventually (\<lambda>i. R i) net"
   1.148 -using assms by (auto elim!: eventually_rev_mp)
   1.149 +  shows "eventually (\<lambda>i. R i) A"
   1.150 +  using assms by (auto elim!: eventually_rev_mp)
   1.151  
   1.152  subsection {* Finer-than relation *}
   1.153  
   1.154 -text {* @{term "net \<le> net'"} means that @{term net} is finer than
   1.155 -@{term net'}. *}
   1.156 +text {* @{term "A \<le> B"} means that filter @{term A} is finer than
   1.157 +filter @{term B}. *}
   1.158  
   1.159 -instantiation net :: (type) complete_lattice
   1.160 +instantiation filter :: (type) complete_lattice
   1.161  begin
   1.162  
   1.163 -definition
   1.164 -  le_net_def: "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
   1.165 +definition le_filter_def:
   1.166 +  "A \<le> B \<longleftrightarrow> (\<forall>P. eventually P B \<longrightarrow> eventually P A)"
   1.167  
   1.168  definition
   1.169 -  less_net_def: "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
   1.170 +  "(A :: 'a filter) < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A"
   1.171  
   1.172  definition
   1.173 -  top_net_def: "top = Abs_net (\<lambda>P. \<forall>x. P x)"
   1.174 +  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
   1.175  
   1.176  definition
   1.177 -  bot_net_def: "bot = Abs_net (\<lambda>P. True)"
   1.178 +  "bot = Abs_filter (\<lambda>P. True)"
   1.179  
   1.180  definition
   1.181 -  sup_net_def: "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
   1.182 +  "sup A B = Abs_filter (\<lambda>P. eventually P A \<and> eventually P B)"
   1.183  
   1.184  definition
   1.185 -  inf_net_def: "inf a b = Abs_net
   1.186 -      (\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.187 +  "inf A B = Abs_filter
   1.188 +      (\<lambda>P. \<exists>Q R. eventually Q A \<and> eventually R B \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.189  
   1.190  definition
   1.191 -  Sup_net_def: "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
   1.192 +  "Sup S = Abs_filter (\<lambda>P. \<forall>A\<in>S. eventually P A)"
   1.193  
   1.194  definition
   1.195 -  Inf_net_def: "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
   1.196 +  "Inf S = Sup {A::'a filter. \<forall>B\<in>S. A \<le> B}"
   1.197  
   1.198  lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
   1.199 -unfolding top_net_def
   1.200 -by (rule eventually_Abs_net, rule is_filter.intro, auto)
   1.201 +  unfolding top_filter_def
   1.202 +  by (rule eventually_Abs_filter, rule is_filter.intro, auto)
   1.203  
   1.204  lemma eventually_bot [simp]: "eventually P bot"
   1.205 -unfolding bot_net_def
   1.206 -by (subst eventually_Abs_net, rule is_filter.intro, auto)
   1.207 +  unfolding bot_filter_def
   1.208 +  by (subst eventually_Abs_filter, rule is_filter.intro, auto)
   1.209  
   1.210  lemma eventually_sup:
   1.211 -  "eventually P (sup net net') \<longleftrightarrow> eventually P net \<and> eventually P net'"
   1.212 -unfolding sup_net_def
   1.213 -by (rule eventually_Abs_net, rule is_filter.intro)
   1.214 -   (auto elim!: eventually_rev_mp)
   1.215 +  "eventually P (sup A B) \<longleftrightarrow> eventually P A \<and> eventually P B"
   1.216 +  unfolding sup_filter_def
   1.217 +  by (rule eventually_Abs_filter, rule is_filter.intro)
   1.218 +     (auto elim!: eventually_rev_mp)
   1.219  
   1.220  lemma eventually_inf:
   1.221 -  "eventually P (inf a b) \<longleftrightarrow>
   1.222 -   (\<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.223 -unfolding inf_net_def
   1.224 -apply (rule eventually_Abs_net, rule is_filter.intro)
   1.225 -apply (fast intro: eventually_True)
   1.226 -apply clarify
   1.227 -apply (intro exI conjI)
   1.228 -apply (erule (1) eventually_conj)
   1.229 -apply (erule (1) eventually_conj)
   1.230 -apply simp
   1.231 -apply auto
   1.232 -done
   1.233 +  "eventually P (inf A B) \<longleftrightarrow>
   1.234 +   (\<exists>Q R. eventually Q A \<and> eventually R B \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.235 +  unfolding inf_filter_def
   1.236 +  apply (rule eventually_Abs_filter, rule is_filter.intro)
   1.237 +  apply (fast intro: eventually_True)
   1.238 +  apply clarify
   1.239 +  apply (intro exI conjI)
   1.240 +  apply (erule (1) eventually_conj)
   1.241 +  apply (erule (1) eventually_conj)
   1.242 +  apply simp
   1.243 +  apply auto
   1.244 +  done
   1.245  
   1.246  lemma eventually_Sup:
   1.247 -  "eventually P (Sup A) \<longleftrightarrow> (\<forall>net\<in>A. eventually P net)"
   1.248 -unfolding Sup_net_def
   1.249 -apply (rule eventually_Abs_net, rule is_filter.intro)
   1.250 -apply (auto intro: eventually_conj elim!: eventually_rev_mp)
   1.251 -done
   1.252 +  "eventually P (Sup S) \<longleftrightarrow> (\<forall>A\<in>S. eventually P A)"
   1.253 +  unfolding Sup_filter_def
   1.254 +  apply (rule eventually_Abs_filter, rule is_filter.intro)
   1.255 +  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
   1.256 +  done
   1.257  
   1.258  instance proof
   1.259 -  fix x y :: "'a net" show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
   1.260 -    by (rule less_net_def)
   1.261 +  fix A B :: "'a filter" show "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A"
   1.262 +    by (rule less_filter_def)
   1.263  next
   1.264 -  fix x :: "'a net" show "x \<le> x"
   1.265 -    unfolding le_net_def by simp
   1.266 +  fix A :: "'a filter" show "A \<le> A"
   1.267 +    unfolding le_filter_def by simp
   1.268  next
   1.269 -  fix x y z :: "'a net" assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
   1.270 -    unfolding le_net_def by simp
   1.271 +  fix A B C :: "'a filter" assume "A \<le> B" and "B \<le> C" thus "A \<le> C"
   1.272 +    unfolding le_filter_def by simp
   1.273  next
   1.274 -  fix x y :: "'a net" assume "x \<le> y" and "y \<le> x" thus "x = y"
   1.275 -    unfolding le_net_def expand_net_eq by fast
   1.276 +  fix A B :: "'a filter" assume "A \<le> B" and "B \<le> A" thus "A = B"
   1.277 +    unfolding le_filter_def filter_eq_iff by fast
   1.278  next
   1.279 -  fix x :: "'a net" show "x \<le> top"
   1.280 -    unfolding le_net_def eventually_top by (simp add: always_eventually)
   1.281 +  fix A :: "'a filter" show "A \<le> top"
   1.282 +    unfolding le_filter_def eventually_top by (simp add: always_eventually)
   1.283  next
   1.284 -  fix x :: "'a net" show "bot \<le> x"
   1.285 -    unfolding le_net_def by simp
   1.286 +  fix A :: "'a filter" show "bot \<le> A"
   1.287 +    unfolding le_filter_def by simp
   1.288  next
   1.289 -  fix x y :: "'a net" show "x \<le> sup x y" and "y \<le> sup x y"
   1.290 -    unfolding le_net_def eventually_sup by simp_all
   1.291 +  fix A B :: "'a filter" show "A \<le> sup A B" and "B \<le> sup A B"
   1.292 +    unfolding le_filter_def eventually_sup by simp_all
   1.293  next
   1.294 -  fix x y z :: "'a net" assume "x \<le> z" and "y \<le> z" thus "sup x y \<le> z"
   1.295 -    unfolding le_net_def eventually_sup by simp
   1.296 +  fix A B C :: "'a filter" assume "A \<le> C" and "B \<le> C" thus "sup A B \<le> C"
   1.297 +    unfolding le_filter_def eventually_sup by simp
   1.298  next
   1.299 -  fix x y :: "'a net" show "inf x y \<le> x" and "inf x y \<le> y"
   1.300 -    unfolding le_net_def eventually_inf by (auto intro: eventually_True)
   1.301 +  fix A B :: "'a filter" show "inf A B \<le> A" and "inf A B \<le> B"
   1.302 +    unfolding le_filter_def eventually_inf by (auto intro: eventually_True)
   1.303  next
   1.304 -  fix x y z :: "'a net" assume "x \<le> y" and "x \<le> z" thus "x \<le> inf y z"
   1.305 -    unfolding le_net_def eventually_inf
   1.306 +  fix A B C :: "'a filter" assume "A \<le> B" and "A \<le> C" thus "A \<le> inf B C"
   1.307 +    unfolding le_filter_def eventually_inf
   1.308      by (auto elim!: eventually_mono intro: eventually_conj)
   1.309  next
   1.310 -  fix x :: "'a net" and A assume "x \<in> A" thus "x \<le> Sup A"
   1.311 -    unfolding le_net_def eventually_Sup by simp
   1.312 +  fix A :: "'a filter" and S assume "A \<in> S" thus "A \<le> Sup S"
   1.313 +    unfolding le_filter_def eventually_Sup by simp
   1.314  next
   1.315 -  fix A and y :: "'a net" assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> y" thus "Sup A \<le> y"
   1.316 -    unfolding le_net_def eventually_Sup by simp
   1.317 +  fix S and B :: "'a filter" assume "\<And>A. A \<in> S \<Longrightarrow> A \<le> B" thus "Sup S \<le> B"
   1.318 +    unfolding le_filter_def eventually_Sup by simp
   1.319  next
   1.320 -  fix z :: "'a net" and A assume "z \<in> A" thus "Inf A \<le> z"
   1.321 -    unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
   1.322 +  fix C :: "'a filter" and S assume "C \<in> S" thus "Inf S \<le> C"
   1.323 +    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp
   1.324  next
   1.325 -  fix A and x :: "'a net" assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" thus "x \<le> Inf A"
   1.326 -    unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
   1.327 +  fix S and A :: "'a filter" assume "\<And>B. B \<in> S \<Longrightarrow> A \<le> B" thus "A \<le> Inf S"
   1.328 +    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp
   1.329  qed
   1.330  
   1.331  end
   1.332  
   1.333 -lemma net_leD:
   1.334 -  "net \<le> net' \<Longrightarrow> eventually P net' \<Longrightarrow> eventually P net"
   1.335 -unfolding le_net_def by simp
   1.336 +lemma filter_leD:
   1.337 +  "A \<le> B \<Longrightarrow> eventually P B \<Longrightarrow> eventually P A"
   1.338 +  unfolding le_filter_def by simp
   1.339  
   1.340 -lemma net_leI:
   1.341 -  "(\<And>P. eventually P net' \<Longrightarrow> eventually P net) \<Longrightarrow> net \<le> net'"
   1.342 -unfolding le_net_def by simp
   1.343 +lemma filter_leI:
   1.344 +  "(\<And>P. eventually P B \<Longrightarrow> eventually P A) \<Longrightarrow> A \<le> B"
   1.345 +  unfolding le_filter_def by simp
   1.346  
   1.347  lemma eventually_False:
   1.348 -  "eventually (\<lambda>x. False) net \<longleftrightarrow> net = bot"
   1.349 -unfolding expand_net_eq by (auto elim: eventually_rev_mp)
   1.350 +  "eventually (\<lambda>x. False) A \<longleftrightarrow> A = bot"
   1.351 +  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
   1.352  
   1.353 -subsection {* Map function for nets *}
   1.354 +subsection {* Map function for filters *}
   1.355  
   1.356 -definition netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net" where
   1.357 -  "netmap f net = Abs_net (\<lambda>P. eventually (\<lambda>x. P (f x)) net)"
   1.358 +definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
   1.359 +  where "filtermap f A = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) A)"
   1.360  
   1.361 -lemma eventually_netmap:
   1.362 -  "eventually P (netmap f net) = eventually (\<lambda>x. P (f x)) net"
   1.363 -unfolding netmap_def
   1.364 -apply (rule eventually_Abs_net)
   1.365 -apply (rule is_filter.intro)
   1.366 -apply (auto elim!: eventually_rev_mp)
   1.367 -done
   1.368 +lemma eventually_filtermap:
   1.369 +  "eventually P (filtermap f A) = eventually (\<lambda>x. P (f x)) A"
   1.370 +  unfolding filtermap_def
   1.371 +  apply (rule eventually_Abs_filter)
   1.372 +  apply (rule is_filter.intro)
   1.373 +  apply (auto elim!: eventually_rev_mp)
   1.374 +  done
   1.375  
   1.376 -lemma netmap_ident: "netmap (\<lambda>x. x) net = net"
   1.377 -by (simp add: expand_net_eq eventually_netmap)
   1.378 -
   1.379 -lemma netmap_netmap: "netmap f (netmap g net) = netmap (\<lambda>x. f (g x)) net"
   1.380 -by (simp add: expand_net_eq eventually_netmap)
   1.381 +lemma filtermap_ident: "filtermap (\<lambda>x. x) A = A"
   1.382 +  by (simp add: filter_eq_iff eventually_filtermap)
   1.383  
   1.384 -lemma netmap_mono: "net \<le> net' \<Longrightarrow> netmap f net \<le> netmap f net'"
   1.385 -unfolding le_net_def eventually_netmap by simp
   1.386 +lemma filtermap_filtermap:
   1.387 +  "filtermap f (filtermap g A) = filtermap (\<lambda>x. f (g x)) A"
   1.388 +  by (simp add: filter_eq_iff eventually_filtermap)
   1.389  
   1.390 -lemma netmap_bot [simp]: "netmap f bot = bot"
   1.391 -by (simp add: expand_net_eq eventually_netmap)
   1.392 +lemma filtermap_mono: "A \<le> B \<Longrightarrow> filtermap f A \<le> filtermap f B"
   1.393 +  unfolding le_filter_def eventually_filtermap by simp
   1.394 +
   1.395 +lemma filtermap_bot [simp]: "filtermap f bot = bot"
   1.396 +  by (simp add: filter_eq_iff eventually_filtermap)
   1.397  
   1.398  
   1.399  subsection {* Sequentially *}
   1.400  
   1.401 -definition sequentially :: "nat net" where
   1.402 -  "sequentially = Abs_net (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
   1.403 +definition sequentially :: "nat filter"
   1.404 +  where "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
   1.405  
   1.406  lemma eventually_sequentially:
   1.407    "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   1.408  unfolding sequentially_def
   1.409 -proof (rule eventually_Abs_net, rule is_filter.intro)
   1.410 +proof (rule eventually_Abs_filter, rule is_filter.intro)
   1.411    fix P Q :: "nat \<Rightarrow> bool"
   1.412    assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
   1.413    then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
   1.414 @@ -273,49 +272,48 @@
   1.415  qed auto
   1.416  
   1.417  lemma sequentially_bot [simp]: "sequentially \<noteq> bot"
   1.418 -unfolding expand_net_eq eventually_sequentially by auto
   1.419 +  unfolding filter_eq_iff eventually_sequentially by auto
   1.420  
   1.421  lemma eventually_False_sequentially [simp]:
   1.422    "\<not> eventually (\<lambda>n. False) sequentially"
   1.423 -by (simp add: eventually_False)
   1.424 +  by (simp add: eventually_False)
   1.425  
   1.426  lemma le_sequentially:
   1.427 -  "net \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) net)"
   1.428 -unfolding le_net_def eventually_sequentially
   1.429 -by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
   1.430 +  "A \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) A)"
   1.431 +  unfolding le_filter_def eventually_sequentially
   1.432 +  by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
   1.433  
   1.434  
   1.435 -definition
   1.436 -  trivial_limit :: "'a net \<Rightarrow> bool" where
   1.437 -  "trivial_limit net \<longleftrightarrow> eventually (\<lambda>x. False) net"
   1.438 +definition trivial_limit :: "'a filter \<Rightarrow> bool"
   1.439 +  where "trivial_limit A \<longleftrightarrow> eventually (\<lambda>x. False) A"
   1.440  
   1.441 -lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
   1.442 +lemma trivial_limit_sequentially [intro]: "\<not> trivial_limit sequentially"
   1.443    by (auto simp add: trivial_limit_def eventually_sequentially)
   1.444  
   1.445 -subsection {* Standard Nets *}
   1.446 +subsection {* Standard filters *}
   1.447  
   1.448 -definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
   1.449 -  "net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
   1.450 +definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
   1.451 +  where "A within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) A)"
   1.452  
   1.453 -definition nhds :: "'a::topological_space \<Rightarrow> 'a net" where
   1.454 -  "nhds a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   1.455 +definition nhds :: "'a::topological_space \<Rightarrow> 'a filter"
   1.456 +  where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   1.457  
   1.458 -definition at :: "'a::topological_space \<Rightarrow> 'a net" where
   1.459 -  "at a = nhds a within - {a}"
   1.460 +definition at :: "'a::topological_space \<Rightarrow> 'a filter"
   1.461 +  where "at a = nhds a within - {a}"
   1.462  
   1.463  lemma eventually_within:
   1.464 -  "eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
   1.465 -unfolding within_def
   1.466 -by (rule eventually_Abs_net, rule is_filter.intro)
   1.467 -   (auto elim!: eventually_rev_mp)
   1.468 +  "eventually P (A within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) A"
   1.469 +  unfolding within_def
   1.470 +  by (rule eventually_Abs_filter, rule is_filter.intro)
   1.471 +     (auto elim!: eventually_rev_mp)
   1.472  
   1.473 -lemma within_UNIV: "net within UNIV = net"
   1.474 -  unfolding expand_net_eq eventually_within by simp
   1.475 +lemma within_UNIV: "A within UNIV = A"
   1.476 +  unfolding filter_eq_iff eventually_within by simp
   1.477  
   1.478  lemma eventually_nhds:
   1.479    "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   1.480  unfolding nhds_def
   1.481 -proof (rule eventually_Abs_net, rule is_filter.intro)
   1.482 +proof (rule eventually_Abs_filter, rule is_filter.intro)
   1.483    have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp
   1.484    thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" by - rule
   1.485  next
   1.486 @@ -354,52 +352,52 @@
   1.487  
   1.488  subsection {* Boundedness *}
   1.489  
   1.490 -definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
   1.491 -  "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
   1.492 +definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
   1.493 +  where "Bfun f A = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) A)"
   1.494  
   1.495  lemma BfunI:
   1.496 -  assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) net" shows "Bfun f net"
   1.497 +  assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) A" shows "Bfun f A"
   1.498  unfolding Bfun_def
   1.499  proof (intro exI conjI allI)
   1.500    show "0 < max K 1" by simp
   1.501  next
   1.502 -  show "eventually (\<lambda>x. norm (f x) \<le> max K 1) net"
   1.503 +  show "eventually (\<lambda>x. norm (f x) \<le> max K 1) A"
   1.504      using K by (rule eventually_elim1, simp)
   1.505  qed
   1.506  
   1.507  lemma BfunE:
   1.508 -  assumes "Bfun f net"
   1.509 -  obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) net"
   1.510 +  assumes "Bfun f A"
   1.511 +  obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) A"
   1.512  using assms unfolding Bfun_def by fast
   1.513  
   1.514  
   1.515  subsection {* Convergence to Zero *}
   1.516  
   1.517 -definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
   1.518 -  "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
   1.519 +definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
   1.520 +  where "Zfun f A = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) A)"
   1.521  
   1.522  lemma ZfunI:
   1.523 -  "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net) \<Longrightarrow> Zfun f net"
   1.524 -unfolding Zfun_def by simp
   1.525 +  "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) A) \<Longrightarrow> Zfun f A"
   1.526 +  unfolding Zfun_def by simp
   1.527  
   1.528  lemma ZfunD:
   1.529 -  "\<lbrakk>Zfun f net; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net"
   1.530 -unfolding Zfun_def by simp
   1.531 +  "\<lbrakk>Zfun f A; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) A"
   1.532 +  unfolding Zfun_def by simp
   1.533  
   1.534  lemma Zfun_ssubst:
   1.535 -  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> Zfun g net \<Longrightarrow> Zfun f net"
   1.536 -unfolding Zfun_def by (auto elim!: eventually_rev_mp)
   1.537 +  "eventually (\<lambda>x. f x = g x) A \<Longrightarrow> Zfun g A \<Longrightarrow> Zfun f A"
   1.538 +  unfolding Zfun_def by (auto elim!: eventually_rev_mp)
   1.539  
   1.540 -lemma Zfun_zero: "Zfun (\<lambda>x. 0) net"
   1.541 -unfolding Zfun_def by simp
   1.542 +lemma Zfun_zero: "Zfun (\<lambda>x. 0) A"
   1.543 +  unfolding Zfun_def by simp
   1.544  
   1.545 -lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) net = Zfun (\<lambda>x. f x) net"
   1.546 -unfolding Zfun_def by simp
   1.547 +lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) A = Zfun (\<lambda>x. f x) A"
   1.548 +  unfolding Zfun_def by simp
   1.549  
   1.550  lemma Zfun_imp_Zfun:
   1.551 -  assumes f: "Zfun f net"
   1.552 -  assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) net"
   1.553 -  shows "Zfun (\<lambda>x. g x) net"
   1.554 +  assumes f: "Zfun f A"
   1.555 +  assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) A"
   1.556 +  shows "Zfun (\<lambda>x. g x) A"
   1.557  proof (cases)
   1.558    assume K: "0 < K"
   1.559    show ?thesis
   1.560 @@ -407,9 +405,9 @@
   1.561      fix r::real assume "0 < r"
   1.562      hence "0 < r / K"
   1.563        using K by (rule divide_pos_pos)
   1.564 -    then have "eventually (\<lambda>x. norm (f x) < r / K) net"
   1.565 +    then have "eventually (\<lambda>x. norm (f x) < r / K) A"
   1.566        using ZfunD [OF f] by fast
   1.567 -    with g show "eventually (\<lambda>x. norm (g x) < r) net"
   1.568 +    with g show "eventually (\<lambda>x. norm (g x) < r) A"
   1.569      proof (rule eventually_elim2)
   1.570        fix x
   1.571        assume *: "norm (g x) \<le> norm (f x) * K"
   1.572 @@ -427,7 +425,7 @@
   1.573    proof (rule ZfunI)
   1.574      fix r :: real
   1.575      assume "0 < r"
   1.576 -    from g show "eventually (\<lambda>x. norm (g x) < r) net"
   1.577 +    from g show "eventually (\<lambda>x. norm (g x) < r) A"
   1.578      proof (rule eventually_elim1)
   1.579        fix x
   1.580        assume "norm (g x) \<le> norm (f x) * K"
   1.581 @@ -439,22 +437,22 @@
   1.582    qed
   1.583  qed
   1.584  
   1.585 -lemma Zfun_le: "\<lbrakk>Zfun g net; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f net"
   1.586 -by (erule_tac K="1" in Zfun_imp_Zfun, simp)
   1.587 +lemma Zfun_le: "\<lbrakk>Zfun g A; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f A"
   1.588 +  by (erule_tac K="1" in Zfun_imp_Zfun, simp)
   1.589  
   1.590  lemma Zfun_add:
   1.591 -  assumes f: "Zfun f net" and g: "Zfun g net"
   1.592 -  shows "Zfun (\<lambda>x. f x + g x) net"
   1.593 +  assumes f: "Zfun f A" and g: "Zfun g A"
   1.594 +  shows "Zfun (\<lambda>x. f x + g x) A"
   1.595  proof (rule ZfunI)
   1.596    fix r::real assume "0 < r"
   1.597    hence r: "0 < r / 2" by simp
   1.598 -  have "eventually (\<lambda>x. norm (f x) < r/2) net"
   1.599 +  have "eventually (\<lambda>x. norm (f x) < r/2) A"
   1.600      using f r by (rule ZfunD)
   1.601    moreover
   1.602 -  have "eventually (\<lambda>x. norm (g x) < r/2) net"
   1.603 +  have "eventually (\<lambda>x. norm (g x) < r/2) A"
   1.604      using g r by (rule ZfunD)
   1.605    ultimately
   1.606 -  show "eventually (\<lambda>x. norm (f x + g x) < r) net"
   1.607 +  show "eventually (\<lambda>x. norm (f x + g x) < r) A"
   1.608    proof (rule eventually_elim2)
   1.609      fix x
   1.610      assume *: "norm (f x) < r/2" "norm (g x) < r/2"
   1.611 @@ -467,28 +465,28 @@
   1.612    qed
   1.613  qed
   1.614  
   1.615 -lemma Zfun_minus: "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. - f x) net"
   1.616 -unfolding Zfun_def by simp
   1.617 +lemma Zfun_minus: "Zfun f A \<Longrightarrow> Zfun (\<lambda>x. - f x) A"
   1.618 +  unfolding Zfun_def by simp
   1.619  
   1.620 -lemma Zfun_diff: "\<lbrakk>Zfun f net; Zfun g net\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) net"
   1.621 -by (simp only: diff_minus Zfun_add Zfun_minus)
   1.622 +lemma Zfun_diff: "\<lbrakk>Zfun f A; Zfun g A\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) A"
   1.623 +  by (simp only: diff_minus Zfun_add Zfun_minus)
   1.624  
   1.625  lemma (in bounded_linear) Zfun:
   1.626 -  assumes g: "Zfun g net"
   1.627 -  shows "Zfun (\<lambda>x. f (g x)) net"
   1.628 +  assumes g: "Zfun g A"
   1.629 +  shows "Zfun (\<lambda>x. f (g x)) A"
   1.630  proof -
   1.631    obtain K where "\<And>x. norm (f x) \<le> norm x * K"
   1.632      using bounded by fast
   1.633 -  then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) net"
   1.634 +  then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) A"
   1.635      by simp
   1.636    with g show ?thesis
   1.637      by (rule Zfun_imp_Zfun)
   1.638  qed
   1.639  
   1.640  lemma (in bounded_bilinear) Zfun:
   1.641 -  assumes f: "Zfun f net"
   1.642 -  assumes g: "Zfun g net"
   1.643 -  shows "Zfun (\<lambda>x. f x ** g x) net"
   1.644 +  assumes f: "Zfun f A"
   1.645 +  assumes g: "Zfun g A"
   1.646 +  shows "Zfun (\<lambda>x. f x ** g x) A"
   1.647  proof (rule ZfunI)
   1.648    fix r::real assume r: "0 < r"
   1.649    obtain K where K: "0 < K"
   1.650 @@ -496,13 +494,13 @@
   1.651      using pos_bounded by fast
   1.652    from K have K': "0 < inverse K"
   1.653      by (rule positive_imp_inverse_positive)
   1.654 -  have "eventually (\<lambda>x. norm (f x) < r) net"
   1.655 +  have "eventually (\<lambda>x. norm (f x) < r) A"
   1.656      using f r by (rule ZfunD)
   1.657    moreover
   1.658 -  have "eventually (\<lambda>x. norm (g x) < inverse K) net"
   1.659 +  have "eventually (\<lambda>x. norm (g x) < inverse K) A"
   1.660      using g K' by (rule ZfunD)
   1.661    ultimately
   1.662 -  show "eventually (\<lambda>x. norm (f x ** g x) < r) net"
   1.663 +  show "eventually (\<lambda>x. norm (f x ** g x) < r) A"
   1.664    proof (rule eventually_elim2)
   1.665      fix x
   1.666      assume *: "norm (f x) < r" "norm (g x) < inverse K"
   1.667 @@ -517,12 +515,12 @@
   1.668  qed
   1.669  
   1.670  lemma (in bounded_bilinear) Zfun_left:
   1.671 -  "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. f x ** a) net"
   1.672 -by (rule bounded_linear_left [THEN bounded_linear.Zfun])
   1.673 +  "Zfun f A \<Longrightarrow> Zfun (\<lambda>x. f x ** a) A"
   1.674 +  by (rule bounded_linear_left [THEN bounded_linear.Zfun])
   1.675  
   1.676  lemma (in bounded_bilinear) Zfun_right:
   1.677 -  "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. a ** f x) net"
   1.678 -by (rule bounded_linear_right [THEN bounded_linear.Zfun])
   1.679 +  "Zfun f A \<Longrightarrow> Zfun (\<lambda>x. a ** f x) A"
   1.680 +  by (rule bounded_linear_right [THEN bounded_linear.Zfun])
   1.681  
   1.682  lemmas Zfun_mult = mult.Zfun
   1.683  lemmas Zfun_mult_right = mult.Zfun_right
   1.684 @@ -531,9 +529,9 @@
   1.685  
   1.686  subsection {* Limits *}
   1.687  
   1.688 -definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
   1.689 +definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool"
   1.690      (infixr "--->" 55) where
   1.691 -  "(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
   1.692 +  "(f ---> l) A \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) A)"
   1.693  
   1.694  ML {*
   1.695  structure Tendsto_Intros = Named_Thms
   1.696 @@ -545,74 +543,74 @@
   1.697  
   1.698  setup Tendsto_Intros.setup
   1.699  
   1.700 -lemma tendsto_mono: "net \<le> net' \<Longrightarrow> (f ---> l) net' \<Longrightarrow> (f ---> l) net"
   1.701 -unfolding tendsto_def le_net_def by fast
   1.702 +lemma tendsto_mono: "A \<le> A' \<Longrightarrow> (f ---> l) A' \<Longrightarrow> (f ---> l) A"
   1.703 +  unfolding tendsto_def le_filter_def by fast
   1.704  
   1.705  lemma topological_tendstoI:
   1.706 -  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
   1.707 -    \<Longrightarrow> (f ---> l) net"
   1.708 +  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) A)
   1.709 +    \<Longrightarrow> (f ---> l) A"
   1.710    unfolding tendsto_def by auto
   1.711  
   1.712  lemma topological_tendstoD:
   1.713 -  "(f ---> l) net \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
   1.714 +  "(f ---> l) A \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) A"
   1.715    unfolding tendsto_def by auto
   1.716  
   1.717  lemma tendstoI:
   1.718 -  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
   1.719 -  shows "(f ---> l) net"
   1.720 -apply (rule topological_tendstoI)
   1.721 -apply (simp add: open_dist)
   1.722 -apply (drule (1) bspec, clarify)
   1.723 -apply (drule assms)
   1.724 -apply (erule eventually_elim1, simp)
   1.725 -done
   1.726 +  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) A"
   1.727 +  shows "(f ---> l) A"
   1.728 +  apply (rule topological_tendstoI)
   1.729 +  apply (simp add: open_dist)
   1.730 +  apply (drule (1) bspec, clarify)
   1.731 +  apply (drule assms)
   1.732 +  apply (erule eventually_elim1, simp)
   1.733 +  done
   1.734  
   1.735  lemma tendstoD:
   1.736 -  "(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
   1.737 -apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
   1.738 -apply (clarsimp simp add: open_dist)
   1.739 -apply (rule_tac x="e - dist x l" in exI, clarsimp)
   1.740 -apply (simp only: less_diff_eq)
   1.741 -apply (erule le_less_trans [OF dist_triangle])
   1.742 -apply simp
   1.743 -apply simp
   1.744 -done
   1.745 +  "(f ---> l) A \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) A"
   1.746 +  apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
   1.747 +  apply (clarsimp simp add: open_dist)
   1.748 +  apply (rule_tac x="e - dist x l" in exI, clarsimp)
   1.749 +  apply (simp only: less_diff_eq)
   1.750 +  apply (erule le_less_trans [OF dist_triangle])
   1.751 +  apply simp
   1.752 +  apply simp
   1.753 +  done
   1.754  
   1.755  lemma tendsto_iff:
   1.756 -  "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
   1.757 -using tendstoI tendstoD by fast
   1.758 +  "(f ---> l) A \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) A)"
   1.759 +  using tendstoI tendstoD by fast
   1.760  
   1.761 -lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\<lambda>x. f x - a) net"
   1.762 -by (simp only: tendsto_iff Zfun_def dist_norm)
   1.763 +lemma tendsto_Zfun_iff: "(f ---> a) A = Zfun (\<lambda>x. f x - a) A"
   1.764 +  by (simp only: tendsto_iff Zfun_def dist_norm)
   1.765  
   1.766  lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
   1.767 -unfolding tendsto_def eventually_at_topological by auto
   1.768 +  unfolding tendsto_def eventually_at_topological by auto
   1.769  
   1.770  lemma tendsto_ident_at_within [tendsto_intros]:
   1.771    "((\<lambda>x. x) ---> a) (at a within S)"
   1.772 -unfolding tendsto_def eventually_within eventually_at_topological by auto
   1.773 +  unfolding tendsto_def eventually_within eventually_at_topological by auto
   1.774  
   1.775 -lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) net"
   1.776 -by (simp add: tendsto_def)
   1.777 +lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) A"
   1.778 +  by (simp add: tendsto_def)
   1.779  
   1.780  lemma tendsto_const_iff:
   1.781    fixes k l :: "'a::metric_space"
   1.782 -  assumes "net \<noteq> bot" shows "((\<lambda>n. k) ---> l) net \<longleftrightarrow> k = l"
   1.783 -apply (safe intro!: tendsto_const)
   1.784 -apply (rule ccontr)
   1.785 -apply (drule_tac e="dist k l" in tendstoD)
   1.786 -apply (simp add: zero_less_dist_iff)
   1.787 -apply (simp add: eventually_False assms)
   1.788 -done
   1.789 +  assumes "A \<noteq> bot" shows "((\<lambda>n. k) ---> l) A \<longleftrightarrow> k = l"
   1.790 +  apply (safe intro!: tendsto_const)
   1.791 +  apply (rule ccontr)
   1.792 +  apply (drule_tac e="dist k l" in tendstoD)
   1.793 +  apply (simp add: zero_less_dist_iff)
   1.794 +  apply (simp add: eventually_False assms)
   1.795 +  done
   1.796  
   1.797  lemma tendsto_dist [tendsto_intros]:
   1.798 -  assumes f: "(f ---> l) net" and g: "(g ---> m) net"
   1.799 -  shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) net"
   1.800 +  assumes f: "(f ---> l) A" and g: "(g ---> m) A"
   1.801 +  shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) A"
   1.802  proof (rule tendstoI)
   1.803    fix e :: real assume "0 < e"
   1.804    hence e2: "0 < e/2" by simp
   1.805    from tendstoD [OF f e2] tendstoD [OF g e2]
   1.806 -  show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) net"
   1.807 +  show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) A"
   1.808    proof (rule eventually_elim2)
   1.809      fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2"
   1.810      then show "dist (dist (f x) (g x)) (dist l m) < e"
   1.811 @@ -626,48 +624,48 @@
   1.812  qed
   1.813  
   1.814  lemma norm_conv_dist: "norm x = dist x 0"
   1.815 -unfolding dist_norm by simp
   1.816 +  unfolding dist_norm by simp
   1.817  
   1.818  lemma tendsto_norm [tendsto_intros]:
   1.819 -  "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
   1.820 -unfolding norm_conv_dist by (intro tendsto_intros)
   1.821 +  "(f ---> a) A \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) A"
   1.822 +  unfolding norm_conv_dist by (intro tendsto_intros)
   1.823  
   1.824  lemma tendsto_norm_zero:
   1.825 -  "(f ---> 0) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) net"
   1.826 -by (drule tendsto_norm, simp)
   1.827 +  "(f ---> 0) A \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) A"
   1.828 +  by (drule tendsto_norm, simp)
   1.829  
   1.830  lemma tendsto_norm_zero_cancel:
   1.831 -  "((\<lambda>x. norm (f x)) ---> 0) net \<Longrightarrow> (f ---> 0) net"
   1.832 -unfolding tendsto_iff dist_norm by simp
   1.833 +  "((\<lambda>x. norm (f x)) ---> 0) A \<Longrightarrow> (f ---> 0) A"
   1.834 +  unfolding tendsto_iff dist_norm by simp
   1.835  
   1.836  lemma tendsto_norm_zero_iff:
   1.837 -  "((\<lambda>x. norm (f x)) ---> 0) net \<longleftrightarrow> (f ---> 0) net"
   1.838 -unfolding tendsto_iff dist_norm by simp
   1.839 +  "((\<lambda>x. norm (f x)) ---> 0) A \<longleftrightarrow> (f ---> 0) A"
   1.840 +  unfolding tendsto_iff dist_norm by simp
   1.841  
   1.842  lemma tendsto_add [tendsto_intros]:
   1.843    fixes a b :: "'a::real_normed_vector"
   1.844 -  shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) net"
   1.845 -by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
   1.846 +  shows "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) A"
   1.847 +  by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
   1.848  
   1.849  lemma tendsto_minus [tendsto_intros]:
   1.850    fixes a :: "'a::real_normed_vector"
   1.851 -  shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) net"
   1.852 -by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
   1.853 +  shows "(f ---> a) A \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) A"
   1.854 +  by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
   1.855  
   1.856  lemma tendsto_minus_cancel:
   1.857    fixes a :: "'a::real_normed_vector"
   1.858 -  shows "((\<lambda>x. - f x) ---> - a) net \<Longrightarrow> (f ---> a) net"
   1.859 -by (drule tendsto_minus, simp)
   1.860 +  shows "((\<lambda>x. - f x) ---> - a) A \<Longrightarrow> (f ---> a) A"
   1.861 +  by (drule tendsto_minus, simp)
   1.862  
   1.863  lemma tendsto_diff [tendsto_intros]:
   1.864    fixes a b :: "'a::real_normed_vector"
   1.865 -  shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) net"
   1.866 -by (simp add: diff_minus tendsto_add tendsto_minus)
   1.867 +  shows "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) A"
   1.868 +  by (simp add: diff_minus tendsto_add tendsto_minus)
   1.869  
   1.870  lemma tendsto_setsum [tendsto_intros]:
   1.871    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
   1.872 -  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) net"
   1.873 -  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) net"
   1.874 +  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) A"
   1.875 +  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) A"
   1.876  proof (cases "finite S")
   1.877    assume "finite S" thus ?thesis using assms
   1.878    proof (induct set: finite)
   1.879 @@ -683,29 +681,29 @@
   1.880  qed
   1.881  
   1.882  lemma (in bounded_linear) tendsto [tendsto_intros]:
   1.883 -  "(g ---> a) net \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) net"
   1.884 -by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
   1.885 +  "(g ---> a) A \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) A"
   1.886 +  by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
   1.887  
   1.888  lemma (in bounded_bilinear) tendsto [tendsto_intros]:
   1.889 -  "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) net"
   1.890 -by (simp only: tendsto_Zfun_iff prod_diff_prod
   1.891 -               Zfun_add Zfun Zfun_left Zfun_right)
   1.892 +  "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) A"
   1.893 +  by (simp only: tendsto_Zfun_iff prod_diff_prod
   1.894 +                 Zfun_add Zfun Zfun_left Zfun_right)
   1.895  
   1.896  
   1.897  subsection {* Continuity of Inverse *}
   1.898  
   1.899  lemma (in bounded_bilinear) Zfun_prod_Bfun:
   1.900 -  assumes f: "Zfun f net"
   1.901 -  assumes g: "Bfun g net"
   1.902 -  shows "Zfun (\<lambda>x. f x ** g x) net"
   1.903 +  assumes f: "Zfun f A"
   1.904 +  assumes g: "Bfun g A"
   1.905 +  shows "Zfun (\<lambda>x. f x ** g x) A"
   1.906  proof -
   1.907    obtain K where K: "0 \<le> K"
   1.908      and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
   1.909      using nonneg_bounded by fast
   1.910    obtain B where B: "0 < B"
   1.911 -    and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) net"
   1.912 +    and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) A"
   1.913      using g by (rule BfunE)
   1.914 -  have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) net"
   1.915 +  have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) A"
   1.916    using norm_g proof (rule eventually_elim1)
   1.917      fix x
   1.918      assume *: "norm (g x) \<le> B"
   1.919 @@ -724,39 +722,39 @@
   1.920  
   1.921  lemma (in bounded_bilinear) flip:
   1.922    "bounded_bilinear (\<lambda>x y. y ** x)"
   1.923 -apply default
   1.924 -apply (rule add_right)
   1.925 -apply (rule add_left)
   1.926 -apply (rule scaleR_right)
   1.927 -apply (rule scaleR_left)
   1.928 -apply (subst mult_commute)
   1.929 -using bounded by fast
   1.930 +  apply default
   1.931 +  apply (rule add_right)
   1.932 +  apply (rule add_left)
   1.933 +  apply (rule scaleR_right)
   1.934 +  apply (rule scaleR_left)
   1.935 +  apply (subst mult_commute)
   1.936 +  using bounded by fast
   1.937  
   1.938  lemma (in bounded_bilinear) Bfun_prod_Zfun:
   1.939 -  assumes f: "Bfun f net"
   1.940 -  assumes g: "Zfun g net"
   1.941 -  shows "Zfun (\<lambda>x. f x ** g x) net"
   1.942 -using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
   1.943 +  assumes f: "Bfun f A"
   1.944 +  assumes g: "Zfun g A"
   1.945 +  shows "Zfun (\<lambda>x. f x ** g x) A"
   1.946 +  using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
   1.947  
   1.948  lemma Bfun_inverse_lemma:
   1.949    fixes x :: "'a::real_normed_div_algebra"
   1.950    shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
   1.951 -apply (subst nonzero_norm_inverse, clarsimp)
   1.952 -apply (erule (1) le_imp_inverse_le)
   1.953 -done
   1.954 +  apply (subst nonzero_norm_inverse, clarsimp)
   1.955 +  apply (erule (1) le_imp_inverse_le)
   1.956 +  done
   1.957  
   1.958  lemma Bfun_inverse:
   1.959    fixes a :: "'a::real_normed_div_algebra"
   1.960 -  assumes f: "(f ---> a) net"
   1.961 +  assumes f: "(f ---> a) A"
   1.962    assumes a: "a \<noteq> 0"
   1.963 -  shows "Bfun (\<lambda>x. inverse (f x)) net"
   1.964 +  shows "Bfun (\<lambda>x. inverse (f x)) A"
   1.965  proof -
   1.966    from a have "0 < norm a" by simp
   1.967    hence "\<exists>r>0. r < norm a" by (rule dense)
   1.968    then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
   1.969 -  have "eventually (\<lambda>x. dist (f x) a < r) net"
   1.970 +  have "eventually (\<lambda>x. dist (f x) a < r) A"
   1.971      using tendstoD [OF f r1] by fast
   1.972 -  hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) net"
   1.973 +  hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) A"
   1.974    proof (rule eventually_elim1)
   1.975      fix x
   1.976      assume "dist (f x) a < r"
   1.977 @@ -783,29 +781,29 @@
   1.978  
   1.979  lemma tendsto_inverse_lemma:
   1.980    fixes a :: "'a::real_normed_div_algebra"
   1.981 -  shows "\<lbrakk>(f ---> a) net; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) net\<rbrakk>
   1.982 -         \<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) net"
   1.983 -apply (subst tendsto_Zfun_iff)
   1.984 -apply (rule Zfun_ssubst)
   1.985 -apply (erule eventually_elim1)
   1.986 -apply (erule (1) inverse_diff_inverse)
   1.987 -apply (rule Zfun_minus)
   1.988 -apply (rule Zfun_mult_left)
   1.989 -apply (rule mult.Bfun_prod_Zfun)
   1.990 -apply (erule (1) Bfun_inverse)
   1.991 -apply (simp add: tendsto_Zfun_iff)
   1.992 -done
   1.993 +  shows "\<lbrakk>(f ---> a) A; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) A\<rbrakk>
   1.994 +         \<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) A"
   1.995 +  apply (subst tendsto_Zfun_iff)
   1.996 +  apply (rule Zfun_ssubst)
   1.997 +  apply (erule eventually_elim1)
   1.998 +  apply (erule (1) inverse_diff_inverse)
   1.999 +  apply (rule Zfun_minus)
  1.1000 +  apply (rule Zfun_mult_left)
  1.1001 +  apply (rule mult.Bfun_prod_Zfun)
  1.1002 +  apply (erule (1) Bfun_inverse)
  1.1003 +  apply (simp add: tendsto_Zfun_iff)
  1.1004 +  done
  1.1005  
  1.1006  lemma tendsto_inverse [tendsto_intros]:
  1.1007    fixes a :: "'a::real_normed_div_algebra"
  1.1008 -  assumes f: "(f ---> a) net"
  1.1009 +  assumes f: "(f ---> a) A"
  1.1010    assumes a: "a \<noteq> 0"
  1.1011 -  shows "((\<lambda>x. inverse (f x)) ---> inverse a) net"
  1.1012 +  shows "((\<lambda>x. inverse (f x)) ---> inverse a) A"
  1.1013  proof -
  1.1014    from a have "0 < norm a" by simp
  1.1015 -  with f have "eventually (\<lambda>x. dist (f x) a < norm a) net"
  1.1016 +  with f have "eventually (\<lambda>x. dist (f x) a < norm a) A"
  1.1017      by (rule tendstoD)
  1.1018 -  then have "eventually (\<lambda>x. f x \<noteq> 0) net"
  1.1019 +  then have "eventually (\<lambda>x. f x \<noteq> 0) A"
  1.1020      unfolding dist_norm by (auto elim!: eventually_elim1)
  1.1021    with f a show ?thesis
  1.1022      by (rule tendsto_inverse_lemma)
  1.1023 @@ -813,32 +811,32 @@
  1.1024  
  1.1025  lemma tendsto_divide [tendsto_intros]:
  1.1026    fixes a b :: "'a::real_normed_field"
  1.1027 -  shows "\<lbrakk>(f ---> a) net; (g ---> b) net; b \<noteq> 0\<rbrakk>
  1.1028 -    \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) net"
  1.1029 -by (simp add: mult.tendsto tendsto_inverse divide_inverse)
  1.1030 +  shows "\<lbrakk>(f ---> a) A; (g ---> b) A; b \<noteq> 0\<rbrakk>
  1.1031 +    \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) A"
  1.1032 +  by (simp add: mult.tendsto tendsto_inverse divide_inverse)
  1.1033  
  1.1034  lemma tendsto_unique:
  1.1035    fixes f :: "'a \<Rightarrow> 'b::t2_space"
  1.1036 -  assumes "\<not> trivial_limit net"  "(f ---> l) net"  "(f ---> l') net"
  1.1037 +  assumes "\<not> trivial_limit A"  "(f ---> l) A"  "(f ---> l') A"
  1.1038    shows "l = l'"
  1.1039  proof (rule ccontr)
  1.1040    assume "l \<noteq> l'"
  1.1041    obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
  1.1042      using hausdorff [OF `l \<noteq> l'`] by fast
  1.1043 -  have "eventually (\<lambda>x. f x \<in> U) net"
  1.1044 -    using `(f ---> l) net` `open U` `l \<in> U` by (rule topological_tendstoD)
  1.1045 +  have "eventually (\<lambda>x. f x \<in> U) A"
  1.1046 +    using `(f ---> l) A` `open U` `l \<in> U` by (rule topological_tendstoD)
  1.1047    moreover
  1.1048 -  have "eventually (\<lambda>x. f x \<in> V) net"
  1.1049 -    using `(f ---> l') net` `open V` `l' \<in> V` by (rule topological_tendstoD)
  1.1050 +  have "eventually (\<lambda>x. f x \<in> V) A"
  1.1051 +    using `(f ---> l') A` `open V` `l' \<in> V` by (rule topological_tendstoD)
  1.1052    ultimately
  1.1053 -  have "eventually (\<lambda>x. False) net"
  1.1054 +  have "eventually (\<lambda>x. False) A"
  1.1055    proof (rule eventually_elim2)
  1.1056      fix x
  1.1057      assume "f x \<in> U" "f x \<in> V"
  1.1058      hence "f x \<in> U \<inter> V" by simp
  1.1059      with `U \<inter> V = {}` show "False" by simp
  1.1060    qed
  1.1061 -  with `\<not> trivial_limit net` show "False"
  1.1062 +  with `\<not> trivial_limit A` show "False"
  1.1063      by (simp add: trivial_limit_def)
  1.1064  qed
  1.1065