# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1554134563 -3600
# Node ID 095dce9892e8bba888d6794b774a40c928280be6
# Parent  571909ef3103a64344869cfbde4e93ffe94fea0e
A few results in Algebra, and bits for Analysis

diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Coset.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -1379,7 +1379,7 @@
   qed
 qed
 
-lemma (in group) normal_inter_subgroup:
+lemma (in group) normal_Int_subgroup:
   assumes "subgroup H G"
     and "N \<lhd> G"
   shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Algebra/Generated_Groups.thy
--- a/src/HOL/Algebra/Generated_Groups.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Generated_Groups.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -563,4 +563,13 @@
     by (simp add: int_pow_def2 pow_subgroup_generated)
 qed
 
+lemma kernel_from_subgroup_generated [simp]:
+  "subgroup S G \<Longrightarrow> kernel (subgroup_generated G S) H f = kernel G H f \<inter> S"
+  using subgroup.carrier_subgroup_generated_subgroup subgroup.subset
+  by (fastforce simp add: kernel_def set_eq_iff)
+
+lemma kernel_to_subgroup_generated [simp]:
+  "kernel G (subgroup_generated H S) f = kernel G H f"
+  by (simp add: kernel_def)
+
 end
\ No newline at end of file
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Group.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -425,7 +425,20 @@
 end
 
 lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"
-by(simp add: int_pow_def nat_pow_def)
+  by(simp add: int_pow_def nat_pow_def)
+
+lemma pow_nat:
+  assumes "i\<ge>0"
+  shows "x [^]\<^bsub>G\<^esub> nat i = x [^]\<^bsub>G\<^esub> i"
+proof (cases i rule: int_cases)
+  case (nonneg n)
+  then show ?thesis
+    by (simp add: int_pow_int)
+next
+  case (neg n)
+  then show ?thesis
+    using assms by linarith
+qed
 
 lemma int_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::int) = \<one>\<^bsub>G\<^esub>"
   by (simp add: int_pow_def)
@@ -450,6 +463,9 @@
   "x \<in> carrier G \<Longrightarrow> x [^] (-i::int) = inv (x [^] i)"
   by (simp add: int_pow_def2)
 
+lemma (in group) int_pow_neg_int: "x \<in> carrier G \<Longrightarrow> x [^] -(int n) = inv (x [^] n)"
+  by (simp add: int_pow_neg int_pow_int)
+
 lemma (in group) int_pow_mult:
   assumes "x \<in> carrier G" shows "x [^] (i + j::int) = x [^] i \<otimes> x [^] j"
 proof -
@@ -502,6 +518,38 @@
   by(simp add: inj_on_def)
 
 
+lemma (in monoid) group_commutes_pow:
+  fixes n::nat
+  shows "\<lbrakk>x \<otimes> y = y \<otimes> x; x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x [^] n \<otimes> y = y \<otimes> x [^] n"
+  apply (induction n, auto)
+  by (metis m_assoc nat_pow_closed)
+
+lemma (in monoid) pow_mult_distrib:
+  assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+  shows "(x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
+proof (induct n)
+  case (Suc n)
+  have "x \<otimes> (y [^] n \<otimes> y) = y [^] n \<otimes> x \<otimes> y"
+    by (simp add: eq group_commutes_pow m_assoc xy)
+  then show ?case
+    using assms Suc.hyps m_assoc by auto
+qed auto
+
+lemma (in group) int_pow_mult_distrib:
+  assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+  shows "(x \<otimes> y) [^] (i::int) = x [^] i \<otimes> y [^] i"
+proof (cases i rule: int_cases)
+  case (nonneg n)
+  then show ?thesis
+    by (metis eq int_pow_int pow_mult_distrib xy)
+next
+  case (neg n)
+  then show ?thesis
+    unfolding neg
+    apply (simp add: xy int_pow_neg_int del: of_nat_Suc)
+    by (metis eq inv_mult_group local.nat_pow_Suc nat_pow_closed pow_mult_distrib xy)
+qed
+
 subsection \<open>Submonoids\<close>
 
 locale submonoid = \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
@@ -852,7 +900,7 @@
 lemma id_iso: "id \<in> iso G G"
   by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
 
-corollary iso_refl : "G \<cong> G"
+corollary iso_refl [simp]: "G \<cong> G"
   using iso_set_refl unfolding is_iso_def by auto
 
 lemma trivial_hom:
