# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1448978950 0
# Node ID d50b993b4fb93c2e357936572400b3686f5b6aad
# Parent  0d399131008f51dfcc49f1d698c3142e5c0d5987
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.

diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Complex.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -748,9 +748,6 @@
 
 subsubsection \<open>Complex exponential\<close>
 
-abbreviation Exp :: "complex \<Rightarrow> complex"
-  where "Exp \<equiv> exp"
-
 lemma cis_conv_exp: "cis b = exp (\<i> * b)"
 proof -
   { fix n :: nat
@@ -766,29 +763,29 @@
              intro!: sums_unique sums_add sums_mult sums_of_real)
 qed
 
-lemma Exp_eq_polar: "Exp z = exp (Re z) * cis (Im z)"
+lemma exp_eq_polar: "exp z = exp (Re z) * cis (Im z)"
   unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by (cases z) simp
 
 lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
-  unfolding Exp_eq_polar by simp
+  unfolding exp_eq_polar by simp
 
 lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
-  unfolding Exp_eq_polar by simp
+  unfolding exp_eq_polar by simp
 
 lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1"
   by (simp add: norm_complex_def)
 
 lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)"
-  by (simp add: cis.code cmod_complex_polar Exp_eq_polar)
+  by (simp add: cis.code cmod_complex_polar exp_eq_polar)
 
-lemma complex_Exp_Ex: "\<exists>a r. z = complex_of_real r * Exp a"
+lemma complex_exp_exists: "\<exists>a r. z = complex_of_real r * exp a"
   apply (insert rcis_Ex [of z])
-  apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
+  apply (auto simp add: exp_eq_polar rcis_def mult.assoc [symmetric])
   apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
   done
 
-lemma Exp_two_pi_i [simp]: "Exp((2::complex) * complex_of_real pi * ii) = 1"
-  by (simp add: Exp_eq_polar complex_eq_iff)
+lemma exp_two_pi_i [simp]: "exp(2 * complex_of_real pi * ii) = 1"
+  by (simp add: exp_eq_polar complex_eq_iff)
 
 subsubsection \<open>Complex argument\<close>
 
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -1644,9 +1644,8 @@
   "(real_of_int (a::int) + b > 0) = (real_of_int a + real_of_int (floor b) > 0 \<or> (real_of_int a + real_of_int (floor b) = 0 \<and> real_of_int (floor b) - b < 0))"
 proof-
   have th: "(real_of_int a + b >0) = (real_of_int (-a) + (-b)< 0)" by arith
-  show ?thesis using myless[of _ "real_of_int (floor b)"]
-    by (simp only:th split_int_less_real'[where a="-a" and b="-b"])
-    (simp add: algebra_simps,arith)
+  show ?thesis 
+    by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) (auto simp add: algebra_simps)
 qed
 
 lemma split_int_le_real:
@@ -3765,8 +3764,7 @@
 proof-
   let ?ss = "s - real_of_int (floor s)"
   from real_of_int_floor_add_one_gt[where r="s", simplified myless[of "s"]]
-    of_int_floor_le  have ss0:"?ss \<ge> 0" and ss1:"?ss < 1"
-    by (auto simp add: myle[of _ "s", symmetric] myless[of "?ss"])
+    of_int_floor_le  have ss0:"?ss \<ge> 0" and ss1:"?ss < 1" by (auto simp: floor_less_cancel)
   from np have n0: "real_of_int n \<ge> 0" by simp
   from mult_left_mono[OF up n0] mult_strict_left_mono[OF u1 np]
   have nu0:"real_of_int n * u - s \<ge> -s" and nun:"real_of_int n * u -s < real_of_int n - s" by auto
@@ -4807,7 +4805,7 @@
   shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real_of_int i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
 proof-
   have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real_of_int i)#bs) (exsplit p))"
-    by (simp add: myless[of _ "1"] myless[of _ "0"] ac_simps)
+    by auto
   also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real_of_int i + x) #bs) p)"
     by (simp only: exsplit[OF qf] ac_simps)
   also have "\<dots> = (\<exists> x. Ifm (x#bs) p)"
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -319,6 +319,16 @@
   apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
   done
 
+lemma finite_finite_vimage_IntI:
+  assumes "finite F" and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)"
+  shows "finite (h -` F \<inter> A)"
+proof -
+  have *: "h -` F \<inter> A = (\<Union> y\<in>F. (h -` {y}) \<inter> A)"
+    by blast
+  show ?thesis
+    by (simp only: * assms finite_UN_I)
+qed
+
 lemma finite_vimageI:
   "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
   using finite_vimage_IntI[of F h UNIV] by auto
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Groups.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -999,6 +999,9 @@
 apply (simp add: algebra_simps)
 done
 
+lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
+by (simp add: less_diff_eq)
+
 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
 by (auto simp add: le_less diff_less_eq )
 
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Inequalities.thy
--- a/src/HOL/Inequalities.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Inequalities.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -66,7 +66,6 @@
       using assms by (cases "i \<le> j") (auto simp: algebra_simps)
   } hence "?S \<le> 0"
     by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
-       (auto simp: field_simps)
   finally show ?thesis by (simp add: algebra_simps)
 qed
 
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Library/BigO.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -200,8 +200,6 @@
   apply (auto simp add: fun_Compl_def func_plus)
   apply (drule_tac x = x in spec)+
   apply force
-  apply (drule_tac x = x in spec)+
-  apply force
   done
 
 lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Library/Float.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -1116,10 +1116,11 @@
 proof -
   have "0 \<le> log 2 x - real_of_int \<lfloor>log 2 x\<rfloor>"
     by (simp add: algebra_simps)
-  from this assms
+  with assms
   show ?thesis
