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