author paulson Sun Jul 15 16:05:38 2018 +0100 (15 months ago) changeset 68635 8094b853a92f parent 68634 db0980691ef4 child 68636 f33ffa0a27a1
fixes and more de-applying
 src/Doc/Tutorial/Types/Numbers.thy file | annotate | diff | revisions src/Doc/Tutorial/document/numerics.tex file | annotate | diff | revisions src/HOL/Analysis/Borel_Space.thy file | annotate | diff | revisions src/HOL/Deriv.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
     1.1 --- a/src/Doc/Tutorial/Types/Numbers.thy	Sun Jul 15 13:15:31 2018 +0100
1.2 +++ b/src/Doc/Tutorial/Types/Numbers.thy	Sun Jul 15 16:05:38 2018 +0100
1.3 @@ -117,7 +117,7 @@
1.6
1.7 -For the integers, I'd list a few theorems that somehow involve negative
1.8 +For the integers, I'd list a few theorems that somehow involve negative
1.9  numbers.\<close>
1.10
1.11
1.12 @@ -137,8 +137,8 @@
1.13  @{thm[display] neg_mod_bound[no_vars]}
1.14  \rulename{neg_mod_bound}
1.15
1.20
1.23 @@ -154,13 +154,13 @@
1.24
1.25  @{thm[display] zmod_zmult2_eq[no_vars]}
1.26  \rulename{zmod_zmult2_eq}
1.27 -\<close>
1.28 +\<close>
1.29
1.30  lemma "abs (x+y) \<le> abs x + abs (y :: int)"
1.31  by arith
1.32
1.33  lemma "abs (2*x) = 2 * abs (x :: int)"
1.36
1.37
1.38  text \<open>Induction rules for the Integers
1.39 @@ -176,7 +176,7 @@
1.40
1.41  @{thm[display] int_less_induct[no_vars]}
1.42  \rulename{int_less_induct}
1.43 -\<close>
1.44 +\<close>
1.45
1.46  text \<open>FIELDS
1.47
1.48 @@ -208,13 +208,13 @@
1.49  \<close>
1.50
1.51  lemma "3/4 < (7/8 :: real)"
1.52 -by simp
1.53 +by simp
1.54
1.55  lemma "P ((3/4) * (8/15 :: real))"
1.56  txt\<open>
1.57  @{subgoals[display,indent=0,margin=65]}
1.58  \<close>
1.59 -apply simp
1.60 +apply simp
1.61  txt\<open>
1.62  @{subgoals[display,indent=0,margin=65]}
1.63  \<close>
1.64 @@ -224,7 +224,7 @@
1.65  txt\<open>
1.66  @{subgoals[display,indent=0,margin=65]}
1.67  \<close>
1.68 -apply simp
1.69 +apply simp
1.70  txt\<open>
1.71  @{subgoals[display,indent=0,margin=65]}
1.72  \<close>

     2.1 --- a/src/Doc/Tutorial/document/numerics.tex	Sun Jul 15 13:15:31 2018 +0100