-    by (auto simp: truncate_down_def round_down_def mult_powr_eq
+    apply (auto simp: truncate_down_def round_down_def mult_powr_eq 
       intro!: ge_one_powr_ge_zero mult_pos_pos)
+    by linarith
 qed
 
 lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -72,10 +72,7 @@
     by(induction rule: finite_psubset_induct)(meson Diff_subset card_Diff1_less card_psubset finite_Diff step)
 qed    
 
-text \<open>
-  As a concrete example, we prove that the set of natural numbers is
-  infinite.
-\<close>
+text \<open>As a concrete example, we prove that the set of natural numbers is infinite.\<close>
 
 lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
   using frequently_cofinite[of "\<lambda>x. x \<in> S"]
@@ -94,6 +91,7 @@
 lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
   by (simp add: finite_nat_iff_bounded)
 
+
 text \<open>
   For a set of natural numbers to be infinite, it is enough to know
   that for any number larger than some \<open>k\<close>, there is some larger
@@ -150,6 +148,32 @@
   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   using assms by (blast dest: inf_img_fin_dom)
 
+proposition finite_image_absD:
+    fixes S :: "'a::linordered_ring set"
+    shows "finite (abs ` S) \<Longrightarrow> finite S"
+  by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
+
+text \<open>The set of integers is also infinite.\<close>
+
+lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)"
+  by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
+
+proposition infinite_int_iff_unbounded_le: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. abs n \<ge> m \<and> n \<in> S)"
+  apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
+  apply (metis abs_ge_zero nat_le_eq_zle le_nat_iff)
+  done
+
+proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. abs n > m \<and> n \<in> S)"
+  apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def)
+  apply (metis (full_types) nat_le_iff nat_mono not_le)
+  done
+
+proposition finite_int_iff_bounded: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {..<k})"
+  using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
+
+proposition finite_int_iff_bounded_le: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {.. k})"
+  using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
+
 subsection "Infinitely Many and Almost All"
 
 text \<open>
@@ -385,24 +409,5 @@
     unfolding bij_betw_def by (auto intro: enumerate_in_set)
 qed
 
-subsection "Miscellaneous"
-
-text \<open>
-  A few trivial lemmas about sets that contain at most one element.
-  These simplify the reasoning about deterministic automata.
-\<close>
-
-definition atmost_one :: "'a set \<Rightarrow> bool"
-  where "atmost_one S \<longleftrightarrow> (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x = y)"
-
-lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
-  by (simp add: atmost_one_def)
-
-lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
-  by (simp add: atmost_one_def)
-
-lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
-  by (simp add: atmost_one_def)
-
 end
 
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -3012,7 +3012,7 @@
                  \<subseteq> ball (p t) (ee (p t))"
             apply (intro subset_path_image_join pi_hgn pi_ghn')
             using \<open>N>0\<close> Suc.prems
-            apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
+            apply (auto simp: path_image_subpath dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
             done
           have pi0: "(f has_contour_integral 0)
                        (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++
@@ -3492,7 +3492,7 @@
   by (simp add: winding_number_valid_path)
 
 lemma winding_number_subpath_trivial [simp]: "z \<noteq> g x \<Longrightarrow> winding_number (subpath x x g) z = 0"
-  by (simp add: winding_number_valid_path)
+  by (simp add: path_image_subpath winding_number_valid_path)
 
 lemma winding_number_join:
   assumes g1: "path g1" "z \<notin> path_image g1"
@@ -3742,7 +3742,7 @@
         by (rule continuous_at_imp_continuous_within)
       have gdx: "\<gamma> differentiable at x"
         using x by (simp add: g_diff_at)
-      have "((\<lambda>c. Exp (- integral {a..c} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0))
+      have "((\<lambda>c. exp (- integral {a..c} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0))
           (at x within {a..b})"
         using x gdx t
         apply (clarsimp simp add: differentiable_iff_scaleR)
@@ -3781,7 +3781,7 @@
                     "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>"
                     "contour_integral p (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
     using winding_number [OF assms, of 1] by auto
-  have [simp]: "(winding_number \<gamma> z \<in> \<int>) = (Exp (contour_integral p (\<lambda>w. 1 / (w - z))) = 1)"
+  have [simp]: "(winding_number \<gamma> z \<in> \<int>) = (exp (contour_integral p (\<lambda>w. 1 / (w - z))) = 1)"
       using p by (simp add: exp_eq_1 complex_is_Int_iff)
   have "winding_number p z \<in> \<int> \<longleftrightarrow> pathfinish p = pathstart p"
     using p z
@@ -3840,7 +3840,7 @@
     using eqArg by (simp add: i_def)
   have gpdt: "\<gamma> piecewise_C1_differentiable_on {0..t}"
     by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl piecewise_C1_differentiable_on_subset gpd t)
-  have "Exp (- i) * (\<gamma> t - z) = \<gamma> 0 - z"
+  have "exp (- i) * (\<gamma> t - z) = \<gamma> 0 - z"
     unfolding i_def
     apply (rule winding_number_exp_integral [OF gpdt])
     using t z unfolding path_image_def
@@ -3855,7 +3855,7 @@
     apply (subst Complex_Transcendental.Arg_eq [of r])
     apply (simp add: iArg)
     using *
-    apply (simp add: Exp_eq_polar field_simps)
+    apply (simp add: exp_eq_polar field_simps)
     done
   with t show ?thesis
     by (rule_tac x="exp(Re i) / norm r" in exI) (auto simp: path_image_def)
@@ -4225,8 +4225,8 @@
     also have "... = winding_number (subpath 0 x \<gamma>) z"
       apply (subst winding_number_valid_path)
       using assms x
-      apply (simp_all add: valid_path_subpath)
-      by (force simp: closed_segment_eq_real_ivl path_image_def)
+      apply (simp_all add: path_image_subpath valid_path_subpath)
+      by (force simp: path_image_def)
     finally show ?thesis .
   qed
   show ?thesis
@@ -4277,7 +4277,7 @@
     have gt: "\<gamma> t - z = - (of_real (exp (- (2 * pi * Im (winding_number (subpath 0 t \<gamma>) z)))) * (\<gamma> 0 - z))"
       using winding_number_exp_2pi [of "subpath 0 t \<gamma>" z]
       apply (simp add: t \<gamma> valid_path_imp_path)
-      using closed_segment_eq_real_ivl path_image_def t z by (fastforce simp add: Euler sub12)
+      using closed_segment_eq_real_ivl path_image_def t z by (fastforce simp: path_image_subpath Euler sub12)
     have "b < a \<bullet> \<gamma> 0"
     proof -
       have "\<gamma> 0 \<in> {c. b < a \<bullet> c}"
@@ -4321,7 +4321,7 @@
     have "isCont (winding_number \<gamma>) z"
       by (metis continuous_at_winding_number valid_path_imp_path \<gamma> z)
     then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < abs(Re(winding_number \<gamma> z)) - 1/2"
-      using continuous_at_eps_delta wnz_12 diff_less_iff(1) by blast
+      using continuous_at_eps_delta wnz_12 diff_gt_0_iff_gt by blast
     def z' \<equiv> "z - (d / (2 * cmod a)) *\<^sub>R a"
     have *: "a \<bullet> z' \<le> b - d / 3 * cmod a"
       unfolding z'_def inner_mult_right' divide_inverse
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -654,7 +654,6 @@
     done
 qed
 
-
 corollary
   shows Arg_ge_0: "0 \<le> Arg z"
     and Arg_lt_2pi: "Arg z < 2*pi"
@@ -772,7 +771,7 @@
 lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   apply (cases "z=0", simp)
   apply (rule Arg_unique [of "inverse (norm z)"])
-  using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] Exp_two_pi_i
+  using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] exp_two_pi_i
   apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
   done
 
