# HG changeset patch
# User wenzelm
# Date 1552256583 -3600
# Node ID 6b03a8cf092ded842282e85af71a8c6f37383d6d
# Parent  2eade8651b93e43dc19711596e037206c91ef49d
more formal contributors (with the help of the history);

diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/Congruence.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -270,9 +270,7 @@
   using assms by (meson closure_of_memE elemE)
 
 
-(* Lemmas by Paulo Emílio de Vilhena *)
-
-lemma (in partition) equivalence_from_partition:
+lemma (in partition) equivalence_from_partition: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "equivalence \<lparr> carrier = A, eq = (\<lambda>x y. y \<in> (THE b. b \<in> B \<and> x \<in> b))\<rparr>"
     unfolding partition_def equivalence_def
 proof (auto)
@@ -285,10 +283,10 @@
     using unique_class by (metis (mono_tags, lifting) the_equality)
 qed
 
-lemma (in partition) partition_coverture: "\<Union>B = A"
+lemma (in partition) partition_coverture: "\<Union>B = A" \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   by (meson Sup_le_iff UnionI unique_class incl subsetI subset_antisym)
 
-lemma (in partition) disjoint_union:
+lemma (in partition) disjoint_union: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "b1 \<in> B" "b2 \<in> B"
     and "b1 \<inter> b2 \<noteq> {}"
   shows "b1 = b2"
@@ -299,7 +297,7 @@
   thus False using unique_class \<open>b1 \<noteq> b2\<close> assms(1) assms(2) by blast
 qed
 
-lemma partitionI:
+lemma partitionI: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   fixes A :: "'a set" and B :: "('a set) set"
   assumes "\<Union>B = A"
     and "\<And>b1 b2. \<lbrakk> b1 \<in> B; b2 \<in> B \<rbrakk> \<Longrightarrow> b1 \<inter> b2 \<noteq> {} \<Longrightarrow> b1 = b2"
@@ -316,7 +314,7 @@
   show "\<And>b. b \<in> B \<Longrightarrow> b \<subseteq> A" using assms(1) by blast
 qed
 
-lemma (in partition) remove_elem:
+lemma (in partition) remove_elem: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "b \<in> B"
   shows "partition (A - b) (B - {b})"
 proof
@@ -327,7 +325,7 @@
     using assms unique_class incl partition_axioms partition_coverture by fastforce
 qed
 
-lemma disjoint_sum:
+lemma disjoint_sum: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "\<lbrakk> finite B; finite A; partition A B\<rbrakk> \<Longrightarrow> (\<Sum>b\<in>B. \<Sum>a\<in>b. f a) = (\<Sum>a\<in>A. f a)"
 proof (induct arbitrary: A set: finite)
   case empty thus ?case using partition.unique_class by fastforce
@@ -343,7 +341,7 @@
     by (metis add.commute insert_iff partition.incl sum.subset_diff)
 qed
 
-lemma (in partition) disjoint_sum:
+lemma (in partition) disjoint_sum: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "finite A"
   shows "(\<Sum>b\<in>B. \<Sum>a\<in>b. f a) = (\<Sum>a\<in>A. f a)"
 proof -
@@ -352,20 +350,20 @@
   thus ?thesis using disjoint_sum assms partition_axioms by blast
 qed
 
-lemma (in equivalence) set_eq_insert_aux:
+lemma (in equivalence) set_eq_insert_aux: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "A \<subseteq> carrier S"
     and "x \<in> carrier S" "x' \<in> carrier S" "x .= x'"
     and "y \<in> insert x A"
   shows "y .\<in> insert x' A"
   by (metis assms(1) assms(4) assms(5) contra_subsetD elemI elem_exact insert_iff)
 
-corollary (in equivalence) set_eq_insert:
+corollary (in equivalence) set_eq_insert: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "A \<subseteq> carrier S"
     and "x \<in> carrier S" "x' \<in> carrier S" "x .= x'"
   shows "insert x A {.=} insert x' A"
   by (meson set_eqI assms set_eq_insert_aux sym equivalence_axioms)
 
-lemma (in equivalence) set_eq_pairI:
+lemma (in equivalence) set_eq_pairI: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes xx': "x .= x'"
     and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S"
   shows "{x, y} {.=} {x', y}"
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/Coset.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -41,21 +41,17 @@
 lemma (in comm_group) subgroup_imp_normal: "subgroup A G \<Longrightarrow> A \<lhd> G"
   by (simp add: normal_def normal_axioms_def is_group l_coset_def r_coset_def m_comm subgroup.mem_carrier)
 
-(*Next two lemmas contributed by Martin Baillon.*)
-
-lemma l_coset_eq_set_mult:
+lemma l_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   fixes G (structure)
   shows "x <# H = {x} <#> H"
   unfolding l_coset_def set_mult_def by simp
 
-lemma r_coset_eq_set_mult:
+lemma r_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   fixes G (structure)
   shows "H #> x = H <#> {x}"
   unfolding r_coset_def set_mult_def by simp
 
-(* Next five lemmas contributed by Paulo Emílio de Vilhena.                    *)
-
-lemma (in subgroup) rcosets_non_empty:
+lemma (in subgroup) rcosets_non_empty: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "R \<in> rcosets H"
   shows "R \<noteq> {}"
 proof -
@@ -66,7 +62,7 @@
   thus ?thesis by blast
 qed
 
-lemma (in group) diff_neutralizes:
+lemma (in group) diff_neutralizes: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "subgroup H G" "R \<in> rcosets H"
   shows "\<And>r1 r2. \<lbrakk> r1 \<in> R; r2 \<in> R \<rbrakk> \<Longrightarrow> r1 \<otimes> (inv r2) \<in> H"
 proof -
@@ -94,24 +90,25 @@
   thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def)
 qed
 
-lemma mono_set_mult: "\<lbrakk> H \<subseteq> H'; K \<subseteq> K' \<rbrakk> \<Longrightarrow> H <#>\<^bsub>G\<^esub> K \<subseteq> H' <#>\<^bsub>G\<^esub> K'"
+lemma mono_set_mult: "\<lbrakk> H \<subseteq> H'; K \<subseteq> K' \<rbrakk> \<Longrightarrow> H <#>\<^bsub>G\<^esub> K \<subseteq> H' <#>\<^bsub>G\<^esub> K'" \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   unfolding set_mult_def by (simp add: UN_mono)
 
 
 subsection \<open>Stable Operations for Subgroups\<close>
 
-lemma set_mult_consistent [simp]:
+lemma set_mult_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K"
   unfolding set_mult_def by simp
 
-lemma r_coset_consistent [simp]:
+lemma r_coset_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #>\<^bsub>G\<^esub> h"
   unfolding r_coset_def by simp
 
-lemma l_coset_consistent [simp]:
+lemma l_coset_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <#\<^bsub>G\<^esub> I"
   unfolding l_coset_def by simp
 
+
 subsection \<open>Basic Properties of set multiplication\<close>
 
 lemma (in group) setmult_subset_G:
@@ -124,8 +121,7 @@
   shows "H <#> K \<subseteq> carrier G"
   using assms by (auto simp add: set_mult_def subsetD)
 
-(* Next lemma contributed by Martin Baillon.*)
-lemma (in group) set_mult_assoc:
+lemma (in group) set_mult_assoc: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "M \<subseteq> carrier G" "H \<subseteq> carrier G" "K \<subseteq> carrier G"
   shows "(M <#> H) <#> K = M <#> (H <#> K)"
 proof
@@ -1094,13 +1090,11 @@
   using FactGroup_iso_set unfolding is_iso_def by auto
 
 
-(* Next two lemmas contributed by Paulo Emílio de Vilhena. *)
-
-lemma (in group_hom) trivial_hom_iff:
+lemma (in group_hom) trivial_hom_iff: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "h ` (carrier G) = { \<one>\<^bsub>H\<^esub> } \<longleftrightarrow> kernel G H h = carrier G"
   unfolding kernel_def using one_closed by force
 
