author | eberlm <eberlm@in.tum.de> |

Sun Jul 22 19:29:51 2018 +0200 (12 months ago) | |

changeset 68677 | 99b1cf1e2d48 |

parent 68676 | 74cb08ff2e66 |

child 68679 | 2a20b315a44d |

Moved Real_Asymp manual

src/Doc/ROOT | file | annotate | diff | revisions | |

src/Doc/Real_Asymp/Real_Asymp_Doc.thy | file | annotate | diff | revisions | |

src/Doc/Real_Asymp/document/root.tex | file | annotate | diff | revisions | |

src/Doc/Real_Asymp/document/style.sty | file | annotate | diff | revisions | |

src/HOL/ROOT | file | annotate | diff | revisions | |

src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy | file | annotate | diff | revisions | |

src/HOL/Real_Asymp/Manual/document/root.tex | file | annotate | diff | revisions | |

src/HOL/Real_Asymp/Manual/document/style.sty | file | annotate | diff | revisions |

1.1 --- a/src/Doc/ROOT Sun Jul 22 14:15:04 2018 +0200 1.2 +++ b/src/Doc/ROOT Sun Jul 22 19:29:51 2018 +0200 1.3 @@ -359,20 +359,6 @@ 1.4 "root.tex" 1.5 "svmono.cls" 1.6 1.7 -session Real_Asymp (doc) in "Real_Asymp" = "HOL-Real_Asymp" + 1.8 - theories 1.9 - Real_Asymp_Doc 1.10 - document_files (in "..") 1.11 - "prepare_document" 1.12 - "pdfsetup.sty" 1.13 - "iman.sty" 1.14 - "extra.sty" 1.15 - "isar.sty" 1.16 - "manual.bib" 1.17 - document_files 1.18 - "root.tex" 1.19 - "style.sty" 1.20 - 1.21 session Sledgehammer (doc) in "Sledgehammer" = Pure + 1.22 options [document_variants = "sledgehammer"] 1.23 document_files (in "..")