@@ -849,8 +848,11 @@
   by auto
 
 lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
-  by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
-
+  by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: exp_eq_polar)
+
+lemma complex_split_polar:
+  obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
+  using Arg cis.ctr cis_conv_exp by fastforce
 
 subsection\<open>Analytic properties of tangent function\<close>
 
@@ -898,7 +900,7 @@
   have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \<le> pi" unfolding ln_complex_def
     apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
     using z assms \<phi>
-    apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
+    apply (auto simp: field_simps exp_complex_eqI exp_eq_polar cis.code)
     done
   then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \<le> pi"
     by auto
@@ -1516,14 +1518,14 @@
   shows "((\<lambda>z. z powr r :: complex) has_field_derivative r * z powr (r - 1)) (at z)"
 proof (subst DERIV_cong_ev[OF refl _ refl])
   from assms have "eventually (\<lambda>z. z \<noteq> 0) (nhds z)" by (intro t1_space_nhds) auto
-  thus "eventually (\<lambda>z. z powr r = Exp (r * Ln z)) (nhds z)"
+  thus "eventually (\<lambda>z. z powr r = exp (r * Ln z)) (nhds z)"
     unfolding powr_def by eventually_elim simp
 
-  have "((\<lambda>z. Exp (r * Ln z)) has_field_derivative Exp (r * Ln z) * (inverse z * r)) (at z)"
+  have "((\<lambda>z. exp (r * Ln z)) has_field_derivative exp (r * Ln z) * (inverse z * r)) (at z)"
     using assms by (auto intro!: derivative_eq_intros has_field_derivative_powr)
-  also have "Exp (r * Ln z) * (inverse z * r) = r * z powr (r - 1)"
+  also have "exp (r * Ln z) * (inverse z * r) = r * z powr (r - 1)"
     unfolding powr_def by (simp add: assms exp_diff field_simps)
-  finally show "((\<lambda>z. Exp (r * Ln z)) has_field_derivative r * z powr (r - 1)) (at z)"
+  finally show "((\<lambda>z. exp (r * Ln z)) has_field_derivative r * z powr (r - 1)) (at z)"
     by simp
 qed
 
@@ -2405,7 +2407,7 @@
 
 lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \<le> pi"
   by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
- 
+
 
 subsection\<open>Interrelations between Arcsin and Arccos\<close>
 
@@ -2481,7 +2483,6 @@
   apply (simp add: cos_squared_eq)
   using assms
   apply (auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff)
-  apply (auto simp: algebra_simps)
   done
 
 lemma sin_cos_csqrt:
@@ -2491,7 +2492,6 @@
   apply (simp add: sin_squared_eq)
   using assms
   apply (auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff)
-  apply (auto simp: algebra_simps)
   done
 
 lemma Arcsin_Arccos_csqrt_pos:
@@ -2661,7 +2661,7 @@
   by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
 
 lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
-  apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
+  apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
   apply (subst Arcsin_Arccos_csqrt_pos)
   apply (auto simp: power_le_one csqrt_1_diff_eq)
   done
@@ -2671,7 +2671,7 @@
   by (simp add: arcsin_minus)
 
 lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
-  apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
+  apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
   apply (subst Arccos_Arcsin_csqrt_pos)
   apply (auto simp: power_le_one csqrt_1_diff_eq)
   done
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -4397,7 +4397,7 @@
     using \<open>y \<in> s\<close>
   proof -
     show "inner (y - z) z < inner (y - z) y"
-      apply (subst diff_less_iff(1)[symmetric])
+      apply (subst diff_gt_0_iff_gt [symmetric])
       unfolding inner_diff_right[symmetric] and inner_gt_zero_iff
       using \<open>y\<in>s\<close> \<open>z\<notin>s\<close>
       apply auto
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -688,7 +688,7 @@
     "x \<in> {a <..< b}"
     "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
   then show ?thesis
-    by (metis (hide_lams) assms(1) diff_less_iff(1) eq_iff_diff_eq_0
+    by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0
       zero_less_mult_iff nonzero_mult_divide_cancel_right not_real_square_gt_zero
       times_divide_eq_left)
 qed
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -599,7 +599,7 @@
   then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
     using assms unfolding box_ne_empty by auto
   have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
-    using ab_ne by (metis diff_le_iff(1))
+    using ab_ne by auto
   moreover
   have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
     using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -375,7 +375,7 @@
 lemma path_compose_reversepath: "f o reversepath p = reversepath(f o p)"
   by (rule ext) (simp add: reversepath_def)
 
-lemma join_paths_eq:
+lemma joinpaths_eq:
   "(\<And>t. t \<in> {0..1} \<Longrightarrow> p t = p' t) \<Longrightarrow>
    (\<And>t. t \<in> {0..1} \<Longrightarrow> q t = q' t)
    \<Longrightarrow>  t \<in> {0..1} \<Longrightarrow> (p +++ q) t = (p' +++ q') t"
@@ -453,8 +453,6 @@
 lemma path_join_imp: "\<lbrakk>path g1; path g2; pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> path(g1 +++ g2)"
   by (simp add: path_join)
 
-lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join
-
 lemma simple_path_join_loop:
   assumes "arc g1" "arc g2"
           "pathfinish g1 = pathstart g2"  "pathfinish g2 = pathstart g1"
@@ -563,18 +561,18 @@
 definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
   where "subpath a b g \<equiv> \<lambda>x. g((b - a) * x + a)"
 
-lemma path_image_subpath_gen [simp]:
-  fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
+lemma path_image_subpath_gen:
+  fixes g :: "_ \<Rightarrow> 'a::real_normed_vector"
   shows "path_image(subpath u v g) = g ` (closed_segment u v)"
   apply (simp add: closed_segment_real_eq path_image_def subpath_def)
   apply (subst o_def [of g, symmetric])
   apply (simp add: image_comp [symmetric])
   done
 
-lemma path_image_subpath [simp]:
+lemma path_image_subpath:
   fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
   shows "path_image(subpath u v g) = (if u \<le> v then g ` {u..v} else g ` {v..u})"
-  by (simp add: closed_segment_eq_real_ivl)
+  by (simp add: path_image_subpath_gen closed_segment_eq_real_ivl)
 
 lemma path_subpath [simp]:
   fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
@@ -614,7 +612,7 @@
 
 lemma affine_ineq:
   fixes x :: "'a::linordered_idom"
-  assumes "x \<le> 1" "v < u"
+  assumes "x \<le> 1" "v \<le> u"
     shows "v + x * u \<le> u + x * v"
 proof -
   have "(1-x)*(u-v) \<ge> 0"
@@ -726,7 +724,7 @@
 
 lemma path_image_subpath_subset:
     "\<lbrakk>path g; u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
-  apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost)
+  apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath)
   apply (auto simp: path_image_def)
   done
 
