(*<*) theory Real_Asymp_Doc imports "HOL-Real_Asymp.Real_Asymp" begin ML_file ‹~~/src/Doc/antiquote_setup.ML› (*>*) section ‹Introduction› text ‹ This document describes the ▩‹real_asymp› package that provides a number of tools related to the asymptotics of real-valued functions. These tools are: ▪ The @{method real_asymp} method to prove limits, statements involving Landau symbols (`Big-O' etc.), and asymptotic equivalence (‹∼›) ▪ The @{command real_limit} command to compute the limit of a real-valued function at a certain point ▪ The @{command real_expansion} command to compute the asymptotic expansion of a real-valued function at a certain point These three tools will be described in the following sections. › section ‹Supported Operations› text ‹ The ▩‹real_asymp› package fully supports the following operations: ▪ Basic arithmetic (addition, subtraction, multiplication, division) ▪ Powers with constant natural exponent ▪ \<^term>‹exp›, \<^term>‹ln›, \<^term>‹log›, \<^term>‹sqrt›, \<^term>‹root k› (for a constant k) ▪ \<^term>‹sin›, \<^term>‹cos›, \<^term>‹tan› at finite points ▪ \<^term>‹sinh›, \<^term>‹cosh›, \<^term>‹tanh› ▪ \<^term>‹min›, \<^term>‹max›, \<^term>‹abs› Additionally, the following operations are supported in a `best effort' fashion using asymptotic upper/lower bounds: ▪ Powers with variable natural exponent ▪ \<^term>‹sin› and \<^term>‹cos› at ‹±∞› ▪ \<^term>‹floor›, \<^term>‹ceiling›, \<^term>‹frac›, and ‹mod› Additionally, the \<^term>‹arctan› function is partially supported. The method may fail when the argument to \<^term>‹arctan› contains functions of different order of growth. › section ‹Proving Limits and Asymptotic Properties› text ‹ \[ @{method_def (HOL) real_asymp} : ‹method› \] \<^rail>‹ @@{method (HOL) real_asymp} opt? (@{syntax simpmod} * ) ; opt: '(' ('verbose' | 'fallback' ) ')' ; @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | '!' | 'del') | 'cong' (() | 'add' | 'del')) ':' @{syntax thms} › › text ‹ The @{method real_asymp} method is a semi-automatic proof method for proving certain statements related to the asymptotic behaviour of real-valued functions. In the following, let ‹f› and ‹g› be functions of type \<^typ>‹real ⇒ real› and ‹F› and ‹G› real filters. The functions ‹f› and ‹g› can be built from the operations mentioned before and may contain free variables. The filters ‹F› and ‹G› can be either ‹±∞› or a finite point in ‹ℝ›, possibly with approach from the left or from the right. The class of statements that is supported by @{method real_asymp} then consists of: ▪ Limits, i.\,e.\ \<^prop>‹filterlim f F G› ▪ Landau symbols, i.\,e.\ \<^prop>‹f ∈ O[F](g)› and analogously for ∗‹o›, ‹Ω›, ‹ω›, ‹Θ› ▪ Asymptotic equivalence, i.\,e.\ \<^prop>‹f ∼[F] g› ▪ Asymptotic inequalities, i.\,e.\ \<^prop>‹eventually (λx. f x ≤ g x) F› For typical problems arising in practice that do not contain free variables, @{method real_asymp} tends to succeed fully automatically within fractions of seconds, e.\,g.: › lemma ‹filterlim (λx::real. (1 + 1 / x) powr x) (nhds (exp 1)) at_top› by real_asymp text ‹ What makes the method ∗‹semi-automatic› is the fact that it has to internally determine the sign of real-valued constants and identical zeroness of real-valued functions, and while the internal heuristics for this work very well most of the time, there are situations where the method fails to determine the sign of a constant, in which case the user needs to go back and supply more information about the sign of that constant in order to get a result. A simple example is the following: › (*<*) experiment fixes a :: real begin (*>*) lemma ‹filterlim (λx::real. exp (a * x)) at_top at_top› oops text ‹ Here, @{method real_asymp} outputs an error message stating that it could not determine the sign of the free variable \<^term>‹a :: real›. In this case, the user must add the assumption ‹a > 0› and give it to @{method real_asymp}. › lemma assumes ‹a > 0› shows ‹filterlim (λx::real. exp (a * x)) at_top at_top› using assms by real_asymp (*<*) end (*>*) text ‹ Additional modifications to the simpset that is used for determining signs can also be made with ‹simp add:› modifiers etc.\ in the same way as when using the @{method simp} method directly. The same situation can also occur without free variables if the constant in question is a complicated expression that the simplifier does not know enough ebout, e.\,g.\ \<^term>‹pi - exp 1›. In order to trace problems with sign determination, the ‹(verbose)› option can be passed to @{method real_asymp}. It will then print a detailed error message whenever it encounters a sign determination problem that it cannot solve. The ‹(fallback)› flag causes the method not to use asymptotic interval arithmetic, but only the much simpler core mechanism of computing a single Multiseries expansion for the input function. There should normally be no need to use this flag; however, the core part of the code has been tested much more rigorously than the asymptotic interval part. In case there is some implementation problem with it for a problem that can be solved without it, the ‹(fallback)› option can be used until that problem is resolved. › section ‹Diagnostic Commands› text ‹ \[\begin{array}{rcl} @{command_def (HOL) real_limit} & : & ‹context →› \\ @{command_def (HOL) real_expansion} & : & ‹context →› \end{array}\] \<^rail>‹ @@{command (HOL) real_limit} (limitopt*) ; @@{command (HOL) real_expansion} (expansionopt*) ; limitopt : ('limit' ':' @{syntax term}) | ('facts' ':' @{syntax thms}) ; expansionopt : ('limit' ':' @{syntax term}) | ('terms' ':' @{syntax nat} ('(' 'strict' ')') ?) | ('facts' ':' @{syntax thms}) › ➧@{command real_limit} computes the limit of the given function ‹f(x)› for as ‹x› tends to the specified limit point. Additional facts can be provided with the ‹facts› option, similarly to the @{command using} command with @{method real_asymp}. The limit point given by the ‹limit› option must be one of the filters \<^term>‹at_top›, \<^term>‹at_bot›, \<^term>‹at_left›, or \<^term>‹at_right›. If no limit point is given, \<^term>‹at_top› is used by default. ┉ The output of @{command real_limit} can be ‹∞›, ‹-∞›, ‹±∞›, ‹c› (for some real constant ‹c›), ‹0⇧^{+}›, or ‹0⇧^{-}›. The ‹+› and ‹-› in the last case indicate whether the approach is from above or from below (corresponding to \<^term>‹at_right (0::real)› and \<^term>‹at_left (0::real)›); for technical reasons, this information is currently not displayed if the limit is not 0. ┉ If the given function does not tend to a definite limit (e.\,g.\ \<^term>‹sin x› for ‹x → ∞›), the command might nevertheless succeed to compute an asymptotic upper and/or lower bound and display the limits of these bounds instead. ➧@{command real_expansion} works similarly to @{command real_limit}, but displays the first few terms of the asymptotic multiseries expansion of the given function at the given limit point and the order of growth of the remainder term. In addition to the options already explained for the @{command real_limit} command, it takes an additional option ‹terms› that controls how many of the leading terms of the expansion are printed. If the ‹(strict)› modifier is passed to the ‹terms option›, terms whose coefficient is 0 are dropped from the output and do not count to the number of terms to be output. ┉ By default, the first three terms are output and the ‹strict› option is disabled. Note that these two commands are intended for diagnostic use only. While the central part of their implementation -- finding a multiseries expansion and reading off the limit -- are the same as in the @{method real_asymp} method and therefore trustworthy, there is a small amount of unverified code involved in pre-processing and printing (e.\,g.\ for reducing all the different options for the ‹limit› option to the \<^term>‹at_top› case). › section ‹Extensibility› subsection ‹Basic fact collections› text ‹ The easiest way to add support for additional operations is to add corresponding facts to one of the following fact collections. However, this only works for particularly simple cases. ➧@{thm [source] real_asymp_reify_simps} specifies a list of (unconditional) equations that are unfolded as a first step of @{method real_asymp} and the related commands. This can be used to add support for operations that can be represented easily by other operations that are already supported, such as \<^term>‹sinh›, which is equal to \<^term>‹λx. (exp x - exp (-x)) / 2›. ➧@{thm [source] real_asymp_nat_reify} and @{thm [source] real_asymp_int_reify} is used to convert operations on natural numbers or integers to operations on real numbers. This enables @{method real_asymp} to also work on functions that return a natural number or an integer. › subsection ‹Expanding Custom Operations› text ‹ Support for some non-trivial new operation ‹f(x⇩_{1}, …, x⇩_{n})› can be added dynamically at any time, but it involves writing ML code and involves a significant amount of effort, especially when the function has essential singularities. The first step is to write an ML function that takes as arguments ▪ the expansion context ▪ the term ‹t› to expand (which will be of the form ‹f(g⇩_{1}(x), …, g⇩_{n}(x))›) ▪ a list of ‹n› theorems of the form \<^prop>‹(g⇩_{i}expands_to G⇩_{i}) bs› ▪ the current basis ‹bs› and returns a theorem of the form \<^prop>‹(t expands_to F) bs'› and a new basis ‹bs'› which must be a superset of the original basis. This function must then be registered as a handler for the operation by proving a vacuous lemma of the form \<^prop>‹REAL_ASYMP_CUSTOM f› (which is only used for tagging) and passing that lemma and the expansion function to @{ML [source] Exp_Log_Expression.register_custom_from_thm} in a @{command local_setup} invocation. If the expansion produced by the handler function contains new definitions, corresponding evaluation equations must be added to the fact collection @{thm [source] real_asymp_eval_eqs}. These equations must have the form ‹h p⇩_{1}… p⇩_{m}= rhs› where ‹h› must be a constant of arity ‹m› (i.\,e.\ the function on the left-hand side must be fully applied) and the ‹p⇩_{i}› can be patterns involving ‹constructors›. New constructors for this pattern matching can be registered by adding a theorem of the form \<^prop>‹REAL_ASYMP_EVAL_CONSTRUCTOR c› to the fact collection @{thm [source] exp_log_eval_constructor}, but this should be quite rare in practice. ┉ Note that there is currently no way to add support for custom operations in connection with `oscillating' terms. The above mechanism only works if all arguments of the new operation have an exact multiseries expansion. › subsection ‹Extending the Sign Oracle› text ‹ By default, the ▩‹real_asymp› package uses the simplifier with the given simpset and facts in order to determine the sign of real constants. This is done by invoking the simplifier on goals like ‹c = 0›, ‹c ≠ 0›, ‹c > 0›, or ‹c < 0› or some subset thereof, depending on the context. If the simplifier cannot prove any of them, the entire method (or command) invocation will fail. It is, however, possible to dynamically add additional sign oracles that will be tried; the most obvious candidate for an oracle that one may want to add or remove dynamically are approximation-based tactics. Adding such a tactic can be done by calling @{ML [source] Multiseries_Expansion.register_sign_oracle}. Note that if the tactic cannot prove a goal, it should fail as fast as possible. › (*<*) end (*>*)