define nets directly as filters, instead of as filter bases
authorhuffman
Sun Apr 25 11:58:39 2010 -0700 (2010-04-25)
changeset 36358246493d61204
parent 36341 2623a1987e1d
child 36359 e5c785c166b2
define nets directly as filters, instead of as filter bases
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Limits.thy	Sun Apr 25 10:23:03 2010 -0700
     1.2 +++ b/src/HOL/Limits.thy	Sun Apr 25 11:58:39 2010 -0700
     1.3 @@ -11,62 +11,55 @@
     1.4  subsection {* Nets *}
     1.5  
     1.6  text {*
     1.7 -  A net is now defined as a filter base.
     1.8 -  The definition also allows non-proper filter bases.
     1.9 +  A net is now defined simply as a filter.
    1.10 +  The definition also allows non-proper filters.
    1.11  *}
    1.12  
    1.13 +locale is_filter =
    1.14 +  fixes net :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.15 +  assumes True: "net (\<lambda>x. True)"
    1.16 +  assumes conj: "net (\<lambda>x. P x) \<Longrightarrow> net (\<lambda>x. Q x) \<Longrightarrow> net (\<lambda>x. P x \<and> Q x)"
    1.17 +  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> net (\<lambda>x. P x) \<Longrightarrow> net (\<lambda>x. Q x)"
    1.18 +
    1.19  typedef (open) 'a net =
    1.20 -  "{net :: 'a set set. (\<exists>A. A \<in> net)
    1.21 -    \<and> (\<forall>A\<in>net. \<forall>B\<in>net. \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B)}"
    1.22 +  "{net :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter net}"
    1.23  proof
    1.24 -  show "UNIV \<in> ?net" by auto
    1.25 +  show "(\<lambda>x. True) \<in> ?net" by (auto intro: is_filter.intro)
    1.26  qed
    1.27  
    1.28 -lemma Rep_net_nonempty: "\<exists>A. A \<in> Rep_net net"
    1.29 -using Rep_net [of net] by simp
    1.30 -
    1.31 -lemma Rep_net_directed:
    1.32 -  "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"
    1.33 +lemma is_filter_Rep_net: "is_filter (Rep_net net)"
    1.34  using Rep_net [of net] by simp
    1.35  
    1.36  lemma Abs_net_inverse':
    1.37 -  assumes "\<exists>A. A \<in> net"
    1.38 -  assumes "\<And>A B. A \<in> net \<Longrightarrow> B \<in> net \<Longrightarrow> \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B" 
    1.39 -  shows "Rep_net (Abs_net net) = net"
    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  
    1.43 -lemma image_nonempty: "\<exists>x. x \<in> A \<Longrightarrow> \<exists>x. x \<in> f ` A"
    1.44 -by auto
    1.45 -
    1.46  
    1.47  subsection {* Eventually *}
    1.48  
    1.49  definition
    1.50    eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
    1.51 -  [code del]: "eventually P net \<longleftrightarrow> (\<exists>A\<in>Rep_net net. \<forall>x\<in>A. P x)"
    1.52 +  [code del]: "eventually P net \<longleftrightarrow> Rep_net net 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  
    1.58  lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
    1.59 -unfolding eventually_def using Rep_net_nonempty [of net] by fast
    1.60 +unfolding eventually_def
    1.61 +by (rule is_filter.True [OF is_filter_Rep_net])
    1.62  
    1.63  lemma eventually_mono:
    1.64    "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
    1.65 -unfolding eventually_def by blast
    1.66 +unfolding eventually_def
    1.67 +by (rule is_filter.mono [OF is_filter_Rep_net])
    1.68  
    1.69  lemma eventually_conj:
    1.70    assumes P: "eventually (\<lambda>x. P x) net"
    1.71    assumes Q: "eventually (\<lambda>x. Q x) net"
    1.72    shows "eventually (\<lambda>x. P x \<and> Q x) net"
    1.73 -proof -
    1.74 -  obtain A where A: "A \<in> Rep_net net" "\<forall>x\<in>A. P x"
    1.75 -    using P unfolding eventually_def by fast
    1.76 -  obtain B where B: "B \<in> Rep_net net" "\<forall>x\<in>B. Q x"
    1.77 -    using Q unfolding eventually_def by fast
    1.78 -  obtain C where C: "C \<in> Rep_net net" "C \<subseteq> A" "C \<subseteq> B"
    1.79 -    using Rep_net_directed [OF A(1) B(1)] by fast
    1.80 -  then have "\<forall>x\<in>C. P x \<and> Q x" "C \<in> Rep_net net"
    1.81 -    using A(2) B(2) by auto
    1.82 -  then show ?thesis unfolding eventually_def ..
    1.83 -qed
    1.84 +using assms unfolding eventually_def
    1.85 +by (rule is_filter.conj [OF is_filter_Rep_net])
    1.86  
    1.87  lemma eventually_mp:
    1.88    assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
    1.89 @@ -105,57 +98,54 @@
    1.90  subsection {* Standard Nets *}
    1.91  
    1.92  definition
    1.93 -  sequentially :: "nat net" where
    1.94 -  [code del]: "sequentially = Abs_net (range (\<lambda>n. {n..}))"
    1.95 -
    1.96 -definition
    1.97 -  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
    1.98 -  [code del]: "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)"
    1.99 +  sequentially :: "nat net"
   1.100 +where [code del]:
   1.101 +  "sequentially = Abs_net (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
   1.102  
   1.103  definition
   1.104 -  at :: "'a::topological_space \<Rightarrow> 'a net" where
   1.105 -  [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
   1.106 -
   1.107 -lemma Rep_net_sequentially:
   1.108 -  "Rep_net sequentially = range (\<lambda>n. {n..})"
   1.109 -unfolding sequentially_def
   1.110 -apply (rule Abs_net_inverse')
   1.111 -apply (rule image_nonempty, simp)
   1.112 -apply (clarsimp, rename_tac m n)
   1.113 -apply (rule_tac x="max m n" in exI, auto)
   1.114 -done
   1.115 +  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70)
   1.116 +where [code del]:
   1.117 +  "net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
   1.118  
   1.119 -lemma Rep_net_within:
   1.120 -  "Rep_net (net within S) = (\<lambda>A. A \<inter> S) ` Rep_net net"
   1.121 -unfolding within_def
   1.122 -apply (rule Abs_net_inverse')
   1.123 -apply (rule image_nonempty, rule Rep_net_nonempty)
   1.124 -apply (clarsimp, rename_tac A B)
   1.125 -apply (drule (1) Rep_net_directed)
   1.126 -apply (clarify, rule_tac x=C in bexI, auto)
   1.127 -done
   1.128 -
   1.129 -lemma Rep_net_at:
   1.130 -  "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
   1.131 -unfolding at_def
   1.132 -apply (rule Abs_net_inverse')
   1.133 -apply (rule image_nonempty)
   1.134 -apply (rule_tac x="UNIV" in exI, simp)
   1.135 -apply (clarsimp, rename_tac S T)
   1.136 -apply (rule_tac x="S \<inter> T" in exI, auto simp add: open_Int)
   1.137 -done
   1.138 +definition
   1.139 +  at :: "'a::topological_space \<Rightarrow> 'a net"
   1.140 +where [code del]:
   1.141 +  "at a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
   1.142  
   1.143  lemma eventually_sequentially:
   1.144    "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   1.145 -unfolding eventually_def Rep_net_sequentially by auto
   1.146 +unfolding sequentially_def
   1.147 +proof (rule eventually_Abs_net, rule is_filter.intro)
   1.148 +  fix P Q :: "nat \<Rightarrow> bool"
   1.149 +  assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
   1.150 +  then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
   1.151 +  then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
   1.152 +  then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
   1.153 +qed auto
   1.154  
   1.155  lemma eventually_within:
   1.156    "eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
   1.157 -unfolding eventually_def Rep_net_within by auto
   1.158 +unfolding within_def
   1.159 +by (rule eventually_Abs_net, rule is_filter.intro)
   1.160 +   (auto elim!: eventually_rev_mp)
   1.161  
   1.162  lemma eventually_at_topological:
   1.163    "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
   1.164 -unfolding eventually_def Rep_net_at by auto
   1.165 +unfolding at_def
   1.166 +proof (rule eventually_Abs_net, rule is_filter.intro)
   1.167 +  have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. x \<noteq> a \<longrightarrow> True)" by simp
   1.168 +  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> True)" by - rule
   1.169 +next
   1.170 +  fix P Q
   1.171 +  assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x)"
   1.172 +     and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> Q x)"
   1.173 +  then obtain S T where
   1.174 +    "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x)"
   1.175 +    "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> Q x)" by auto
   1.176 +  hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). x \<noteq> a \<longrightarrow> P x \<and> Q x)"
   1.177 +    by (simp add: open_Int)
   1.178 +  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x \<and> Q x)" by - rule
   1.179 +qed auto
   1.180  
   1.181  lemma eventually_at:
   1.182    fixes a :: "'a::metric_space"
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 25 10:23:03 2010 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 25 11:58:39 2010 -0700
     2.3 @@ -968,7 +968,7 @@
     2.4  
     2.5  definition
     2.6    at_infinity :: "'a::real_normed_vector net" where
     2.7 -  "at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))"
     2.8 +  "at_infinity = Abs_net (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
     2.9  
    2.10  definition
    2.11    indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a net" (infixr "indirection" 70) where
    2.12 @@ -976,23 +976,32 @@
    2.13  
    2.14  text{* Prove That They are all nets. *}
    2.15  
    2.16 -lemma Rep_net_at_infinity:
    2.17 -  "Rep_net at_infinity = range (\<lambda>r. {x. r \<le> norm x})"
    2.18 +(* TODO: move to HOL/Limits.thy *)
    2.19 +lemma expand_net_eq:
    2.20 +  "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
    2.21 +  unfolding Rep_net_inject [symmetric] expand_fun_eq eventually_def ..
    2.22 +
    2.23 +(* TODO: move to HOL/Limits.thy *)
    2.24 +lemma within_UNIV: "net within UNIV = net"
    2.25 +  unfolding expand_net_eq eventually_within by simp
    2.26 +
    2.27 +lemma eventually_at_infinity:
    2.28 +  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
    2.29  unfolding at_infinity_def
    2.30 -apply (rule Abs_net_inverse')
    2.31 -apply (rule image_nonempty, simp)
    2.32 -apply (clarsimp, rename_tac r s)
    2.33 -apply (rule_tac x="max r s" in exI, auto)
    2.34 -done
    2.35 -
    2.36 -lemma within_UNIV: "net within UNIV = net"
    2.37 -  by (simp add: Rep_net_inject [symmetric] Rep_net_within)
    2.38 +proof (rule eventually_Abs_net, rule is_filter.intro)
    2.39 +  fix P Q :: "'a \<Rightarrow> bool"
    2.40 +  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
    2.41 +  then obtain r s where
    2.42 +    "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
    2.43 +  then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
    2.44 +  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
    2.45 +qed auto
    2.46  
    2.47  subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *}
    2.48  
    2.49  definition
    2.50    trivial_limit :: "'a net \<Rightarrow> bool" where
    2.51 -  "trivial_limit net \<longleftrightarrow> {} \<in> Rep_net net"
    2.52 +  "trivial_limit net \<longleftrightarrow> eventually (\<lambda>x. False) net"
    2.53  
    2.54  lemma trivial_limit_within:
    2.55    shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
    2.56 @@ -1000,21 +1009,21 @@
    2.57    assume "trivial_limit (at a within S)"
    2.58    thus "\<not> a islimpt S"
    2.59      unfolding trivial_limit_def
    2.60 -    unfolding Rep_net_within Rep_net_at
    2.61 +    unfolding eventually_within eventually_at_topological
    2.62      unfolding islimpt_def
    2.63      apply (clarsimp simp add: expand_set_eq)
    2.64      apply (rename_tac T, rule_tac x=T in exI)
    2.65 -    apply (clarsimp, drule_tac x=y in spec, simp)
    2.66 +    apply (clarsimp, drule_tac x=y in bspec, simp_all)
    2.67      done
    2.68  next
    2.69    assume "\<not> a islimpt S"
    2.70    thus "trivial_limit (at a within S)"
    2.71      unfolding trivial_limit_def
    2.72 -    unfolding Rep_net_within Rep_net_at
    2.73 +    unfolding eventually_within eventually_at_topological
    2.74      unfolding islimpt_def
    2.75 -    apply (clarsimp simp add: image_image)
    2.76 -    apply (rule_tac x=T in image_eqI)
    2.77 -    apply (auto simp add: expand_set_eq)
    2.78 +    apply clarsimp
    2.79 +    apply (rule_tac x=T in exI)
    2.80 +    apply auto
    2.81      done
    2.82  qed
    2.83  
    2.84 @@ -1030,14 +1039,14 @@
    2.85  lemma trivial_limit_at_infinity:
    2.86    "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)"
    2.87    (* FIXME: find a more appropriate type class *)
    2.88 -  unfolding trivial_limit_def Rep_net_at_infinity
    2.89 -  apply (clarsimp simp add: expand_set_eq)
    2.90 -  apply (drule_tac x="scaleR r (sgn 1)" in spec)
    2.91 +  unfolding trivial_limit_def eventually_at_infinity
    2.92 +  apply clarsimp
    2.93 +  apply (rule_tac x="scaleR b (sgn 1)" in exI)
    2.94    apply (simp add: norm_sgn)
    2.95    done
    2.96  
    2.97  lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
    2.98 -  by (auto simp add: trivial_limit_def Rep_net_sequentially)
    2.99 +  by (auto simp add: trivial_limit_def eventually_sequentially)
   2.100  
   2.101  subsection{* Some property holds "sufficiently close" to the limit point. *}
   2.102  
   2.103 @@ -1045,10 +1054,6 @@
   2.104    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
   2.105  unfolding eventually_at dist_nz by auto
   2.106  
   2.107 -lemma eventually_at_infinity:
   2.108 -  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
   2.109 -unfolding eventually_def Rep_net_at_infinity by auto
   2.110 -
   2.111  lemma eventually_within: "eventually P (at a within S) \<longleftrightarrow>
   2.112          (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
   2.113  unfolding eventually_within eventually_at dist_nz by auto
   2.114 @@ -1059,18 +1064,20 @@
   2.115  by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl) 
   2.116  
   2.117  lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
   2.118 -  unfolding eventually_def trivial_limit_def
   2.119 -  using Rep_net_nonempty [of net] by auto
   2.120 +  unfolding trivial_limit_def
   2.121 +  by (auto elim: eventually_rev_mp)
   2.122  
   2.123  lemma always_eventually: "(\<forall>x. P x) ==> eventually P net"
   2.124 -  unfolding eventually_def trivial_limit_def
   2.125 -  using Rep_net_nonempty [of net] by auto
   2.126 +proof -
   2.127 +  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
   2.128 +  thus "eventually P net" by simp
   2.129 +qed
   2.130  
   2.131  lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
   2.132 -  unfolding trivial_limit_def eventually_def by auto
   2.133 +  unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
   2.134  
   2.135  lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
   2.136 -  unfolding trivial_limit_def eventually_def by auto
   2.137 +  unfolding trivial_limit_def ..
   2.138  
   2.139  lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
   2.140    apply (safe elim!: trivial_limit_eventually)