--- a/src/HOL/Deriv.thy Mon Mar 24 16:19:24 2014 +0100
+++ b/src/HOL/Deriv.thy Mon Mar 24 17:42:16 2014 +0100
@@ -168,6 +168,9 @@
lemma has_derivative_subset: "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset)
+lemmas has_derivative_within_subset = has_derivative_subset
+
+
subsection {* Continuity *}
lemma has_derivative_continuous:
@@ -477,6 +480,8 @@
lemma differentiable_subset: "f differentiable (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable (at x within t)"
unfolding differentiable_def by (blast intro: has_derivative_subset)
+lemmas differentiable_within_subset = differentiable_subset
+
lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_ident)
@@ -541,6 +546,11 @@
lemma has_field_derivative_imp_has_derivative: "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative op * D) F"
by (simp add: has_field_derivative_def)
+lemma DERIV_subset:
+ "(f has_field_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s
+ \<Longrightarrow> (f has_field_derivative f') (at x within t)"
+ 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 (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
@@ -597,32 +607,47 @@
lemma DERIV_ident [simp]: "((\<lambda>x. x) has_field_derivative 1) (at x within s)"
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto
-lemma DERIV_add:
+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)
+
+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 has_derivative_imp_has_field_derivative[OF has_derivative_add])
- (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
+ 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 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 has_derivative_imp_has_field_derivative[OF has_derivative_minus])
- (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
+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 DERIV_diff:
+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)
+
+corollary DERIV_diff:
"(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 has_derivative_imp_has_field_derivative[OF has_derivative_diff])
- (auto simp: field_simps dest: has_field_derivative_imp_has_derivative)
-
-lemma DERIV_add_minus:
- "(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 (simp only: DERIV_add DERIV_minus)
+ by (rule field_differentiable_diff)
lemma DERIV_continuous: "(f has_field_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
by (drule has_derivative_continuous[OF has_field_derivative_imp_has_derivative]) simp
-lemma DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
- by (auto dest!: DERIV_continuous)
+corollary DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
+ by (rule DERIV_continuous)
+
+lemma DERIV_continuous_on:
+ "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative D) (at x)) \<Longrightarrow> continuous_on s f"
+ by (metis DERIV_continuous continuous_at_imp_continuous_on)
lemma DERIV_mult':
"(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
@@ -1243,19 +1268,18 @@
(* A function with positive derivative is increasing.
A simple proof using the MVT, by Jeremy Avigad. And variants.
*)
-lemma DERIV_pos_imp_increasing:
+lemma DERIV_pos_imp_increasing_open:
fixes a::real and b::real and f::"real => real"
- assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
+ assumes "a < b" and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (EX y. DERIV f x :> y & y > 0)"
+ and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
shows "f a < f b"
proof (rule ccontr)
assume f: "~ f a < f b"
have "EX l z. a < z & z < b & DERIV f z :> l
& f b - f a = (b - a) * l"
apply (rule MVT)
- using assms
- apply auto
- apply (metis DERIV_isCont)
- apply (metis differentiableI less_le)
+ using assms Deriv.differentiableI
+ apply force+
done
then obtain l z where z: "a < z" "z < b" "DERIV f z :> l"
and "f b - f a = (b - a) * l"
@@ -1263,9 +1287,15 @@
with assms f have "~(l > 0)"
by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le)
with assms z show False
- by (metis DERIV_unique less_le)
+ by (metis DERIV_unique)
qed
+lemma DERIV_pos_imp_increasing:
+ fixes a::real and b::real and f::"real => real"
+ assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
+ shows "f a < f b"
+by (metis DERIV_pos_imp_increasing_open [of a b f] assms DERIV_continuous less_imp_le)
+
lemma DERIV_nonneg_imp_nondecreasing:
fixes a::real and b::real and f::"real => real"
assumes "a \<le> b" and
@@ -1295,21 +1325,28 @@
by (metis DERIV_unique order_less_imp_le)
qed
+lemma DERIV_neg_imp_decreasing_open:
+ fixes a::real and b::real and f::"real => real"
+ assumes "a < b" and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (EX y. DERIV f x :> y & y < 0)"
+ and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
+ shows "f a > f b"
+proof -
+ have "(%x. -f x) a < (%x. -f x) b"
+ apply (rule DERIV_pos_imp_increasing_open [of a b "%x. -f x"])
+ using assms
+ apply auto
+ apply (metis field_differentiable_minus neg_0_less_iff_less)
+ done
+ thus ?thesis
+ by simp
+qed
+
lemma DERIV_neg_imp_decreasing:
fixes a::real and b::real and f::"real => real"
assumes "a < b" and
"\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y < 0)"
shows "f a > f b"
-proof -
- have "(%x. -f x) a < (%x. -f x) b"
- apply (rule DERIV_pos_imp_increasing [of a b "%x. -f x"])
- using assms
- apply auto
- apply (metis DERIV_minus neg_0_less_iff_less)
- done
- thus ?thesis
- by simp
-qed
+by (metis DERIV_neg_imp_decreasing_open [of a b f] assms DERIV_continuous less_imp_le)
lemma DERIV_nonpos_imp_nonincreasing:
fixes a::real and b::real and f::"real => real"
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Mar 24 16:19:24 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Mar 24 17:42:16 2014 +0100
@@ -253,16 +253,6 @@
subsection{*DERIV stuff*}
-(*move some premises to a sensible order. Use more \<And> symbols.*)
-
-lemma DERIV_continuous_on: "\<lbrakk>\<And>x. x \<in> s \<Longrightarrow> DERIV f x :> D\<rbrakk> \<Longrightarrow> continuous_on s f"
- by (metis DERIV_continuous continuous_at_imp_continuous_on)
-
-lemma DERIV_subset:
- "(f has_field_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s
- \<Longrightarrow> (f has_field_derivative f') (at x within t)"
- by (simp add: has_field_derivative_def has_derivative_within_subset)
-
lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = op * 0"
by auto
@@ -496,28 +486,6 @@
apply (simp add: lambda_one [symmetric])
done
-(*DERIV_minus*)
-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)
-
-(*DERIV_add*)
-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)
-
-(*DERIV_diff*)
-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 complex_differentiable_minus:
"f complex_differentiable F \<Longrightarrow> (\<lambda>z. -(f z)) complex_differentiable F"
using assms unfolding complex_differentiable_def
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Mar 24 16:19:24 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Mar 24 17:42:16 2014 +0100
@@ -289,20 +289,6 @@
unfolding differentiable_on_def continuous_on_eq_continuous_within
using differentiable_imp_continuous_within by blast
-lemma has_derivative_within_subset:
- "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow>
- (f has_derivative f') (at x within t)"
- unfolding has_derivative_within
- using tendsto_within_subset
- by blast
-
-lemma differentiable_within_subset:
- "f differentiable (at x within t) \<Longrightarrow> s \<subseteq> t \<Longrightarrow>
- f differentiable (at x within s)"
- unfolding differentiable_def
- using has_derivative_within_subset
- by blast
-
lemma differentiable_on_subset:
"f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s"
unfolding differentiable_on_def
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 24 16:19:24 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 24 17:42:16 2014 +0100
@@ -819,12 +819,14 @@
fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
val unique = HOLogic.mk_Trueprop
(Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs));
- val unique_mor = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (init_xs @ Bs @ ss @ init_fs @ init_fs_copy)
- (Logic.list_implies (prems @ mor_prems, unique)))
- (K (mk_init_unique_mor_tac m alg_def alg_init_thm least_min_alg_thms
- in_mono'_thms alg_set_thms morE_thms map_cong0s))
- |> Thm.close_derivation;
+ val cts = map (certify lthy) ss;
+ val unique_mor = singleton (Proof_Context.export names_lthy lthy)
+ (Goal.prove_sorry lthy [] []
+ (fold_rev Logic.all (init_xs @ Bs @ init_fs @ init_fs_copy)
+ (Logic.list_implies (prems @ mor_prems, unique)))
+ (K (mk_init_unique_mor_tac cts m alg_def alg_init_thm least_min_alg_thms
+ in_mono'_thms alg_set_thms morE_thms map_cong0s))
+ |> Thm.close_derivation);
in
split_conj_thm unique_mor
end;
@@ -951,7 +953,7 @@
|> Thm.close_derivation;
fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
- val cts = map3 (SOME o certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
+ val cts = map3 (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
val mor_Abs =
Goal.prove_sorry lthy [] []
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Mar 24 16:19:24 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Mar 24 17:42:16 2014 +0100
@@ -28,8 +28,8 @@
val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> thm -> thm ->
tactic
val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
- val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
- thm list -> tactic
+ val mk_init_unique_mor_tac: cterm list -> int -> thm -> thm -> thm list -> thm list -> thm list ->
+ thm list -> thm list -> tactic
val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
val mk_least_min_alg_tac: thm -> thm -> tactic
@@ -46,8 +46,8 @@
val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
val mk_min_algs_tac: thm -> thm list -> tactic
- val mk_mor_Abs_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
- thm list -> tactic
+ val mk_mor_Abs_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> thm list ->
+ tactic
val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list ->
thm list list -> tactic
val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic
@@ -349,7 +349,7 @@
etac mor_comp, rtac mor_incl, REPEAT_DETERM_N n o rtac subset_UNIV] 1
end;
-fun mk_init_unique_mor_tac m
+fun mk_init_unique_mor_tac cts m
alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s =
let
val n = length least_min_algs;
@@ -358,21 +358,23 @@
fun mor_tac morE in_mono = EVERY' [etac morE, rtac set_mp, rtac in_mono,
REPEAT_DETERM_N n o rtac @{thm Collect_restrict}, rtac CollectI,
REPEAT_DETERM_N (m + n) o (TRY o rtac conjI THEN' atac)];
- fun cong_tac map_cong0 = EVERY' [rtac (map_cong0 RS arg_cong),
+ fun cong_tac ct map_cong0 = EVERY'
+ [rtac (map_cong0 RS cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong),
REPEAT_DETERM_N m o rtac refl,
REPEAT_DETERM_N n o (etac @{thm prop_restrict} THEN' atac)];
- fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI,
- REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
- REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
- rtac trans, mor_tac morE in_mono,
- rtac trans, cong_tac map_cong0,
- rtac sym, mor_tac morE in_mono];
+ fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
+ EVERY' [rtac ballI, rtac CollectI,
+ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
+ REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
+ rtac trans, mor_tac morE in_mono,
+ rtac trans, cong_tac ct map_cong0,
+ rtac sym, mor_tac morE in_mono];
fun mk_unique_tac (k, least_min_alg) =
select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN'
rtac (alg_def RS iffD2) THEN'
- CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s)));
+ CONJ_WRAP' mk_alg_tac (cts ~~ (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s))));
in
CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1
end;
@@ -414,7 +416,7 @@
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
CONJ_WRAP' (fn (ct, thm) =>
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
- rtac (thm RS (cterm_instantiate_pos [NONE, NONE, ct] arg_cong) RS sym),
+ rtac (thm RS (cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong) RS sym),
EVERY' (map (fn Abs_inverse =>
EVERY' [rtac (o_apply RS trans RS ballI), etac (set_mp RS Abs_inverse), atac])
Abs_inverses)])
@@ -535,8 +537,9 @@
rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
fun mk_set_nat cset ctor_map ctor_set set_nats =
- EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl,
- rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, ctor_set RS trans]),
+ EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl, rtac sym,
+ rtac (trans OF [ctor_map RS cterm_instantiate_pos [NONE, NONE, SOME cset] arg_cong,
+ ctor_set RS trans]),
rtac sym, EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
rtac sym, rtac (nth set_nats (i - 1)),
REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
--- a/src/HOL/Tools/BNF/bnf_lfp_util.ML Mon Mar 24 16:19:24 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_util.ML Mon Mar 24 17:42:16 2014 +0100
@@ -8,8 +8,6 @@
signature BNF_LFP_UTIL =
sig
- val HOL_arg_cong: cterm -> thm
-
val mk_bij_betw: term -> term -> term -> term
val mk_cardSuc: term -> term
val mk_not_empty: term -> term
@@ -25,9 +23,6 @@
open BNF_Util
-fun HOL_arg_cong ct = Drule.instantiate'
- (map SOME (Thm.dest_ctyp (Thm.ctyp_of_term ct))) [NONE, NONE, SOME ct] arg_cong;
-
(*reverse application*)
fun mk_rapp arg T = Term.absdummy (fastype_of arg --> T) (Bound 0 $ arg);
--- a/src/HOL/Transcendental.thy Mon Mar 24 16:19:24 2014 +0100
+++ b/src/HOL/Transcendental.thy Mon Mar 24 17:42:16 2014 +0100
@@ -3745,7 +3745,7 @@
have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
unfolding suminf_c'_eq_geom
by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
- from DERIV_add_minus[OF this DERIV_arctan]
+ from DERIV_diff [OF this DERIV_arctan]
show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
by auto
qed