-lemma (in group_hom) trivial_ker_imp_inj:
+lemma (in group_hom) trivial_ker_imp_inj: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "kernel G H h = { \<one> }"
   shows "inj_on h (carrier G)"
 proof (rule inj_onI)
@@ -1197,11 +1191,9 @@
 qed
 
 
-(* Next subsection contributed by Martin Baillon. *)
-
 subsection \<open>Theorems about Factor Groups and Direct product\<close>
 
-lemma (in group) DirProd_normal :
+lemma (in group) DirProd_normal : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "group K"
     and "H \<lhd> G"
     and "N \<lhd> K"
@@ -1231,7 +1223,7 @@
   qed
 qed
 
-lemma (in group) FactGroup_DirProd_multiplication_iso_set :
+lemma (in group) FactGroup_DirProd_multiplication_iso_set : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "group K"
     and "H \<lhd> G"
     and "N \<lhd> K"
@@ -1261,14 +1253,14 @@
     unfolding iso_def hom_def bij_betw_def inj_on_def by simp
 qed
 
-corollary (in group) FactGroup_DirProd_multiplication_iso_1 :
+corollary (in group) FactGroup_DirProd_multiplication_iso_1 : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "group K"
     and "H \<lhd> G"
     and "N \<lhd> K"
   shows "  ((G Mod H) \<times>\<times> (K Mod N)) \<cong> (G \<times>\<times> K Mod H \<times> N)"
   unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto
 
-corollary (in group) FactGroup_DirProd_multiplication_iso_2 :
+corollary (in group) FactGroup_DirProd_multiplication_iso_2 : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "group K"
     and "H \<lhd> G"
     and "N \<lhd> K"
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -755,8 +755,7 @@
   using assms
   by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)
 
-(*by Paulo Emílio de Vilhena*)
-lemma (in comm_monoid_cancel) prime_irreducible:
+lemma (in comm_monoid_cancel) prime_irreducible: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "prime G p"
   shows "irreducible G p"
 proof (rule irreducibleI)
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -517,9 +517,7 @@
     using finprod_Suc[of f k] assms atMost_Suc lessThan_Suc_atMost by simp
 qed
 
