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]