Quelle Ring.thy Sprache: Isabelle

(* Title:  ZF/ex/Ring.thy

*)

section \<open>Rings\<close>

theory Ring imports Group begin

no_notation cadd  (infixl \<open>\<oplus>\<close> 65) and cmult  (infixl \<open>\<otimes>\<close> 70)

(*First, we must simulate a record declaration:
record ring = monoid +
  add :: "[i, i] \<Rightarrow> i" (infixl "\<oplus>\<index>" 65)
  zero :: i ("\<zero>\<index>")
*)

definition
  add_field :: "i \ i" where
  "add_field(M) = fst(snd(snd(snd(M))))"

definition
  ring_add :: "[i, i, i] \ i" (infixl \\\\ 65) where
  "ring_add(M,x,y) = add_field(M) ` \x,y\"

definition
  zero :: "i \ i" (\\\\) where
  "zero(M) = fst(snd(snd(snd(snd(M)))))"

lemma add_field_eq [simp]: "add_field() = A"
  by (simp add: add_field_def)

lemma add_eq [simp]: "ring_add(, x, y) = A ` \x,y\"
  by (simp add: ring_add_def)

lemma zero_eq [simp]: "zero() = Z"
  by (simp add: zero_def)

text \<open>Derived operations.\<close>

definition
  a_inv :: "[i,i] \ i" (\\\ _\ [81] 80) where
  "a_inv(R) \ m_inv ()"

definition
  minus :: "[i,i,i] \ i" (\(\notation=\infix \\\_ \\ _)\ [65,66] 65) where
  "\x \ carrier(R); y \ carrier(R)\ \ x \\<^bsub>R\<^esub> y = x \\<^bsub>R\<^esub> (\\<^bsub>R\<^esub> y)"

locale abelian_monoid = fixes G (structure)
  assumes a_comm_monoid:
    "comm_monoid ()"

text \<open>
  The following definition is redundant but simple to use.
\<close>

locale abelian_group = abelian_monoid +
  assumes a_comm_group:
    "comm_group ()"

locale ring = abelian_group R + monoid R for R (structure) +
  assumes l_distr: "\x \ carrier(R); y \ carrier(R); z \ carrier(R)\
      \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
    and r_distr: "\x \ carrier(R); y \ carrier(R); z \ carrier(R)\
      \<Longrightarrow> z \<cdot> (x \<oplus> y) = z \<cdot> x \<oplus> z \<cdot> y"

locale cring = ring + comm_monoid R

locale "domain" = cring +
  assumes one_not_zero [simp]: "\ \ \"
    and integral: "\a \ b = \; a \ carrier(R); b \ carrier(R)\ \
                  a = \<zero> | b = \<zero>"

subsection \<open>Basic Properties\<close>

lemma (in abelian_monoid) a_monoid:
     "monoid ()"
apply (insert a_comm_monoid)
apply (simp add: comm_monoid_def)
done

lemma (in abelian_group) a_group:
     "group ()"
apply (insert a_comm_group)
apply (simp add: comm_group_def group_def)
done

lemma (in abelian_monoid) l_zero [simp]:
     "x \ carrier(G) \ \ \ x = x"
apply (insert monoid.l_one [OF a_monoid])
apply (simp add: ring_add_def)
done

lemma (in abelian_monoid) zero_closed [intro, simp]:
     "\ \ carrier(G)"
by (rule monoid.one_closed [OF a_monoid, simplified])

lemma (in abelian_group) a_inv_closed [intro, simp]:
     "x \ carrier(G) \ \ x \ carrier(G)"
by (simp add: a_inv_def  group.inv_closed [OF a_group, simplified])

lemma (in abelian_monoid) a_closed [intro, simp]:
     "\x \ carrier(G); y \ carrier(G)\ \ x \ y \ carrier(G)"