@@ -805,7 +803,7 @@
     apply (rule that [OF `0 \<le> u` `u \<le> 1`])
     apply (metis DiffI disj frontier_def g0 notin pathstart_def)
     using `0 \<le> u` g0 disj
-    apply (simp add:)
+    apply (simp add: path_image_subpath_gen)
     apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def)
     apply (rename_tac y)
     apply (drule_tac x="y/u" in spec)
@@ -825,7 +823,7 @@
   show ?thesis
     apply (rule that [of "subpath 0 u g"])
     using assms u
-    apply simp_all
+    apply (simp_all add: path_image_subpath)
     apply (simp add: pathstart_def)
     apply (force simp: closed_segment_eq_real_ivl path_image_def)
     done
@@ -966,7 +964,7 @@
   unfolding linepath_def
   by (intro continuous_intros)
 
-lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)"
+lemma continuous_on_linepath [intro,continuous_intros]: "continuous_on s (linepath a b)"
   using continuous_linepath_at
   by (auto intro!: continuous_at_imp_continuous_on)
 
@@ -982,6 +980,9 @@
   unfolding reversepath_def linepath_def
   by auto
 
+lemma linepath_0 [simp]: "linepath 0 b x = x *\<^sub>R b"
+  by (simp add: linepath_def)
+
 lemma arc_linepath:
   assumes "a \<noteq> b"
   shows "arc (linepath a b)"
@@ -1566,7 +1567,7 @@
       have CC: "1 \<le> 1 + (C - 1) * u"
         using `x \<noteq> a` `0 \<le> u`
         apply (simp add: C_def divide_simps norm_minus_commute)
-        by (metis Bx diff_le_iff(1) less_eq_real_def mult_nonneg_nonneg)
+        using Bx by auto
       have *: "\<And>v. (1 - u) *\<^sub>R x + u *\<^sub>R (a + v *\<^sub>R (x - a)) = a + (1 + (v - 1) * u) *\<^sub>R (x - a)"
         by (simp add: algebra_simps)
       have "a + ((1 / (1 + C * u - u)) *\<^sub>R x + ((u / (1 + C * u - u)) *\<^sub>R a + (C * u / (1 + C * u - u)) *\<^sub>R x)) =
@@ -1601,7 +1602,7 @@
       have DD: "1 \<le> 1 + (D - 1) * u"
         using `y \<noteq> a` `0 \<le> u`
         apply (simp add: D_def divide_simps norm_minus_commute)
-        by (metis By diff_le_iff(1) less_eq_real_def mult_nonneg_nonneg)
+        using By by auto
       have *: "\<And>v. (1 - u) *\<^sub>R y + u *\<^sub>R (a + v *\<^sub>R (y - a)) = a + (1 + (v - 1) * u) *\<^sub>R (y - a)"
         by (simp add: algebra_simps)
       have "a + ((1 / (1 + D * u - u)) *\<^sub>R y + ((u / (1 + D * u - u)) *\<^sub>R a + (D * u / (1 + D * u - u)) *\<^sub>R y)) =
@@ -2793,7 +2794,7 @@
 proposition homotopic_paths_sym_eq: "homotopic_paths s p q \<longleftrightarrow> homotopic_paths s q p"
   by (metis homotopic_paths_sym)
 
-proposition homotopic_paths_trans:
+proposition homotopic_paths_trans [trans]:
      "\<lbrakk>homotopic_paths s p q; homotopic_paths s q r\<rbrakk> \<Longrightarrow> homotopic_paths s p r"
   apply (simp add: homotopic_paths_def)
   apply (rule homotopic_with_trans, assumption)
@@ -3262,4 +3263,83 @@
     by (metis atLeastAtMost_iff imageI le_less_trans not_le path_image_def)
 qed
 
