--- 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}"
--- 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"
--- 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)
--- 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>)"]
--- 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 -
--- 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 -
--- 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 -
--- 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)
--- 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 -
--- 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
--- 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 -
--- 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})"