products/sources/formale sprachen/Isabelle/ZF/ex/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: matrices.pvs   Sprache: PVS

Original von: 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] => 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 \<open>\<oplus>\<index>\<close> 65) where
  "ring_add(M,x,y) = add_field(M) ` "

definition
  zero :: "i => i" (\<open>\<zero>\<index>\<close>) 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 ` "
  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" (\<open>\<ominus>\<index> _\<close> [81] 80) where
  "a_inv(R) == m_inv ()"

definition
  minus :: "[i,i,i] => i" (\<open>(_ \<ominus>\<index> _)\<close> [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.~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) & y \<in> carrier(R) \<longrightarrow>
        h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
        h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) &
      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

¤ Dauer der Verarbeitung: 0.32 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff