--- a/src/HOL/Limits.thy Mon Dec 03 18:13:23 2012 +0100
+++ b/src/HOL/Limits.thy Mon Dec 03 18:18:59 2012 +0100
@@ -614,24 +614,24 @@
subsection {* Limits *}
-definition filter_lim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
- "filter_lim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
+definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
+ "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
syntax
"_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
translations
- "LIM x F1. f :> F2" == "CONST filter_lim (%x. f) F2 F1"
+ "LIM x F1. f :> F2" == "CONST filterlim (%x. f) F2 F1"
-lemma filter_limE: "(LIM x F1. f x :> F2) \<Longrightarrow> eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1"
- by (auto simp: filter_lim_def eventually_filtermap le_filter_def)
+lemma filterlimE: "(LIM x F1. f x :> F2) \<Longrightarrow> eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1"
+ by (auto simp: filterlim_def eventually_filtermap le_filter_def)
-lemma filter_limI: "(\<And>P. eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1) \<Longrightarrow> (LIM x F1. f x :> F2)"
- by (auto simp: filter_lim_def eventually_filtermap le_filter_def)
+lemma filterlimI: "(\<And>P. eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1) \<Longrightarrow> (LIM x F1. f x :> F2)"
+ by (auto simp: filterlim_def eventually_filtermap le_filter_def)
abbreviation (in topological_space)
tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
- "(f ---> l) F \<equiv> filter_lim f (nhds l) F"
+ "(f ---> l) F \<equiv> filterlim f (nhds l) F"
ML {*
structure Tendsto_Intros = Named_Thms
@@ -644,7 +644,7 @@
setup Tendsto_Intros.setup
lemma tendsto_def: "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
- unfolding filter_lim_def
+ unfolding filterlim_def
proof safe
fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l"
then show "eventually (\<lambda>x. f x \<in> S) F"
@@ -1075,20 +1075,20 @@
subsection {* Limits to @{const at_top} and @{const at_bot} *}
-lemma filter_lim_at_top:
+lemma filterlim_at_top:
fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
- by (safe elim!: filter_limE intro!: filter_limI)
+ by (safe elim!: filterlimE intro!: filterlimI)
(auto simp: eventually_at_top_dense elim!: eventually_elim1)
-lemma filter_lim_at_bot:
+lemma filterlim_at_bot:
fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
- by (safe elim!: filter_limE intro!: filter_limI)
+ by (safe elim!: filterlimE intro!: filterlimI)
(auto simp: eventually_at_bot_dense elim!: eventually_elim1)
-lemma filter_lim_real_sequentially: "LIM x sequentially. real x :> at_top"
- unfolding filter_lim_at_top
+lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
+ unfolding filterlim_at_top
apply (intro allI)
apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI)
apply (auto simp: natceiling_le_eq)
--- a/src/HOL/Log.thy Mon Dec 03 18:13:23 2012 +0100
+++ b/src/HOL/Log.thy Mon Dec 03 18:18:59 2012 +0100
@@ -364,7 +364,7 @@
proof (rule tendstoI)
fix e :: real assume "0 < e"
def Z \<equiv> "e powr (1 / s)"
- from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: filter_lim_at_top)
+ from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: filterlim_at_top)
moreover
from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
by (auto simp: Z_def intro!: powr_less_mono2_neg)
--- a/src/HOL/NSA/HLim.thy Mon Dec 03 18:13:23 2012 +0100
+++ b/src/HOL/NSA/HLim.thy Mon Dec 03 18:18:59 2012 +0100
@@ -133,7 +133,7 @@
lemma NSLIM_self: "(%x. x) -- a --NS> a"
by (simp add: NSLIM_def)
-subsubsection {* Equivalence of @{term filter_lim} and @{term NSLIM} *}
+subsubsection {* Equivalence of @{term filterlim} and @{term NSLIM} *}
lemma LIM_NSLIM:
assumes f: "f -- a --> L" shows "f -- a --NS> L"