68630
|
1 |
(*<*)
|
|
2 |
theory Real_Asymp_Doc
|
|
3 |
imports "HOL-Real_Asymp.Real_Asymp"
|
|
4 |
begin
|
|
5 |
|
|
6 |
ML_file \<open>../antiquote_setup.ML\<close>
|
|
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 |
(*>*) |