new material for multivariate analysis, etc.
authorpaulson
Mon Jul 20 23:12:50 2015 +0100 (2015-07-20)
changeset 60762bf0c76ccee8d
parent 60761 a443b08281e2
child 60763 b8170925c848
new material for multivariate analysis, etc.
src/HOL/Finite_Set.thy
src/HOL/Groups.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Jul 20 11:40:43 2015 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Jul 20 23:12:50 2015 +0100
     1.3 @@ -1249,6 +1249,12 @@
     1.4  apply(simp del:insert_Diff_single)
     1.5  done
     1.6  
     1.7 +lemma card_insert_le_m1: "n>0 \<Longrightarrow> card y \<le> n-1 \<Longrightarrow> card (insert x y) \<le> n"
     1.8 +  apply (cases "finite y")
     1.9 +  apply (cases "x \<in> y")
    1.10 +  apply (auto simp: insert_absorb)
    1.11 +  done
    1.12 +
    1.13  lemma card_Diff_singleton:
    1.14    "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
    1.15    by (simp add: card_Suc_Diff1 [symmetric])
     2.1 --- a/src/HOL/Groups.thy	Mon Jul 20 11:40:43 2015 +0200
     2.2 +++ b/src/HOL/Groups.thy	Mon Jul 20 23:12:50 2015 +0100
     2.3 @@ -1372,6 +1372,15 @@
     2.4  
     2.5  end
     2.6  
     2.7 +lemma dense_eq0_I:
     2.8 +  fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
     2.9 +  shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
    2.10 +  apply (cases "abs x=0", simp)
    2.11 +  apply (simp only: zero_less_abs_iff [symmetric])
    2.12 +  apply (drule dense)
    2.13 +  apply (auto simp add: not_less [symmetric])
    2.14 +  done
    2.15 +
    2.16  hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
    2.17  
    2.18  lemmas add_0 = add_0_left -- \<open>FIXME duplicate\<close>
     3.1 --- a/src/HOL/Library/Extended_Real.thy	Mon Jul 20 11:40:43 2015 +0200
     3.2 +++ b/src/HOL/Library/Extended_Real.thy	Mon Jul 20 23:12:50 2015 +0100
     3.3 @@ -1820,7 +1820,7 @@
     3.4      using * by (force simp: bot_ereal_def)
     3.5    then show "bdd_above A" "A \<noteq> {}"
     3.6      by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
     3.7 -qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
     3.8 +qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
     3.9  
    3.10  lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
    3.11    using ereal_Sup[of "f`A"] by auto
    3.12 @@ -1833,7 +1833,7 @@
    3.13      using * by (force simp: top_ereal_def)
    3.14    then show "bdd_below A" "A \<noteq> {}"
    3.15      by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
    3.16 -qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
    3.17 +qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
    3.18  
    3.19  lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))"
    3.20    using ereal_Inf[of "f`A"] by auto
    3.21 @@ -1947,7 +1947,7 @@
    3.22    assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
    3.23      unfolding Sup_image_eq[symmetric]
    3.24      by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
    3.25 -       (auto simp: continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
    3.26 +       (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
    3.27  qed
    3.28  
    3.29  lemma SUP_ereal_add_right:
    3.30 @@ -2070,7 +2070,7 @@
    3.31    assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
    3.32      unfolding SUP_def
    3.33      by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
    3.34 -       (auto simp: mono_def continuous_at continuous_at_within \<open>I \<noteq> {}\<close>
    3.35 +       (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
    3.36               intro!: ereal_mult_left_mono c)
    3.37  qed
    3.38  
     4.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 20 11:40:43 2015 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 20 23:12:50 2015 +0100
     4.3 @@ -1437,7 +1437,7 @@
     4.4  
     4.5  subsection \<open>Convex hull\<close>
     4.6  
     4.7 -lemma convex_convex_hull: "convex (convex hull s)"
     4.8 +lemma convex_convex_hull [iff]: "convex (convex hull s)"
     4.9    unfolding hull_def
    4.10    using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
    4.11    by auto
    4.12 @@ -6312,6 +6312,10 @@
    4.13    "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"
    4.14    unfolding convex_alt closed_segment_def by auto
    4.15  
    4.16 +lemma closed_segment_subset_convex_hull:
    4.17 +    "\<lbrakk>x \<in> convex hull s; y \<in> convex hull s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull s"
    4.18 +  using convex_contains_segment by blast  
    4.19 +
    4.20  lemma convex_imp_starlike:
    4.21    "convex s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> starlike s"
    4.22    unfolding convex_contains_segment starlike_def by auto
    4.23 @@ -8906,8 +8910,27 @@
    4.24    then show ?thesis
    4.25      using \<open>y < x\<close> by (simp add: field_simps)
    4.26  qed simp
    4.27 +
    4.28  subsection\<open>Explicit formulas for interior and relative interior of convex hull\<close>
    4.29 - 
    4.30 +
    4.31 +lemma interior_atLeastAtMost [simp]:
    4.32 +  fixes a::real shows "interior {a..b} = {a<..<b}"
    4.33 +  using interior_cbox [of a b] by auto
    4.34 +
    4.35 +lemma interior_atLeastLessThan [simp]:
    4.36 +  fixes a::real shows "interior {a..<b} = {a<..<b}"
    4.37 +  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_inter interior_interior interior_real_semiline)
    4.38 +
    4.39 +lemma interior_lessThanAtMost [simp]:
    4.40 +  fixes a::real shows "interior {a<..b} = {a<..<b}"
    4.41 +  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_inter
    4.42 +            interior_interior interior_real_semiline)
    4.43 +
    4.44 +lemma at_within_closed_interval:
    4.45 +    fixes x::real
    4.46 +    shows "a < x \<Longrightarrow> x < b \<Longrightarrow> (at x within {a..b}) = at x"
    4.47 +  by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost)
    4.48 +
    4.49  lemma affine_independent_convex_affine_hull:
    4.50    fixes s :: "'a::euclidean_space set"
    4.51    assumes "~affine_dependent s" "t \<subseteq> s"
    4.52 @@ -9276,7 +9299,7 @@
    4.53  
    4.54  lemma interior_convex_hull_eq_empty:
    4.55    fixes s :: "'a::euclidean_space set"
    4.56 -  assumes "card s = Suc (DIM ('a))" "x \<in> s"
    4.57 +  assumes "card s = Suc (DIM ('a))"
    4.58    shows   "interior(convex hull s) = {} \<longleftrightarrow> affine_dependent s"
    4.59  proof -
    4.60    { fix a b
    4.61 @@ -9294,4 +9317,205 @@
    4.62      done
    4.63  qed
    4.64  
    4.65 +subsection \<open>Coplanarity, and collinearity in terms of affine hull\<close>
    4.66 +
    4.67 +
    4.68 +definition coplanar  where
    4.69 +   "coplanar s \<equiv> \<exists>u v w. s \<subseteq> affine hull {u,v,w}"
    4.70 +
    4.71 +lemma collinear_affine_hull:
    4.72 +  "collinear s \<longleftrightarrow> (\<exists>u v. s \<subseteq> affine hull {u,v})"
    4.73 +proof (cases "s={}")
    4.74 +  case True then show ?thesis
    4.75 +    by simp
    4.76 +next
    4.77 +  case False
    4.78 +  then obtain x where x: "x \<in> s" by auto
    4.79 +  { fix u
    4.80 +    assume *: "\<And>x y. \<lbrakk>x\<in>s; y\<in>s\<rbrakk> \<Longrightarrow> \<exists>c. x - y = c *\<^sub>R u"
    4.81 +    have "\<exists>u v. s \<subseteq> {a *\<^sub>R u + b *\<^sub>R v |a b. a + b = 1}"
    4.82 +      apply (rule_tac x=x in exI)
    4.83 +      apply (rule_tac x="x+u" in exI, clarify)
    4.84 +      apply (erule exE [OF * [OF x]])
    4.85 +      apply (rename_tac c)
    4.86 +      apply (rule_tac x="1+c" in exI)
    4.87 +      apply (rule_tac x="-c" in exI)
    4.88 +      apply (simp add: algebra_simps)
    4.89 +      done
    4.90 +  } moreover
    4.91 +  { fix u v x y
    4.92 +    assume *: "s \<subseteq> {a *\<^sub>R u + b *\<^sub>R v |a b. a + b = 1}"
    4.93 +    have "x\<in>s \<Longrightarrow> y\<in>s \<Longrightarrow> \<exists>c. x - y = c *\<^sub>R (v-u)"
    4.94 +      apply (drule subsetD [OF *])+
    4.95 +      apply simp
    4.96 +      apply clarify
    4.97 +      apply (rename_tac r1 r2)
    4.98 +      apply (rule_tac x="r1-r2" in exI)
    4.99 +      apply (simp add: algebra_simps)
   4.100 +      apply (metis scaleR_left.add)
   4.101 +      done
   4.102 +  } ultimately
   4.103 +  show ?thesis
   4.104 +  unfolding collinear_def affine_hull_2
   4.105 +    by blast
   4.106 +qed
   4.107 +
   4.108 +lemma collinear_imp_coplanar:
   4.109 +  "collinear s ==> coplanar s"
   4.110 +by (metis collinear_affine_hull coplanar_def insert_absorb2)
   4.111 +
   4.112 +lemma collinear_small:
   4.113 +  assumes "finite s" "card s \<le> 2"
   4.114 +    shows "collinear s"
   4.115 +proof -
   4.116 +  have "card s = 0 \<or> card s = 1 \<or> card s = 2"
   4.117 +    using assms by linarith
   4.118 +  then show ?thesis using assms
   4.119 +    using card_eq_SucD
   4.120 +    by auto (metis collinear_2 numeral_2_eq_2)
   4.121 +qed
   4.122 +
   4.123 +lemma coplanar_small:
   4.124 +  assumes "finite s" "card s \<le> 3"
   4.125 +    shows "coplanar s"
   4.126 +proof -
   4.127 +  have "card s \<le> 2 \<or> card s = Suc (Suc (Suc 0))"
   4.128 +    using assms by linarith
   4.129 +  then show ?thesis using assms
   4.130 +    apply safe
   4.131 +    apply (simp add: collinear_small collinear_imp_coplanar)
   4.132 +    apply (safe dest!: card_eq_SucD)
   4.133 +    apply (auto simp: coplanar_def)
   4.134 +    apply (metis hull_subset insert_subset)
   4.135 +    done
   4.136 +qed
   4.137 +
   4.138 +lemma coplanar_empty: "coplanar {}"
   4.139 +  by (simp add: coplanar_small)
   4.140 +
   4.141 +lemma coplanar_sing: "coplanar {a}"
   4.142 +  by (simp add: coplanar_small)
   4.143 +
   4.144 +lemma coplanar_2: "coplanar {a,b}"
   4.145 +  by (auto simp: card_insert_if coplanar_small)
   4.146 +
   4.147 +lemma coplanar_3: "coplanar {a,b,c}"
   4.148 +  by (auto simp: card_insert_if coplanar_small)
   4.149 +
   4.150 +lemma collinear_affine_hull_collinear: "collinear(affine hull s) \<longleftrightarrow> collinear s"
   4.151 +  unfolding collinear_affine_hull
   4.152 +  by (metis affine_affine_hull subset_hull hull_hull hull_mono)
   4.153 +
   4.154 +lemma coplanar_affine_hull_coplanar: "coplanar(affine hull s) \<longleftrightarrow> coplanar s"
   4.155 +  unfolding coplanar_def
   4.156 +  by (metis affine_affine_hull subset_hull hull_hull hull_mono)
   4.157 +
   4.158 +lemma coplanar_linear_image:
   4.159 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   4.160 +  assumes "coplanar s" "linear f" shows "coplanar(f ` s)"
   4.161 +proof -
   4.162 +  { fix u v w
   4.163 +    assume "s \<subseteq> affine hull {u, v, w}"
   4.164 +    then have "f ` s \<subseteq> f ` (affine hull {u, v, w})"
   4.165 +      by (simp add: image_mono)
   4.166 +    then have "f ` s \<subseteq> affine hull (f ` {u, v, w})"
   4.167 +      by (metis assms(2) linear_conv_bounded_linear affine_hull_linear_image)
   4.168 +  } then
   4.169 +  show ?thesis
   4.170 +    by auto (meson assms(1) coplanar_def)
   4.171 +qed
   4.172 +
   4.173 +(*?  Still not ported
   4.174 +lemma COPLANAR_TRANSLATION_EQ: "coplanar((\<lambda>x. a + x) ` s) \<longleftrightarrow> coplanar s"
   4.175 +  apply (simp add: coplanar_def)
   4.176 +  apply (simp add: Set.image_subset_iff_subset_vimage)
   4.177 +  apply (auto simp:)
   4.178 +  apply (rule_tac x="u-a" in exI)
   4.179 +  apply (rule_tac x="v-a" in exI)
   4.180 +  apply (rule_tac x="w-a" in exI)
   4.181 +  apply (auto simp:)
   4.182 +  apply (drule_tac c="x+a" in subsetD)
   4.183 +  apply (simp add: affine_alt)
   4.184 +
   4.185 +lemma COPLANAR_TRANSLATION:
   4.186 +  !a:real^N s. coplanar s ==> coplanar(IMAGE (\x. a + x) s)"
   4.187 +  REWRITE_TAC[COPLANAR_TRANSLATION_EQ]);;
   4.188 +
   4.189 +lemma coplanar_linear_image_eq:
   4.190 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.191 +  assumes "linear f" "inj f" shows "coplanar(f ` s) = coplanar s"
   4.192 +  MATCH_ACCEPT_TAC(LINEAR_INVARIANT_RULE COPLANAR_LINEAR_IMAGE));;
   4.193 +*)
   4.194 +
   4.195 +lemma coplanar_subset: "\<lbrakk>coplanar t; s \<subseteq> t\<rbrakk> \<Longrightarrow> coplanar s"
   4.196 +  by (meson coplanar_def order_trans)
   4.197 +
   4.198 +lemma affine_hull_3_imp_collinear: "c \<in> affine hull {a,b} \<Longrightarrow> collinear {a,b,c}"
   4.199 +  by (metis collinear_2 collinear_affine_hull_collinear hull_redundant insert_commute)
   4.200 +
   4.201 +lemma collinear_3_imp_in_affine_hull: "\<lbrakk>collinear {a,b,c}; a \<noteq> b\<rbrakk> \<Longrightarrow> c \<in> affine hull {a,b}"
   4.202 +  unfolding collinear_def
   4.203 +  apply clarify
   4.204 +  apply (frule_tac x=b in bspec, blast, drule_tac x=a in bspec, blast, erule exE)
   4.205 +  apply (drule_tac x=c in bspec, blast, drule_tac x=a in bspec, blast, erule exE)
   4.206 +  apply (rename_tac y x)
   4.207 +  apply (simp add: affine_hull_2)
   4.208 +  apply (rule_tac x="1 - x/y" in exI)
   4.209 +  apply (simp add: algebra_simps)
   4.210 +  done
   4.211 +
   4.212 +lemma collinear_3_affine_hull:
   4.213 +  assumes "a \<noteq> b"
   4.214 +    shows "collinear {a,b,c} \<longleftrightarrow> c \<in> affine hull {a,b}"
   4.215 +using affine_hull_3_imp_collinear assms collinear_3_imp_in_affine_hull by blast
   4.216 +
   4.217 +lemma collinear_3_eq_affine_dependent:
   4.218 +  "collinear{a,b,c} \<longleftrightarrow> a = b \<or> a = c \<or> b = c \<or> affine_dependent {a,b,c}"
   4.219 +apply (case_tac "a=b", simp)
   4.220 +apply (case_tac "a=c")
   4.221 +apply (simp add: insert_commute)
   4.222 +apply (case_tac "b=c")
   4.223 +apply (simp add: insert_commute)
   4.224 +apply (auto simp: affine_dependent_def collinear_3_affine_hull insert_Diff_if)
   4.225 +apply (metis collinear_3_affine_hull insert_commute)+
   4.226 +done
   4.227 +
   4.228 +lemma affine_dependent_imp_collinear_3:
   4.229 +  "affine_dependent {a,b,c} \<Longrightarrow> collinear{a,b,c}"
   4.230 +by (simp add: collinear_3_eq_affine_dependent)
   4.231 +
   4.232 +lemma collinear_3: "NO_MATCH 0 x \<Longrightarrow> collinear {x,y,z} \<longleftrightarrow> collinear {0, x-y, z-y}"
   4.233 +  by (auto simp add: collinear_def)
   4.234 +
   4.235 +
   4.236 +thm affine_hull_nonempty
   4.237 +corollary affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
   4.238 +  using affine_hull_nonempty by blast
   4.239 +
   4.240 +lemma affine_hull_2_alt:
   4.241 +  fixes a b :: "'a::real_vector"
   4.242 +  shows "affine hull {a,b} = range (\<lambda>u. a + u *\<^sub>R (b - a))"
   4.243 +apply (simp add: affine_hull_2, safe)
   4.244 +apply (rule_tac x=v in image_eqI)
   4.245 +apply (simp add: algebra_simps)
   4.246 +apply (metis scaleR_add_left scaleR_one, simp)
   4.247 +apply (rule_tac x="1-u" in exI)
   4.248 +apply (simp add: algebra_simps)
   4.249 +done
   4.250 +
   4.251 +lemma interior_convex_hull_3_minimal:
   4.252 +  fixes a :: "'a::euclidean_space"
   4.253 +  shows "\<lbrakk>~ collinear{a,b,c}; DIM('a) = 2\<rbrakk>
   4.254 +         \<Longrightarrow> interior(convex hull {a,b,c}) =
   4.255 +                {v. \<exists>x y z. 0 < x \<and> 0 < y \<and> 0 < z \<and> x + y + z = 1 \<and>
   4.256 +                            x *\<^sub>R a + y *\<^sub>R b + z *\<^sub>R c = v}"
   4.257 +apply (simp add: collinear_3_eq_affine_dependent interior_convex_hull_explicit_minimal, safe)
   4.258 +apply (rule_tac x="u a" in exI, simp)
   4.259 +apply (rule_tac x="u b" in exI, simp)
   4.260 +apply (rule_tac x="u c" in exI, simp)
   4.261 +apply (rename_tac uu x y z)
   4.262 +apply (rule_tac x="\<lambda>r. (if r=a then x else if r=b then y else if r=c then z else 0)" in exI)
   4.263 +apply simp
   4.264 +done
   4.265 +
   4.266  end
     5.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jul 20 11:40:43 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jul 20 23:12:50 2015 +0100
     5.3 @@ -2312,4 +2312,7 @@
     5.4    apply (simp only: o_def real_scaleR_def scaleR_scaleR)
     5.5    done
     5.6  
     5.7 +lemma vector_derivative_const_at [simp]: "vector_derivative (\<lambda>x. c) (at a) = 0"
     5.8 +  by (simp add: vector_derivative_at)
     5.9 +
    5.10  end
     6.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jul 20 11:40:43 2015 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jul 20 23:12:50 2015 +0100
     6.3 @@ -576,6 +576,9 @@
     6.4  lemma content_empty [simp]: "content {} = 0"
     6.5    unfolding content_def by auto
     6.6  
     6.7 +lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
     6.8 +  by (simp add: content_real)
     6.9 +
    6.10  lemma content_subset:
    6.11    assumes "cbox a b \<subseteq> cbox c d"
    6.12    shows "content (cbox a b) \<le> content (cbox c d)"
    6.13 @@ -2467,6 +2470,11 @@
    6.14    shows "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. f x * c) = integral s f * c"
    6.15    by (blast intro:  has_integral_mult_left)
    6.16  
    6.17 +lemma has_integral_mult_right:
    6.18 +  fixes c :: "'a :: real_normed_algebra"
    6.19 +  shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
    6.20 +  using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)
    6.21 +    
    6.22  lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
    6.23    unfolding o_def[symmetric]
    6.24    by (metis has_integral_linear bounded_linear_scaleR_right)
    6.25 @@ -2780,9 +2788,12 @@
    6.26  lemma integrable_on_refl[intro]: "f integrable_on cbox a a"
    6.27    unfolding integrable_on_def by auto
    6.28  
    6.29 -lemma integral_refl: "integral (cbox a a) f = 0"
    6.30 +lemma integral_refl [simp]: "integral (cbox a a) f = 0"
    6.31    by (rule integral_unique) auto
    6.32  
    6.33 +lemma integral_singleton [simp]: "integral {a} f = 0"
    6.34 +  by auto
    6.35 +
    6.36  
    6.37  subsection \<open>Cauchy-type criterion for integrability.\<close>
    6.38  
    6.39 @@ -5394,7 +5405,7 @@
    6.40    apply auto
    6.41    done
    6.42  
    6.43 -lemma negligible_empty[intro]: "negligible {}"
    6.44 +lemma negligible_empty[iff]: "negligible {}"
    6.45    by auto
    6.46  
    6.47  lemma negligible_finite[intro]:
    6.48 @@ -5688,7 +5699,7 @@
    6.49    assumes "monoidal opp"
    6.50    shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a .. b::real} = neutral opp) \<and>
    6.51      (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a .. c}) (f {c .. b}) = f {a .. b}))"
    6.52 -  apply (simp add: operative_def content_real_eq_0)
    6.53 +  apply (simp add: operative_def content_real_eq_0 del: content_real_if)
    6.54  proof safe
    6.55    fix a b c :: real
    6.56    assume as:
    6.57 @@ -6467,7 +6478,7 @@
    6.58          show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x .. y}"
    6.59            apply (subst *)
    6.60            unfolding **
    6.61 -          by auto
    6.62 +          by blast
    6.63          show "\<forall>xa\<in>{x .. y}. norm (f xa - f x) \<le> e"
    6.64            apply safe
    6.65            apply (rule less_imp_le)
    6.66 @@ -6523,7 +6534,7 @@
    6.67          show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y .. x}"
    6.68            apply (subst *)
    6.69            unfolding **
    6.70 -          apply auto
    6.71 +          apply blast
    6.72            done
    6.73          show "\<forall>xa\<in>{y .. x}. norm (f xa - f x) \<le> e"
    6.74            apply safe
    6.75 @@ -12133,11 +12144,6 @@
    6.76    qed
    6.77  qed
    6.78  
    6.79 -lemma dense_eq0_I:
    6.80 -  fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
    6.81 -  shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
    6.82 -by (metis dense not_less zero_less_abs_iff)
    6.83 -
    6.84  lemma integral_Pair_const:
    6.85      "integral (cbox (a,c) (b,d)) (\<lambda>x. k) =
    6.86       integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. k))"
     7.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Jul 20 11:40:43 2015 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Jul 20 23:12:50 2015 +0100
     7.3 @@ -462,6 +462,12 @@
     7.4    apply auto
     7.5    done
     7.6  
     7.7 +lemma approachable_lt_le2:  --{*like the above, but pushes aside an extra formula*}
     7.8 +    "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
     7.9 +  apply auto
    7.10 +  apply (rule_tac x="d/2" in exI, auto)
    7.11 +  done
    7.12 +
    7.13  lemma triangle_lemma:
    7.14    fixes x y z :: real
    7.15    assumes x: "0 \<le> x"
    7.16 @@ -2933,13 +2939,13 @@
    7.17  definition collinear :: "'a::real_vector set \<Rightarrow> bool"
    7.18    where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
    7.19  
    7.20 -lemma collinear_empty: "collinear {}"
    7.21 +lemma collinear_empty [iff]: "collinear {}"
    7.22    by (simp add: collinear_def)
    7.23  
    7.24 -lemma collinear_sing: "collinear {x}"
    7.25 +lemma collinear_sing [iff]: "collinear {x}"
    7.26    by (simp add: collinear_def)
    7.27  
    7.28 -lemma collinear_2: "collinear {x, y}"
    7.29 +lemma collinear_2 [iff]: "collinear {x, y}"
    7.30    apply (simp add: collinear_def)
    7.31    apply (rule exI[where x="x - y"])
    7.32    apply auto
     8.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jul 20 11:40:43 2015 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jul 20 23:12:50 2015 +0100
     8.3 @@ -1826,7 +1826,7 @@
     8.4  
     8.5  text\<open>Interrelations between restricted and unrestricted limits.\<close>
     8.6  
     8.7 -lemma Lim_at_within: (* FIXME: rename *)
     8.8 +lemma Lim_at_imp_Lim_at_within: 
     8.9    "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
    8.10    by (metis order_refl filterlim_mono subset_UNIV at_le)
    8.11  
    8.12 @@ -2728,6 +2728,11 @@
    8.13    apply arith
    8.14    done
    8.15  
    8.16 +lemma bounded_pos_less: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x < b)"
    8.17 +  apply (simp add: bounded_pos)
    8.18 +  apply (safe; rule_tac x="b+1" in exI; force)
    8.19 +  done
    8.20 +
    8.21  lemma Bseq_eq_bounded:
    8.22    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    8.23    shows "Bseq f \<longleftrightarrow> bounded (range f)"
    8.24 @@ -4636,7 +4641,7 @@
    8.25  
    8.26  lemma continuous_at_imp_continuous_within:
    8.27    "continuous (at x) f \<Longrightarrow> continuous (at x within s) f"
    8.28 -  unfolding continuous_within continuous_at using Lim_at_within by auto
    8.29 +  unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto
    8.30  
    8.31  lemma Lim_trivial_limit: "trivial_limit net \<Longrightarrow> (f ---> l) net"
    8.32    by simp
     9.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Jul 20 11:40:43 2015 +0200
     9.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jul 20 23:12:50 2015 +0100
     9.3 @@ -862,6 +862,25 @@
     9.4    shows "norm (x ^ n) = norm x ^ n"
     9.5  by (induct n) (simp_all add: norm_mult)
     9.6  
     9.7 +lemma norm_mult_numeral1 [simp]:
     9.8 +  fixes a b :: "'a::{real_normed_field, field}"
     9.9 +  shows "norm (numeral w * a) = numeral w * norm a"
    9.10 +by (simp add: norm_mult)
    9.11 +
    9.12 +lemma norm_mult_numeral2 [simp]:
    9.13 +  fixes a b :: "'a::{real_normed_field, field}"
    9.14 +  shows "norm (a * numeral w) = norm a * numeral w"
    9.15 +by (simp add: norm_mult)
    9.16 +
    9.17 +lemma norm_divide_numeral [simp]:
    9.18 +  fixes a b :: "'a::{real_normed_field, field}"
    9.19 +  shows "norm (a / numeral w) = norm a / numeral w"
    9.20 +by (simp add: norm_divide)
    9.21 +
    9.22 +lemma norm_of_real_diff [simp]:
    9.23 +    "norm (of_real b - of_real a :: 'a::real_normed_algebra_1) \<le> \<bar>b - a\<bar>"
    9.24 +  by (metis norm_of_real of_real_diff order_refl)
    9.25 +
    9.26  text\<open>Despite a superficial resemblance, @{text norm_eq_1} is not relevant.\<close>
    9.27  lemma square_norm_one:
    9.28    fixes x :: "'a::real_normed_div_algebra"
    10.1 --- a/src/HOL/Set_Interval.thy	Mon Jul 20 11:40:43 2015 +0200
    10.2 +++ b/src/HOL/Set_Interval.thy	Mon Jul 20 23:12:50 2015 +0100
    10.3 @@ -1357,6 +1357,10 @@
    10.4    "{..< n} - {..< m} = {m ..< n}"
    10.5    by auto
    10.6  
    10.7 +lemma (in linorder) atLeastAtMost_diff_ends:
    10.8 +  "{a..b} - {a, b} = {a<..<b}"
    10.9 +  by auto
   10.10 +
   10.11  
   10.12  subsubsection \<open>Some Subset Conditions\<close>
   10.13  
    11.1 --- a/src/HOL/Topological_Spaces.thy	Mon Jul 20 11:40:43 2015 +0200
    11.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Jul 20 23:12:50 2015 +0100
    11.3 @@ -1526,7 +1526,7 @@
    11.4  lemma isCont_def: "isCont f a \<longleftrightarrow> f -- a --> f a"
    11.5    by (rule continuous_at)
    11.6  
    11.7 -lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
    11.8 +lemma continuous_at_imp_continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
    11.9    by (auto intro: tendsto_mono at_le simp: continuous_at continuous_within)
   11.10  
   11.11  lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
   11.12 @@ -1536,7 +1536,7 @@
   11.13    unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
   11.14  
   11.15  lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
   11.16 -  by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
   11.17 +  by (auto intro: continuous_at_imp_continuous_at_within simp: continuous_on_eq_continuous_within)
   11.18  
   11.19  lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   11.20    unfolding isCont_def by (rule tendsto_compose)
   11.21 @@ -1549,7 +1549,7 @@
   11.22  
   11.23  lemma continuous_within_compose3:
   11.24    "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
   11.25 -  using continuous_within_compose2[of x s f g] by (simp add: continuous_at_within)
   11.26 +  using continuous_within_compose2[of x s f g] by (simp add: continuous_at_imp_continuous_at_within)
   11.27  
   11.28  lemma filtermap_nhds_open_map:
   11.29    assumes cont: "isCont f a" and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
    12.1 --- a/src/HOL/Transcendental.thy	Mon Jul 20 11:40:43 2015 +0200
    12.2 +++ b/src/HOL/Transcendental.thy	Mon Jul 20 23:12:50 2015 +0100
    12.3 @@ -748,7 +748,7 @@
    12.4      shows "summable (\<lambda>n. diffs c n * x^n)"
    12.5    apply (rule termdiff_converges [where K = "1 + norm x"])
    12.6    using assms
    12.7 -  apply (auto simp: )
    12.8 +  apply auto
    12.9    done
   12.10  
   12.11  lemma termdiffs_strong:
   12.12 @@ -757,17 +757,16 @@
   12.13        and K: "norm x < norm K"
   12.14    shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. diffs c n * x^n)"
   12.15  proof -
   12.16 -  have [simp]: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
   12.17 +  have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
   12.18      using K
   12.19      apply (auto simp: norm_divide)
   12.20      apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"])
   12.21      apply (auto simp: mult_2_right norm_triangle_mono)
   12.22      done
   12.23 +  then have [simp]: "norm ((of_real (norm K) + of_real (norm x)) :: 'a) < norm K * 2"
   12.24 +    by simp
   12.25    have "summable (\<lambda>n. c n * (of_real (norm x + norm K) / 2) ^ n)"
   12.26 -    apply (rule summable_norm_cancel [OF powser_insidea [OF sm]])
   12.27 -    using K
   12.28 -    apply (auto simp: algebra_simps)
   12.29 -    done
   12.30 +    by (metis K2 summable_norm_cancel [OF powser_insidea [OF sm]] add.commute of_real_add)
   12.31    moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs c n * x ^ n)"
   12.32      by (blast intro: sm termdiff_converges powser_inside)
   12.33    moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs(diffs c) n * x ^ n)"
   12.34 @@ -776,8 +775,6 @@
   12.35      apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
   12.36      apply (auto simp: algebra_simps)
   12.37      using K
   12.38 -    apply (simp add: norm_divide)
   12.39 -    apply (rule less_le_trans [of _ "of_real (norm K) + of_real (norm x)"])
   12.40      apply (simp_all add: of_real_add [symmetric] del: of_real_add)
   12.41      done
   12.42  qed