--- a/NEWS Thu Apr 03 21:55:48 2014 +0200
+++ b/NEWS Thu Apr 03 22:04:57 2014 +0200
@@ -534,6 +534,13 @@
- Renamed FDERIV_... lemmas to has_derivative_...
+ - renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV
+
+ - removed DERIV_intros, has_derivative_eq_intros
+
+ - introduced derivative_intros and deriative_eq_intros which includes now rules for
+ DERIV, has_derivative and has_vector_derivative.
+
- Other renamings:
differentiable_def ~> real_differentiable_def
differentiableE ~> real_differentiableE
@@ -541,6 +548,7 @@
field_fderiv_def ~> field_has_derivative_at
isDiff_der ~> differentiable_def
deriv_fderiv ~> has_field_derivative_def
+ deriv_def ~> DERIV_def
INCOMPATIBILITY.
* Include more theorems in continuous_intros. Remove the continuous_on_intros,
--- a/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 21:55:48 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 22:04:57 2014 +0200
@@ -199,7 +199,7 @@
for Alt-Ergo, set the
environment variable \texttt{WHY3\_HOME} to the directory that contains the
\texttt{why3} executable.
-Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.1, E 1.0 to 1.8,
+Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.0 to 1.8,
LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.%
\footnote{Following the rewrite of Vampire, the counter for version numbers was
reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
@@ -208,7 +208,7 @@
versions might not work well with Sledgehammer. Ideally,
you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.8'').
+\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0'').
Similarly, if you want to build CVC3, or found a
Yices or Z3 executable somewhere (e.g.,
@@ -823,9 +823,8 @@
ATP developed by Bobot et al.\ \cite{alt-ergo}.
It supports the TPTP polymorphic typed first-order format (TFF1) via Why3
\cite{why3}. To use Alt-Ergo, set the environment variable \texttt{WHY3\_HOME}
-to the directory that contains the \texttt{why3} executable. Sledgehammer has
-been tested with Alt-Ergo 0.95.1 and an unidentified development version of
-Why3.
+to the directory that contains the \texttt{why3} executable. Sledgehammer
+requires Alt-Ergo 0.95.2 and Why3 0.83.
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
@@ -898,7 +897,7 @@
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g.,
-``2.6''). Sledgehammer has been tested with versions 0.6 to 3.0.
+``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0.
Versions strictly above 1.8 support the TPTP typed first-order format (TFF0).
\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
@@ -920,12 +919,20 @@
are treated as a different prover by Isabelle. To use these, set the environment
variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable,
including the file name. You also need to set \texttt{Z3\_NON\_COMMERCIAL} to
-``yes'', as described above. Sledgehammer has been tested with versions 4.3.0 and
-4.3.1.
+``yes'', as described above. Sledgehammer has been tested with versions 4.3.0
+and 4.3.1.
\end{enum}
+
+\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
+an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
+formats (FOF and TFF0). It is included for experimental purposes. It requires
+version 4.3.1 of Z3 above. To use it, set the environment variable
+\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp}
+executable.
+
\end{sloppy}
-The following remote provers are supported:
+In addition to the local provers, the following remote provers are supported:
\begin{enum}
\item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
--- a/src/HOL/Complex.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Complex.thy Thu Apr 03 22:04:57 2014 +0200
@@ -374,30 +374,20 @@
lemma bounded_linear_Im: "bounded_linear Im"
by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
-lemmas tendsto_Re [tendsto_intros] =
- bounded_linear.tendsto [OF bounded_linear_Re]
-
-lemmas tendsto_Im [tendsto_intros] =
- bounded_linear.tendsto [OF bounded_linear_Im]
-
-lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
-lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
-
-lemma continuous_Re: "continuous_on X Re"
- by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re
- continuous_on_cong continuous_on_id)
-
-lemma continuous_Im: "continuous_on X Im"
- by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im
- continuous_on_cong continuous_on_id)
-
-lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F"
- by (auto simp add: has_derivative_def bounded_linear_Re tendsto_const)
-
-lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F"
- by (auto simp add: has_derivative_def bounded_linear_Im tendsto_const)
+lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Re]
+lemmas tendsto_Im [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im]
+lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
+lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
+lemmas continuous_Re [simp] = bounded_linear.continuous [OF bounded_linear_Re]
+lemmas continuous_Im [simp] = bounded_linear.continuous [OF bounded_linear_Im]
+lemmas continuous_on_Re [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Re]
+lemmas continuous_on_Im [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im]
+lemmas has_derivative_Re [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Re]
+lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im]
+lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re]
+lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]
lemma tendsto_Complex [tendsto_intros]:
assumes "(f ---> a) F" and "(g ---> b) F"
@@ -445,8 +435,7 @@
qed
declare
- DERIV_power[where 'a=complex, THEN DERIV_cong,
- unfolded of_nat_def[symmetric], DERIV_intros]
+ DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]
subsection {* The Complex Number $i$ *}
@@ -605,11 +594,11 @@
using complex_cnj_add complex_cnj_scaleR
by (rule bounded_linear_intro [where K=1], simp)
-lemmas tendsto_cnj [tendsto_intros] =
- bounded_linear.tendsto [OF bounded_linear_cnj]
-
-lemmas isCont_cnj [simp] =
- bounded_linear.isCont [OF bounded_linear_cnj]
+lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]
+lemmas isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
+lemmas continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]
+lemmas continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj]
+lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]
lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
@@ -704,12 +693,6 @@
lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
-lemma sums_Re: "f sums a \<Longrightarrow> (\<lambda>x. Re (f x)) sums Re a"
- unfolding sums_complex_iff by blast
-
-lemma sums_Im: "f sums a \<Longrightarrow> (\<lambda>x. Im (f x)) sums Im a"
- unfolding sums_complex_iff by blast
-
lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and> summable (\<lambda>x. Im (f x))"
unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps)
@@ -976,5 +959,4 @@
lemmas complex_Re_Im_cancel_iff = complex_eq_iff
lemmas complex_equality = complex_eqI
-
end
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 03 22:04:57 2014 +0200
@@ -2674,24 +2674,24 @@
proof (induct f arbitrary: x)
case (Inverse a)
thus ?case
- by (auto intro!: DERIV_intros simp add: algebra_simps power2_eq_square)
+ by (auto intro!: derivative_eq_intros simp add: algebra_simps power2_eq_square)
next
case (Cos a)
thus ?case
- by (auto intro!: DERIV_intros
+ by (auto intro!: derivative_eq_intros
simp del: interpret_floatarith.simps(5)
simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
next
case (Power a n)
thus ?case
- by (cases n) (auto intro!: DERIV_intros simp del: power_Suc)
+ by (cases n) (auto intro!: derivative_eq_intros simp del: power_Suc simp add: real_of_nat_def)
next
case (Ln a)
- thus ?case by (auto intro!: DERIV_intros simp add: divide_inverse)
+ thus ?case by (auto intro!: derivative_eq_intros simp add: divide_inverse)
next
case (Var i)
thus ?case using `n < length vs` by auto
-qed (auto intro!: DERIV_intros)
+qed (auto intro!: derivative_eq_intros)
declare approx.simps[simp del]
--- a/src/HOL/Deriv.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Deriv.thy Thu Apr 03 22:04:57 2014 +0200
@@ -29,6 +29,48 @@
most cases @{term s} is either a variable or @{term UNIV}.
*}
+lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
+ by simp
+
+definition
+ has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
+ (infix "(has'_field'_derivative)" 50)
+where
+ "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F"
+
+lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F"
+ by simp
+
+definition
+ has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> real filter \<Rightarrow> bool"
+ (infix "has'_vector'_derivative" 50)
+where
+ "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net"
+
+lemma has_vector_derivative_eq_rhs: "(f has_vector_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_vector_derivative Y) F"
+ by simp
+
+ML {*
+
+structure Derivative_Intros = Named_Thms
+(
+ val name = @{binding derivative_intros}
+ val description = "structural introduction rules for derivatives"
+)
+
+*}
+
+setup {*
+ let
+ val eq_thms = [@{thm has_derivative_eq_rhs}, @{thm DERIV_cong}, @{thm has_vector_derivative_eq_rhs}]
+ fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms
+ in
+ Derivative_Intros.setup #>
+ Global_Theory.add_thms_dynamic
+ (@{binding derivative_eq_intros}, map_filter eq_rule o Derivative_Intros.get o Context.proof_of)
+ end;
+*}
+
text {*
The following syntax is only used as a legacy syntax.
*}
@@ -38,36 +80,16 @@
where
"FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)"
-
-lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
- by simp
-
-ML {*
-
-structure has_derivative_Intros = Named_Thms
-(
- val name = @{binding has_derivative_intros}
- val description = "introduction rules for FDERIV"
-)
-
-*}
-
-setup {*
- has_derivative_Intros.setup #>
- Global_Theory.add_thms_dynamic (@{binding has_derivative_eq_intros},
- map_filter (try (fn thm => @{thm has_derivative_eq_rhs} OF [thm])) o has_derivative_Intros.get o Context.proof_of);
-*}
-
lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
by (simp add: has_derivative_def)
lemma has_derivative_linear: "(f has_derivative f') F \<Longrightarrow> linear f'"
using bounded_linear.linear[OF has_derivative_bounded_linear] .
-lemma has_derivative_ident[has_derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
+lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
by (simp add: has_derivative_def tendsto_const)
-lemma has_derivative_const[has_derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
+lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
by (simp add: has_derivative_def tendsto_const)
lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
@@ -81,19 +103,19 @@
apply (simp add: scaleR diff add zero)
done
-lemmas has_derivative_scaleR_right [has_derivative_intros] =
+lemmas has_derivative_scaleR_right [derivative_intros] =
bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
-lemmas has_derivative_scaleR_left [has_derivative_intros] =
+lemmas has_derivative_scaleR_left [derivative_intros] =
bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
-lemmas has_derivative_mult_right [has_derivative_intros] =
+lemmas has_derivative_mult_right [derivative_intros] =
bounded_linear.has_derivative [OF bounded_linear_mult_right]
-lemmas has_derivative_mult_left [has_derivative_intros] =
+lemmas has_derivative_mult_left [derivative_intros] =
bounded_linear.has_derivative [OF bounded_linear_mult_left]
-lemma has_derivative_add[simp, has_derivative_intros]:
+lemma has_derivative_add[simp, derivative_intros]:
assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F"
shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F"
unfolding has_derivative_def
@@ -106,7 +128,7 @@
by (simp add: field_simps scaleR_add_right scaleR_diff_right)
qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear)
-lemma has_derivative_setsum[simp, has_derivative_intros]:
+lemma has_derivative_setsum[simp, derivative_intros]:
assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
proof cases
@@ -114,10 +136,10 @@
by induct (simp_all add: f)
qed simp
-lemma has_derivative_minus[simp, has_derivative_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
+lemma has_derivative_minus[simp, derivative_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
using has_derivative_scaleR_right[of f f' F "-1"] by simp
-lemma has_derivative_diff[simp, has_derivative_intros]:
+lemma has_derivative_diff[simp, derivative_intros]:
"(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F"
by (simp only: diff_conv_add_uminus has_derivative_add has_derivative_minus)
@@ -320,10 +342,10 @@
qed simp
qed
-lemmas has_derivative_mult[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
-lemmas has_derivative_scaleR[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
+lemmas has_derivative_mult[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
+lemmas has_derivative_scaleR[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
-lemma has_derivative_setprod[simp, has_derivative_intros]:
+lemma has_derivative_setprod[simp, derivative_intros]:
fixes f :: "'i \<Rightarrow> 'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)"
shows "((\<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)"
@@ -341,7 +363,7 @@
qed simp
qed simp
-lemma has_derivative_power[simp, has_derivative_intros]:
+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)"
@@ -392,13 +414,13 @@
norm (?inv y - ?inv x) * norm (?inv x)" .
qed
-lemma has_derivative_inverse[simp, has_derivative_intros]:
+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)"
shows "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))) (at x within s)"
using has_derivative_compose[OF f has_derivative_inverse', OF x] .
-lemma has_derivative_divide[simp, has_derivative_intros]:
+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 x: "g x \<noteq> 0"
@@ -409,7 +431,7 @@
text{*Conventional form requires mult-AC laws. Types real and complex only.*}
-lemma has_derivative_divide'[has_derivative_intros]:
+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)" 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)"
@@ -485,10 +507,10 @@
lemmas differentiable_within_subset = differentiable_subset
-lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable F"
+lemma differentiable_ident [simp, derivative_intros]: "(\<lambda>x. x) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_ident)
-lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable F"
+lemma differentiable_const [simp, derivative_intros]: "(\<lambda>z. a) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_const)
lemma differentiable_in_compose:
@@ -499,48 +521,42 @@
"f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f (g x)) differentiable (at x within s)"
by (blast intro: differentiable_in_compose differentiable_subset)
-lemma differentiable_sum [simp]:
+lemma differentiable_sum [simp, derivative_intros]:
"f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_add)
-lemma differentiable_minus [simp]:
+lemma differentiable_minus [simp, derivative_intros]:
"f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_minus)
-lemma differentiable_diff [simp]:
+lemma differentiable_diff [simp, derivative_intros]:
"f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x - g x) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_diff)
-lemma differentiable_mult [simp]:
+lemma differentiable_mult [simp, derivative_intros]:
fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_algebra"
shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x * g x) differentiable (at x within s)"
unfolding differentiable_def by (blast intro: has_derivative_mult)
-lemma differentiable_inverse [simp]:
+lemma differentiable_inverse [simp, derivative_intros]:
fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
shows "f differentiable (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable (at x within s)"
unfolding differentiable_def by (blast intro: has_derivative_inverse)
-lemma differentiable_divide [simp]:
+lemma differentiable_divide [simp, derivative_intros]:
fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable (at x within s)"
unfolding divide_inverse using assms by simp
-lemma differentiable_power [simp]:
+lemma differentiable_power [simp, derivative_intros]:
fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)"
unfolding differentiable_def by (blast intro: has_derivative_power)
-lemma differentiable_scaleR [simp]:
+lemma differentiable_scaleR [simp, derivative_intros]:
"f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable (at x within s)"
unfolding differentiable_def by (blast intro: has_derivative_scaleR)
-definition
- has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
- (infix "(has'_field'_derivative)" 50)
-where
- "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F"
-
lemma has_derivative_imp_has_field_derivative:
"(f has_derivative D) F \<Longrightarrow> (\<And>x. x * D' = D x) \<Longrightarrow> (f has_field_derivative D') F"
unfolding has_field_derivative_def
@@ -555,7 +571,7 @@
by (simp add: has_field_derivative_def has_derivative_within_subset)
abbreviation (input)
- deriv :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
where
"DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)"
@@ -588,8 +604,7 @@
lemma differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
by (force simp add: real_differentiable_def)
-lemma deriv_def:
- "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
apply (subst (2) tendsto_norm_zero_iff[symmetric])
apply (rule filterlim_cong)
@@ -602,40 +617,36 @@
subsection {* Derivatives *}
lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
- by (simp add: deriv_def)
+ by (simp add: DERIV_def)
-lemma DERIV_const [simp]: "((\<lambda>x. k) has_field_derivative 0) (at x within s)"
+lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F"
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto
-lemma DERIV_ident [simp]: "((\<lambda>x. x) has_field_derivative 1) (at x within s)"
+lemma DERIV_ident [simp, derivative_intros]: "((\<lambda>x. x) has_field_derivative 1) F"
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto
-lemma field_differentiable_add:
- assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
- shows "((\<lambda>z. f z + g z) has_field_derivative f' + g') F"
- apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
- using assms
- by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
+lemma field_differentiable_add[derivative_intros]:
+ "(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow>
+ ((\<lambda>z. f z + g z) has_field_derivative f' + g') F"
+ by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
+ (auto simp: has_field_derivative_def field_simps mult_commute_abs)
corollary DERIV_add:
"(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
((\<lambda>x. f x + g x) has_field_derivative D + E) (at x within s)"
by (rule field_differentiable_add)
-lemma field_differentiable_minus:
- assumes "(f has_field_derivative f') F"
- shows "((\<lambda>z. - (f z)) has_field_derivative -f') F"
- apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
- using assms
- by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
+lemma field_differentiable_minus[derivative_intros]:
+ "(f has_field_derivative f') F \<Longrightarrow> ((\<lambda>z. - (f z)) has_field_derivative -f') F"
+ by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
+ (auto simp: has_field_derivative_def field_simps mult_commute_abs)
corollary DERIV_minus: "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. - f x) has_field_derivative -D) (at x within s)"
by (rule field_differentiable_minus)
-lemma field_differentiable_diff:
- assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
- shows "((\<lambda>z. f z - g z) has_field_derivative f' - g') F"
-by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
+lemma field_differentiable_diff[derivative_intros]:
+ "(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> ((\<lambda>z. f z - g z) has_field_derivative f' - g') F"
+ by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
corollary DERIV_diff:
"(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
@@ -658,7 +669,7 @@
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
(auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
-lemma DERIV_mult:
+lemma DERIV_mult[derivative_intros]:
"(f has_field_derivative Da) (at x within s) \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
((\<lambda>x. f x * g x) has_field_derivative Da * g x + Db * f x) (at x within s)"
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
@@ -672,7 +683,7 @@
lemma DERIV_cmult_right:
"(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
- using DERIV_cmult by (force simp add: mult_ac)
+ using DERIV_cmult by (force simp add: mult_ac)
lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)"
by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
@@ -683,15 +694,15 @@
lemma DERIV_unique:
"DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
- unfolding deriv_def by (rule LIM_unique)
+ unfolding DERIV_def by (rule LIM_unique)
-lemma DERIV_setsum:
+lemma DERIV_setsum[derivative_intros]:
"(\<And> n. n \<in> S \<Longrightarrow> ((\<lambda>x. f x n) has_field_derivative (f' x n)) F) \<Longrightarrow>
((\<lambda>x. setsum (f x) S) has_field_derivative setsum (f' x) S) F"
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_setsum])
(auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative)
-lemma DERIV_inverse':
+lemma DERIV_inverse'[derivative_intros]:
"(f has_field_derivative D) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_inverse])
@@ -712,7 +723,7 @@
text {* Derivative of quotient *}
-lemma DERIV_divide:
+lemma DERIV_divide[derivative_intros]:
"(f has_field_derivative D) (at x within s) \<Longrightarrow>
(g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
((\<lambda>x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)"
@@ -731,7 +742,7 @@
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
(auto simp: has_field_derivative_def)
-lemma DERIV_power:
+lemma DERIV_power[derivative_intros]:
"(f has_field_derivative D) (at x within s) \<Longrightarrow>
((\<lambda>x. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)"
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
@@ -778,34 +789,8 @@
shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
by (metis UNIV_I DERIV_chain_s [of UNIV] assms)
-
-subsubsection {* @{text "DERIV_intros"} *}
-
-ML {*
-structure Deriv_Intros = Named_Thms
-(
- val name = @{binding DERIV_intros}
- val description = "DERIV introduction rules"
-)
-*}
-
-setup Deriv_Intros.setup
-
-lemma DERIV_cong: "(f has_field_derivative X) (at x within s) \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) (at x within s)"
- by simp
-
declare
- DERIV_const[THEN DERIV_cong, DERIV_intros]
- DERIV_ident[THEN DERIV_cong, DERIV_intros]
- DERIV_add[THEN DERIV_cong, DERIV_intros]
- DERIV_minus[THEN DERIV_cong, DERIV_intros]
- DERIV_mult[THEN DERIV_cong, DERIV_intros]
- DERIV_diff[THEN DERIV_cong, DERIV_intros]
- DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
- DERIV_divide[THEN DERIV_cong, DERIV_intros]
- DERIV_power[where 'a=real, THEN DERIV_cong,
- unfolded real_of_nat_def[symmetric], DERIV_intros]
- DERIV_setsum[THEN DERIV_cong, DERIV_intros]
+ DERIV_power[where 'a=real, unfolded real_of_nat_def[symmetric], derivative_intros]
text{*Alternative definition for differentiability*}
@@ -821,7 +806,7 @@
done
lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
- by (simp add: deriv_def DERIV_LIM_iff)
+ by (simp add: DERIV_def DERIV_LIM_iff)
lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
@@ -836,11 +821,11 @@
lemma DERIV_shift:
"(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
- by (simp add: deriv_def field_simps)
+ by (simp add: DERIV_def field_simps)
lemma DERIV_mirror:
"(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
- by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
+ by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
tendsto_minus_cancel_left field_simps conj_commute)
text {* Caratheodory formulation of derivative at a point *}
@@ -855,7 +840,7 @@
let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
show "isCont ?g x" using der
- by (simp add: isCont_iff deriv_def cong: LIM_equal [rule_format])
+ by (simp add: isCont_iff DERIV_def cong: LIM_equal [rule_format])
show "?g x = l" by simp
qed
next
@@ -863,7 +848,7 @@
then obtain g where
"(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
thus "(DERIV f x :> l)"
- by (auto simp add: isCont_iff deriv_def cong: LIM_cong)
+ by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
qed
text {*
@@ -1477,7 +1462,7 @@
from cdef have "DERIV ?h c :> l" by auto
moreover have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)"
- using g'cdef f'cdef by (auto intro!: DERIV_intros)
+ using g'cdef f'cdef by (auto intro!: derivative_eq_intros)
ultimately have leq: "l = g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
{
--- a/src/HOL/Library/Inner_Product.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Library/Inner_Product.thy Thu Apr 03 22:04:57 2014 +0200
@@ -180,7 +180,7 @@
lemmas isCont_inner [simp] =
bounded_bilinear.isCont [OF bounded_bilinear_inner]
-lemmas has_derivative_inner [has_derivative_intros] =
+lemmas has_derivative_inner [derivative_intros] =
bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
lemmas bounded_linear_inner_left =
@@ -189,10 +189,10 @@
lemmas bounded_linear_inner_right =
bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
-lemmas has_derivative_inner_right [has_derivative_intros] =
+lemmas has_derivative_inner_right [derivative_intros] =
bounded_linear.has_derivative [OF bounded_linear_inner_right]
-lemmas has_derivative_inner_left [has_derivative_intros] =
+lemmas has_derivative_inner_left [derivative_intros] =
bounded_linear.has_derivative [OF bounded_linear_inner_left]
lemma differentiable_inner [simp]:
--- a/src/HOL/Library/Poly_Deriv.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy Thu Apr 03 22:04:57 2014 +0200
@@ -28,9 +28,8 @@
by (simp add: pderiv.simps)
lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
- apply (induct p arbitrary: n, simp)
- apply (simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
- done
+ by (induct p arbitrary: n)
+ (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
primrec pderiv_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list"
where
@@ -54,8 +53,7 @@
apply (cases "degree p", simp)
apply (rule le_degree)
apply (simp add: coeff_pderiv del: of_nat_Suc)
- apply (rule subst, assumption)
- apply (rule leading_coeff_neq_0, clarsimp)
+ apply (metis degree_0 leading_coeff_0_iff nat.distinct(1))
done
lemma pderiv_singleton [simp]: "pderiv [:a:] = 0"
@@ -74,10 +72,7 @@
by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p"
-apply (induct p)
-apply simp
-apply (simp add: pderiv_add pderiv_smult pderiv_pCons algebra_simps)
-done
+by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps)
lemma pderiv_power_Suc:
"pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p"
@@ -87,13 +82,9 @@
apply (subst pderiv_mult)
apply (erule ssubst)
apply (simp only: of_nat_Suc smult_add_left smult_1_left)
-apply (simp add: algebra_simps) (* FIXME *)
+apply (simp add: algebra_simps)
done
-
-lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
-by (simp add: DERIV_cmult mult_commute [of _ c])
-
lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
by (rule DERIV_cong, rule DERIV_pow, simp)
declare DERIV_pow2 [simp] DERIV_pow [simp]
@@ -102,7 +93,7 @@
by (rule DERIV_cong, rule DERIV_add, auto)
lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
- by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
+ by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons)
text{* Consequences of the derivative theorem above*}
@@ -116,9 +107,8 @@
lemma poly_IVT_pos: "[| a < b; poly p (a::real) < 0; 0 < poly p b |]
==> \<exists>x. a < x & x < b & (poly p x = 0)"
-apply (cut_tac f = "%x. poly p x" and a = a and b = b and y = 0 in IVT_objl)
-apply (auto simp add: order_le_less)
-done
+using IVT_objl [of "poly p" a 0 b]
+by (auto simp add: order_le_less)
lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |]
==> \<exists>x. a < x & x < b & (poly p x = 0)"
@@ -126,7 +116,8 @@
lemma poly_MVT: "(a::real) < b ==>
\<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
-apply (drule_tac f = "poly p" in MVT, auto)
+using MVT [of a b "poly p"]
+apply auto
apply (rule_tac x = z in exI)
apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
done
@@ -135,16 +126,12 @@
lemma order_unique_lemma:
fixes p :: "'a::idom poly"
- assumes "[:-a, 1:] ^ n dvd p \<and> \<not> [:-a, 1:] ^ Suc n dvd p"
+ assumes "[:-a, 1:] ^ n dvd p" "\<not> [:-a, 1:] ^ Suc n dvd p"
shows "n = order a p"
unfolding Polynomial.order_def
apply (rule Least_equality [symmetric])
-apply (rule assms [THEN conjunct2])
-apply (erule contrapos_np)
-apply (rule power_le_dvd)
-apply (rule assms [THEN conjunct1])
-apply simp
-done
+apply (rule assms)
+by (metis assms not_less_eq_eq power_le_dvd)
lemma lemma_order_pderiv1:
"pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
@@ -158,45 +145,43 @@
shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
by (drule (1) Rings.dvd_diff, simp)
-lemma lemma_order_pderiv [rule_format]:
- "\<forall>p q a. 0 < n &
- pderiv p \<noteq> 0 &
- p = [:- a, 1:] ^ n * q & ~ [:- a, 1:] dvd q
- --> n = Suc (order a (pderiv p))"
- apply (cases "n", safe, rename_tac n p q a)
- apply (rule order_unique_lemma)
- apply (rule conjI)
- apply (subst lemma_order_pderiv1)
- apply (rule dvd_add)
- apply (rule dvd_mult2)
- apply (rule le_imp_power_dvd, simp)
- apply (rule dvd_smult)
- apply (rule dvd_mult)
- apply (rule dvd_refl)
- apply (subst lemma_order_pderiv1)
- apply (erule contrapos_nn) back
- apply (subgoal_tac "[:- a, 1:] ^ Suc n dvd q * [:- a, 1:] ^ n")
- apply (simp del: mult_pCons_left)
- apply (drule dvd_add_cancel1)
- apply (simp del: mult_pCons_left)
- apply (drule dvd_smult_cancel, simp del: of_nat_Suc)
- apply assumption
-done
+lemma lemma_order_pderiv:
+ assumes n: "0 < n"
+ and pd: "pderiv p \<noteq> 0"
+ and pe: "p = [:- a, 1:] ^ n * q"
+ and nd: "~ [:- a, 1:] dvd q"
+ shows "n = Suc (order a (pderiv p))"
+using n
+proof -
+ have "pderiv ([:- a, 1:] ^ n * q) \<noteq> 0"
+ using assms by auto
+ obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
+ using assms by (cases n) auto
+ then have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
+ by (metis dvd_add_cancel1 dvd_smult_iff dvd_triv_left of_nat_eq_0_iff old.nat.distinct(2))
+ have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))"
+ proof (rule order_unique_lemma)
+ show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
+ apply (subst lemma_order_pderiv1)
+ apply (rule dvd_add)
+ apply (metis dvdI dvd_mult2 power_Suc2)
+ apply (metis dvd_smult dvd_triv_right)
+ done
+ next
+ show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
+ apply (subst lemma_order_pderiv1)
+ by (metis * nd dvd_mult_cancel_right field_power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
+ qed
+ then show ?thesis
+ by (metis `n = Suc n'` pe)
+qed
lemma order_decomp:
"p \<noteq> 0
==> \<exists>q. p = [:-a, 1:] ^ (order a p) * q &
~([:-a, 1:] dvd q)"
apply (drule order [where a=a])
-apply (erule conjE)
-apply (erule dvdE)
-apply (rule exI)
-apply (rule conjI, assumption)
-apply (erule contrapos_nn)
-apply (erule ssubst) back
-apply (subst power_Suc2)
-apply (erule mult_dvd_mono [OF dvd_refl])
-done
+by (metis dvdE dvd_mult_cancel_left power_Suc2)
lemma order_pderiv: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
==> (order a p = Suc (order a (pderiv p)))"
@@ -219,9 +204,9 @@
apply (drule order [where a=a and p=p, folded i_def t_def])
apply (drule order [where a=a and p=q, folded j_def t_def])
apply clarify
+ apply (erule dvdE)+
apply (rule order_unique_lemma [symmetric], fold t_def)
- apply (erule dvdE)+
- apply (simp add: power_add t_dvd_iff)
+ apply (simp_all add: power_add t_dvd_iff)
done
qed
@@ -230,9 +215,7 @@
lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
apply (cases "p = 0", auto)
apply (drule order_2 [where a=a and p=p])
-apply (erule contrapos_np)
-apply (erule power_le_dvd)
-apply simp
+apply (metis not_less_eq_eq power_le_dvd)
apply (erule power_le_dvd [OF order_1])
done
@@ -277,13 +260,11 @@
pderiv p = e * d;
d = r * p + s * pderiv p
|] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
-apply (blast intro: poly_squarefree_decomp_order)
-done
+by (blast intro: poly_squarefree_decomp_order)
lemma order_pderiv2: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
==> (order a (pderiv p) = n) = (order a p = Suc n)"
-apply (auto dest: order_pderiv)
-done
+by (auto dest: order_pderiv)
definition
rsquarefree :: "'a::idom poly => bool" where
@@ -300,13 +281,9 @@
apply (case_tac "p = 0", simp, simp)
apply (case_tac "pderiv p = 0")
apply simp
-apply (drule pderiv_iszero, clarify)
-apply simp
-apply (rule allI)
-apply (cut_tac p = "[:h:]" and a = a in order_root)
-apply simp
-apply (auto simp add: order_root order_pderiv2)
-apply (erule_tac x="a" in allE, simp)
+apply (drule pderiv_iszero, clarsimp)
+apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
+apply (force simp add: order_root order_pderiv2)
done
lemma poly_squarefree_decomp:
--- a/src/HOL/Library/Polynomial.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Library/Polynomial.thy Thu Apr 03 22:04:57 2014 +0200
@@ -1747,12 +1747,9 @@
lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
apply (cases "p = 0", simp_all)
apply (rule iffI)
-apply (rule ccontr, simp)
-apply (frule order_2 [where a=a], simp)
-apply (simp add: poly_eq_0_iff_dvd)
-apply (simp add: poly_eq_0_iff_dvd)
-apply (simp only: order_def)
-apply (drule not_less_Least, simp)
+apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right)
+unfolding poly_eq_0_iff_dvd
+apply (metis dvd_power dvd_trans order_1)
done
--- a/src/HOL/Library/Product_Vector.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Library/Product_Vector.thy Thu Apr 03 22:04:57 2014 +0200
@@ -478,7 +478,7 @@
subsubsection {* Frechet derivatives involving pairs *}
-lemma has_derivative_Pair [has_derivative_intros]:
+lemma has_derivative_Pair [derivative_intros]:
assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
proof (rule has_derivativeI_sandwich[of 1])
@@ -497,10 +497,10 @@
by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
qed simp
-lemmas has_derivative_fst [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
-lemmas has_derivative_snd [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
+lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
+lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
-lemma has_derivative_split [has_derivative_intros]:
+lemma has_derivative_split [derivative_intros]:
"((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
unfolding split_beta' .
--- a/src/HOL/MacLaurin.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/MacLaurin.thy Thu Apr 03 22:04:57 2014 +0200
@@ -40,7 +40,8 @@
have "DERIV (difg m) t :> diff (Suc m) t -
((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
- by (auto intro!: DERIV_intros DERIV[rule_format, OF INIT2])
+ by (auto intro!: derivative_eq_intros DERIV[rule_format, OF INIT2]
+ simp: real_of_nat_def[symmetric])
moreover
from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
unfolding atLeast0LessThan[symmetric] by auto
@@ -209,7 +210,7 @@
f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
diff n t / real (fact n) * h ^ n"
proof -
- txt "Transform @{text ABL'} into @{text DERIV_intros} format."
+ txt "Transform @{text ABL'} into @{text derivative_intros} format."
note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
from assms
have "\<exists>t>0. t < - h \<and>
@@ -217,7 +218,7 @@
(\<Sum>m<n.
(- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
(- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
- by (intro Maclaurin) (auto intro!: DERIV_intros DERIV')
+ by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
then guess t ..
moreover
have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
@@ -417,7 +418,7 @@
apply safe
apply (simp (no_asm))
apply (simp (no_asm) add: sin_expansion_lemma)
-apply (force intro!: DERIV_intros)
+apply (force intro!: derivative_eq_intros)
apply (subst (asm) setsum_0', clarify, case_tac "x", simp, simp)
apply (cases n, simp, simp)
apply (rule ccontr, simp)
@@ -446,7 +447,7 @@
apply safe
apply simp
apply (simp (no_asm) add: sin_expansion_lemma)
-apply (force intro!: DERIV_intros)
+apply (force intro!: derivative_eq_intros)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
@@ -463,7 +464,7 @@
apply safe
apply simp
apply (simp (no_asm) add: sin_expansion_lemma)
-apply (force intro!: DERIV_intros)
+apply (force intro!: derivative_eq_intros)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
@@ -553,7 +554,7 @@
apply (clarify)
apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
apply (cut_tac m=m in mod_exhaust_less_4)
- apply (safe, auto intro!: DERIV_intros)
+ apply (safe, auto intro!: derivative_eq_intros)
done
from Maclaurin_all_le [OF diff_0 DERIV_diff]
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Apr 03 22:04:57 2014 +0200
@@ -15,7 +15,7 @@
shows "((op * c) has_derivative (op * c)) F"
by (rule has_derivative_mult_right [OF has_derivative_id])
-lemma has_derivative_of_real[has_derivative_intros, simp]:
+lemma has_derivative_of_real[derivative_intros, simp]:
"(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
using bounded_linear.has_derivative[OF bounded_linear_of_real] .
@@ -200,14 +200,6 @@
shows "DERIV g a :> f'"
by (blast intro: assms DERIV_transform_within)
-subsection{*Further useful properties of complex conjugation*}
-
-lemma continuous_within_cnj: "continuous (at z within s) cnj"
-by (metis bounded_linear_cnj linear_continuous_within)
-
-lemma continuous_on_cnj: "continuous_on s cnj"
-by (metis bounded_linear_cnj linear_continuous_on)
-
subsection {*Some limit theorems about real part of real series etc.*}
(*MOVE? But not to Finite_Cartesian_Product*)
@@ -521,29 +513,29 @@
"\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
\<Longrightarrow> deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
- by (auto intro!: DERIV_imp_deriv DERIV_intros)
+ by (auto intro!: DERIV_imp_deriv derivative_intros)
lemma complex_derivative_diff:
"\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
\<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
- by (auto intro!: DERIV_imp_deriv DERIV_intros)
+ by (auto intro!: DERIV_imp_deriv derivative_intros)
lemma complex_derivative_mult:
"\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
\<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
- by (auto intro!: DERIV_imp_deriv DERIV_intros)
+ by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
lemma complex_derivative_cmult:
"f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
- by (auto intro!: DERIV_imp_deriv DERIV_intros)
+ by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
lemma complex_derivative_cmult_right:
"f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
- by (auto intro!: DERIV_imp_deriv DERIV_intros)
+ by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
lemma complex_derivative_transform_within_open:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk>
@@ -1037,7 +1029,7 @@
then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / of_nat (fact i)))
has_field_derivative f (Suc n) u * (z-u) ^ n / of_nat (fact n))
(at u within s)"
- apply (intro DERIV_intros DERIV_power[THEN DERIV_cong])
+ apply (intro derivative_eq_intros)
apply (blast intro: assms `u \<in> s`)
apply (rule refl)+
apply (auto simp: field_simps)
@@ -1083,7 +1075,7 @@
proof -
have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
- note assms[unfolded has_field_derivative_def, has_derivative_intros]
+ note assms[unfolded has_field_derivative_def, derivative_intros]
show ?thesis
apply (cut_tac mvt_simple
[of 0 1 "Re o f o (\<lambda>t. (1 - t) *\<^sub>R w + t *\<^sub>R z)"
@@ -1091,7 +1083,7 @@
apply auto
apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
apply (auto simp add: open_segment_def twz) []
- apply (intro has_derivative_eq_intros has_derivative_at_within)
+ apply (intro derivative_eq_intros has_derivative_at_within)
apply simp_all
apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
apply (force simp add: twz closed_segment_def)
@@ -1136,7 +1128,7 @@
f (Suc n) u * (z - u) ^ n / of_nat (fact n)" .
then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / of_nat (fact i)) has_field_derivative
f (Suc n) u * (z - u) ^ n / of_nat (fact n)) (at u)"
- apply (intro DERIV_intros)+
+ apply (intro derivative_eq_intros)+
apply (force intro: u assms)
apply (rule refl)+
apply (auto simp: mult_ac)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Apr 03 22:04:57 2014 +0200
@@ -45,7 +45,7 @@
lemma has_derivative_add_const:
"(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
- by (intro has_derivative_eq_intros) auto
+ by (intro derivative_eq_intros) auto
subsection {* Derivative with composed bilinear function. *}
@@ -319,14 +319,14 @@
subsection {* The chain rule *}
-lemma diff_chain_within[has_derivative_intros]:
+lemma diff_chain_within[derivative_intros]:
assumes "(f has_derivative f') (at x within s)"
and "(g has_derivative g') (at (f x) within (f ` s))"
shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)"
using has_derivative_in_compose[OF assms]
by (simp add: comp_def)
-lemma diff_chain_at[has_derivative_intros]:
+lemma diff_chain_at[derivative_intros]:
"(f has_derivative f') (at x) \<Longrightarrow>
(g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)"
using has_derivative_compose[of f f' x UNIV g g']
@@ -544,7 +544,7 @@
from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
unfolding eventually_at by (force simp: dist_commute)
have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
- by (intro has_derivative_eq_intros, auto)
+ by (intro derivative_eq_intros) auto
then have "FDERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> (\<lambda>k. f' (k *\<^sub>R h))"
by (rule has_derivative_compose, simp add: deriv)
then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
@@ -677,7 +677,7 @@
assume x: "x \<in> {a <..< b}"
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
- by (intro has_derivative_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
+ by (intro derivative_intros assms(3)[rule_format,OF x])
qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
then obtain x where
"x \<in> {a <..< b}"
@@ -815,7 +815,7 @@
let ?u = "x + u *\<^sub>R (y - x)"
have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
apply (rule diff_chain_within)
- apply (rule has_derivative_intros)+
+ apply (rule derivative_intros)+
apply (rule has_derivative_within_subset)
apply (rule assms(2)[rule_format])
using goal1 *
@@ -1538,12 +1538,12 @@
unfolding ph' *
apply (simp add: comp_def)
apply (rule bounded_linear.has_derivative[OF assms(3)])
- apply (rule has_derivative_intros)
+ apply (rule derivative_intros)
defer
apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
apply (rule has_derivative_at_within)
using assms(5) and `u \<in> s` `a \<in> s`
- apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
+ apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
done
have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
apply (rule_tac[!] bounded_linear_sub)
@@ -1600,7 +1600,7 @@
fix x
assume "x \<in> s"
show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
- by (rule has_derivative_intros assms(2)[rule_format] `x\<in>s`)+
+ by (rule derivative_intros assms(2)[rule_format] `x\<in>s`)+
show "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e"
proof (rule onorm_bound)
fix h
@@ -1933,44 +1933,58 @@
apply auto
done
-
text {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *}
-definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> real filter \<Rightarrow> bool"
- (infix "has'_vector'_derivative" 50)
- where "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net"
-
-definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
-
-lemma vector_derivative_works:
- fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
- shows "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
- (is "?l = ?r")
-proof
- assume ?l
- obtain f' where f': "(f has_derivative f') net"
- using `?l` unfolding differentiable_def ..
- then interpret bounded_linear f'
- by auto
- show ?r
- unfolding vector_derivative_def has_vector_derivative_def
- apply -
- apply (rule someI_ex,rule_tac x="f' 1" in exI)
- using f'
- unfolding scaleR[symmetric]
- apply auto
- done
-next
- assume ?r
- then show ?l
- unfolding vector_derivative_def has_vector_derivative_def differentiable_def
- by auto
-qed
-
lemma has_field_derivative_iff_has_vector_derivative:
"(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..
+lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net"
+ by (auto simp: has_vector_derivative_def)
+
+lemma has_vector_derivative_id[simp, derivative_intros]: "((\<lambda>x. x) has_vector_derivative 1) net"
+ by (auto simp: has_vector_derivative_def)
+
+lemma has_vector_derivative_neg[derivative_intros]:
+ "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net"
+ by (auto simp: has_vector_derivative_def)
+
+lemma has_vector_derivative_add[derivative_intros]:
+ "(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow>
+ ((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net"
+ by (auto simp: has_vector_derivative_def scaleR_right_distrib)
+
+lemma has_vector_derivative_sub[derivative_intros]:
+ "(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow>
+ ((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
+ by (auto simp: has_vector_derivative_def scaleR_diff_right)
+
+lemma (in bounded_linear) has_vector_derivative:
+ assumes "(g has_vector_derivative g') (at x within s)"
+ shows "((\<lambda>x. f (g x)) has_vector_derivative f g') (at x within s)"
+ using has_derivative[OF assms[unfolded has_vector_derivative_def]]
+ by (simp add: has_vector_derivative_def scaleR)
+
+lemma (in bounded_bilinear) has_vector_derivative:
+ assumes "(f has_vector_derivative f') (at x within s)"
+ and "(g has_vector_derivative g') (at x within s)"
+ shows "((\<lambda>x. f x ** g x) has_vector_derivative (f x ** g' + f' ** g x)) (at x within s)"
+ using FDERIV[OF assms(1-2)[unfolded has_vector_derivative_def]]
+ by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib)
+
+lemma has_vector_derivative_scaleR[derivative_intros]:
+ "(f has_field_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
+ ((\<lambda>x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)"
+ unfolding has_field_derivative_iff_has_vector_derivative
+ by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR])
+
+lemma has_vector_derivative_mult[derivative_intros]:
+ "(f has_vector_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
+ ((\<lambda>x. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within s)"
+ by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult])
+
+definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
+
lemma vector_derivative_unique_at:
assumes "(f has_vector_derivative f') (at x)"
and "(f has_vector_derivative f'') (at x)"
@@ -1983,6 +1997,20 @@
unfolding fun_eq_iff by auto
qed
+lemma vector_derivative_works:
+ "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
+ (is "?l = ?r")
+proof
+ assume ?l
+ obtain f' where f': "(f has_derivative f') net"
+ using `?l` unfolding differentiable_def ..
+ then interpret bounded_linear f'
+ by auto
+ show ?r
+ unfolding vector_derivative_def has_vector_derivative_def
+ by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f')
+qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
+
lemma vector_derivative_unique_within_closed_interval:
assumes "a < b"
and "x \<in> cbox a b"
@@ -2028,87 +2056,8 @@
done
lemma has_vector_derivative_within_subset:
- "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow>
- (f has_vector_derivative f') (at x within t)"
- unfolding has_vector_derivative_def
- apply (rule has_derivative_within_subset)
- apply auto
- done
-
-lemma has_vector_derivative_const: "((\<lambda>x. c) has_vector_derivative 0) net"
- unfolding has_vector_derivative_def
- using has_derivative_const
- by auto
-
-lemma has_vector_derivative_id: "((\<lambda>x::real. x) has_vector_derivative 1) net"
- unfolding has_vector_derivative_def
- using has_derivative_id
- by auto
-
-lemma has_vector_derivative_cmul:
- "(f has_vector_derivative f') net \<Longrightarrow>
- ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
- unfolding has_vector_derivative_def
- apply (drule scaleR_right_has_derivative)
- apply (auto simp add: algebra_simps)
- done
-
-lemma has_vector_derivative_cmul_eq:
- assumes "c \<noteq> 0"
- shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)"
- apply (rule iffI)
- apply (drule has_vector_derivative_cmul[where c="1/c"])
- apply (rule_tac [2] has_vector_derivative_cmul)
- using assms
- apply auto
- done
-
-lemma has_vector_derivative_neg:
- "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net"
- unfolding has_vector_derivative_def
- apply (drule has_derivative_neg)
- apply auto
- done
-
-lemma has_vector_derivative_add:
- assumes "(f has_vector_derivative f') net"
- and "(g has_vector_derivative g') net"
- shows "((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net"
- using has_derivative_add[OF assms[unfolded has_vector_derivative_def]]
- unfolding has_vector_derivative_def
- unfolding scaleR_right_distrib
- by auto
-
-lemma has_vector_derivative_sub:
- assumes "(f has_vector_derivative f') net"
- and "(g has_vector_derivative g') net"
- shows "((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
- using has_derivative_sub[OF assms[unfolded has_vector_derivative_def]]
- unfolding has_vector_derivative_def scaleR_right_diff_distrib
- by auto
-
-lemma has_vector_derivative_bilinear_within:
- assumes "(f has_vector_derivative f') (at x within s)"
- and "(g has_vector_derivative g') (at x within s)"
- assumes "bounded_bilinear h"
- shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x within s)"
-proof -
- interpret bounded_bilinear h
- using assms by auto
- show ?thesis
- using has_derivative_bilinear_within[OF assms(1-2)[unfolded has_vector_derivative_def], of h]
- unfolding o_def has_vector_derivative_def
- using assms(3)
- unfolding scaleR_right scaleR_left scaleR_right_distrib
- by auto
-qed
-
-lemma has_vector_derivative_bilinear_at:
- assumes "(f has_vector_derivative f') (at x)"
- and "(g has_vector_derivative g') (at x)"
- assumes "bounded_bilinear h"
- shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
- using has_vector_derivative_bilinear_within[OF assms] .
+ "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
+ by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
lemma has_vector_derivative_at_within:
"(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Apr 03 22:04:57 2014 +0200
@@ -8793,11 +8793,10 @@
by (auto simp add: algebra_simps)
have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x))
(at t within {0 .. 1})"
- apply (rule diff_chain_within)
- apply (rule has_derivative_add)
+ apply (intro derivative_eq_intros)
+ apply simp_all
+ apply (simp add: field_simps)
unfolding scaleR_simps
- apply (intro has_derivative_intros)
- apply (intro has_derivative_intros)
apply (rule has_derivative_within_subset,rule assms(6)[rule_format])
apply (rule *)
apply safe
--- a/src/HOL/NSA/HDeriv.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/NSA/HDeriv.thy Thu Apr 03 22:04:57 2014 +0200
@@ -34,10 +34,10 @@
lemma DERIV_NS_iff:
"(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)"
-by (simp add: deriv_def LIM_NSLIM_iff)
+by (simp add: DERIV_def LIM_NSLIM_iff)
lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D"
-by (simp add: deriv_def LIM_NSLIM_iff)
+by (simp add: DERIV_def LIM_NSLIM_iff)
lemma hnorm_of_hypreal:
"\<And>r. hnorm (( *f* of_real) r::'a::real_normed_div_algebra star) = \<bar>r\<bar>"
@@ -377,7 +377,7 @@
text{*Now equivalence between NSDERIV and DERIV*}
lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)"
-by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
+by (simp add: DERIV_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
(* NS version *)
lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
--- a/src/HOL/NthRoot.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/NthRoot.thy Thu Apr 03 22:04:57 2014 +0200
@@ -326,7 +326,7 @@
qed
next
show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
using n x by simp
qed (rule isCont_real_root)
@@ -471,8 +471,8 @@
using DERIV_real_sqrt_generic by simp
declare
- DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
- DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros]
+ DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros]
lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
apply auto
--- a/src/HOL/Probability/Distributions.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy Thu Apr 03 22:04:57 2014 +0200
@@ -52,7 +52,7 @@
let ?F = "\<lambda>x. - exp (- x * l)"
have deriv: "\<And>x. DERIV ?F x :> ?f x" "\<And>x. 0 \<le> l * exp (- x * l)"
- by (auto intro!: DERIV_intros simp: zero_le_mult_iff)
+ by (auto intro!: derivative_eq_intros simp: zero_le_mult_iff)
have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)"
by (auto simp: emeasure_density exponential_density_def
@@ -178,12 +178,12 @@
proof (rule integral_FTC_atLeastAtMost)
fix x assume "0 \<le> x" "x \<le> b"
show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)"
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_eq_intros)
show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x "
by (intro continuous_intros)
qed fact
also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)"
- by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros)
+ by (rule integral_FTC_atLeastAtMost) (auto intro!: derivative_eq_intros)
finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)"
by (auto simp: field_simps exp_minus inverse_eq_divide)
qed
@@ -374,7 +374,7 @@
fix x
show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
using uniform_distributed_params[OF D]
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_eq_intros)
show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
using uniform_distributed_params[OF D]
by (auto intro!: isCont_divide)
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 03 22:04:57 2014 +0200
@@ -237,7 +237,7 @@
val alt_ergo_config : atp_config =
{exec = K (["WHY3_HOME"], ["why3"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- "--format tptp --prover 'Alt-Ergo,0.95,' --timelimit " ^
+ "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^
string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
proof_delims = [],
known_failures =
@@ -559,7 +559,7 @@
(* Vampire *)
-(* Vampire 1.8 has TFF support, but the support was buggy until revision
+(* Vampire 1.8 has TFF0 support, but the support was buggy until revision
1435 (or shortly before). *)
fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
@@ -574,9 +574,8 @@
" --proof tptp --output_axiom_names on" ^
(if is_vampire_at_least_1_8 () then
(* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
- " --forced_options propositional_to_bdd=off" ^
(if full_proof then
- ":splitting=off:equality_proxy=off:general_splitting=off\
+ "--forced_options splitting=off:equality_proxy=off:general_splitting=off\
\:inequality_splitting=0:naming=0"
else
"")
@@ -619,11 +618,10 @@
val z3_tff0 = TFF Monomorphic
val z3_tptp_config : atp_config =
- {exec = K (["Z3_HOME"], ["z3"]),
+ {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
- string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
- proof_delims = [("\ncore(", ").")],
+ "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
+ proof_delims = [],
known_failures = known_szs_status_failures,
prem_role = Hypothesis,
best_slices =
--- a/src/HOL/Transcendental.thy Thu Apr 03 21:55:48 2014 +0200
+++ b/src/HOL/Transcendental.thy Thu Apr 03 22:04:57 2014 +0200
@@ -630,7 +630,7 @@
and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
and 4: "norm x < norm K"
shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
- unfolding deriv_def
+ unfolding DERIV_def
proof (rule LIM_zero_cancel)
show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
- suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
@@ -669,7 +669,7 @@
and "summable L"
and L_def: "\<And>n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar>f x n - f y n\<bar> \<le> L n * \<bar>x - y\<bar>"
shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))"
- unfolding deriv_def
+ unfolding DERIV_def
proof (rule LIM_I)
fix r :: real
assume "0 < r" hence "0 < r/3" by auto
@@ -863,7 +863,7 @@
{
fix n
show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
- by (auto intro!: DERIV_intros simp del: power_Suc)
+ by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def)
}
{
fix x
@@ -978,7 +978,7 @@
apply (simp del: of_real_add)
done
-declare DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
lemma isCont_exp: "isCont exp x"
by (rule DERIV_exp [THEN DERIV_isCont])
@@ -1315,7 +1315,7 @@
lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
-declare DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
lemma ln_series:
assumes "0 < x" and "x < 2"
@@ -1356,7 +1356,7 @@
hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
unfolding One_nat_def by auto
hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
- unfolding deriv_def repos .
+ unfolding DERIV_def repos .
ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
by (rule DERIV_diff)
thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
@@ -1621,7 +1621,7 @@
proof -
let ?l = "\<lambda>y. ln y - y + 1"
have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_eq_intros)
show ?thesis
proof (cases rule: linorder_cases)
@@ -1699,9 +1699,9 @@
show ?case
proof (rule lhospital_at_top_at_top)
show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
- by eventually_elim (intro DERIV_intros, simp, simp)
+ by eventually_elim (intro derivative_eq_intros, auto)
show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
- by eventually_elim (auto intro!: DERIV_intros)
+ by eventually_elim auto
show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
by auto
from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
@@ -1825,12 +1825,12 @@
proof -
def lb \<equiv> "1 / ln b"
moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
- using `x > 0` by (auto intro!: DERIV_intros)
+ using `x > 0` by (auto intro!: derivative_eq_intros)
ultimately show ?thesis
by (simp add: log_def)
qed
-lemmas DERIV_log[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
by (simp add: powr_def log_def)
@@ -2180,7 +2180,7 @@
summable_minus summable_sin summable_cos)
done
-declare DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
unfolding cos_def sin_def
@@ -2189,7 +2189,7 @@
summable_minus summable_sin summable_cos suminf_minus)
done
-declare DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
lemma isCont_sin: "isCont sin x"
by (rule DERIV_sin [THEN DERIV_isCont])
@@ -2238,7 +2238,7 @@
lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
proof -
have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_eq_intros)
hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
by (rule DERIV_isconst_all)
thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
@@ -2276,19 +2276,19 @@
lemma DERIV_fun_pow: "DERIV g x :> m ==>
DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
lemma DERIV_fun_exp:
"DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_intros)
lemma DERIV_fun_sin:
"DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_intros)
lemma DERIV_fun_cos:
"DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
lemma sin_cos_add_lemma:
"(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
@@ -2296,7 +2296,7 @@
(is "?f x = 0")
proof -
have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
- by (auto intro!: DERIV_intros simp add: algebra_simps)
+ by (auto intro!: derivative_eq_intros simp add: algebra_simps)
hence "?f x = ?f 0"
by (rule DERIV_isconst_all)
thus ?thesis by simp
@@ -2312,7 +2312,7 @@
"(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
proof -
have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
- by (auto intro!: DERIV_intros simp add: algebra_simps)
+ by (auto intro!: derivative_eq_intros simp add: algebra_simps)
hence "?f x = ?f 0"
by (rule DERIV_isconst_all)
thus ?thesis by simp
@@ -2859,7 +2859,7 @@
lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
unfolding tan_def
- by (auto intro!: DERIV_intros, simp add: divide_inverse power2_eq_square)
+ by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
by (rule DERIV_tan [THEN DERIV_isCont])
@@ -3332,9 +3332,9 @@
done
declare
- DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
- DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
- DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
+ DERIV_arccos[THEN DERIV_chain2, derivative_intros]
+ DERIV_arctan[THEN DERIV_chain2, derivative_intros]
lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
@@ -3465,7 +3465,7 @@
done
lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
- by (auto intro!: DERIV_intros)
+ by (auto intro!: derivative_eq_intros)
lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
by (auto simp add: sin_zero_iff even_mult_two_ex)