# HG changeset patch # User eberlm # Date 1503491842 -7200 # Node ID 495df623251763a83d15e86c3c5d75c2513f07df # Parent 307c19f24d5cf183e4a3ddcc1efde81cc59e30b7# Parent 9d83e8fe3de35243864a84968eba09cbbb4a6020 Merged diff -r 307c19f24d5c -r 495df6232517 NEWS --- a/NEWS Wed Aug 23 00:38:53 2017 +0100 +++ b/NEWS Wed Aug 23 14:37:22 2017 +0200 @@ -215,6 +215,9 @@ * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has been renamed to bij_swap_compose_bij. INCOMPATIBILITY. +* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F" +filter for describing points x such that f(x) is in the filter F. + * Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space. INCOMPATIBILITY. diff -r 307c19f24d5c -r 495df6232517 src/HOL/Library/Going_To_Filter.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Going_To_Filter.thy Wed Aug 23 14:37:22 2017 +0200 @@ -0,0 +1,124 @@ +(* + File: Going_To_Filter.thy + Author: Manuel Eberl, TU München + + A filter describing the points x such that f(x) tends to some other filter. +*) +section \The `going\_to' filter\ +theory Going_To_Filter + imports Complex_Main +begin + +definition going_to_within :: "('a \ 'b) \ 'b filter \ 'a set \ 'a filter" + ("(_)/ going'_to (_)/ within (_)" [1000,60,60] 60) where + "f going_to F within A = inf (filtercomap f F) (principal A)" + +abbreviation going_to :: "('a \ 'b) \ 'b filter \ 'a filter" + (infix "going'_to" 60) + where "f going_to F \ f going_to F within UNIV" + +text \ + The `going\_to' filter is, in a sense, the opposite of @{term filtermap}. + It corresponds to the intuition of, given a function $f: A \to B$ and a filter $F$ on the + range of $B$, looking at such values of $x$ that $f(x)$ approaches $F$. This can be + written as @{term "f going_to F"}. + + A classic example is the @{term "at_infinity"} filter, which describes the neigbourhood + of infinity (i.\,e.\ all values sufficiently far away from the zero). This can also be written + as @{term "norm going_to at_top"}. + + Additionally, the `going\_to' filter can be restricted with an optional `within' parameter. + For instance, if one would would want to consider the filter of complex numbers near infinity + that do not lie on the negative real line, one could write + @{term "norm going_to at_top within - complex_of_real ` {..0}"}. + + A third, less mathematical example lies in the complexity analysis of algorithms. + Suppose we wanted to say that an algorithm on lists takes $O(n^2)$ time where $n$ is + the length of the input list. We can write this using the Landau symbols from the AFP, + where the underlying filter is @{term "length going_to at_top"}. If, on the other hand, + we want to look the complexity of the algorithm on sorted lists, we could use the filter + @{term "length going_to at_top within {xs. sorted xs}"}. +\ + +lemma going_to_def: "f going_to F = filtercomap f F" + by (simp add: going_to_within_def) + +lemma eventually_going_toI [intro]: + assumes "eventually P F" + shows "eventually (\x. P (f x)) (f going_to F)" + using assms by (auto simp: going_to_def) + +lemma filterlim_going_toI_weak [intro]: "filterlim f F (f going_to F within A)" + unfolding going_to_within_def + by (meson filterlim_filtercomap filterlim_iff inf_le1 le_filter_def) + +lemma going_to_mono: "F \ G \ A \ B \ f going_to F within A \ f going_to G within B" + unfolding going_to_within_def by (intro inf_mono filtercomap_mono) simp_all + +lemma going_to_inf: + "f going_to (inf F G) within A = inf (f going_to F within A) (f going_to G within A)" + by (simp add: going_to_within_def filtercomap_inf inf_assoc inf_commute inf_left_commute) + +lemma going_to_sup: + "f going_to (sup F G) within A \ sup (f going_to F within A) (f going_to G within A)" + by (auto simp: going_to_within_def intro!: inf.coboundedI1 filtercomap_sup filtercomap_mono) + +lemma going_to_top [simp]: "f going_to top within A = principal A" + by (simp add: going_to_within_def) + +lemma going_to_bot [simp]: "f going_to bot within A = bot" + by (simp add: going_to_within_def) + +lemma going_to_principal: + "f going_to principal A within B = principal (f -` A \ B)" + by (simp add: going_to_within_def) + +lemma going_to_within_empty [simp]: "f going_to F within {} = bot" + by (simp add: going_to_within_def) + +lemma going_to_within_union [simp]: + "f going_to F within (A \ B) = sup (f going_to F within A) (f going_to F within B)" + by (simp add: going_to_within_def inf_sup_distrib1 [symmetric]) + +lemma eventually_going_to_at_top_linorder: + fixes f :: "'a \ 'b :: linorder" + shows "eventually P (f going_to at_top within A) \ (\C. \x\A. f x \ C \ P x)" + unfolding going_to_within_def eventually_filtercomap + eventually_inf_principal eventually_at_top_linorder by fast + +lemma eventually_going_to_at_bot_linorder: + fixes f :: "'a \ 'b :: linorder" + shows "eventually P (f going_to at_bot within A) \ (\C. \x\A. f x \ C \ P x)" + unfolding going_to_within_def eventually_filtercomap + eventually_inf_principal eventually_at_bot_linorder by fast + +lemma eventually_going_to_at_top_dense: + fixes f :: "'a \ 'b :: {linorder,no_top}" + shows "eventually P (f going_to at_top within A) \ (\C. \x\A. f x > C \ P x)" + unfolding going_to_within_def eventually_filtercomap + eventually_inf_principal eventually_at_top_dense by fast + +lemma eventually_going_to_at_bot_dense: + fixes f :: "'a \ 'b :: {linorder,no_bot}" + shows "eventually P (f going_to at_bot within A) \ (\C. \x\A. f x < C \ P x)" + unfolding going_to_within_def eventually_filtercomap + eventually_inf_principal eventually_at_bot_dense by fast + +lemma eventually_going_to_nhds: + "eventually P (f going_to nhds a within A) \ + (\S. open S \ a \ S \ (\x\A. f x \ S \ P x))" + unfolding going_to_within_def eventually_filtercomap eventually_inf_principal + eventually_nhds by fast + +lemma eventually_going_to_at: + "eventually P (f going_to (at a within B) within A) \ + (\S. open S \ a \ S \ (\x\A. f x \ B \ S - {a} \ P x))" + unfolding at_within_def going_to_inf eventually_inf_principal + eventually_going_to_nhds going_to_principal by fast + +lemma norm_going_to_at_top_eq: "norm going_to at_top = at_infinity" + by (simp add: eventually_at_infinity eventually_going_to_at_top_linorder filter_eq_iff) + +lemmas at_infinity_altdef = norm_going_to_at_top_eq [symmetric] + +end diff -r 307c19f24d5c -r 495df6232517 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Aug 23 00:38:53 2017 +0100 +++ b/src/HOL/Library/Library.thy Wed Aug 23 14:37:22 2017 +0200 @@ -30,6 +30,7 @@ Function_Division Function_Growth Fun_Lexorder + Going_To_Filter Groups_Big_Fun Indicator_Function Infinite_Set