more formal contributors (with the help of the history);
authorwenzelm
Sun Mar 10 23:23:03 2019 +0100 (6 weeks ago ago)
changeset 700766b03a8cf092d
parent 70075 2eade8651b93
child 70077 be7243b97c41
more formal contributors (with the help of the history);
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/Multiplicative_Group.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/Product_Order.thy
     1.1 --- a/src/HOL/Algebra/Congruence.thy	Sun Mar 10 22:38:00 2019 +0100
     1.2 +++ b/src/HOL/Algebra/Congruence.thy	Sun Mar 10 23:23:03 2019 +0100
     1.3 @@ -270,9 +270,7 @@
     1.4    using assms by (meson closure_of_memE elemE)
     1.5  
     1.6  
     1.7 -(* Lemmas by Paulo Emílio de Vilhena *)
     1.8 -
     1.9 -lemma (in partition) equivalence_from_partition:
    1.10 +lemma (in partition) equivalence_from_partition: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.11    "equivalence \<lparr> carrier = A, eq = (\<lambda>x y. y \<in> (THE b. b \<in> B \<and> x \<in> b))\<rparr>"
    1.12      unfolding partition_def equivalence_def
    1.13  proof (auto)
    1.14 @@ -285,10 +283,10 @@
    1.15      using unique_class by (metis (mono_tags, lifting) the_equality)
    1.16  qed
    1.17  
    1.18 -lemma (in partition) partition_coverture: "\<Union>B = A"
    1.19 +lemma (in partition) partition_coverture: "\<Union>B = A" \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.20    by (meson Sup_le_iff UnionI unique_class incl subsetI subset_antisym)
    1.21  
    1.22 -lemma (in partition) disjoint_union:
    1.23 +lemma (in partition) disjoint_union: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.24    assumes "b1 \<in> B" "b2 \<in> B"
    1.25      and "b1 \<inter> b2 \<noteq> {}"
    1.26    shows "b1 = b2"
    1.27 @@ -299,7 +297,7 @@
    1.28    thus False using unique_class \<open>b1 \<noteq> b2\<close> assms(1) assms(2) by blast
    1.29  qed
    1.30  
    1.31 -lemma partitionI:
    1.32 +lemma partitionI: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.33    fixes A :: "'a set" and B :: "('a set) set"
    1.34    assumes "\<Union>B = A"
    1.35      and "\<And>b1 b2. \<lbrakk> b1 \<in> B; b2 \<in> B \<rbrakk> \<Longrightarrow> b1 \<inter> b2 \<noteq> {} \<Longrightarrow> b1 = b2"
    1.36 @@ -316,7 +314,7 @@
    1.37    show "\<And>b. b \<in> B \<Longrightarrow> b \<subseteq> A" using assms(1) by blast
    1.38  qed
    1.39  
    1.40 -lemma (in partition) remove_elem:
    1.41 +lemma (in partition) remove_elem: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.42    assumes "b \<in> B"
    1.43    shows "partition (A - b) (B - {b})"
    1.44  proof
    1.45 @@ -327,7 +325,7 @@
    1.46      using assms unique_class incl partition_axioms partition_coverture by fastforce
    1.47  qed
    1.48  
    1.49 -lemma disjoint_sum:
    1.50 +lemma disjoint_sum: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.51    "\<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)"
    1.52  proof (induct arbitrary: A set: finite)
    1.53    case empty thus ?case using partition.unique_class by fastforce
    1.54 @@ -343,7 +341,7 @@
    1.55      by (metis add.commute insert_iff partition.incl sum.subset_diff)
    1.56  qed
    1.57  
    1.58 -lemma (in partition) disjoint_sum:
    1.59 +lemma (in partition) disjoint_sum: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.60    assumes "finite A"
    1.61    shows "(\<Sum>b\<in>B. \<Sum>a\<in>b. f a) = (\<Sum>a\<in>A. f a)"
    1.62  proof -
    1.63 @@ -352,20 +350,20 @@
    1.64    thus ?thesis using disjoint_sum assms partition_axioms by blast
    1.65  qed
    1.66  
    1.67 -lemma (in equivalence) set_eq_insert_aux:
    1.68 +lemma (in equivalence) set_eq_insert_aux: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.69    assumes "A \<subseteq> carrier S"
    1.70      and "x \<in> carrier S" "x' \<in> carrier S" "x .= x'"
    1.71      and "y \<in> insert x A"
    1.72    shows "y .\<in> insert x' A"
    1.73    by (metis assms(1) assms(4) assms(5) contra_subsetD elemI elem_exact insert_iff)
    1.74  
    1.75 -corollary (in equivalence) set_eq_insert:
    1.76 +corollary (in equivalence) set_eq_insert: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.77    assumes "A \<subseteq> carrier S"
    1.78      and "x \<in> carrier S" "x' \<in> carrier S" "x .= x'"
    1.79    shows "insert x A {.=} insert x' A"
    1.80    by (meson set_eqI assms set_eq_insert_aux sym equivalence_axioms)
    1.81  
    1.82 -lemma (in equivalence) set_eq_pairI:
    1.83 +lemma (in equivalence) set_eq_pairI: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    1.84    assumes xx': "x .= x'"
    1.85      and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S"
    1.86    shows "{x, y} {.=} {x', y}"
     2.1 --- a/src/HOL/Algebra/Coset.thy	Sun Mar 10 22:38:00 2019 +0100
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Sun Mar 10 23:23:03 2019 +0100
     2.3 @@ -41,21 +41,17 @@
     2.4  lemma (in comm_group) subgroup_imp_normal: "subgroup A G \<Longrightarrow> A \<lhd> G"
     2.5    by (simp add: normal_def normal_axioms_def is_group l_coset_def r_coset_def m_comm subgroup.mem_carrier)
     2.6  
     2.7 -(*Next two lemmas contributed by Martin Baillon.*)
     2.8 -
     2.9 -lemma l_coset_eq_set_mult:
    2.10 +lemma l_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    2.11    fixes G (structure)
    2.12    shows "x <# H = {x} <#> H"
    2.13    unfolding l_coset_def set_mult_def by simp
    2.14  
    2.15 -lemma r_coset_eq_set_mult:
    2.16 +lemma r_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    2.17    fixes G (structure)
    2.18    shows "H #> x = H <#> {x}"
    2.19    unfolding r_coset_def set_mult_def by simp
    2.20  
    2.21 -(* Next five lemmas contributed by Paulo Emílio de Vilhena.                    *)
    2.22 -
    2.23 -lemma (in subgroup) rcosets_non_empty:
    2.24 +lemma (in subgroup) rcosets_non_empty: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    2.25    assumes "R \<in> rcosets H"
    2.26    shows "R \<noteq> {}"
    2.27  proof -
    2.28 @@ -66,7 +62,7 @@
    2.29    thus ?thesis by blast
    2.30  qed
    2.31  
    2.32 -lemma (in group) diff_neutralizes:
    2.33 +lemma (in group) diff_neutralizes: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    2.34    assumes "subgroup H G" "R \<in> rcosets H"
    2.35    shows "\<And>r1 r2. \<lbrakk> r1 \<in> R; r2 \<in> R \<rbrakk> \<Longrightarrow> r1 \<otimes> (inv r2) \<in> H"
    2.36  proof -
    2.37 @@ -94,24 +90,25 @@
    2.38    thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def)
    2.39  qed
    2.40  
    2.41 -lemma mono_set_mult: "\<lbrakk> H \<subseteq> H'; K \<subseteq> K' \<rbrakk> \<Longrightarrow> H <#>\<^bsub>G\<^esub> K \<subseteq> H' <#>\<^bsub>G\<^esub> K'"
    2.42 +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>
    2.43    unfolding set_mult_def by (simp add: UN_mono)
    2.44  
    2.45  
    2.46  subsection \<open>Stable Operations for Subgroups\<close>
    2.47  
    2.48 -lemma set_mult_consistent [simp]:
    2.49 +lemma set_mult_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    2.50    "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K"
    2.51    unfolding set_mult_def by simp
    2.52  
    2.53 -lemma r_coset_consistent [simp]:
    2.54 +lemma r_coset_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    2.55    "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #>\<^bsub>G\<^esub> h"
    2.56    unfolding r_coset_def by simp
    2.57  
    2.58 -lemma l_coset_consistent [simp]:
    2.59 +lemma l_coset_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    2.60    "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <#\<^bsub>G\<^esub> I"
    2.61    unfolding l_coset_def by simp
    2.62  
    2.63 +
    2.64  subsection \<open>Basic Properties of set multiplication\<close>
    2.65  
    2.66  lemma (in group) setmult_subset_G:
    2.67 @@ -124,8 +121,7 @@
    2.68    shows "H <#> K \<subseteq> carrier G"
    2.69    using assms by (auto simp add: set_mult_def subsetD)
    2.70  
    2.71 -(* Next lemma contributed by Martin Baillon.*)
    2.72 -lemma (in group) set_mult_assoc:
    2.73 +lemma (in group) set_mult_assoc: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    2.74    assumes "M \<subseteq> carrier G" "H \<subseteq> carrier G" "K \<subseteq> carrier G"
    2.75    shows "(M <#> H) <#> K = M <#> (H <#> K)"
    2.76  proof
    2.77 @@ -1094,13 +1090,11 @@
    2.78    using FactGroup_iso_set unfolding is_iso_def by auto
    2.79  
    2.80  
    2.81 -(* Next two lemmas contributed by Paulo Emílio de Vilhena. *)
    2.82 -
    2.83 -lemma (in group_hom) trivial_hom_iff:
    2.84 +lemma (in group_hom) trivial_hom_iff: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    2.85    "h ` (carrier G) = { \<one>\<^bsub>H\<^esub> } \<longleftrightarrow> kernel G H h = carrier G"
    2.86    unfolding kernel_def using one_closed by force
    2.87  
    2.88 -lemma (in group_hom) trivial_ker_imp_inj:
    2.89 +lemma (in group_hom) trivial_ker_imp_inj: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    2.90    assumes "kernel G H h = { \<one> }"
    2.91    shows "inj_on h (carrier G)"
    2.92  proof (rule inj_onI)
    2.93 @@ -1197,11 +1191,9 @@
    2.94  qed
    2.95  
    2.96  
    2.97 -(* Next subsection contributed by Martin Baillon. *)
    2.98 -
    2.99  subsection \<open>Theorems about Factor Groups and Direct product\<close>
   2.100  
   2.101 -lemma (in group) DirProd_normal :
   2.102 +lemma (in group) DirProd_normal : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   2.103    assumes "group K"
   2.104      and "H \<lhd> G"
   2.105      and "N \<lhd> K"
   2.106 @@ -1231,7 +1223,7 @@
   2.107    qed
   2.108  qed
   2.109  
   2.110 -lemma (in group) FactGroup_DirProd_multiplication_iso_set :
   2.111 +lemma (in group) FactGroup_DirProd_multiplication_iso_set : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   2.112    assumes "group K"
   2.113      and "H \<lhd> G"
   2.114      and "N \<lhd> K"
   2.115 @@ -1261,14 +1253,14 @@
   2.116      unfolding iso_def hom_def bij_betw_def inj_on_def by simp
   2.117  qed
   2.118  
   2.119 -corollary (in group) FactGroup_DirProd_multiplication_iso_1 :
   2.120 +corollary (in group) FactGroup_DirProd_multiplication_iso_1 : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   2.121    assumes "group K"
   2.122      and "H \<lhd> G"
   2.123      and "N \<lhd> K"
   2.124    shows "  ((G Mod H) \<times>\<times> (K Mod N)) \<cong> (G \<times>\<times> K Mod H \<times> N)"
   2.125    unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto
   2.126  
   2.127 -corollary (in group) FactGroup_DirProd_multiplication_iso_2 :
   2.128 +corollary (in group) FactGroup_DirProd_multiplication_iso_2 : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   2.129    assumes "group K"
   2.130      and "H \<lhd> G"
   2.131      and "N \<lhd> K"
     3.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 10 22:38:00 2019 +0100
     3.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 10 23:23:03 2019 +0100
     3.3 @@ -755,8 +755,7 @@
     3.4    using assms
     3.5    by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)
     3.6  
     3.7 -(*by Paulo Emílio de Vilhena*)
     3.8 -lemma (in comm_monoid_cancel) prime_irreducible:
     3.9 +lemma (in comm_monoid_cancel) prime_irreducible: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    3.10    assumes "prime G p"
    3.11    shows "irreducible G p"
    3.12  proof (rule irreducibleI)
     4.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 10 22:38:00 2019 +0100
     4.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 10 23:23:03 2019 +0100
     4.3 @@ -517,9 +517,7 @@
     4.4      using finprod_Suc[of f k] assms atMost_Suc lessThan_Suc_atMost by simp
     4.5  qed
     4.6  
     4.7 -(* The following two were contributed by Jeremy Avigad. *)
     4.8 -
     4.9 -lemma finprod_reindex:
    4.10 +lemma finprod_reindex: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close>
    4.11    "f \<in> (h ` A) \<rightarrow> carrier G \<Longrightarrow>
    4.12          inj_on h A \<Longrightarrow> finprod G f (h ` A) = finprod G (\<lambda>x. f (h x)) A"
    4.13  proof (induct A rule: infinite_finite_induct)
    4.14 @@ -529,7 +527,7 @@
    4.15    with \<open>\<not> finite A\<close> show ?case by simp
    4.16  qed (auto simp add: Pi_def)
    4.17  
    4.18 -lemma finprod_const:
    4.19 +lemma finprod_const: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close>
    4.20    assumes a [simp]: "a \<in> carrier G"
    4.21      shows "finprod G (\<lambda>x. a) A = a [^] card A"
    4.22  proof (induct A rule: infinite_finite_induct)
    4.23 @@ -541,9 +539,7 @@
    4.24    qed auto
    4.25  qed auto
    4.26  
    4.27 -(* The following lemma was contributed by Jesus Aransay. *)
    4.28 -
    4.29 -lemma finprod_singleton:
    4.30 +lemma finprod_singleton: \<^marker>\<open>contributor \<open>Jesus Aransay\<close>\<close>
    4.31    assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
    4.32    shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i"
    4.33    using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
     5.1 --- a/src/HOL/Algebra/Group.thy	Sun Mar 10 22:38:00 2019 +0100
     5.2 +++ b/src/HOL/Algebra/Group.thy	Sun Mar 10 23:23:03 2019 +0100
     5.3 @@ -501,23 +501,23 @@
     5.4  lemma (in group) inj_on_cmult: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. c \<otimes> x) (carrier G)"
     5.5    by(simp add: inj_on_def)
     5.6  
     5.7 -(*Following subsection contributed by Martin Baillon*)
     5.8 +
     5.9  subsection \<open>Submonoids\<close>
    5.10  
    5.11 -locale submonoid =
    5.12 +locale submonoid = \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.13    fixes H and G (structure)
    5.14    assumes subset: "H \<subseteq> carrier G"
    5.15      and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
    5.16      and one_closed [simp]: "\<one> \<in> H"
    5.17  
    5.18 -lemma (in submonoid) is_submonoid:
    5.19 +lemma (in submonoid) is_submonoid: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.20    "submonoid H G" by (rule submonoid_axioms)
    5.21  
    5.22 -lemma (in submonoid) mem_carrier [simp]:
    5.23 +lemma (in submonoid) mem_carrier [simp]: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.24    "x \<in> H \<Longrightarrow> x \<in> carrier G"
    5.25    using subset by blast
    5.26  
    5.27 -lemma (in submonoid) submonoid_is_monoid [intro]:
    5.28 +lemma (in submonoid) submonoid_is_monoid [intro]: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.29    assumes "monoid G"
    5.30    shows "monoid (G\<lparr>carrier := H\<rparr>)"
    5.31  proof -
    5.32 @@ -526,11 +526,11 @@
    5.33      by (simp add: monoid_def m_assoc)
    5.34  qed
    5.35  
    5.36 -lemma submonoid_nonempty:
    5.37 +lemma submonoid_nonempty: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.38    "~ submonoid {} G"
    5.39    by (blast dest: submonoid.one_closed)
    5.40  
    5.41 -lemma (in submonoid) finite_monoid_imp_card_positive:
    5.42 +lemma (in submonoid) finite_monoid_imp_card_positive: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.43    "finite (carrier G) ==> 0 < card H"
    5.44  proof (rule classical)
    5.45    assume "finite (carrier G)" and a: "~ 0 < card H"
    5.46 @@ -540,7 +540,7 @@
    5.47  qed
    5.48  
    5.49  
    5.50 -lemma (in monoid) monoid_incl_imp_submonoid :
    5.51 +lemma (in monoid) monoid_incl_imp_submonoid : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.52    assumes "H \<subseteq> carrier G"
    5.53  and "monoid (G\<lparr>carrier := H\<rparr>)"
    5.54  shows "submonoid H G"
    5.55 @@ -552,7 +552,7 @@
    5.56    show "\<one> \<in> H " using monoid.one_closed[OF assms(2)] assms by simp
    5.57  qed
    5.58  
    5.59 -lemma (in monoid) inv_unique':
    5.60 +lemma (in monoid) inv_unique': \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.61    assumes "x \<in> carrier G" "y \<in> carrier G"
    5.62    shows "\<lbrakk> x \<otimes> y = \<one>; y \<otimes> x = \<one> \<rbrakk> \<Longrightarrow> y = inv x"
    5.63  proof -
    5.64 @@ -563,7 +563,7 @@
    5.65      using inv_unique[OF l_inv Units_r_inv[OF unit] assms Units_inv_closed[OF unit]] .
    5.66  qed
    5.67  
    5.68 -lemma (in monoid) m_inv_monoid_consistent: (* contributed by Paulo *)
    5.69 +lemma (in monoid) m_inv_monoid_consistent: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    5.70    assumes "x \<in> Units (G \<lparr> carrier := H \<rparr>)" and "submonoid H G"
    5.71    shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
    5.72  proof -
    5.73 @@ -620,7 +620,7 @@
    5.74    shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
    5.75    using assms m_inv_monoid_consistent[OF _ subgroup_is_submonoid] subgroup_Units[of H] by auto
    5.76  
    5.77 -lemma (in group) int_pow_consistent: (* by Paulo *)
    5.78 +lemma (in group) int_pow_consistent: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    5.79    assumes "subgroup H G" "x \<in> H"
    5.80    shows "x [^] (n :: int) = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
    5.81  proof (cases)
    5.82 @@ -687,19 +687,17 @@
    5.83  lemma (in subgroup) finite_imp_card_positive: "finite (carrier G) \<Longrightarrow> 0 < card H"
    5.84    using subset one_closed card_gt_0_iff finite_subset by blast
    5.85  
    5.86 -(*Following 3 lemmas contributed by Martin Baillon*)
    5.87 -
    5.88 -lemma (in subgroup) subgroup_is_submonoid :
    5.89 +lemma (in subgroup) subgroup_is_submonoid : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.90    "submonoid H G"
    5.91    by (simp add: submonoid.intro subset)
    5.92  
    5.93 -lemma (in group) submonoid_subgroupI :
    5.94 +lemma (in group) submonoid_subgroupI : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
    5.95    assumes "submonoid H G"
    5.96      and "\<And>a. a \<in> H \<Longrightarrow> inv a \<in> H"
    5.97    shows "subgroup H G"
    5.98    by (metis assms subgroup_def submonoid_def)
    5.99  
   5.100 -lemma (in group) group_incl_imp_subgroup:
   5.101 +lemma (in group) group_incl_imp_subgroup: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   5.102    assumes "H \<subseteq> carrier G"
   5.103      and "group (G\<lparr>carrier := H\<rparr>)"
   5.104    shows "subgroup H G"
   5.105 @@ -914,9 +912,7 @@
   5.106    using bij_betw_same_card  unfolding is_iso_def iso_def by auto
   5.107  
   5.108  
   5.109 -(* Next four lemmas contributed by Paulo. *)
   5.110 -
   5.111 -lemma (in monoid) hom_imp_img_monoid:
   5.112 +lemma (in monoid) hom_imp_img_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.113    assumes "h \<in> hom G H"
   5.114    shows "monoid (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)" (is "monoid ?h_img")
   5.115  proof (rule monoidI)
   5.116 @@ -953,7 +949,7 @@
   5.117    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)" .
   5.118  qed
   5.119  
   5.120 -lemma (in group) hom_imp_img_group:
   5.121 +lemma (in group) hom_imp_img_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.122    assumes "h \<in> hom G H"
   5.123    shows "group (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)" (is "group ?h_img")
   5.124  proof -
   5.125 @@ -977,7 +973,7 @@
   5.126    qed
   5.127  qed
   5.128  
   5.129 -lemma (in group) iso_imp_group:
   5.130 +lemma (in group) iso_imp_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.131    assumes "G \<cong> H" and "monoid H"
   5.132    shows "group H"
   5.133  proof -
   5.134 @@ -1027,7 +1023,7 @@
   5.135    thus ?thesis unfolding group_def group_axioms_def using assms(2) by simp
   5.136  qed
   5.137  
   5.138 -corollary (in group) iso_imp_img_group:
   5.139 +corollary (in group) iso_imp_img_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.140    assumes "h \<in> iso G H"
   5.141    shows "group (H \<lparr> one := h \<one> \<rparr>)"
   5.142  proof -
   5.143 @@ -1131,20 +1127,17 @@
   5.144    with assms show ?thesis by (simp del: H.r_inv H.Units_r_inv)
   5.145  qed
   5.146  
   5.147 -(* Contributed by Joachim Breitner *)
   5.148 -lemma (in group) int_pow_is_hom:
   5.149 +lemma (in group) int_pow_is_hom: \<^marker>\<open>contributor \<open>Joachim Breitner\<close>\<close>
   5.150    "x \<in> carrier G \<Longrightarrow> (([^]) x) \<in> hom \<lparr> carrier = UNIV, mult = (+), one = 0::int \<rparr> G "
   5.151    unfolding hom_def by (simp add: int_pow_mult)
   5.152  
   5.153 -(* Next six lemmas contributed by Paulo. *)
   5.154 -
   5.155 -lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H"
   5.156 +lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H" \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.157    apply (rule subgroupI)
   5.158    apply (auto simp add: image_subsetI)
   5.159    apply (metis G.inv_closed hom_inv image_iff)
   5.160    by (metis G.monoid_axioms hom_mult image_eqI monoid.m_closed)
   5.161  
   5.162 -lemma (in group_hom) subgroup_img_is_subgroup:
   5.163 +lemma (in group_hom) subgroup_img_is_subgroup: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.164    assumes "subgroup I G"
   5.165    shows "subgroup (h ` I) H"
   5.166  proof -
   5.167 @@ -1158,7 +1151,7 @@
   5.168      using group_hom.img_is_subgroup[of "G \<lparr> carrier := I \<rparr>" H h] by simp
   5.169  qed
   5.170  
   5.171 -lemma (in group_hom) induced_group_hom:
   5.172 +lemma (in group_hom) induced_group_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.173    assumes "subgroup I G"
   5.174    shows "group_hom (G \<lparr> carrier := I \<rparr>) (H \<lparr> carrier := h ` I \<rparr>) h"
   5.175  proof -
   5.176 @@ -1170,18 +1163,18 @@
   5.177            subgroup.subgroup_is_group[OF subgroup_img_is_subgroup[OF assms] is_group] by simp
   5.178  qed
   5.179  
   5.180 -lemma (in group) canonical_inj_is_hom:
   5.181 +lemma (in group) canonical_inj_is_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.182    assumes "subgroup H G"
   5.183    shows "group_hom (G \<lparr> carrier := H \<rparr>) G id"
   5.184    unfolding group_hom_def group_hom_axioms_def hom_def
   5.185    using subgroup.subgroup_is_group[OF assms is_group]
   5.186          is_group subgroup.subset[OF assms] by auto
   5.187  
   5.188 -lemma (in group_hom) nat_pow_hom:
   5.189 +lemma (in group_hom) nat_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.190    "x \<in> carrier G \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
   5.191    by (induction n) auto
   5.192  
   5.193 -lemma (in group_hom) int_pow_hom:
   5.194 +lemma (in group_hom) int_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.195    "x \<in> carrier G \<Longrightarrow> h (x [^] (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
   5.196    using nat_pow_hom by (simp add: int_pow_def2)
   5.197  
   5.198 @@ -1286,9 +1279,7 @@
   5.199    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   5.200    by (simp add: m_ac inv_mult_group)
   5.201  
   5.202 -(* Next three lemmas contributed by Paulo. *)
   5.203 -
   5.204 -lemma (in comm_monoid) hom_imp_img_comm_monoid:
   5.205 +lemma (in comm_monoid) hom_imp_img_comm_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.206    assumes "h \<in> hom G H"
   5.207    shows "comm_monoid (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)" (is "comm_monoid ?h_img")
   5.208  proof (rule monoid.monoid_comm_monoidI)
   5.209 @@ -1309,13 +1300,13 @@
   5.210    finally show "x \<otimes>\<^bsub>(?h_img)\<^esub> y = y \<otimes>\<^bsub>(?h_img)\<^esub> x" .
   5.211  qed
   5.212  
   5.213 -lemma (in comm_group) hom_imp_img_comm_group:
   5.214 +lemma (in comm_group) hom_imp_img_comm_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.215    assumes "h \<in> hom G H"
   5.216    shows "comm_group (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
   5.217    unfolding comm_group_def
   5.218    using hom_imp_img_group[OF assms] hom_imp_img_comm_monoid[OF assms] by simp
   5.219  
   5.220 -lemma (in comm_group) iso_imp_img_comm_group:
   5.221 +lemma (in comm_group) iso_imp_img_comm_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.222    assumes "h \<in> iso G H"
   5.223    shows "comm_group (H \<lparr> one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
   5.224  proof -
   5.225 @@ -1329,7 +1320,7 @@
   5.226    ultimately show ?thesis by simp
   5.227  qed
   5.228  
   5.229 -lemma (in comm_group) iso_imp_comm_group:
   5.230 +lemma (in comm_group) iso_imp_comm_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   5.231    assumes "G \<cong> H" "monoid H"
   5.232    shows "comm_group H"
   5.233  proof -
     6.1 --- a/src/HOL/Algebra/Ideal.thy	Sun Mar 10 22:38:00 2019 +0100
     6.2 +++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 10 23:23:03 2019 +0100
     6.3 @@ -513,13 +513,11 @@
     6.4  qed
     6.5  
     6.6  
     6.7 -(* Next lemma contributed by Paulo Emílio de Vilhena. *)
     6.8 -
     6.9  text \<open>This next lemma would be trivial if placed in a theory that imports QuotRing,
    6.10        but it makes more sense to have it here (easier to find and coherent with the
    6.11        previous developments).\<close>
    6.12  
    6.13 -lemma (in cring) cgenideal_prod:
    6.14 +lemma (in cring) cgenideal_prod: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    6.15    assumes "a \<in> carrier R" "b \<in> carrier R"
    6.16    shows "(PIdl a) <#> (PIdl b) = PIdl (a \<otimes> b)"
    6.17  proof -
     7.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Sun Mar 10 22:38:00 2019 +0100
     7.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Sun Mar 10 23:23:03 2019 +0100
     7.3 @@ -425,8 +425,7 @@
     7.4    thus "?L \<subseteq> ?R" by auto
     7.5  qed
     7.6  
     7.7 -(* Next three lemmas contributed by Paulo Emílio de Vilhena*)
     7.8 -lemma generate_pow_on_finite_carrier:
     7.9 +lemma generate_pow_on_finite_carrier: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    7.10    assumes "finite (carrier G)" and "a \<in> carrier G"
    7.11    shows "generate G { a } = { a [^] k | k. k \<in> (UNIV :: nat set) }"
    7.12  proof
    7.13 @@ -469,7 +468,7 @@
    7.14    qed
    7.15  qed
    7.16  
    7.17 -lemma generate_pow_card:
    7.18 +lemma generate_pow_card: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    7.19    assumes "finite (carrier G)" and "a \<in> carrier G"
    7.20    shows "ord a = card (generate G { a })"
    7.21  proof -
    7.22 @@ -481,7 +480,7 @@
    7.23  
    7.24  (* This lemma was a suggestion of generalization given by Jeremy Avigad
    7.25     at the end of the theory FiniteProduct. *)
    7.26 -corollary power_order_eq_one_group_version:
    7.27 +corollary power_order_eq_one_group_version: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    7.28    assumes "finite (carrier G)" and "a \<in> carrier G"
    7.29    shows "a [^] (order G) = \<one>"
    7.30  proof -
     8.1 --- a/src/HOL/Algebra/Ring.thy	Sun Mar 10 22:38:00 2019 +0100
     8.2 +++ b/src/HOL/Algebra/Ring.thy	Sun Mar 10 23:23:03 2019 +0100
     8.3 @@ -532,18 +532,16 @@
     8.4    case (insert x F) then show ?case by (simp add: Pi_def r_distr)
     8.5  qed
     8.6  
     8.7 -(* ************************************************************************** *)
     8.8 -(* Contributed by Paulo E. de Vilhena.                                        *)
     8.9  
    8.10  text \<open>A quick detour\<close>
    8.11  
    8.12 -lemma add_pow_int_ge: "(k :: int) \<ge> 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = [ nat k ] \<cdot>\<^bsub>R\<^esub> a"
    8.13 +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>
    8.14    by (simp add: add_pow_def int_pow_def nat_pow_def)
    8.15  
    8.16 -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)"
    8.17 +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>
    8.18    by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def)
    8.19  
    8.20 -corollary (in semiring) add_pow_ldistr:
    8.21 +corollary (in semiring) add_pow_ldistr: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    8.22    assumes "a \<in> carrier R" "b \<in> carrier R"
    8.23    shows "([(k :: nat)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)"
    8.24  proof -
    8.25 @@ -556,7 +554,7 @@
    8.26    finally show ?thesis .
    8.27  qed
    8.28  
    8.29 -corollary (in semiring) add_pow_rdistr:
    8.30 +corollary (in semiring) add_pow_rdistr: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    8.31    assumes "a \<in> carrier R" "b \<in> carrier R"
    8.32    shows "a \<otimes> ([(k :: nat)] \<cdot> b) = [k] \<cdot> (a \<otimes> b)"
    8.33  proof -
    8.34 @@ -570,7 +568,7 @@
    8.35  qed
    8.36  
    8.37  (* For integers, we need the uniqueness of the additive inverse *)
    8.38 -lemma (in ring) add_pow_ldistr_int:
    8.39 +lemma (in ring) add_pow_ldistr_int: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    8.40    assumes "a \<in> carrier R" "b \<in> carrier R"
    8.41    shows "([(k :: int)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)"
    8.42  proof (cases "k \<ge> 0")
    8.43 @@ -582,7 +580,7 @@
    8.44            add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto
    8.45  qed
    8.46  
    8.47 -lemma (in ring) add_pow_rdistr_int:
    8.48 +lemma (in ring) add_pow_rdistr_int: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    8.49    assumes "a \<in> carrier R" "b \<in> carrier R"
    8.50    shows "a \<otimes> ([(k :: int)] \<cdot> b) = [k] \<cdot> (a \<otimes> b)"
    8.51  proof (cases "k \<ge> 0")
    8.52 @@ -801,9 +799,7 @@
    8.53  lemma id_ring_hom [simp]: "id \<in> ring_hom R R"
    8.54    by (auto intro!: ring_hom_memI)
    8.55  
    8.56 -(* Next lemma contributed by Paulo Emílio de Vilhena. *)
    8.57 -
    8.58 -lemma ring_hom_trans:
    8.59 +lemma ring_hom_trans: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    8.60    "\<lbrakk> f \<in> ring_hom R S; g \<in> ring_hom S T \<rbrakk> \<Longrightarrow> g \<circ> f \<in> ring_hom R T"
    8.61    by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one)
    8.62  
     9.1 --- a/src/HOL/Algebra/RingHom.thy	Sun Mar 10 22:38:00 2019 +0100
     9.2 +++ b/src/HOL/Algebra/RingHom.thy	Sun Mar 10 23:23:03 2019 +0100
     9.3 @@ -181,8 +181,7 @@
     9.4    by (induct n) (auto)
     9.5  
     9.6  
     9.7 -(*contributed by Paulo Emílio de Vilhena*)
     9.8 -lemma (in ring_hom_ring) inj_on_domain:
     9.9 +lemma (in ring_hom_ring) inj_on_domain: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
    9.10    assumes "inj_on h (carrier R)"
    9.11    shows "domain S \<Longrightarrow> domain R"
    9.12  proof -
    10.1 --- a/src/HOL/Library/Multiset.thy	Sun Mar 10 22:38:00 2019 +0100
    10.2 +++ b/src/HOL/Library/Multiset.thy	Sun Mar 10 23:23:03 2019 +0100
    10.3 @@ -2099,8 +2099,7 @@
    10.4    shows "mset_set A = mset_set B \<longleftrightarrow> A = B"
    10.5    using assms by (fastforce dest: finite_set_mset_mset_set)
    10.6  
    10.7 -(* Contributed by Lukas Bulwahn *)
    10.8 -lemma image_mset_mset_set:
    10.9 +lemma image_mset_mset_set: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
   10.10    assumes "inj_on f A"
   10.11    shows "image_mset f (mset_set A) = mset_set (f ` A)"
   10.12  proof cases
    11.1 --- a/src/HOL/Library/Permutations.thy	Sun Mar 10 22:38:00 2019 +0100
    11.2 +++ b/src/HOL/Library/Permutations.thy	Sun Mar 10 23:23:03 2019 +0100
    11.3 @@ -112,8 +112,7 @@
    11.4  lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
    11.5    by (simp add: Ball_def permutes_def) metis
    11.6  
    11.7 -(* Next three lemmas contributed by Lukas Bulwahn *)
    11.8 -lemma permutes_bij_inv_into:
    11.9 +lemma permutes_bij_inv_into: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
   11.10    fixes A :: "'a set"
   11.11      and B :: "'b set"
   11.12    assumes "p permutes A"
   11.13 @@ -132,12 +131,12 @@
   11.14    then show "(if x \<in> B then f (p (inv_into A f x)) else x) = x" by auto
   11.15  qed
   11.16  
   11.17 -lemma permutes_image_mset:
   11.18 +lemma permutes_image_mset: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
   11.19    assumes "p permutes A"
   11.20    shows "image_mset p (mset_set A) = mset_set A"
   11.21    using assms by (metis image_mset_mset_set bij_betw_imp_inj_on permutes_imp_bij permutes_image)
   11.22  
   11.23 -lemma permutes_implies_image_mset_eq:
   11.24 +lemma permutes_implies_image_mset_eq: \<^marker>\<open>contributor \<open>Lukas Bulwahn\<close>\<close>
   11.25    assumes "p permutes A" "\<And>x. x \<in> A \<Longrightarrow> f x = f' (p x)"
   11.26    shows "image_mset f' (mset_set A) = image_mset f (mset_set A)"
   11.27  proof -
    12.1 --- a/src/HOL/Library/Product_Order.thy	Sun Mar 10 22:38:00 2019 +0100
    12.2 +++ b/src/HOL/Library/Product_Order.thy	Sun Mar 10 23:23:03 2019 +0100
    12.3 @@ -219,20 +219,18 @@
    12.4  text \<open>Alternative formulations for set infima and suprema over the product
    12.5  of two complete lattices:\<close>
    12.6  
    12.7 -lemma INF_prod_alt_def:
    12.8 +lemma INF_prod_alt_def: \<^marker>\<open>contributor \<open>Alessandro Coglio\<close>\<close>
    12.9    "Inf (f ` A) = (Inf ((fst \<circ> f) ` A), Inf ((snd \<circ> f) ` A))"
   12.10    by (simp add: Inf_prod_def image_image)
   12.11  
   12.12 -lemma SUP_prod_alt_def:
   12.13 +lemma SUP_prod_alt_def: \<^marker>\<open>contributor \<open>Alessandro Coglio\<close>\<close>
   12.14    "Sup (f ` A) = (Sup ((fst \<circ> f) ` A), Sup((snd \<circ> f) ` A))"
   12.15    by (simp add: Sup_prod_def image_image)
   12.16  
   12.17  
   12.18  subsection \<open>Complete distributive lattices\<close>
   12.19  
   12.20 -(* Contribution: Alessandro Coglio *)
   12.21 -
   12.22 -instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
   12.23 +instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice \<^marker>\<open>contributor \<open>Alessandro Coglio\<close>\<close>
   12.24  proof
   12.25    fix A::"('a\<times>'b) set set"
   12.26    show "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"