new lemmas and movement of lemmas into place
authorpaulson
Mon Sep 21 19:52:13 2015 +0100 (2015-09-21)
changeset 612043e491e34a62e
parent 61203 a8a8eca85801
child 61221 bf194f7c4c8e
new lemmas and movement of lemmas into place
src/HOL/Deriv.thy
src/HOL/Fun.thy
src/HOL/Int.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Real.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Deriv.thy	Mon Sep 21 14:44:32 2015 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Mon Sep 21 19:52:13 2015 +0100
     1.3 @@ -644,6 +644,18 @@
     1.4      ((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
     1.5    by (auto simp: has_vector_derivative_def scaleR_diff_right)
     1.6  
     1.7 +lemma has_vector_derivative_add_const:
     1.8 +     "((\<lambda>t. g t + z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
     1.9 +apply (intro iffI)
    1.10 +apply (drule has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const], simp)
    1.11 +apply (drule has_vector_derivative_add [OF _ has_vector_derivative_const], simp)
    1.12 +done
    1.13 +
    1.14 +lemma has_vector_derivative_diff_const:
    1.15 +     "((\<lambda>t. g t - z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
    1.16 +using has_vector_derivative_add_const [where z = "-z"]
    1.17 +by simp
    1.18 +
    1.19  lemma (in bounded_linear) has_vector_derivative:
    1.20    assumes "(g has_vector_derivative g') F"
    1.21    shows "((\<lambda>x. f (g x)) has_vector_derivative f g') F"
     2.1 --- a/src/HOL/Fun.thy	Mon Sep 21 14:44:32 2015 +0200
     2.2 +++ b/src/HOL/Fun.thy	Mon Sep 21 19:52:13 2015 +0100
     2.3 @@ -69,7 +69,7 @@
     2.4  
     2.5  lemma comp_eq_elim:
     2.6    "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
     2.7 -  by (simp add: fun_eq_iff) 
     2.8 +  by (simp add: fun_eq_iff)
     2.9  
    2.10  lemma comp_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
    2.11    by clarsimp
    2.12 @@ -833,7 +833,7 @@
    2.13    thus False by best
    2.14  qed
    2.15  
    2.16 -subsection \<open>Setup\<close> 
    2.17 +subsection \<open>Setup\<close>
    2.18  
    2.19  subsubsection \<open>Proof tools\<close>
    2.20  
     3.1 --- a/src/HOL/Int.thy	Mon Sep 21 14:44:32 2015 +0200
     3.2 +++ b/src/HOL/Int.thy	Mon Sep 21 19:52:13 2015 +0100
     3.3 @@ -518,7 +518,7 @@
     3.4  lemma int_cases3 [case_names zero pos neg]:
     3.5    fixes k :: int
     3.6    assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
     3.7 -    and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P" 
     3.8 +    and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
     3.9    shows "P"
    3.10  proof (cases k "0::int" rule: linorder_cases)
    3.11    case equal with assms(1) show P by simp
    3.12 @@ -890,7 +890,7 @@
    3.13    moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
    3.14      using that by induct simp
    3.15    ultimately show ?thesis by blast
    3.16 -qed  
    3.17 +qed
    3.18  
    3.19  lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
    3.20  apply (rule sym)
     4.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Sep 21 14:44:32 2015 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Sep 21 19:52:13 2015 +0100
     4.3 @@ -4,58 +4,6 @@
     4.4  imports Complex_Transcendental Weierstrass
     4.5  begin
     4.6  
     4.7 -(*FIXME migrate into libraries*)
     4.8 -
     4.9 -lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)"
    4.10 -  by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
    4.11 -
    4.12 -lemma continuous_on_strong_cong:
    4.13 -  "s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
    4.14 -  by (simp add: simp_implies_def)
    4.15 -
    4.16 -thm image_affinity_atLeastAtMost_div_diff
    4.17 -lemma image_affinity_atLeastAtMost_div:
    4.18 -  fixes c :: "'a::linordered_field"
    4.19 -  shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
    4.20 -            else if 0 \<le> m then {a/m + c .. b/m + c}
    4.21 -            else {b/m + c .. a/m + c})"
    4.22 -  using image_affinity_atLeastAtMost [of "inverse m" c a b]
    4.23 -  by (simp add: field_class.field_divide_inverse algebra_simps)
    4.24 -
    4.25 -thm continuous_on_closed_Un
    4.26 -lemma continuous_on_open_Un:
    4.27 -  "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
    4.28 -  using continuous_on_open_Union [of "{s,t}"] by auto
    4.29 -
    4.30 -thm continuous_on_eq (*REPLACE*)
    4.31 -lemma continuous_on_eq:
    4.32 -  "\<lbrakk>continuous_on s f; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> continuous_on s g"
    4.33 -  unfolding continuous_on_def tendsto_def eventually_at_topological
    4.34 -  by simp
    4.35 -
    4.36 -thm vector_derivative_add_at
    4.37 -lemma vector_derivative_mult_at [simp]:
    4.38 -  fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra"
    4.39 -  shows  "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
    4.40 -   \<Longrightarrow> vector_derivative (\<lambda>x. f x * g x) (at a) = f a * vector_derivative g (at a) + vector_derivative f (at a) * g a"
    4.41 -  by (simp add: vector_derivative_at has_vector_derivative_mult vector_derivative_works [symmetric])
    4.42 -
    4.43 -lemma vector_derivative_scaleR_at [simp]:
    4.44 -    "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
    4.45 -   \<Longrightarrow> vector_derivative (\<lambda>x. f x *\<^sub>R g x) (at a) = f a *\<^sub>R vector_derivative g (at a) + vector_derivative f (at a) *\<^sub>R g a"
    4.46 -apply (rule vector_derivative_at)
    4.47 -apply (rule has_vector_derivative_scaleR)
    4.48 -apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
    4.49 -done
    4.50 -
    4.51 -thm Derivative.vector_diff_chain_at
    4.52 -lemma vector_derivative_chain_at:
    4.53 -  assumes "f differentiable at x" "(g differentiable at (f x))"
    4.54 -  shows "vector_derivative (g \<circ> f) (at x) =
    4.55 -         vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
    4.56 -by (metis Derivative.vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
    4.57 -
    4.58 -
    4.59  subsection \<open>Piecewise differentiable functions\<close>
    4.60  
    4.61  definition piecewise_differentiable_on
    4.62 @@ -89,6 +37,9 @@
    4.63  by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def
    4.64           intro: differentiable_within_subset)
    4.65  
    4.66 +lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on s"
    4.67 +  by (simp add: differentiable_imp_piecewise_differentiable)
    4.68 +
    4.69  lemma piecewise_differentiable_compose:
    4.70      "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s);
    4.71        \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
    4.72 @@ -466,7 +417,7 @@
    4.73      by (auto simp: piecewise_C1_differentiable_on_def continuous_on_add)
    4.74  qed
    4.75  
    4.76 -lemma piecewise_C1_differentiable_C1_diff:
    4.77 +lemma piecewise_C1_differentiable_diff:
    4.78      "\<lbrakk>f piecewise_C1_differentiable_on s;  g piecewise_C1_differentiable_on s\<rbrakk>
    4.79       \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_C1_differentiable_on s"
    4.80    unfolding diff_conv_add_uminus
     5.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Sep 21 14:44:32 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Sep 21 19:52:13 2015 +0100
     5.3 @@ -2277,6 +2277,20 @@
     5.4     \<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
     5.5    by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])
     5.6  
     5.7 +lemma vector_derivative_mult_at [simp]:
     5.8 +  fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra"
     5.9 +  shows  "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
    5.10 +   \<Longrightarrow> vector_derivative (\<lambda>x. f x * g x) (at a) = f a * vector_derivative g (at a) + vector_derivative f (at a) * g a"
    5.11 +  by (simp add: vector_derivative_at has_vector_derivative_mult vector_derivative_works [symmetric])
    5.12 +
    5.13 +lemma vector_derivative_scaleR_at [simp]:
    5.14 +    "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
    5.15 +   \<Longrightarrow> vector_derivative (\<lambda>x. f x *\<^sub>R g x) (at a) = f a *\<^sub>R vector_derivative g (at a) + vector_derivative f (at a) *\<^sub>R g a"
    5.16 +apply (rule vector_derivative_at)
    5.17 +apply (rule has_vector_derivative_scaleR)
    5.18 +apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
    5.19 +done
    5.20 +
    5.21  lemma vector_derivative_within_closed_interval:
    5.22    assumes "a < b"
    5.23      and "x \<in> cbox a b"
    5.24 @@ -2356,4 +2370,10 @@
    5.25      a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
    5.26  using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
    5.27  
    5.28 +lemma vector_derivative_chain_at:
    5.29 +  assumes "f differentiable at x" "(g differentiable at (f x))"
    5.30 +  shows "vector_derivative (g \<circ> f) (at x) =
    5.31 +         vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
    5.32 +by (metis vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
    5.33 +
    5.34  end
     6.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 21 14:44:32 2015 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 21 19:52:13 2015 +0100
     6.3 @@ -496,6 +496,9 @@
     6.4  lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
     6.5    by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
     6.6  
     6.7 +lemma abs_eq_content: "abs (y - x) = (if x\<le>y then content {x .. y} else content {y..x})"
     6.8 +  by (auto simp: content_real)
     6.9 +
    6.10  lemma content_singleton[simp]: "content {a} = 0"
    6.11  proof -
    6.12    have "content (cbox a a) = 0"
    6.13 @@ -6414,133 +6417,75 @@
    6.14    apply (rule has_integral_const)
    6.15    done
    6.16  
    6.17 +lemma integral_has_vector_derivative_continuous_at:
    6.18 +  fixes f :: "real \<Rightarrow> 'a::banach"
    6.19 +  assumes f: "f integrable_on {a..b}"
    6.20 +      and x: "x \<in> {a..b}"
    6.21 +      and fx: "continuous (at x within {a..b}) f"
    6.22 +  shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
    6.23 +proof -
    6.24 +  let ?I = "\<lambda>a b. integral {a..b} f"
    6.25 +  { fix e::real 
    6.26 +    assume "e > 0"
    6.27 +    obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
    6.28 +      using `e>0` fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
    6.29 +    have "norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
    6.30 +           if y: "y \<in> {a..b}" and yx: "\<bar>y - x\<bar> < d" for y  
    6.31 +    proof (cases "y < x")
    6.32 +      case False
    6.33 +      have "f integrable_on {a..y}"
    6.34 +        using f y by (simp add: integrable_subinterval_real)
    6.35 +      then have Idiff: "?I a y - ?I a x = ?I x y" 
    6.36 +        using False x by (simp add: algebra_simps integral_combine)
    6.37 +      have fux_int: "((\<lambda>u. f u - f x) has_integral integral {x..y} f - (y - x) *\<^sub>R f x) {x..y}"
    6.38 +        apply (rule has_integral_sub)
    6.39 +        using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
    6.40 +        using has_integral_const_real [of "f x" x y] False
    6.41 +        apply (simp add: )
    6.42 +        done
    6.43 +      show ?thesis
    6.44 +        using False
    6.45 +        apply (simp add: abs_eq_content del: content_real_if)
    6.46 +        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
    6.47 +        using yx False d x y `e>0` apply (auto simp add: Idiff fux_int)
    6.48 +        done
    6.49 +    next
    6.50 +      case True
    6.51 +      have "f integrable_on {a..x}"
    6.52 +        using f x by (simp add: integrable_subinterval_real)
    6.53 +      then have Idiff: "?I a x - ?I a y = ?I y x" 
    6.54 +        using True x y by (simp add: algebra_simps integral_combine)
    6.55 +      have fux_int: "((\<lambda>u. f u - f x) has_integral integral {y..x} f - (x - y) *\<^sub>R f x) {y..x}"
    6.56 +        apply (rule has_integral_sub)
    6.57 +        using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
    6.58 +        using has_integral_const_real [of "f x" y x] True
    6.59 +        apply (simp add: )
    6.60 +        done
    6.61 +      have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
    6.62 +        using True
    6.63 +        apply (simp add: abs_eq_content del: content_real_if)
    6.64 +        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
    6.65 +        using yx True d x y `e>0` apply (auto simp add: Idiff fux_int)
    6.66 +        done
    6.67 +      then show ?thesis
    6.68 +        by (simp add: algebra_simps norm_minus_commute)
    6.69 +    qed
    6.70 +    then have "\<exists>d>0. \<forall>y\<in>{a..b}. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
    6.71 +      using `d>0` by blast 
    6.72 +  } 
    6.73 +  then show ?thesis
    6.74 +    by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left)
    6.75 +qed
    6.76 +
    6.77  lemma integral_has_vector_derivative:
    6.78    fixes f :: "real \<Rightarrow> 'a::banach"
    6.79    assumes "continuous_on {a .. b} f"
    6.80      and "x \<in> {a .. b}"
    6.81    shows "((\<lambda>u. integral {a .. u} f) has_vector_derivative f(x)) (at x within {a .. b})"
    6.82 -  unfolding has_vector_derivative_def has_derivative_within_alt
    6.83 -  apply safe
    6.84 -  apply (rule bounded_linear_scaleR_left)
    6.85 -proof -
    6.86 -  fix e :: real
    6.87 -  assume e: "e > 0"
    6.88 -  note compact_uniformly_continuous[OF assms(1) compact_Icc,unfolded uniformly_continuous_on_def]
    6.89 -  from this[rule_format,OF e] guess d by (elim conjE exE) note d=this[rule_format]
    6.90 -  let ?I = "\<lambda>a b. integral {a .. b} f"
    6.91 -  show "\<exists>d>0. \<forall>y\<in>{a .. b}. norm (y - x) < d \<longrightarrow>
    6.92 -    norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)"
    6.93 -  proof (rule, rule, rule d, safe, goal_cases)
    6.94 -    case prems: (1 y)
    6.95 -    show ?case
    6.96 -    proof (cases "y < x")
    6.97 -      case False
    6.98 -      have "f integrable_on {a .. y}"
    6.99 -        apply (rule integrable_subinterval_real,rule integrable_continuous_real)
   6.100 -        apply (rule assms)
   6.101 -        unfolding not_less
   6.102 -        using assms(2) prems
   6.103 -        apply auto
   6.104 -        done
   6.105 -      then have *: "?I a y - ?I a x = ?I x y"
   6.106 -        unfolding algebra_simps
   6.107 -        apply (subst eq_commute)
   6.108 -        apply (rule integral_combine)
   6.109 -        using False
   6.110 -        unfolding not_less
   6.111 -        using assms(2) prems
   6.112 -        apply auto
   6.113 -        done
   6.114 -      have **: "norm (y - x) = content {x .. y}"
   6.115 -        using False by (auto simp: content_real)
   6.116 -      show ?thesis
   6.117 -        unfolding **
   6.118 -        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
   6.119 -        unfolding *
   6.120 -        defer
   6.121 -        apply (rule has_integral_sub)
   6.122 -        apply (rule integrable_integral)
   6.123 -        apply (rule integrable_subinterval_real)
   6.124 -        apply (rule integrable_continuous_real)
   6.125 -        apply (rule assms)+
   6.126 -      proof -
   6.127 -        show "{x .. y} \<subseteq> {a .. b}"
   6.128 -          using prems assms(2) by auto
   6.129 -        have *: "y - x = norm (y - x)"
   6.130 -          using False by auto
   6.131 -        show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x .. y}"
   6.132 -          apply (subst *)
   6.133 -          unfolding **
   6.134 -          by blast
   6.135 -        show "\<forall>xa\<in>{x .. y}. norm (f xa - f x) \<le> e"
   6.136 -          apply safe
   6.137 -          apply (rule less_imp_le)
   6.138 -          apply (rule d(2)[unfolded dist_norm])
   6.139 -          using assms(2)
   6.140 -          using prems
   6.141 -          apply auto
   6.142 -          done
   6.143 -      qed (insert e, auto)
   6.144 -    next
   6.145 -      case True
   6.146 -      have "f integrable_on cbox a x"
   6.147 -        apply (rule integrable_subinterval,rule integrable_continuous)
   6.148 -        unfolding box_real
   6.149 -        apply (rule assms)+
   6.150 -        unfolding not_less
   6.151 -        using assms(2) prems
   6.152 -        apply auto
   6.153 -        done
   6.154 -      then have *: "?I a x - ?I a y = ?I y x"
   6.155 -        unfolding algebra_simps
   6.156 -        apply (subst eq_commute)
   6.157 -        apply (rule integral_combine)
   6.158 -        using True using assms(2) prems
   6.159 -        apply auto
   6.160 -        done
   6.161 -      have **: "norm (y - x) = content {y .. x}"
   6.162 -        apply (subst content_real)
   6.163 -        using True
   6.164 -        unfolding not_less
   6.165 -        apply auto
   6.166 -        done
   6.167 -      have ***: "\<And>fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)"
   6.168 -        unfolding scaleR_left.diff by auto
   6.169 -      show ?thesis
   6.170 -        apply (subst ***)
   6.171 -        unfolding norm_minus_cancel **
   6.172 -        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
   6.173 -        unfolding *
   6.174 -        unfolding o_def
   6.175 -        defer
   6.176 -        apply (rule has_integral_sub)
   6.177 -        apply (subst minus_minus[symmetric])
   6.178 -        unfolding minus_minus
   6.179 -        apply (rule integrable_integral)
   6.180 -        apply (rule integrable_subinterval_real,rule integrable_continuous_real)
   6.181 -        apply (rule assms)+
   6.182 -      proof -
   6.183 -        show "{y .. x} \<subseteq> {a .. b}"
   6.184 -          using prems assms(2) by auto
   6.185 -        have *: "x - y = norm (y - x)"
   6.186 -          using True by auto
   6.187 -        show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y .. x}"
   6.188 -          apply (subst *)
   6.189 -          unfolding **
   6.190 -          apply blast
   6.191 -          done
   6.192 -        show "\<forall>xa\<in>{y .. x}. norm (f xa - f x) \<le> e"
   6.193 -          apply safe
   6.194 -          apply (rule less_imp_le)
   6.195 -          apply (rule d(2)[unfolded dist_norm])
   6.196 -          using assms(2)
   6.197 -          using prems
   6.198 -          apply auto
   6.199 -          done
   6.200 -      qed (insert e, auto)
   6.201 -    qed
   6.202 -  qed
   6.203 -qed
   6.204 +apply (rule integral_has_vector_derivative_continuous_at [OF integrable_continuous_real])
   6.205 +using assms
   6.206 +apply (auto simp: continuous_on_eq_continuous_within)
   6.207 +done
   6.208  
   6.209  lemma antiderivative_continuous:
   6.210    fixes q b :: real
     7.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Sep 21 14:44:32 2015 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Sep 21 19:52:13 2015 +0100
     7.3 @@ -437,11 +437,8 @@
     7.4    apply (auto simp: continuous_on_op_minus)
     7.5    done
     7.6  
     7.7 -lemma forall_01_trivial: "(\<forall>x\<in>{0..1}. x \<le> 0 \<longrightarrow> P x) \<longleftrightarrow> P (0::real)"
     7.8 -  by auto
     7.9 -
    7.10 -lemma forall_half1_trivial: "(\<forall>x\<in>{1/2..1}. x * 2 \<le> 1 \<longrightarrow> P x) \<longleftrightarrow> P (1/2::real)"
    7.11 -  by auto (metis add_divide_distrib mult_2_right real_sum_of_halves)
    7.12 +lemma half_bounded_equal: "1 \<le> x * 2 \<Longrightarrow> x * 2 \<le> 1 \<longleftrightarrow> x = (1/2::real)"
    7.13 +  by simp
    7.14  
    7.15  lemma continuous_on_joinpaths:
    7.16    assumes "continuous_on {0..1} g1" "continuous_on {0..1} g2" "pathfinish g1 = pathstart g2"
    7.17 @@ -451,17 +448,17 @@
    7.18      by auto
    7.19    have gg: "g2 0 = g1 1"
    7.20      by (metis assms(3) pathfinish_def pathstart_def)
    7.21 -  have 1: "continuous_on {0..1 / 2} (g1 +++ g2)"
    7.22 +  have 1: "continuous_on {0..1/2} (g1 +++ g2)"
    7.23      apply (rule continuous_on_eq [of _ "g1 o (\<lambda>x. 2*x)"])
    7.24 -    apply (simp add: joinpaths_def)
    7.25 -    apply (rule continuous_intros | simp add: assms)+
    7.26 +    apply (rule continuous_intros | simp add: joinpaths_def assms)+
    7.27      done
    7.28 -  have 2: "continuous_on {1 / 2..1} (g1 +++ g2)"
    7.29 -    apply (rule continuous_on_eq [of _ "g2 o (\<lambda>x. 2*x-1)"])
    7.30 -    apply (simp add: joinpaths_def)
    7.31 -    apply (rule continuous_intros | simp add: forall_half1_trivial gg)+
    7.32 -    apply (rule continuous_on_subset)
    7.33 -    apply (rule assms, auto)
    7.34 +  have "continuous_on {1/2..1} (g2 o (\<lambda>x. 2*x-1))"
    7.35 +    apply (rule continuous_on_subset [of "{1/2..1}"])
    7.36 +    apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff assms)+
    7.37 +    done
    7.38 +  then have 2: "continuous_on {1/2..1} (g1 +++ g2)"
    7.39 +    apply (rule continuous_on_eq [of "{1/2..1}" "g2 o (\<lambda>x. 2*x-1)"])
    7.40 +    apply (rule assms continuous_intros | simp add: joinpaths_def mult.commute half_bounded_equal gg)+
    7.41      done
    7.42    show ?thesis
    7.43      apply (subst *)
    7.44 @@ -800,7 +797,6 @@
    7.45      apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"])
    7.46      prefer 3
    7.47      apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"])
    7.48 -    defer
    7.49      prefer 3
    7.50      apply (rule continuous_intros)+
    7.51      prefer 2
     8.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 21 14:44:32 2015 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 21 19:52:13 2015 +0100
     8.3 @@ -2309,13 +2309,7 @@
     8.4  
     8.5  subsection \<open>More properties of closed balls\<close>
     8.6  
     8.7 -lemma closed_vimage: (* TODO: move to Topological_Spaces.thy *)
     8.8 -  assumes "closed s" and "continuous_on UNIV f"
     8.9 -  shows "closed (vimage f s)"
    8.10 -  using assms unfolding continuous_on_closed_vimage [OF closed_UNIV]
    8.11 -  by simp
    8.12 -
    8.13 -lemma closed_cball: "closed (cball x e)"
    8.14 +lemma closed_cball [iff]: "closed (cball x e)"
    8.15  proof -
    8.16    have "closed (dist x -` {..e})"
    8.17      by (intro closed_vimage closed_atMost continuous_intros)
    8.18 @@ -4663,7 +4657,7 @@
    8.19    by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE)
    8.20  
    8.21  lemma continuous_on_eq:
    8.22 -  "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
    8.23 +  "\<lbrakk>continuous_on s f; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> continuous_on s g"
    8.24    unfolding continuous_on_def tendsto_def eventually_at_topological
    8.25    by simp
    8.26  
     9.1 --- a/src/HOL/Real.thy	Mon Sep 21 14:44:32 2015 +0200
     9.2 +++ b/src/HOL/Real.thy	Mon Sep 21 19:52:13 2015 +0100
     9.3 @@ -22,6 +22,13 @@
     9.4  
     9.5  subsection \<open>Preliminary lemmas\<close>
     9.6  
     9.7 +lemma inj_add_left [simp]: 
     9.8 +  fixes x :: "'a::cancel_semigroup_add" shows "inj (op+ x)"
     9.9 +by (meson add_left_imp_eq injI)
    9.10 +
    9.11 +lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)"
    9.12 +  by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
    9.13 +
    9.14  lemma add_diff_add:
    9.15    fixes a b c d :: "'a::ab_group_add"
    9.16    shows "(a + c) - (b + d) = (a - b) + (c - d)"
    10.1 --- a/src/HOL/Set_Interval.thy	Mon Sep 21 14:44:32 2015 +0200
    10.2 +++ b/src/HOL/Set_Interval.thy	Mon Sep 21 19:52:13 2015 +0100
    10.3 @@ -863,6 +863,14 @@
    10.4    using image_affinity_atLeastAtMost [of m "-c" a b]
    10.5    by simp
    10.6  
    10.7 +lemma image_affinity_atLeastAtMost_div:
    10.8 +  fixes c :: "'a::linordered_field"
    10.9 +  shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
   10.10 +            else if 0 \<le> m then {a/m + c .. b/m + c}
   10.11 +            else {b/m + c .. a/m + c})"
   10.12 +  using image_affinity_atLeastAtMost [of "inverse m" c a b]
   10.13 +  by (simp add: field_class.field_divide_inverse algebra_simps)
   10.14 +    
   10.15  lemma image_affinity_atLeastAtMost_div_diff:
   10.16    fixes c :: "'a::linordered_field"
   10.17    shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
    11.1 --- a/src/HOL/Topological_Spaces.thy	Mon Sep 21 14:44:32 2015 +0200
    11.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Sep 21 19:52:13 2015 +0100
    11.3 @@ -1392,6 +1392,10 @@
    11.4    "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
    11.5    unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
    11.6  
    11.7 +lemma continuous_on_open_Un:
    11.8 +  "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
    11.9 +  using continuous_on_open_Union [of "{s,t}"] by auto
   11.10 +
   11.11  lemma continuous_on_closed_Un:
   11.12    "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
   11.13    by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)