HOL-Library: going_to filter
authorManuel Eberl <eberlm@in.tum.de>
Wed Aug 23 01:05:39 2017 +0200 (21 months ago)
changeset 664889d83e8fe3de3
parent 66486 ffaaa83543b2
child 66489 495df6232517
HOL-Library: going_to filter
NEWS
src/HOL/Library/Going_To_Filter.thy
src/HOL/Library/Library.thy
     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