-(* The following two were contributed by Jeremy Avigad. *)
-
-lemma finprod_reindex:
+lemma finprod_reindex: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close>
   "f \<in> (h ` A) \<rightarrow> carrier G \<Longrightarrow>
         inj_on h A \<Longrightarrow> finprod G f (h ` A) = finprod G (\<lambda>x. f (h x)) A"
 proof (induct A rule: infinite_finite_induct)
@@ -529,7 +527,7 @@
   with \<open>\<not> finite A\<close> show ?case by simp
 qed (auto simp add: Pi_def)
 
-lemma finprod_const:
+lemma finprod_const: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close>
   assumes a [simp]: "a \<in> carrier G"
     shows "finprod G (\<lambda>x. a) A = a [^] card A"
 proof (induct A rule: infinite_finite_induct)
@@ -541,9 +539,7 @@
   qed auto
 qed auto
 
-(* The following lemma was contributed by Jesus Aransay. *)
-
-lemma finprod_singleton:
+lemma finprod_singleton: \<^marker>\<open>contributor \<open>Jesus Aransay\<close>\<close>
   assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
   shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i"
   using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/Group.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -501,23 +501,23 @@
 lemma (in group) inj_on_cmult: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. c \<otimes> x) (carrier G)"
   by(simp add: inj_on_def)
 
-(*Following subsection contributed by Martin Baillon*)
+
 subsection \<open>Submonoids\<close>
 
-locale submonoid =
+locale submonoid = \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   fixes H and G (structure)
   assumes subset: "H \<subseteq> carrier G"
     and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
     and one_closed [simp]: "\<one> \<in> H"
 
-lemma (in submonoid) is_submonoid:
+lemma (in submonoid) is_submonoid: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   "submonoid H G" by (rule submonoid_axioms)
 
-lemma (in submonoid) mem_carrier [simp]:
+lemma (in submonoid) mem_carrier [simp]: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   "x \<in> H \<Longrightarrow> x \<in> carrier G"
   using subset by blast
 
-lemma (in submonoid) submonoid_is_monoid [intro]:
+lemma (in submonoid) submonoid_is_monoid [intro]: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "monoid G"
   shows "monoid (G\<lparr>carrier := H\<rparr>)"
 proof -
@@ -526,11 +526,11 @@
     by (simp add: monoid_def m_assoc)
 qed
 
-lemma submonoid_nonempty:
+lemma submonoid_nonempty: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   "~ submonoid {} G"
   by (blast dest: submonoid.one_closed)
 
-lemma (in submonoid) finite_monoid_imp_card_positive:
+lemma (in submonoid) finite_monoid_imp_card_positive: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   "finite (carrier G) ==> 0 < card H"
 proof (rule classical)
   assume "finite (carrier G)" and a: "~ 0 < card H"
@@ -540,7 +540,7 @@
 qed
 
 
-lemma (in monoid) monoid_incl_imp_submonoid :
+lemma (in monoid) monoid_incl_imp_submonoid : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "H \<subseteq> carrier G"
 and "monoid (G\<lparr>carrier := H\<rparr>)"
 shows "submonoid H G"
@@ -552,7 +552,7 @@
   show "\<one> \<in> H " using monoid.one_closed[OF assms(2)] assms by simp
 qed
 
-lemma (in monoid) inv_unique':
+lemma (in monoid) inv_unique': \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "x \<in> carrier G" "y \<in> carrier G"
   shows "\<lbrakk> x \<otimes> y = \<one>; y \<otimes> x = \<one> \<rbrakk> \<Longrightarrow> y = inv x"
 proof -
@@ -563,7 +563,7 @@
     using inv_unique[OF l_inv Units_r_inv[OF unit] assms Units_inv_closed[OF unit]] .
 qed
 
-lemma (in monoid) m_inv_monoid_consistent: (* contributed by Paulo *)
+lemma (in monoid) m_inv_monoid_consistent: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "x \<in> Units (G \<lparr> carrier := H \<rparr>)" and "submonoid H G"
   shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
 proof -
@@ -620,7 +620,7 @@
   shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
   using assms m_inv_monoid_consistent[OF _ subgroup_is_submonoid] subgroup_Units[of H] by auto
 
-lemma (in group) int_pow_consistent: (* by Paulo *)
+lemma (in group) int_pow_consistent: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "subgroup H G" "x \<in> H"
   shows "x [^] (n :: int) = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
 proof (cases)
@@ -687,19 +687,17 @@
 lemma (in subgroup) finite_imp_card_positive: "finite (carrier G) \<Longrightarrow> 0 < card H"
   using subset one_closed card_gt_0_iff finite_subset by blast
 
-(*Following 3 lemmas contributed by Martin Baillon*)
-
-lemma (in subgroup) subgroup_is_submonoid :
+lemma (in subgroup) subgroup_is_submonoid : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   "submonoid H G"
   by (simp add: submonoid.intro subset)
 
-lemma (in group) submonoid_subgroupI :
+lemma (in group) submonoid_subgroupI : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "submonoid H G"
     and "\<And>a. a \<in> H \<Longrightarrow> inv a \<in> H"
   shows "subgroup H G"
   by (metis assms subgroup_def submonoid_def)
 
-lemma (in group) group_incl_imp_subgroup:
+lemma (in group) group_incl_imp_subgroup: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "H \<subseteq> carrier G"
     and "group (G\<lparr>carrier := H\<rparr>)"
   shows "subgroup H G"
@@ -914,9 +912,7 @@
   using bij_betw_same_card  unfolding is_iso_def iso_def by auto
 
 
-(* Next four lemmas contributed by Paulo. *)
-
-lemma (in monoid) hom_imp_img_monoid:
+lemma (in monoid) hom_imp_img_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> hom G H"
   shows "monoid (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)" (is "monoid ?h_img")
 proof (rule monoidI)
@@ -953,7 +949,7 @@
   finally show "(x \<otimes>\<^bsub>(?h_img)\<^esub> y) \<otimes>\<^bsub>(?h_img)\<^esub> z = x \<otimes>\<^bsub>(?h_img)\<^esub> (y \<otimes>\<^bsub>(?h_img)\<^esub> z)" .
 qed
 
-lemma (in group) hom_imp_img_group:
+lemma (in group) hom_imp_img_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> hom G H"
   shows "group (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)" (is "group ?h_img")
 proof -
@@ -977,7 +973,7 @@
   qed
 qed
 
-lemma (in group) iso_imp_group:
+lemma (in group) iso_imp_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "G \<cong> H" and "monoid H"
   shows "group H"
 proof -
@@ -1027,7 +1023,7 @@
   thus ?thesis unfolding group_def group_axioms_def using assms(2) by simp
 qed
 
-corollary (in group) iso_imp_img_group:
+corollary (in group) iso_imp_img_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> iso G H"
   shows "group (H \<lparr> one := h \<one> \<rparr>)"
 proof -
@@ -1131,20 +1127,17 @@
   with assms show ?thesis by (simp del: H.r_inv H.Units_r_inv)
 qed
 
-(* Contributed by Joachim Breitner *)
-lemma (in group) int_pow_is_hom:
+lemma (in group) int_pow_is_hom: \<^marker>\<open>contributor \<open>Joachim Breitner\<close>\<close>
   "x \<in> carrier G \<Longrightarrow> (([^]) x) \<in> hom \<lparr> carrier = UNIV, mult = (+), one = 0::int \<rparr> G "
   unfolding hom_def by (simp add: int_pow_mult)
 
-(* Next six lemmas contributed by Paulo. *)
-
-lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H"
+lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H" \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   apply (rule subgroupI)
   apply (auto simp add: image_subsetI)
   apply (metis G.inv_closed hom_inv image_iff)
   by (metis G.monoid_axioms hom_mult image_eqI monoid.m_closed)
 
-lemma (in group_hom) subgroup_img_is_subgroup:
+lemma (in group_hom) subgroup_img_is_subgroup: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "subgroup I G"
   shows "subgroup (h ` I) H"
 proof -
