# HG changeset patch
# User paulson
# Date 1437430370 -3600
# Node ID bf0c76ccee8d579013a94c5ef88b8dd225155245
# Parent  a443b08281e221082864b544d05c1bdc1e4f7ff3
new material for multivariate analysis, etc.

diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -1249,6 +1249,12 @@
 apply(simp del:insert_Diff_single)
 done
 
+lemma card_insert_le_m1: "n>0 \<Longrightarrow> card y \<le> n-1 \<Longrightarrow> card (insert x y) \<le> n"
+  apply (cases "finite y")
+  apply (cases "x \<in> y")
+  apply (auto simp: insert_absorb)
+  done
+
 lemma card_Diff_singleton:
   "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
   by (simp add: card_Suc_Diff1 [symmetric])
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Groups.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -1372,6 +1372,15 @@
 
 end
 
+lemma dense_eq0_I:
+  fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
+  shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
+  apply (cases "abs x=0", simp)
+  apply (simp only: zero_less_abs_iff [symmetric])
+  apply (drule dense)
+  apply (auto simp add: not_less [symmetric])
+  done
+
 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
 
 lemmas add_0 = add_0_left -- \<open>FIXME duplicate\<close>
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -1820,7 +1820,7 @@
     using * by (force simp: bot_ereal_def)
   then show "bdd_above A" "A \<noteq> {}"
     by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
-qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
+qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
 
 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))"
   using ereal_Sup[of "f`A"] by auto
@@ -1833,7 +1833,7 @@
     using * by (force simp: top_ereal_def)
   then show "bdd_below A" "A \<noteq> {}"
     by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
-qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
+qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
 
 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))"
   using ereal_Inf[of "f`A"] by auto
@@ -1947,7 +1947,7 @@
   assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
     unfolding Sup_image_eq[symmetric]
     by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
-       (auto simp: continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
+       (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
 qed
 
 lemma SUP_ereal_add_right:
@@ -2070,7 +2070,7 @@
   assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
     unfolding SUP_def
     by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
-       (auto simp: mono_def continuous_at continuous_at_within \<open>I \<noteq> {}\<close>
+       (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
              intro!: ereal_mult_left_mono c)
 qed
 
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -1437,7 +1437,7 @@
 
 subsection \<open>Convex hull\<close>
 
-lemma convex_convex_hull: "convex (convex hull s)"
+lemma convex_convex_hull [iff]: "convex (convex hull s)"
   unfolding hull_def
   using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
   by auto
@@ -6312,6 +6312,10 @@
   "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"
   unfolding convex_alt closed_segment_def by auto
 
+lemma closed_segment_subset_convex_hull:
+    "\<lbrakk>x \<in> convex hull s; y \<in> convex hull s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull s"
+  using convex_contains_segment by blast  
+
 lemma convex_imp_starlike:
   "convex s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> starlike s"
   unfolding convex_contains_segment starlike_def by auto
@@ -8906,8 +8910,27 @@
   then show ?thesis
     using \<open>y < x\<close> by (simp add: field_simps)
 qed simp
+
 subsection\<open>Explicit formulas for interior and relative interior of convex hull\<close>
- 
+
+lemma interior_atLeastAtMost [simp]:
+  fixes a::real shows "interior {a..b} = {a<..<b}"
+  using interior_cbox [of a b] by auto
+
+lemma interior_atLeastLessThan [simp]:
+  fixes a::real shows "interior {a..<b} = {a<..<b}"
+  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_inter interior_interior interior_real_semiline)
+
+lemma interior_lessThanAtMost [simp]:
+  fixes a::real shows "interior {a<..b} = {a<..<b}"
+  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_inter
+            interior_interior interior_real_semiline)
+
+lemma at_within_closed_interval:
+    fixes x::real
+    shows "a < x \<Longrightarrow> x < b \<Longrightarrow> (at x within {a..b}) = at x"
+  by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost)
+
 lemma affine_independent_convex_affine_hull:
   fixes s :: "'a::euclidean_space set"
   assumes "~affine_dependent s" "t \<subseteq> s"
