src/HOL/Algebra/Ring.thy
 changeset 68551 b680e74eb6f2 parent 68517 6b5f15387353 child 68552 391e89e03eef
```     1.1 --- a/src/HOL/Algebra/Ring.thy	Fri Jun 29 23:04:36 2018 +0200
1.2 +++ b/src/HOL/Algebra/Ring.thy	Sat Jun 30 15:44:04 2018 +0100
1.3 @@ -333,11 +333,6 @@
1.4      and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
1.5    using assms cring_def apply auto by (simp add: assms cring.axioms(1) ringE(3))
1.6
1.7 -(*
1.8 -lemma (in cring) is_comm_monoid:
1.9 -  "comm_monoid R"
1.10 -  by (auto intro!: comm_monoidI m_assoc m_comm)
1.11 -*)
1.12  lemma (in cring) is_cring:
1.13    "cring R" by (rule cring_axioms)
1.14
1.15 @@ -652,6 +647,15 @@
1.16  text \<open>Field would not need to be derived from domain, the properties
1.17    for domain follow from the assumptions of field\<close>
1.18
1.19 +lemma fieldE :
1.20 +  fixes R (structure)
1.21 +  assumes "field R"
1.22 +  shows "cring R"
1.23 +    and one_not_zero : "\<one> \<noteq> \<zero>"
1.24 +    and integral: "\<And>a b. \<lbrakk> a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>"
1.25 +  and field_Units: "Units R = carrier R - {\<zero>}"
1.26 +  using assms unfolding field_def field_axioms_def domain_def domain_axioms_def by simp_all
1.27 +
1.28  lemma (in cring) cring_fieldI:
1.29    assumes field_Units: "Units R = carrier R - {\<zero>}"
1.30    shows "field R"
```