@@ -1158,7 +1151,7 @@
     using group_hom.img_is_subgroup[of "G \<lparr> carrier := I \<rparr>" H h] by simp
 qed
 
-lemma (in group_hom) induced_group_hom:
+lemma (in group_hom) induced_group_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "subgroup I G"
   shows "group_hom (G \<lparr> carrier := I \<rparr>) (H \<lparr> carrier := h ` I \<rparr>) h"
 proof -
@@ -1170,18 +1163,18 @@
           subgroup.subgroup_is_group[OF subgroup_img_is_subgroup[OF assms] is_group] by simp
 qed
 
-lemma (in group) canonical_inj_is_hom:
+lemma (in group) canonical_inj_is_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "subgroup H G"
   shows "group_hom (G \<lparr> carrier := H \<rparr>) G id"
   unfolding group_hom_def group_hom_axioms_def hom_def
   using subgroup.subgroup_is_group[OF assms is_group]
         is_group subgroup.subset[OF assms] by auto
 
-lemma (in group_hom) nat_pow_hom:
+lemma (in group_hom) nat_pow_hom: \<^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:
+lemma (in group_hom) int_pow_hom: \<^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)
 
@@ -1286,9 +1279,7 @@
   "[| 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)
 
-(* Next three lemmas contributed by Paulo. *)
-
-lemma (in comm_monoid) hom_imp_img_comm_monoid:
+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")
 proof (rule monoid.monoid_comm_monoidI)
@@ -1309,13 +1300,13 @@
   finally show "x \<otimes>\<^bsub>(?h_img)\<^esub> y = y \<otimes>\<^bsub>(?h_img)\<^esub> x" .
 qed
 
-lemma (in comm_group) hom_imp_img_comm_group:
+lemma (in comm_group) hom_imp_img_comm_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> hom G H"
   shows "comm_group (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
   unfolding comm_group_def
   using hom_imp_img_group[OF assms] hom_imp_img_comm_monoid[OF assms] by simp
 
