define finer-than ordering on net type; move some theorems into Limits.thy
authorhuffman
Sun Apr 25 20:48:19 2010 -0700 (2010-04-25)
changeset 363609d8f7efd9289
parent 36359 e5c785c166b2
child 36361 1debc8e29f6a
define finer-than ordering on net type; move some theorems into Limits.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Limits.thy	Sun Apr 25 16:23:40 2010 -0700
     1.2 +++ b/src/HOL/Limits.thy	Sun Apr 25 20:48:19 2010 -0700
     1.3 @@ -45,6 +45,10 @@
     1.4    assumes "is_filter net" shows "eventually P (Abs_net net) = net P"
     1.5  unfolding eventually_def using assms by (simp add: Abs_net_inverse)
     1.6  
     1.7 +lemma expand_net_eq:
     1.8 +  shows "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
     1.9 +unfolding Rep_net_inject [symmetric] expand_fun_eq eventually_def ..
    1.10 +
    1.11  lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
    1.12  unfolding eventually_def
    1.13  by (rule is_filter.True [OF is_filter_Rep_net])
    1.14 @@ -95,6 +99,62 @@
    1.15  using assms by (auto elim!: eventually_rev_mp)
    1.16  
    1.17  
    1.18 +subsection {* Finer-than relation *}
    1.19 +
    1.20 +text {* @{term "net \<le> net'"} means that @{term net'} is finer than
    1.21 +@{term net}. *}
    1.22 +
    1.23 +instantiation net :: (type) "{order,top}"
    1.24 +begin
    1.25 +
    1.26 +definition
    1.27 +  le_net_def [code del]:
    1.28 +    "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net \<longrightarrow> eventually P net')"
    1.29 +
    1.30 +definition
    1.31 +  less_net_def [code del]:
    1.32 +    "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
    1.33 +
    1.34 +definition
    1.35 +  top_net_def [code del]:
    1.36 +    "top = Abs_net (\<lambda>P. True)"
    1.37 +
    1.38 +lemma eventually_top [simp]: "eventually P top"
    1.39 +unfolding top_net_def
    1.40 +by (subst eventually_Abs_net, rule is_filter.intro, auto)
    1.41 +
    1.42 +instance proof
    1.43 +  fix x y :: "'a net" show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    1.44 +    by (rule less_net_def)
    1.45 +next
    1.46 +  fix x :: "'a net" show "x \<le> x"
    1.47 +    unfolding le_net_def by simp
    1.48 +next
    1.49 +  fix x y z :: "'a net" assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
    1.50 +    unfolding le_net_def by simp
    1.51 +next
    1.52 +  fix x y :: "'a net" assume "x \<le> y" and "y \<le> x" thus "x = y"
    1.53 +    unfolding le_net_def expand_net_eq by fast
    1.54 +next
    1.55 +  fix x :: "'a net" show "x \<le> top"
    1.56 +    unfolding le_net_def by simp
    1.57 +qed
    1.58 +
    1.59 +end
    1.60 +
    1.61 +lemma net_leD:
    1.62 +  "net \<le> net' \<Longrightarrow> eventually P net \<Longrightarrow> eventually P net'"
    1.63 +unfolding le_net_def by simp
    1.64 +
    1.65 +lemma net_leI:
    1.66 +  "(\<And>P. eventually P net \<Longrightarrow> eventually P net') \<Longrightarrow> net \<le> net'"
    1.67 +unfolding le_net_def by simp
    1.68 +
    1.69 +lemma eventually_False:
    1.70 +  "eventually (\<lambda>x. False) net \<longleftrightarrow> net = top"
    1.71 +unfolding expand_net_eq by (auto elim: eventually_rev_mp)
    1.72 +
    1.73 +
    1.74  subsection {* Standard Nets *}
    1.75  
    1.76  definition
    1.77 @@ -129,6 +189,9 @@
    1.78  by (rule eventually_Abs_net, rule is_filter.intro)
    1.79     (auto elim!: eventually_rev_mp)
    1.80  
    1.81 +lemma within_UNIV: "net within UNIV = net"
    1.82 +  unfolding expand_net_eq eventually_within by simp
    1.83 +
    1.84  lemma eventually_at_topological:
    1.85    "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.86  unfolding at_def
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 25 16:23:40 2010 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 25 20:48:19 2010 -0700
     2.3 @@ -976,15 +976,6 @@
     2.4  
     2.5  text{* Prove That They are all nets. *}
     2.6  
     2.7 -(* TODO: move to HOL/Limits.thy *)
     2.8 -lemma expand_net_eq:
     2.9 -  "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
    2.10 -  unfolding Rep_net_inject [symmetric] expand_fun_eq eventually_def ..
    2.11 -
    2.12 -(* TODO: move to HOL/Limits.thy *)
    2.13 -lemma within_UNIV: "net within UNIV = net"
    2.14 -  unfolding expand_net_eq eventually_within by simp
    2.15 -
    2.16  lemma eventually_at_infinity:
    2.17    "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
    2.18  unfolding at_infinity_def