+subsection\<open> Homotopy and subpaths\<close>
+
+lemma homotopic_join_subpaths1:
+  assumes "path g" and pag: "path_image g \<subseteq> s"
+      and u: "u \<in> {0..1}" and v: "v \<in> {0..1}" and w: "w \<in> {0..1}" "u \<le> v" "v \<le> w"
+    shows "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
+proof -
+  have 1: "t * 2 \<le> 1 \<Longrightarrow> u + t * (v * 2) \<le> v + t * (u * 2)" for t
+    using affine_ineq \<open>u \<le> v\<close> by fastforce
+  have 2: "t * 2 > 1 \<Longrightarrow> u + (2*t - 1) * v \<le> v + (2*t - 1) * w" for t
+    by (metis add_mono_thms_linordered_semiring(1) diff_gt_0_iff_gt less_eq_real_def mult.commute mult_right_mono \<open>u \<le> v\<close> \<open>v \<le> w\<close>)
+  have t2: "\<And>t::real. t*2 = 1 \<Longrightarrow> t = 1/2" by auto
+  show ?thesis
+    apply (rule homotopic_paths_subset [OF _ pag])
+    using assms
+    apply (cases "w = u")
+    using homotopic_paths_rinv [of "subpath u v g" "path_image g"]
+    apply (force simp: closed_segment_eq_real_ivl image_mono path_image_def subpath_refl)
+      apply (rule homotopic_paths_sym)
+      apply (rule homotopic_paths_reparametrize
+             [where f = "\<lambda>t. if  t \<le> 1 / 2
+                             then inverse((w - u)) *\<^sub>R (2 * (v - u)) *\<^sub>R t
+                             else inverse((w - u)) *\<^sub>R ((v - u) + (w - v) *\<^sub>R (2 *\<^sub>R t - 1))"])
+      using \<open>path g\<close> path_subpath u w apply blast
+      using \<open>path g\<close> path_image_subpath_subset u w(1) apply blast
+      apply simp_all
+      apply (subst split_01)
+      apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
+      apply (simp_all add: field_simps not_le)
+      apply (force dest!: t2)
+      apply (force simp: algebra_simps mult_left_mono affine_ineq dest!: 1 2)
+      apply (simp add: joinpaths_def subpath_def)
+      apply (force simp: algebra_simps)
+      done
+qed
+
+lemma homotopic_join_subpaths2:
+  assumes "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
+    shows "homotopic_paths s (subpath w v g +++ subpath v u g) (subpath w u g)"
+by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath)
+
+lemma homotopic_join_subpaths3:
+  assumes hom: "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
+      and "path g" and pag: "path_image g \<subseteq> s"
+      and u: "u \<in> {0..1}" and v: "v \<in> {0..1}" and w: "w \<in> {0..1}"
+    shows "homotopic_paths s (subpath v w g +++ subpath w u g) (subpath v u g)"
+proof -
+  have "homotopic_paths s (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
+    apply (rule homotopic_paths_join)
+    using hom homotopic_paths_sym_eq apply blast
+    apply (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w)
+    apply (simp add:)
+    done
+  also have "homotopic_paths s ((subpath u v g +++ subpath v w g) +++ subpath w v g) (subpath u v g +++ subpath v w g +++ subpath w v g)"
+    apply (rule homotopic_paths_sym [OF homotopic_paths_assoc])
+    using assms by (simp_all add: path_image_subpath_subset [THEN order_trans])
+  also have "homotopic_paths s (subpath u v g +++ subpath v w g +++ subpath w v g)
+                               (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))"
+    apply (rule homotopic_paths_join)
+    apply (metis \<open>path g\<close> homotopic_paths_eq order.trans pag path_image_subpath_subset path_subpath u v)
+    apply (metis (no_types, lifting) \<open>path g\<close> homotopic_paths_linv order_trans pag path_image_subpath_subset path_subpath pathfinish_subpath reversepath_subpath v w)
+    apply (simp add:)
+    done
+  also have "homotopic_paths s (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)"
+    apply (rule homotopic_paths_rid)
+    using \<open>path g\<close> path_subpath u v apply blast
+    apply (meson \<open>path g\<close> order.trans pag path_image_subpath_subset u v)
+    done
+  finally have "homotopic_paths s (subpath u w g +++ subpath w v g) (subpath u v g)" .
+  then show ?thesis
+    using homotopic_join_subpaths2 by blast
+qed
+
+proposition homotopic_join_subpaths:
+   "\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
+    \<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
+apply (rule le_cases3 [of u v w])
+using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
+
 end
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -817,6 +817,9 @@
 definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   where "cball x e = {y. dist x y \<le> e}"
 
+definition sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+  where "sphere x e = {y. dist x y = e}"
+
 lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
   by (simp add: ball_def)
 
@@ -863,19 +866,6 @@
 lemma cball_diff_eq_sphere: "cball a r - ball a r =  {x. dist x a = r}"
   by (auto simp: cball_def ball_def dist_commute)
 
-lemma diff_less_iff:
-  "(a::real) - b > 0 \<longleftrightarrow> a > b"
-  "(a::real) - b < 0 \<longleftrightarrow> a < b"
-  "a - b < c \<longleftrightarrow> a < c + b" "a - b > c \<longleftrightarrow> a > c + b"
-  by arith+
-
-lemma diff_le_iff:
-  "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
-  "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b"
-  "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
-  "a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
-  by arith+
-
 lemma open_ball [intro, simp]: "open (ball x e)"
 proof -
   have "open (dist x -` {..<e})"
@@ -7347,7 +7337,7 @@
     then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
       unfolding image_iff Bex_def mem_box
       apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
-      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult.commute diff_le_iff inner_distrib inner_diff_left)
+      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left)
       done
   }
   moreover
@@ -7357,7 +7347,7 @@
     then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
       unfolding image_iff Bex_def mem_box
       apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
-      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult.commute diff_le_iff inner_distrib inner_diff_left)
+      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left)
       done
   }
   ultimately show ?thesis using False by (auto simp: cbox_def)
@@ -8187,8 +8177,8 @@
   shows "cball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r < 0"
         (is "?lhs = ?rhs")
 proof
-  assume ?lhs 
-  then show ?rhs 
+  assume ?lhs
+  then show ?rhs
   proof (cases "r < 0")
     case True then show ?rhs by simp
   next
@@ -8209,13 +8199,13 @@
         using  \<open>a \<noteq> a'\<close> by (simp add: abs_mult_pos field_simps)
       finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \<bar>norm (a - a') + r\<bar>" by linarith
       show ?thesis
-        using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \<open>?lhs\<close>] \<open>a \<noteq> a'\<close> 
+        using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \<open>?lhs\<close>] \<open>a \<noteq> a'\<close>
         by (simp add: dist_norm scaleR_add_left)
     qed
     then show ?rhs by (simp add: dist_norm)
   qed
 next
-  assume ?rhs then show ?lhs 
+  assume ?rhs then show ?lhs
     apply (auto simp: ball_def dist_norm )
     apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt order_trans)
     using le_less_trans apply fastforce
@@ -8227,8 +8217,8 @@
   shows "cball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r < r' \<or> r < 0"
         (is "?lhs = ?rhs")
 proof
-  assume ?lhs 
-  then show ?rhs 
+  assume ?lhs
+  then show ?rhs
   proof (cases "r < 0")
     case True then show ?rhs by simp
   next
@@ -8256,7 +8246,7 @@
     then show ?rhs by (simp add: dist_norm)
   qed
 next
-  assume ?rhs then show ?lhs 
+  assume ?rhs then show ?lhs
     apply (auto simp: ball_def dist_norm )
     apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt le_less_trans)
     using le_less_trans apply fastforce
@@ -8268,10 +8258,10 @@
   shows "ball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
         (is "?lhs = ?rhs")
 proof (cases "r \<le> 0")
-  case True then show ?thesis   
+  case True then show ?thesis
     using dist_not_less_zero less_le_trans by force
 next
-  case False show ?thesis  
+  case False show ?thesis
   proof
     assume ?lhs
     then have "(cball a r \<subseteq> cball a' r')"
@@ -8280,7 +8270,7 @@
       using False cball_subset_cball_iff by fastforce
   next
     assume ?rhs with False show ?lhs
-      using ball_subset_cball cball_subset_cball_iff by blast 
+      using ball_subset_cball cball_subset_cball_iff by blast
   qed
 qed
 
@@ -8289,10 +8279,10 @@
   shows "ball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
         (is "?lhs = ?rhs")
 proof (cases "r \<le> 0")
-  case True then show ?thesis   
+  case True then show ?thesis
     using dist_not_less_zero less_le_trans by force
 next
-  case False show ?thesis  
+  case False show ?thesis
   proof
     assume ?lhs
     then have "0 < r'"
@@ -8316,22 +8306,22 @@
   shows "ball x d = ball y e \<longleftrightarrow> d \<le> 0 \<and> e \<le> 0 \<or> x=y \<and> d=e"
         (is "?lhs = ?rhs")
 proof
-  assume ?lhs 
-  then show ?rhs 
+  assume ?lhs
+  then show ?rhs
   proof (cases "d \<le> 0 \<or> e \<le> 0")
-    case True 
+    case True
       with \<open>?lhs\<close> show ?rhs
         by safe (simp_all only: ball_eq_empty [of y e, symmetric] ball_eq_empty [of x d, symmetric])
   next
     case False
-    with \<open>?lhs\<close> show ?rhs 
+    with \<open>?lhs\<close> show ?rhs
       apply (auto simp add: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps)
       apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
       apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
       done
   qed
 next
-  assume ?rhs then show ?lhs 
+  assume ?rhs then show ?lhs
     by (auto simp add: set_eq_subset ball_subset_ball_iff)
 qed
 
@@ -8340,22 +8330,22 @@
   shows "cball x d = cball y e \<longleftrightarrow> d < 0 \<and> e < 0 \<or> x=y \<and> d=e"
         (is "?lhs = ?rhs")
 proof
-  assume ?lhs 
-  then show ?rhs 
+  assume ?lhs
+  then show ?rhs
   proof (cases "d < 0 \<or> e < 0")
-    case True 
+    case True
       with \<open>?lhs\<close> show ?rhs
         by safe (simp_all only: cball_eq_empty [of y e, symmetric] cball_eq_empty [of x d, symmetric])
   next
     case False
-    with \<open>?lhs\<close> show ?rhs 
+    with \<open>?lhs\<close> show ?rhs
       apply (auto simp add: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps)
       apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
       apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
       done
   qed
 next
-  assume ?rhs then show ?lhs 
+  assume ?rhs then show ?lhs
     by (auto simp add: set_eq_subset cball_subset_cball_iff)
 qed
 
@@ -8363,7 +8353,7 @@
   fixes x :: "'a :: euclidean_space"
   shows "ball x d = cball y e \<longleftrightarrow> d \<le> 0 \<and> e < 0" (is "?lhs = ?rhs")
 proof
-  assume ?lhs 
+  assume ?lhs
   then show ?rhs
     apply (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
     apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
@@ -8371,7 +8361,7 @@
     using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
     done
 next
-  assume ?rhs then show ?lhs 
+  assume ?rhs then show ?lhs
     by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff)
 qed
 
@@ -8379,7 +8369,7 @@
   fixes x :: "'a :: euclidean_space"
   shows "cball x d = ball y e \<longleftrightarrow> d < 0 \<and> e \<le> 0" (is "?lhs = ?rhs")
 proof
-  assume ?lhs 
+  assume ?lhs
   then show ?rhs
     apply (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
     apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
@@ -8387,7 +8377,7 @@
     using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
     done
 next
-  assume ?rhs then show ?lhs 
+  assume ?rhs then show ?lhs
     by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff)
 qed
 
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Multivariate_Analysis/Weierstrass.thy
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -380,9 +380,7 @@
       by (simp add: algebra_simps power_mult power2_eq_square power_mult_distrib [symmetric])
     also have "... \<le> (1/(k * (p t))^n) * 1"
       apply (rule mult_left_mono [OF power_le_one])
-      apply (metis diff_le_iff(1) less_eq_real_def mult.commute power_le_one power_mult ptn_pos ptn_le)
-      using pt_pos [OF t] \<open>k>0\<close>
-      apply auto
+      using pt_pos \<open>k>0\<close> p01 power_le_one t apply auto
       done
     also have "... \<le> (1 / (k*\<delta>))^n"
       using \<open>k>0\<close> \<delta>01  power_mono pt_\<delta> t
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/NSA/Examples/NSPrimes.thy
--- a/src/HOL/NSA/Examples/NSPrimes.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/NSA/Examples/NSPrimes.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -61,7 +61,7 @@
 (* Goldblatt: Exercise 5.11(3a) - p 57  *)
 lemma starprime:
   "starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
-by (transfer, auto simp add: prime_nat_def)
+by (transfer, auto simp add: prime_def)
 
 (* Goldblatt Exercise 5.11(3b) - p 57  *)
 lemma hyperprime_factor_exists [rule_format]:
@@ -262,17 +262,14 @@
 text{*Already proved as @{text primes_infinite}, but now using non-standard naturals.*}
 theorem not_finite_prime: "~ finite {p::nat. prime p}"
 apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
-apply (cut_tac hypnat_dvd_all_hypnat_of_nat)
-apply (erule exE)
-apply (erule conjE)
-apply (subgoal_tac "1 < N + 1")
-prefer 2 apply (blast intro: hypnat_add_one_gt_one)
+using hypnat_dvd_all_hypnat_of_nat
+apply clarify
+apply (drule hypnat_add_one_gt_one)
 apply (drule hyperprime_factor_exists)
-apply auto
+apply clarify
 apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
-apply (force simp add: starprime_def, safe)
-apply (drule_tac x = x in bspec, auto)
-apply (metis add.commute hdvd_diff hdvd_one_eq_one hypnat_diff_add_inverse2 hypnat_one_not_prime)
+apply (force simp add: starprime_def)
+apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime imageE insert_iff mem_Collect_eq zero_not_prime_nat)
 done
 
 end
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -294,8 +294,8 @@
     from 2 show ?thesis
       apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
         dest: prime_gt_Suc_0_nat)
-      apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_def)
-      apply (metis One_nat_def Suc_le_eq aux prime_nat_def)
+      apply (metis One_nat_def Suc_le_eq less_not_refl prime_def)
+      apply (metis One_nat_def Suc_le_eq aux prime_def)
       done
   qed
 qed
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -457,11 +457,11 @@
   proof
     assume "prime n"
     then show ?rhs
-      by (metis one_not_prime_nat prime_nat_def)
+      by (metis one_not_prime_nat prime_def)
   next
     assume ?rhs
     with False show "prime n"
-      by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_nat_def)
+      by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_def)
   qed
 qed
 
@@ -538,7 +538,7 @@
   and pp: "prime p" and pn: "p dvd n"
   shows "[p = 1] (mod q)"
 proof -
-  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp one_not_prime_nat zero_not_prime_nat by auto
+  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp one_not_prime_nat zero_not_prime_nat by (auto intro: prime_gt_0_nat)
   obtain k where k: "a ^ (q * r) - 1 = n*k"
     by (metis an cong_to_1_nat dvd_def nqr)
   from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
