1(*<*) 2theory Real_Asymp_Doc 3 imports "HOL-Real_Asymp.Real_Asymp" 4begin 5 6ML_file \<open>~~/src/Doc/antiquote_setup.ML\<close> 7(*>*) 8 9section \<open>Introduction\<close> 10 11text \<open> 12 This document describes the \<^verbatim>\<open>real_asymp\<close> package that provides a number of tools 13 related to the asymptotics of real-valued functions. These tools are: 14 15 \<^item> The @{method real_asymp} method to prove limits, statements involving Landau symbols 16 (`Big-O' etc.), and asymptotic equivalence (\<open>\<sim>\<close>) 17 18 \<^item> The @{command real_limit} command to compute the limit of a real-valued function at a 19 certain point 20 21 \<^item> The @{command real_expansion} command to compute the asymptotic expansion of a 22 real-valued function at a certain point 23 24 These three tools will be described in the following sections. 25\<close> 26 27section \<open>Supported Operations\<close> 28 29text \<open> 30 The \<^verbatim>\<open>real_asymp\<close> package fully supports the following operations: 31 32 \<^item> Basic arithmetic (addition, subtraction, multiplication, division) 33 34 \<^item> Powers with constant natural exponent 35 36 \<^item> \<^term>\<open>exp\<close>, \<^term>\<open>ln\<close>, \<^term>\<open>log\<close>, \<^term>\<open>sqrt\<close>, \<^term>\<open>root k\<close> (for a constant k) 37 38 \<^item> \<^term>\<open>sin\<close>, \<^term>\<open>cos\<close>, \<^term>\<open>tan\<close> at finite points 39 40 \<^item> \<^term>\<open>sinh\<close>, \<^term>\<open>cosh\<close>, \<^term>\<open>tanh\<close> 41 42 \<^item> \<^term>\<open>min\<close>, \<^term>\<open>max\<close>, \<^term>\<open>abs\<close> 43 44 Additionally, the following operations are supported in a `best effort' fashion using asymptotic 45 upper/lower bounds: 46 47 \<^item> Powers with variable natural exponent 48 49 \<^item> \<^term>\<open>sin\<close> and \<^term>\<open>cos\<close> at \<open>\<plusminus>\<infinity>\<close> 50 51 \<^item> \<^term>\<open>floor\<close>, \<^term>\<open>ceiling\<close>, \<^term>\<open>frac\<close>, and \<open>mod\<close> 52 53 Additionally, the \<^term>\<open>arctan\<close> function is partially supported. The method may fail when 54 the argument to \<^term>\<open>arctan\<close> contains functions of different order of growth. 55\<close> 56 57 58section \<open>Proving Limits and Asymptotic Properties\<close> 59 60text \<open> 61 \[ 62 @{method_def (HOL) real_asymp} : \<open>method\<close> 63 \] 64 65 \<^rail>\<open> 66 @@{method (HOL) real_asymp} opt? (@{syntax simpmod} * ) 67 ; 68 opt: '(' ('verbose' | 'fallback' ) ')' 69 ; 70 @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | '!' | 'del') | 71 'cong' (() | 'add' | 'del')) ':' @{syntax thms} 72 \<close> 73\<close> 74 75text \<open> 76 The @{method real_asymp} method is a semi-automatic proof method for proving certain statements 77 related to the asymptotic behaviour of real-valued functions. In the following, let \<open>f\<close> and \<open>g\<close> 78 be functions of type \<^typ>\<open>real \<Rightarrow> real\<close> and \<open>F\<close> and \<open>G\<close> real filters. 79 80 The functions \<open>f\<close> and \<open>g\<close> can be built from the operations mentioned before and may contain free 81 variables. The filters \<open>F\<close> and \<open>G\<close> can be either \<open>\<plusminus>\<infinity>\<close> or a finite point in \<open>\<real>\<close>, possibly 82 with approach from the left or from the right. 83 84 The class of statements that is supported by @{method real_asymp} then consists of: 85 86 \<^item> Limits, i.\,e.\ \<^prop>\<open>filterlim f F G\<close> 87 88 \<^item> Landau symbols, i.\,e.\ \<^prop>\<open>f \<in> O[F](g)\<close> and analogously for \<^emph>\<open>o\<close>, \<open>\<Omega>\<close>, \<open>\<omega>\<close>, \<open>\<Theta>\<close> 89 90 \<^item> Asymptotic equivalence, i.\,e.\ \<^prop>\<open>f \<sim>[F] g\<close> 91 92 \<^item> Asymptotic inequalities, i.\,e.\ \<^prop>\<open>eventually (\<lambda>x. f x \<le> g x) F\<close> 93 94 For typical problems arising in practice that do not contain free variables, @{method real_asymp} 95 tends to succeed fully automatically within fractions of seconds, e.\,g.: 96\<close> 97 98lemma \<open>filterlim (\<lambda>x::real. (1 + 1 / x) powr x) (nhds (exp 1)) at_top\<close> 99 by real_asymp 100 101text \<open> 102 What makes the method \<^emph>\<open>semi-automatic\<close> is the fact that it has to internally determine the 103 sign of real-valued constants and identical zeroness of real-valued functions, and while the 104 internal heuristics for this work very well most of the time, there are situations where the 105 method fails to determine the sign of a constant, in which case the user needs to go back and 106 supply more information about the sign of that constant in order to get a result. 107 108 A simple example is the following: 109\<close> 110(*<*) 111experiment 112 fixes a :: real 113begin 114(*>*) 115lemma \<open>filterlim (\<lambda>x::real. exp (a * x)) at_top at_top\<close> 116oops 117 118text \<open> 119 Here, @{method real_asymp} outputs an error message stating that it could not determine the 120 sign of the free variable \<^term>\<open>a :: real\<close>. In this case, the user must add the assumption 121 \<open>a > 0\<close> and give it to @{method real_asymp}. 122\<close> 123lemma 124 assumes \<open>a > 0\<close> 125 shows \<open>filterlim (\<lambda>x::real. exp (a * x)) at_top at_top\<close> 126 using assms by real_asymp 127(*<*) 128end 129(*>*) 130text \<open> 131 Additional modifications to the simpset that is used for determining signs can also be made 132 with \<open>simp add:\<close> modifiers etc.\ in the same way as when using the @{method simp} method directly. 133 134 The same situation can also occur without free variables if the constant in question is a 135 complicated expression that the simplifier does not know enough ebout, 136 e.\,g.\ \<^term>\<open>pi - exp 1\<close>. 137 138 In order to trace problems with sign determination, the \<open>(verbose)\<close> option can be passed to 139 @{method real_asymp}. It will then print a detailed error message whenever it encounters 140 a sign determination problem that it cannot solve. 141 142 The \<open>(fallback)\<close> flag causes the method not to use asymptotic interval arithmetic, but only 143 the much simpler core mechanism of computing a single Multiseries expansion for the input 144 function. There should normally be no need to use this flag; however, the core part of the 145 code has been tested much more rigorously than the asymptotic interval part. In case there 146 is some implementation problem with it for a problem that can be solved without it, the 147 \<open>(fallback)\<close> option can be used until that problem is resolved. 148\<close> 149 150 151 152section \<open>Diagnostic Commands\<close> 153 154text \<open> 155 \[\begin{array}{rcl} 156 @{command_def (HOL) real_limit} & : & \<open>context \<rightarrow>\<close> \\ 157 @{command_def (HOL) real_expansion} & : & \<open>context \<rightarrow>\<close> 158 \end{array}\] 159 160 \<^rail>\<open> 161 @@{command (HOL) real_limit} (limitopt*) 162 ; 163 @@{command (HOL) real_expansion} (expansionopt*) 164 ; 165 limitopt : ('limit' ':' @{syntax term}) | ('facts' ':' @{syntax thms}) 166 ; 167 expansionopt : 168 ('limit' ':' @{syntax term}) | 169 ('terms' ':' @{syntax nat} ('(' 'strict' ')') ?) | 170 ('facts' ':' @{syntax thms}) 171 \<close> 172 173 \<^descr>@{command real_limit} computes the limit of the given function \<open>f(x)\<close> for as \<open>x\<close> tends 174 to the specified limit point. Additional facts can be provided with the \<open>facts\<close> option, 175 similarly to the @{command using} command with @{method real_asymp}. The limit point given 176 by the \<open>limit\<close> option must be one of the filters \<^term>\<open>at_top\<close>, \<^term>\<open>at_bot\<close>, 177 \<^term>\<open>at_left\<close>, or \<^term>\<open>at_right\<close>. If no limit point is given, \<^term>\<open>at_top\<close> is used 178 by default. 179 180 \<^medskip> 181 The output of @{command real_limit} can be \<open>\<infinity>\<close>, \<open>-\<infinity>\<close>, \<open>\<plusminus>\<infinity>\<close>, \<open>c\<close> (for some real constant \<open>c\<close>), 182 \<open>0\<^sup>+\<close>, or \<open>0\<^sup>-\<close>. The \<open>+\<close> and \<open>-\<close> in the last case indicate whether the approach is from above 183 or from below (corresponding to \<^term>\<open>at_right (0::real)\<close> and \<^term>\<open>at_left (0::real)\<close>); 184 for technical reasons, this information is currently not displayed if the limit is not 0. 185 186 \<^medskip> 187 If the given function does not tend to a definite limit (e.\,g.\ \<^term>\<open>sin x\<close> for \<open>x \<rightarrow> \<infinity>\<close>), 188 the command might nevertheless succeed to compute an asymptotic upper and/or lower bound and 189 display the limits of these bounds instead. 190 191 \<^descr>@{command real_expansion} works similarly to @{command real_limit}, but displays the first few 192 terms of the asymptotic multiseries expansion of the given function at the given limit point 193 and the order of growth of the remainder term. 194 195 In addition to the options already explained for the @{command real_limit} command, it takes 196 an additional option \<open>terms\<close> that controls how many of the leading terms of the expansion are 197 printed. If the \<open>(strict)\<close> modifier is passed to the \<open>terms option\<close>, terms whose coefficient is 198 0 are dropped from the output and do not count to the number of terms to be output. 199 200 \<^medskip> 201 By default, the first three terms are output and the \<open>strict\<close> option is disabled. 202 203 Note that these two commands are intended for diagnostic use only. While the central part 204 of their implementation -- finding a multiseries expansion and reading off the limit -- are the 205 same as in the @{method real_asymp} method and therefore trustworthy, there is a small amount 206 of unverified code involved in pre-processing and printing (e.\,g.\ for reducing all the 207 different options for the \<open>limit\<close> option to the \<^term>\<open>at_top\<close> case). 208\<close> 209 210 211section \<open>Extensibility\<close> 212 213subsection \<open>Basic fact collections\<close> 214 215text \<open> 216 The easiest way to add support for additional operations is to add corresponding facts 217 to one of the following fact collections. However, this only works for particularly simple cases. 218 219 \<^descr>@{thm [source] real_asymp_reify_simps} specifies a list of (unconditional) equations that are 220 unfolded as a first step of @{method real_asymp} and the related commands. This can be used to 221 add support for operations that can be represented easily by other operations that are already 222 supported, such as \<^term>\<open>sinh\<close>, which is equal to \<^term>\<open>\<lambda>x. (exp x - exp (-x)) / 2\<close>. 223 224 \<^descr>@{thm [source] real_asymp_nat_reify} and @{thm [source] real_asymp_int_reify} is used to 225 convert operations on natural numbers or integers to operations on real numbers. This enables 226 @{method real_asymp} to also work on functions that return a natural number or an integer. 227\<close> 228 229subsection \<open>Expanding Custom Operations\<close> 230 231text \<open> 232 Support for some non-trivial new operation \<open>f(x\<^sub>1, \<dots>, x\<^sub>n)\<close> can be added dynamically at any 233 time, but it involves writing ML code and involves a significant amount of effort, especially 234 when the function has essential singularities. 235 236 The first step is to write an ML function that takes as arguments 237 \<^item> the expansion context 238 \<^item> the term \<open>t\<close> to expand (which will be of the form \<open>f(g\<^sub>1(x), \<dots>, g\<^sub>n(x))\<close>) 239 \<^item> a list of \<open>n\<close> theorems of the form \<^prop>\<open>(g\<^sub>i expands_to G\<^sub>i) bs\<close> 240 \<^item> the current basis \<open>bs\<close> 241 and returns a theorem of the form \<^prop>\<open>(t expands_to F) bs'\<close> and a new basis \<open>bs'\<close> which 242 must be a superset of the original basis. 243 244 This function must then be registered as a handler for the operation by proving a vacuous lemma 245 of the form \<^prop>\<open>REAL_ASYMP_CUSTOM f\<close> (which is only used for tagging) and passing that 246 lemma and the expansion function to @{ML [source] Exp_Log_Expression.register_custom_from_thm} 247 in a @{command local_setup} invocation. 248 249 If the expansion produced by the handler function contains new definitions, corresponding 250 evaluation equations must be added to the fact collection @{thm [source] real_asymp_eval_eqs}. 251 These equations must have the form \<open>h p\<^sub>1 \<dots> p\<^sub>m = rhs\<close> where \<open>h\<close> must be a constant of arity \<open>m\<close> 252 (i.\,e.\ the function on the left-hand side must be fully applied) and the \<open>p\<^sub>i\<close> can be patterns 253 involving \<open>constructors\<close>. 254 255 New constructors for this pattern matching can be registered by adding a theorem of the form 256 \<^prop>\<open>REAL_ASYMP_EVAL_CONSTRUCTOR c\<close> to the fact collection 257 @{thm [source] exp_log_eval_constructor}, but this should be quite rare in practice. 258 259 \<^medskip> 260 Note that there is currently no way to add support for custom operations in connection with 261 `oscillating' terms. The above mechanism only works if all arguments of the new operation have 262 an exact multiseries expansion. 263\<close> 264 265 266subsection \<open>Extending the Sign Oracle\<close> 267 268text \<open> 269 By default, the \<^verbatim>\<open>real_asymp\<close> package uses the simplifier with the given simpset and facts 270 in order to determine the sign of real constants. This is done by invoking the simplifier 271 on goals like \<open>c = 0\<close>, \<open>c \<noteq> 0\<close>, \<open>c > 0\<close>, or \<open>c < 0\<close> or some subset thereof, depending on the 272 context. 273 274 If the simplifier cannot prove any of them, the entire method (or command) invocation will fail. 275 It is, however, possible to dynamically add additional sign oracles that will be tried; the 276 most obvious candidate for an oracle that one may want to add or remove dynamically are 277 approximation-based tactics. 278 279 Adding such a tactic can be done by calling 280 @{ML [source] Multiseries_Expansion.register_sign_oracle}. Note that if the tactic cannot prove 281 a goal, it should fail as fast as possible. 282\<close> 283 284(*<*) 285end 286(*>*) 287