replace filters with filter bases
authorhuffman
Tue Jun 02 17:03:22 2009 -0700 (2009-06-02)
changeset 3139269570155ddf8
parent 31391 97a2a3d4088e
child 31393 b8570dead501
replace filters with filter bases
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Lim.thy	Tue Jun 02 15:37:59 2009 -0700
     1.2 +++ b/src/HOL/Lim.thy	Tue Jun 02 17:03:22 2009 -0700
     1.3 @@ -13,10 +13,6 @@
     1.4  text{*Standard Definitions*}
     1.5  
     1.6  definition
     1.7 -  at :: "'a::metric_space \<Rightarrow> 'a filter" where
     1.8 -  [code del]: "at a = Abs_filter (\<lambda>P. \<exists>r>0. \<forall>x. x \<noteq> a \<and> dist x a < r \<longrightarrow> P x)"
     1.9 -
    1.10 -definition
    1.11    LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
    1.12          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
    1.13    [code del]: "f -- a --> L =
    1.14 @@ -31,23 +27,11 @@
    1.15    isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
    1.16    [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
    1.17  
    1.18 -subsection {* Neighborhood Filter *}
    1.19 -
    1.20 -lemma eventually_at:
    1.21 -  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
    1.22 -unfolding at_def
    1.23 -apply (rule eventually_Abs_filter)
    1.24 -apply (rule_tac x=1 in exI, simp)
    1.25 -apply (clarify, rule_tac x=r in exI, simp)
    1.26 -apply (clarify, rename_tac r s)
    1.27 -apply (rule_tac x="min r s" in exI, simp)
    1.28 -done
    1.29 +subsection {* Limits of Functions *}
    1.30  
    1.31  lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> tendsto f L (at a)"
    1.32  unfolding LIM_def tendsto_def eventually_at ..
    1.33  
    1.34 -subsection {* Limits of Functions *}
    1.35 -
    1.36  lemma metric_LIM_I:
    1.37    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
    1.38      \<Longrightarrow> f -- a --> L"
     2.1 --- a/src/HOL/Limits.thy	Tue Jun 02 15:37:59 2009 -0700
     2.2 +++ b/src/HOL/Limits.thy	Tue Jun 02 17:03:22 2009 -0700
     2.3 @@ -8,128 +8,204 @@
     2.4  imports RealVector RComplete
     2.5  begin
     2.6  
     2.7 -subsection {* Filters *}
     2.8 +subsection {* Nets *}
     2.9 +
    2.10 +text {*
    2.11 +  A net is now defined as a filter base.
    2.12 +  The definition also allows non-proper filter bases.
    2.13 +*}
    2.14 +
    2.15 +typedef (open) 'a net =
    2.16 +  "{net :: 'a set set. (\<exists>A. A \<in> net)
    2.17 +    \<and> (\<forall>A\<in>net. \<forall>B\<in>net. \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B)}"
    2.18 +proof
    2.19 +  show "UNIV \<in> ?net" by auto
    2.20 +qed
    2.21  
    2.22 -typedef (open) 'a filter =
    2.23 -  "{f :: ('a \<Rightarrow> bool) \<Rightarrow> bool. f (\<lambda>x. True)
    2.24 -    \<and> (\<forall>P Q. (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> f P \<longrightarrow> f Q)
    2.25 -    \<and> (\<forall>P Q. f P \<longrightarrow> f Q \<longrightarrow> f (\<lambda>x. P x \<and> Q x))}"
    2.26 -proof
    2.27 -  show "(\<lambda>P. True) \<in> ?filter" by simp
    2.28 -qed
    2.29 +lemma Rep_net_nonempty: "\<exists>A. A \<in> Rep_net net"
    2.30 +using Rep_net [of net] by simp
    2.31 +
    2.32 +lemma Rep_net_directed:
    2.33 +  "A \<in> Rep_net net \<Longrightarrow> B \<in> Rep_net net \<Longrightarrow> \<exists>C\<in>Rep_net net. C \<subseteq> A \<and> C \<subseteq> B"
    2.34 +using Rep_net [of net] by simp
    2.35 +
    2.36 +lemma Abs_net_inverse':
    2.37 +  assumes "\<exists>A. A \<in> net"
    2.38 +  assumes "\<And>A B. A \<in> net \<Longrightarrow> B \<in> net \<Longrightarrow> \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B" 
    2.39 +  shows "Rep_net (Abs_net net) = net"
    2.40 +using assms by (simp add: Abs_net_inverse)
    2.41 +
    2.42 +lemma image_nonempty: "\<exists>x. x \<in> A \<Longrightarrow> \<exists>x. x \<in> f ` A"
    2.43 +by auto
    2.44 +
    2.45 +
    2.46 +subsection {* Eventually *}
    2.47  
    2.48  definition
    2.49 -  eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" where
    2.50 -  [code del]: "eventually P F \<longleftrightarrow> Rep_filter F P"
    2.51 +  eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
    2.52 +  [code del]: "eventually P net \<longleftrightarrow> (\<exists>A\<in>Rep_net net. \<forall>x\<in>A. P x)"
    2.53  
    2.54 -lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
    2.55 -unfolding eventually_def using Rep_filter [of F] by blast
    2.56 +lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
    2.57 +unfolding eventually_def using Rep_net_nonempty [of net] by fast
    2.58  
    2.59  lemma eventually_mono:
    2.60 -  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
    2.61 -unfolding eventually_def using Rep_filter [of F] by blast
    2.62 +  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
    2.63 +unfolding eventually_def by blast
    2.64  
    2.65  lemma eventually_conj:
    2.66 -  "\<lbrakk>eventually (\<lambda>x. P x) F; eventually (\<lambda>x. Q x) F\<rbrakk>
    2.67 -    \<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) F"
    2.68 -unfolding eventually_def using Rep_filter [of F] by blast
    2.69 +  assumes P: "eventually (\<lambda>x. P x) net"
    2.70 +  assumes Q: "eventually (\<lambda>x. Q x) net"
    2.71 +  shows "eventually (\<lambda>x. P x \<and> Q x) net"
    2.72 +proof -
    2.73 +  obtain A where A: "A \<in> Rep_net net" "\<forall>x\<in>A. P x"
    2.74 +    using P unfolding eventually_def by fast
    2.75 +  obtain B where B: "B \<in> Rep_net net" "\<forall>x\<in>B. Q x"
    2.76 +    using Q unfolding eventually_def by fast
    2.77 +  obtain C where C: "C \<in> Rep_net net" "C \<subseteq> A" "C \<subseteq> B"
    2.78 +    using Rep_net_directed [OF A(1) B(1)] by fast
    2.79 +  then have "\<forall>x\<in>C. P x \<and> Q x" "C \<in> Rep_net net"
    2.80 +    using A(2) B(2) by auto
    2.81 +  then show ?thesis unfolding eventually_def ..
    2.82 +qed
    2.83  
    2.84  lemma eventually_mp:
    2.85 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    2.86 -  assumes "eventually (\<lambda>x. P x) F"
    2.87 -  shows "eventually (\<lambda>x. Q x) F"
    2.88 +  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
    2.89 +  assumes "eventually (\<lambda>x. P x) net"
    2.90 +  shows "eventually (\<lambda>x. Q x) net"
    2.91  proof (rule eventually_mono)
    2.92    show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
    2.93 -  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
    2.94 +  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) net"
    2.95      using assms by (rule eventually_conj)
    2.96  qed
    2.97  
    2.98  lemma eventually_rev_mp:
    2.99 -  assumes "eventually (\<lambda>x. P x) F"
   2.100 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   2.101 -  shows "eventually (\<lambda>x. Q x) F"
   2.102 +  assumes "eventually (\<lambda>x. P x) net"
   2.103 +  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
   2.104 +  shows "eventually (\<lambda>x. Q x) net"
   2.105  using assms(2) assms(1) by (rule eventually_mp)
   2.106  
   2.107  lemma eventually_conj_iff:
   2.108    "eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net"
   2.109  by (auto intro: eventually_conj elim: eventually_rev_mp)
   2.110  
   2.111 -lemma eventually_Abs_filter:
   2.112 -  assumes "f (\<lambda>x. True)"
   2.113 -  assumes "\<And>P Q. (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> f P \<Longrightarrow> f Q"
   2.114 -  assumes "\<And>P Q. f P \<Longrightarrow> f Q \<Longrightarrow> f (\<lambda>x. P x \<and> Q x)"
   2.115 -  shows "eventually P (Abs_filter f) \<longleftrightarrow> f P"
   2.116 -unfolding eventually_def using assms
   2.117 -by (subst Abs_filter_inverse, auto)
   2.118 -
   2.119 -lemma filter_ext:
   2.120 -  "(\<And>P. eventually P F \<longleftrightarrow> eventually P F') \<Longrightarrow> F = F'"
   2.121 -unfolding eventually_def
   2.122 -by (simp add: Rep_filter_inject [THEN iffD1] ext)
   2.123 -
   2.124  lemma eventually_elim1:
   2.125 -  assumes "eventually (\<lambda>i. P i) F"
   2.126 +  assumes "eventually (\<lambda>i. P i) net"
   2.127    assumes "\<And>i. P i \<Longrightarrow> Q i"
   2.128 -  shows "eventually (\<lambda>i. Q i) F"
   2.129 +  shows "eventually (\<lambda>i. Q i) net"
   2.130  using assms by (auto elim!: eventually_rev_mp)
   2.131  
   2.132  lemma eventually_elim2:
   2.133 -  assumes "eventually (\<lambda>i. P i) F"
   2.134 -  assumes "eventually (\<lambda>i. Q i) F"
   2.135 +  assumes "eventually (\<lambda>i. P i) net"
   2.136 +  assumes "eventually (\<lambda>i. Q i) net"
   2.137    assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
   2.138 -  shows "eventually (\<lambda>i. R i) F"
   2.139 +  shows "eventually (\<lambda>i. R i) net"
   2.140  using assms by (auto elim!: eventually_rev_mp)
   2.141  
   2.142  
   2.143 +subsection {* Standard Nets *}
   2.144 +
   2.145 +definition
   2.146 +  sequentially :: "nat net" where
   2.147 +  [code del]: "sequentially = Abs_net (range (\<lambda>n. {n..}))"
   2.148 +
   2.149 +definition
   2.150 +  at :: "'a::metric_space \<Rightarrow> 'a net" where
   2.151 +  [code del]: "at a = Abs_net ((\<lambda>r. {x. x \<noteq> a \<and> dist x a < r}) ` {r. 0 < r})"
   2.152 +
   2.153 +definition
   2.154 +  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
   2.155 +  [code del]: "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)"
   2.156 +
   2.157 +lemma Rep_net_sequentially:
   2.158 +  "Rep_net sequentially = range (\<lambda>n. {n..})"
   2.159 +unfolding sequentially_def
   2.160 +apply (rule Abs_net_inverse')
   2.161 +apply (rule image_nonempty, simp)
   2.162 +apply (clarsimp, rename_tac m n)
   2.163 +apply (rule_tac x="max m n" in exI, auto)
   2.164 +done
   2.165 +
   2.166 +lemma Rep_net_at:
   2.167 +  "Rep_net (at a) = ((\<lambda>r. {x. x \<noteq> a \<and> dist x a < r}) ` {r. 0 < r})"
   2.168 +unfolding at_def
   2.169 +apply (rule Abs_net_inverse')
   2.170 +apply (rule image_nonempty, rule_tac x=1 in exI, simp)
   2.171 +apply (clarsimp, rename_tac r s)
   2.172 +apply (rule_tac x="min r s" in exI, auto)
   2.173 +done
   2.174 +
   2.175 +lemma Rep_net_within:
   2.176 +  "Rep_net (net within S) = (\<lambda>A. A \<inter> S) ` Rep_net net"
   2.177 +unfolding within_def
   2.178 +apply (rule Abs_net_inverse')
   2.179 +apply (rule image_nonempty, rule Rep_net_nonempty)
   2.180 +apply (clarsimp, rename_tac A B)
   2.181 +apply (drule (1) Rep_net_directed)
   2.182 +apply (clarify, rule_tac x=C in bexI, auto)
   2.183 +done
   2.184 +
   2.185 +lemma eventually_sequentially:
   2.186 +  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   2.187 +unfolding eventually_def Rep_net_sequentially by auto
   2.188 +
   2.189 +lemma eventually_at:
   2.190 +  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
   2.191 +unfolding eventually_def Rep_net_at by auto
   2.192 +
   2.193 +lemma eventually_within:
   2.194 +  "eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
   2.195 +unfolding eventually_def Rep_net_within by auto
   2.196 +
   2.197 +
   2.198  subsection {* Boundedness *}
   2.199  
   2.200  definition
   2.201 -  Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
   2.202 -  [code del]: "Bfun S F = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) F)"
   2.203 +  Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
   2.204 +  [code del]: "Bfun S net = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) net)"
   2.205  
   2.206 -lemma BfunI: assumes K: "eventually (\<lambda>i. norm (X i) \<le> K) F" shows "Bfun X F"
   2.207 +lemma BfunI: assumes K: "eventually (\<lambda>i. norm (X i) \<le> K) net" shows "Bfun X net"
   2.208  unfolding Bfun_def
   2.209  proof (intro exI conjI allI)
   2.210    show "0 < max K 1" by simp
   2.211  next
   2.212 -  show "eventually (\<lambda>i. norm (X i) \<le> max K 1) F"
   2.213 +  show "eventually (\<lambda>i. norm (X i) \<le> max K 1) net"
   2.214      using K by (rule eventually_elim1, simp)
   2.215  qed
   2.216  
   2.217  lemma BfunE:
   2.218 -  assumes "Bfun S F"
   2.219 -  obtains B where "0 < B" and "eventually (\<lambda>i. norm (S i) \<le> B) F"
   2.220 +  assumes "Bfun S net"
   2.221 +  obtains B where "0 < B" and "eventually (\<lambda>i. norm (S i) \<le> B) net"
   2.222  using assms unfolding Bfun_def by fast
   2.223  
   2.224  
   2.225  subsection {* Convergence to Zero *}
   2.226  
   2.227  definition
   2.228 -  Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
   2.229 -  [code del]: "Zfun S F = (\<forall>r>0. eventually (\<lambda>i. norm (S i) < r) F)"
   2.230 +  Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
   2.231 +  [code del]: "Zfun S net = (\<forall>r>0. eventually (\<lambda>i. norm (S i) < r) net)"
   2.232  
   2.233  lemma ZfunI:
   2.234 -  "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F) \<Longrightarrow> Zfun S F"
   2.235 +  "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) net) \<Longrightarrow> Zfun S net"
   2.236  unfolding Zfun_def by simp
   2.237  
   2.238  lemma ZfunD:
   2.239 -  "\<lbrakk>Zfun S F; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F"
   2.240 +  "\<lbrakk>Zfun S net; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) net"
   2.241  unfolding Zfun_def by simp
   2.242  
   2.243  lemma Zfun_ssubst:
   2.244 -  "eventually (\<lambda>i. X i = Y i) F \<Longrightarrow> Zfun Y F \<Longrightarrow> Zfun X F"
   2.245 +  "eventually (\<lambda>i. X i = Y i) net \<Longrightarrow> Zfun Y net \<Longrightarrow> Zfun X net"
   2.246  unfolding Zfun_def by (auto elim!: eventually_rev_mp)
   2.247  
   2.248 -lemma Zfun_zero: "Zfun (\<lambda>i. 0) F"
   2.249 +lemma Zfun_zero: "Zfun (\<lambda>i. 0) net"
   2.250  unfolding Zfun_def by simp
   2.251  
   2.252 -lemma Zfun_norm_iff: "Zfun (\<lambda>i. norm (S i)) F = Zfun (\<lambda>i. S i) F"
   2.253 +lemma Zfun_norm_iff: "Zfun (\<lambda>i. norm (S i)) net = Zfun (\<lambda>i. S i) net"
   2.254  unfolding Zfun_def by simp
   2.255  
   2.256  lemma Zfun_imp_Zfun:
   2.257 -  assumes X: "Zfun X F"
   2.258 -  assumes Y: "eventually (\<lambda>i. norm (Y i) \<le> norm (X i) * K) F"
   2.259 -  shows "Zfun (\<lambda>n. Y n) F"
   2.260 +  assumes X: "Zfun X net"
   2.261 +  assumes Y: "eventually (\<lambda>i. norm (Y i) \<le> norm (X i) * K) net"
   2.262 +  shows "Zfun (\<lambda>n. Y n) net"
   2.263  proof (cases)
   2.264    assume K: "0 < K"
   2.265    show ?thesis
   2.266 @@ -137,9 +213,9 @@
   2.267      fix r::real assume "0 < r"
   2.268      hence "0 < r / K"
   2.269        using K by (rule divide_pos_pos)
   2.270 -    then have "eventually (\<lambda>i. norm (X i) < r / K) F"
   2.271 +    then have "eventually (\<lambda>i. norm (X i) < r / K) net"
   2.272        using ZfunD [OF X] by fast
   2.273 -    with Y show "eventually (\<lambda>i. norm (Y i) < r) F"
   2.274 +    with Y show "eventually (\<lambda>i. norm (Y i) < r) net"
   2.275      proof (rule eventually_elim2)
   2.276        fix i
   2.277        assume *: "norm (Y i) \<le> norm (X i) * K"
   2.278 @@ -157,7 +233,7 @@
   2.279    proof (rule ZfunI)
   2.280      fix r :: real
   2.281      assume "0 < r"
   2.282 -    from Y show "eventually (\<lambda>i. norm (Y i) < r) F"
   2.283 +    from Y show "eventually (\<lambda>i. norm (Y i) < r) net"
   2.284      proof (rule eventually_elim1)
   2.285        fix i
   2.286        assume "norm (Y i) \<le> norm (X i) * K"
   2.287 @@ -169,22 +245,22 @@
   2.288    qed
   2.289  qed
   2.290  
   2.291 -lemma Zfun_le: "\<lbrakk>Zfun Y F; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zfun X F"
   2.292 +lemma Zfun_le: "\<lbrakk>Zfun Y net; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zfun X net"
   2.293  by (erule_tac K="1" in Zfun_imp_Zfun, simp)
   2.294  
   2.295  lemma Zfun_add:
   2.296 -  assumes X: "Zfun X F" and Y: "Zfun Y F"
   2.297 -  shows "Zfun (\<lambda>n. X n + Y n) F"
   2.298 +  assumes X: "Zfun X net" and Y: "Zfun Y net"
   2.299 +  shows "Zfun (\<lambda>n. X n + Y n) net"
   2.300  proof (rule ZfunI)
   2.301    fix r::real assume "0 < r"
   2.302    hence r: "0 < r / 2" by simp
   2.303 -  have "eventually (\<lambda>i. norm (X i) < r/2) F"
   2.304 +  have "eventually (\<lambda>i. norm (X i) < r/2) net"
   2.305      using X r by (rule ZfunD)
   2.306    moreover
   2.307 -  have "eventually (\<lambda>i. norm (Y i) < r/2) F"
   2.308 +  have "eventually (\<lambda>i. norm (Y i) < r/2) net"
   2.309      using Y r by (rule ZfunD)
   2.310    ultimately
   2.311 -  show "eventually (\<lambda>i. norm (X i + Y i) < r) F"
   2.312 +  show "eventually (\<lambda>i. norm (X i + Y i) < r) net"
   2.313    proof (rule eventually_elim2)
   2.314      fix i
   2.315      assume *: "norm (X i) < r/2" "norm (Y i) < r/2"
   2.316 @@ -197,28 +273,28 @@
   2.317    qed
   2.318  qed
   2.319  
   2.320 -lemma Zfun_minus: "Zfun X F \<Longrightarrow> Zfun (\<lambda>i. - X i) F"
   2.321 +lemma Zfun_minus: "Zfun X net \<Longrightarrow> Zfun (\<lambda>i. - X i) net"
   2.322  unfolding Zfun_def by simp
   2.323  
   2.324 -lemma Zfun_diff: "\<lbrakk>Zfun X F; Zfun Y F\<rbrakk> \<Longrightarrow> Zfun (\<lambda>i. X i - Y i) F"
   2.325 +lemma Zfun_diff: "\<lbrakk>Zfun X net; Zfun Y net\<rbrakk> \<Longrightarrow> Zfun (\<lambda>i. X i - Y i) net"
   2.326  by (simp only: diff_minus Zfun_add Zfun_minus)
   2.327  
   2.328  lemma (in bounded_linear) Zfun:
   2.329 -  assumes X: "Zfun X F"
   2.330 -  shows "Zfun (\<lambda>n. f (X n)) F"
   2.331 +  assumes X: "Zfun X net"
   2.332 +  shows "Zfun (\<lambda>n. f (X n)) net"
   2.333  proof -
   2.334    obtain K where "\<And>x. norm (f x) \<le> norm x * K"
   2.335      using bounded by fast
   2.336 -  then have "eventually (\<lambda>i. norm (f (X i)) \<le> norm (X i) * K) F"
   2.337 +  then have "eventually (\<lambda>i. norm (f (X i)) \<le> norm (X i) * K) net"
   2.338      by simp
   2.339    with X show ?thesis
   2.340      by (rule Zfun_imp_Zfun)
   2.341  qed
   2.342  
   2.343  lemma (in bounded_bilinear) Zfun:
   2.344 -  assumes X: "Zfun X F"
   2.345 -  assumes Y: "Zfun Y F"
   2.346 -  shows "Zfun (\<lambda>n. X n ** Y n) F"
   2.347 +  assumes X: "Zfun X net"
   2.348 +  assumes Y: "Zfun Y net"
   2.349 +  shows "Zfun (\<lambda>n. X n ** Y n) net"
   2.350  proof (rule ZfunI)
   2.351    fix r::real assume r: "0 < r"
   2.352    obtain K where K: "0 < K"
   2.353 @@ -226,13 +302,13 @@
   2.354      using pos_bounded by fast
   2.355    from K have K': "0 < inverse K"
   2.356      by (rule positive_imp_inverse_positive)
   2.357 -  have "eventually (\<lambda>i. norm (X i) < r) F"
   2.358 +  have "eventually (\<lambda>i. norm (X i) < r) net"
   2.359      using X r by (rule ZfunD)
   2.360    moreover
   2.361 -  have "eventually (\<lambda>i. norm (Y i) < inverse K) F"
   2.362 +  have "eventually (\<lambda>i. norm (Y i) < inverse K) net"
   2.363      using Y K' by (rule ZfunD)
   2.364    ultimately
   2.365 -  show "eventually (\<lambda>i. norm (X i ** Y i) < r) F"
   2.366 +  show "eventually (\<lambda>i. norm (X i ** Y i) < r) net"
   2.367    proof (rule eventually_elim2)
   2.368      fix i
   2.369      assume *: "norm (X i) < r" "norm (Y i) < inverse K"
   2.370 @@ -247,11 +323,11 @@
   2.371  qed
   2.372  
   2.373  lemma (in bounded_bilinear) Zfun_left:
   2.374 -  "Zfun X F \<Longrightarrow> Zfun (\<lambda>n. X n ** a) F"
   2.375 +  "Zfun X net \<Longrightarrow> Zfun (\<lambda>n. X n ** a) net"
   2.376  by (rule bounded_linear_left [THEN bounded_linear.Zfun])
   2.377  
   2.378  lemma (in bounded_bilinear) Zfun_right:
   2.379 -  "Zfun X F \<Longrightarrow> Zfun (\<lambda>n. a ** X n) F"
   2.380 +  "Zfun X net \<Longrightarrow> Zfun (\<lambda>n. a ** X n) net"
   2.381  by (rule bounded_linear_right [THEN bounded_linear.Zfun])
   2.382  
   2.383  lemmas Zfun_mult = mult.Zfun
   2.384 @@ -262,7 +338,7 @@
   2.385  subsection{* Limits *}
   2.386  
   2.387  definition
   2.388 -  tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool" where
   2.389 +  tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" where
   2.390    [code del]: "tendsto f l net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
   2.391  
   2.392  lemma tendstoI:
   2.393 @@ -274,15 +350,15 @@
   2.394    "tendsto f l net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
   2.395    unfolding tendsto_def by auto
   2.396  
   2.397 -lemma tendsto_Zfun_iff: "tendsto (\<lambda>n. X n) L F = Zfun (\<lambda>n. X n - L) F"
   2.398 +lemma tendsto_Zfun_iff: "tendsto (\<lambda>n. X n) L net = Zfun (\<lambda>n. X n - L) net"
   2.399  by (simp only: tendsto_def Zfun_def dist_norm)
   2.400  
   2.401 -lemma tendsto_const: "tendsto (\<lambda>n. k) k F"
   2.402 +lemma tendsto_const: "tendsto (\<lambda>n. k) k net"
   2.403  by (simp add: tendsto_def)
   2.404  
   2.405  lemma tendsto_norm:
   2.406    fixes a :: "'a::real_normed_vector"
   2.407 -  shows "tendsto X a F \<Longrightarrow> tendsto (\<lambda>n. norm (X n)) (norm a) F"
   2.408 +  shows "tendsto X a net \<Longrightarrow> tendsto (\<lambda>n. norm (X n)) (norm a) net"
   2.409  apply (simp add: tendsto_def dist_norm, safe)
   2.410  apply (drule_tac x="e" in spec, safe)
   2.411  apply (erule eventually_elim1)
   2.412 @@ -301,30 +377,30 @@
   2.413  
   2.414  lemma tendsto_add:
   2.415    fixes a b :: "'a::real_normed_vector"
   2.416 -  shows "\<lbrakk>tendsto X a F; tendsto Y b F\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n + Y n) (a + b) F"
   2.417 +  shows "\<lbrakk>tendsto X a net; tendsto Y b net\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n + Y n) (a + b) net"
   2.418  by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
   2.419  
   2.420  lemma tendsto_minus:
   2.421    fixes a :: "'a::real_normed_vector"
   2.422 -  shows "tendsto X a F \<Longrightarrow> tendsto (\<lambda>n. - X n) (- a) F"
   2.423 +  shows "tendsto X a net \<Longrightarrow> tendsto (\<lambda>n. - X n) (- a) net"
   2.424  by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
   2.425  
   2.426  lemma tendsto_minus_cancel:
   2.427    fixes a :: "'a::real_normed_vector"
   2.428 -  shows "tendsto (\<lambda>n. - X n) (- a) F \<Longrightarrow> tendsto X a F"
   2.429 +  shows "tendsto (\<lambda>n. - X n) (- a) net \<Longrightarrow> tendsto X a net"
   2.430  by (drule tendsto_minus, simp)
   2.431  
   2.432  lemma tendsto_diff:
   2.433    fixes a b :: "'a::real_normed_vector"
   2.434 -  shows "\<lbrakk>tendsto X a F; tendsto Y b F\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n - Y n) (a - b) F"
   2.435 +  shows "\<lbrakk>tendsto X a net; tendsto Y b net\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n - Y n) (a - b) net"
   2.436  by (simp add: diff_minus tendsto_add tendsto_minus)
   2.437  
   2.438  lemma (in bounded_linear) tendsto:
   2.439 -  "tendsto X a F \<Longrightarrow> tendsto (\<lambda>n. f (X n)) (f a) F"
   2.440 +  "tendsto X a net \<Longrightarrow> tendsto (\<lambda>n. f (X n)) (f a) net"
   2.441  by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
   2.442  
   2.443  lemma (in bounded_bilinear) tendsto:
   2.444 -  "\<lbrakk>tendsto X a F; tendsto Y b F\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n ** Y n) (a ** b) F"
   2.445 +  "\<lbrakk>tendsto X a net; tendsto Y b net\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n ** Y n) (a ** b) net"
   2.446  by (simp only: tendsto_Zfun_iff prod_diff_prod
   2.447                 Zfun_add Zfun Zfun_left Zfun_right)
   2.448  
   2.449 @@ -332,17 +408,17 @@
   2.450  subsection {* Continuity of Inverse *}
   2.451  
   2.452  lemma (in bounded_bilinear) Zfun_prod_Bfun:
   2.453 -  assumes X: "Zfun X F"
   2.454 -  assumes Y: "Bfun Y F"
   2.455 -  shows "Zfun (\<lambda>n. X n ** Y n) F"
   2.456 +  assumes X: "Zfun X net"
   2.457 +  assumes Y: "Bfun Y net"
   2.458 +  shows "Zfun (\<lambda>n. X n ** Y n) net"
   2.459  proof -
   2.460    obtain K where K: "0 \<le> K"
   2.461      and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
   2.462      using nonneg_bounded by fast
   2.463    obtain B where B: "0 < B"
   2.464 -    and norm_Y: "eventually (\<lambda>i. norm (Y i) \<le> B) F"
   2.465 +    and norm_Y: "eventually (\<lambda>i. norm (Y i) \<le> B) net"
   2.466      using Y by (rule BfunE)
   2.467 -  have "eventually (\<lambda>i. norm (X i ** Y i) \<le> norm (X i) * (B * K)) F"
   2.468 +  have "eventually (\<lambda>i. norm (X i ** Y i) \<le> norm (X i) * (B * K)) net"
   2.469    using norm_Y proof (rule eventually_elim1)
   2.470      fix i
   2.471      assume *: "norm (Y i) \<le> B"
   2.472 @@ -370,9 +446,9 @@
   2.473  using bounded by fast
   2.474  
   2.475  lemma (in bounded_bilinear) Bfun_prod_Zfun:
   2.476 -  assumes X: "Bfun X F"
   2.477 -  assumes Y: "Zfun Y F"
   2.478 -  shows "Zfun (\<lambda>n. X n ** Y n) F"
   2.479 +  assumes X: "Bfun X net"
   2.480 +  assumes Y: "Zfun Y net"
   2.481 +  shows "Zfun (\<lambda>n. X n ** Y n) net"
   2.482  using flip Y X by (rule bounded_bilinear.Zfun_prod_Bfun)
   2.483  
   2.484  lemma inverse_diff_inverse:
   2.485 @@ -389,16 +465,16 @@
   2.486  
   2.487  lemma Bfun_inverse:
   2.488    fixes a :: "'a::real_normed_div_algebra"
   2.489 -  assumes X: "tendsto X a F"
   2.490 +  assumes X: "tendsto X a net"
   2.491    assumes a: "a \<noteq> 0"
   2.492 -  shows "Bfun (\<lambda>n. inverse (X n)) F"
   2.493 +  shows "Bfun (\<lambda>n. inverse (X n)) net"
   2.494  proof -
   2.495    from a have "0 < norm a" by simp
   2.496    hence "\<exists>r>0. r < norm a" by (rule dense)
   2.497    then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
   2.498 -  have "eventually (\<lambda>i. dist (X i) a < r) F"
   2.499 +  have "eventually (\<lambda>i. dist (X i) a < r) net"
   2.500      using tendstoD [OF X r1] by fast
   2.501 -  hence "eventually (\<lambda>i. norm (inverse (X i)) \<le> inverse (norm a - r)) F"
   2.502 +  hence "eventually (\<lambda>i. norm (inverse (X i)) \<le> inverse (norm a - r)) net"
   2.503    proof (rule eventually_elim1)
   2.504      fix i
   2.505      assume "dist (X i) a < r"
   2.506 @@ -425,8 +501,8 @@
   2.507  
   2.508  lemma tendsto_inverse_lemma:
   2.509    fixes a :: "'a::real_normed_div_algebra"
   2.510 -  shows "\<lbrakk>tendsto X a F; a \<noteq> 0; eventually (\<lambda>i. X i \<noteq> 0) F\<rbrakk>
   2.511 -         \<Longrightarrow> tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
   2.512 +  shows "\<lbrakk>tendsto X a net; a \<noteq> 0; eventually (\<lambda>i. X i \<noteq> 0) net\<rbrakk>
   2.513 +         \<Longrightarrow> tendsto (\<lambda>i. inverse (X i)) (inverse a) net"
   2.514  apply (subst tendsto_Zfun_iff)
   2.515  apply (rule Zfun_ssubst)
   2.516  apply (erule eventually_elim1)
   2.517 @@ -440,14 +516,14 @@
   2.518  
   2.519  lemma tendsto_inverse:
   2.520    fixes a :: "'a::real_normed_div_algebra"
   2.521 -  assumes X: "tendsto X a F"
   2.522 +  assumes X: "tendsto X a net"
   2.523    assumes a: "a \<noteq> 0"
   2.524 -  shows "tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
   2.525 +  shows "tendsto (\<lambda>i. inverse (X i)) (inverse a) net"
   2.526  proof -
   2.527    from a have "0 < norm a" by simp
   2.528 -  with X have "eventually (\<lambda>i. dist (X i) a < norm a) F"
   2.529 +  with X have "eventually (\<lambda>i. dist (X i) a < norm a) net"
   2.530      by (rule tendstoD)
   2.531 -  then have "eventually (\<lambda>i. X i \<noteq> 0) F"
   2.532 +  then have "eventually (\<lambda>i. X i \<noteq> 0) net"
   2.533      unfolding dist_norm by (auto elim!: eventually_elim1)
   2.534    with X a show ?thesis
   2.535      by (rule tendsto_inverse_lemma)
   2.536 @@ -455,8 +531,8 @@
   2.537  
   2.538  lemma tendsto_divide:
   2.539    fixes a b :: "'a::real_normed_field"
   2.540 -  shows "\<lbrakk>tendsto X a F; tendsto Y b F; b \<noteq> 0\<rbrakk>
   2.541 -    \<Longrightarrow> tendsto (\<lambda>n. X n / Y n) (a / b) F"
   2.542 +  shows "\<lbrakk>tendsto X a net; tendsto Y b net; b \<noteq> 0\<rbrakk>
   2.543 +    \<Longrightarrow> tendsto (\<lambda>n. X n / Y n) (a / b) net"
   2.544  by (simp add: mult.tendsto tendsto_inverse divide_inverse)
   2.545  
   2.546  end
     3.1 --- a/src/HOL/SEQ.thy	Tue Jun 02 15:37:59 2009 -0700
     3.2 +++ b/src/HOL/SEQ.thy	Tue Jun 02 17:03:22 2009 -0700
     3.3 @@ -13,10 +13,6 @@
     3.4  begin
     3.5  
     3.6  definition
     3.7 -  sequentially :: "nat filter" where
     3.8 -  [code del]: "sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)"
     3.9 -
    3.10 -definition
    3.11    Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
    3.12      --{*Standard definition of sequence converging to zero*}
    3.13    [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
    3.14 @@ -71,24 +67,6 @@
    3.15    [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
    3.16  
    3.17  
    3.18 -subsection {* Sequentially *}
    3.19 -
    3.20 -lemma eventually_sequentially:
    3.21 -  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
    3.22 -unfolding sequentially_def
    3.23 -apply (rule eventually_Abs_filter)
    3.24 -apply simp
    3.25 -apply (clarify, rule_tac x=N in exI, simp)
    3.26 -apply (clarify, rename_tac M N)
    3.27 -apply (rule_tac x="max M N" in exI, simp)
    3.28 -done
    3.29 -
    3.30 -lemma Zseq_conv_Zfun: "Zseq X \<longleftrightarrow> Zfun X sequentially"
    3.31 -unfolding Zseq_def Zfun_def eventually_sequentially ..
    3.32 -
    3.33 -lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> tendsto X L sequentially"
    3.34 -unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
    3.35 -
    3.36  subsection {* Bounded Sequences *}
    3.37  
    3.38  lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
    3.39 @@ -150,6 +128,9 @@
    3.40    "\<lbrakk>Zseq X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r"
    3.41  unfolding Zseq_def by simp
    3.42  
    3.43 +lemma Zseq_conv_Zfun: "Zseq X \<longleftrightarrow> Zfun X sequentially"
    3.44 +unfolding Zseq_def Zfun_def eventually_sequentially ..
    3.45 +
    3.46  lemma Zseq_zero: "Zseq (\<lambda>n. 0)"
    3.47  unfolding Zseq_def by simp
    3.48  
    3.49 @@ -212,6 +193,9 @@
    3.50  
    3.51  subsection {* Limits of Sequences *}
    3.52  
    3.53 +lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> tendsto X L sequentially"
    3.54 +unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
    3.55 +
    3.56  lemma LIMSEQ_iff:
    3.57    fixes L :: "'a::real_normed_vector"
    3.58    shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"