--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Sep 16 23:51:24 2019 +0200
@@ -4960,7 +4960,7 @@
(\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
(at x within X)"
apply (simp add: part_circlepath_def linepath_def scaleR_conv_of_real)
- apply (rule has_vector_derivative_real_complex)
+ apply (rule has_vector_derivative_real_field)
apply (rule derivative_eq_intros | simp)+
done
@@ -7824,7 +7824,7 @@
hence h_holo: "h holomorphic_on A"
by (auto simp: h_def intro!: holomorphic_intros)
have "\<exists>c. \<forall>x\<in>A. f x / exp (h x) - 1 = c"
- proof (rule DERIV_zero_constant, goal_cases)
+ proof (rule has_field_derivative_zero_constant, goal_cases)
case (2 x)
note [simp] = at_within_open[OF _ \<open>open A\<close>]
from 2 and z0 and f show ?case
--- a/src/HOL/Analysis/Change_Of_Vars.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Mon Sep 16 23:51:24 2019 +0200
@@ -1171,7 +1171,7 @@
by metis
next
assume RHS: ?rhs
- with borel_measurable_simple_function_limit [of f UNIV, unfolded borel_measurable_UNIV_eq]
+ with borel_measurable_simple_function_limit [of f UNIV, unfolded lebesgue_on_UNIV_eq]
show ?lhs
by (blast intro: order_trans)
qed
@@ -2518,13 +2518,13 @@
have "(\<lambda>x. if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV intS)
then have Df_borel: "(\<lambda>x. if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) \<in> borel_measurable lebesgue"
- using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+ using integrable_imp_measurable lebesgue_on_UNIV_eq by force
have S': "S' \<in> sets lebesgue"
proof -
from Df_borel borel_measurable_vimage_open [of _ UNIV]
have "{x. (if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) \<in> T} \<in> sets lebesgue"
if "open T" for T
- using that unfolding borel_measurable_UNIV_eq
+ using that unfolding lebesgue_on_UNIV_eq
by (fastforce simp add: dest!: spec)
then have "{x. (if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) \<in> -{0}} \<in> sets lebesgue"
using open_Compl by blast
@@ -2649,7 +2649,7 @@
then have "(\<lambda>x. if x \<in> S then ?D x else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV)
then have D_borel: "(\<lambda>x. if x \<in> S then ?D x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
- using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+ using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
then have Dlt: "{x \<in> S. ?D x < 0} \<in> sets lebesgue"
unfolding borel_measurable_vimage_halfspace_component_lt
by (drule_tac x=0 in spec) (auto simp: eq)
@@ -2860,7 +2860,7 @@
then have "(\<lambda>x. if x \<in> S then ?DP x else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV)
then have D_borel: "(\<lambda>x. if x \<in> S then ?DP x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
- using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+ using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
then have SN: "{x \<in> S. ?DP x < 0} \<in> sets lebesgue"
unfolding borel_measurable_vimage_halfspace_component_lt
by (drule_tac x=0 in spec) (auto simp: eq)
@@ -2924,7 +2924,7 @@
then have "(\<lambda>x. if x \<in> T then f x else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV)
then have D_borel: "(\<lambda>x. if x \<in> T then f x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
- using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+ using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
then have TN: "{x \<in> T. f x < 0} \<in> sets lebesgue"
unfolding borel_measurable_vimage_halfspace_component_lt
by (drule_tac x=0 in spec) (auto simp: eq)
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Sep 16 23:51:24 2019 +0200
@@ -15,33 +15,11 @@
lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z"
by (simp add: complex_nonneg_Reals_iff cmod_eq_Re)
-lemma has_derivative_mult_right:
- fixes c:: "'a :: real_normed_algebra"
- shows "(((*) c) has_derivative ((*) c)) F"
-by (rule has_derivative_mult_right [OF has_derivative_ident])
-
-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] .
-
-lemma has_vector_derivative_real_field:
- "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
- using has_derivative_compose[of of_real of_real a _ f "(*) f'"]
- by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
-lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field
-
lemma fact_cancel:
fixes c :: "'a::real_field"
shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)"
using of_nat_neq_0 by force
-lemma bilinear_times:
- fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
- by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
-
-lemma linear_cnj: "linear cnj"
- using bounded_linear.linear[OF bounded_linear_cnj] .
-
lemma vector_derivative_cnj_within:
assumes "at x within A \<noteq> bot" and "f differentiable at x within A"
shows "vector_derivative (\<lambda>z. cnj (f z)) (at x within A) =
@@ -83,8 +61,6 @@
lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
by (intro continuous_on_id continuous_on_norm)
-lemmas DERIV_zero_constant = has_field_derivative_zero_constant
-
lemma DERIV_zero_unique:
assumes "convex S"
and d0: "\<And>x. x\<in>S \<Longrightarrow> (f has_field_derivative 0) (at x within S)"
--- a/src/HOL/Analysis/Conformal_Mappings.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Mon Sep 16 23:51:24 2019 +0200
@@ -4783,8 +4783,7 @@
then show " (f' has_field_derivative of_int po * pp w * (w - p) powr of_int (po - 1)
+ deriv pp w * (w - p) powr of_int po) (at w)"
unfolding f'_def using \<open>w\<noteq>p\<close>
- apply (auto intro!: derivative_eq_intros(35) DERIV_cong[OF has_field_derivative_powr_of_int])
- by (auto intro: derivative_eq_intros)
+ by (auto intro!: derivative_eq_intros DERIV_cong[OF has_field_derivative_powr_of_int])
qed
ultimately show "prin w + anal w = ff' w"
unfolding ff'_def prin_def anal_def
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Sep 16 23:51:24 2019 +0200
@@ -4611,7 +4611,7 @@
have "(UNIV::'a set) \<in> sets lborel"
by simp
then show ?thesis
- using assms borel_measurable_if_D borel_measurable_UNIV_eq integrable_imp_measurable_weak integrable_restrict_UNIV by blast
+ by (metis (mono_tags, lifting) assms borel_measurable_if_D integrable_imp_measurable_weak integrable_restrict_UNIV lebesgue_on_UNIV_eq sets_lebesgue_on_refl)
qed
lemma integrable_iff_integrable_on:
@@ -4767,7 +4767,7 @@
then have "(\<lambda>x. if x \<in> S then f x else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV)
then have borel: "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
- using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+ using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
then show "{x \<in> S. f x \<noteq> 0} \<in> sets lebesgue"
unfolding borel_measurable_vimage_open
by (rule allE [where x = "-{0}"]) auto
@@ -4777,7 +4777,7 @@
then have "(\<lambda>x. if x \<in> T then f x else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV)
then have borel: "(\<lambda>x. if x \<in> T then f x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
- using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+ using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
then show "{x \<in> T. f x \<noteq> 0} \<in> sets lebesgue"
unfolding borel_measurable_vimage_open
by (rule allE [where x = "-{0}"]) auto
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Mon Sep 16 23:51:24 2019 +0200
@@ -1360,16 +1360,30 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes N: "N \<in> null_sets (lebesgue_on S)" and S: "S \<in> sets lebesgue"
shows "f \<in> borel_measurable (lebesgue_on (S-N)) \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S)"
- unfolding in_borel_measurable borel_measurable_UNIV_eq [symmetric] space_lebesgue_on sets_restrict_UNIV
+ unfolding in_borel_measurable space_lebesgue_on sets_restrict_UNIV
proof (intro ball_cong iffI)
show "f -` T \<inter> S \<in> sets (lebesgue_on S)"
if "f -` T \<inter> (S-N) \<in> sets (lebesgue_on (S-N))" for T
- using that assms
- by (smt Diff_Int_distrib completion.complete2 diff_null_sets_lebesgue inf.idem inf_le2 inf_mono lebesgue_on_UNIV_eq null_setsD2 null_sets_restrict_space sets.Diff sets_restrict_space_iff space_lebesgue_on space_restrict_space)
+ proof -
+ have "N \<inter> S = N"
+ by (metis N S inf.orderE null_sets_restrict_space)
+ moreover have "N \<inter> S \<in> sets lebesgue"
+ by (metis N S inf.orderE null_setsD2 null_sets_restrict_space)
+ moreover have "f -` T \<inter> S \<inter> (f -` T \<inter> N) \<in> sets lebesgue"
+ by (metis N S completion.complete inf.absorb2 inf_le2 inf_mono null_sets_restrict_space)
+ ultimately show ?thesis
+ by (metis Diff_Int_distrib Int_Diff_Un S inf_le2 sets.Diff sets.Un sets_restrict_space_iff space_lebesgue_on space_restrict_space that)
+ qed
show "f -` T \<inter> (S-N) \<in> sets (lebesgue_on (S-N))"
if "f -` T \<inter> S \<in> sets (lebesgue_on S)" for T
- using image_eqI inf.commute inf_top_right sets_restrict_space that
- by (smt Int_Diff S sets.Int_space_eq2 sets_restrict_space_iff space_lebesgue_on)
+ proof -
+ have "(S - N) \<inter> f -` T = (S - N) \<inter> (f -` T \<inter> S)"
+ by blast
+ then have "(S - N) \<inter> f -` T \<in> sets.restricted_space lebesgue (S - N)"
+ by (metis S image_iff sets.Int_space_eq2 sets_restrict_space_iff that)
+ then show ?thesis
+ by (simp add: inf.commute sets_restrict_space)
+ qed
qed auto
lemma lebesgue_measurable_diff_null:
@@ -1600,4 +1614,53 @@
using measurable_on_UNIV by blast
qed
+subsection \<open>Measurability on generalisations of the binary product\<close>
+lemma measurable_on_bilinear:
+ fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+ assumes h: "bilinear h" and f: "f measurable_on S" and g: "g measurable_on S"
+ shows "(\<lambda>x. h (f x) (g x)) measurable_on S"
+proof (rule measurable_on_combine [where h = h])
+ show "continuous_on UNIV (\<lambda>x. h (fst x) (snd x))"
+ by (simp add: bilinear_continuous_on_compose [OF continuous_on_fst continuous_on_snd h])
+ show "h 0 0 = 0"
+ by (simp add: bilinear_lzero h)
+qed (auto intro: assms)
+
+lemma borel_measurable_bilinear:
+ fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+ assumes "bilinear h" "f \<in> borel_measurable (lebesgue_on S)" "g \<in> borel_measurable (lebesgue_on S)"
+ and S: "S \<in> sets lebesgue"
+ shows "(\<lambda>x. h (f x) (g x)) \<in> borel_measurable (lebesgue_on S)"
+ using assms measurable_on_bilinear [of h f S g]
+ by (simp flip: measurable_on_iff_borel_measurable)
+
+lemma absolutely_integrable_bounded_measurable_product:
+ fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+ assumes "bilinear h" and f: "f \<in> borel_measurable (lebesgue_on S)" "S \<in> sets lebesgue"
+ and bou: "bounded (f ` S)" and g: "g absolutely_integrable_on S"
+ shows "(\<lambda>x. h (f x) (g x)) absolutely_integrable_on S"
+proof -
+ obtain B where "B > 0" and B: "\<And>x y. norm (h x y) \<le> B * norm x * norm y"
+ using bilinear_bounded_pos \<open>bilinear h\<close> by blast
+ obtain C where "C > 0" and C: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> C"
+ using bounded_pos by (metis bou imageI)
+ show ?thesis
+ proof (rule measurable_bounded_by_integrable_imp_absolutely_integrable [OF _ \<open>S \<in> sets lebesgue\<close>])
+ show "norm (h (f x) (g x)) \<le> B * C * norm(g x)" if "x \<in> S" for x
+ by (meson less_le mult_left_mono mult_right_mono norm_ge_zero order_trans that \<open>B > 0\<close> B C)
+ show "(\<lambda>x. h (f x) (g x)) \<in> borel_measurable (lebesgue_on S)"
+ using \<open>bilinear h\<close> f g
+ by (blast intro: borel_measurable_bilinear dest: absolutely_integrable_measurable)
+ show "(\<lambda>x. B * C * norm(g x)) integrable_on S"
+ using \<open>0 < B\<close> \<open>0 < C\<close> absolutely_integrable_on_def g by auto
+ qed
+qed
+
+lemma absolutely_integrable_bounded_measurable_product_real:
+ fixes f :: "real \<Rightarrow> real"
+ assumes "f \<in> borel_measurable (lebesgue_on S)" "S \<in> sets lebesgue"
+ and "bounded (f ` S)" and "g absolutely_integrable_on S"
+ shows "(\<lambda>x. f x * g x) absolutely_integrable_on S"
+ using absolutely_integrable_bounded_measurable_product bilinear_times assms by blast
+
end
--- a/src/HOL/Analysis/Gamma_Function.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Mon Sep 16 23:51:24 2019 +0200
@@ -1564,7 +1564,7 @@
by (subst of_real_in_nonpos_Ints_iff) (auto elim!: nonpos_Ints_cases')
then have "x \<noteq> 0" by auto
with x have "(rGamma has_field_derivative - rGamma x * Digamma x) (at x)"
- by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex
+ by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_field
simp: Polygamma_of_real rGamma_real_def [abs_def])
thus "let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (x + of_nat k))
\<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in (\<lambda>y. (rGamma y - rGamma x +
@@ -1574,7 +1574,7 @@
next
fix n :: nat
have "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n :: real))"
- by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex
+ by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_field
simp: Polygamma_of_real rGamma_real_def [abs_def])
thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * prod of_nat {1..n} *
(y - x)) /\<^sub>R norm (y - x)) \<midarrow>x::real\<rightarrow> 0"
@@ -1676,7 +1676,7 @@
shows "(ln_Gamma has_field_derivative Digamma x) (at x)"
proof (subst DERIV_cong_ev[OF refl _ refl])
from assms show "((Re \<circ> ln_Gamma \<circ> complex_of_real) has_field_derivative Digamma x) (at x)"
- by (auto intro!: derivative_eq_intros has_vector_derivative_real_complex
+ by (auto intro!: derivative_eq_intros has_vector_derivative_real_field
simp: Polygamma_of_real o_def)
from eventually_nhds_in_nhd[of x "{0<..}"] assms
show "eventually (\<lambda>y. ln_Gamma y = (Re \<circ> ln_Gamma \<circ> of_real) y) (nhds x)"
@@ -2816,7 +2816,7 @@
have "((\<lambda>t. complex_of_real t powr (z - 1)) has_integral
(of_real 1 powr z / z - of_real 0 powr z / z)) {0..1}" using 0
by (intro fundamental_theorem_of_calculus_interior)
- (auto intro!: continuous_intros derivative_eq_intros has_vector_derivative_real_complex)
+ (auto intro!: continuous_intros derivative_eq_intros has_vector_derivative_real_field)
thus ?case by simp
next
case (Suc n)
@@ -2833,9 +2833,9 @@
next
fix t :: real assume t: "t \<in> {0<..<1}"
show "(?f has_vector_derivative ?f' t) (at t)" using t Suc.prems
- by (auto intro!: derivative_eq_intros has_vector_derivative_real_complex)
+ by (auto intro!: derivative_eq_intros has_vector_derivative_real_field)
show "(?g has_vector_derivative ?g' t) (at t)"
- by (rule has_vector_derivative_real_complex derivative_eq_intros refl)+ simp_all
+ by (rule has_vector_derivative_real_field derivative_eq_intros refl)+ simp_all
next
from Suc.prems have [simp]: "z \<noteq> 0" by auto
from Suc.prems have A: "Re (z + of_nat n) > 0" for n by simp
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Mon Sep 16 23:51:24 2019 +0200
@@ -433,10 +433,6 @@
by (auto simp: restrict_space_def)
qed
-lemma integrable_lebesgue_on_UNIV_eq:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
- shows "integrable (lebesgue_on UNIV) f = integrable lebesgue f"
- by (auto simp: integrable_restrict_space)
lemma integral_restrict_Int:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "S \<in> sets lebesgue" "T \<in> sets lebesgue"
@@ -671,9 +667,6 @@
by (simp add: borel_measurable_vimage_open)
qed
-lemma borel_measurable_UNIV_eq: "borel_measurable (lebesgue_on UNIV) = borel_measurable lebesgue"
- by auto
-
lemma borel_measurable_vimage_borel:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
--- a/src/HOL/Analysis/Linear_Algebra.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Mon Sep 16 23:51:24 2019 +0200
@@ -369,6 +369,10 @@
lemma bilinear_radd: "bilinear h \<Longrightarrow> h x (y + z) = h x y + h x z"
by (simp add: bilinear_def linear_iff)
+lemma bilinear_times:
+ fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
+ by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
+
lemma bilinear_lmul: "bilinear h \<Longrightarrow> h (c *\<^sub>R x) y = c *\<^sub>R h x y"
by (simp add: bilinear_def linear_iff)
--- a/src/HOL/Complex.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Complex.thy Mon Sep 16 23:51:24 2019 +0200
@@ -611,6 +611,9 @@
lemma bounded_linear_cnj: "bounded_linear cnj"
using complex_cnj_add complex_cnj_scaleR by (rule bounded_linear_intro [where K=1]) simp
+lemma linear_cnj: "linear cnj"
+ using bounded_linear.linear[OF bounded_linear_cnj] .
+
lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]
and isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
and continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]
--- a/src/HOL/Data_Structures/RBT_Map.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Data_Structures/RBT_Map.thy Mon Sep 16 23:51:24 2019 +0200
@@ -72,8 +72,7 @@
(auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
theorem rbt_update: "rbt t \<Longrightarrow> rbt (update x y t)"
-by (simp add: invc_upd(2) invh_upd(1) color_paint_Black invc_paint_Black invh_paint
- rbt_def update_def)
+by (simp add: invc_upd(2) invh_upd(1) color_paint_Black invh_paint rbt_def update_def)
subsubsection \<open>Deletion\<close>
@@ -102,7 +101,7 @@
qed auto
theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
-by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
+by (metis delete_def rbt_def color_paint_Black del_invc_invh invc2I invh_paint)
interpretation M: Map_by_Ordered
where empty = empty and lookup = lookup and update = update and delete = delete
--- a/src/HOL/Data_Structures/RBT_Set.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy Mon Sep 16 23:51:24 2019 +0200
@@ -107,9 +107,9 @@
"invc (Node l a c r) =
(invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
-fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
-"invc2 Leaf = True" |
-"invc2 (Node l a c r) = (invc l \<and> invc r)"
+text \<open>Weaker version:\<close>
+abbreviation invc2 :: "'a rbt \<Rightarrow> bool" where
+"invc2 t \<equiv> invc(paint Black t)"
fun invh :: "'a rbt \<Rightarrow> bool" where
"invh Leaf = True" |
@@ -124,10 +124,7 @@
lemma color_paint_Black: "color (paint Black t) = Black"
by (cases t) auto
-lemma paint_invc2: "invc2 t \<Longrightarrow> invc2 (paint c t)"
-by (cases t) auto
-
-lemma invc_paint_Black: "invc2 t \<Longrightarrow> invc (paint Black t)"
+lemma paint2: "paint c2 (paint c1 t) = paint c2 t"
by (cases t) auto
lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
@@ -157,23 +154,37 @@
"\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
by (induct l a r rule: baliR.induct) auto
+text \<open>All in one:\<close>
+
+lemma inv_baliR: "\<lbrakk> invh l; invh r; invc l; invc2 r; bheight l = bheight r \<rbrakk>
+ \<Longrightarrow> invc (baliR l a r) \<and> invh (baliR l a r) \<and> bheight (baliR l a r) = Suc (bheight l)"
+by (induct l a r rule: baliR.induct) auto
+
+lemma inv_baliL: "\<lbrakk> invh l; invh r; invc2 l; invc r; bheight l = bheight r \<rbrakk>
+ \<Longrightarrow> invc (baliL l a r) \<and> invh (baliL l a r) \<and> bheight (baliL l a r) = Suc (bheight l)"
+by (induct l a r rule: baliL.induct) auto
subsubsection \<open>Insertion\<close>
-lemma invc_ins: assumes "invc t"
- shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
-using assms
+lemma invc_ins: "invc t \<longrightarrow> invc2 (ins x t) \<and> (color t = Black \<longrightarrow> invc (ins x t))"
by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
-lemma invh_ins: assumes "invh t"
- shows "invh (ins x t)" "bheight (ins x t) = bheight t"
-using assms
+lemma invh_ins: "invh t \<Longrightarrow> invh (ins x t) \<and> bheight (ins x t) = bheight t"
by(induct x t rule: ins.induct)
(auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
-by (simp add: invc_ins(2) invh_ins(1) color_paint_Black invc_paint_Black invh_paint
- rbt_def insert_def)
+by (simp add: invc_ins invh_ins color_paint_Black invh_paint rbt_def insert_def)
+
+text \<open>All in one variant:\<close>
+
+lemma inv_ins: "\<lbrakk> invc t; invh t \<rbrakk> \<Longrightarrow>
+ invc2 (ins x t) \<and> (color t = Black \<longrightarrow> invc (ins x t)) \<and>
+ invh(ins x t) \<and> bheight (ins x t) = bheight t"
+by (induct x t rule: ins.induct) (auto simp: inv_baliL inv_baliR invc2I)
+
+theorem rbt_insert2: "rbt t \<Longrightarrow> rbt (insert x t)"
+by (simp add: inv_ins color_paint_Black invh_paint rbt_def insert_def)
subsubsection \<open>Deletion\<close>
@@ -197,7 +208,7 @@
by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
lemma invc2_baldL: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
-by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I)
+by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint2 invc2I)
lemma invh_baldR_invc:
"\<lbrakk> invh l; invh r; bheight l = bheight r + 1; invc l \<rbrakk>
@@ -209,7 +220,7 @@
by (induct l a r rule: baldR.induct) (simp_all add: invc_baliL)
lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l a r)"
-by (induct l a r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
+by (induct l a r rule: baldR.induct) (auto simp: invc_baliL paint2 invc2I)
lemma invh_combine:
"\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk>
@@ -218,10 +229,8 @@
(auto simp: invh_baldL_Black split: tree.splits color.splits)
lemma invc_combine:
- assumes "invc l" "invc r"
- shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)"
- "invc2 (combine l r)"
-using assms
+ "\<lbrakk> invc l; invc r \<rbrakk> \<Longrightarrow>
+ (color l = Black \<and> color r = Black \<longrightarrow> invc (combine l r)) \<and> invc2 (combine l r)"
by (induct l r rule: combine.induct)
(auto simp: invc_baldL invc2I split: tree.splits color.splits)
@@ -252,7 +261,7 @@
qed auto
theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)"
-by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
+by (metis delete_def rbt_def color_paint_Black del_invc_invh invc2I invh_paint)
text \<open>Overall correctness:\<close>
--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy Mon Sep 16 23:51:24 2019 +0200
@@ -101,7 +101,7 @@
(* unused *)
lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)"
-by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def
+by(simp add: invc2_joinL invc2_joinR invh_joinL invh_joinR invh_paint rbt_def
color_paint_Black join_def)
text \<open>To make sure the the black height is not increased unnecessarily:\<close>
@@ -206,7 +206,7 @@
by(auto simp: bst_paint bst_joinL bst_joinR join_def)
lemma inv_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> invc(join l x r) \<and> invh(join l x r)"
-by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint join_def)
+by (simp add: invc2_joinL invc2_joinR invh_joinL invh_joinR invh_paint join_def)
subsubsection "Interpretation of \<^locale>\<open>Set2_Join\<close> with Red-Black Tree"
--- a/src/HOL/Deriv.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Deriv.thy Mon Sep 16 23:51:24 2019 +0200
@@ -107,6 +107,9 @@
lemmas has_derivative_mult_left [derivative_intros] =
bounded_linear.has_derivative [OF bounded_linear_mult_left]
+lemmas has_derivative_of_real[derivative_intros, simp] =
+ bounded_linear.has_derivative[OF bounded_linear_of_real]
+
lemma has_derivative_add[simp, derivative_intros]:
assumes f: "(f has_derivative f') F"
and g: "(g has_derivative g') F"
@@ -793,6 +796,11 @@
by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
(simp add: has_field_derivative_iff_has_vector_derivative)
+lemma has_vector_derivative_real_field:
+ "(f has_field_derivative f') (at (of_real a)) \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
+ using has_derivative_compose[of of_real of_real a _ f "(*) f'"]
+ by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
+
lemma has_vector_derivative_continuous:
"(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)
@@ -1085,6 +1093,27 @@
lemmas has_derivative_floor[derivative_intros] =
floor_has_real_derivative[THEN DERIV_compose_FDERIV]
+lemma continuous_floor:
+ fixes x::real
+ shows "x \<notin> \<int> \<Longrightarrow> continuous (at x) (real_of_int \<circ> floor)"
+ using floor_has_real_derivative [where f=id]
+ by (auto simp: o_def has_field_derivative_def intro: has_derivative_continuous)
+
+lemma continuous_frac:
+ fixes x::real
+ assumes "x \<notin> \<int>"
+ shows "continuous (at x) frac"
+proof -
+ have "isCont (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x"
+ using continuous_floor [OF assms] by (simp add: o_def)
+ then have *: "continuous (at x) (\<lambda>x. x - real_of_int \<lfloor>x\<rfloor>)"
+ by (intro continuous_intros)
+ moreover have "\<forall>\<^sub>F x in nhds x. frac x = x - real_of_int \<lfloor>x\<rfloor>"
+ by (simp add: frac_def)
+ ultimately show ?thesis
+ by (simp add: LIM_imp_LIM frac_def isCont_def)
+qed
+
text \<open>Caratheodory formulation of derivative at a point\<close>
lemma CARAT_DERIV:
--- a/src/HOL/Topological_Spaces.thy Mon Sep 16 23:25:09 2019 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Sep 16 23:51:24 2019 +0200
@@ -2162,6 +2162,9 @@
lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
unfolding continuous_within by (rule tendsto_ident_at)
+lemma continuous_id[continuous_intros, simp]: "continuous (at x within S) id"
+ by (simp add: id_def)
+
lemma continuous_const[continuous_intros, simp]: "continuous F (\<lambda>x. c)"
unfolding continuous_def by (rule tendsto_const)