@@ -9276,7 +9299,7 @@
 
 lemma interior_convex_hull_eq_empty:
   fixes s :: "'a::euclidean_space set"
-  assumes "card s = Suc (DIM ('a))" "x \<in> s"
+  assumes "card s = Suc (DIM ('a))"
   shows   "interior(convex hull s) = {} \<longleftrightarrow> affine_dependent s"
 proof -
   { fix a b
@@ -9294,4 +9317,205 @@
     done
 qed
 
+subsection \<open>Coplanarity, and collinearity in terms of affine hull\<close>
+
+
+definition coplanar  where
+   "coplanar s \<equiv> \<exists>u v w. s \<subseteq> affine hull {u,v,w}"
+
+lemma collinear_affine_hull:
+  "collinear s \<longleftrightarrow> (\<exists>u v. s \<subseteq> affine hull {u,v})"
+proof (cases "s={}")
+  case True then show ?thesis
+    by simp
+next
+  case False
+  then obtain x where x: "x \<in> s" by auto
+  { fix u
+    assume *: "\<And>x y. \<lbrakk>x\<in>s; y\<in>s\<rbrakk> \<Longrightarrow> \<exists>c. x - y = c *\<^sub>R u"
+    have "\<exists>u v. s \<subseteq> {a *\<^sub>R u + b *\<^sub>R v |a b. a + b = 1}"
+      apply (rule_tac x=x in exI)
+      apply (rule_tac x="x+u" in exI, clarify)
+      apply (erule exE [OF * [OF x]])
+      apply (rename_tac c)
+      apply (rule_tac x="1+c" in exI)
+      apply (rule_tac x="-c" in exI)
+      apply (simp add: algebra_simps)
+      done
+  } moreover
+  { fix u v x y
+    assume *: "s \<subseteq> {a *\<^sub>R u + b *\<^sub>R v |a b. a + b = 1}"
+    have "x\<in>s \<Longrightarrow> y\<in>s \<Longrightarrow> \<exists>c. x - y = c *\<^sub>R (v-u)"
+      apply (drule subsetD [OF *])+
+      apply simp
+      apply clarify
+      apply (rename_tac r1 r2)
+      apply (rule_tac x="r1-r2" in exI)
+      apply (simp add: algebra_simps)
+      apply (metis scaleR_left.add)
+      done
+  } ultimately
+  show ?thesis
+  unfolding collinear_def affine_hull_2
+    by blast
+qed
+
+lemma collinear_imp_coplanar:
+  "collinear s ==> coplanar s"
+by (metis collinear_affine_hull coplanar_def insert_absorb2)
+
+lemma collinear_small:
+  assumes "finite s" "card s \<le> 2"
+    shows "collinear s"
+proof -
+  have "card s = 0 \<or> card s = 1 \<or> card s = 2"
+    using assms by linarith
+  then show ?thesis using assms
+    using card_eq_SucD
+    by auto (metis collinear_2 numeral_2_eq_2)
+qed
+
+lemma coplanar_small:
+  assumes "finite s" "card s \<le> 3"
+    shows "coplanar s"
+proof -
+  have "card s \<le> 2 \<or> card s = Suc (Suc (Suc 0))"
+    using assms by linarith
+  then show ?thesis using assms
+    apply safe
+    apply (simp add: collinear_small collinear_imp_coplanar)
+    apply (safe dest!: card_eq_SucD)
+    apply (auto simp: coplanar_def)
+    apply (metis hull_subset insert_subset)
+    done
+qed
+
+lemma coplanar_empty: "coplanar {}"
+  by (simp add: coplanar_small)
+
+lemma coplanar_sing: "coplanar {a}"
+  by (simp add: coplanar_small)
+
+lemma coplanar_2: "coplanar {a,b}"
+  by (auto simp: card_insert_if coplanar_small)
+
+lemma coplanar_3: "coplanar {a,b,c}"
+  by (auto simp: card_insert_if coplanar_small)
+
+lemma collinear_affine_hull_collinear: "collinear(affine hull s) \<longleftrightarrow> collinear s"
+  unfolding collinear_affine_hull
+  by (metis affine_affine_hull subset_hull hull_hull hull_mono)
+
+lemma coplanar_affine_hull_coplanar: "coplanar(affine hull s) \<longleftrightarrow> coplanar s"
+  unfolding coplanar_def
+  by (metis affine_affine_hull subset_hull hull_hull hull_mono)
+
+lemma coplanar_linear_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "coplanar s" "linear f" shows "coplanar(f ` s)"
+proof -
+  { fix u v w
+    assume "s \<subseteq> affine hull {u, v, w}"
+    then have "f ` s \<subseteq> f ` (affine hull {u, v, w})"
+      by (simp add: image_mono)
+    then have "f ` s \<subseteq> affine hull (f ` {u, v, w})"
+      by (metis assms(2) linear_conv_bounded_linear affine_hull_linear_image)
+  } then
+  show ?thesis
+    by auto (meson assms(1) coplanar_def)
+qed
+
+(*?  Still not ported
+lemma COPLANAR_TRANSLATION_EQ: "coplanar((\<lambda>x. a + x) ` s) \<longleftrightarrow> coplanar s"
+  apply (simp add: coplanar_def)
+  apply (simp add: Set.image_subset_iff_subset_vimage)
+  apply (auto simp:)
+  apply (rule_tac x="u-a" in exI)
+  apply (rule_tac x="v-a" in exI)
+  apply (rule_tac x="w-a" in exI)
+  apply (auto simp:)
+  apply (drule_tac c="x+a" in subsetD)
+  apply (simp add: affine_alt)
+
+lemma COPLANAR_TRANSLATION:
+  !a:real^N s. coplanar s ==> coplanar(IMAGE (\x. a + x) s)"
+  REWRITE_TAC[COPLANAR_TRANSLATION_EQ]);;
+
+lemma coplanar_linear_image_eq:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "linear f" "inj f" shows "coplanar(f ` s) = coplanar s"
+  MATCH_ACCEPT_TAC(LINEAR_INVARIANT_RULE COPLANAR_LINEAR_IMAGE));;
+*)
+
+lemma coplanar_subset: "\<lbrakk>coplanar t; s \<subseteq> t\<rbrakk> \<Longrightarrow> coplanar s"
+  by (meson coplanar_def order_trans)
+
+lemma affine_hull_3_imp_collinear: "c \<in> affine hull {a,b} \<Longrightarrow> collinear {a,b,c}"
+  by (metis collinear_2 collinear_affine_hull_collinear hull_redundant insert_commute)
+
+lemma collinear_3_imp_in_affine_hull: "\<lbrakk>collinear {a,b,c}; a \<noteq> b\<rbrakk> \<Longrightarrow> c \<in> affine hull {a,b}"
+  unfolding collinear_def
+  apply clarify
+  apply (frule_tac x=b in bspec, blast, drule_tac x=a in bspec, blast, erule exE)
+  apply (drule_tac x=c in bspec, blast, drule_tac x=a in bspec, blast, erule exE)
+  apply (rename_tac y x)
+  apply (simp add: affine_hull_2)
+  apply (rule_tac x="1 - x/y" in exI)
+  apply (simp add: algebra_simps)
+  done
+
+lemma collinear_3_affine_hull:
+  assumes "a \<noteq> b"
+    shows "collinear {a,b,c} \<longleftrightarrow> c \<in> affine hull {a,b}"
+using affine_hull_3_imp_collinear assms collinear_3_imp_in_affine_hull by blast
+
+lemma collinear_3_eq_affine_dependent:
+  "collinear{a,b,c} \<longleftrightarrow> a = b \<or> a = c \<or> b = c \<or> affine_dependent {a,b,c}"
+apply (case_tac "a=b", simp)
+apply (case_tac "a=c")
+apply (simp add: insert_commute)
+apply (case_tac "b=c")
+apply (simp add: insert_commute)
+apply (auto simp: affine_dependent_def collinear_3_affine_hull insert_Diff_if)
+apply (metis collinear_3_affine_hull insert_commute)+
+done
+
+lemma affine_dependent_imp_collinear_3:
+  "affine_dependent {a,b,c} \<Longrightarrow> collinear{a,b,c}"
+by (simp add: collinear_3_eq_affine_dependent)
+
+lemma collinear_3: "NO_MATCH 0 x \<Longrightarrow> collinear {x,y,z} \<longleftrightarrow> collinear {0, x-y, z-y}"
+  by (auto simp add: collinear_def)
+
+
+thm affine_hull_nonempty
+corollary affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
+  using affine_hull_nonempty by blast
+
+lemma affine_hull_2_alt:
+  fixes a b :: "'a::real_vector"
+  shows "affine hull {a,b} = range (\<lambda>u. a + u *\<^sub>R (b - a))"
+apply (simp add: affine_hull_2, safe)
+apply (rule_tac x=v in image_eqI)
+apply (simp add: algebra_simps)
+apply (metis scaleR_add_left scaleR_one, simp)
+apply (rule_tac x="1-u" in exI)
+apply (simp add: algebra_simps)
+done
+
+lemma interior_convex_hull_3_minimal:
+  fixes a :: "'a::euclidean_space"
+  shows "\<lbrakk>~ collinear{a,b,c}; DIM('a) = 2\<rbrakk>
+         \<Longrightarrow> interior(convex hull {a,b,c}) =
+                {v. \<exists>x y z. 0 < x \<and> 0 < y \<and> 0 < z \<and> x + y + z = 1 \<and>
+                            x *\<^sub>R a + y *\<^sub>R b + z *\<^sub>R c = v}"
+apply (simp add: collinear_3_eq_affine_dependent interior_convex_hull_explicit_minimal, safe)
+apply (rule_tac x="u a" in exI, simp)
+apply (rule_tac x="u b" in exI, simp)
+apply (rule_tac x="u c" in exI, simp)
+apply (rename_tac uu x y z)
+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)
+apply simp
+done
+
 end
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -2312,4 +2312,7 @@
   apply (simp only: o_def real_scaleR_def scaleR_scaleR)
   done
 