@@ -689,7 +689,7 @@
     from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast
     from n m have m0: "m > 0" "m\<noteq>0" by auto
     have "1 < p"
-      by (metis p(1) prime_nat_def)
+      by (metis p(1) prime_def)
     with m0 m have mn: "m < n" by auto
     from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" ..
     from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def)
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -37,38 +37,33 @@
 definition prime :: "nat \<Rightarrow> bool"
   where "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
 
-lemmas prime_nat_def = prime_def
-
-
 subsection \<open>Primes\<close>
 
 lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
-  apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
+  apply (auto simp add: prime_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
   apply (metis dvd_eq_mod_eq_0 even_Suc mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
   done
 
-(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
+lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > 0"
+  unfolding prime_def by auto
 
-lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
-  unfolding prime_nat_def by auto
+lemma prime_ge_1_nat: "prime p \<Longrightarrow> p >= 1"
+  unfolding prime_def by auto
 
-lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
-  unfolding prime_nat_def by auto
+lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > 1"
+  unfolding prime_def by auto
 
-lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
-  unfolding prime_nat_def by auto
-
-lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
-  unfolding prime_nat_def by auto
+lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p >= Suc 0"
+  unfolding prime_def by auto
 
-lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
-  unfolding prime_nat_def by auto
+lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
+  unfolding prime_def by auto
 
-lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
-  unfolding prime_nat_def by auto
+lemma prime_ge_2_nat: "prime p \<Longrightarrow> p >= 2"
+  unfolding prime_def by auto
 
 lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
-  apply (unfold prime_nat_def)
+  apply (unfold prime_def)
   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
   done
 
@@ -105,7 +100,7 @@
 
 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
-  unfolding prime_nat_def dvd_def apply auto
+  unfolding prime_def dvd_def apply auto
   by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
       n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
 
@@ -129,18 +124,18 @@
 subsubsection \<open>Make prime naively executable\<close>
 
 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
-  by (simp add: prime_nat_def)
+  by (simp add: prime_def)
 
 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
-  by (simp add: prime_nat_def)
+  by (simp add: prime_def)
 
 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
-  by (simp add: prime_nat_def)
+  by (simp add: prime_def)
 
 lemma prime_nat_code [code]:
     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   apply (simp add: Ball_def)
-  apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
+  apply (metis One_nat_def less_not_refl prime_def dvd_triv_right not_prime_eq_prod_nat)
   done
 
 lemma prime_nat_simp:
@@ -178,7 +173,7 @@
   using two_is_prime_nat
   apply blast
   apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
-    nat_dvd_not_less neq0_conv prime_nat_def)
+    nat_dvd_not_less neq0_conv prime_def)
   done
 
 text \<open>One property of coprimality is easier to prove via prime factors.\<close>
@@ -239,7 +234,8 @@
       by (rule dvd_diff_nat)
     then have "p dvd 1" by simp
     then have "p <= 1" by auto
-    moreover from \<open>prime p\<close> have "p > 1" by auto
+    moreover from \<open>prime p\<close> have "p > 1"
+      using prime_def by blast
     ultimately have False by auto}
   then have "n < p" by presburger
   with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
@@ -270,7 +266,7 @@
 proof -
   from assms have
     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
-    unfolding prime_nat_def by auto
+    unfolding prime_def by auto
   from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   have "p dvd p * q" by simp
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -107,9 +107,7 @@
   ultimately have "a ^ count M a dvd a ^ count N a"
     by (elim coprime_dvd_mult_nat)
   with a show ?thesis
-    apply (intro power_dvd_imp_le)
-    apply auto
-    done
+    using power_dvd_imp_le prime_def by blast
 next
   case False
   then show ?thesis
@@ -247,14 +245,14 @@
   using assms apply auto
   done
 
-lemma prime_factors_gt_0_nat [elim]:
+lemma prime_factors_gt_0_nat:
   fixes p :: nat
   shows "p \<in> prime_factors x \<Longrightarrow> p > 0"
-  by (auto dest!: prime_factors_prime_nat)
+    using prime_factors_prime_nat by force
 
-lemma prime_factors_gt_0_int [elim]:
+lemma prime_factors_gt_0_int:
   shows "x \<ge> 0 \<Longrightarrow> p \<in> prime_factors x \<Longrightarrow> int p > (0::int)"
-  by auto
+    by (simp add: prime_factors_gt_0_nat)
 
 lemma prime_factors_finite_nat [iff]:
   fixes n :: nat
@@ -303,7 +301,8 @@
 proof -
   from assms have "f \<in> multiset"
     by (auto simp add: multiset_def)
-  moreover from assms have "n > 0" by force
+  moreover from assms have "n > 0" 
+    by (auto intro: prime_gt_0_nat)
   ultimately have "multiset_prime_factorization n = Abs_multiset f"
     apply (unfold multiset_prime_factorization_def)
     apply (subst if_P, assumption)
@@ -723,16 +722,16 @@
     (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))"
   (is "_ = ?z")
 proof -
-  have [arith]: "?z > 0"
-    by auto
+  have [arith]: "?z > 0" 
+    using prime_factors_gt_0_nat by auto
   have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)"
     apply (subst multiplicity_prod_prime_powers_nat)
     apply auto
     done
   have "?z dvd x"
-    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
+    by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
   moreover have "?z dvd y"
-    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
+    by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
   moreover have "w dvd x \<and> w dvd y \<longrightarrow> w dvd ?z" for w
   proof (cases "w = 0")
     case True
@@ -758,7 +757,7 @@
   (is "_ = ?z")
 proof -
   have [arith]: "?z > 0"
-    by auto
+    by (auto intro: prime_gt_0_nat)
   have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)"
     apply (subst multiplicity_prod_prime_powers_nat)
     apply auto
