|
1 (*<*) |
|
2 theory Real_Asymp_Doc |
|
3 imports "HOL-Real_Asymp.Real_Asymp" |
|
4 begin |
|
5 |
|
6 ML_file "~~/src/Doc/antiquote_setup.ML" |
|
7 (*>*) |
|
8 |
|
9 section \<open>Introduction\<close> |
|
10 |
|
11 text \<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 |
|
27 section \<open>Supported Operations\<close> |
|
28 |
|
29 text \<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 exp}, @{term ln}, @{term log}, @{term sqrt}, @{term "root k"} (for a constant k) |
|
37 |
|
38 \<^item> @{term sin}, @{term cos}, @{term tan} at finite points |
|
39 |
|
40 \<^item> @{term sinh}, @{term cosh}, @{term tanh} |
|
41 |
|
42 \<^item> @{term min}, @{term max}, @{term abs} |
|
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 sin} and @{term cos} at \<open>\<plusminus>\<infinity>\<close> |
|
50 |
|
51 \<^item> @{term floor}, @{term ceiling}, @{term frac}, and \<open>mod\<close> |
|
52 |
|
53 Additionally, the @{term arctan} function is partially supported. The method may fail when |
|
54 the argument to @{term arctan} contains functions of different order of growth. |
|
55 \<close> |
|
56 |
|
57 |
|
58 section \<open>Proving Limits and Asymptotic Properties\<close> |
|
59 |
|
60 text \<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 |
|
75 text \<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 "real \<Rightarrow> real"} 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 "filterlim f F G"} |
|
87 |
|
88 \<^item> Landau symbols, i.\,e.\ @{prop "f \<in> O[F](g)"} and analogously for \<^emph>\<open>o\<close>, \<open>\<Omega>\<close>, \<open>\<omega>\<close>, \<open>\<Theta>\<close> |
|
89 |
|
90 \<^item> Asymptotic equivalence, i.\,e.\ @{prop "f \<sim>[F] g"} |
|
91 |
|
92 \<^item> Asymptotic inequalities, i.\,e.\ @{prop "eventually (\<lambda>x. f x \<le> g x) F"} |
|
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 |
|
98 lemma \<open>filterlim (\<lambda>x::real. (1 + 1 / x) powr x) (nhds (exp 1)) at_top\<close> |
|
99 by real_asymp |
|
100 |
|
101 text \<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 (*<*) |
|
111 experiment |
|
112 fixes a :: real |
|
113 begin |
|
114 (*>*) |
|
115 lemma \<open>filterlim (\<lambda>x::real. exp (a * x)) at_top at_top\<close> |
|
116 oops |
|
117 |
|
118 text \<open> |
|
119 Here, @{method real_asymp} outputs an error message stating that it could not determine the |
|
120 sign of the free variable @{term "a :: real"}. In this case, the user must add the assumption |
|
121 \<open>a > 0\<close> and give it to @{method real_asymp}. |
|
122 \<close> |
|
123 lemma |
|
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 (*<*) |
|
128 end |
|
129 (*>*) |
|
130 text \<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 "pi - exp 1"}. |
|
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 |
|
152 section \<open>Diagnostic Commands\<close> |
|
153 |
|
154 text \<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 "at_top"}, @{term "at_bot"}, |
|
177 @{term "at_left"}, or @{term "at_right"}. If no limit point is given, @{term "at_top"} 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 "at_right (0::real)"} and @{term "at_left (0::real)"}); |
|
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 "sin x"} 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 at_top} case). |
|
208 \<close> |
|
209 |
|
210 |
|
211 section \<open>Extensibility\<close> |
|
212 |
|
213 subsection \<open>Basic fact collections\<close> |
|
214 |
|
215 text \<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 sinh}, which is equal to @{term "\<lambda>x. (exp x - exp (-x)) / 2"}. |
|
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 |
|
229 subsection \<open>Expanding Custom Operations\<close> |
|
230 |
|
231 text \<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 "(g\<^sub>i expands_to G\<^sub>i) bs"} |
|
240 \<^item> the current basis \<open>bs\<close> |
|
241 and returns a theorem of the form @{prop "(t expands_to F) bs'"} 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 "REAL_ASYMP_CUSTOM f"} (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 "REAL_ASYMP_EVAL_CONSTRUCTOR c"} 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 |
|
266 subsection \<open>Extending the Sign Oracle\<close> |
|
267 |
|
268 text \<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 (*<*) |
|
285 end |
|
286 (*>*) |