+lemma vector_derivative_const_at [simp]: "vector_derivative (\<lambda>x. c) (at a) = 0"
+  by (simp add: vector_derivative_at)
+
 end
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -576,6 +576,9 @@
 lemma content_empty [simp]: "content {} = 0"
   unfolding content_def by auto
 
+lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
+  by (simp add: content_real)
+
 lemma content_subset:
   assumes "cbox a b \<subseteq> cbox c d"
   shows "content (cbox a b) \<le> content (cbox c d)"
@@ -2467,6 +2470,11 @@
   shows "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. f x * c) = integral s f * c"
   by (blast intro:  has_integral_mult_left)
 
+lemma has_integral_mult_right:
+  fixes c :: "'a :: real_normed_algebra"
+  shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
+  using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)
+    
 lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
   unfolding o_def[symmetric]
   by (metis has_integral_linear bounded_linear_scaleR_right)
@@ -2780,9 +2788,12 @@
 lemma integrable_on_refl[intro]: "f integrable_on cbox a a"
   unfolding integrable_on_def by auto
 
-lemma integral_refl: "integral (cbox a a) f = 0"
+lemma integral_refl [simp]: "integral (cbox a a) f = 0"
   by (rule integral_unique) auto
 
+lemma integral_singleton [simp]: "integral {a} f = 0"
+  by auto
+
 
 subsection \<open>Cauchy-type criterion for integrability.\<close>
 