-lemma (in comm_group) iso_imp_img_comm_group:
+lemma (in comm_group) iso_imp_img_comm_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> iso G H"
   shows "comm_group (H \<lparr> one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
 proof -
@@ -1329,7 +1320,7 @@
   ultimately show ?thesis by simp
 qed
 
-lemma (in comm_group) iso_imp_comm_group:
+lemma (in comm_group) iso_imp_comm_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "G \<cong> H" "monoid H"
   shows "comm_group H"
 proof -
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -513,13 +513,11 @@
 qed
 
 
-(* Next lemma contributed by Paulo Emílio de Vilhena. *)
-
 text \<open>This next lemma would be trivial if placed in a theory that imports QuotRing,
       but it makes more sense to have it here (easier to find and coherent with the
       previous developments).\<close>
 
-lemma (in cring) cgenideal_prod:
+lemma (in cring) cgenideal_prod: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "(PIdl a) <#> (PIdl b) = PIdl (a \<otimes> b)"
 proof -
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -425,8 +425,7 @@
   thus "?L \<subseteq> ?R" by auto
 qed
 
-(* Next three lemmas contributed by Paulo Emílio de Vilhena*)
-lemma generate_pow_on_finite_carrier:
+lemma generate_pow_on_finite_carrier: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "finite (carrier G)" and "a \<in> carrier G"
   shows "generate G { a } = { a [^] k | k. k \<in> (UNIV :: nat set) }"
 proof
@@ -469,7 +468,7 @@
   qed
 qed
 
-lemma generate_pow_card:
+lemma generate_pow_card: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "finite (carrier G)" and "a \<in> carrier G"
   shows "ord a = card (generate G { a })"
 proof -
@@ -481,7 +480,7 @@
 
 (* This lemma was a suggestion of generalization given by Jeremy Avigad
    at the end of the theory FiniteProduct. *)
-corollary power_order_eq_one_group_version:
+corollary power_order_eq_one_group_version: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "finite (carrier G)" and "a \<in> carrier G"
   shows "a [^] (order G) = \<one>"
 proof -
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/Ring.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -532,18 +532,16 @@
   case (insert x F) then show ?case by (simp add: Pi_def r_distr)
 qed
 
-(* ************************************************************************** *)
-(* Contributed by Paulo E. de Vilhena.                                        *)
 
 text \<open>A quick detour\<close>
 
-lemma add_pow_int_ge: "(k :: int) \<ge> 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = [ nat k ] \<cdot>\<^bsub>R\<^esub> a"
+lemma add_pow_int_ge: "(k :: int) \<ge> 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = [ nat k ] \<cdot>\<^bsub>R\<^esub> a" \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   by (simp add: add_pow_def int_pow_def nat_pow_def)
 
-lemma add_pow_int_lt: "(k :: int) < 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = \<ominus>\<^bsub>R\<^esub> ([ nat (- k) ] \<cdot>\<^bsub>R\<^esub> a)"
+lemma add_pow_int_lt: "(k :: int) < 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = \<ominus>\<^bsub>R\<^esub> ([ nat (- k) ] \<cdot>\<^bsub>R\<^esub> a)" \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def)
 
-corollary (in semiring) add_pow_ldistr:
+corollary (in semiring) add_pow_ldistr: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "([(k :: nat)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)"
 proof -
@@ -556,7 +554,7 @@
   finally show ?thesis .
 qed
 
-corollary (in semiring) add_pow_rdistr:
+corollary (in semiring) add_pow_rdistr: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "a \<otimes> ([(k :: nat)] \<cdot> b) = [k] \<cdot> (a \<otimes> b)"
 proof -
@@ -570,7 +568,7 @@
 qed
 
 (* For integers, we need the uniqueness of the additive inverse *)
-lemma (in ring) add_pow_ldistr_int:
+lemma (in ring) add_pow_ldistr_int: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "([(k :: int)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)"
 proof (cases "k \<ge> 0")
@@ -582,7 +580,7 @@
           add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto
 qed
 