2.1 --- a/src/Doc/Real_Asymp/Real_Asymp_Doc.thy Sun Jul 22 14:15:04 2018 +0200 2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 2.3 @@ -1,286 +0,0 @@ 2.4 -(*<*) 2.5 -theory Real_Asymp_Doc 2.6 - imports "HOL-Real_Asymp.Real_Asymp" 2.7 -begin 2.8 - 2.9 -ML_file \<open>../antiquote_setup.ML\<close> 2.10 -(*>*) 2.11 - 2.12 -section \<open>Introduction\<close> 2.13 - 2.14 -text \<open> 2.15 - This document describes the \<^verbatim>\<open>real_asymp\<close> package that provides a number of tools 2.16 - related to the asymptotics of real-valued functions. These tools are: 2.17 - 2.18 - \<^item> The @{method real_asymp} method to prove limits, statements involving Landau symbols 2.19 - (`Big-O' etc.), and asymptotic equivalence (\<open>\<sim>\<close>) 2.20 - 2.21 - \<^item> The @{command real_limit} command to compute the limit of a real-valued function at a 2.22 - certain point 2.23 - 2.24 - \<^item> The @{command real_expansion} command to compute the asymptotic expansion of a 2.25 - real-valued function at a certain point 2.26 - 2.27 - These three tools will be described in the following sections. 2.28 -\<close> 2.29 - 2.30 -section \<open>Supported Operations\<close> 2.31 - 2.32 -text \<open> 2.33 - The \<^verbatim>\<open>real_asymp\<close> package fully supports the following operations: 2.34 - 2.35 - \<^item> Basic arithmetic (addition, subtraction, multiplication, division) 2.36 - 2.37 - \<^item> Powers with constant natural exponent 2.38 - 2.39 - \<^item> @{term exp}, @{term ln}, @{term log}, @{term sqrt}, @{term "root k"} (for a constant k) 2.40 - 2.41 - \<^item> @{term sin}, @{term cos}, @{term tan} at finite points 2.42 - 2.43 - \<^item> @{term sinh}, @{term cosh}, @{term tanh} 2.44 - 2.45 - \<^item> @{term min}, @{term max}, @{term abs} 2.46 - 2.47 - Additionally, the following operations are supported in a `best effort' fashion using asymptotic 2.48 - upper/lower bounds: 2.49 - 2.50 - \<^item> Powers with variable natural exponent 2.51 - 2.52 - \<^item> @{term sin} and @{term cos} at \<open>\<plusminus>\<infinity>\<close> 2.53 - 2.54 - \<^item> @{term floor}, @{term ceiling}, @{term frac}, and \<open>mod\<close> 2.55 - 2.56 - Additionally, the @{term arctan} function is partially supported. The method may fail when 2.57 - the argument to @{term arctan} contains functions of different order of growth. 2.58 -\<close> 2.59 - 2.60 - 2.61 -section \<open>Proving Limits and Asymptotic Properties\<close> 2.62 - 2.63 -text \<open> 2.64 - \[ 2.65 - @{method_def (HOL) real_asymp} : \<open>method\<close> 2.66 - \] 2.67 - 2.68 - @{rail \<open> 2.69 - @@{method (HOL) real_asymp} opt? (@{syntax simpmod} * ) 2.70 - ; 2.71 - opt: '(' ('verbose' | 'fallback' ) ')' 2.72 - ; 2.73 - @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | '!' | 'del') | 2.74 - 'cong' (() | 'add' | 'del')) ':' @{syntax thms} 2.75 - \<close>} 2.76 -\<close> 2.77 - 2.78 -text \<open> 2.79 - The @{method real_asymp} method is a semi-automatic proof method for proving certain statements 2.80 - related to the asymptotic behaviour of real-valued functions. In the following, let \<open>f\<close> and \<open>g\<close> 2.81 - be functions of type @{typ "real \<Rightarrow> real"} and \<open>F\<close> and \<open>G\<close> real filters. 2.82 - 2.83 - The functions \<open>f\<close> and \<open>g\<close> can be built from the operations mentioned before and may contain free 2.84 - 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 2.85 - with approach from the left or from the right. 2.86 - 2.87 - The class of statements that is supported by @{method real_asymp} then consists of: 2.88 - 2.89 - \<^item> Limits, i.\,e.\ @{prop "filterlim f F G"} 2.90 - 2.91 - \<^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> 2.92 - 2.93 - \<^item> Asymptotic equivalence, i.\,e.\ @{prop "f \<sim>[F] g"} 2.94 - 2.95 - \<^item> Asymptotic inequalities, i.\,e.\ @{prop "eventually (\<lambda>x. f x \<le> g x) F"} 2.96 - 2.97 - For typical problems arising in practice that do not contain free variables, @{method real_asymp} 2.98 - tends to succeed fully automatically within fractions of seconds, e.\,g.: 2.99 -\<close> 2.100 - 2.101 -lemma \<open>filterlim (\<lambda>x::real. (1 + 1 / x) powr x) (nhds (exp 1)) at_top\<close> 2.102 - by real_asymp 2.103 - 2.104 -text \<open> 2.105 - What makes the method \<^emph>\<open>semi-automatic\<close> is the fact that it has to internally determine the 2.106 - sign of real-valued constants and identical zeroness of real-valued functions, and while the 2.107 - internal heuristics for this work very well most of the time, there are situations where the 2.108 - method fails to determine the sign of a constant, in which case the user needs to go back and 2.109 - supply more information about the sign of that constant in order to get a result. 2.110 - 2.111 - A simple example is the following: 2.112 -\<close> 2.113 -(*<*) 2.114 -experiment 2.115 - fixes a :: real 2.116 -begin 2.117 -(*>*) 2.118 -lemma \<open>filterlim (\<lambda>x::real. exp (a * x)) at_top at_top\<close> 2.119 -oops 2.120 - 2.121 -text \<open> 2.122 - Here, @{method real_asymp} outputs an error message stating that it could not determine the 2.123 - sign of the free variable @{term "a :: real"}. In this case, the user must add the assumption 2.124 - \<open>a > 0\<close> and give it to @{method real_asymp}. 2.125 -\<close> 2.126 -lemma 2.127 - assumes \<open>a > 0\<close> 2.128 - shows \<open>filterlim (\<lambda>x::real. exp (a * x)) at_top at_top\<close> 2.129 - using assms by real_asymp 2.130 -(*<*) 2.131 -end 2.132 -(*>*) 2.133 -text \<open> 2.134 - Additional modifications to the simpset that is used for determining signs can also be made 2.135 - with \<open>simp add:\<close> modifiers etc.\ in the same way as when using the @{method simp} method directly. 2.136 - 2.137 - The same situation can also occur without free variables if the constant in question is a 2.138 - complicated expression that the simplifier does not know enough ebout, 2.139 - e.\,g.\ @{term "pi - exp 1"}. 2.140 - 2.141 - In order to trace problems with sign determination, the \<open>(verbose)\<close> option can be passed to 2.142 - @{method real_asymp}. It will then print a detailed error message whenever it encounters 2.143 - a sign determination problem that it cannot solve. 2.144 - 2.145 - The \<open>(fallback)\<close> flag causes the method not to use asymptotic interval arithmetic, but only 2.146 - the much simpler core mechanism of computing a single Multiseries expansion for the input 2.147 - function. There should normally be no need to use this flag; however, the core part of the 2.148 - code has been tested much more rigorously than the asymptotic interval part. In case there 2.149 - is some implementation problem with it for a problem that can be solved without it, the 2.150 - \<open>(fallback)\<close> option can be used until that problem is resolved. 2.151 -\<close> 2.152 - 2.153 - 2.154 - 2.155 -section \<open>Diagnostic Commands\<close> 2.156 - 2.157 -text \<open> 2.158 - \[\begin{array}{rcl} 2.159 - @{command_def (HOL) real_limit} & : & \<open>context \<rightarrow>\<close> \\ 2.160 - @{command_def (HOL) real_expansion} & : & \<open>context \<rightarrow>\<close> 2.161 - \end{array}\] 2.162 - 2.163 - @{rail \<open> 2.164 - @@{command (HOL) real_limit} (limitopt*) 2.165 - ; 2.166 - @@{command (HOL) real_expansion} (expansionopt*) 2.167 - ; 2.168 - limitopt : ('limit' ':' @{syntax term}) | ('facts' ':' @{syntax thms}) 2.169 - ; 2.170 - expansionopt : 2.171 - ('limit' ':' @{syntax term}) | 2.172 - ('terms' ':' @{syntax nat} ('(' 'strict' ')') ?) | 2.173 - ('facts' ':' @{syntax thms}) 2.174 - \<close>} 2.175 - 2.176 - \<^descr>@{command real_limit} computes the limit of the given function \<open>f(x)\<close> for as \<open>x\<close> tends 2.177 - to the specified limit point. Additional facts can be provided with the \<open>facts\<close> option, 2.178 - similarly to the @{command using} command with @{method real_asymp}. The limit point given 2.179 - by the \<open>limit\<close> option must be one of the filters @{term "at_top"}, @{term "at_bot"}, 2.180 - @{term "at_left"}, or @{term "at_right"}. If no limit point is given, @{term "at_top"} is used 2.181 - by default. 2.182 - 2.183 - \<^medskip> 2.184 - 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>), 2.185 - \<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 2.186 - or from below (corresponding to @{term "at_right (0::real)"} and @{term "at_left (0::real)"}); 2.187 - for technical reasons, this information is currently not displayed if the limit is not 0. 2.188 - 2.189 - \<^medskip> 2.190 - If the given function does not tend to a definite limit (e.\,g.\ @{term "sin x"} for \<open>x \<rightarrow> \<infinity>\<close>), 2.191 - the command might nevertheless succeed to compute an asymptotic upper and/or lower bound and 2.192 - display the limits of these bounds instead. 2.193 - 2.194 - \<^descr>@{command real_expansion} works similarly to @{command real_limit}, but displays the first few 2.195 - terms of the asymptotic multiseries expansion of the given function at the given limit point 2.196 - and the order of growth of the remainder term. 2.197 - 2.198 - In addition to the options already explained for the @{command real_limit} command, it takes 2.199 - an additional option \<open>terms\<close> that controls how many of the leading terms of the expansion are 2.200 - printed. If the \<open>(strict)\<close> modifier is passed to the \<open>terms option\<close>, terms whose coefficient is 2.201 - 0 are dropped from the output and do not count to the number of terms to be output. 2.202 - 2.203 - \<^medskip> 2.204 - By default, the first three terms are output and the \<open>strict\<close> option is disabled. 2.205 - 2.206 - Note that these two commands are intended for diagnostic use only. While the central part 2.207 - of their implementation – finding a multiseries expansion and reading off the limit – are the 2.208 - same as in the @{method real_asymp} method and therefore trustworthy, there is a small amount 2.209 - of unverified code involved in pre-processing and printing (e.\,g.\ for reducing all the 2.210 - different options for the \<open>limit\<close> option to the @{term at_top} case). 2.211 -\<close> 2.212 - 2.213 - 2.214 -section \<open>Extensibility\<close> 2.215 - 2.216 -subsection \<open>Basic fact collections\<close> 2.217 - 2.218 -text \<open> 2.219 - The easiest way to add support for additional operations is to add corresponding facts 2.220 - to one of the following fact collections. However, this only works for particularly simple cases. 2.221 - 2.222 - \<^descr>@{thm [source] real_asymp_reify_simps} specifies a list of (unconditional) equations that are 2.223 - unfolded as a first step of @{method real_asymp} and the related commands. This can be used to 2.224 - add support for operations that can be represented easily by other operations that are already 2.225 - supported, such as @{term sinh}, which is equal to @{term "\<lambda>x. (exp x - exp (-x)) / 2"}. 2.226 - 2.227 - \<^descr>@{thm [source] real_asymp_nat_reify} and @{thm [source] real_asymp_int_reify} is used to 2.228 - convert operations on natural numbers or integers to operations on real numbers. This enables 2.229 - @{method real_asymp} to also work on functions that return a natural number or an integer. 2.230 -\<close> 2.231 - 2.232 -subsection \<open>Expanding Custom Operations\<close> 2.233 - 2.234 -text \<open> 2.235 - Support for some non-trivial new operation \<open>f(x\<^sub>1, \<dots>, x\<^sub>n)\<close> can be added dynamically at any 2.236 - time, but it involves writing ML code and involves a significant amount of effort, especially 2.237 - when the function has essential singularities. 2.238 - 2.239 - The first step is to write an ML function that takes as arguments 2.240 - \<^item> the expansion context 2.241 - \<^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>) 2.242 - \<^item> a list of \<open>n\<close> theorems of the form @{prop "(g\<^sub>i expands_to G\<^sub>i) bs"} 2.243 - \<^item> the current basis \<open>bs\<close> 2.244 - and returns a theorem of the form @{prop "(t expands_to F) bs'"} and a new basis \<open>bs'\<close> which 2.245 - must be a superset of the original basis. 2.246 - 2.247 - This function must then be registered as a handler for the operation by proving a vacuous lemma 2.248 - of the form @{prop "REAL_ASYMP_CUSTOM f"} (which is only used for tagging) and passing that 2.249 - lemma and the expansion function to @{ML [source] Exp_Log_Expression.register_custom_from_thm} 2.250 - in a @{command local_setup} invocation. 2.251 - 2.252 - If the expansion produced by the handler function contains new definitions, corresponding 2.253 - evaluation equations must be added to the fact collection @{thm [source] real_asymp_eval_eqs}. 2.254 - 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> 2.255 - (i.\,e.\ the function on the left-hand side must be fully applied) and the \<open>p\<^sub>i\<close> can be patterns 2.256 - involving \<open>constructors\<close>. 2.257 - 2.258 - New constructors for this pattern matching can be registered by adding a theorem of the form 2.259 - @{prop "REAL_ASYMP_EVAL_CONSTRUCTOR c"} to the fact collection 2.260 - @{thm [source] exp_log_eval_constructor}, but this should be quite rare in practice. 2.261 - 2.262 - \<^medskip> 2.263 - Note that there is currently no way to add support for custom operations in connection with 2.264 - `oscillating' terms. The above mechanism only works if all arguments of the new operation have 2.265 - an exact multiseries expansion. 2.266 -\<close> 2.267 - 2.268 - 2.269 -subsection \<open>Extending the Sign Oracle\<close> 2.270 - 2.271 -text \<open> 2.272 - By default, the \<^verbatim>\<open>real_asymp\<close> package uses the simplifier with the given simpset and facts 2.273 - in order to determine the sign of real constants. This is done by invoking the simplifier 2.274 - 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 2.275 - context. 2.276 - 2.277 - If the simplifier cannot prove any of them, the entire method (or command) invocation will fail. 2.278 - It is, however, possible to dynamically add additional sign oracles that will be tried; the 2.279 - most obvious candidate for an oracle that one may want to add or remove dynamically are 2.280 - approximation-based tactics. 2.281 - 2.282 - Adding such a tactic can be done by calling 2.283 - @{ML [source] Multiseries_Expansion.register_sign_oracle}. Note that if the tactic cannot prove 2.284 - a goal, it should fail as fast as possible. 2.285 -\<close> 2.286 - 2.287 -(*<*) 2.288 -end 2.289 -(*>*) 2.290 \ No newline at end of file

3.1 --- a/src/Doc/Real_Asymp/document/root.tex Sun Jul 22 14:15:04 2018 +0200 3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 3.3 @@ -1,39 +0,0 @@ 3.4 -\documentclass[11pt,a4paper]{article} 3.5 -\usepackage{amsfonts, amsmath, amssymb} 3.6 -\usepackage{railsetup} 3.7 -\usepackage{iman} 3.8 -\usepackage{extra} 3.9 -\usepackage{isar} 3.10 -\usepackage{isabelle} 3.11 -\usepackage{isabellesym} 3.12 -\usepackage{style} 3.13 - 3.14 -% this should be the last package used 3.15 -\usepackage{pdfsetup} 3.16 - 3.17 -% urls in roman style, theory text in math-similar italics 3.18 -\urlstyle{rm} 3.19 -\isabellestyle{it} 3.20 - 3.21 - 3.22 -\begin{document} 3.23 - 3.24 -\title{\texttt{real\_asymp}: Semi-Automatic Real Asymptotics\\ in Isabelle\slash HOL} 3.25 -\author{Manuel Eberl} 3.26 -\maketitle 3.27 - 3.28 -\tableofcontents 3.29 -\newpage 3.30 -\parindent 0pt\parskip 0.5ex 3.31 - 3.32 -\input{session} 3.33 - 3.34 -\bibliographystyle{abbrv} 3.35 -\bibliography{root} 3.36 - 3.37 -\end{document} 3.38 - 3.39 -%%% Local Variables: 3.40 -%%% mode: latex 3.41 -%%% TeX-master: t 3.42 -%%% End:

4.1 --- a/src/Doc/Real_Asymp/document/style.sty Sun Jul 22 14:15:04 2018 +0200 4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 4.3 @@ -1,46 +0,0 @@ 4.4 - 4.5 -%% toc 4.6 -\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} 4.7 -\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} 4.8 - 4.9 -%% paragraphs 4.10 -\setlength{\parindent}{1em} 4.11 - 4.12 -%% references 4.13 -\newcommand{\secref}[1]{\S\ref{#1}} 4.14 -\newcommand{\figref}[1]{figure~\ref{#1}} 4.15 - 4.16 -%% logical markup 4.17 -\newcommand{\strong}[1]{{\bfseries {#1}}} 4.18 -\newcommand{\qn}[1]{\emph{#1}} 4.19 - 4.20 -%% typographic conventions 4.21 -\newcommand{\qt}[1]{``{#1}''} 4.22 -\newcommand{\ditem}[1]{\item[\isastyletext #1]} 4.23 - 4.24 -%% quote environment 4.25 -\isakeeptag{quote} 4.26 -\renewenvironment{quote} 4.27 - {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax} 4.28 - {\endlist} 4.29 -\renewcommand{\isatagquote}{\begin{quote}} 4.30 -\renewcommand{\endisatagquote}{\end{quote}} 4.31 -\newcommand{\quotebreak}{\\[1.2ex]} 4.32 - 4.33 -%% presentation 4.34 -\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} 4.35 - 4.36 -%% character detail 4.37 -\renewcommand{\isadigit}[1]{\isamath{#1}} 4.38 -\binperiod 4.39 -\underscoreoff 4.40 - 4.41 -%% format 4.42 -\pagestyle{headings} 4.43 -\isabellestyle{it} 4.44 - 4.45 - 4.46 -%%% Local Variables: 4.47 -%%% mode: latex 4.48 -%%% TeX-master: "implementation" 4.49 -%%% End:

5.1 --- a/src/HOL/ROOT Sun Jul 22 14:15:04 2018 +0200 5.2 +++ b/src/HOL/ROOT Sun Jul 22 19:29:51 2018 +0200 5.3 @@ -84,7 +84,18 @@ 5.4 theories 5.5 Real_Asymp 5.6 Real_Asymp_Approx 5.7 - Real_Asymp_Examples 5.8 + Real_Asymp_Examples 5.9 + 5.10 +session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + 5.11 + theories 5.12 + Real_Asymp_Doc 5.13 + document_files (in "~~/src/Doc") 5.14 + "iman.sty" 5.15 + "extra.sty" 5.16 + "isar.sty" 5.17 + document_files 5.18 + "root.tex" 5.19 + "style.sty" 5.20 5.21 session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" + 5.22 description {*

6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 6.2 +++ b/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy Sun Jul 22 19:29:51 2018 +0200 6.3 @@ -0,0 +1,286 @@ 6.4 +(*<*) 6.5 +theory Real_Asymp_Doc 6.6 + imports "HOL-Real_Asymp.Real_Asymp" 6.7 +begin 6.8 + 6.9 +ML_file "~~/src/Doc/antiquote_setup.ML" 6.10 +(*>*) 6.11 + 6.12 +section \<open>Introduction\<close> 6.13 + 6.14 +text \<open> 6.15 + This document describes the \<^verbatim>\<open>real_asymp\<close> package that provides a number of tools 6.16 + related to the asymptotics of real-valued functions. These tools are: 6.17 + 6.18 + \<^item> The @{method real_asymp} method to prove limits, statements involving Landau symbols 6.19 + (`Big-O' etc.), and asymptotic equivalence (\<open>\<sim>\<close>) 6.20 + 6.21 + \<^item> The @{command real_limit} command to compute the limit of a real-valued function at a 6.22 + certain point 6.23 + 6.24 + \<^item> The @{command real_expansion} command to compute the asymptotic expansion of a 6.25 + real-valued function at a certain point 6.26 + 6.27 + These three tools will be described in the following sections. 6.28 +\<close> 6.29 + 6.30 +section \<open>Supported Operations\<close> 6.31 + 6.32 +text \<open> 6.33 + The \<^verbatim>\<open>real_asymp\<close> package fully supports the following operations: 6.34 + 6.35 + \<^item> Basic arithmetic (addition, subtraction, multiplication, division) 6.36 + 6.37 + \<^item> Powers with constant natural exponent 6.38 + 6.39 + \<^item> @{term exp}, @{term ln}, @{term log}, @{term sqrt}, @{term "root k"} (for a constant k) 6.40 + 6.41 + \<^item> @{term sin}, @{term cos}, @{term tan} at finite points 6.42 + 6.43 + \<^item> @{term sinh}, @{term cosh}, @{term tanh} 6.44 + 6.45 + \<^item> @{term min}, @{term max}, @{term abs} 6.46 + 6.47 + Additionally, the following operations are supported in a `best effort' fashion using asymptotic 6.48 + upper/lower bounds: 6.49 + 6.50 + \<^item> Powers with variable natural exponent 6.51 + 6.52 + \<^item> @{term sin} and @{term cos} at \<open>\<plusminus>\<infinity>\<close> 6.53 + 6.54 + \<^item> @{term floor}, @{term ceiling}, @{term frac}, and \<open>mod\<close> 6.55 + 6.56 + Additionally, the @{term arctan} function is partially supported. The method may fail when 6.57 + the argument to @{term arctan} contains functions of different order of growth. 6.58 +\<close> 6.59 + 6.60 + 6.61 +section \<open>Proving Limits and Asymptotic Properties\<close> 6.62 + 6.63 +text \<open> 6.64 + \[ 6.65 + @{method_def (HOL) real_asymp} : \<open>method\<close> 6.66 + \] 6.67 + 6.68 + @{rail \<open> 6.69 + @@{method (HOL) real_asymp} opt? (@{syntax simpmod} * ) 6.70 + ; 6.71 + opt: '(' ('verbose' | 'fallback' ) ')' 6.72 + ; 6.73 + @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | '!' | 'del') | 6.74 + 'cong' (() | 'add' | 'del')) ':' @{syntax thms} 6.75 + \<close>} 6.76 +\<close> 6.77 + 6.78 +text \<open> 6.79 + The @{method real_asymp} method is a semi-automatic proof method for proving certain statements 6.80 + related to the asymptotic behaviour of real-valued functions. In the following, let \<open>f\<close> and \<open>g\<close> 6.81 + be functions of type @{typ "real \<Rightarrow> real"} and \<open>F\<close> and \<open>G\<close> real filters. 6.82 + 6.83 + The functions \<open>f\<close> and \<open>g\<close> can be built from the operations mentioned before and may contain free 6.84 + 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 6.85 + with approach from the left or from the right. 6.86 + 6.87 + The class of statements that is supported by @{method real_asymp} then consists of: 6.88 + 6.89 + \<^item> Limits, i.\,e.\ @{prop "filterlim f F G"} 6.90 + 6.91 + \<^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> 6.92 + 6.93 + \<^item> Asymptotic equivalence, i.\,e.\ @{prop "f \<sim>[F] g"} 6.94 + 6.95 + \<^item> Asymptotic inequalities, i.\,e.\ @{prop "eventually (\<lambda>x. f x \<le> g x) F"} 6.96 + 6.97 + For typical problems arising in practice that do not contain free variables, @{method real_asymp} 6.98 + tends to succeed fully automatically within fractions of seconds, e.\,g.: 6.99 +\<close> 6.100 + 6.101 +lemma \<open>filterlim (\<lambda>x::real. (1 + 1 / x) powr x) (nhds (exp 1)) at_top\<close> 6.102 + by real_asymp 6.103 + 6.104 +text \<open> 6.105 + What makes the method \<^emph>\<open>semi-automatic\<close> is the fact that it has to internally determine the 6.106 + sign of real-valued constants and identical zeroness of real-valued functions, and while the 6.107 + internal heuristics for this work very well most of the time, there are situations where the 6.108 + method fails to determine the sign of a constant, in which case the user needs to go back and 6.109 + supply more information about the sign of that constant in order to get a result. 6.110 + 6.111 + A simple example is the following: 6.112 +\<close> 6.113 +(*<*) 6.114 +experiment 6.115 + fixes a :: real 6.116 +begin 6.117 +(*>*) 6.118 +lemma \<open>filterlim (\<lambda>x::real. exp (a * x)) at_top at_top\<close> 6.119 +oops 6.120 + 6.121 +text \<open> 6.122 + Here, @{method real_asymp} outputs an error message stating that it could not determine the 6.123 + sign of the free variable @{term "a :: real"}. In this case, the user must add the assumption 6.124 + \<open>a > 0\<close> and give it to @{method real_asymp}. 6.125 +\<close> 6.126 +lemma 6.127 + assumes \<open>a > 0\<close> 6.128 + shows \<open>filterlim (\<lambda>x::real. exp (a * x)) at_top at_top\<close> 6.129 + using assms by real_asymp 6.130 +(*<*) 6.131 +end 6.132 +(*>*) 6.133 +text \<open> 6.134 + Additional modifications to the simpset that is used for determining signs can also be made 6.135 + with \<open>simp add:\<close> modifiers etc.\ in the same way as when using the @{method simp} method directly. 6.136 + 6.137 + The same situation can also occur without free variables if the constant in question is a 6.138 + complicated expression that the simplifier does not know enough ebout, 6.139 + e.\,g.\ @{term "pi - exp 1"}. 6.140 + 6.141 + In order to trace problems with sign determination, the \<open>(verbose)\<close> option can be passed to 6.142 + @{method real_asymp}. It will then print a detailed error message whenever it encounters 6.143 + a sign determination problem that it cannot solve. 6.144 + 6.145 + The \<open>(fallback)\<close> flag causes the method not to use asymptotic interval arithmetic, but only 6.146 + the much simpler core mechanism of computing a single Multiseries expansion for the input 6.147 + function. There should normally be no need to use this flag; however, the core part of the 6.148 + code has been tested much more rigorously than the asymptotic interval part. In case there 6.149 + is some implementation problem with it for a problem that can be solved without it, the 6.150 + \<open>(fallback)\<close> option can be used until that problem is resolved. 6.151 +\<close> 6.152 + 6.153 + 6.154 + 6.155 +section \<open>Diagnostic Commands\<close> 6.156 + 6.157 +text \<open> 6.158 + \[\begin{array}{rcl} 6.159 + @{command_def (HOL) real_limit} & : & \<open>context \<rightarrow>\<close> \\ 6.160 + @{command_def (HOL) real_expansion} & : & \<open>context \<rightarrow>\<close> 6.161 + \end{array}\] 6.162 + 6.163 + @{rail \<open> 6.164 + @@{command (HOL) real_limit} (limitopt*) 6.165 + ; 6.166 + @@{command (HOL) real_expansion} (expansionopt*) 6.167 + ; 6.168 + limitopt : ('limit' ':' @{syntax term}) | ('facts' ':' @{syntax thms}) 6.169 + ; 6.170 + expansionopt : 6.171 + ('limit' ':' @{syntax term}) | 6.172 + ('terms' ':' @{syntax nat} ('(' 'strict' ')') ?) | 6.173 + ('facts' ':' @{syntax thms}) 6.174 + \<close>} 6.175 + 6.176 + \<^descr>@{command real_limit} computes the limit of the given function \<open>f(x)\<close> for as \<open>x\<close> tends 6.177 + to the specified limit point. Additional facts can be provided with the \<open>facts\<close> option, 6.178 + similarly to the @{command using} command with @{method real_asymp}. The limit point given 6.179 + by the \<open>limit\<close> option must be one of the filters @{term "at_top"}, @{term "at_bot"}, 6.180 + @{term "at_left"}, or @{term "at_right"}. If no limit point is given, @{term "at_top"} is used 6.181 + by default. 6.182 + 6.183 + \<^medskip> 6.184 + 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>), 6.185 + \<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 6.186 + or from below (corresponding to @{term "at_right (0::real)"} and @{term "at_left (0::real)"}); 6.187 + for technical reasons, this information is currently not displayed if the limit is not 0. 6.188 + 6.189 + \<^medskip> 6.190 + If the given function does not tend to a definite limit (e.\,g.\ @{term "sin x"} for \<open>x \<rightarrow> \<infinity>\<close>), 6.191 + the command might nevertheless succeed to compute an asymptotic upper and/or lower bound and 6.192 + display the limits of these bounds instead. 6.193 + 6.194 + \<^descr>@{command real_expansion} works similarly to @{command real_limit}, but displays the first few 6.195 + terms of the asymptotic multiseries expansion of the given function at the given limit point 6.196 + and the order of growth of the remainder term. 6.197 + 6.198 + In addition to the options already explained for the @{command real_limit} command, it takes 6.199 + an additional option \<open>terms\<close> that controls how many of the leading terms of the expansion are 6.200 + printed. If the \<open>(strict)\<close> modifier is passed to the \<open>terms option\<close>, terms whose coefficient is 6.201 + 0 are dropped from the output and do not count to the number of terms to be output. 6.202 + 6.203 + \<^medskip> 6.204 + By default, the first three terms are output and the \<open>strict\<close> option is disabled. 6.205 + 6.206 + Note that these two commands are intended for diagnostic use only. While the central part 6.207 + of their implementation – finding a multiseries expansion and reading off the limit – are the 6.208 + same as in the @{method real_asymp} method and therefore trustworthy, there is a small amount 6.209 + of unverified code involved in pre-processing and printing (e.\,g.\ for reducing all the 6.210 + different options for the \<open>limit\<close> option to the @{term at_top} case). 6.211 +\<close> 6.212 + 6.213 + 6.214 +section \<open>Extensibility\<close> 6.215 + 6.216 +subsection \<open>Basic fact collections\<close> 6.217 + 6.218 +text \<open> 6.219 + The easiest way to add support for additional operations is to add corresponding facts 6.220 + to one of the following fact collections. However, this only works for particularly simple cases. 6.221 + 6.222 + \<^descr>@{thm [source] real_asymp_reify_simps} specifies a list of (unconditional) equations that are 6.223 + unfolded as a first step of @{method real_asymp} and the related commands. This can be used to 6.224 + add support for operations that can be represented easily by other operations that are already 6.225 + supported, such as @{term sinh}, which is equal to @{term "\<lambda>x. (exp x - exp (-x)) / 2"}. 6.226 + 6.227 + \<^descr>@{thm [source] real_asymp_nat_reify} and @{thm [source] real_asymp_int_reify} is used to 6.228 + convert operations on natural numbers or integers to operations on real numbers. This enables 6.229 + @{method real_asymp} to also work on functions that return a natural number or an integer. 6.230 +\<close> 6.231 + 6.232 +subsection \<open>Expanding Custom Operations\<close> 6.233 + 6.234 +text \<open> 6.235 + Support for some non-trivial new operation \<open>f(x\<^sub>1, \<dots>, x\<^sub>n)\<close> can be added dynamically at any 6.236 + time, but it involves writing ML code and involves a significant amount of effort, especially 6.237 + when the function has essential singularities. 6.238 + 6.239 + The first step is to write an ML function that takes as arguments 6.240 + \<^item> the expansion context 6.241 + \<^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>) 6.242 + \<^item> a list of \<open>n\<close> theorems of the form @{prop "(g\<^sub>i expands_to G\<^sub>i) bs"} 6.243 + \<^item> the current basis \<open>bs\<close> 6.244 + and returns a theorem of the form @{prop "(t expands_to F) bs'"} and a new basis \<open>bs'\<close> which 6.245 + must be a superset of the original basis. 6.246 + 6.247 + This function must then be registered as a handler for the operation by proving a vacuous lemma 6.248 + of the form @{prop "REAL_ASYMP_CUSTOM f"} (which is only used for tagging) and passing that 6.249 + lemma and the expansion function to @{ML [source] Exp_Log_Expression.register_custom_from_thm} 6.250 + in a @{command local_setup} invocation. 6.251 + 6.252 + If the expansion produced by the handler function contains new definitions, corresponding 6.253 + evaluation equations must be added to the fact collection @{thm [source] real_asymp_eval_eqs}. 6.254 + 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> 6.255 + (i.\,e.\ the function on the left-hand side must be fully applied) and the \<open>p\<^sub>i\<close> can be patterns 6.256 + involving \<open>constructors\<close>. 6.257 + 6.258 + New constructors for this pattern matching can be registered by adding a theorem of the form 6.259 + @{prop "REAL_ASYMP_EVAL_CONSTRUCTOR c"} to the fact collection 6.260 + @{thm [source] exp_log_eval_constructor}, but this should be quite rare in practice. 6.261 + 6.262 + \<^medskip> 6.263 + Note that there is currently no way to add support for custom operations in connection with 6.264 + `oscillating' terms. The above mechanism only works if all arguments of the new operation have 6.265 + an exact multiseries expansion. 6.266 +\<close> 6.267 + 6.268 + 6.269 +subsection \<open>Extending the Sign Oracle\<close> 6.270 + 6.271 +text \<open> 6.272 + By default, the \<^verbatim>\<open>real_asymp\<close> package uses the simplifier with the given simpset and facts 6.273 + in order to determine the sign of real constants. This is done by invoking the simplifier 6.274 + 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 6.275 + context. 6.276 + 6.277 + If the simplifier cannot prove any of them, the entire method (or command) invocation will fail. 6.278 + It is, however, possible to dynamically add additional sign oracles that will be tried; the 6.279 + most obvious candidate for an oracle that one may want to add or remove dynamically are 6.280 + approximation-based tactics. 6.281 + 6.282 + Adding such a tactic can be done by calling 6.283 + @{ML [source] Multiseries_Expansion.register_sign_oracle}. Note that if the tactic cannot prove 6.284 + a goal, it should fail as fast as possible. 6.285 +\<close> 6.286 + 6.287 +(*<*) 6.288 +end 6.289 +(*>*)

7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 7.2 +++ b/src/HOL/Real_Asymp/Manual/document/root.tex Sun Jul 22 19:29:51 2018 +0200 7.3 @@ -0,0 +1,39 @@ 7.4 +\documentclass[11pt,a4paper]{article} 7.5 +\usepackage{amsfonts, amsmath, amssymb} 7.6 +\usepackage{railsetup} 7.7 +\usepackage{iman} 7.8 +\usepackage{extra} 7.9 +\usepackage{isar} 7.10 +\usepackage{isabelle} 7.11 +\usepackage{isabellesym} 7.12 +\usepackage{style} 7.13 + 7.14 +% this should be the last package used 7.15 +\usepackage{pdfsetup} 7.16 + 7.17 +% urls in roman style, theory text in math-similar italics 7.18 +\urlstyle{rm} 7.19 +\isabellestyle{it} 7.20 + 7.21 + 7.22 +\begin{document} 7.23 + 7.24 +\title{\texttt{real\_asymp}: Semi-Automatic Real Asymptotics\\ in Isabelle\slash HOL} 7.25 +\author{Manuel Eberl} 7.26 +\maketitle 7.27 + 7.28 +\tableofcontents 7.29 +\newpage 7.30 +\parindent 0pt\parskip 0.5ex 7.31 + 7.32 +\input{session} 7.33 + 7.34 +\bibliographystyle{abbrv} 7.35 +\bibliography{root} 7.36 + 7.37 +\end{document} 7.38 + 7.39 +%%% Local Variables: 7.40 +%%% mode: latex 7.41 +%%% TeX-master: t 7.42 +%%% End:

8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 8.2 +++ b/src/HOL/Real_Asymp/Manual/document/style.sty Sun Jul 22 19:29:51 2018 +0200 8.3 @@ -0,0 +1,46 @@ 8.4 + 8.5 +%% toc 8.6 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} 8.7 +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} 8.8 + 8.9 +%% paragraphs 8.10 +\setlength{\parindent}{1em} 8.11 + 8.12 +%% references 8.13 +\newcommand{\secref}[1]{\S\ref{#1}} 8.14 +\newcommand{\figref}[1]{figure~\ref{#1}} 8.15 + 8.16 +%% logical markup 8.17 +\newcommand{\strong}[1]{{\bfseries {#1}}} 8.18 +\newcommand{\qn}[1]{\emph{#1}} 8.19 + 8.20 +%% typographic conventions 8.21 +\newcommand{\qt}[1]{``{#1}''} 8.22 +\newcommand{\ditem}[1]{\item[\isastyletext #1]} 8.23 + 8.24 +%% quote environment 8.25 +\isakeeptag{quote} 8.26 +\renewenvironment{quote} 8.27 + {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax} 8.28 + {\endlist} 8.29 +\renewcommand{\isatagquote}{\begin{quote}} 8.30 +\renewcommand{\endisatagquote}{\end{quote}} 8.31 +\newcommand{\quotebreak}{\\[1.2ex]} 8.32 + 8.33 +%% presentation 8.34 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} 8.35 + 8.36 +%% character detail 8.37 +\renewcommand{\isadigit}[1]{\isamath{#1}} 8.38 +\binperiod 8.39 +\underscoreoff 8.40 + 8.41 +%% format 8.42 +\pagestyle{headings} 8.43 +\isabellestyle{it} 8.44 + 8.45 + 8.46 +%%% Local Variables: 8.47 +%%% mode: latex 8.48 +%%% TeX-master: "implementation" 8.49 +%%% End: