src/HOL/Library/Going_To_Filter.thy
 author Manuel Eberl Mon Mar 26 16:14:16 2018 +0200 (19 months ago) changeset 67951 655aa11359dc parent 67409 060efe532189 child 68406 6beb45f6cf67 permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
 eberlm@66488  1 (*  eberlm@66488  2  File: Going_To_Filter.thy  eberlm@66488  3  Author: Manuel Eberl, TU München  eberlm@66488  4 eberlm@66488  5  A filter describing the points x such that f(x) tends to some other filter.  eberlm@66488  6 *)  wenzelm@67409  7 wenzelm@67409  8 section \The \going_to\ filter\  wenzelm@67409  9 eberlm@66488  10 theory Going_To_Filter  eberlm@66488  11  imports Complex_Main  eberlm@66488  12 begin  eberlm@66488  13 eberlm@66488  14 definition going_to_within :: "('a \ 'b) \ 'b filter \ 'a set \ 'a filter"  eberlm@66488  15  ("(_)/ going'_to (_)/ within (_)" [1000,60,60] 60) where  eberlm@66488  16  "f going_to F within A = inf (filtercomap f F) (principal A)"  eberlm@66488  17 eberlm@66488  18 abbreviation going_to :: "('a \ 'b) \ 'b filter \ 'a filter"  eberlm@66488  19  (infix "going'_to" 60)  eberlm@66488  20  where "f going_to F \ f going_to F within UNIV"  eberlm@66488  21 eberlm@66488  22 text \  wenzelm@67409  23  The \going_to\ filter is, in a sense, the opposite of @{term filtermap}.  eberlm@66488  24  It corresponds to the intuition of, given a function $f: A \to B$ and a filter $F$ on the  eberlm@66488  25  range of $B$, looking at such values of $x$ that $f(x)$ approaches $F$. This can be  eberlm@66488  26  written as @{term "f going_to F"}.  eberlm@66488  27   eberlm@66488  28  A classic example is the @{term "at_infinity"} filter, which describes the neigbourhood  eberlm@66488  29  of infinity (i.\,e.\ all values sufficiently far away from the zero). This can also be written  eberlm@66488  30  as @{term "norm going_to at_top"}.  eberlm@66488  31 wenzelm@67409  32  Additionally, the \going_to\ filter can be restricted with an optional within' parameter.  eberlm@66488  33  For instance, if one would would want to consider the filter of complex numbers near infinity  eberlm@66488  34  that do not lie on the negative real line, one could write  eberlm@66488  35  @{term "norm going_to at_top within - complex_of_real  {..0}"}.  eberlm@66488  36 eberlm@66488  37  A third, less mathematical example lies in the complexity analysis of algorithms.  eberlm@66488  38  Suppose we wanted to say that an algorithm on lists takes $O(n^2)$ time where $n$ is  eberlm@66488  39  the length of the input list. We can write this using the Landau symbols from the AFP,  eberlm@66488  40  where the underlying filter is @{term "length going_to at_top"}. If, on the other hand,  eberlm@66488  41  we want to look the complexity of the algorithm on sorted lists, we could use the filter  eberlm@66488  42  @{term "length going_to at_top within {xs. sorted xs}"}.  eberlm@66488  43 \  eberlm@66488  44 eberlm@66488  45 lemma going_to_def: "f going_to F = filtercomap f F"  eberlm@66488  46  by (simp add: going_to_within_def)  eberlm@66488  47 eberlm@66488  48 lemma eventually_going_toI [intro]:  eberlm@66488  49  assumes "eventually P F"  eberlm@66488  50  shows "eventually (\x. P (f x)) (f going_to F)"  eberlm@66488  51  using assms by (auto simp: going_to_def)  eberlm@66488  52 eberlm@66488  53 lemma filterlim_going_toI_weak [intro]: "filterlim f F (f going_to F within A)"  eberlm@66488  54  unfolding going_to_within_def  eberlm@66488  55  by (meson filterlim_filtercomap filterlim_iff inf_le1 le_filter_def)  eberlm@66488  56 eberlm@66488  57 lemma going_to_mono: "F \ G \ A \ B \ f going_to F within A \ f going_to G within B"  eberlm@66488  58  unfolding going_to_within_def by (intro inf_mono filtercomap_mono) simp_all  eberlm@66488  59 eberlm@66488  60 lemma going_to_inf:  eberlm@66488  61  "f going_to (inf F G) within A = inf (f going_to F within A) (f going_to G within A)"  eberlm@66488  62  by (simp add: going_to_within_def filtercomap_inf inf_assoc inf_commute inf_left_commute)  eberlm@66488  63 eberlm@66488  64 lemma going_to_sup:  eberlm@66488  65  "f going_to (sup F G) within A \ sup (f going_to F within A) (f going_to G within A)"  eberlm@66488  66  by (auto simp: going_to_within_def intro!: inf.coboundedI1 filtercomap_sup filtercomap_mono)  eberlm@66488  67 eberlm@66488  68 lemma going_to_top [simp]: "f going_to top within A = principal A"  eberlm@66488  69  by (simp add: going_to_within_def)  eberlm@66488  70   eberlm@66488  71 lemma going_to_bot [simp]: "f going_to bot within A = bot"  eberlm@66488  72  by (simp add: going_to_within_def)  eberlm@66488  73   eberlm@66488  74 lemma going_to_principal:  eberlm@66488  75  "f going_to principal A within B = principal (f - A \ B)"  eberlm@66488  76  by (simp add: going_to_within_def)  eberlm@66488  77   eberlm@66488  78 lemma going_to_within_empty [simp]: "f going_to F within {} = bot"  eberlm@66488  79  by (simp add: going_to_within_def)  eberlm@66488  80 eberlm@66488  81 lemma going_to_within_union [simp]:  eberlm@66488  82  "f going_to F within (A \ B) = sup (f going_to F within A) (f going_to F within B)"  eberlm@66488  83  by (simp add: going_to_within_def inf_sup_distrib1 [symmetric])  eberlm@66488  84 eberlm@66488  85 lemma eventually_going_to_at_top_linorder:  eberlm@66488  86  fixes f :: "'a \ 'b :: linorder"  eberlm@66488  87  shows "eventually P (f going_to at_top within A) \ (\C. \x\A. f x \ C \ P x)"  eberlm@66488  88  unfolding going_to_within_def eventually_filtercomap  eberlm@66488  89  eventually_inf_principal eventually_at_top_linorder by fast  eberlm@66488  90 eberlm@66488  91 lemma eventually_going_to_at_bot_linorder:  eberlm@66488  92  fixes f :: "'a \ 'b :: linorder"  eberlm@66488  93  shows "eventually P (f going_to at_bot within A) \ (\C. \x\A. f x \ C \ P x)"  eberlm@66488  94  unfolding going_to_within_def eventually_filtercomap  eberlm@66488  95  eventually_inf_principal eventually_at_bot_linorder by fast  eberlm@66488  96 eberlm@66488  97 lemma eventually_going_to_at_top_dense:  eberlm@66488  98  fixes f :: "'a \ 'b :: {linorder,no_top}"  eberlm@66488  99  shows "eventually P (f going_to at_top within A) \ (\C. \x\A. f x > C \ P x)"  eberlm@66488  100  unfolding going_to_within_def eventually_filtercomap  eberlm@66488  101  eventually_inf_principal eventually_at_top_dense by fast  eberlm@66488  102 eberlm@66488  103 lemma eventually_going_to_at_bot_dense:  eberlm@66488  104  fixes f :: "'a \ 'b :: {linorder,no_bot}"  eberlm@66488  105  shows "eventually P (f going_to at_bot within A) \ (\C. \x\A. f x < C \ P x)"  eberlm@66488  106  unfolding going_to_within_def eventually_filtercomap  eberlm@66488  107  eventually_inf_principal eventually_at_bot_dense by fast  eberlm@66488  108   eberlm@66488  109 lemma eventually_going_to_nhds:  eberlm@66488  110  "eventually P (f going_to nhds a within A) \  eberlm@66488  111  (\S. open S \ a \ S \ (\x\A. f x \ S \ P x))"  eberlm@66488  112  unfolding going_to_within_def eventually_filtercomap eventually_inf_principal  eberlm@66488  113  eventually_nhds by fast  eberlm@66488  114 eberlm@66488  115 lemma eventually_going_to_at:  eberlm@66488  116  "eventually P (f going_to (at a within B) within A) \  eberlm@66488  117  (\S. open S \ a \ S \ (\x\A. f x \ B \ S - {a} \ P x))"  eberlm@66488  118  unfolding at_within_def going_to_inf eventually_inf_principal  eberlm@66488  119  eventually_going_to_nhds going_to_principal by fast  eberlm@66488  120 eberlm@66488  121 lemma norm_going_to_at_top_eq: "norm going_to at_top = at_infinity"  eberlm@66488  122  by (simp add: eventually_at_infinity eventually_going_to_at_top_linorder filter_eq_iff)  eberlm@66488  123 eberlm@66488  124 lemmas at_infinity_altdef = norm_going_to_at_top_eq [symmetric]  eberlm@66488  125 eberlm@66488  126 end `