by (rule monoid.m_closed [OF a_monoid,
                  simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_group) minus_closed [intro, simp]:
     "\x \ carrier(G); y \ carrier(G)\ \ x \ y \ carrier(G)"
by (simp add: minus_def)

lemma (in abelian_group) a_l_cancel [simp]:
     "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\
      \<Longrightarrow> (x \<oplus> y = x \<oplus> z) \<longleftrightarrow> (y = z)"
by (rule group.l_cancel [OF a_group,
             simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_group) a_r_cancel [simp]:
     "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\
      \<Longrightarrow> (y \<oplus> x = z \<oplus> x) \<longleftrightarrow> (y = z)"
by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_monoid) a_assoc:
  "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\
   \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_group) l_neg:
     "x \ carrier(G) \ \ x \ x = \"
by (simp add: a_inv_def
     group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_monoid) a_comm:
     "\x \ carrier(G); y \ carrier(G)\ \ x \ y = y \ x"
by (rule comm_monoid.m_comm [OF a_comm_monoid,
    simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_monoid) a_lcomm:
     "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\
      \<Longrightarrow> x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
    simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_monoid) r_zero [simp]:
     "x \ carrier(G) \ x \ \ = x"
  using monoid.r_one [OF a_monoid]
  by (simp add: ring_add_def [symmetric])

lemma (in abelian_group) r_neg:
     "x \ carrier(G) \ x \ (\ x) = \"
  using group.r_inv [OF a_group]
  by (simp add: a_inv_def ring_add_def [symmetric])

lemma (in abelian_group) minus_zero [simp]:
     "\ \ = \"
  by (simp add: a_inv_def
    group.inv_one [OF a_group, simplified ])

lemma (in abelian_group) minus_minus [simp]:
     "x \ carrier(G) \ \ (\ x) = x"
  using group.inv_inv [OF a_group, simplified]
  by (simp add: a_inv_def)

lemma (in abelian_group) minus_add:
     "\x \ carrier(G); y \ carrier(G)\ \ \ (x \ y) = \ x \ \ y"
  using comm_group.inv_mult [OF a_comm_group]
  by (simp add: a_inv_def ring_add_def [symmetric])

lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm

text \<open>
  The following proofs are from Jacobson, Basic Algebra I, pp.\<not>88--89
\<close>

context ring
begin

lemma l_null [simp]: "x \ carrier(R) \ \ \ x = \"
proof -
  assume R: "x \ carrier(R)"
  then have "\ \ x \ \ \ x = (\ \ \) \ x"
    by (blast intro: l_distr [THEN sym])
  also from R have "... = \ \ x \ \" by simp
  finally have "\ \ x \ \ \ x = \ \ x \ \" .
  with R show ?thesis by (simp del: r_zero)
qed

lemma r_null [simp]: "x \ carrier(R) \ x \ \ = \"
proof -
  assume R: "x \ carrier(R)"
  then have "x \ \ \ x \ \ = x \ (\ \ \)"
    by (simp add: r_distr del: l_zero r_zero)
  also from R have "... = x \ \ \ \" by simp
  finally have "x \ \ \ x \ \ = x \ \ \ \" .
  with R show ?thesis by (simp del: r_zero)
qed

lemma l_minus:
  "\x \ carrier(R); y \ carrier(R)\ \ \ x \ y = \ (x \ y)"
proof -
  assume R: "x \ carrier(R)" "y \ carrier(R)"
  then have "(\ x) \ y \ x \ y = (\ x \ x) \ y" by (simp add: l_distr)
  also from R have "... = \" by (simp add: l_neg)
  finally have "(\ x) \ y \ x \ y = \" .
  with R have "(\ x) \ y \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp
  with R show ?thesis by (simp add: a_assoc r_neg)
qed

lemma r_minus:
  "\x \ carrier(R); y \ carrier(R)\ \ x \ \ y = \ (x \ y)"
proof -
  assume R: "x \ carrier(R)" "y \ carrier(R)"
  then have "x \ (\ y) \ x \ y = x \ (\ y \ y)" by (simp add: r_distr)
  also from R have "... = \" by (simp add: l_neg)
  finally have "x \ (\ y) \ x \ y = \" .
  with R have "x \ (\ y) \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp
  with R show ?thesis by (simp add: a_assoc r_neg)
qed

lemma minus_eq:
  "\x \ carrier(R); y \ carrier(R)\ \ x \ y = x \ \ y"
  by (simp only: minus_def)

end

subsection \<open>Morphisms\<close>

definition
  ring_hom :: "[i,i] \ i" where
  "ring_hom(R,S) \
    {h \<in> carrier(R) -> carrier(S).
      (\<forall>x y. x \<in> carrier(R) \<and> y \<in> carrier(R) \<longrightarrow>
        h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) \<and>
        h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) \<and>
      h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"

lemma ring_hom_memI:
  assumes hom_type: "h \ carrier(R) \ carrier(S)"
    and hom_mult: "\x y. \x \ carrier(R); y \ carrier(R)\ \
      h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
    and hom_add: "\x y. \x \ carrier(R); y \ carrier(R)\ \
      h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
    and hom_one: "h ` \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>"
  shows "h \ ring_hom(R,S)"
by (auto simp add: ring_hom_def assms)

lemma ring_hom_closed:
     "\h \ ring_hom(R,S); x \ carrier(R)\ \ h ` x \ carrier(S)"
by (auto simp add: ring_hom_def)

lemma ring_hom_mult:
     "\h \ ring_hom(R,S); x \ carrier(R); y \ carrier(R)\
      \<Longrightarrow> h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
by (simp add: ring_hom_def)

lemma ring_hom_add:
     "\h \ ring_hom(R,S); x \ carrier(R); y \ carrier(R)\
      \<Longrightarrow> h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
by (simp add: ring_hom_def)

lemma ring_hom_one: "h \ ring_hom(R,S) \ h ` \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>"
by (simp add: ring_hom_def)

locale ring_hom_cring = R: cring R + S: cring S
  for R (structure) and S (structure) and h +
  assumes homh [simp, intro]: "h \ ring_hom(R,S)"
  notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
    and hom_mult [simp] = ring_hom_mult [OF homh]
    and hom_add [simp] = ring_hom_add [OF homh]
    and hom_one [simp] = ring_hom_one [OF homh]

lemma (in ring_hom_cring) hom_zero [simp]:
     "h ` \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>"
proof -
  have "h ` \\<^bsub>R\<^esub> \\<^bsub>S\<^esub> h ` \ = h ` \\<^bsub>R\<^esub> \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>"
    by (simp add: hom_add [symmetric] del: hom_add)
  then show ?thesis by (simp del: S.r_zero)
qed

lemma (in ring_hom_cring) hom_a_inv [simp]:
     "x \ carrier(R) \ h ` (\\<^bsub>R\<^esub> x) = \\<^bsub>S\<^esub> h ` x"
proof -
  assume R: "x \ carrier(R)"
  then have "h ` x \\<^bsub>S\<^esub> h ` (\ x) = h ` x \\<^bsub>S\<^esub> (\\<^bsub>S\<^esub> (h ` x))"
    by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
  with R show ?thesis by simp
qed

lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) \ ring_hom(R,R)"
apply (rule ring_hom_memI)
apply (auto simp add: id_type)
done

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.