src/HOL/Limits.thy
changeset 36629 de62713aec6e
parent 36360 9d8f7efd9289
child 36630 aa1f8acdcc1c
     1.1 --- a/src/HOL/Limits.thy	Sat May 01 07:53:42 2010 -0700
     1.2 +++ b/src/HOL/Limits.thy	Sat May 01 09:43:40 2010 -0700
     1.3 @@ -101,26 +101,26 @@
     1.4  
     1.5  subsection {* Finer-than relation *}
     1.6  
     1.7 -text {* @{term "net \<le> net'"} means that @{term net'} is finer than
     1.8 -@{term net}. *}
     1.9 +text {* @{term "net \<le> net'"} means that @{term net} is finer than
    1.10 +@{term net'}. *}
    1.11  
    1.12 -instantiation net :: (type) "{order,top}"
    1.13 +instantiation net :: (type) "{order,bot}"
    1.14  begin
    1.15  
    1.16  definition
    1.17    le_net_def [code del]:
    1.18 -    "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net \<longrightarrow> eventually P net')"
    1.19 +    "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
    1.20  
    1.21  definition
    1.22    less_net_def [code del]:
    1.23      "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
    1.24  
    1.25  definition
    1.26 -  top_net_def [code del]:
    1.27 -    "top = Abs_net (\<lambda>P. True)"
    1.28 +  bot_net_def [code del]:
    1.29 +    "bot = Abs_net (\<lambda>P. True)"
    1.30  
    1.31 -lemma eventually_top [simp]: "eventually P top"
    1.32 -unfolding top_net_def
    1.33 +lemma eventually_bot [simp]: "eventually P bot"
    1.34 +unfolding bot_net_def
    1.35  by (subst eventually_Abs_net, rule is_filter.intro, auto)
    1.36  
    1.37  instance proof
    1.38 @@ -136,22 +136,22 @@
    1.39    fix x y :: "'a net" assume "x \<le> y" and "y \<le> x" thus "x = y"
    1.40      unfolding le_net_def expand_net_eq by fast
    1.41  next
    1.42 -  fix x :: "'a net" show "x \<le> top"
    1.43 +  fix x :: "'a net" show "bot \<le> x"
    1.44      unfolding le_net_def by simp
    1.45  qed
    1.46  
    1.47  end
    1.48  
    1.49  lemma net_leD:
    1.50 -  "net \<le> net' \<Longrightarrow> eventually P net \<Longrightarrow> eventually P net'"
    1.51 +  "net \<le> net' \<Longrightarrow> eventually P net' \<Longrightarrow> eventually P net"
    1.52  unfolding le_net_def by simp
    1.53  
    1.54  lemma net_leI:
    1.55 -  "(\<And>P. eventually P net \<Longrightarrow> eventually P net') \<Longrightarrow> net \<le> net'"
    1.56 +  "(\<And>P. eventually P net' \<Longrightarrow> eventually P net) \<Longrightarrow> net \<le> net'"
    1.57  unfolding le_net_def by simp
    1.58  
    1.59  lemma eventually_False:
    1.60 -  "eventually (\<lambda>x. False) net \<longleftrightarrow> net = top"
    1.61 +  "eventually (\<lambda>x. False) net \<longleftrightarrow> net = bot"
    1.62  unfolding expand_net_eq by (auto elim: eventually_rev_mp)
    1.63  
    1.64