--- a/src/Doc/Tutorial/Types/Numbers.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/Doc/Tutorial/Types/Numbers.thy Sun Jul 15 18:22:31 2018 +0100
@@ -117,7 +117,7 @@
@{thm[display] dvd_add[no_vars]}
\rulename{dvd_add}
-For the integers, I'd list a few theorems that somehow involve negative
+For the integers, I'd list a few theorems that somehow involve negative
numbers.\<close>
@@ -137,14 +137,14 @@
@{thm[display] neg_mod_bound[no_vars]}
\rulename{neg_mod_bound}
-@{thm[display] zdiv_zadd1_eq[no_vars]}
-\rulename{zdiv_zadd1_eq}
+@{thm[display] div_add1_eq[no_vars]}
+\rulename{div_add1_eq}
@{thm[display] mod_add_eq[no_vars]}
\rulename{mod_add_eq}
-@{thm[display] zdiv_zmult1_eq[no_vars]}
-\rulename{zdiv_zmult1_eq}
+@{thm[display] div_mult1_eq[no_vars]}
+\rulename{div_mult1_eq}
@{thm[display] mod_mult_right_eq[no_vars]}
\rulename{mod_mult_right_eq}
@@ -154,13 +154,13 @@
@{thm[display] zmod_zmult2_eq[no_vars]}
\rulename{zmod_zmult2_eq}
-\<close>
+\<close>
lemma "abs (x+y) \<le> abs x + abs (y :: int)"
by arith
lemma "abs (2*x) = 2 * abs (x :: int)"
-by (simp add: abs_if)
+by (simp add: abs_if)
text \<open>Induction rules for the Integers
@@ -176,7 +176,7 @@
@{thm[display] int_less_induct[no_vars]}
\rulename{int_less_induct}
-\<close>
+\<close>
text \<open>FIELDS
@@ -208,13 +208,13 @@
\<close>
lemma "3/4 < (7/8 :: real)"
-by simp
+by simp
lemma "P ((3/4) * (8/15 :: real))"
txt\<open>
@{subgoals[display,indent=0,margin=65]}
\<close>
-apply simp
+apply simp
txt\<open>
@{subgoals[display,indent=0,margin=65]}
\<close>
@@ -224,7 +224,7 @@
txt\<open>
@{subgoals[display,indent=0,margin=65]}
\<close>
-apply simp
+apply simp
txt\<open>
@{subgoals[display,indent=0,margin=65]}
\<close>
--- a/src/Doc/Tutorial/document/numerics.tex Sun Jul 15 14:46:57 2018 +0200
+++ b/src/Doc/Tutorial/document/numerics.tex Sun Jul 15 18:22:31 2018 +0100
@@ -11,7 +11,7 @@
subtraction. With subtraction, arithmetic reasoning is easier, which makes
the integers preferable to the natural numbers for
complicated arithmetic expressions, even if they are non-negative. There are also the types
-\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers. Isabelle has no
+\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers. Isabelle has no
subtyping, so the numeric
types are distinct and there are functions to convert between them.
Most numeric operations are overloaded: the same symbol can be
@@ -19,7 +19,7 @@
shows the most important operations, together with the priorities of the
infix symbols. Algebraic properties are organized using type classes
around algebraic concepts such as rings and fields;
-a property such as the commutativity of addition is a single theorem
+a property such as the commutativity of addition is a single theorem
(\isa{add.commute}) that applies to all numeric types.
\index{linear arithmetic}%
@@ -28,7 +28,7 @@
\methdx{arith}. Linear arithmetic comprises addition, subtraction
and multiplication by constant factors; subterms involving other operators
are regarded as variables. The procedure can be slow, especially if the
-subgoal to be proved involves subtraction over type \isa{nat}, which
+subgoal to be proved involves subtraction over type \isa{nat}, which
causes case splits. On types \isa{nat} and \isa{int}, \methdx{arith}
can deal with quantifiers---this is known as Presburger arithmetic---whereas on type \isa{real} it cannot.
@@ -51,19 +51,19 @@
numbers, integers, rationals, reals, etc.; they denote integer values of
arbitrary size.
-Literals look like constants, but they abbreviate
-terms representing the number in a two's complement binary notation.
-Isabelle performs arithmetic on literals by rewriting rather
-than using the hardware arithmetic. In most cases arithmetic
-is fast enough, even for numbers in the millions. The arithmetic operations
-provided for literals include addition, subtraction, multiplication,
+Literals look like constants, but they abbreviate
+terms representing the number in a two's complement binary notation.
+Isabelle performs arithmetic on literals by rewriting rather
+than using the hardware arithmetic. In most cases arithmetic
+is fast enough, even for numbers in the millions. The arithmetic operations
+provided for literals include addition, subtraction, multiplication,
integer division and remainder. Fractions of literals (expressed using
division) are reduced to lowest terms.
\begin{warn}\index{overloading!and arithmetic}
-The arithmetic operators are
-overloaded, so you must be careful to ensure that each numeric
-expression refers to a specific type, if necessary by inserting
+The arithmetic operators are
+overloaded, so you must be careful to ensure that each numeric
+expression refers to a specific type, if necessary by inserting
type constraints. Here is an example of what can go wrong:
\par
\begin{isabelle}
@@ -80,7 +80,7 @@
\end{warn}
\begin{warn}
-\index{function@\isacommand {function} (command)!and numeric literals}
+\index{function@\isacommand {function} (command)!and numeric literals}
Numeric literals are not constructors and therefore
must not be used in patterns. For example, this declaration is
rejected:
@@ -103,7 +103,7 @@
\index{natural numbers|(}\index{*nat (type)|(}%
This type requires no introduction: we have been using it from the
beginning. Hundreds of theorems about the natural numbers are
-proved in the theories \isa{Nat} and \isa{Divides}.
+proved in the theories \isa{Nat} and \isa{Divides}.
Basic properties of addition and multiplication are available through the
axiomatic type class for semirings (\S\ref{sec:numeric-classes}).
@@ -123,7 +123,7 @@
applied to terms of the form \isa{Suc\ $n$}.
The following default simplification rules replace
-small literals by zero and successor:
+small literals by zero and successor:
\begin{isabelle}
2\ +\ n\ =\ Suc\ (Suc\ n)
\rulename{add_2_eq_Suc}\isanewline
@@ -146,7 +146,7 @@
\rulenamedx{div_mult_mod_eq}
\end{isabelle}
-Many less obvious facts about quotient and remainder are also provided.
+Many less obvious facts about quotient and remainder are also provided.
Here is a selection:
\begin{isabelle}
a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
@@ -181,7 +181,7 @@
The \textbf{divides} relation\index{divides relation}
has the standard definition, which
-is overloaded over all numeric types:
+is overloaded over all numeric types:
\begin{isabelle}
m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
\rulenamedx{dvd_def}
@@ -198,10 +198,10 @@
\subsubsection{Subtraction}
-There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless
+There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless
\isa{m} exceeds~\isa{n}. The following is one of the few facts
about \isa{m\ -\ n} that is not subject to
-the condition \isa{n\ \isasymle \ m}.
+the condition \isa{n\ \isasymle \ m}.
\begin{isabelle}
(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
\rulenamedx{diff_mult_distrib}
@@ -234,7 +234,7 @@
\subsection{The Type of Integers, {\tt\slshape int}}
\index{integers|(}\index{*int (type)|(}%
-Reasoning methods for the integers resemble those for the natural numbers,
+Reasoning methods for the integers resemble those for the natural numbers,
but induction and
the constant \isa{Suc} are not available. HOL provides many lemmas for
proving inequalities involving integer multiplication and division, similar
@@ -242,9 +242,9 @@
and multiplication are available through the axiomatic type class for rings
(\S\ref{sec:numeric-classes}).
-The \rmindex{absolute value} function \cdx{abs} is overloaded, and is
+The \rmindex{absolute value} function \cdx{abs} is overloaded, and is
defined for all types that involve negative numbers, including the integers.
-The \isa{arith} method can prove facts about \isa{abs} automatically,
+The \isa{arith} method can prove facts about \isa{abs} automatically,
though as it does so by case analysis, the cost can be exponential.
\begin{isabelle}
\isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
@@ -271,7 +271,7 @@
\begin{isabelle}
(a\ +\ b)\ div\ c\ =\isanewline
a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
-\rulename{zdiv_zadd1_eq}
+\rulename{div_add1_eq}
\par\smallskip
(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
\rulename{mod_add_eq}
@@ -320,9 +320,9 @@
\index{rational numbers|(}\index{*rat (type)|(}%
\index{real numbers|(}\index{*real (type)|(}%
\index{complex numbers|(}\index{*complex (type)|(}%
-These types provide true division, the overloaded operator \isa{/},
-which differs from the operator \isa{div} of the
-natural numbers and integers. The rationals and reals are
+These types provide true division, the overloaded operator \isa{/},
+which differs from the operator \isa{div} of the
+natural numbers and integers. The rationals and reals are
\textbf{dense}: between every two distinct numbers lies another.
This property follows from the division laws, since if $x\not=y$ then $(x+y)/2$ lies between them:
\begin{isabelle}
@@ -334,7 +334,7 @@
is bounded above has a least upper bound. Completeness distinguishes the
reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
upper bound. (It could only be $\surd2$, which is irrational.) The
-formalization of completeness, which is complicated,
+formalization of completeness, which is complicated,
can be found in theory \texttt{RComplete}.
Numeric literals\index{numeric literals!for type \protect\isa{real}}
@@ -357,13 +357,13 @@
\end{warn}
Available in the logic HOL-NSA is the
-theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
+theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
\rmindex{non-standard reals}. These
\textbf{hyperreals} include infinitesimals, which represent infinitely
small and infinitely large quantities; they facilitate proofs
about limits, differentiation and integration~\cite{fleuriot-jcm}. The
development defines an infinitely large number, \isa{omega} and an
-infinitely small positive number, \isa{epsilon}. The
+infinitely small positive number, \isa{epsilon}. The
relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
Theory \isa{Hyperreal} also defines transcendental functions such as sine,
cosine, exponential and logarithm --- even the versions for type
@@ -381,23 +381,23 @@
for all numeric types satisfying the necessary axioms. The theory defines
dozens of type classes, such as the following:
\begin{itemize}
-\item
+\item
\tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring}
provides the associative operators \isa{+} and~\isa{*}, with \isa{0} and~\isa{1}
as their respective identities. The operators enjoy the usual distributive law,
and addition (\isa{+}) is also commutative.
An \emph{ordered semiring} is also linearly
ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring.
-\item
+\item
\tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring
with unary minus (the additive inverse) and subtraction (both
denoted~\isa{-}). An \emph{ordered ring} includes the absolute value
function, \cdx{abs}. Type \isa{int} is an ordered ring.
-\item
+\item
\tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the
multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/})).
An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
-\item
+\item
\tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}
and \isa{a / 0 = 0}. These include all of Isabelle's standard numeric types.
However, the basic properties of fields are derived without assuming
@@ -435,7 +435,7 @@
\subsubsection{Simplifying with the AC-Laws}
-Suppose that two expressions are equal, differing only in
+Suppose that two expressions are equal, differing only in
associativity and commutativity of addition. Simplifying with the
following equations sorts the terms and groups them to the right, making
the two expressions identical.
@@ -447,9 +447,9 @@
a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
\rulename{add.left_commute}
\end{isabelle}
-The name \isa{ac_simps}\index{*ac_simps (theorems)}
+The name \isa{ac_simps}\index{*ac_simps (theorems)}
refers to the list of all three theorems; similarly
-there is \isa{ac_simps}.\index{*ac_simps (theorems)}
+there is \isa{ac_simps}.\index{*ac_simps (theorems)}
They are all proved for semirings and therefore hold for all numeric types.
Here is an example of the sorting effect. Start
@@ -506,16 +506,16 @@
\subsubsection{Absolute Value}
-The \rmindex{absolute value} function \cdx{abs} is available for all
+The \rmindex{absolute value} function \cdx{abs} is available for all
ordered rings, including types \isa{int}, \isa{rat} and \isa{real}.
It satisfies many properties,
such as the following:
\begin{isabelle}
-\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
+\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
\rulename{abs_mult}\isanewline
(\isasymbar a\isasymbar \ \isasymle \ b)\ =\ (a\ \isasymle \ b\ \isasymand \ -\ a\ \isasymle \ b)
\rulename{abs_le_iff}\isanewline
-\isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar
+\isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar
\rulename{abs_triangle_ineq}
\end{isabelle}
@@ -528,9 +528,9 @@
\subsubsection{Raising to a Power}
-Another type class, \tcdx{ordered\_idom}, specifies rings that also have
+Another type class, \tcdx{ordered\_idom}, specifies rings that also have
exponentation to a natural number power, defined using the obvious primitive
-recursion. Theory \thydx{Power} proves various theorems, such as the
+recursion. Theory \thydx{Power} proves various theorems, such as the
following.
\begin{isabelle}
a\ \isacharcircum \ (m\ +\ n)\ =\ a\ \isacharcircum \ m\ *\ a\ \isacharcircum \ n%
--- a/src/HOL/Analysis/Borel_Space.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Sun Jul 15 18:22:31 2018 +0100
@@ -254,8 +254,8 @@
shows "g a \<le> g b"
proof (cases "a < b")
assume "a < b"
- from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
- from MVT2[OF \<open>a < b\<close> this] and deriv
+ from deriv have "\<And>x. \<lbrakk>x \<ge> a; x \<le> b\<rbrakk> \<Longrightarrow> (g has_real_derivative g' x) (at x)" by simp
+ with MVT2[OF \<open>a < b\<close>] and deriv
obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
with g_ab show ?thesis by simp
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Jul 15 18:22:31 2018 +0100
@@ -6919,7 +6919,7 @@
then have "f field_differentiable at a"
using holfb \<open>0 < e\<close> holomorphic_on_imp_differentiable_at by auto
with True show ?thesis
- by (auto simp: continuous_at DERIV_iff2 simp flip: DERIV_deriv_iff_field_differentiable
+ by (auto simp: continuous_at has_field_derivative_iff simp flip: DERIV_deriv_iff_field_differentiable
elim: rev_iffD1 [OF _ LIM_equal])
next
case False with 2 that show ?thesis
--- a/src/HOL/Analysis/Further_Topology.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Sun Jul 15 18:22:31 2018 +0100
@@ -3987,7 +3987,7 @@
have "g field_differentiable at z within S" if "f field_differentiable at z within S" "z \<in> S" for z
proof -
obtain f' where f': "((\<lambda>y. (f y - f z) / (y - z)) \<longlongrightarrow> f') (at z within S)"
- using \<open>f field_differentiable at z within S\<close> by (auto simp: field_differentiable_def DERIV_iff2)
+ using \<open>f field_differentiable at z within S\<close> by (auto simp: field_differentiable_def has_field_derivative_iff)
then have ee: "((\<lambda>x. (exp(g x) - exp(g z)) / (x - z)) \<longlongrightarrow> f') (at z within S)"
by (simp add: feq \<open>z \<in> S\<close> Lim_transform_within [OF _ zero_less_one])
have "(((\<lambda>y. if y = g z then exp (g z) else (exp y - exp (g z)) / (y - g z)) \<circ> g) \<longlongrightarrow> exp (g z))
@@ -4013,7 +4013,7 @@
then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
then show ?thesis
- by (auto simp: field_differentiable_def DERIV_iff2)
+ by (auto simp: field_differentiable_def has_field_derivative_iff)
qed
then have "g holomorphic_on S"
using holf holomorphic_on_def by auto
@@ -4035,7 +4035,7 @@
have "g field_differentiable at z within S" if "f field_differentiable at z within S" "z \<in> S" for z
proof -
obtain f' where f': "((\<lambda>y. (f y - f z) / (y - z)) \<longlongrightarrow> f') (at z within S)"
- using \<open>f field_differentiable at z within S\<close> by (auto simp: field_differentiable_def DERIV_iff2)
+ using \<open>f field_differentiable at z within S\<close> by (auto simp: field_differentiable_def has_field_derivative_iff)
then have ee: "((\<lambda>x. (exp(g x) - exp(g z)) / (x - z)) \<longlongrightarrow> f') (at z within S)"
by (simp add: feq \<open>z \<in> S\<close> Lim_transform_within [OF _ zero_less_one])
have "(((\<lambda>y. if y = g z then exp (g z) else (exp y - exp (g z)) / (y - g z)) \<circ> g) \<longlongrightarrow> exp (g z))
@@ -4061,7 +4061,7 @@
then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
then show ?thesis
- by (auto simp: field_differentiable_def DERIV_iff2)
+ by (auto simp: field_differentiable_def has_field_derivative_iff)
qed
then have "g holomorphic_on S"
using holf holomorphic_on_def by auto
--- a/src/HOL/Analysis/Riemann_Mapping.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Sun Jul 15 18:22:31 2018 +0100
@@ -1363,7 +1363,7 @@
using \<open>z \<in> S\<close> contg continuous_on_eq_continuous_at isCont_def openS apply blast
by (simp add: \<open>g z \<noteq> 0\<close>)
then have "(g has_field_derivative deriv f z / (g z + g z)) (at z)"
- unfolding DERIV_iff2
+ unfolding has_field_derivative_iff
proof (rule Lim_transform_within_open)
show "open (ball z \<delta> \<inter> S)"
by (simp add: openS open_Int)
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Jul 15 18:22:31 2018 +0100
@@ -47,7 +47,7 @@
put_simpset HOL_basic_ss ctxt
addsimps @{thms refl mod_add_eq mod_add_left_eq
mod_add_right_eq
- div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
+ div_add1_eq [symmetric] div_add1_eq [symmetric]
mod_self
div_by_0 mod_by_0 div_0 mod_0
div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0
--- a/src/HOL/Deriv.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Deriv.thy Sun Jul 15 18:22:31 2018 +0100
@@ -93,11 +93,7 @@
lemma (in bounded_linear) has_derivative:
"(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F"
unfolding has_derivative_def
- apply safe
- apply (erule bounded_linear_compose [OF bounded_linear])
- apply (drule tendsto)
- apply (simp add: scaleR diff add zero)
- done
+ by (auto simp add: bounded_linear_compose [OF bounded_linear] scaleR diff dest: tendsto)
lemmas has_derivative_scaleR_right [derivative_intros] =
bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
@@ -157,15 +153,18 @@
lemma field_has_derivative_at:
fixes x :: "'a::real_normed_field"
- shows "(f has_derivative ( * ) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
- apply (unfold has_derivative_at)
- apply (simp add: bounded_linear_mult_right)
- apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
- apply (subst diff_divide_distrib)
- apply (subst times_divide_eq_left [symmetric])
- apply (simp cong: LIM_cong)
- apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
- done
+ shows "(f has_derivative ( * ) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" (is "?lhs = ?rhs")
+proof -
+ have "?lhs = (\<lambda>h. norm (f (x + h) - f x - D * h) / norm h) \<midarrow>0 \<rightarrow> 0"
+ by (simp add: bounded_linear_mult_right has_derivative_at)
+ also have "... = (\<lambda>y. norm ((f (x + y) - f x - D * y) / y)) \<midarrow>0\<rightarrow> 0"
+ by (simp cong: LIM_cong flip: nonzero_norm_divide)
+ also have "... = (\<lambda>y. norm ((f (x + y) - f x) / y - D / y * y)) \<midarrow>0\<rightarrow> 0"
+ by (simp only: diff_divide_distrib times_divide_eq_left [symmetric])
+ also have "... = ?rhs"
+ by (simp add: tendsto_norm_zero_iff LIM_zero_iff cong: LIM_cong)
+ finally show ?thesis .
+qed
lemma has_derivativeI:
"bounded_linear f' \<Longrightarrow>
@@ -414,8 +413,8 @@
lemma has_derivative_prod[simp, derivative_intros]:
fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_field"
- shows "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)) \<Longrightarrow>
- ((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within s)"
+ shows "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within S)) \<Longrightarrow>
+ ((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within S)"
proof (induct I rule: infinite_finite_induct)
case infinite
then show ?case by simp
@@ -425,7 +424,7 @@
next
case (insert i I)
let ?P = "\<lambda>y. f i x * (\<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x)) + (f' i y) * (\<Prod>i\<in>I. f i x)"
- have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within s)"
+ have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within S)"
using insert by (intro has_derivative_mult) auto
also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
using insert(1,2)
@@ -436,69 +435,56 @@
lemma has_derivative_power[simp, derivative_intros]:
fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
- assumes f: "(f has_derivative f') (at x within s)"
- shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within s)"
+ assumes f: "(f has_derivative f') (at x within S)"
+ shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within S)"
using has_derivative_prod[OF f, of "{..< n}"] by (simp add: prod_constant ac_simps)
lemma has_derivative_inverse':
fixes x :: "'a::real_normed_div_algebra"
assumes x: "x \<noteq> 0"
- shows "(inverse has_derivative (\<lambda>h. - (inverse x * h * inverse x))) (at x within s)"
- (is "(?inv has_derivative ?f) _")
+ shows "(inverse has_derivative (\<lambda>h. - (inverse x * h * inverse x))) (at x within S)"
+ (is "(_ has_derivative ?f) _")
proof (rule has_derivativeI_sandwich)
- show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
- apply (rule bounded_linear_minus)
- apply (rule bounded_linear_mult_const)
- apply (rule bounded_linear_const_mult)
- apply (rule bounded_linear_ident)
- done
+ show "bounded_linear (\<lambda>h. - (inverse x * h * inverse x))"
+ by (simp add: bounded_linear_minus bounded_linear_mult_const bounded_linear_mult_right)
show "0 < norm x" using x by simp
- show "((\<lambda>y. norm (?inv y - ?inv x) * norm (?inv x)) \<longlongrightarrow> 0) (at x within s)"
- apply (rule tendsto_mult_left_zero)
- apply (rule tendsto_norm_zero)
- apply (rule LIM_zero)
- apply (rule tendsto_inverse)
- apply (rule tendsto_ident_at)
- apply (rule x)
- done
+ have "(inverse \<longlongrightarrow> inverse x) (at x within S)"
+ using tendsto_inverse tendsto_ident_at x by auto
+ then show "((\<lambda>y. norm (inverse y - inverse x) * norm (inverse x)) \<longlongrightarrow> 0) (at x within S)"
+ by (simp add: LIM_zero_iff tendsto_mult_left_zero tendsto_norm_zero)
next
fix y :: 'a
assume h: "y \<noteq> x" "dist y x < norm x"
then have "y \<noteq> 0" by auto
- have "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) =
- norm ((?inv y - ?inv x) * (y - x) * ?inv x) / norm (y - x)"
- apply (subst inverse_diff_inverse [OF \<open>y \<noteq> 0\<close> x])
- apply (subst minus_diff_minus)
- apply (subst norm_minus_cancel)
- apply (simp add: left_diff_distrib)
- done
- also have "\<dots> \<le> norm (?inv y - ?inv x) * norm (y - x) * norm (?inv x) / norm (y - x)"
- apply (rule divide_right_mono [OF _ norm_ge_zero])
- apply (rule order_trans [OF norm_mult_ineq])
- apply (rule mult_right_mono [OF _ norm_ge_zero])
- apply (rule norm_mult_ineq)
- done
- also have "\<dots> = norm (?inv y - ?inv x) * norm (?inv x)"
+ have "norm (inverse y - inverse x - ?f (y -x)) / norm (y - x)
+ = norm (- (inverse y * (y - x) * inverse x - inverse x * (y - x) * inverse x)) /
+ norm (y - x)"
+ by (simp add: \<open>y \<noteq> 0\<close> inverse_diff_inverse x)
+ also have "... = norm ((inverse y - inverse x) * (y - x) * inverse x) / norm (y - x)"
+ by (simp add: left_diff_distrib norm_minus_commute)
+ also have "\<dots> \<le> norm (inverse y - inverse x) * norm (y - x) * norm (inverse x) / norm (y - x)"
+ by (simp add: norm_mult)
+ also have "\<dots> = norm (inverse y - inverse x) * norm (inverse x)"
by simp
- finally show "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) \<le>
- norm (?inv y - ?inv x) * norm (?inv x)" .
+ finally show "norm (inverse y - inverse x - ?f (y -x)) / norm (y - x) \<le>
+ norm (inverse y - inverse x) * norm (inverse x)" .
qed
lemma has_derivative_inverse[simp, derivative_intros]:
fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
assumes x: "f x \<noteq> 0"
- and f: "(f has_derivative f') (at x within s)"
+ and f: "(f has_derivative f') (at x within S)"
shows "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>h. - (inverse (f x) * f' h * inverse (f x))))
- (at x within s)"
+ (at x within S)"
using has_derivative_compose[OF f has_derivative_inverse', OF x] .
lemma has_derivative_divide[simp, derivative_intros]:
fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
- assumes f: "(f has_derivative f') (at x within s)"
- and g: "(g has_derivative g') (at x within s)"
+ assumes f: "(f has_derivative f') (at x within S)"
+ and g: "(g has_derivative g') (at x within S)"
assumes x: "g x \<noteq> 0"
shows "((\<lambda>x. f x / g x) has_derivative
- (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within s)"
+ (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within S)"
using has_derivative_mult[OF f has_derivative_inverse[OF x g]]
by (simp add: field_simps)
@@ -507,10 +493,10 @@
lemma has_derivative_divide'[derivative_intros]:
fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
- assumes f: "(f has_derivative f') (at x within s)"
- and g: "(g has_derivative g') (at x within s)"
+ assumes f: "(f has_derivative f') (at x within S)"
+ and g: "(g has_derivative g') (at x within S)"
and x: "g x \<noteq> 0"
- shows "((\<lambda>x. f x / g x) has_derivative (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))) (at x within s)"
+ shows "((\<lambda>x. f x / g x) has_derivative (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))) (at x within S)"
proof -
have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
(f' h * g x - f x * g' h) / (g x * g x)" for h
@@ -550,12 +536,12 @@
by (auto simp add: F.zero)
with ** have "0 < ?r h"
by simp
- from LIM_D [OF * this] obtain s
- where s: "0 < s" and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h"
+ from LIM_D [OF * this] obtain S
+ where S: "0 < S" and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < S \<Longrightarrow> ?r x < ?r h"
by auto
- from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
+ from dense [OF S] obtain t where t: "0 < t \<and> t < S" ..
let ?x = "scaleR (t / norm h) h"
- have "?x \<noteq> 0" and "norm ?x < s"
+ have "?x \<noteq> 0" and "norm ?x < S"
using t h by simp_all
then have "?r ?x < ?r h"
by (rule r)
@@ -711,12 +697,15 @@
lemma has_field_derivative_iff:
"(f has_field_derivative D) (at x within S) \<longleftrightarrow>
((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)"
- apply (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right
- LIM_zero_iff[symmetric, of _ D])
- apply (subst (2) tendsto_norm_zero_iff[symmetric])
- apply (rule filterlim_cong)
- apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
- done
+proof -
+ have "((\<lambda>y. norm (f y - f x - D * (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within S)
+ = ((\<lambda>y. (f y - f x) / (y - x) - D) \<longlongrightarrow> 0) (at x within S)"
+ apply (subst tendsto_norm_zero_iff[symmetric], rule filterlim_cong)
+ apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
+ done
+ then show ?thesis
+ by (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right LIM_zero_iff)
+qed
lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
@@ -773,10 +762,8 @@
lemma has_vector_derivative_add_const:
"((\<lambda>t. g t + z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net"
apply (intro iffI)
- apply (drule has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const])
- apply simp
- apply (drule has_vector_derivative_add [OF _ has_vector_derivative_const])
- apply simp
+ apply (force dest: has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const])
+ apply (force dest: has_vector_derivative_add [OF _ has_vector_derivative_const])
done
lemma has_vector_derivative_diff_const:
@@ -1027,37 +1014,43 @@
lemma DERIV_LIM_iff:
fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a"
- shows "((\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0\<rightarrow> D) = ((\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D)"
- apply (rule iffI)
- apply (drule_tac k="- a" in LIM_offset)
- apply simp
- apply (drule_tac k="a" in LIM_offset)
- apply (simp add: add.commute)
- done
-
-lemmas DERIV_iff2 = has_field_derivative_iff
+ shows "((\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0\<rightarrow> D) = ((\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D)" (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>0 - - a\<rightarrow> D"
+ by (rule LIM_offset)
+ then show ?rhs
+ by simp
+next
+ assume ?rhs
+ then have "(\<lambda>x. (f (x+a) - f a) / ((x+a) - a)) \<midarrow>a-a\<rightarrow> D"
+ by (rule LIM_offset)
+ then show ?lhs
+ by (simp add: add.commute)
+qed
lemma has_field_derivative_cong_ev:
assumes "x = y"
- and *: "eventually (\<lambda>x. x \<in> s \<longrightarrow> f x = g x) (nhds x)"
- and "u = v" "s = t" "x \<in> s"
- shows "(f has_field_derivative u) (at x within s) = (g has_field_derivative v) (at y within t)"
- unfolding DERIV_iff2
+ and *: "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x = g x) (nhds x)"
+ and "u = v" "S = t" "x \<in> S"
+ shows "(f has_field_derivative u) (at x within S) = (g has_field_derivative v) (at y within t)"
+ unfolding has_field_derivative_iff
proof (rule filterlim_cong)
from assms have "f y = g y"
by (auto simp: eventually_nhds)
- with * show "\<forall>\<^sub>F xa in at x within s. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)"
+ with * show "\<forall>\<^sub>F z in at x within S. (f z - f x) / (z - x) = (g z - g y) / (z - y)"
unfolding eventually_at_filter
by eventually_elim (auto simp: assms \<open>f y = g y\<close>)
qed (simp_all add: assms)
lemma has_field_derivative_cong_eventually:
- assumes "eventually (\<lambda>x. f x = g x) (at x within s)" "f x=g x"
- shows "(f has_field_derivative u) (at x within s) = (g has_field_derivative u) (at x within s)"
- unfolding DERIV_iff2
- apply (rule tendsto_cong)
- apply (insert assms)
- by (auto elim: eventually_mono)
+ assumes "eventually (\<lambda>x. f x = g x) (at x within S)" "f x = g x"
+ shows "(f has_field_derivative u) (at x within S) = (g has_field_derivative u) (at x within S)"
+ unfolding has_field_derivative_iff
+proof (rule tendsto_cong)
+ show "\<forall>\<^sub>F y in at x within S. (f y - f x) / (y - x) = (g y - g x) / (y - x)"
+ using assms by (auto elim: eventually_mono)
+qed
lemma DERIV_cong_ev:
"x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
@@ -1265,22 +1258,24 @@
subsection \<open>Rolle's Theorem\<close>
text \<open>Lemma about introducing open ball in open interval\<close>
-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)"
- for a b x :: real
- apply (simp add: abs_less_iff)
- apply (insert linorder_linear [of "x - a" "b - x"])
- apply safe
- apply (rule_tac x = "x - a" in exI)
- apply (rule_tac [2] x = "b - x" in exI)
- apply auto
- done
+lemma lemma_interval_lt:
+ fixes a b x :: real
+ assumes "a < x" "x < b"
+ shows "\<exists>d. 0 < d \<and> (\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a < y \<and> y < b)"
+ using linorder_linear [of "x - a" "b - x"]
+proof
+ assume "x - a \<le> b - x"
+ with assms show ?thesis
+ by (rule_tac x = "x - a" in exI) auto
+next
+ assume "b - x \<le> x - a"
+ with assms show ?thesis
+ by (rule_tac x = "b - x" in exI) auto
+qed
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)"
for a b x :: real
- apply (drule lemma_interval_lt)
- apply auto
- apply force
- done
+ by (force dest: lemma_interval_lt)
text \<open>Rolle's Theorem.
If @{term f} is defined and continuous on the closed interval
@@ -1409,14 +1404,23 @@
qed
qed
-lemma MVT2:
- "a < b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> DERIV f x :> f' x \<Longrightarrow>
- \<exists>z::real. a < z \<and> z < b \<and> (f b - f a = (b - a) * f' z)"
- apply (drule MVT)
- apply (blast intro: DERIV_isCont)
- apply (force dest: order_less_imp_le simp add: real_differentiable_def)
- apply (blast dest: DERIV_unique order_less_imp_le)
- done
+corollary MVT2:
+ assumes "a < b" and der: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> DERIV f x :> f' x"
+ shows "\<exists>z::real. a < z \<and> z < b \<and> (f b - f a = (b - a) * f' z)"
+proof -
+ have "\<exists>l z. a < z \<and>
+ z < b \<and>
+ (f has_real_derivative l) (at z) \<and>
+ f b - f a = (b - a) * l"
+ proof (rule MVT [OF \<open>a < b\<close>])
+ show "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
+ using assms by (blast intro: DERIV_isCont)
+ show "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable at x"
+ using assms by (force dest: order_less_imp_le simp add: real_differentiable_def)
+ qed
+ with assms show ?thesis
+ by (blast dest: DERIV_unique order_less_imp_le)
+qed
lemma pos_deriv_imp_strict_mono:
assumes "\<And>x. (f has_real_derivative f' x) (at x)"
@@ -1698,7 +1702,7 @@
and inj: "\<And>y. \<lbrakk>a < y; y < b\<rbrakk> \<Longrightarrow> f (g y) = y"
and cont: "isCont g x"
shows "DERIV g x :> inverse D"
-unfolding DERIV_iff2
+unfolding has_field_derivative_iff
proof (rule LIM_equal2)
show "0 < min (x - a) (b - x)"
using x by arith
@@ -1711,7 +1715,7 @@
by (simp add: inj)
next
have "(\<lambda>z. (f z - f (g x)) / (z - g x)) \<midarrow>g x\<rightarrow> D"
- by (rule der [unfolded DERIV_iff2])
+ by (rule der [unfolded has_field_derivative_iff])
then have 1: "(\<lambda>z. (f z - x) / (z - g x)) \<midarrow>g x\<rightarrow> D"
using inj x by simp
have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x"
--- a/src/HOL/Divides.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Divides.thy Sun Jul 15 18:22:31 2018 +0100
@@ -228,15 +228,16 @@
lemma zdiv_zminus1_eq_if:
"b \<noteq> (0::int)
- ==> (-a) div b =
- (if a mod b = 0 then - (a div b) else - (a div b) - 1)"
+ \<Longrightarrow> (-a) div b = (if a mod b = 0 then - (a div b) else - (a div b) - 1)"
by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
lemma zmod_zminus1_eq_if:
"(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))"
-apply (case_tac "b = 0", simp)
-apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
-done
+proof (cases "b = 0")
+ case False
+ then show ?thesis
+ by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
+qed auto
lemma zmod_zminus1_not_zero:
fixes k l :: int
@@ -261,101 +262,93 @@
subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
-lemma zdiv_mono1: "[| a \<le> a'; 0 < (b::int) |] ==> a div b \<le> a' div b"
-using mult_div_mod_eq [symmetric, of a b]
-using mult_div_mod_eq [symmetric, of a' b]
-apply -
-apply (rule unique_quotient_lemma)
-apply (erule subst)
-apply (erule subst, simp_all)
-done
+lemma zdiv_mono1:
+ fixes b::int
+ assumes "a \<le> a'" "0 < b" shows "a div b \<le> a' div b"
+proof (rule unique_quotient_lemma)
+ show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b"
+ using assms(1) by auto
+qed (use assms in auto)
-lemma zdiv_mono1_neg: "[| a \<le> a'; (b::int) < 0 |] ==> a' div b \<le> a div b"
-using mult_div_mod_eq [symmetric, of a b]
-using mult_div_mod_eq [symmetric, of a' b]
-apply -
-apply (rule unique_quotient_lemma_neg)
-apply (erule subst)
-apply (erule subst, simp_all)
-done
+lemma zdiv_mono1_neg:
+ fixes b::int
+ assumes "a \<le> a'" "b < 0" shows "a' div b \<le> a div b"
+proof (rule unique_quotient_lemma_neg)
+ show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b"
+ using assms(1) by auto
+qed (use assms in auto)
subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
lemma q_pos_lemma:
- "[| 0 \<le> b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \<le> (q'::int)"
-apply (subgoal_tac "0 < b'* (q' + 1) ")
- apply (simp add: zero_less_mult_iff)
-apply (simp add: distrib_left)
-done
+ fixes q'::int
+ assumes "0 \<le> b'*q' + r'" "r' < b'" "0 < b'"
+ shows "0 \<le> q'"
+proof -
+ have "0 < b'* (q' + 1)"
+ using assms by (simp add: distrib_left)
+ with assms show ?thesis
+ by (simp add: zero_less_mult_iff)
+qed
lemma zdiv_mono2_lemma:
- "[| b*q + r = b'*q' + r'; 0 \<le> b'*q' + r';
- r' < b'; 0 \<le> r; 0 < b'; b' \<le> b |]
- ==> q \<le> (q'::int)"
-apply (frule q_pos_lemma, assumption+)
-apply (subgoal_tac "b*q < b* (q' + 1) ")
- apply (simp add: mult_less_cancel_left)
-apply (subgoal_tac "b*q = r' - r + b'*q'")
- prefer 2 apply simp
-apply (simp (no_asm_simp) add: distrib_left)
-apply (subst add.commute, rule add_less_le_mono, arith)
-apply (rule mult_right_mono, auto)
-done
+ fixes q'::int
+ assumes eq: "b*q + r = b'*q' + r'" and le: "0 \<le> b'*q' + r'" and "r' < b'" "0 \<le> r" "0 < b'" "b' \<le> b"
+ shows "q \<le> q'"
+proof -
+ have "0 \<le> q'"
+ using q_pos_lemma le \<open>r' < b'\<close> \<open>0 < b'\<close> by blast
+ moreover have "b*q = r' - r + b'*q'"
+ using eq by linarith
+ ultimately have "b*q < b* (q' + 1)"
+ using mult_right_mono assms unfolding distrib_left by fastforce
+ with assms show ?thesis
+ by (simp add: mult_less_cancel_left_pos)
+qed
lemma zdiv_mono2:
- "[| (0::int) \<le> a; 0 < b'; b' \<le> b |] ==> a div b \<le> a div b'"
-apply (subgoal_tac "b \<noteq> 0")
- prefer 2 apply arith
-using mult_div_mod_eq [symmetric, of a b]
-using mult_div_mod_eq [symmetric, of a b']
-apply -
-apply (rule zdiv_mono2_lemma)
-apply (erule subst)
-apply (erule subst, simp_all)
-done
-
-lemma q_neg_lemma:
- "[| b'*q' + r' < 0; 0 \<le> r'; 0 < b' |] ==> q' \<le> (0::int)"
-apply (subgoal_tac "b'*q' < 0")
- apply (simp add: mult_less_0_iff, arith)
-done
+ fixes a::int
+ assumes "0 \<le> a" "0 < b'" "b' \<le> b" shows "a div b \<le> a div b'"
+proof (rule zdiv_mono2_lemma)
+ have "b \<noteq> 0"
+ using assms by linarith
+ show "b * (a div b) + a mod b = b' * (a div b') + a mod b'"
+ by simp
+qed (use assms in auto)
lemma zdiv_mono2_neg_lemma:
- "[| b*q + r = b'*q' + r'; b'*q' + r' < 0;
- r < b; 0 \<le> r'; 0 < b'; b' \<le> b |]
- ==> q' \<le> (q::int)"
-apply (frule q_neg_lemma, assumption+)
-apply (subgoal_tac "b*q' < b* (q + 1) ")
- apply (simp add: mult_less_cancel_left)
-apply (simp add: distrib_left)
-apply (subgoal_tac "b*q' \<le> b'*q'")
- prefer 2 apply (simp add: mult_right_mono_neg, arith)
-done
+ fixes q'::int
+ assumes "b*q + r = b'*q' + r'" "b'*q' + r' < 0" "r < b" "0 \<le> r'" "0 < b'" "b' \<le> b"
+ shows "q' \<le> q"
+proof -
+ have "b'*q' < 0"
+ using assms by linarith
+ with assms have "q' \<le> 0"
+ by (simp add: mult_less_0_iff)
+ have "b*q' \<le> b'*q'"
+ by (simp add: \<open>q' \<le> 0\<close> assms(6) mult_right_mono_neg)
+ then have "b*q' < b* (q + 1)"
+ using assms by (simp add: distrib_left)
+ then show ?thesis
+ using assms by (simp add: mult_less_cancel_left)
+qed
lemma zdiv_mono2_neg:
- "[| a < (0::int); 0 < b'; b' \<le> b |] ==> a div b' \<le> a div b"
-using mult_div_mod_eq [symmetric, of a b]
-using mult_div_mod_eq [symmetric, of a b']
-apply -
-apply (rule zdiv_mono2_neg_lemma)
-apply (erule subst)
-apply (erule subst, simp_all)
-done
+ fixes a::int
+ assumes "a < 0" "0 < b'" "b' \<le> b" shows "a div b' \<le> a div b"
+proof (rule zdiv_mono2_neg_lemma)
+ have "b \<noteq> 0"
+ using assms by linarith
+ show "b * (a div b) + a mod b = b' * (a div b') + a mod b'"
+ by simp
+qed (use assms in auto)
subsubsection \<open>More Algebraic Laws for div and mod\<close>
-lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
- by (fact div_mult1_eq)
-
-(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
-lemma zdiv_zadd1_eq:
- "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
- by (fact div_add1_eq)
-
lemma zmod_eq_0_iff: "(m mod d = 0) = (\<exists>q::int. m = d*q)"
-by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
+ by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
(* REVISIT: should this be generalized to all semiring_div types? *)
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
@@ -369,40 +362,53 @@
text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
-lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r \<le> 0 |] ==> b * c < b * (q mod c) + r"
-apply (subgoal_tac "b * (c - q mod c) < r * 1")
- apply (simp add: algebra_simps)
-apply (rule order_le_less_trans)
- apply (erule_tac [2] mult_strict_right_mono)
- apply (rule mult_left_mono_neg)
- using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
- apply (simp)
-apply (simp)
-done
+lemma zmult2_lemma_aux1:
+ fixes c::int
+ assumes "0 < c" "b < r" "r \<le> 0"
+ shows "b * c < b * (q mod c) + r"
+proof -
+ have "b * (c - q mod c) \<le> b * 1"
+ by (rule mult_left_mono_neg) (use assms in \<open>auto simp: int_one_le_iff_zero_less\<close>)
+ also have "... < r * 1"
+ by (simp add: \<open>b < r\<close>)
+ finally show ?thesis
+ by (simp add: algebra_simps)
+qed
lemma zmult2_lemma_aux2:
- "[| (0::int) < c; b < r; r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
-apply (subgoal_tac "b * (q mod c) \<le> 0")
- apply arith
-apply (simp add: mult_le_0_iff)
-done
+ fixes c::int
+ assumes "0 < c" "b < r" "r \<le> 0"
+ shows "b * (q mod c) + r \<le> 0"
+proof -
+ have "b * (q mod c) \<le> 0"
+ using assms by (simp add: mult_le_0_iff)
+ with assms show ?thesis
+ by arith
+qed
-lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 \<le> r; r < b |] ==> 0 \<le> b * (q mod c) + r"
-apply (subgoal_tac "0 \<le> b * (q mod c) ")
-apply arith
-apply (simp add: zero_le_mult_iff)
-done
+lemma zmult2_lemma_aux3:
+ fixes c::int
+ assumes "0 < c" "0 \<le> r" "r < b"
+ shows "0 \<le> b * (q mod c) + r"
+proof -
+ have "0 \<le> b * (q mod c)"
+ using assms by (simp add: mult_le_0_iff)
+ with assms show ?thesis
+ by arith
+qed
-lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
-apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
- apply (simp add: right_diff_distrib)
-apply (rule order_less_le_trans)
- apply (erule mult_strict_right_mono)
- apply (rule_tac [2] mult_left_mono)
- apply simp
- using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
-apply simp
-done
+lemma zmult2_lemma_aux4:
+ fixes c::int
+ assumes "0 < c" "0 \<le> r" "r < b"
+ shows "b * (q mod c) + r < b * c"
+proof -
+ have "r * 1 < b * 1"
+ by (simp add: \<open>r < b\<close>)
+ also have "\<dots> \<le> b * (c - q mod c) "
+ by (rule mult_left_mono) (use assms in \<open>auto simp: int_one_le_iff_zero_less\<close>)
+ finally show ?thesis
+ by (simp add: algebra_simps)
+qed
lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
@@ -412,17 +418,23 @@
lemma zdiv_zmult2_eq:
fixes a b c :: int
- shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
-apply (case_tac "b = 0", simp)
-apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
-done
+ assumes "0 \<le> c"
+ shows "a div (b * c) = (a div b) div c"
+proof (cases "b = 0")
+ case False
+ with assms show ?thesis
+ by (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
+qed auto
lemma zmod_zmult2_eq:
fixes a b c :: int
- shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
-apply (case_tac "b = 0", simp)
-apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
-done
+ assumes "0 \<le> c"
+ shows "a mod (b * c) = b * (a div b mod c) + a mod b"
+proof (cases "b = 0")
+ case False
+ with assms show ?thesis
+ by (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
+qed auto
lemma div_pos_geq:
fixes k l :: int
@@ -464,24 +476,24 @@
((k = 0 \<longrightarrow> P 0) \<and>
(0<k \<longrightarrow> (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P i)) \<and>
(k<0 \<longrightarrow> (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P i)))"
- apply (cases "k = 0")
- apply simp
-apply (simp only: linorder_neq_iff)
- apply (auto simp add: split_pos_lemma [of concl: "%x y. P x"]
- split_neg_lemma [of concl: "%x y. P x"])
-done
+proof (cases "k = 0")
+ case False
+ then show ?thesis
+ unfolding linorder_neq_iff
+ by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P x"] split_neg_lemma [of concl: "\<lambda>x y. P x"])
+qed auto
lemma split_zmod:
"P(n mod k :: int) =
((k = 0 \<longrightarrow> P n) \<and>
(0<k \<longrightarrow> (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P j)) \<and>
(k<0 \<longrightarrow> (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P j)))"
-apply (case_tac "k=0", simp)
-apply (simp only: linorder_neq_iff)
-apply (erule disjE)
- apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
- split_neg_lemma [of concl: "%x y. P y"])
-done
+proof (cases "k = 0")
+ case False
+ then show ?thesis
+ unfolding linorder_neq_iff
+ by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P y"] split_neg_lemma [of concl: "\<lambda>x y. P y"])
+qed auto
text \<open>Enable (lin)arith to deal with @{const divide} and @{const modulo}
when these are applied to some constant that is of the form
@@ -515,7 +527,6 @@
using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
by (rule div_int_unique)
-(* FIXME: add rules for negative numerals *)
lemma zdiv_numeral_Bit0 [simp]:
"numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
numeral v div (numeral w :: int)"
@@ -543,7 +554,6 @@
using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
by (rule mod_int_unique)
-(* FIXME: add rules for negative numerals *)
lemma zmod_numeral_Bit0 [simp]:
"numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
(2::int) * (numeral v mod numeral w)"
@@ -591,68 +601,81 @@
lemma zmod_minus1: "0 < b \<Longrightarrow> - 1 mod b = b - 1" for b :: int
by (auto simp add: modulo_int_def)
-lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0"
-apply (subgoal_tac "a div b \<le> -1", force)
-apply (rule order_trans)
-apply (rule_tac a' = "-1" in zdiv_mono1)
-apply (auto simp add: div_eq_minus1)
-done
+lemma div_neg_pos_less0:
+ fixes a::int
+ assumes "a < 0" "0 < b"
+ shows "a div b < 0"
+proof -
+ have "a div b \<le> - 1 div b"
+ using Divides.zdiv_mono1 assms by auto
+ also have "... \<le> -1"
+ by (simp add: assms(2) div_eq_minus1)
+ finally show ?thesis
+ by force
+qed
lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
-by (drule zdiv_mono1_neg, auto)
+ by (drule zdiv_mono1_neg, auto)
lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
-by (drule zdiv_mono1, auto)
+ by (drule zdiv_mono1, auto)
text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
They should all be simp rules unless that causes too much search.\<close>
-lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
-apply auto
-apply (drule_tac [2] zdiv_mono1)
-apply (auto simp add: linorder_neq_iff)
-apply (simp (no_asm_use) add: linorder_not_less [symmetric])
-apply (blast intro: div_neg_pos_less0)
-done
+lemma pos_imp_zdiv_nonneg_iff:
+ fixes a::int
+ assumes "0 < b"
+ shows "(0 \<le> a div b) = (0 \<le> a)"
+proof
+ show "0 \<le> a div b \<Longrightarrow> 0 \<le> a"
+ using assms
+ by (simp add: linorder_not_less [symmetric]) (blast intro: div_neg_pos_less0)
+next
+ assume "0 \<le> a"
+ then have "0 div b \<le> a div b"
+ using zdiv_mono1 assms by blast
+ then show "0 \<le> a div b"
+ by auto
+qed
lemma pos_imp_zdiv_pos_iff:
"0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
-using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
-by arith
+ using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k] by arith
+
lemma neg_imp_zdiv_nonneg_iff:
- "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
-apply (subst div_minus_minus [symmetric])
-apply (subst pos_imp_zdiv_nonneg_iff, auto)
-done
+ fixes a::int
+ assumes "b < 0"
+ shows "(0 \<le> a div b) = (a \<le> 0)"
+ using assms by (simp add: div_minus_minus [of a, symmetric] pos_imp_zdiv_nonneg_iff del: div_minus_minus)
(*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
-by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
+ by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
(*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
-by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
+ by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
lemma nonneg1_imp_zdiv_pos_iff:
- "(0::int) \<le> a \<Longrightarrow> (a div b > 0) = (a \<ge> b \<and> b>0)"
-apply rule
- apply rule
- using div_pos_pos_trivial[of a b]apply arith
- apply(cases "b=0")apply simp
- using div_nonneg_neg_le0[of a b]apply arith
-using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
-done
+ fixes a::int
+ assumes "0 \<le> a"
+ shows "a div b > 0 \<longleftrightarrow> a \<ge> b \<and> b>0"
+proof -
+ have "0 < a div b \<Longrightarrow> b \<le> a"
+ using div_pos_pos_trivial[of a b] assms by arith
+ moreover have "0 < a div b \<Longrightarrow> b > 0"
+ using assms div_nonneg_neg_le0[of a b] by(cases "b=0"; force)
+ moreover have "b \<le> a \<and> 0 < b \<Longrightarrow> 0 < a div b"
+ using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b] by simp
+ ultimately show ?thesis
+ by blast
+qed
-lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
-apply (rule split_zmod[THEN iffD2])
-apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
-done
-
-
-subsubsection \<open>Computation of Division and Remainder\<close>
-
+lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 \<Longrightarrow> m mod k \<le> m"
+ by (rule split_zmod[THEN iffD2]) (fastforce dest: q_pos_lemma intro: split_mult_pos_le)
subsubsection \<open>Further properties\<close>
@@ -661,21 +684,23 @@
"k div l \<ge> 0 \<longleftrightarrow> k = 0 \<or> l = 0 \<or> k \<ge> 0 \<and> l \<ge> 0
\<or> k < 0 \<and> l < 0"
for k l :: int
- apply (cases "k = 0 \<or> l = 0")
+proof (cases "k = 0 \<or> l = 0")
+ case False
+ then show ?thesis
apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
- apply (rule ccontr)
- apply (simp add: neg_imp_zdiv_nonneg_iff)
- done
+ by (meson neg_imp_zdiv_neg_iff not_le not_less_iff_gr_or_eq)
+qed auto
lemma mod_int_pos_iff:
"k mod l \<ge> 0 \<longleftrightarrow> l dvd k \<or> l = 0 \<and> k \<ge> 0 \<or> l > 0"
for k l :: int
- apply (cases "l > 0")
- apply (simp_all add: dvd_eq_mod_eq_0)
- apply (use neg_mod_conj [of l k] in \<open>auto simp add: le_less not_less\<close>)
- done
+proof (cases "l > 0")
+ case False
+ then show ?thesis
+ by (simp add: dvd_eq_mod_eq_0) (use neg_mod_conj [of l k] in \<open>auto simp add: le_less not_less\<close>)
+qed auto
-text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
+text \<open>Simplify expressions in which div and mod combine numerical constants\<close>
lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
@@ -693,39 +718,56 @@
simp add: eucl_rel_int_iff)
lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
-by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
+ unfolding dvd_def by (cases "y=0") (auto simp add: abs_mult)
text\<open>Suggested by Matthias Daum\<close>
lemma int_power_div_base:
- "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
-apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
- apply (erule ssubst)
- apply (simp only: power_add)
- apply simp_all
-done
+ fixes k :: int
+ assumes "0 < m" "0 < k"
+ shows "k ^ m div k = (k::int) ^ (m - Suc 0)"
+proof -
+ have eq: "k ^ m = k ^ ((m - Suc 0) + Suc 0)"
+ by (simp add: assms)
+ show ?thesis
+ using assms by (simp only: power_add eq) auto
+qed
text \<open>Distributive laws for function \<open>nat\<close>.\<close>
-lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
-apply (rule linorder_cases [of y 0])
-apply (simp add: div_nonneg_neg_le0)
-apply simp
-apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
-done
+lemma nat_div_distrib:
+ assumes "0 \<le> x"
+ shows "nat (x div y) = nat x div nat y"
+proof (cases y "0::int" rule: linorder_cases)
+ case less
+ with assms show ?thesis
+ using div_nonneg_neg_le0 by auto
+next
+ case greater
+ then show ?thesis
+ by (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
+qed auto
(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
lemma nat_mod_distrib:
- "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
-apply (case_tac "y = 0", simp)
-apply (simp add: nat_eq_iff zmod_int)
-done
+ assumes "0 \<le> x" "0 \<le> y"
+ shows "nat (x mod y) = nat x mod nat y"
+proof (cases "y = 0")
+ case False
+ with assms show ?thesis
+ by (simp add: nat_eq_iff zmod_int)
+qed auto
text\<open>Suggested by Matthias Daum\<close>
-lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
-apply (subgoal_tac "nat x div nat k < nat x")
- apply (simp add: nat_div_distrib [symmetric])
-apply (rule div_less_dividend, simp_all)
-done
+lemma int_div_less_self:
+ fixes x::int
+ assumes "0 < x" "1 < k"
+ shows "x div k < x"
+proof -
+ have "nat x div nat k < nat x"
+ by (simp add: assms)
+ with assms show ?thesis
+ by (simp add: nat_div_distrib [symmetric])
+qed
lemma mod_eq_dvd_iff_nat:
"m mod q = n mod q \<longleftrightarrow> q dvd m - n" if "m \<ge> n" for m n q :: nat
@@ -1290,16 +1332,13 @@
subsection \<open>Lemmas of doubtful value\<close>
-lemma div_geq:
- "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
+lemma div_geq: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
-lemma mod_geq:
- "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
+lemma mod_geq: "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
-lemma mod_eq_0D:
- "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
- using that by (auto simp add: mod_eq_0_iff_dvd elim: dvdE)
+lemma mod_eq_0D: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
+ using that by (auto simp add: mod_eq_0_iff_dvd)
end
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun Jul 15 18:22:31 2018 +0100
@@ -370,7 +370,7 @@
moreover from x have "(int p - 1) div 2 \<le> - 1 + x mod p"
by (auto simp: BuDuF_def)
moreover have "int p * (int q - 1) div 2 = int p * ((int q - 1) div 2)"
- using zdiv_zmult1_eq odd_q by auto
+ by (subst div_mult1_eq) (simp add: odd_q)
then have "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)"
by fastforce
ultimately have "x \<le> p * ((int q + 1) div 2 - 1) - 1 + x mod p"
@@ -409,7 +409,7 @@
then have "snd x \<le> (int q - 1) div 2"
by force
moreover have "int p * ((int q - 1) div 2) = (int p * int q - int p) div 2"
- using int_distrib(4) zdiv_zmult1_eq[of "int p" "int q - 1" 2] odd_q by fastforce
+ using int_distrib(4) div_mult1_eq[of "int p" "int q - 1" 2] odd_q by fastforce
ultimately have "(snd x) * int p \<le> (int q * int p - int p) div 2"
using mult_right_mono[of "snd x" "(int q - 1) div 2" p] mult.commute[of "(int q - 1) div 2" p]
pq_commute
--- a/src/HOL/Tools/Qelim/cooper.ML Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Jul 15 18:22:31 2018 +0100
@@ -9,7 +9,7 @@
type entry
val get: Proof.context -> entry
val del: term list -> attribute
- val add: term list -> attribute
+ val add: term list -> attribute
exception COOPER of string
val conv: Proof.context -> conv
val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
@@ -20,13 +20,13 @@
type entry = simpset * term list;
-val allowed_consts =
+val allowed_consts =
[@{term "(+) :: int => _"}, @{term "(+) :: nat => _"},
@{term "(-) :: int => _"}, @{term "(-) :: nat => _"},
@{term "( * ) :: int => _"}, @{term "( * ) :: nat => _"},
@{term "(div) :: int => _"}, @{term "(div) :: nat => _"},
@{term "(mod) :: int => _"}, @{term "(mod) :: nat => _"},
- @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies},
+ @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies},
@{term "(=) :: int => _"}, @{term "(=) :: nat => _"}, @{term "(=) :: bool => _"},
@{term "(<) :: int => _"}, @{term "(<) :: nat => _"},
@{term "(<=) :: int => _"}, @{term "(<=) :: nat => _"},
@@ -55,12 +55,12 @@
val get = Data.get o Context.Proof;
-fun add ts = Thm.declaration_attribute (fn th => fn context =>
+fun add ts = Thm.declaration_attribute (fn th => fn context =>
context |> Data.map (fn (ss, ts') =>
(simpset_map (Context.proof_of context) (fn ctxt => ctxt addsimps [th]) ss,
merge (op aconv) (ts', ts))))
-fun del ts = Thm.declaration_attribute (fn th => fn context =>
+fun del ts = Thm.declaration_attribute (fn th => fn context =>
context |> Data.map (fn (ss, ts') =>
(simpset_map (Context.proof_of context) (fn ctxt => ctxt delsimps [th]) ss,
subtract (op aconv) ts' ts)))
@@ -709,9 +709,9 @@
in A :: strip_objimp B end
| _ => [ct]);
-fun strip_objall ct =
- case Thm.term_of ct of
- Const (@{const_name All}, _) $ Abs (xn,_,_) =>
+fun strip_objall ct =
+ case Thm.term_of ct of
+ Const (@{const_name All}, _) $ Abs (xn,_,_) =>
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
in apfst (cons (a,v)) (strip_objall t')
end
@@ -730,12 +730,12 @@
val (ps, c) = split_last (strip_objimp p)
val qs = filter P ps
val q = if P c then c else @{cterm "False"}
- val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs
+ val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs
(fold_rev (fn p => fn q => Thm.apply (Thm.apply @{cterm HOL.implies} p) q) qs q)
val g = Thm.apply (Thm.apply @{cterm "(==>)"} (Thm.apply @{cterm "Trueprop"} ng)) p'
val ntac = (case qs of [] => q aconvc @{cterm "False"}
| _ => false)
- in
+ in
if ntac then no_tac
else
(case try (fn () =>
@@ -746,7 +746,7 @@
end;
local
- fun isnum t = case t of
+ fun isnum t = case t of
Const(@{const_name Groups.zero},_) => true
| Const(@{const_name Groups.one},_) => true
| @{term Suc}$s => isnum s
@@ -761,10 +761,10 @@
| Const(@{const_name Rings.divide},_)$l$r => isnum l andalso isnum r
| _ => is_number t orelse can HOLogic.dest_nat t
- fun ty cts t =
+ fun ty cts t =
if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t))
- then false
- else case Thm.term_of t of
+ then false
+ else case Thm.term_of t of
c$l$r => if member (op =) [@{term"( * )::int => _"}, @{term"( * )::nat => _"}] c
then not (isnum l orelse isnum r)
else not (member (op aconv) cts c)
@@ -778,8 +778,8 @@
| Abs (_,_,t) => h acc t
| _ => acc
in h [] end;
-in
-fun is_relevant ctxt ct =
+in
+fun is_relevant ctxt ct =
subset (op aconv) (term_constants (Thm.term_of ct), snd (get ctxt))
andalso
forall (fn Free (_, T) => member (op =) [@{typ int}, @{typ nat}] T)
@@ -789,7 +789,7 @@
(Misc_Legacy.term_vars (Thm.term_of ct));
fun int_nat_terms ctxt ct =
- let
+ let
val cts = snd (get ctxt)
fun h acc t = if ty cts t then insert (op aconvc) t acc else
case Thm.term_of t of
@@ -800,7 +800,7 @@
end;
fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
- let
+ let
fun all x t =
Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
val ts = sort Thm.fast_term_ord (f p)
@@ -810,22 +810,22 @@
local
val ss1 =
simpset_of (put_simpset comp_ss @{context}
- addsimps @{thms simp_thms} @
- [@{thm "nat_numeral"} RS sym, @{thm int_dvd_int_iff [symmetric]}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}]
+ addsimps @{thms simp_thms} @
+ [@{thm "nat_numeral"} RS sym, @{thm int_dvd_int_iff [symmetric]}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}]
@ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}]
|> Splitter.add_split @{thm "zdiff_int_split"})
val ss2 =
simpset_of (put_simpset HOL_basic_ss @{context}
addsimps [@{thm "nat_0_le"}, @{thm "of_nat_numeral"},
- @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"},
+ @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"},
@{thm "le_numeral_extra"(3)}, @{thm "of_nat_0"}, @{thm "of_nat_1"}, @{thm "Suc_eq_plus1"}]
|> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}])
val div_mod_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
addsimps @{thms simp_thms
mod_eq_0_iff_dvd mod_add_left_eq mod_add_right_eq
- mod_add_eq div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
+ mod_add_eq div_add1_eq [symmetric] div_add1_eq [symmetric]
mod_self mod_by_0 div_by_0
div_0 mod_0 div_by_1 mod_by_1
div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1
@@ -835,11 +835,11 @@
simpset_of (put_simpset comp_ss @{context}
addsimps [@{thm minus_div_mult_eq_mod [symmetric]}]
|> fold Splitter.add_split
- [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
+ [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
in
-fun nat_to_int_tac ctxt =
+fun nat_to_int_tac ctxt =
simp_tac (put_simpset ss1 ctxt) THEN_ALL_NEW
simp_tac (put_simpset ss2 ctxt) THEN_ALL_NEW
simp_tac (put_simpset comp_ss ctxt);
@@ -851,7 +851,7 @@
fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
let
- val cpth =
+ val cpth =
if Config.get ctxt quick_and_dirty
then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (Thm.term_of (Thm.dest_arg p))))
else Conv.arg_conv (conv ctxt) p
--- a/src/HOL/Transcendental.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/Transcendental.thy Sun Jul 15 18:22:31 2018 +0100
@@ -2303,7 +2303,7 @@
have "((\<lambda>z::'a. exp(z) - 1) has_field_derivative 1) (at 0)"
by (intro derivative_eq_intros | simp)+
then show ?thesis
- by (simp add: Deriv.DERIV_iff2)
+ by (simp add: Deriv.has_field_derivative_iff)
qed
lemma ln_at_0: "LIM x at_right 0. ln (x::real) :> at_bot"
@@ -4165,7 +4165,7 @@
shows "cos x < cos y"
proof -
have "- (x - y) < 0" using assms by auto
- from MVT2[OF \<open>y < x\<close> DERIV_cos[THEN impI, THEN allI]]
+ from MVT2[OF \<open>y < x\<close> DERIV_cos]
obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
by auto
then have "0 < z" and "z < pi"
@@ -4677,14 +4677,11 @@
assumes "- (pi/2) < y" and "y < x" and "x < pi/2"
shows "tan y < tan x"
proof -
- have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
- proof (rule allI, rule impI)
- fix x' :: real
- assume "y \<le> x' \<and> x' \<le> x"
- then have "-(pi/2) < x'" and "x' < pi/2"
- using assms by auto
- from cos_gt_zero_pi[OF this]
- have "cos x' \<noteq> 0" by auto
+ have "DERIV tan x' :> inverse ((cos x')\<^sup>2)" if "y \<le> x'" "x' \<le> x" for x'
+ proof -
+ have "-(pi/2) < x'" and "x' < pi/2"
+ using that assms by auto
+ with cos_gt_zero_pi have "cos x' \<noteq> 0" by force
then show "DERIV tan x' :> inverse ((cos x')\<^sup>2)"
by (rule DERIV_tan)
qed
--- a/src/HOL/ex/Gauge_Integration.thy Sun Jul 15 14:46:57 2018 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Sun Jul 15 18:22:31 2018 +0100
@@ -540,7 +540,7 @@
fix x :: real assume "a \<le> x" and "x \<le> b"
with f' have "DERIV f x :> f'(x)" by simp
then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
- by (simp add: DERIV_iff2 LIM_eq)
+ by (simp add: has_field_derivative_iff LIM_eq)
with \<open>0 < e\<close> obtain s
where "z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s" for z
by (drule_tac x="e/2" in spec, auto)