# HG changeset patch
# User huffman
# Date 1313847291 25200
# Node ID 8321948340ea589ab38f937586dbbb97030f1c48
# Parent  33439faadd6715bb2b06bbc93de2916c3070f562
redefine constant 'trivial_limit' as an abbreviation

diff -r 33439faadd67 -r 8321948340ea src/HOL/Limits.thy
--- 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)
diff -r 33439faadd67 -r 8321948340ea src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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" *}