-lemma (in ring) add_pow_rdistr_int:
+lemma (in ring) add_pow_rdistr_int: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "a \<otimes> ([(k :: int)] \<cdot> b) = [k] \<cdot> (a \<otimes> b)"
 proof (cases "k \<ge> 0")
@@ -801,9 +799,7 @@
 lemma id_ring_hom [simp]: "id \<in> ring_hom R R"
   by (auto intro!: ring_hom_memI)
 
-(* Next lemma contributed by Paulo Emílio de Vilhena. *)
-
-lemma ring_hom_trans:
+lemma ring_hom_trans: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "\<lbrakk> f \<in> ring_hom R S; g \<in> ring_hom S T \<rbrakk> \<Longrightarrow> g \<circ> f \<in> ring_hom R T"
   by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one)
 
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -181,8 +181,7 @@
   by (induct n) (auto)
 
 
-(*contributed by Paulo Emílio de Vilhena*)
-lemma (in ring_hom_ring) inj_on_domain:
+lemma (in ring_hom_ring) inj_on_domain: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "inj_on h (carrier R)"
   shows "domain S \<Longrightarrow> domain R"
 proof -
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Library/Multiset.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -2099,8 +2099,7 @@
   shows "mset_set A = mset_set B \<longleftrightarrow> A = B"
   using assms by (fastforce dest: finite_set_mset_mset_set)
 
-(* Contributed by Lukas Bulwahn *)
-lemma image_mset_mset_set:
+lemma image_mset_mset_set: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
   assumes "inj_on f A"
   shows "image_mset f (mset_set A) = mset_set (f ` A)"
 proof cases
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Library/Permutations.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -112,8 +112,7 @@
 lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
   by (simp add: Ball_def permutes_def) metis
 
-(* Next three lemmas contributed by Lukas Bulwahn *)
-lemma permutes_bij_inv_into:
+lemma permutes_bij_inv_into: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
   fixes A :: "'a set"
     and B :: "'b set"
   assumes "p permutes A"
@@ -132,12 +131,12 @@
   then show "(if x \<in> B then f (p (inv_into A f x)) else x) = x" by auto
 qed
 
-lemma permutes_image_mset:
+lemma permutes_image_mset: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
   assumes "p permutes A"
   shows "image_mset p (mset_set A) = mset_set A"
   using assms by (metis image_mset_mset_set bij_betw_imp_inj_on permutes_imp_bij permutes_image)
 
-lemma permutes_implies_image_mset_eq:
+lemma permutes_implies_image_mset_eq: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
   assumes "p permutes A" "\<And>x. x \<in> A \<Longrightarrow> f x = f' (p x)"
   shows "image_mset f' (mset_set A) = image_mset f (mset_set A)"
 proof -
diff -r 2eade8651b93 -r 6b03a8cf092d src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Library/Product_Order.thy	Sun Mar 10 23:23:03 2019 +0100
@@ -219,20 +219,18 @@
 text \<open>Alternative formulations for set infima and suprema over the product
 of two complete lattices:\<close>
 
-lemma INF_prod_alt_def:
+lemma INF_prod_alt_def: \<^marker>\<open>contributor \<open>Alessandro Coglio\<close>\<close>
   "Inf (f ` A) = (Inf ((fst \<circ> f) ` A), Inf ((snd \<circ> f) ` A))"
   by (simp add: Inf_prod_def image_image)
 
-lemma SUP_prod_alt_def:
+lemma SUP_prod_alt_def: \<^marker>\<open>contributor \<open>Alessandro Coglio\<close>\<close>
   "Sup (f ` A) = (Sup ((fst \<circ> f) ` A), Sup((snd \<circ> f) ` A))"
   by (simp add: Sup_prod_def image_image)
 
 
 subsection \<open>Complete distributive lattices\<close>
 
-(* Contribution: Alessandro Coglio *)
-
-instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
+instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice \<^marker>\<open>contributor \<open>Alessandro Coglio\<close>\<close>
 proof
   fix A::"('a\<times>'b) set set"
   show "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"