@@ -5394,7 +5405,7 @@
   apply auto
   done
 
-lemma negligible_empty[intro]: "negligible {}"
+lemma negligible_empty[iff]: "negligible {}"
   by auto
 
 lemma negligible_finite[intro]:
@@ -5688,7 +5699,7 @@
   assumes "monoidal opp"
   shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a .. b::real} = neutral opp) \<and>
     (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a .. c}) (f {c .. b}) = f {a .. b}))"
-  apply (simp add: operative_def content_real_eq_0)
+  apply (simp add: operative_def content_real_eq_0 del: content_real_if)
 proof safe
   fix a b c :: real
   assume as:
@@ -6467,7 +6478,7 @@
         show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x .. y}"
           apply (subst *)
           unfolding **
-          by auto
+          by blast
         show "\<forall>xa\<in>{x .. y}. norm (f xa - f x) \<le> e"
           apply safe
           apply (rule less_imp_le)
@@ -6523,7 +6534,7 @@
         show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y .. x}"
           apply (subst *)
           unfolding **
-          apply auto
+          apply blast
           done
         show "\<forall>xa\<in>{y .. x}. norm (f xa - f x) \<le> e"
           apply safe
@@ -12133,11 +12144,6 @@
   qed
 qed
 
-lemma dense_eq0_I:
-  fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
-  shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
-by (metis dense not_less zero_less_abs_iff)
-
 lemma integral_Pair_const:
     "integral (cbox (a,c) (b,d)) (\<lambda>x. k) =
      integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. k))"
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -462,6 +462,12 @@
   apply auto
   done
 
