--- a/src/HOL/Limits.thy Fri Aug 19 19:01:00 2011 -0700
+++ b/src/HOL/Limits.thy Sat Aug 20 06:34:51 2011 -0700
@@ -216,6 +216,13 @@
"eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
+abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
+ where "trivial_limit F \<equiv> F = bot"
+
+lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
+ by (rule eventually_False [symmetric])
+
+
subsection {* Map function for filters *}
definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
@@ -259,9 +266,11 @@
then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
qed auto
-lemma sequentially_bot [simp]: "sequentially \<noteq> bot"
+lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
unfolding filter_eq_iff eventually_sequentially by auto
+lemmas trivial_limit_sequentially = sequentially_bot
+
lemma eventually_False_sequentially [simp]:
"\<not> eventually (\<lambda>n. False) sequentially"
by (simp add: eventually_False)
@@ -272,12 +281,6 @@
by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
-definition trivial_limit :: "'a filter \<Rightarrow> bool"
- where "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
-
-lemma trivial_limit_sequentially [intro]: "\<not> trivial_limit sequentially"
- by (auto simp add: trivial_limit_def eventually_sequentially)
-
subsection {* Standard filters *}
definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 19 19:01:00 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Aug 20 06:34:51 2011 -0700
@@ -966,13 +966,8 @@
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
-lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
- unfolding trivial_limit_def ..
-
lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
- apply (safe elim!: trivial_limit_eventually)
- apply (simp add: eventually_False [symmetric])
- done
+ by (simp add: filter_eq_iff)
text{* Combining theorems for "eventually" *}