redefine constant 'trivial_limit' as an abbreviation
authorhuffman
Sat Aug 20 06:34:51 2011 -0700 (2011-08-20)
changeset 443428321948340ea
parent 44320 33439faadd67
child 44343 e5294bcf58a4
redefine constant 'trivial_limit' as an abbreviation
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Limits.thy	Fri Aug 19 19:01:00 2011 -0700
     1.2 +++ b/src/HOL/Limits.thy	Sat Aug 20 06:34:51 2011 -0700
     1.3 @@ -216,6 +216,13 @@
     1.4    "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
     1.5    unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
     1.6  
     1.7 +abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
     1.8 +  where "trivial_limit F \<equiv> F = bot"
     1.9 +
    1.10 +lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
    1.11 +  by (rule eventually_False [symmetric])
    1.12 +
    1.13 +
    1.14  subsection {* Map function for filters *}
    1.15  
    1.16  definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
    1.17 @@ -259,9 +266,11 @@
    1.18    then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
    1.19  qed auto
    1.20  
    1.21 -lemma sequentially_bot [simp]: "sequentially \<noteq> bot"
    1.22 +lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
    1.23    unfolding filter_eq_iff eventually_sequentially by auto
    1.24  
    1.25 +lemmas trivial_limit_sequentially = sequentially_bot
    1.26 +
    1.27  lemma eventually_False_sequentially [simp]:
    1.28    "\<not> eventually (\<lambda>n. False) sequentially"
    1.29    by (simp add: eventually_False)
    1.30 @@ -272,12 +281,6 @@
    1.31    by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
    1.32  
    1.33  
    1.34 -definition trivial_limit :: "'a filter \<Rightarrow> bool"
    1.35 -  where "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
    1.36 -
    1.37 -lemma trivial_limit_sequentially [intro]: "\<not> trivial_limit sequentially"
    1.38 -  by (auto simp add: trivial_limit_def eventually_sequentially)
    1.39 -
    1.40  subsection {* Standard filters *}
    1.41  
    1.42  definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 19 19:01:00 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Aug 20 06:34:51 2011 -0700
     2.3 @@ -966,13 +966,8 @@
     2.4  lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
     2.5    unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
     2.6  
     2.7 -lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
     2.8 -  unfolding trivial_limit_def ..
     2.9 -
    2.10  lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
    2.11 -  apply (safe elim!: trivial_limit_eventually)
    2.12 -  apply (simp add: eventually_False [symmetric])
    2.13 -  done
    2.14 +  by (simp add: filter_eq_iff)
    2.15  
    2.16  text{* Combining theorems for "eventually" *}
    2.17