@@ -901,11 +949,11 @@
 corollary (in group) iso_sym: "G \<cong> H \<Longrightarrow> H \<cong> G"
   using iso_set_sym unfolding is_iso_def by auto
 
-lemma (in group) iso_set_trans:
-  "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
-  by (auto simp add: iso_def hom_compose bij_betw_compose)
+lemma iso_set_trans:
+  "\<lbrakk>h \<in> Group.iso G H; i \<in> Group.iso H I\<rbrakk> \<Longrightarrow> i \<circ> h \<in> Group.iso G I"
+  by (force simp: iso_def hom_compose intro: bij_betw_trans)
 
-corollary (in group) iso_trans: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
+corollary iso_trans [trans]: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
   using iso_set_trans unfolding is_iso_def by blast
 
 lemma iso_same_card: "G \<cong> H \<Longrightarrow> card (carrier G) = card (carrier H)"
@@ -1081,6 +1129,8 @@
   fixes h
   assumes homh [simp]: "h \<in> hom G H"
 
+declare group_hom.homh [simp]
+
 lemma (in group_hom) hom_mult [simp]:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
 proof -
@@ -1170,14 +1220,21 @@
   using subgroup.subgroup_is_group[OF assms is_group]
         is_group subgroup.subset[OF assms] by auto
 
-lemma (in group_hom) nat_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
+lemma (in group_hom) hom_nat_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "x \<in> carrier G \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
   by (induction n) auto
 
-lemma (in group_hom) int_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
+lemma (in group_hom) hom_int_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "x \<in> carrier G \<Longrightarrow> h (x [^] (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
-  using nat_pow_hom by (simp add: int_pow_def2)
+  using hom_nat_pow by (simp add: int_pow_def2)
 
+lemma hom_nat_pow:
+  "\<lbrakk>h \<in> hom G H; x \<in> carrier G; group G; group H\<rbrakk> \<Longrightarrow> h (x [^]\<^bsub>G\<^esub> (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
+  by (simp add: group_hom.hom_nat_pow group_hom_axioms_def group_hom_def)
+
+lemma hom_int_pow:
+  "\<lbrakk>h \<in> hom G H; x \<in> carrier G; group G; group H\<rbrakk> \<Longrightarrow> h (x [^]\<^bsub>G\<^esub> (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
+  by (simp add: group_hom.hom_int_pow group_hom_axioms.intro group_hom_def)
 
 subsection \<open>Commutative Structures\<close>
 
@@ -1225,11 +1282,6 @@
   shows "comm_monoid G"
   by (rule comm_monoidI) (auto intro: m_assoc m_comm)
 