+lemma approachable_lt_le2:  --{*like the above, but pushes aside an extra formula*}
+    "(\<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)"
+  apply auto
+  apply (rule_tac x="d/2" in exI, auto)
+  done
+
 lemma triangle_lemma:
   fixes x y z :: real
   assumes x: "0 \<le> x"
@@ -2933,13 +2939,13 @@
 definition collinear :: "'a::real_vector set \<Rightarrow> bool"
   where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
 
-lemma collinear_empty: "collinear {}"
+lemma collinear_empty [iff]: "collinear {}"
   by (simp add: collinear_def)
 
-lemma collinear_sing: "collinear {x}"
+lemma collinear_sing [iff]: "collinear {x}"
   by (simp add: collinear_def)
 
-lemma collinear_2: "collinear {x, y}"
+lemma collinear_2 [iff]: "collinear {x, y}"
   apply (simp add: collinear_def)
   apply (rule exI[where x="x - y"])
   apply auto
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -1826,7 +1826,7 @@
 
 text\<open>Interrelations between restricted and unrestricted limits.\<close>
 
-lemma Lim_at_within: (* FIXME: rename *)
+lemma Lim_at_imp_Lim_at_within: 
   "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
   by (metis order_refl filterlim_mono subset_UNIV at_le)
 
@@ -2728,6 +2728,11 @@
   apply arith
   done
 
+lemma bounded_pos_less: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x < b)"
+  apply (simp add: bounded_pos)
+  apply (safe; rule_tac x="b+1" in exI; force)
+  done
+
 lemma Bseq_eq_bounded:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "Bseq f \<longleftrightarrow> bounded (range f)"
@@ -4636,7 +4641,7 @@
 
 lemma continuous_at_imp_continuous_within:
   "continuous (at x) f \<Longrightarrow> continuous (at x within s) f"
-  unfolding continuous_within continuous_at using Lim_at_within by auto
+  unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto
 
 lemma Lim_trivial_limit: "trivial_limit net \<Longrightarrow> (f ---> l) net"
   by simp
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -862,6 +862,25 @@
   shows "norm (x ^ n) = norm x ^ n"
 by (induct n) (simp_all add: norm_mult)
 