2.2 +++ b/src/Doc/Tutorial/document/numerics.tex	Sun Jul 15 16:05:38 2018 +0100
2.3 @@ -11,7 +11,7 @@
2.4  subtraction.  With subtraction, arithmetic reasoning is easier, which makes
2.5  the integers preferable to the natural numbers for
2.6  complicated arithmetic expressions, even if they are non-negative.  There are also the types
2.7 -\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers.  Isabelle has no
2.8 +\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers.  Isabelle has no
2.9  subtyping,  so the numeric
2.10  types are distinct and there are functions to convert between them.
2.11  Most numeric operations are overloaded: the same symbol can be
2.12 @@ -19,7 +19,7 @@
2.13  shows the most important operations, together with the priorities of the
2.14  infix symbols. Algebraic properties are organized using type classes
2.15  around algebraic concepts such as rings and fields;
2.16 -a property such as the commutativity of addition is a single theorem
2.17 +a property such as the commutativity of addition is a single theorem
2.18  (\isa{add.commute}) that applies to all numeric types.
2.19
2.20  \index{linear arithmetic}%
2.21 @@ -28,7 +28,7 @@
2.22  \methdx{arith}.  Linear arithmetic comprises addition, subtraction
2.23  and multiplication by constant factors; subterms involving other operators
2.24  are regarded as variables.  The procedure can be slow, especially if the
2.25 -subgoal to be proved involves subtraction over type \isa{nat}, which
2.26 +subgoal to be proved involves subtraction over type \isa{nat}, which
2.27  causes case splits.  On types \isa{nat} and \isa{int}, \methdx{arith}
2.28  can deal with quantifiers---this is known as Presburger arithmetic---whereas on type \isa{real} it cannot.
2.29
2.30 @@ -51,19 +51,19 @@
2.31  numbers, integers, rationals, reals, etc.; they denote integer values of
2.32  arbitrary size.
2.33
2.34 -Literals look like constants, but they abbreviate
2.35 -terms representing the number in a two's complement binary notation.
2.36 -Isabelle performs arithmetic on literals by rewriting rather
2.37 -than using the hardware arithmetic. In most cases arithmetic
2.38 -is fast enough, even for numbers in the millions. The arithmetic operations
2.39 -provided for literals include addition, subtraction, multiplication,
2.40 +Literals look like constants, but they abbreviate
2.41 +terms representing the number in a two's complement binary notation.
2.42 +Isabelle performs arithmetic on literals by rewriting rather
2.43 +than using the hardware arithmetic. In most cases arithmetic
2.44 +is fast enough, even for numbers in the millions. The arithmetic operations
2.45 +provided for literals include addition, subtraction, multiplication,
2.46  integer division and remainder.  Fractions of literals (expressed using
2.47  division) are reduced to lowest terms.
2.48
2.50 -The arithmetic operators are
2.51 -overloaded, so you must be careful to ensure that each numeric
2.52 -expression refers to a specific type, if necessary by inserting
2.53 +The arithmetic operators are
2.54 +overloaded, so you must be careful to ensure that each numeric
2.55 +expression refers to a specific type, if necessary by inserting
2.56  type constraints.  Here is an example of what can go wrong:
2.57  \par
2.58  \begin{isabelle}
2.59 @@ -80,7 +80,7 @@
2.60  \end{warn}
2.61
2.62  \begin{warn}
2.63 -\index{function@\isacommand {function} (command)!and numeric literals}
2.64 +\index{function@\isacommand {function} (command)!and numeric literals}
2.65  Numeric literals are not constructors and therefore
2.66  must not be used in patterns.  For example, this declaration is
2.67  rejected:
2.68 @@ -103,7 +103,7 @@
2.69  \index{natural numbers|(}\index{*nat (type)|(}%
2.70  This type requires no introduction: we have been using it from the
2.71  beginning.  Hundreds of theorems about the natural numbers are
2.72 -proved in the theories \isa{Nat} and \isa{Divides}.
2.73 +proved in the theories \isa{Nat} and \isa{Divides}.
2.74  Basic properties of addition and multiplication are available through the
2.75  axiomatic type class for semirings (\S\ref{sec:numeric-classes}).
2.76
2.77 @@ -123,7 +123,7 @@
2.78  applied to terms of the form \isa{Suc\ $n$}.
2.79
2.80  The following default  simplification rules replace
2.81 -small literals by zero and successor:
2.82 +small literals by zero and successor:
2.83  \begin{isabelle}
2.84  2\ +\ n\ =\ Suc\ (Suc\ n)
2.86 @@ -146,7 +146,7 @@
2.87  \rulenamedx{div_mult_mod_eq}
2.88  \end{isabelle}
2.89
2.90 -Many less obvious facts about quotient and remainder are also provided.
2.91 +Many less obvious facts about quotient and remainder are also provided.
2.92  Here is a selection:
2.93  \begin{isabelle}
2.94  a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
2.95 @@ -181,7 +181,7 @@
2.96
2.97  The \textbf{divides} relation\index{divides relation}
2.98  has the standard definition, which
2.99 -is overloaded over all numeric types:
2.100 +is overloaded over all numeric types:
2.101  \begin{isabelle}
2.102  m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
2.103  \rulenamedx{dvd_def}
2.104 @@ -198,10 +198,10 @@
2.105
2.106  \subsubsection{Subtraction}
2.107
2.108 -There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless
2.109 +There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless
2.110  \isa{m} exceeds~\isa{n}. The following is one of the few facts
2.111  about \isa{m\ -\ n} that is not subject to
2.112 -the condition \isa{n\ \isasymle \  m}.
2.113 +the condition \isa{n\ \isasymle \  m}.
2.114  \begin{isabelle}
2.115  (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
2.116  \rulenamedx{diff_mult_distrib}
2.117 @@ -234,7 +234,7 @@
2.118  \subsection{The Type of Integers, {\tt\slshape int}}
2.119
2.120  \index{integers|(}\index{*int (type)|(}%
2.121 -Reasoning methods for the integers resemble those for the natural numbers,
2.122 +Reasoning methods for the integers resemble those for the natural numbers,
2.123  but induction and
2.124  the constant \isa{Suc} are not available.  HOL provides many lemmas for
2.125  proving inequalities involving integer multiplication and division, similar
2.126 @@ -242,9 +242,9 @@
2.127  and multiplication are available through the axiomatic type class for rings
2.128  (\S\ref{sec:numeric-classes}).
2.129
2.130 -The \rmindex{absolute value} function \cdx{abs} is overloaded, and is
2.131 +The \rmindex{absolute value} function \cdx{abs} is overloaded, and is
2.132  defined for all types that involve negative numbers, including the integers.
2.133 -The \isa{arith} method can prove facts about \isa{abs} automatically,
2.134 +The \isa{arith} method can prove facts about \isa{abs} automatically,
2.135  though as it does so by case analysis, the cost can be exponential.
2.136  \begin{isabelle}
2.137  \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
2.138 @@ -271,7 +271,7 @@
2.139  \begin{isabelle}
2.140  (a\ +\ b)\ div\ c\ =\isanewline
2.141  a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
2.144  \par\smallskip
2.145  (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
2.147 @@ -320,9 +320,9 @@
2.148  \index{rational numbers|(}\index{*rat (type)|(}%
2.149  \index{real numbers|(}\index{*real (type)|(}%
2.150  \index{complex numbers|(}\index{*complex (type)|(}%
2.151 -These types provide true division, the overloaded operator \isa{/},
2.152 -which differs from the operator \isa{div} of the
2.153 -natural numbers and integers. The rationals and reals are
2.154 +These types provide true division, the overloaded operator \isa{/},
2.155 +which differs from the operator \isa{div} of the
2.156 +natural numbers and integers. The rationals and reals are
2.157  \textbf{dense}: between every two distinct numbers lies another.
2.158  This property follows from the division laws, since if $x\not=y$ then $(x+y)/2$ lies between them:
2.159  \begin{isabelle}
2.160 @@ -334,7 +334,7 @@
2.161  is bounded above has a least upper bound.  Completeness distinguishes the
2.162  reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
2.163  upper bound.  (It could only be $\surd2$, which is irrational.) The
2.164 -formalization of completeness, which is complicated,
2.165 +formalization of completeness, which is complicated,
2.166  can be found in theory \texttt{RComplete}.
2.167
2.168  Numeric literals\index{numeric literals!for type \protect\isa{real}}
2.169 @@ -357,13 +357,13 @@
2.170  \end{warn}
2.171
2.172  Available in the logic HOL-NSA is the
2.173 -theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
2.174 +theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
2.175  \rmindex{non-standard reals}.  These
2.176  \textbf{hyperreals} include infinitesimals, which represent infinitely
2.177  small and infinitely large quantities; they facilitate proofs
2.178  about limits, differentiation and integration~\cite{fleuriot-jcm}.  The
2.179  development defines an infinitely large number, \isa{omega} and an
2.180 -infinitely small positive number, \isa{epsilon}.  The
2.181 +infinitely small positive number, \isa{epsilon}.  The
2.182  relation $x\approx y$ means $x$ is infinitely close to~$y$.''
2.183  Theory \isa{Hyperreal} also defines transcendental functions such as sine,
2.184  cosine, exponential and logarithm --- even the versions for type
2.185 @@ -381,23 +381,23 @@
2.186  for all numeric types satisfying the necessary axioms. The theory defines
2.187  dozens of type classes, such as the following:
2.188  \begin{itemize}
2.189 -\item
2.190 +\item
2.191  \tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring}
2.192  provides the associative operators \isa{+} and~\isa{*}, with \isa{0} and~\isa{1}
2.193  as their respective identities. The operators enjoy the usual distributive law,
2.194  and addition (\isa{+}) is also commutative.
2.195  An \emph{ordered semiring} is also linearly
2.196  ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring.
2.197 -\item
2.198 +\item
2.199  \tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring
2.200  with unary minus (the additive inverse) and subtraction (both
2.201  denoted~\isa{-}). An \emph{ordered ring} includes the absolute value
2.202  function, \cdx{abs}. Type \isa{int} is an ordered ring.
2.203 -\item
2.204 +\item
2.205  \tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the
2.206  multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/})).
2.207  An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
2.208 -\item
2.209 +\item
2.210  \tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}
2.211  and \isa{a / 0 = 0}. These include all of Isabelle's standard numeric types.
2.212  However, the basic properties of fields are derived without assuming
2.213 @@ -435,7 +435,7 @@
2.214
2.215
2.216  \subsubsection{Simplifying with the AC-Laws}
2.217 -Suppose that two expressions are equal, differing only in
2.218 +Suppose that two expressions are equal, differing only in
2.219  associativity and commutativity of addition.  Simplifying with the
2.220  following equations sorts the terms and groups them to the right, making
2.221  the two expressions identical.
2.222 @@ -447,9 +447,9 @@
2.223  a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
2.225  \end{isabelle}
2.226 -The name \isa{ac_simps}\index{*ac_simps (theorems)}
2.227 +The name \isa{ac_simps}\index{*ac_simps (theorems)}
2.228  refers to the list of all three theorems; similarly
2.229 -there is \isa{ac_simps}.\index{*ac_simps (theorems)}
2.230 +there is \isa{ac_simps}.\index{*ac_simps (theorems)}
2.231  They are all proved for semirings and therefore hold for all numeric types.
2.232
2.233  Here is an example of the sorting effect.  Start
2.234 @@ -506,16 +506,16 @@
2.235
2.236  \subsubsection{Absolute Value}
2.237
2.238 -The \rmindex{absolute value} function \cdx{abs} is available for all
2.239 +The \rmindex{absolute value} function \cdx{abs} is available for all
2.240  ordered rings, including types \isa{int}, \isa{rat} and \isa{real}.
2.241  It satisfies many properties,
2.242  such as the following:
2.243  \begin{isabelle}
2.244 -\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
2.245 +\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
2.246  \rulename{abs_mult}\isanewline
2.247  (\isasymbar a\isasymbar \ \isasymle \ b)\ =\ (a\ \isasymle \ b\ \isasymand \ -\ a\ \isasymle \ b)
2.248  \rulename{abs_le_iff}\isanewline
2.249 -\isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar
2.250 +\isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar
2.251  \rulename{abs_triangle_ineq}
2.252  \end{isabelle}
2.253
2.254 @@ -528,9 +528,9 @@
2.255
2.256  \subsubsection{Raising to a Power}
2.257
2.258 -Another type class, \tcdx{ordered\_idom}, specifies rings that also have
2.259 +Another type class, \tcdx{ordered\_idom}, specifies rings that also have
2.260  exponentation to a natural number power, defined using the obvious primitive
2.261 -recursion. Theory \thydx{Power} proves various theorems, such as the
2.262 +recursion. Theory \thydx{Power} proves various theorems, such as the
2.263  following.
2.264  \begin{isabelle}
2.265  a\ \isacharcircum \ (m\ +\ n)\ =\ a\ \isacharcircum \ m\ *\ a\ \isacharcircum \ n%

     3.1 --- a/src/HOL/Analysis/Borel_Space.thy	Sun Jul 15 13:15:31 2018 +0100
3.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Sun Jul 15 16:05:38 2018 +0100
3.3 @@ -254,8 +254,8 @@
3.4    shows "g a \<le> g b"
3.5  proof (cases "a < b")
3.6    assume "a < b"
3.7 -  from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
3.8 -  from MVT2[OF \<open>a < b\<close> this] and deriv
3.9 +  from deriv have "\<And>x. \<lbrakk>x \<ge> a; x \<le> b\<rbrakk> \<Longrightarrow> (g has_real_derivative g' x) (at x)" by simp
3.10 +  with MVT2[OF \<open>a < b\<close>] and deriv
3.11      obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
3.12    from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
3.13    with g_ab show ?thesis by simp

     4.1 --- a/src/HOL/Deriv.thy	Sun Jul 15 13:15:31 2018 +0100
4.2 +++ b/src/HOL/Deriv.thy	Sun Jul 15 16:05:38 2018 +0100
4.3 @@ -1031,25 +1031,26 @@
4.4
4.5  lemma has_field_derivative_cong_ev:
4.6    assumes "x = y"
4.7 -    and *: "eventually (\<lambda>x. x \<in> s \<longrightarrow> f x = g x) (nhds x)"
4.8 -    and "u = v" "s = t" "x \<in> s"
4.9 -  shows "(f has_field_derivative u) (at x within s) = (g has_field_derivative v) (at y within t)"
4.10 +    and *: "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x = g x) (nhds x)"
4.11 +    and "u = v" "S = t" "x \<in> S"
4.12 +  shows "(f has_field_derivative u) (at x within S) = (g has_field_derivative v) (at y within t)"
4.13    unfolding has_field_derivative_iff
4.14  proof (rule filterlim_cong)
4.15    from assms have "f y = g y"
4.16      by (auto simp: eventually_nhds)
4.17 -  with * show "\<forall>\<^sub>F xa in at x within s. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)"
4.18 +  with * show "\<forall>\<^sub>F z in at x within S. (f z - f x) / (z - x) = (g z - g y) / (z - y)"
4.19      unfolding eventually_at_filter
4.20      by eventually_elim (auto simp: assms \<open>f y = g y\<close>)
4.22
4.23  lemma has_field_derivative_cong_eventually:
4.24 -  assumes "eventually (\<lambda>x. f x = g x) (at x within s)" "f x=g x"
4.25 -  shows "(f has_field_derivative u) (at x within s) = (g has_field_derivative u) (at x within s)"
4.26 +  assumes "eventually (\<lambda>x. f x = g x) (at x within S)" "f x = g x"
4.27 +  shows "(f has_field_derivative u) (at x within S) = (g has_field_derivative u) (at x within S)"
4.28    unfolding has_field_derivative_iff
4.29 -  apply (rule tendsto_cong)
4.30 -  apply (insert assms)
4.31 -  by (auto elim: eventually_mono)
4.32 +proof (rule tendsto_cong)
4.33 +  show "\<forall>\<^sub>F y in at x within S. (f y - f x) / (y - x) = (g y - g x) / (y - x)"
4.34 +    using assms by (auto elim: eventually_mono)
4.35 +qed
4.36
4.37  lemma DERIV_cong_ev:
4.38    "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
4.39 @@ -1257,22 +1258,24 @@
4.40  subsection \<open>Rolle's Theorem\<close>
4.41
4.42  text \<open>Lemma about introducing open ball in open interval\<close>
4.43 -lemma lemma_interval_lt: "a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a < y \<and> y < b)"
4.44 -  for a b x :: real
4.45 -  apply (simp add: abs_less_iff)
4.46 -  apply (insert linorder_linear [of "x - a" "b - x"])
4.47 -  apply safe
4.48 -   apply (rule_tac x = "x - a" in exI)
4.49 -   apply (rule_tac [2] x = "b - x" in exI)
4.50 -   apply auto
4.51 -  done
4.52 +lemma lemma_interval_lt:
4.53 +  fixes a b x :: real
4.54 +  assumes "a < x" "x < b"
4.55 +  shows "\<exists>d. 0 < d \<and> (\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a < y \<and> y < b)"
4.56 +  using linorder_linear [of "x - a" "b - x"]
4.57 +proof
4.58 +  assume "x - a \<le> b - x"
4.59 +  with assms show ?thesis
4.60 +    by (rule_tac x = "x - a" in exI) auto
4.61 +next
4.62 +  assume "b - x \<le> x - a"
4.63 +  with assms show ?thesis
4.64 +    by (rule_tac x = "b - x" in exI) auto
4.65 +qed
4.66
4.67  lemma lemma_interval: "a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b)"
4.68    for a b x :: real
4.69 -  apply (drule lemma_interval_lt)
4.70 -   apply auto
4.71 -  apply force
4.72 -  done
4.73 +  by (force dest: lemma_interval_lt)
4.74
4.75  text \<open>Rolle's Theorem.
4.76     If @{term f} is defined and continuous on the closed interval
4.77 @@ -1401,14 +1404,23 @@
4.78    qed
4.79  qed
4.80
4.81 -lemma MVT2:
4.82 -  "a < b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> DERIV f x :> f' x \<Longrightarrow>
4.83 -    \<exists>z::real. a < z \<and> z < b \<and> (f b - f a = (b - a) * f' z)"
4.84 -  apply (drule MVT)
4.85 -    apply (blast intro: DERIV_isCont)
4.86 -   apply (force dest: order_less_imp_le simp add: real_differentiable_def)
4.87 -  apply (blast dest: DERIV_unique order_less_imp_le)
4.88 -  done
4.89 +corollary MVT2:
4.90 +  assumes "a < b" and der: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> DERIV f x :> f' x"
4.91 +  shows "\<exists>z::real. a < z \<and> z < b \<and> (f b - f a = (b - a) * f' z)"
4.92 +proof -
4.93 +  have "\<exists>l z. a < z \<and>
4.94 +           z < b \<and>
4.95 +           (f has_real_derivative l) (at z) \<and>
4.96 +           f b - f a = (b - a) * l"
4.97 +  proof (rule MVT [OF \<open>a < b\<close>])
4.98 +    show "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
4.99 +      using assms by (blast intro: DERIV_isCont)
4.100 +    show "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable at x"
4.101 +      using assms by (force dest: order_less_imp_le simp add: real_differentiable_def)
4.102 +  qed
4.103 +  with assms show ?thesis
4.104 +    by (blast dest: DERIV_unique order_less_imp_le)
4.105 +qed
4.106
4.107  lemma pos_deriv_imp_strict_mono:
4.108    assumes "\<And>x. (f has_real_derivative f' x) (at x)"

     5.1 --- a/src/HOL/Transcendental.thy	Sun Jul 15 13:15:31 2018 +0100
5.2 +++ b/src/HOL/Transcendental.thy	Sun Jul 15 16:05:38 2018 +0100
5.3 @@ -4165,7 +4165,7 @@
5.4    shows "cos x < cos y"
5.5  proof -
5.6    have "- (x - y) < 0" using assms by auto
5.7 -  from MVT2[OF \<open>y < x\<close> DERIV_cos[THEN impI, THEN allI]]
5.8 +  from MVT2[OF \<open>y < x\<close> DERIV_cos]
5.9    obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
5.10      by auto
5.11    then have "0 < z" and "z < pi"
5.12 @@ -4677,14 +4677,11 @@
5.13    assumes "- (pi/2) < y" and "y < x" and "x < pi/2"
5.14    shows "tan y < tan x"
5.15  proof -
5.16 -  have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
5.17 -  proof (rule allI, rule impI)
5.18 -    fix x' :: real
5.19 -    assume "y \<le> x' \<and> x' \<le> x"
5.20 -    then have "-(pi/2) < x'" and "x' < pi/2"
5.21 -      using assms by auto
5.22 -    from cos_gt_zero_pi[OF this]
5.23 -    have "cos x' \<noteq> 0" by auto
5.24 +  have "DERIV tan x' :> inverse ((cos x')\<^sup>2)" if "y \<le> x'" "x' \<le> x" for x'
5.25 +  proof -
5.26 +    have "-(pi/2) < x'" and "x' < pi/2"
5.27 +      using that assms by auto
5.28 +    with cos_gt_zero_pi have "cos x' \<noteq> 0" by force
5.29      then show "DERIV tan x' :> inverse ((cos x')\<^sup>2)"
5.30        by (rule DERIV_tan)
5.31    qed