@@ -776,7 +775,7 @@
     then show ?thesis
       apply auto
       apply (rule multiplicity_dvd'_nat)
-      apply (auto intro: dvd_multiplicity_nat simp add: aux)
+      apply (auto intro: prime_gt_0_nat dvd_multiplicity_nat simp add: aux)
       done
   qed
   ultimately have "?z = lcm x y"
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -665,7 +665,8 @@
   apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
   apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   apply (frule_tac a = m in pos_mod_bound)
-  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
+  apply (simp del: pos_mod_bound add: algebra_simps nat_diff_distrib gcd_diff2 nat_le_eq_zle)
+  apply (metis dual_order.strict_implies_order gcd.simps gcd_0_left gcd_diff2 mod_by_0 nat_mono)
   done
 
 lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Orderings.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -310,6 +310,11 @@
   "(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
 using linear by blast
 
+lemma (in linorder) le_cases3:
+  "\<lbrakk>\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> P; \<lbrakk>y \<le> x; x \<le> z\<rbrakk> \<Longrightarrow> P; \<lbrakk>x \<le> z; z \<le> y\<rbrakk> \<Longrightarrow> P;
+    \<lbrakk>z \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> P; \<lbrakk>y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> P; \<lbrakk>z \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by (blast intro: le_cases)
+
 lemma linorder_cases [case_names less equal greater]:
   "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
 using less_linear by blast
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -46,8 +46,8 @@
   assume l_r[simp]: "\<And>n. l n \<le> r n" and "a \<le> b" and disj: "disjoint_family (\<lambda>n. {l n<..r n})"
   assume lr_eq_ab: "(\<Union>i. {l i<..r i}) = {a<..b}"
 
-  have [intro, simp]: "\<And>a b. a \<le> b \<Longrightarrow> 0 \<le> F b - F a"
-    by (auto intro!: l_r mono_F simp: diff_le_iff)
+  have [intro, simp]: "\<And>a b. a \<le> b \<Longrightarrow> F a \<le> F b"
+    by (auto intro!: l_r mono_F)
 
   { fix S :: "nat set" assume "finite S"
     moreover note `a \<le> b`
@@ -92,7 +92,7 @@
           by (auto simp add: Ioc_subset_iff intro!: mono_F)
         finally show ?case
           by (auto intro: add_mono)
-      qed (simp add: `a \<le> b` less_le)
+      qed (auto simp add: `a \<le> b` less_le)
     qed }
   note claim1 = this
 
@@ -280,7 +280,7 @@
     by (auto simp add: claim1 intro!: suminf_bound)
   ultimately show "(\<Sum>n. ereal (F (r n) - F (l n))) = ereal (F b - F a)"
     by simp
-qed (auto simp: Ioc_inj diff_le_iff mono_F)
+qed (auto simp: Ioc_inj mono_F)
 
 lemma measure_interval_measure_Ioc:
   assumes "a \<le> b"
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -29,7 +29,7 @@
   by (induct m) auto
 
 lemma prime_eq: "prime (p::nat) = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
-  apply (simp add: prime_nat_def)
+  apply (simp add: prime_def)
   apply (rule iffI)
   apply blast
   apply (erule conjE)
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -9,6 +9,10 @@
 imports Real Topological_Spaces
 begin
 
+
+lemma (in ordered_ab_group_add) diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
+  by (simp add: le_diff_eq)
+
 subsection \<open>Locale for additive functions\<close>
 
 locale additive =
@@ -777,6 +781,11 @@
   thus ?thesis by simp
 qed
 
+lemma norm_add_leD:
+  fixes a b :: "'a::real_normed_vector"
+  shows "norm (a + b) \<le> c \<Longrightarrow> norm b \<le> norm a + c"
+    by (metis add.commute diff_le_eq norm_diff_ineq order.trans)
+
 lemma norm_diff_triangle_ineq:
   fixes a b c d :: "'a::real_normed_vector"
   shows "norm ((a + b) - (c + d)) \<le> norm (a - c) + norm (b - d)"
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Rings.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -1559,6 +1559,9 @@
 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   by (simp add: not_less)
 
+proposition abs_eq_iff: "abs x = abs y \<longleftrightarrow> x = y \<or> x = -y"
+  by (auto simp add: abs_if split: split_if_asm)
+
 end
 
 class linordered_ring_strict = ring + linordered_semiring_strict
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Transcendental.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -10,6 +10,16 @@
 imports Binomial Series Deriv NthRoot
 begin
 
+lemma of_int_leD: 
+  fixes x :: "'a :: linordered_idom"
+  shows "\<bar>of_int n\<bar> \<le> x \<Longrightarrow> n=0 \<or> x\<ge>1"
+  by (metis (no_types) le_less_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff)
+
+lemma of_int_lessD: 
+  fixes x :: "'a :: linordered_idom"
+  shows "\<bar>of_int n\<bar> < x \<Longrightarrow> n=0 \<or> x>1"
+  by (metis less_le_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff)
+
 lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
 
 lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
@@ -1979,8 +1989,7 @@
       assume "x \<le> y" "y \<le> a"
       with \<open>0 < x\<close> \<open>a < 1\<close> have "0 < 1 / y - 1" "0 < y"
         by (auto simp: field_simps)
-      with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
-        by auto
+      with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z" by blast
     qed
     also have "\<dots> \<le> 0"
       using ln_le_minus_one \<open>0 < x\<close> \<open>x < a\<close> by (auto simp: field_simps)
@@ -3090,6 +3099,11 @@
   using cos_add [where x=x and y=x]
   by (simp add: power2_eq_square)
 
+lemma sin_cos_le1:
+  fixes x::real shows "abs (sin x * sin y + cos x * cos y) \<le> 1"
+  using cos_diff [of x y]
+  by (metis abs_cos_le_one add.commute)
+
 lemma DERIV_fun_pow: "DERIV g x :> m ==>
       DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
   by (auto intro!: derivative_eq_intros simp:)
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -784,8 +784,7 @@
     qed
     hence "y < r" by simp
     with ypos have  dless: "?d < (r * ?d)/y"
-      by (simp add: pos_less_divide_eq mult.commute [of ?d]
-                    mult_strict_right_mono dpos)
+      using dpos less_divide_eq_1 by fastforce
     have "r + ?d < r*x"
     proof -
       have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/ex/Sqrt.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -14,7 +14,7 @@
   assumes "prime (p::nat)"
   shows "sqrt p \<notin> \<rat>"
 proof
-  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def)
+  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
@@ -59,7 +59,7 @@
   assumes "prime (p::nat)"
   shows "sqrt p \<notin> \<rat>"
 proof
-  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def)
+  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
diff -r 0d399131008f -r d50b993b4fb9 src/HOL/ex/Sqrt_Script.thy
--- a/src/HOL/ex/Sqrt_Script.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/ex/Sqrt_Script.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -17,7 +17,7 @@
 subsection \<open>Preliminaries\<close>
 
 lemma prime_nonzero:  "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
-  by (force simp add: prime_nat_def)
+  by (force simp add: prime_def)
 
 lemma prime_dvd_other_side:
     "(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
@@ -32,7 +32,7 @@
   apply (erule disjE)
    apply (frule mult_le_mono, assumption)
    apply auto
-  apply (force simp add: prime_nat_def)
+  apply (force simp add: prime_def)
   done
 
 lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"