-lemma (in comm_monoid) nat_pow_distr:
-  "[| x \<in> carrier G; y \<in> carrier G |] ==>
-  (x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
-  by (induct n) (simp, simp add: m_ac)
-
 lemma (in comm_monoid) submonoid_is_comm_monoid :
   assumes "submonoid H G"
   shows "comm_monoid (G\<lparr>carrier := H\<rparr>)"
@@ -1279,6 +1331,17 @@
   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   by (simp add: m_ac inv_mult_group)
 
+lemma (in comm_monoid) nat_pow_distrib:
+  fixes n::nat
+  assumes "x \<in> carrier G" "y \<in> carrier G"
+  shows "(x \<otimes> y) [^] n = x [^] n \<otimes> y [^] n"
+  by (simp add: assms pow_mult_distrib m_comm)
+
+lemma (in comm_group) int_pow_distrib:
+  assumes "x \<in> carrier G" "y \<in> carrier G"
+  shows "(x \<otimes> y) [^] (i::int) = x [^] i \<otimes> y [^] i"
+  by (simp add: assms int_pow_mult_distrib m_comm)
+
 lemma (in comm_monoid) hom_imp_img_comm_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> hom G H"
   shows "comm_monoid (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)" (is "comm_monoid ?h_img")
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Algebra/Polynomials.thy
--- a/src/HOL/Algebra/Polynomials.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Polynomials.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -2190,7 +2190,7 @@
   have eq: "\<And>t. t \<in> set (dense_repr p) \<Longrightarrow> h [ fst t ] \<otimes>\<^bsub>A\<^esub> (h X [^]\<^bsub>A\<^esub> (snd t)) = (h \<circ> ?f) t"
     using ring_hom_memE(2)[OF ring_hom_ring.homh[OF assms(3)]
           const_in_carrier var_pow_closed[OF assms(1)]]
-          ring_hom_ring.nat_pow_hom[OF assms(3) var_closed(1)[OF assms(1)]] by auto
+          ring_hom_ring.hom_nat_pow[OF assms(3) var_closed(1)[OF assms(1)]] by auto
   show ?thesis
     using A.add.finprod_cong'[OF _ h eq] hp by simp
 qed
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -176,7 +176,7 @@
     using assms by (auto simp: intro: homeq_imp_rcos rcos_imp_homeq a_elemrcos_carrier)
 qed
 
-lemma (in ring_hom_ring) nat_pow_hom:
+lemma (in ring_hom_ring) hom_nat_pow:
   "x \<in> carrier R \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>S\<^esub> n"
   by (induct n) (auto)
 
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Algebra/Zassenhaus.thy
--- a/src/HOL/Algebra/Zassenhaus.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Zassenhaus.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -203,7 +203,7 @@
   hence N_incl : "N \<subseteq> N <#> H"
     by (metis assms(1) normal_imp_subgroup coset_mult_one subgroup_def)
   thus "normal N (G\<lparr>carrier := N <#> H\<rparr>)"
-    using normal_inter_subgroup[OF mult_norm_subgroup[OF assms] assms(1)]
+    using normal_Int_subgroup[OF mult_norm_subgroup[OF assms] assms(1)]
     by (simp add : inf_absorb1)
 qed
 
@@ -308,7 +308,7 @@
     ultimately have "(G\<lparr>carrier := H\<rparr> Mod N \<inter> H) \<cong> (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
       using group_hom.FactGroup_iso[OF homomorphism im_f] by auto
     hence "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H"
-      by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_inter_subgroup)
+      by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_Int_subgroup)
     thus "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
 qed
 
@@ -636,8 +636,7 @@
   qed
   hence  "Gmod3  = Gmod4" using Hp Gmod4_def by simp
   hence "Gmod1 \<cong> Gmod2"
-    using group.iso_sym group.iso_trans Hyp normal.factorgroup_is_group
-    by (metis assms Gmod1_def Gmod2_def preliminary2)
+    by (metis assms group.iso_sym iso_trans Hyp normal.factorgroup_is_group Gmod2_def preliminary2)
   thus ?thesis using Gmod1_def Gmod2_def by (simp add: inf_commute)
 qed
 
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Analysis/Abstract_Euclidean_Space.thy
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -81,13 +81,13 @@
    "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
     \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i + g x i)"
   unfolding Euclidean_space_def continuous_map_in_subtopology
-  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_real_add)
+  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_add)
 
 lemma continuous_map_Euclidean_space_diff [continuous_intros]:
    "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
     \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i - g x i)"
   unfolding Euclidean_space_def continuous_map_in_subtopology
-  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_real_diff)
+  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff)
 
 lemma homeomorphic_Euclidean_space_product_topology:
   "Euclidean_space n homeomorphic_space product_topology (\<lambda>i. euclideanreal) {..<n}"
@@ -158,12 +158,11 @@
 lemma continuous_map_nsphere_reflection:
   "continuous_map (nsphere n) (nsphere n) (\<lambda>x i. if i = k then -x i else x i)"
 proof -
-  have cm: "continuous_map (powertop_real UNIV)
-           euclideanreal (\<lambda>x. if j = k then - x j else x j)" for j
+  have cm: "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. if j = k then - x j else x j)" for j
   proof (cases "j=k")
     case True
     then show ?thesis
-      by simp (metis UNIV_I continuous_map_product_projection continuous_map_real_minus)
+      by simp (metis UNIV_I continuous_map_product_projection)
   next
     case False
     then show ?thesis
@@ -173,7 +172,7 @@
     by simp
   show ?thesis
     apply (simp add: nsphere continuous_map_in_subtopology continuous_map_componentwise_UNIV
-        continuous_map_from_subtopology  cm topspace_subtopology)
+                     continuous_map_from_subtopology cm)
     apply (intro conjI allI impI continuous_intros continuous_map_from_subtopology continuous_map_product_projection)
       apply (auto simp: power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] eq cong: if_cong)
     done
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Analysis/Abstract_Limits.thy
--- a/src/HOL/Analysis/Abstract_Limits.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Limits.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -47,7 +47,7 @@
 definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
   "limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
 
-lemma limitin_euclideanreal_iff [simp]: "limitin euclideanreal f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
+lemma limitin_canonical_iff [simp]: "limitin euclidean f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
   by (auto simp: limitin_def tendsto_def)
 
 lemma limitin_topspace: "limitin X f l F \<Longrightarrow> l \<in> topspace X"
@@ -203,8 +203,8 @@
 
 subsection\<open>Combining theorems for continuous functions into the reals\<close>
 
-lemma continuous_map_real_const [simp,continuous_intros]:
-   "continuous_map X euclideanreal (\<lambda>x. c)"
+lemma continuous_map_canonical_const [continuous_intros]:
+   "continuous_map X euclidean (\<lambda>x. c)"
   by simp
 
 lemma continuous_map_real_mult [continuous_intros]:
@@ -240,24 +240,31 @@
    "continuous_map X euclideanreal (\<lambda>x. f x * c) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
   by (simp add: mult.commute flip: continuous_map_real_mult_left_eq)
 
-lemma continuous_map_real_minus [continuous_intros]:
-   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. - f x)"
+lemma continuous_map_minus [continuous_intros]:
+  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+  shows "continuous_map X euclidean f \<Longrightarrow> continuous_map X euclidean (\<lambda>x. - f x)"
   by (simp add: continuous_map_atin tendsto_minus)
 
-lemma continuous_map_real_minus_eq:
-   "continuous_map X euclideanreal (\<lambda>x. - f x) \<longleftrightarrow> continuous_map X euclideanreal f"
-  using continuous_map_real_mult_left_eq [where c = "-1"] by auto
+lemma continuous_map_minus_eq [simp]:
+  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+  shows "continuous_map X euclidean (\<lambda>x. - f x) \<longleftrightarrow> continuous_map X euclidean f"
+  using continuous_map_minus add.inverse_inverse continuous_map_eq by fastforce
 
-lemma continuous_map_real_add [continuous_intros]:
-   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
-   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x + g x)"
+lemma continuous_map_add [continuous_intros]:
+  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+  shows "\<lbrakk>continuous_map X euclidean f; continuous_map X euclidean g\<rbrakk> \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x + g x)"
   by (simp add: continuous_map_atin tendsto_add)
 
-lemma continuous_map_real_diff [continuous_intros]:
-   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
-   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x - g x)"
+lemma continuous_map_diff [continuous_intros]:
+  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+  shows "\<lbrakk>continuous_map X euclidean f; continuous_map X euclidean g\<rbrakk> \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x - g x)"
   by (simp add: continuous_map_atin tendsto_diff)
 
+lemma continuous_map_norm [continuous_intros]:
+  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
+  shows "continuous_map X euclidean f \<Longrightarrow> continuous_map X euclidean (\<lambda>x. norm(f x))"
+  by (simp add: continuous_map_atin tendsto_norm)
+
 lemma continuous_map_real_abs [continuous_intros]:
    "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. abs(f x))"
   by (simp add: continuous_map_atin tendsto_rabs)
@@ -273,8 +280,9 @@
   by (simp add: continuous_map_atin tendsto_min)
 
 lemma continuous_map_sum [continuous_intros]:
-   "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
-        \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sum (f x) I)"
+  fixes f :: "'a\<Rightarrow>'b\<Rightarrow>'c::real_normed_vector"
+  shows "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x i)\<rbrakk>
+         \<Longrightarrow> continuous_map X euclidean (\<lambda>x. sum (f x) I)"
   by (simp add: continuous_map_atin tendsto_sum)
 
 lemma continuous_map_prod [continuous_intros]:
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -608,7 +608,7 @@
   using continuous_map_product_coordinates [of _ UNIV "\<lambda>i. euclidean"]
     by (metis (no_types) continuous_map_iff_continuous euclidean_product_topology iso_tuple_UNIV_I subtopology_UNIV)
 
-lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
+lemma continuous_on_coordinatewise_then_product [continuous_intros]:
   fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
   assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
   shows "continuous_on S f"
@@ -635,7 +635,7 @@
 lemma continuous_on_coordinatewise_iff:
   fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
   shows "continuous_on (A \<inter> S) f \<longleftrightarrow> (\<forall>i. continuous_on (A \<inter> S) (\<lambda>x. f x i))"
-  by (auto simp: continuous_on_product_then_coordinatewise)
+  by (auto simp: continuous_on_product_then_coordinatewise continuous_on_coordinatewise_then_product)
 
 subsubsection%important \<open>Topological countability for product spaces\<close>
 
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -411,7 +411,7 @@
    "\<lbrakk>Hausdorff_space X; finite S\<rbrakk> \<Longrightarrow> closedin X S \<longleftrightarrow> S \<subseteq> topspace X"
   by (meson closedin_Hausdorff_finite closedin_def)
 
-lemma derived_set_of_infinite_open_in:
+lemma derived_set_of_infinite_openin:
    "Hausdorff_space X
         \<Longrightarrow> X derived_set_of S =
             {x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)}"
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -879,7 +879,7 @@
   "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
   unfolding is_interval_def by auto
 
-lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
+lemma is_interval_Int: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
   unfolding is_interval_def
   by blast
 
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -319,12 +319,12 @@
     proof (cases "even k")
       case True
       with * \<open>in_carrier ls\<close> show ?thesis
-        by (simp add: even_pow sqr_ci nat_pow_distr nat_pow_mult
+        by (simp add: even_pow sqr_ci nat_pow_distrib nat_pow_mult
           mult_2 [symmetric] even_two_times_div_two)
     next
       case False
       with * \<open>in_carrier ls\<close> show ?thesis
-        by (simp add: odd_pow mul_ci sqr_ci nat_pow_distr nat_pow_mult
+        by (simp add: odd_pow mul_ci sqr_ci nat_pow_distrib nat_pow_mult
           mult_2 [symmetric] trans [OF nat_pow_Suc m_comm, symmetric])
     qed
   qed
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -159,7 +159,7 @@
   proof (cases x y rule: pexpr_cases2)
     case (PPow_PPow e n e' m)
     then show ?thesis
-      by (simp del: npemul.simps add: 1 npepow_correct nat_pow_distr
+      by (simp del: npemul.simps add: 1 npepow_correct nat_pow_distrib
           npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"])
   qed simp_all
 qed
@@ -258,7 +258,7 @@
   by (induct e n e' m arbitrary: p e'' rule: isin.induct)
     (force
        simp add:
-         nat_pow_distr nat_pow_pow nat_pow_mult m_ac
+         nat_pow_distrib nat_pow_pow nat_pow_mult m_ac
          npemul_correct npepow_correct
        split: option.split_asm prod.split_asm if_split_asm)+
 
@@ -323,7 +323,7 @@
     peval xs (PExpr2 (PMul (snd (snd (split_aux e\<^sub>1 n e\<^sub>2))) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
   by (induct e\<^sub>1 n e\<^sub>2 rule: split_aux_induct)
     (auto simp add: split_beta
-       nat_pow_distr nat_pow_pow nat_pow_mult m_ac
+       nat_pow_distrib nat_pow_pow nat_pow_mult m_ac
        npemul_correct npepow_correct isin_correct'
        split: option.split)
 
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -2045,24 +2045,49 @@
   for f :: "'a \<Rightarrow> 'a"
   by (fastforce simp:surj_def dest!: endo_inj_surj)
 
-corollary infinite_UNIV_nat [iff]: "\<not> finite (UNIV :: nat set)"
-proof
-  assume "finite (UNIV :: nat set)"
-  with finite_UNIV_inj_surj [of Suc] show False
-    by simp (blast dest: Suc_neq_Zero surjD)
-qed
-
-lemma infinite_UNIV_char_0: "\<not> finite (UNIV :: 'a::semiring_char_0 set)"
+lemma surjective_iff_injective_gen:
+  assumes fS: "finite S"
+    and fT: "finite T"
+    and c: "card S = card T"
+    and ST: "f ` S \<subseteq> T"
+  shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S"
+  (is "?lhs \<longleftrightarrow> ?rhs")
 proof
-  assume "finite (UNIV :: 'a set)"
-  with subset_UNIV have "finite (range of_nat :: 'a set)"
-    by (rule finite_subset)
-  moreover have "inj (of_nat :: nat \<Rightarrow> 'a)"
-    by (simp add: inj_on_def)
-  ultimately have "finite (UNIV :: nat set)"
-    by (rule finite_imageD)
-  then show False
-    by simp
+  assume h: "?lhs"
+  {
+    fix x y
+    assume x: "x \<in> S"
+    assume y: "y \<in> S"
+    assume f: "f x = f y"
+    from x fS have S0: "card S \<noteq> 0"
+      by auto
+    have "x = y"
+    proof (rule ccontr)
+      assume xy: "\<not> ?thesis"
+      have th: "card S \<le> card (f ` (S - {y}))"
+        unfolding c
+      proof (rule card_mono)
+        show "finite (f ` (S - {y}))"
+          by (simp add: fS)
+        have "\<lbrakk>x \<noteq> y; x \<in> S; z \<in> S; f x = f y\<rbrakk>
+         \<Longrightarrow> \<exists>x \<in> S. x \<noteq> y \<and> f z = f x" for z
+          by (case_tac "z = y \<longrightarrow> z = x") auto
+        then show "T \<subseteq> f ` (S - {y})"
+          using h xy x y f by fastforce
+      qed
+      also have " \<dots> \<le> card (S - {y})"
+        by (simp add: card_image_le fS)
+      also have "\<dots> \<le> card S - 1" using y fS by simp
+      finally show False using S0 by arith
+    qed
+  }
+  then show ?rhs
+    unfolding inj_on_def by blast
+next
+  assume h: ?rhs
+  have "f ` S = T"
+    by (simp add: ST c card_image card_subset_eq fT h)
+  then show ?lhs by blast
 qed
 
 hide_const (open) Finite_Set.fold
@@ -2084,6 +2109,26 @@
   infinite set, the result is still infinite.
 \<close>
 
+lemma infinite_UNIV_nat [iff]: "infinite (UNIV :: nat set)"
+proof
+  assume "finite (UNIV :: nat set)"
+  with finite_UNIV_inj_surj [of Suc] show False
+    by simp (blast dest: Suc_neq_Zero surjD)
+qed
+
+lemma infinite_UNIV_char_0: "infinite (UNIV :: 'a::semiring_char_0 set)"
+proof
+  assume "finite (UNIV :: 'a set)"
+  with subset_UNIV have "finite (range of_nat :: 'a set)"
+    by (rule finite_subset)
+  moreover have "inj (of_nat :: nat \<Rightarrow> 'a)"
+    by (simp add: inj_on_def)
+  ultimately have "finite (UNIV :: nat set)"
+    by (rule finite_imageD)
+  then show False
+    by simp
+qed
+
 lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
   by auto
 
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -148,6 +148,10 @@
     by simp
 qed
 
+lemma linear_scale_real:
+  fixes r::real shows "linear f \<Longrightarrow> f (r * b) = r * f b"
+  using linear_scale by fastforce
+
 interpretation scaleR_left: additive "(\<lambda>a. scaleR a x :: 'a::real_vector)"
   by standard (rule scaleR_left_distrib)
 
diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Vector_Spaces.thy
--- a/src/HOL/Vector_Spaces.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Vector_Spaces.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -993,48 +993,6 @@
 
 end
 
-lemma surjective_iff_injective_gen:
-  assumes fS: "finite S"
-    and fT: "finite T"
-    and c: "card S = card T"
-    and ST: "f ` S \<subseteq> T"
-  shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume h: "?lhs"
-  {
-    fix x y
-    assume x: "x \<in> S"
-    assume y: "y \<in> S"
-    assume f: "f x = f y"
-    from x fS have S0: "card S \<noteq> 0"
-      by auto
-    have "x = y"
-    proof (rule ccontr)
-      assume xy: "\<not> ?thesis"
-      have th: "card S \<le> card (f ` (S - {y}))"
-        unfolding c
-      proof (rule card_mono)
-        show "finite (f ` (S - {y}))"
-          by (simp add: fS)
-        show "T \<subseteq> f ` (S - {y})"
-          using h xy x y f unfolding subset_eq image_iff
-          by (metis member_remove remove_def)
-      qed
-      also have " \<dots> \<le> card (S - {y})"
-        by (simp add: card_image_le fS)
-      also have "\<dots> \<le> card S - 1" using y fS by simp
-      finally show False using S0 by arith
-    qed
-  }
-  then show ?rhs
-    unfolding inj_on_def by blast
-next
-  assume h: ?rhs
-  have "f ` S = T"
-    by (simp add: ST c card_image card_subset_eq fT h)
-  then show ?lhs by blast
-qed
 
 locale finite_dimensional_vector_space = vector_space +
   fixes Basis :: "'b set"