+lemma norm_mult_numeral1 [simp]:
+  fixes a b :: "'a::{real_normed_field, field}"
+  shows "norm (numeral w * a) = numeral w * norm a"
+by (simp add: norm_mult)
+
+lemma norm_mult_numeral2 [simp]:
+  fixes a b :: "'a::{real_normed_field, field}"
+  shows "norm (a * numeral w) = norm a * numeral w"
+by (simp add: norm_mult)
+
+lemma norm_divide_numeral [simp]:
+  fixes a b :: "'a::{real_normed_field, field}"
+  shows "norm (a / numeral w) = norm a / numeral w"
+by (simp add: norm_divide)
+
+lemma norm_of_real_diff [simp]:
+    "norm (of_real b - of_real a :: 'a::real_normed_algebra_1) \<le> \<bar>b - a\<bar>"
+  by (metis norm_of_real of_real_diff order_refl)
+
 text\<open>Despite a superficial resemblance, @{text norm_eq_1} is not relevant.\<close>
 lemma square_norm_one:
   fixes x :: "'a::real_normed_div_algebra"
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -1357,6 +1357,10 @@
   "{..< n} - {..< m} = {m ..< n}"
   by auto
 
+lemma (in linorder) atLeastAtMost_diff_ends:
+  "{a..b} - {a, b} = {a<..<b}"
+  by auto
+
 
 subsubsection \<open>Some Subset Conditions\<close>
 
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -1526,7 +1526,7 @@
 lemma isCont_def: "isCont f a \<longleftrightarrow> f -- a --> f a"
   by (rule continuous_at)
 
-lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
+lemma continuous_at_imp_continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
   by (auto intro: tendsto_mono at_le simp: continuous_at continuous_within)
 
 lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
@@ -1536,7 +1536,7 @@
   unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
 
 lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
-  by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
+  by (auto intro: continuous_at_imp_continuous_at_within simp: continuous_on_eq_continuous_within)
 
 lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   unfolding isCont_def by (rule tendsto_compose)
@@ -1549,7 +1549,7 @@
 
 lemma continuous_within_compose3:
   "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
-  using continuous_within_compose2[of x s f g] by (simp add: continuous_at_within)
+  using continuous_within_compose2[of x s f g] by (simp add: continuous_at_imp_continuous_at_within)
 
 lemma filtermap_nhds_open_map:
   assumes cont: "isCont f a" and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
diff -r a443b08281e2 -r bf0c76ccee8d src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Transcendental.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -748,7 +748,7 @@
     shows "summable (\<lambda>n. diffs c n * x^n)"
   apply (rule termdiff_converges [where K = "1 + norm x"])
   using assms
-  apply (auto simp: )
+  apply auto
   done
 
 lemma termdiffs_strong:
@@ -757,17 +757,16 @@
       and K: "norm x < norm K"
   shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. diffs c n * x^n)"
 proof -
-  have [simp]: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
+  have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
     using K
     apply (auto simp: norm_divide)
     apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"])
     apply (auto simp: mult_2_right norm_triangle_mono)
     done
+  then have [simp]: "norm ((of_real (norm K) + of_real (norm x)) :: 'a) < norm K * 2"
+    by simp
   have "summable (\<lambda>n. c n * (of_real (norm x + norm K) / 2) ^ n)"
-    apply (rule summable_norm_cancel [OF powser_insidea [OF sm]])
-    using K
-    apply (auto simp: algebra_simps)
-    done
+    by (metis K2 summable_norm_cancel [OF powser_insidea [OF sm]] add.commute of_real_add)
   moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs c n * x ^ n)"
     by (blast intro: sm termdiff_converges powser_inside)
   moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs(diffs c) n * x ^ n)"
@@ -776,8 +775,6 @@
     apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
     apply (auto simp: algebra_simps)
     using K
-    apply (simp add: norm_divide)
-    apply (rule less_le_trans [of _ "of_real (norm K) + of_real (norm x)"])
     apply (simp_all add: of_real_add [symmetric] del: of_real_add)
     done
 qed