src/HOL/Algebra/Ring.thy
 changeset 67091 1393c2340eec parent 63167 0909deb8059b child 67341 df79ef3b3a41
```     1.1 --- a/src/HOL/Algebra/Ring.thy	Sun Nov 26 13:19:52 2017 +0100
1.2 +++ b/src/HOL/Algebra/Ring.thy	Sun Nov 26 21:08:32 2017 +0100
1.3 @@ -238,9 +238,9 @@
1.4  locale cring = ring + comm_monoid R
1.5
1.6  locale "domain" = cring +
1.7 -  assumes one_not_zero [simp]: "\<one> ~= \<zero>"
1.8 +  assumes one_not_zero [simp]: "\<one> \<noteq> \<zero>"
1.9      and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==>
1.10 -                  a = \<zero> | b = \<zero>"
1.11 +                  a = \<zero> \<or> b = \<zero>"
1.12
1.13  locale field = "domain" +
1.14    assumes field_Units: "Units R = carrier R - {\<zero>}"
1.15 @@ -427,7 +427,7 @@
1.16    a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
1.17
1.18  lemma (in semiring) nat_pow_zero:
1.19 -  "(n::nat) ~= 0 ==> \<zero> (^) n = \<zero>"
1.20 +  "(n::nat) \<noteq> 0 \<Longrightarrow> \<zero> (^) n = \<zero>"
1.21    by (induct n) simp_all
1.22
1.23  context semiring begin
1.24 @@ -469,7 +469,7 @@
1.25    fixes R (structure) and S (structure)
1.26    assumes "ring R" "cring S"
1.27    assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
1.28 -  shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
1.29 +  shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b \<and> c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
1.30  proof -
1.31    interpret ring R by fact
1.32    interpret cring S by fact
1.33 @@ -513,27 +513,27 @@
1.34  context "domain" begin
1.35
1.36  lemma zero_not_one [simp]:
1.37 -  "\<zero> ~= \<one>"
1.38 +  "\<zero> \<noteq> \<one>"
1.39    by (rule not_sym) simp
1.40
1.41  lemma integral_iff: (* not by default a simp rule! *)
1.42 -  "[| a \<in> carrier R; b \<in> carrier R |] ==> (a \<otimes> b = \<zero>) = (a = \<zero> | b = \<zero>)"
1.43 +  "[| a \<in> carrier R; b \<in> carrier R |] ==> (a \<otimes> b = \<zero>) = (a = \<zero> \<or> b = \<zero>)"
1.44  proof
1.45    assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>"
1.46 -  then show "a = \<zero> | b = \<zero>" by (simp add: integral)
1.47 +  then show "a = \<zero> \<or> b = \<zero>" by (simp add: integral)
1.48  next
1.49 -  assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> | b = \<zero>"
1.50 +  assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> \<or> b = \<zero>"
1.51    then show "a \<otimes> b = \<zero>" by auto
1.52  qed
1.53
1.54  lemma m_lcancel:
1.55 -  assumes prem: "a ~= \<zero>"
1.56 +  assumes prem: "a \<noteq> \<zero>"
1.57      and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
1.58    shows "(a \<otimes> b = a \<otimes> c) = (b = c)"
1.59  proof
1.60    assume eq: "a \<otimes> b = a \<otimes> c"
1.61    with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
1.62 -  with R have "a = \<zero> | (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
1.63 +  with R have "a = \<zero> \<or> (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
1.64    with prem and R have "b \<ominus> c = \<zero>" by auto
1.65    with R have "b = b \<ominus> (b \<ominus> c)" by algebra
1.66    also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
1.67 @@ -543,7 +543,7 @@
1.68  qed
1.69
1.70  lemma m_rcancel:
1.71 -  assumes prem: "a ~= \<zero>"
1.72 +  assumes prem: "a \<noteq> \<zero>"
1.73      and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
1.74    shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)"
1.75  proof -
1.76 @@ -609,9 +609,9 @@
1.77  definition
1.78    ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
1.79    where "ring_hom R S =
1.80 -    {h. h \<in> carrier R \<rightarrow> carrier S &
1.81 -      (ALL x y. x \<in> carrier R & y \<in> carrier R -->
1.82 -        h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
1.83 +    {h. h \<in> carrier R \<rightarrow> carrier S \<and>
1.84 +      (\<forall>x y. x \<in> carrier R \<and> y \<in> carrier R \<longrightarrow>
1.85 +        h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y \<and> h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) \<and>
1.86        h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
1.87
1.88  lemma ring_hom_memI:
1.89 @@ -675,13 +675,13 @@
1.90  qed
1.91
1.92  lemma (in ring_hom_cring) hom_finsum [simp]:
1.93 -  "f \<in> A \<rightarrow> carrier R ==>
1.94 -  h (finsum R f A) = finsum S (h o f) A"
1.95 +  "f \<in> A \<rightarrow> carrier R \<Longrightarrow>
1.96 +  h (finsum R f A) = finsum S (h \<circ> f) A"
1.97    by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
1.98
1.99  lemma (in ring_hom_cring) hom_finprod:
1.100 -  "f \<in> A \<rightarrow> carrier R ==>
1.101 -  h (finprod R f A) = finprod S (h o f) A"
1.102 +  "f \<in> A \<rightarrow> carrier R \<Longrightarrow>
1.103 +  h (finprod R f A) = finprod S (h \<circ> f) A"
1.104    by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
1.105
1.106  declare ring_hom_cring.hom_finprod [simp]
```