Moved Real_Asymp manual
authoreberlm <eberlm@in.tum.de>
Sun Jul 22 19:29:51 2018 +0200 (12 months ago)
changeset 6867799b1cf1e2d48
parent 68676 74cb08ff2e66
child 68679 2a20b315a44d
Moved Real_Asymp manual
src/Doc/ROOT
src/Doc/Real_Asymp/Real_Asymp_Doc.thy
src/Doc/Real_Asymp/document/root.tex
src/Doc/Real_Asymp/document/style.sty
src/HOL/ROOT
src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy
src/HOL/Real_Asymp/Manual/document/root.tex
src/HOL/Real_Asymp/Manual/document/style.sty
     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: