src/ZF/ex/Ring.thy
 author ballarin Thu Dec 11 18:30:26 2008 +0100 (2008-12-11) changeset 29223 e09c53289830 parent 28952 15a4b2cf8c34 child 41524 4d2f9a1c24c7 permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
```     1 (* Title:  ZF/ex/Ring.thy
```
```     2
```
```     3 *)
```
```     4
```
```     5 header {* Rings *}
```
```     6
```
```     7 theory Ring imports Group begin
```
```     8
```
```     9 (*First, we must simulate a record declaration:
```
```    10 record ring = monoid +
```
```    11   add :: "[i, i] => i" (infixl "\<oplus>\<index>" 65)
```
```    12   zero :: i ("\<zero>\<index>")
```
```    13 *)
```
```    14
```
```    15 definition
```
```    16   add_field :: "i => i" where
```
```    17   "add_field(M) = fst(snd(snd(snd(M))))"
```
```    18
```
```    19 definition
```
```    20   ring_add :: "[i, i, i] => i" (infixl "\<oplus>\<index>" 65) where
```
```    21   "ring_add(M,x,y) = add_field(M) ` <x,y>"
```
```    22
```
```    23 definition
```
```    24   zero :: "i => i" ("\<zero>\<index>") where
```
```    25   "zero(M) = fst(snd(snd(snd(snd(M)))))"
```
```    26
```
```    27
```
```    28 lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A"
```
```    29   by (simp add: add_field_def)
```
```    30
```
```    31 lemma add_eq [simp]: "ring_add(<C,M,I,A,z>, x, y) = A ` <x,y>"
```
```    32   by (simp add: ring_add_def)
```
```    33
```
```    34 lemma zero_eq [simp]: "zero(<C,M,I,A,Z,z>) = Z"
```
```    35   by (simp add: zero_def)
```
```    36
```
```    37
```
```    38 text {* Derived operations. *}
```
```    39
```
```    40 definition
```
```    41   a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80) where
```
```    42   "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
```
```    43
```
```    44 definition
```
```    45   minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
```
```    46   "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
```
```    47
```
```    48 locale abelian_monoid = fixes G (structure)
```
```    49   assumes a_comm_monoid:
```
```    50     "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
```
```    51
```
```    52 text {*
```
```    53   The following definition is redundant but simple to use.
```
```    54 *}
```
```    55
```
```    56 locale abelian_group = abelian_monoid +
```
```    57   assumes a_comm_group:
```
```    58     "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
```
```    59
```
```    60 locale ring = abelian_group R + monoid R for R (structure) +
```
```    61   assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
```
```    62       \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
```
```    63     and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
```
```    64       \<Longrightarrow> z \<cdot> (x \<oplus> y) = z \<cdot> x \<oplus> z \<cdot> y"
```
```    65
```
```    66 locale cring = ring + comm_monoid R
```
```    67
```
```    68 locale "domain" = cring +
```
```    69   assumes one_not_zero [simp]: "\<one> \<noteq> \<zero>"
```
```    70     and integral: "\<lbrakk>a \<cdot> b = \<zero>; a \<in> carrier(R); b \<in> carrier(R)\<rbrakk> \<Longrightarrow>
```
```    71                   a = \<zero> | b = \<zero>"
```
```    72
```
```    73
```
```    74 subsection {* Basic Properties *}
```
```    75
```
```    76 lemma (in abelian_monoid) a_monoid:
```
```    77      "monoid (<carrier(G), add_field(G), zero(G), 0>)"
```
```    78 apply (insert a_comm_monoid)
```
```    79 apply (simp add: comm_monoid_def)
```
```    80 done
```
```    81
```
```    82 lemma (in abelian_group) a_group:
```
```    83      "group (<carrier(G), add_field(G), zero(G), 0>)"
```
```    84 apply (insert a_comm_group)
```
```    85 apply (simp add: comm_group_def group_def)
```
```    86 done
```
```    87
```
```    88
```
```    89 lemma (in abelian_monoid) l_zero [simp]:
```
```    90      "x \<in> carrier(G) \<Longrightarrow> \<zero> \<oplus> x = x"
```
```    91 apply (insert monoid.l_one [OF a_monoid])
```
```    92 apply (simp add: ring_add_def)
```
```    93 done
```
```    94
```
```    95 lemma (in abelian_monoid) zero_closed [intro, simp]:
```
```    96      "\<zero> \<in> carrier(G)"
```
```    97 by (rule monoid.one_closed [OF a_monoid, simplified])
```
```    98
```
```    99 lemma (in abelian_group) a_inv_closed [intro, simp]:
```
```   100      "x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<in> carrier(G)"
```
```   101 by (simp add: a_inv_def  group.inv_closed [OF a_group, simplified])
```
```   102
```
```   103 lemma (in abelian_monoid) a_closed [intro, simp]:
```
```   104      "[| x \<in> carrier(G); y \<in> carrier(G) |] ==> x \<oplus> y \<in> carrier(G)"
```
```   105 by (rule monoid.m_closed [OF a_monoid,
```
```   106                   simplified, simplified ring_add_def [symmetric]])
```
```   107
```
```   108 lemma (in abelian_group) minus_closed [intro, simp]:
```
```   109      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<ominus> y \<in> carrier(G)"
```
```   110 by (simp add: minus_def)
```
```   111
```
```   112 lemma (in abelian_group) a_l_cancel [simp]:
```
```   113      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
```
```   114       \<Longrightarrow> (x \<oplus> y = x \<oplus> z) <-> (y = z)"
```
```   115 by (rule group.l_cancel [OF a_group,
```
```   116              simplified, simplified ring_add_def [symmetric]])
```
```   117
```
```   118 lemma (in abelian_group) a_r_cancel [simp]:
```
```   119      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
```
```   120       \<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
```
```   121 by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
```
```   122
```
```   123 lemma (in abelian_monoid) a_assoc:
```
```   124   "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
```
```   125    \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
```
```   126 by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])
```
```   127
```
```   128 lemma (in abelian_group) l_neg:
```
```   129      "x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<oplus> x = \<zero>"
```
```   130 by (simp add: a_inv_def
```
```   131      group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]])
```
```   132
```
```   133 lemma (in abelian_monoid) a_comm:
```
```   134      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
```
```   135 by (rule comm_monoid.m_comm [OF a_comm_monoid,
```
```   136     simplified, simplified ring_add_def [symmetric]])
```
```   137
```
```   138 lemma (in abelian_monoid) a_lcomm:
```
```   139      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
```
```   140       \<Longrightarrow> x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
```
```   141 by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
```
```   142     simplified, simplified ring_add_def [symmetric]])
```
```   143
```
```   144 lemma (in abelian_monoid) r_zero [simp]:
```
```   145      "x \<in> carrier(G) \<Longrightarrow> x \<oplus> \<zero> = x"
```
```   146   using monoid.r_one [OF a_monoid]
```
```   147   by (simp add: ring_add_def [symmetric])
```
```   148
```
```   149 lemma (in abelian_group) r_neg:
```
```   150      "x \<in> carrier(G) \<Longrightarrow> x \<oplus> (\<ominus> x) = \<zero>"
```
```   151   using group.r_inv [OF a_group]
```
```   152   by (simp add: a_inv_def ring_add_def [symmetric])
```
```   153
```
```   154 lemma (in abelian_group) minus_zero [simp]:
```
```   155      "\<ominus> \<zero> = \<zero>"
```
```   156   by (simp add: a_inv_def
```
```   157     group.inv_one [OF a_group, simplified ])
```
```   158
```
```   159 lemma (in abelian_group) minus_minus [simp]:
```
```   160      "x \<in> carrier(G) \<Longrightarrow> \<ominus> (\<ominus> x) = x"
```
```   161   using group.inv_inv [OF a_group, simplified]
```
```   162   by (simp add: a_inv_def)
```
```   163
```
```   164 lemma (in abelian_group) minus_add:
```
```   165      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
```
```   166   using comm_group.inv_mult [OF a_comm_group]
```
```   167   by (simp add: a_inv_def ring_add_def [symmetric])
```
```   168
```
```   169 lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
```
```   170
```
```   171 text {*
```
```   172   The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
```
```   173 *}
```
```   174
```
```   175 context ring
```
```   176 begin
```
```   177
```
```   178 lemma l_null [simp]: "x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"
```
```   179 proof -
```
```   180   assume R: "x \<in> carrier(R)"
```
```   181   then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
```
```   182     by (blast intro: l_distr [THEN sym])
```
```   183   also from R have "... = \<zero> \<cdot> x \<oplus> \<zero>" by simp
```
```   184   finally have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = \<zero> \<cdot> x \<oplus> \<zero>" .
```
```   185   with R show ?thesis by (simp del: r_zero)
```
```   186 qed
```
```   187
```
```   188 lemma r_null [simp]: "x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>"
```
```   189 proof -
```
```   190   assume R: "x \<in> carrier(R)"
```
```   191   then have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> (\<zero> \<oplus> \<zero>)"
```
```   192     by (simp add: r_distr del: l_zero r_zero)
```
```   193   also from R have "... = x \<cdot> \<zero> \<oplus> \<zero>" by simp
```
```   194   finally have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> \<zero> \<oplus> \<zero>" .
```
```   195   with R show ?thesis by (simp del: r_zero)
```
```   196 qed
```
```   197
```
```   198 lemma l_minus:
```
```   199   "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> \<ominus> x \<cdot> y = \<ominus> (x \<cdot> y)"
```
```   200 proof -
```
```   201   assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
```
```   202   then have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = (\<ominus> x \<oplus> x) \<cdot> y" by (simp add: l_distr)
```
```   203   also from R have "... = \<zero>" by (simp add: l_neg l_null)
```
```   204   finally have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = \<zero>" .
```
```   205   with R have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
```
```   206   with R show ?thesis by (simp add: a_assoc r_neg)
```
```   207 qed
```
```   208
```
```   209 lemma r_minus:
```
```   210   "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<cdot> \<ominus> y = \<ominus> (x \<cdot> y)"
```
```   211 proof -
```
```   212   assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
```
```   213   then have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = x \<cdot> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
```
```   214   also from R have "... = \<zero>" by (simp add: l_neg r_null)
```
```   215   finally have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = \<zero>" .
```
```   216   with R have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
```
```   217   with R show ?thesis by (simp add: a_assoc r_neg)
```
```   218 qed
```
```   219
```
```   220 lemma minus_eq:
```
```   221   "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> \<ominus> y"
```
```   222   by (simp only: minus_def)
```
```   223
```
```   224 end
```
```   225
```
```   226
```
```   227 subsection {* Morphisms *}
```
```   228
```
```   229 definition
```
```   230   ring_hom :: "[i,i] => i" where
```
```   231   "ring_hom(R,S) ==
```
```   232     {h \<in> carrier(R) -> carrier(S).
```
```   233       (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) -->
```
```   234         h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
```
```   235         h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) &
```
```   236       h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
```
```   237
```
```   238 lemma ring_hom_memI:
```
```   239   assumes hom_type: "h \<in> carrier(R) \<rightarrow> carrier(S)"
```
```   240     and hom_mult: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow>
```
```   241       h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
```
```   242     and hom_add: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow>
```
```   243       h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
```
```   244     and hom_one: "h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
```
```   245   shows "h \<in> ring_hom(R,S)"
```
```   246 by (auto simp add: ring_hom_def prems)
```
```   247
```
```   248 lemma ring_hom_closed:
```
```   249      "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(S)"
```
```   250 by (auto simp add: ring_hom_def)
```
```   251
```
```   252 lemma ring_hom_mult:
```
```   253      "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
```
```   254       \<Longrightarrow> h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
```
```   255 by (simp add: ring_hom_def)
```
```   256
```
```   257 lemma ring_hom_add:
```
```   258      "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
```
```   259       \<Longrightarrow> h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
```
```   260 by (simp add: ring_hom_def)
```
```   261
```
```   262 lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
```
```   263 by (simp add: ring_hom_def)
```
```   264
```
```   265 locale ring_hom_cring = R: cring R + S: cring S
```
```   266   for R (structure) and S (structure) and h +
```
```   267   assumes homh [simp, intro]: "h \<in> ring_hom(R,S)"
```
```   268   notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
```
```   269     and hom_mult [simp] = ring_hom_mult [OF homh]
```
```   270     and hom_add [simp] = ring_hom_add [OF homh]
```
```   271     and hom_one [simp] = ring_hom_one [OF homh]
```
```   272
```
```   273 lemma (in ring_hom_cring) hom_zero [simp]:
```
```   274      "h ` \<zero>\<^bsub>R\<^esub> = \<zero>\<^bsub>S\<^esub>"
```
```   275 proof -
```
```   276   have "h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> h ` \<zero> = h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> \<zero>\<^bsub>S\<^esub>"
```
```   277     by (simp add: hom_add [symmetric] del: hom_add)
```
```   278   then show ?thesis by (simp del: S.r_zero)
```
```   279 qed
```
```   280
```
```   281 lemma (in ring_hom_cring) hom_a_inv [simp]:
```
```   282      "x \<in> carrier(R) \<Longrightarrow> h ` (\<ominus>\<^bsub>R\<^esub> x) = \<ominus>\<^bsub>S\<^esub> h ` x"
```
```   283 proof -
```
```   284   assume R: "x \<in> carrier(R)"
```
```   285   then have "h ` x \<oplus>\<^bsub>S\<^esub> h ` (\<ominus> x) = h ` x \<oplus>\<^bsub>S\<^esub> (\<ominus>\<^bsub>S\<^esub> (h ` x))"
```
```   286     by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
```
```   287   with R show ?thesis by simp
```
```   288 qed
```
```   289
```
```   290 lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) \<in> ring_hom(R,R)"
```
```   291 apply (rule ring_hom_memI)
```
```   292 apply (auto simp add: id_type)
```
```   293 done
```
```   294
```
```   295 end
```