src/HOL/Limits.thy
changeset 50322 b06b95a5fda2
parent 50247 491c5c81c2e8
child 50323 3764d4620fb3
     1.1 --- a/src/HOL/Limits.thy	Mon Dec 03 18:13:23 2012 +0100
     1.2 +++ b/src/HOL/Limits.thy	Mon Dec 03 18:18:59 2012 +0100
     1.3 @@ -614,24 +614,24 @@
     1.4  
     1.5  subsection {* Limits *}
     1.6  
     1.7 -definition filter_lim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
     1.8 -  "filter_lim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
     1.9 +definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
    1.10 +  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
    1.11  
    1.12  syntax
    1.13    "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
    1.14  
    1.15  translations
    1.16 -  "LIM x F1. f :> F2"   == "CONST filter_lim (%x. f) F2 F1"
    1.17 +  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
    1.18  
    1.19 -lemma filter_limE: "(LIM x F1. f x :> F2) \<Longrightarrow> eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1"
    1.20 -  by (auto simp: filter_lim_def eventually_filtermap le_filter_def)
    1.21 +lemma filterlimE: "(LIM x F1. f x :> F2) \<Longrightarrow> eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1"
    1.22 +  by (auto simp: filterlim_def eventually_filtermap le_filter_def)
    1.23  
    1.24 -lemma filter_limI: "(\<And>P. eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1) \<Longrightarrow> (LIM x F1. f x :> F2)"
    1.25 -  by (auto simp: filter_lim_def eventually_filtermap le_filter_def)
    1.26 +lemma filterlimI: "(\<And>P. eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1) \<Longrightarrow> (LIM x F1. f x :> F2)"
    1.27 +  by (auto simp: filterlim_def eventually_filtermap le_filter_def)
    1.28  
    1.29  abbreviation (in topological_space)
    1.30    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
    1.31 -  "(f ---> l) F \<equiv> filter_lim f (nhds l) F"
    1.32 +  "(f ---> l) F \<equiv> filterlim f (nhds l) F"
    1.33  
    1.34  ML {*
    1.35  structure Tendsto_Intros = Named_Thms
    1.36 @@ -644,7 +644,7 @@
    1.37  setup Tendsto_Intros.setup
    1.38  
    1.39  lemma tendsto_def: "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
    1.40 -  unfolding filter_lim_def
    1.41 +  unfolding filterlim_def
    1.42  proof safe
    1.43    fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l"
    1.44    then show "eventually (\<lambda>x. f x \<in> S) F"
    1.45 @@ -1075,20 +1075,20 @@
    1.46  
    1.47  subsection {* Limits to @{const at_top} and @{const at_bot} *}
    1.48  
    1.49 -lemma filter_lim_at_top:
    1.50 +lemma filterlim_at_top:
    1.51    fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
    1.52    shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
    1.53 -  by (safe elim!: filter_limE intro!: filter_limI)
    1.54 +  by (safe elim!: filterlimE intro!: filterlimI)
    1.55       (auto simp: eventually_at_top_dense elim!: eventually_elim1)
    1.56  
    1.57 -lemma filter_lim_at_bot: 
    1.58 +lemma filterlim_at_bot: 
    1.59    fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
    1.60    shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
    1.61 -  by (safe elim!: filter_limE intro!: filter_limI)
    1.62 +  by (safe elim!: filterlimE intro!: filterlimI)
    1.63       (auto simp: eventually_at_bot_dense elim!: eventually_elim1)
    1.64  
    1.65 -lemma filter_lim_real_sequentially: "LIM x sequentially. real x :> at_top"
    1.66 -  unfolding filter_lim_at_top
    1.67 +lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
    1.68 +  unfolding filterlim_at_top
    1.69    apply (intro allI)
    1.70    apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI)
    1.71    apply (auto simp: natceiling_le_eq)