remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
authorhuffman
Mon Aug 15 12:13:46 2011 -0700 (2011-08-15)
changeset 44211bd7c586b902e
parent 44210 eba74571833b
child 44212 4d10e7f342b1
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 10:49:48 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 12:13:46 2011 -0700
     1.3 @@ -1370,7 +1370,7 @@
     1.4  lemma Lim_component_eq_cart: fixes f :: "'a \<Rightarrow> real^'n"
     1.5    assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$i = b) net"
     1.6    shows "l$i = b"
     1.7 -  using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge_cart[OF net, of b i] and
     1.8 +  using ev[unfolded order_eq_iff eventually_conj_iff] using Lim_component_ge_cart[OF net, of b i] and
     1.9      Lim_component_le_cart[OF net, of i b] by auto
    1.10  
    1.11  lemma connected_ivt_component_cart: fixes x::"real^'n" shows
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 10:49:48 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 12:13:46 2011 -0700
     2.3 @@ -976,21 +976,10 @@
     2.4  
     2.5  text{* Combining theorems for "eventually" *}
     2.6  
     2.7 -lemma eventually_conjI:
     2.8 -  "\<lbrakk>eventually (\<lambda>x. P x) net; eventually (\<lambda>x. Q x) net\<rbrakk>
     2.9 -    \<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) net"
    2.10 -by (rule eventually_conj) (* FIXME: delete *)
    2.11 -
    2.12  lemma eventually_rev_mono:
    2.13    "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
    2.14  using eventually_mono [of P Q] by fast
    2.15  
    2.16 -lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net"
    2.17 -  by (rule eventually_conj_iff) (* FIXME: delete *)
    2.18 -
    2.19 -lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
    2.20 -  by (rule eventually_False) (* FIXME: delete *)
    2.21 -
    2.22  lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
    2.23    by (simp add: eventually_False)
    2.24  
    2.25 @@ -1255,7 +1244,7 @@
    2.26      hence "dist (f x) 0 < e" by (simp add: dist_norm)
    2.27    }
    2.28    thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
    2.29 -    using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (g x) 0 < e" net]
    2.30 +    using eventually_conj_iff[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (g x) 0 < e" net]
    2.31      using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (g x) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net]
    2.32      using assms `e>0` unfolding tendsto_iff by auto
    2.33  qed
    2.34 @@ -1271,7 +1260,7 @@
    2.35      assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
    2.36      hence "dist (f x) 0 < e" by (simp add: dist_norm)}
    2.37    thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
    2.38 -    using eventually_and[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
    2.39 +    using eventually_conj_iff[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
    2.40      using eventually_mono[of "\<lambda>x. norm (f x) \<le> norm (g x) \<and> dist (g x) 0 < e" "\<lambda>x. dist (f x) 0 < e" net]
    2.41      using assms `e>0` unfolding tendsto_iff by blast
    2.42  qed
    2.43 @@ -1304,7 +1293,7 @@
    2.44    with assms(2) have "eventually (\<lambda>x. dist (f x) l < dist a l - e) net"
    2.45      by (rule tendstoD)
    2.46    with assms(3) have "eventually (\<lambda>x. dist a (f x) \<le> e \<and> dist (f x) l < dist a l - e) net"
    2.47 -    by (rule eventually_conjI)
    2.48 +    by (rule eventually_conj)
    2.49    then obtain w where "dist a (f w) \<le> e" "dist (f w) l < dist a l - e"
    2.50      using assms(1) eventually_happens by auto
    2.51    hence "dist a (f w) + dist (f w) l < e + (dist a l - e)"
    2.52 @@ -1326,7 +1315,7 @@
    2.53    with assms(2) have "eventually (\<lambda>x. dist (f x) l < norm l - e) net"
    2.54      by (rule tendstoD)
    2.55    with assms(3) have "eventually (\<lambda>x. norm (f x) \<le> e \<and> dist (f x) l < norm l - e) net"
    2.56 -    by (rule eventually_conjI)
    2.57 +    by (rule eventually_conj)
    2.58    then obtain w where "norm (f w) \<le> e" "dist (f w) l < norm l - e"
    2.59      using assms(1) eventually_happens by auto
    2.60    hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm)
    2.61 @@ -1345,7 +1334,7 @@
    2.62    with assms(2) have "eventually (\<lambda>x. dist (f x) l < e - norm l) net"
    2.63      by (rule tendstoD)
    2.64    with assms(3) have "eventually (\<lambda>x. e \<le> norm (f x) \<and> dist (f x) l < e - norm l) net"
    2.65 -    by (rule eventually_conjI)
    2.66 +    by (rule eventually_conj)
    2.67    then obtain w where "e \<le> norm (f w)" "dist (f w) l < e - norm l"
    2.68      using assms(1) eventually_happens by auto
    2.69    hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm)
    2.70 @@ -4236,7 +4225,7 @@
    2.71    { fix x and e::real assume "x\<in>s" "e>0"
    2.72      have "eventually (\<lambda>n. \<forall>x\<in>s. norm (f n x - g x) < e / 3) net" using `e>0` assms(3)[THEN spec[where x="e/3"]] by auto
    2.73      then obtain n where n:"\<forall>xa\<in>s. norm (f n xa - g xa) < e / 3"  "continuous_on s (f n)"
    2.74 -      using eventually_and[of "(\<lambda>n. \<forall>x\<in>s. norm (f n x - g x) < e / 3)" "(\<lambda>n. continuous_on s (f n))" net] assms(1,2) eventually_happens by blast
    2.75 +      using eventually_conj_iff[of "(\<lambda>n. \<forall>x\<in>s. norm (f n x - g x) < e / 3)" "(\<lambda>n. continuous_on s (f n))" net] assms(1,2) eventually_happens by blast
    2.76      have "e / 3 > 0" using `e>0` by auto
    2.77      then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f n x') (f n x) < e / 3"
    2.78        using n(2)[unfolded continuous_on_iff, THEN bspec[where x=x], OF `x\<in>s`, THEN spec[where x="e/3"]] by blast
    2.79 @@ -5305,7 +5294,7 @@
    2.80  lemma Lim_component_eq: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
    2.81    assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$$i = b) net"
    2.82    shows "l$$i = b"
    2.83 -  using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
    2.84 +  using ev[unfolded order_eq_iff eventually_conj_iff] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
    2.85  text{* Limits relative to a union.                                               *}
    2.86  
    2.87  lemma eventually_within_Un: