# HG changeset patch
# User paulson
# Date 1530830237 -3600
# Node ID 57b9d993cc987e41f3898a64551a5b40d92a9205
# Parent  90381a0f54740c5e1417a3ca2f5b2777984f0315# Parent  5b05ede597b8d0004df01450f1b0feff667f4ada
merged

diff -r 90381a0f5474 -r 57b9d993cc98 src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Thu Jul 05 23:21:28 2018 +0200
+++ b/src/HOL/Algebra/Module.thy	Thu Jul 05 23:37:17 2018 +0100
@@ -167,4 +167,85 @@
     by (simp add: Pi_def smult_r_distr)
 qed
 
+
+
+subsection \<open>Submodules\<close>
+
+locale submodule = subgroup H "add_monoid M" for H and R :: "('a, 'b) ring_scheme" and M (structure)
++ assumes smult_closed [simp, intro]:
+      "\<lbrakk>a \<in> carrier R; x \<in> H\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>M\<^esub> x \<in> H"
+
+
+lemma (in module) submoduleI :
+  assumes subset: "H \<subseteq> carrier M"
+    and zero: "\<zero>\<^bsub>M\<^esub> \<in> H"
+    and a_inv: "!!a. a \<in> H \<Longrightarrow> \<ominus>\<^bsub>M\<^esub> a \<in> H"
+    and add : "\<And> a b. \<lbrakk>a \<in> H ; b \<in> H\<rbrakk> \<Longrightarrow> a \<oplus>\<^bsub>M\<^esub> b \<in> H"
+    and smult_closed : "\<And> a x. \<lbrakk>a \<in> carrier R; x \<in> H\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>M\<^esub> x \<in> H"
+  shows "submodule H R M"
+  apply (intro submodule.intro subgroup.intro)
+  using assms unfolding submodule_axioms_def
+  by (simp_all add : a_inv_def)
+
+
+lemma (in module) submoduleE :
+  assumes "submodule H R M"
+  shows "H \<subseteq> carrier M"
+    and "H \<noteq> {}"
+    and "\<And>a. a \<in> H \<Longrightarrow> \<ominus>\<^bsub>M\<^esub> a \<in> H"
+    and "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> H\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>M\<^esub> b \<in> H"
+    and "\<And> a b. \<lbrakk>a \<in> H ; b \<in> H\<rbrakk> \<Longrightarrow> a \<oplus>\<^bsub>M\<^esub> b \<in> H"
+    and "\<And> x. x \<in> H \<Longrightarrow> (a_inv M x) \<in> H"
+  using group.subgroupE[of "add_monoid M" H, OF _ submodule.axioms(1)[OF assms]] a_comm_group
+        submodule.smult_closed[OF assms]
+  unfolding comm_group_def a_inv_def
+  by auto
+
+
+lemma (in module) carrier_is_submodule :
+"submodule (carrier M) R M"
+  apply (intro  submoduleI)
+  using a_comm_group group.inv_closed unfolding comm_group_def a_inv_def group_def monoid_def
+  by auto
+
+lemma (in submodule) submodule_is_module :
+  assumes "module R M"
+  shows "module R (M\<lparr>carrier := H\<rparr>)"
+proof (auto intro! : moduleI abelian_group.intro)
+  show "cring (R)" using assms unfolding module_def by auto
+  show "abelian_monoid (M\<lparr>carrier := H\<rparr>)"
+    using comm_monoid.submonoid_is_comm_monoid[OF _ subgroup_is_submonoid] assms
+    unfolding abelian_monoid_def module_def abelian_group_def
+    by auto
+  thus "abelian_group_axioms (M\<lparr>carrier := H\<rparr>)"
+    using subgroup_is_group assms
+    unfolding abelian_group_axioms_def comm_group_def abelian_monoid_def module_def abelian_group_def
+    by auto
+  show "\<And>z. z \<in> H \<Longrightarrow> \<one>\<^bsub>R\<^esub> \<odot> z = z"
+    using subgroup_imp_subset[OF subgroup_axioms] module.smult_one[OF assms]
+    by auto
+  fix a b x y assume a : "a \<in> carrier R" and b : "b \<in> carrier R" and x : "x \<in> H" and y : "y \<in> H"
+  show "(a \<oplus>\<^bsub>R\<^esub> b) \<odot> x = a \<odot> x \<oplus> b \<odot> x"
+    using a b x module.smult_l_distr[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+    by auto
+  show "a \<odot> (x \<oplus> y) = a \<odot> x \<oplus> a \<odot> y"
+    using a x y module.smult_r_distr[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+    by auto
+  show "a \<otimes>\<^bsub>R\<^esub> b \<odot> x = a \<odot> (b \<odot> x)"
+    using a b x module.smult_assoc1[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+    by auto
+qed
+
+
+lemma (in module) module_incl_imp_submodule :
+  assumes "H \<subseteq> carrier M"
+    and "module R (M\<lparr>carrier := H\<rparr>)"
+  shows "submodule H R M"
+  apply (intro submodule.intro)
+  using add.group_incl_imp_subgroup[OF assms(1)] assms module.axioms(2)[OF assms(2)]
+        module.smult_closed[OF assms(2)]
+  unfolding abelian_group_def abelian_group_axioms_def comm_group_def submodule_axioms_def
+  by simp_all
+
+
 end
diff -r 90381a0f5474 -r 57b9d993cc98 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Jul 05 23:21:28 2018 +0200
+++ b/src/HOL/Limits.thy	Thu Jul 05 23:37:17 2018 +0100
@@ -2442,7 +2442,7 @@
   assumes "0 < R"
     and "\<And>x. x \<noteq> a \<Longrightarrow> norm (x - a) < R \<Longrightarrow> f x = g x"
   shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>a\<rightarrow> l"
-  by (rule metric_LIM_equal2 [OF assms]) (simp_all add: dist_norm)
+  by (rule metric_LIM_equal2 [OF _ assms]) (simp_all add: dist_norm)
 
 lemma LIM_compose2:
   fixes a :: "'a::real_normed_vector"
@@ -2556,15 +2556,7 @@
   assumes "uniformly_continuous_on S f" "Cauchy X" "\<And>n. X n \<in> S"
   shows "Cauchy (\<lambda>n. f (X n))"
   using assms
-  apply (simp only: uniformly_continuous_on_def)
-  apply (rule metric_CauchyI)
-  apply (drule_tac x=e in spec)
-  apply safe
-  apply (drule_tac e=d in metric_CauchyD)
-   apply safe
-  apply (rule_tac x=M in exI)
-  apply simp
-  done
+  unfolding uniformly_continuous_on_def  by (meson Cauchy_def)
 
 lemma isUCont_Cauchy: "isUCont f \<Longrightarrow> Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all
diff -r 90381a0f5474 -r 57b9d993cc98 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Jul 05 23:21:28 2018 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Jul 05 23:37:17 2018 +0100
@@ -54,7 +54,7 @@
 
 global_interpretation real_vector?: vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
   rewrites "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
-    and "Vector_Spaces.linear ( * ) ( *\<^sub>R) = linear"
+    and "Vector_Spaces.linear ( *) ( *\<^sub>R) = linear"
   defines dependent_raw_def: dependent = real_vector.dependent
     and representation_raw_def: representation = real_vector.representation
     and subspace_raw_def: subspace = real_vector.subspace
@@ -66,8 +66,8 @@
       apply (rule scaleR_add_left)
      apply (rule scaleR_scaleR)
     apply (rule scaleR_one)
-   apply (force simp add: linear_def)
-  apply (force simp add: linear_def real_scaleR_def[abs_def])
+   apply (force simp: linear_def)
+  apply (force simp: linear_def real_scaleR_def[abs_def])
   done
 
 hide_const (open)\<comment> \<open>locale constants\<close>
@@ -83,7 +83,7 @@
 
 global_interpretation real_vector?: vector_space_pair "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
   rewrites  "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
-    and "Vector_Spaces.linear ( * ) ( *\<^sub>R) = linear"
+    and "Vector_Spaces.linear ( *) ( *\<^sub>R) = linear"
   defines construct_raw_def: construct = real_vector.construct
   apply unfold_locales
   unfolding linear_def real_scaleR_def
@@ -92,7 +92,7 @@
 hide_const (open)\<comment> \<open>locale constants\<close>
   real_vector.construct
 
-lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g o f)"
+lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g \<circ> f)"
   unfolding linear_def by (rule Vector_Spaces.linear_compose)
 
 text \<open>Recover original theorem names\<close>
@@ -161,12 +161,7 @@
 
 lemma inverse_scaleR_distrib: "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
   for x :: "'a::{real_div_algebra,division_ring}"
-  apply (cases "a = 0")
-   apply simp
-  apply (cases "x = 0")
-   apply simp
-  apply (erule (1) nonzero_inverse_scaleR_distrib)
-  done
+  by (metis inverse_zero nonzero_inverse_scaleR_distrib scale_eq_0_iff)
 
 lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment> \<open>legacy name\<close>
 
@@ -367,56 +362,32 @@
 lemma Reals_numeral [simp]: "numeral w \<in> \<real>"
   by (subst of_real_numeral [symmetric], rule Reals_of_real)
 
-lemma Reals_0 [simp]: "0 \<in> \<real>"
-  apply (unfold Reals_def)
-  apply (rule range_eqI)
-  apply (rule of_real_0 [symmetric])
-  done
-
-lemma Reals_1 [simp]: "1 \<in> \<real>"
-  apply (unfold Reals_def)
-  apply (rule range_eqI)
-  apply (rule of_real_1 [symmetric])
-  done
+lemma Reals_0 [simp]: "0 \<in> \<real>" and Reals_1 [simp]: "1 \<in> \<real>"
+  by (simp_all add: Reals_def)
 
 lemma Reals_add [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a + b \<in> \<real>"
-  apply (auto simp add: Reals_def)
-  apply (rule range_eqI)
-  apply (rule of_real_add [symmetric])
-  done
+  by (metis (no_types, hide_lams) Reals_def Reals_of_real imageE of_real_add)
 
 lemma Reals_minus [simp]: "a \<in> \<real> \<Longrightarrow> - a \<in> \<real>"
-  by (auto simp add: Reals_def)
+  by (auto simp: Reals_def)
 
 lemma Reals_minus_iff [simp]: "- a \<in> \<real> \<longleftrightarrow> a \<in> \<real>"
   apply (auto simp: Reals_def)
   by (metis add.inverse_inverse of_real_minus rangeI)
 
 lemma Reals_diff [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a - b \<in> \<real>"
-  apply (auto simp add: Reals_def)
-  apply (rule range_eqI)
-  apply (rule of_real_diff [symmetric])
-  done
+  by (metis Reals_add Reals_minus_iff add_uminus_conv_diff)
 
 lemma Reals_mult [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a * b \<in> \<real>"
-  apply (auto simp add: Reals_def)
-  apply (rule range_eqI)
-  apply (rule of_real_mult [symmetric])
-  done
+  by (metis (no_types, lifting) Reals_def Reals_of_real imageE of_real_mult)
 
 lemma nonzero_Reals_inverse: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> inverse a \<in> \<real>"
   for a :: "'a::real_div_algebra"
-  apply (auto simp add: Reals_def)
-  apply (rule range_eqI)
-  apply (erule nonzero_of_real_inverse [symmetric])
-  done
+  by (metis Reals_def Reals_of_real imageE of_real_inverse)
 
 lemma Reals_inverse: "a \<in> \<real> \<Longrightarrow> inverse a \<in> \<real>"
   for a :: "'a::{real_div_algebra,division_ring}"
-  apply (auto simp add: Reals_def)
-  apply (rule range_eqI)
-  apply (rule of_real_inverse [symmetric])
-  done
+  using nonzero_Reals_inverse by fastforce
 
 lemma Reals_inverse_iff [simp]: "inverse x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
   for x :: "'a::{real_div_algebra,division_ring}"
@@ -424,24 +395,15 @@
 
 lemma nonzero_Reals_divide: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a / b \<in> \<real>"
   for a b :: "'a::real_field"
-  apply (auto simp add: Reals_def)
-  apply (rule range_eqI)
-  apply (erule nonzero_of_real_divide [symmetric])
-  done
+  by (simp add: divide_inverse)
 
 lemma Reals_divide [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a / b \<in> \<real>"
   for a b :: "'a::{real_field,field}"
-  apply (auto simp add: Reals_def)
-  apply (rule range_eqI)
-  apply (rule of_real_divide [symmetric])
-  done
+  using nonzero_Reals_divide by fastforce
 
 lemma Reals_power [simp]: "a \<in> \<real> \<Longrightarrow> a ^ n \<in> \<real>"
   for a :: "'a::real_algebra_1"
-  apply (auto simp add: Reals_def)
-  apply (rule range_eqI)
-  apply (rule of_real_power [symmetric])
-  done
+  by (metis Reals_def Reals_of_real imageE of_real_power)
 
 lemma Reals_cases [cases set: Reals]:
   assumes "q \<in> \<real>"
@@ -478,11 +440,7 @@
 begin
 
 lemma scaleR_mono: "a \<le> b \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> x \<Longrightarrow> a *\<^sub>R x \<le> b *\<^sub>R y"
-  apply (erule scaleR_right_mono [THEN order_trans])
-   apply assumption
-  apply (erule scaleR_left_mono)
-  apply assumption
-  done
+  by (meson local.dual_order.trans local.scaleR_left_mono local.scaleR_right_mono)
 
 lemma scaleR_mono': "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R d"
   by (rule scaleR_mono) (auto intro: order.trans)
@@ -542,7 +500,7 @@
 
 lemma split_scaleR_neg_le: "(0 \<le> a \<and> x \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> x) \<Longrightarrow> a *\<^sub>R x \<le> 0"
   for x :: "'a::ordered_real_vector"
-  by (auto simp add: scaleR_nonneg_nonpos scaleR_nonpos_nonneg)
+  by (auto simp: scaleR_nonneg_nonpos scaleR_nonpos_nonneg)
 
 lemma le_add_iff1: "a *\<^sub>R e + c \<le> b *\<^sub>R e + d \<longleftrightarrow> (a - b) *\<^sub>R e + c \<le> d"
   for c d e :: "'a::ordered_real_vector"
@@ -554,14 +512,12 @@
 
 lemma scaleR_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b"
   for a b :: "'a::ordered_real_vector"
-  apply (drule scaleR_left_mono [of _ _ "- c"])
-   apply simp_all
+  apply (drule scaleR_left_mono [of _ _ "- c"], simp_all)
   done
 
 lemma scaleR_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R c"
   for c :: "'a::ordered_real_vector"
-  apply (drule scaleR_right_mono [of _ _ "- c"])
-   apply simp_all
+  apply (drule scaleR_right_mono [of _ _ "- c"], simp_all)
   done
 
 lemma scaleR_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a *\<^sub>R b"
@@ -570,7 +526,7 @@
 
 lemma split_scaleR_pos_le: "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a *\<^sub>R b"
   for b :: "'a::ordered_real_vector"
-  by (auto simp add: scaleR_nonneg_nonneg scaleR_nonpos_nonpos)
+  by (auto simp: scaleR_nonneg_nonneg scaleR_nonpos_nonpos)
 
 lemma zero_le_scaleR_iff:
   fixes b :: "'a::ordered_real_vector"
@@ -612,7 +568,7 @@
 
 lemma scaleR_le_cancel_left: "c *\<^sub>R a \<le> c *\<^sub>R b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   for b :: "'a::ordered_real_vector"
-  by (auto simp add: neq_iff scaleR_left_mono scaleR_left_mono_neg
+  by (auto simp: neq_iff scaleR_left_mono scaleR_left_mono_neg
       dest: scaleR_left_mono[where a="inverse c"] scaleR_left_mono_neg[where c="inverse c"])
 
 lemma scaleR_le_cancel_left_pos: "0 < c \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b \<longleftrightarrow> a \<le> b"
@@ -752,12 +708,14 @@
 
 lemma norm_triangle_ineq3: "\<bar>norm a - norm b\<bar> \<le> norm (a - b)"
   for a b :: "'a::real_normed_vector"
-  apply (subst abs_le_iff)
-  apply auto
-   apply (rule norm_triangle_ineq2)
-  apply (subst norm_minus_commute)
-  apply (rule norm_triangle_ineq2)
-  done
+proof -
+  have "norm a - norm b \<le> norm (a - b)"
+    by (simp add: norm_triangle_ineq2)
+  moreover have "norm b - norm a \<le> norm (a - b)"
+    by (metis norm_minus_commute norm_triangle_ineq2)
+  ultimately show ?thesis
+    by (simp add: abs_le_iff)
+qed
 
 lemma norm_triangle_ineq4: "norm (a - b) \<le> norm a + norm b"
   for a b :: "'a::real_normed_vector"
@@ -854,22 +812,15 @@
   by (subst of_real_of_int_eq [symmetric], rule norm_of_real)
 
 lemma norm_of_nat [simp]: "norm (of_nat n::'a::real_normed_algebra_1) = of_nat n"
-  apply (subst of_real_of_nat_eq [symmetric])
-  apply (subst norm_of_real, simp)
-  done
+  by (metis abs_of_nat norm_of_real of_real_of_nat_eq)
 
 lemma nonzero_norm_inverse: "a \<noteq> 0 \<Longrightarrow> norm (inverse a) = inverse (norm a)"
   for a :: "'a::real_normed_div_algebra"
-  apply (rule inverse_unique [symmetric])
-  apply (simp add: norm_mult [symmetric])
-  done
+  by (metis inverse_unique norm_mult norm_one right_inverse)
 
 lemma norm_inverse: "norm (inverse a) = inverse (norm a)"
   for a :: "'a::{real_normed_div_algebra,division_ring}"
-  apply (cases "a = 0")
-   apply simp
-  apply (erule nonzero_norm_inverse)
-  done
+  by (metis inverse_zero nonzero_norm_inverse norm_zero)
 
 lemma nonzero_norm_divide: "b \<noteq> 0 \<Longrightarrow> norm (a / b) = norm a / norm b"
   for a b :: "'a::real_normed_field"
@@ -982,7 +933,7 @@
   have "norm ((\<Prod>i\<in>insert i I. z i) - (\<Prod>i\<in>insert i I. w i)) =
     norm ((\<Prod>i\<in>I. z i) * (z i - w i) + ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) * w i)"
     (is "_ = norm (?t1 + ?t2)")
-    by (auto simp add: field_simps)
+    by (auto simp: field_simps)
   also have "\<dots> \<le> norm ?t1 + norm ?t2"
     by (rule norm_triangle_ineq)
   also have "norm ?t1 \<le> norm (\<Prod>i\<in>I. z i) * norm (z i - w i)"
@@ -998,7 +949,7 @@
   also have "norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
     using insert by auto
   finally show ?case
-    by (auto simp add: ac_simps mult_right_mono mult_left_mono)
+    by (auto simp: ac_simps mult_right_mono mult_left_mono)
 next
   case infinite
   then show ?case by simp
@@ -1012,7 +963,7 @@
   have "norm (z^m - w^m) = norm ((\<Prod> i < m. z) - (\<Prod> i < m. w))"
     by (simp add: prod_constant)
   also have "\<dots> \<le> (\<Sum>i<m. norm (z - w))"
-    by (intro norm_prod_diff) (auto simp add: assms)
+    by (intro norm_prod_diff) (auto simp: assms)
   also have "\<dots> = m * norm (z - w)"
     by simp
   finally show ?thesis .
@@ -1184,17 +1135,7 @@
 definition real_norm_def [simp]: "norm r = \<bar>r\<bar>"
 
 instance
-  apply intro_classes
-         apply (unfold real_norm_def real_scaleR_def)
-         apply (rule dist_real_def)
-        apply (simp add: sgn_real_def)
-       apply (rule uniformity_real_def)
-      apply (rule open_real_def)
-     apply (rule abs_eq_0)
-    apply (rule abs_triangle_ineq)
-   apply (rule abs_mult)
-  apply (rule abs_mult)
-  done
+  by intro_classes (auto simp: abs_mult open_real_def dist_real_def sgn_real_def uniformity_real_def)
 
 end
 
@@ -1369,7 +1310,7 @@
 
 corollary real_linearD:
   fixes f :: "real \<Rightarrow> real"
-  assumes "linear f" obtains c where "f = ( * ) c"
+  assumes "linear f" obtains c where "f = ( *) c"
   by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
 
 lemma linear_times_of_real: "linear (\<lambda>x. a * of_real x)"
@@ -1467,22 +1408,20 @@
 
 
 lemma bounded_linear_left: "bounded_linear (\<lambda>a. a ** b)"
-  apply (insert bounded)
-  apply safe
-  apply (rule_tac K="norm b * K" in bounded_linear_intro)
-    apply (rule add_left)
-   apply (rule scaleR_left)
-  apply (simp add: ac_simps)
-  done
+proof -
+  obtain K where "\<And>a b. norm (a ** b) \<le> norm a * norm b * K"
+    using pos_bounded by blast
+  then show ?thesis
+    by (rule_tac K="norm b * K" in bounded_linear_intro) (auto simp: algebra_simps scaleR_left add_left)
+qed
 
 lemma bounded_linear_right: "bounded_linear (\<lambda>b. a ** b)"
-  apply (insert bounded)
-  apply safe
-  apply (rule_tac K="norm a * K" in bounded_linear_intro)
-    apply (rule add_right)
-   apply (rule scaleR_right)
-  apply (simp add: ac_simps)
-  done
+proof -
+  obtain K where "\<And>a b. norm (a ** b) \<le> norm a * norm b * K"
+    using pos_bounded by blast
+  then show ?thesis
+    by (rule_tac K="norm a * K" in bounded_linear_intro) (auto simp: algebra_simps scaleR_right add_right)
+qed
 
 lemma prod_diff_prod: "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
   by (simp add: diff_left diff_right)
@@ -1493,14 +1432,11 @@
      apply (rule add_left)
     apply (rule scaleR_right)
    apply (rule scaleR_left)
-  apply (subst mult.commute)
-  apply (insert bounded)
-  apply blast
-  done
+  by (metis bounded mult.commute)
 
 lemma comp1:
   assumes "bounded_linear g"
-  shows "bounded_bilinear (\<lambda>x. ( ** ) (g x))"
+  shows "bounded_bilinear (\<lambda>x. ( **) (g x))"
 proof unfold_locales
   interpret g: bounded_linear g by fact
   show "\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b"
@@ -1564,7 +1500,7 @@
 
 lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. f x - g x)"
   using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g]
-  by (auto simp add: algebra_simps)
+  by (auto simp: algebra_simps)
 
 lemma bounded_linear_sum:
   fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
@@ -1602,13 +1538,10 @@
   qed
 qed
 
-lemma bounded_bilinear_mult: "bounded_bilinear (( * ) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
+lemma bounded_bilinear_mult: "bounded_bilinear (( *) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
   apply (rule bounded_bilinear.intro)
-      apply (rule distrib_right)
-     apply (rule distrib_left)
-    apply (rule mult_scaleR_left)
-   apply (rule mult_scaleR_right)
-  apply (rule_tac x="1" in exI)
+      apply (auto simp: algebra_simps)
+  apply (rule_tac x=1 in exI)
   apply (simp add: norm_mult_ineq)
   done
 
@@ -1632,12 +1565,8 @@
 
 lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR"
   apply (rule bounded_bilinear.intro)
-      apply (rule scaleR_left_distrib)
-     apply (rule scaleR_right_distrib)
-    apply simp
-   apply (rule scaleR_left_commute)
-  apply (rule_tac x="1" in exI)
-  apply simp
+      apply (auto simp: algebra_simps)
+  apply (rule_tac x=1 in exI, simp)
   done
 
 lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)"
@@ -1674,8 +1603,7 @@
 instance real_normed_algebra_1 \<subseteq> perfect_space
 proof
   show "\<not> open {x}" for x :: 'a
-    apply (simp only: open_dist dist_norm)
-    apply clarsimp
+    apply (clarsimp simp: open_dist dist_norm)
     apply (rule_tac x = "x + of_real (e/2)" in exI)
     apply simp
     done
@@ -1725,10 +1653,9 @@
 
 lemma eventually_at_le: "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a \<le> d \<longrightarrow> P x)"
   for a :: "'a::metric_space"
-  apply (simp only: eventually_at_filter eventually_nhds_metric)
-  apply auto
-  apply (rule_tac x="d / 2" in exI)
-  apply auto
+  unfolding eventually_at_filter eventually_nhds_metric
+  apply safe
+  apply (rule_tac x="d / 2" in exI, auto)
   done
 
 lemma eventually_at_left_real: "a > (b :: real) \<Longrightarrow> eventually (\<lambda>x. x \<in> {b<..<a}) (at_left a)"
@@ -1752,23 +1679,25 @@
 qed
 
 lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
-  apply (simp only: filterlim_at_top)
-  apply (intro allI)
-  apply (rule_tac c="nat \<lceil>Z + 1\<rceil>" in eventually_sequentiallyI)
-  apply linarith
+  apply (clarsimp simp: filterlim_at_top)
+  apply (rule_tac c="nat \<lceil>Z + 1\<rceil>" in eventually_sequentiallyI, linarith)
   done
 
 lemma filterlim_nat_sequentially: "filterlim nat sequentially at_top"
-  unfolding filterlim_at_top
-  apply (rule allI)
-  subgoal for Z by (auto intro!: eventually_at_top_linorderI[where c="int Z"])
-  done
+proof -
+  have "\<forall>\<^sub>F x in at_top. Z \<le> nat x" for Z
+    by (auto intro!: eventually_at_top_linorderI[where c="int Z"])
+  then show ?thesis
+    unfolding filterlim_at_top ..
+qed
 
 lemma filterlim_floor_sequentially: "filterlim floor at_top at_top"
-  unfolding filterlim_at_top
-  apply (rule allI)
-  subgoal for Z by (auto simp: le_floor_iff intro!: eventually_at_top_linorderI[where c="of_int Z"])
-  done
+proof -
+  have "\<forall>\<^sub>F x in at_top. Z \<le> \<lfloor>x\<rfloor>" for Z
+    by (auto simp: le_floor_iff intro!: eventually_at_top_linorderI[where c="of_int Z"])
+  then show ?thesis
+    unfolding filterlim_at_top ..
+qed
 
 lemma filterlim_sequentially_iff_filterlim_real:
   "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F"
@@ -1847,22 +1776,22 @@
   assumes f: "f \<midarrow>a\<rightarrow> l"
     and le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
   shows "g \<midarrow>a\<rightarrow> m"
-  by (rule metric_tendsto_imp_tendsto [OF f]) (auto simp add: eventually_at_topological le)
+  by (rule metric_tendsto_imp_tendsto [OF f]) (auto simp: eventually_at_topological le)
 
 lemma metric_LIM_equal2:
   fixes a :: "'a::metric_space"
-  assumes "0 < R"
+  assumes "g \<midarrow>a\<rightarrow> l" "0 < R"
     and "\<And>x. x \<noteq> a \<Longrightarrow> dist x a < R \<Longrightarrow> f x = g x"
-  shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>a\<rightarrow> l"
-  apply (rule topological_tendstoI)
-  apply (drule (2) topological_tendstoD)
-  apply (simp add: eventually_at)
-  apply safe
-  apply (rule_tac x="min d R" in exI)
-  apply safe
-   apply (simp add: assms(1))
-  apply (simp add: assms(2))
-  done
+  shows "f \<midarrow>a\<rightarrow> l"
+proof -
+  have "\<And>S. \<lbrakk>open S; l \<in> S; \<forall>\<^sub>F x in at a. g x \<in> S\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at a. f x \<in> S"
+    apply (clarsimp simp add: eventually_at)
+    apply (rule_tac x="min d R" in exI)
+     apply (auto simp: assms)
+    done
+  then show ?thesis
+    using assms by (simp add: tendsto_def)
+qed
 
 lemma metric_LIM_compose2:
   fixes a :: "'a::metric_space"
@@ -1933,7 +1862,7 @@
 lemma (in metric_space) Cauchy_altdef2: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
 proof 
   assume "Cauchy s"
-  then show ?rhs by (force simp add: Cauchy_def)
+  then show ?rhs by (force simp: Cauchy_def)
 next
     assume ?rhs
     {
@@ -1971,19 +1900,8 @@
 
 lemma (in metric_space) metric_Cauchy_iff2:
   "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < inverse(real (Suc j))))"
-  apply (simp add: Cauchy_def)
-  apply auto
-  apply (drule reals_Archimedean)
-  apply safe
-  apply (drule_tac x = n in spec)
-  apply auto
-  apply (rule_tac x = M in exI)
-  apply auto
-  apply (drule_tac x = m in spec)
-  apply simp
-  apply (drule_tac x = na in spec)
-  apply auto
-  done
+  apply (auto simp add: Cauchy_def)
+  by (metis less_trans of_nat_Suc reals_Archimedean)
 
 lemma Cauchy_iff2: "Cauchy X \<longleftrightarrow> (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse (real (Suc j))))"
   by (simp only: metric_Cauchy_iff2 dist_real_def)
@@ -2092,12 +2010,12 @@
   qed fact
 qed
 
+text\<open>apparently unused\<close>
 lemma (in metric_space) totally_bounded_metric:
   "totally_bounded S \<longleftrightarrow> (\<forall>e>0. \<exists>k. finite k \<and> S \<subseteq> (\<Union>x\<in>k. {y. dist x y < e}))"
-  apply (simp only: totally_bounded_def eventually_uniformity_metric imp_ex)
+  unfolding totally_bounded_def eventually_uniformity_metric imp_ex
   apply (subst all_comm)
-  apply (intro arg_cong[where f=All] ext)
-  apply safe
+  apply (intro arg_cong[where f=All] ext, safe)
   subgoal for e
     apply (erule allE[of _ "\<lambda>(x, y). dist x y < e"])
     apply auto
@@ -2125,7 +2043,7 @@
   fixes u::"nat \<Rightarrow> 'a::metric_space"
   assumes "Cauchy u"
     "strict_mono r"
-    "(u o r) \<longlonglongrightarrow> l"
+    "(u \<circ> r) \<longlonglongrightarrow> l"
   shows "u \<longlonglongrightarrow> l"
 proof -
   have *: "eventually (\<lambda>n. dist (u n) l < e) sequentially" if "e > 0" for e
@@ -2133,17 +2051,17 @@
     have "e/2 > 0" using that by auto
     then obtain N1 where N1: "\<And>m n. m \<ge> N1 \<Longrightarrow> n \<ge> N1 \<Longrightarrow> dist (u m) (u n) < e/2"
       using \<open>Cauchy u\<close> unfolding Cauchy_def by blast
-    obtain N2 where N2: "\<And>n. n \<ge> N2 \<Longrightarrow> dist ((u o r) n) l < e / 2"
-      using order_tendstoD(2)[OF iffD1[OF tendsto_dist_iff \<open>(u o r) \<longlonglongrightarrow> l\<close>] \<open>e/2 > 0\<close>]
+    obtain N2 where N2: "\<And>n. n \<ge> N2 \<Longrightarrow> dist ((u \<circ> r) n) l < e / 2"
+      using order_tendstoD(2)[OF iffD1[OF tendsto_dist_iff \<open>(u \<circ> r) \<longlonglongrightarrow> l\<close>] \<open>e/2 > 0\<close>]
       unfolding eventually_sequentially by auto
     have "dist (u n) l < e" if "n \<ge> max N1 N2" for n
     proof -
-      have "dist (u n) l \<le> dist (u n) ((u o r) n) + dist ((u o r) n) l"
+      have "dist (u n) l \<le> dist (u n) ((u \<circ> r) n) + dist ((u \<circ> r) n) l"
         by (rule dist_triangle)
-      also have "... < e/2 + e/2"
+      also have "\<dots> < e/2 + e/2"
         apply (intro add_strict_mono)
         using N1[of n "r n"] N2[of n] that unfolding comp_def
-        by (auto simp add: less_imp_le) (meson assms(2) less_imp_le order.trans seq_suble)
+        by (auto simp: less_imp_le) (meson assms(2) less_imp_le order.trans seq_suble)
       finally show ?thesis by simp
     qed 
     then show ?thesis unfolding eventually_sequentially by blast
diff -r 90381a0f5474 -r 57b9d993cc98 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu Jul 05 23:21:28 2018 +0200
+++ b/src/HOL/Series.thy	Thu Jul 05 23:37:17 2018 +0100
@@ -28,7 +28,7 @@
 
 text\<open>Variants of the definition\<close>
 lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
-  apply (simp add: sums_def)
+  unfolding sums_def
   apply (subst LIMSEQ_Suc_iff [symmetric])
   apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
   done
@@ -81,15 +81,9 @@
 
 lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. sum f {n * k ..< n * k + k}) sums s"
   apply (simp only: sums_def sum_nat_group tendsto_def eventually_sequentially)
-  apply safe
-  apply (erule_tac x=S in allE)
-  apply safe
-  apply (rule_tac x="N" in exI, safe)
-  apply (drule_tac x="n*k" in spec)
-  apply (erule mp)
-  apply (erule order_trans)
-  apply simp
-  done
+  apply (erule all_forward imp_forward exE| assumption)+
+  apply (rule_tac x="N" in exI)
+  by (metis le_square mult.commute mult.left_neutral mult_le_cancel2 mult_le_mono)
 
 lemma suminf_cong: "(\<And>n. f n = g n) \<Longrightarrow> suminf f = suminf g"
   by (rule arg_cong[of f g], rule ext) simp
@@ -454,16 +448,7 @@
   apply (drule summable_iff_convergent [THEN iffD1])
   apply (drule convergent_Cauchy)
   apply (simp only: Cauchy_iff LIMSEQ_iff)
-  apply safe
-  apply (drule_tac x="r" in spec)
-  apply safe
-  apply (rule_tac x="M" in exI)
-  apply safe
-  apply (drule_tac x="Suc n" in spec)
-  apply simp
-  apply (drule_tac x="n" in spec)
-  apply simp
-  done
+  by (metis add.commute add_diff_cancel_right' diff_zero le_SucI sum_lessThan_Suc)
 
 lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f"
   by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
@@ -725,17 +710,9 @@
 text \<open>Absolute convergence imples normal convergence.\<close>
 
 lemma summable_norm_cancel: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f"
-  apply (simp only: summable_Cauchy)
-  apply safe
-  apply (drule_tac x="e" in spec)
-  apply safe
-  apply (rule_tac x="N" in exI)
-  apply safe
-  apply (drule_tac x="m" in spec)
-  apply safe
-  apply (rule order_le_less_trans [OF norm_sum])
-  apply (rule order_le_less_trans [OF abs_ge_self])
-  apply simp
+  unfolding summable_Cauchy
+  apply (erule all_forward imp_forward ex_forward | assumption)+
+  apply (fastforce simp add: order_le_less_trans [OF norm_sum] order_le_less_trans [OF abs_ge_self])
   done
 
 lemma summable_norm: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))"
@@ -834,16 +811,10 @@
   shows "summable (\<lambda>n. norm (a n) * r^n)"
 proof (rule summable_comparison_test')
   show "summable (\<lambda>n. M * (r / r0) ^ n)"
-    using assms
-    by (auto simp add: summable_mult summable_geometric)
+    using assms by (auto simp add: summable_mult summable_geometric)
   show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n" for n
-    using r r0 M [of n]
-    apply (auto simp add: abs_mult field_simps)
-    apply (cases "r = 0")
-     apply simp
-     apply (cases n)
-      apply auto
-    done
+    using r r0 M [of n] dual_order.order_iff_strict
+    by (fastforce simp add: abs_mult field_simps)
 qed
 
 
diff -r 90381a0f5474 -r 57b9d993cc98 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Jul 05 23:21:28 2018 +0200
+++ b/src/HOL/Transcendental.thy	Thu Jul 05 23:37:17 2018 +0100
@@ -626,38 +626,41 @@
   fixes h :: "'a::field"
   assumes h: "h \<noteq> 0"
   shows "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
-    h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))"
+         h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))"
     (is "?lhs = ?rhs")
-  apply (subgoal_tac "h * ?lhs = h * ?rhs")
-   apply (simp add: h)
-  apply (simp add: right_diff_distrib diff_divide_distrib h)
-  apply (simp add: mult.assoc [symmetric])
-  apply (cases n)
-  apply simp
-  apply (simp add: diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
-      del: power_Suc sum_lessThan_Suc of_nat_Suc)
-  apply (subst lemma_realpow_rev_sumr)
-  apply (subst sumr_diff_mult_const2)
-  apply simp
-  apply (simp only: lemma_termdiff1 sum_distrib_left)
-  apply (rule sum.cong [OF refl])
-  apply (simp add: less_iff_Suc_add)
-  apply clarify
-  apply (simp add: sum_distrib_left diff_power_eq_sum ac_simps
-      del: sum_lessThan_Suc power_Suc)
-  apply (subst mult.assoc [symmetric], subst power_add [symmetric])
-  apply (simp add: ac_simps)
-  done
+proof (cases n)
+  case (Suc n)
+  have 0: "\<And>x k. (\<Sum>n<Suc k. h * (z ^ x * (z ^ (k - n) * (h + z) ^ n))) =
+                 (\<Sum>j<Suc k.  h * ((h + z) ^ j * z ^ (x + k - j)))"
+    apply (rule sum.cong [OF refl])
+    by (simp add: power_add [symmetric] mult.commute)
+  have *: "(\<Sum>i<n. z ^ i * ((z + h) ^ (n - i) - z ^ (n - i))) =
+           (\<Sum>i<n. \<Sum>j<n - i. h * ((z + h) ^ j * z ^ (n - Suc j)))"
+    apply (rule sum.cong [OF refl])
+    apply (clarsimp simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
+        simp del: sum_lessThan_Suc power_Suc)
+    done
+  have "h * ?lhs = h * ?rhs"
+    apply (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
+    using Suc
+    apply (simp add: diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
+        del: power_Suc sum_lessThan_Suc of_nat_Suc)
+    apply (subst lemma_realpow_rev_sumr)
+    apply (subst sumr_diff_mult_const2)
+    apply (simp add: lemma_termdiff1 sum_distrib_left *)
+    done
+  then show ?thesis
+    by (simp add: h)
+qed auto
+
 
 lemma real_sum_nat_ivl_bounded2:
   fixes K :: "'a::linordered_semidom"
   assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
     and K: "0 \<le> K"
   shows "sum f {..<n-k} \<le> of_nat n * K"
-  apply (rule order_trans [OF sum_mono])
-   apply (rule f)
-   apply simp
-  apply (simp add: mult_right_mono K)
+  apply (rule order_trans [OF sum_mono [OF f]])
+  apply (auto simp add: mult_right_mono K)
   done
 
 lemma lemma_termdiff3:
@@ -775,9 +778,8 @@
     also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
       (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
       apply (rule ext)
-      apply (simp add: diffs_def)
       apply (case_tac n)
-       apply (simp_all add: r_neq_0)
+      apply (simp_all add: diffs_def r_neq_0)
       done
     finally have "summable
       (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
@@ -874,12 +876,13 @@
     apply (auto simp: norm_divide norm_mult norm_power field_simps)
     done
   have "summable (\<lambda>n. (of_nat n * c n) * x ^ n)"
-    apply (rule summable_comparison_test' [of "\<lambda>n. norm(c n * (of_real r) ^ n)" N])
-     apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]])
-    using N r norm_of_real [of "r + K", where 'a = 'a]
-      apply (auto simp add: norm_divide norm_mult norm_power field_simps)
-    apply (fastforce simp: less_eq_real_def)
-    done
+  proof (rule summable_comparison_test')
+    show "summable (\<lambda>n. norm (c n * of_real r ^ n))"
+      apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]])
+      using N r norm_of_real [of "r + K", where 'a = 'a] by auto
+    show "\<And>n. N \<le> n \<Longrightarrow> norm (of_nat n * c n * x ^ n) \<le> norm (c n * of_real r ^ n)"
+      using N r by (fastforce simp add: norm_mult norm_power less_eq_real_def)
+  qed
   then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)"
     using summable_iff_shift [of "\<lambda>n. of_nat n * c n * x ^ n" 1]
     by simp
@@ -894,10 +897,7 @@
   fixes x :: "'a::{real_normed_field,banach}"
   assumes "\<And>x. summable (\<lambda>n. c n * x^n)"
   shows "summable (\<lambda>n. diffs c n * x^n)"
-  apply (rule termdiff_converges [where K = "1 + norm x"])
-  using assms
-   apply auto
-  done
+  by (rule termdiff_converges [where K = "1 + norm x"]) (use assms in auto)
 
 lemma termdiffs_strong:
   fixes K x :: "'a::{real_normed_field,banach}"
@@ -921,9 +921,9 @@
     by (blast intro: sm termdiff_converges powser_inside)
   ultimately show ?thesis
     apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
+    using K
       apply (auto simp: field_simps)
-    using K
-    apply (simp_all add: of_real_add [symmetric] del: of_real_add)
+    apply (simp flip: of_real_add)
     done
 qed