author | Manuel Eberl <eberlm@in.tum.de> |

Wed Aug 23 01:05:39 2017 +0200 (21 months ago) | |

changeset 66488 | 9d83e8fe3de3 |

parent 66486 | ffaaa83543b2 |

child 66489 | 495df6232517 |

HOL-Library: going_to filter

NEWS | file | annotate | diff | revisions | |

src/HOL/Library/Going_To_Filter.thy | file | annotate | diff | revisions | |

src/HOL/Library/Library.thy | file | annotate | diff | revisions |

1.1 --- a/NEWS Tue Aug 22 21:36:48 2017 +0200 1.2 +++ b/NEWS Wed Aug 23 01:05:39 2017 +0200 1.3 @@ -215,6 +215,9 @@ 1.4 * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has 1.5 been renamed to bij_swap_compose_bij. INCOMPATIBILITY. 1.6 1.7 +* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F" 1.8 +filter for describing points x such that f(x) is in the filter F. 1.9 + 1.10 * Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been 1.11 renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name 1.12 space. INCOMPATIBILITY.

2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 2.2 +++ b/src/HOL/Library/Going_To_Filter.thy Wed Aug 23 01:05:39 2017 +0200 2.3 @@ -0,0 +1,124 @@ 2.4 +(* 2.5 + File: Going_To_Filter.thy 2.6 + Author: Manuel Eberl, TU München 2.7 + 2.8 + A filter describing the points x such that f(x) tends to some other filter. 2.9 +*) 2.10 +section \<open>The `going\_to' filter\<close> 2.11 +theory Going_To_Filter 2.12 + imports Complex_Main 2.13 +begin 2.14 + 2.15 +definition going_to_within :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" 2.16 + ("(_)/ going'_to (_)/ within (_)" [1000,60,60] 60) where 2.17 + "f going_to F within A = inf (filtercomap f F) (principal A)" 2.18 + 2.19 +abbreviation going_to :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter" 2.20 + (infix "going'_to" 60) 2.21 + where "f going_to F \<equiv> f going_to F within UNIV" 2.22 + 2.23 +text \<open> 2.24 + The `going\_to' filter is, in a sense, the opposite of @{term filtermap}. 2.25 + It corresponds to the intuition of, given a function $f: A \to B$ and a filter $F$ on the 2.26 + range of $B$, looking at such values of $x$ that $f(x)$ approaches $F$. This can be 2.27 + written as @{term "f going_to F"}. 2.28 + 2.29 + A classic example is the @{term "at_infinity"} filter, which describes the neigbourhood 2.30 + of infinity (i.\,e.\ all values sufficiently far away from the zero). This can also be written 2.31 + as @{term "norm going_to at_top"}. 2.32 + 2.33 + Additionally, the `going\_to' filter can be restricted with an optional `within' parameter. 2.34 + For instance, if one would would want to consider the filter of complex numbers near infinity 2.35 + that do not lie on the negative real line, one could write 2.36 + @{term "norm going_to at_top within - complex_of_real ` {..0}"}. 2.37 + 2.38 + A third, less mathematical example lies in the complexity analysis of algorithms. 2.39 + Suppose we wanted to say that an algorithm on lists takes $O(n^2)$ time where $n$ is 2.40 + the length of the input list. We can write this using the Landau symbols from the AFP, 2.41 + where the underlying filter is @{term "length going_to at_top"}. If, on the other hand, 2.42 + we want to look the complexity of the algorithm on sorted lists, we could use the filter 2.43 + @{term "length going_to at_top within {xs. sorted xs}"}. 2.44 +\<close> 2.45 + 2.46 +lemma going_to_def: "f going_to F = filtercomap f F" 2.47 + by (simp add: going_to_within_def) 2.48 + 2.49 +lemma eventually_going_toI [intro]: 2.50 + assumes "eventually P F" 2.51 + shows "eventually (\<lambda>x. P (f x)) (f going_to F)" 2.52 + using assms by (auto simp: going_to_def) 2.53 + 2.54 +lemma filterlim_going_toI_weak [intro]: "filterlim f F (f going_to F within A)" 2.55 + unfolding going_to_within_def 2.56 + by (meson filterlim_filtercomap filterlim_iff inf_le1 le_filter_def) 2.57 + 2.58 +lemma going_to_mono: "F \<le> G \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f going_to F within A \<le> f going_to G within B" 2.59 + unfolding going_to_within_def by (intro inf_mono filtercomap_mono) simp_all 2.60 + 2.61 +lemma going_to_inf: 2.62 + "f going_to (inf F G) within A = inf (f going_to F within A) (f going_to G within A)" 2.63 + by (simp add: going_to_within_def filtercomap_inf inf_assoc inf_commute inf_left_commute) 2.64 + 2.65 +lemma going_to_sup: 2.66 + "f going_to (sup F G) within A \<ge> sup (f going_to F within A) (f going_to G within A)" 2.67 + by (auto simp: going_to_within_def intro!: inf.coboundedI1 filtercomap_sup filtercomap_mono) 2.68 + 2.69 +lemma going_to_top [simp]: "f going_to top within A = principal A" 2.70 + by (simp add: going_to_within_def) 2.71 + 2.72 +lemma going_to_bot [simp]: "f going_to bot within A = bot" 2.73 + by (simp add: going_to_within_def) 2.74 + 2.75 +lemma going_to_principal: 2.76 + "f going_to principal A within B = principal (f -` A \<inter> B)" 2.77 + by (simp add: going_to_within_def) 2.78 + 2.79 +lemma going_to_within_empty [simp]: "f going_to F within {} = bot" 2.80 + by (simp add: going_to_within_def) 2.81 + 2.82 +lemma going_to_within_union [simp]: 2.83 + "f going_to F within (A \<union> B) = sup (f going_to F within A) (f going_to F within B)" 2.84 + by (simp add: going_to_within_def inf_sup_distrib1 [symmetric]) 2.85 + 2.86 +lemma eventually_going_to_at_top_linorder: 2.87 + fixes f :: "'a \<Rightarrow> 'b :: linorder" 2.88 + shows "eventually P (f going_to at_top within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x \<ge> C \<longrightarrow> P x)" 2.89 + unfolding going_to_within_def eventually_filtercomap 2.90 + eventually_inf_principal eventually_at_top_linorder by fast 2.91 + 2.92 +lemma eventually_going_to_at_bot_linorder: 2.93 + fixes f :: "'a \<Rightarrow> 'b :: linorder" 2.94 + shows "eventually P (f going_to at_bot within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x \<le> C \<longrightarrow> P x)" 2.95 + unfolding going_to_within_def eventually_filtercomap 2.96 + eventually_inf_principal eventually_at_bot_linorder by fast 2.97 + 2.98 +lemma eventually_going_to_at_top_dense: 2.99 + fixes f :: "'a \<Rightarrow> 'b :: {linorder,no_top}" 2.100 + shows "eventually P (f going_to at_top within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x > C \<longrightarrow> P x)" 2.101 + unfolding going_to_within_def eventually_filtercomap 2.102 + eventually_inf_principal eventually_at_top_dense by fast 2.103 + 2.104 +lemma eventually_going_to_at_bot_dense: 2.105 + fixes f :: "'a \<Rightarrow> 'b :: {linorder,no_bot}" 2.106 + shows "eventually P (f going_to at_bot within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x < C \<longrightarrow> P x)" 2.107 + unfolding going_to_within_def eventually_filtercomap 2.108 + eventually_inf_principal eventually_at_bot_dense by fast 2.109 + 2.110 +lemma eventually_going_to_nhds: 2.111 + "eventually P (f going_to nhds a within A) \<longleftrightarrow> 2.112 + (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>A. f x \<in> S \<longrightarrow> P x))" 2.113 + unfolding going_to_within_def eventually_filtercomap eventually_inf_principal 2.114 + eventually_nhds by fast 2.115 + 2.116 +lemma eventually_going_to_at: 2.117 + "eventually P (f going_to (at a within B) within A) \<longleftrightarrow> 2.118 + (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>A. f x \<in> B \<inter> S - {a} \<longrightarrow> P x))" 2.119 + unfolding at_within_def going_to_inf eventually_inf_principal 2.120 + eventually_going_to_nhds going_to_principal by fast 2.121 + 2.122 +lemma norm_going_to_at_top_eq: "norm going_to at_top = at_infinity" 2.123 + by (simp add: eventually_at_infinity eventually_going_to_at_top_linorder filter_eq_iff) 2.124 + 2.125 +lemmas at_infinity_altdef = norm_going_to_at_top_eq [symmetric] 2.126 + 2.127 +end

3.1 --- a/src/HOL/Library/Library.thy Tue Aug 22 21:36:48 2017 +0200 3.2 +++ b/src/HOL/Library/Library.thy Wed Aug 23 01:05:39 2017 +0200 3.3 @@ -30,6 +30,7 @@ 3.4 Function_Division 3.5 Function_Growth 3.6 Fun_Lexorder 3.7 + Going_To_Filter 3.8 Groups_Big_Fun 3.9 Indicator_Function 3.10 Infinite_Set