diff -r 516e81f75957 -r b680e74eb6f2 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy Fri Jun 29 23:04:36 2018 +0200
+++ b/src/HOL/Algebra/RingHom.thy Sat Jun 30 15:44:04 2018 +0100
@@ -203,4 +203,37 @@
show "x \ a_kernel R S h +> a" by (rule homeq_imp_rcos)
qed
+(*contributed by Paulo EmÃlio de Vilhena*)
+lemma (in ring_hom_ring) inj_on_domain:
+ assumes "inj_on h (carrier R)"
+ shows "domain S \ domain R"
+proof -
+ assume A: "domain S" show "domain R"
+ proof
+ have "h \ = \\<^bsub>S\<^esub> \ h \ = \\<^bsub>S\<^esub>" by simp
+ hence "h \ \ h \"
+ using domain.one_not_zero[OF A] by simp
+ thus "\ \ \"
+ using assms unfolding inj_on_def by fastforce
+ next
+ fix a b
+ assume a: "a \ carrier R"
+ and b: "b \ carrier R"
+ have "h (a \ b) = (h a) \\<^bsub>S\<^esub> (h b)" by (simp add: a b)
+ also have " ... = (h b) \\<^bsub>S\<^esub> (h a)" using a b A cringE(1)[of S]
+ by (simp add: cring.cring_simprules(14) domain_def)
+ also have " ... = h (b \ a)" by (simp add: a b)
+ finally have "h (a \ b) = h (b \ a)" .
+ thus "a \ b = b \ a"
+ using assms a b unfolding inj_on_def by simp
+
+ assume ab: "a \ b = \"
+ hence "h (a \ b) = \\<^bsub>S\<^esub>" by simp
+ hence "(h a) \\<^bsub>S\<^esub> (h b) = \\<^bsub>S\<^esub>" using a b by simp
+ hence "h a = \\<^bsub>S\<^esub> \ h b = \\<^bsub>S\<^esub>" using a b domain.integral[OF A] by simp
+ thus "a = \ \ b = \"
+ using a b assms unfolding inj_on_def by force
+ qed
+qed
+
end