src/HOL/Algebra/IntRing.thy
 author ballarin Tue Jul 24 15:29:57 2007 +0200 (2007-07-24) changeset 23957 54fab60ddc97 parent 22063 717425609192 child 24131 1099f6c73649 permissions -rw-r--r--
Interpretation of rings (as integers) maps defined operations to defined
operations..
```     1 (*
```
```     2   Title:     HOL/Algebra/IntRing.thy
```
```     3   Id:        \$Id\$
```
```     4   Author:    Stephan Hohe, TU Muenchen
```
```     5 *)
```
```     6
```
```     7 theory IntRing
```
```     8 imports QuotRing IntDef
```
```     9 begin
```
```    10
```
```    11
```
```    12 section {* The Ring of Integers *}
```
```    13
```
```    14 subsection {* Some properties of @{typ int} *}
```
```    15
```
```    16 lemma dvds_imp_abseq:
```
```    17   "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)"
```
```    18 apply (subst abs_split, rule conjI)
```
```    19  apply (clarsimp, subst abs_split, rule conjI)
```
```    20   apply (clarsimp)
```
```    21   apply (cases "k=0", simp)
```
```    22   apply (cases "l=0", simp)
```
```    23   apply (simp add: zdvd_anti_sym)
```
```    24  apply clarsimp
```
```    25  apply (cases "k=0", simp)
```
```    26  apply (simp add: zdvd_anti_sym)
```
```    27 apply (clarsimp, subst abs_split, rule conjI)
```
```    28  apply (clarsimp)
```
```    29  apply (cases "l=0", simp)
```
```    30  apply (simp add: zdvd_anti_sym)
```
```    31 apply (clarsimp)
```
```    32 apply (subgoal_tac "-l = -k", simp)
```
```    33 apply (intro zdvd_anti_sym, simp+)
```
```    34 done
```
```    35
```
```    36 lemma abseq_imp_dvd:
```
```    37   assumes a_lk: "abs l = abs (k::int)"
```
```    38   shows "l dvd k"
```
```    39 proof -
```
```    40   from a_lk
```
```    41       have "nat (abs l) = nat (abs k)" by simp
```
```    42   hence "nat (abs l) dvd nat (abs k)" by simp
```
```    43   hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff)
```
```    44   hence "abs l dvd k" by simp
```
```    45   thus "l dvd k"
```
```    46   apply (unfold dvd_def, cases "l<0")
```
```    47    defer 1 apply clarsimp
```
```    48   proof (clarsimp)
```
```    49     fix k
```
```    50     assume l0: "l < 0"
```
```    51     have "- (l * k) = l * (-k)" by simp
```
```    52     thus "\<exists>ka. - (l * k) = l * ka" by fast
```
```    53   qed
```
```    54 qed
```
```    55
```
```    56 lemma dvds_eq_abseq:
```
```    57   "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
```
```    58 apply rule
```
```    59  apply (simp add: dvds_imp_abseq)
```
```    60 apply (rule conjI)
```
```    61  apply (simp add: abseq_imp_dvd)+
```
```    62 done
```
```    63
```
```    64
```
```    65
```
```    66 subsection {* The Set of Integers as Algebraic Structure *}
```
```    67
```
```    68 subsubsection {* Definition of @{text "\<Z>"} *}
```
```    69
```
```    70 constdefs
```
```    71   int_ring :: "int ring" ("\<Z>")
```
```    72   "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
```
```    73
```
```    74 lemma int_Zcarr [intro!, simp]:
```
```    75   "k \<in> carrier \<Z>"
```
```    76   by (simp add: int_ring_def)
```
```    77
```
```    78 lemma int_is_cring:
```
```    79   "cring \<Z>"
```
```    80 unfolding int_ring_def
```
```    81 apply (rule cringI)
```
```    82   apply (rule abelian_groupI, simp_all)
```
```    83   defer 1
```
```    84   apply (rule comm_monoidI, simp_all)
```
```    85  apply (rule zadd_zmult_distrib)
```
```    86 apply (fast intro: zadd_zminus_inverse2)
```
```    87 done
```
```    88
```
```    89 (*
```
```    90 lemma int_is_domain:
```
```    91   "domain \<Z>"
```
```    92 apply (intro domain.intro domain_axioms.intro)
```
```    93   apply (rule int_is_cring)
```
```    94  apply (unfold int_ring_def, simp+)
```
```    95 done
```
```    96 *)
```
```    97 subsubsection {* Interpretations *}
```
```    98
```
```    99 text {* Since definitions of derived operations are global, their
```
```   100   interpretation needs to be done as early as possible --- that is,
```
```   101   with as few assumptions as possible. *}
```
```   102
```
```   103 interpretation int: monoid ["\<Z>"]
```
```   104   where "carrier \<Z> = UNIV"
```
```   105     and "mult \<Z> x y = x * y"
```
```   106     and "one \<Z> = 1"
```
```   107     and "pow \<Z> x n = x^n"
```
```   108 proof -
```
```   109   -- "Specification"
```
```   110   show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
```
```   111   then interpret int: monoid ["\<Z>"] .
```
```   112
```
```   113   -- "Carrier"
```
```   114   show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
```
```   115
```
```   116   -- "Operations"
```
```   117   { fix x y show "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
```
```   118   note mult = this
```
```   119   show one: "one \<Z> = 1" by (simp add: int_ring_def)
```
```   120   show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
```
```   121 qed
```
```   122
```
```   123 interpretation int: comm_monoid ["\<Z>"]
```
```   124   where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
```
```   125 proof -
```
```   126   -- "Specification"
```
```   127   show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
```
```   128   then interpret int: comm_monoid ["\<Z>"] .
```
```   129
```
```   130   -- "Operations"
```
```   131   { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
```
```   132   note mult = this
```
```   133   have one: "one \<Z> = 1" by (simp add: int_ring_def)
```
```   134   show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
```
```   135   proof (cases "finite A")
```
```   136     case True then show ?thesis proof induct
```
```   137       case empty show ?case by (simp add: one)
```
```   138     next
```
```   139       case insert then show ?case by (simp add: Pi_def mult)
```
```   140     qed
```
```   141   next
```
```   142     case False then show ?thesis by (simp add: finprod_def)
```
```   143   qed
```
```   144 qed
```
```   145
```
```   146 interpretation int: abelian_monoid ["\<Z>"]
```
```   147   where "zero \<Z> = 0"
```
```   148     and "add \<Z> x y = x + y"
```
```   149     and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
```
```   150 proof -
```
```   151   -- "Specification"
```
```   152   show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
```
```   153   then interpret int: abelian_monoid ["\<Z>"] .
```
```   154
```
```   155   -- "Operations"
```
```   156   { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
```
```   157   note add = this
```
```   158   show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
```
```   159   show "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
```
```   160   proof (cases "finite A")
```
```   161     case True then show ?thesis proof induct
```
```   162       case empty show ?case by (simp add: zero)
```
```   163     next
```
```   164       case insert then show ?case by (simp add: Pi_def add)
```
```   165     qed
```
```   166   next
```
```   167     case False then show ?thesis by (simp add: finsum_def finprod_def)
```
```   168   qed
```
```   169 qed
```
```   170
```
```   171 interpretation int: abelian_group ["\<Z>"]
```
```   172   where "a_inv \<Z> x = - x"
```
```   173     and "a_minus \<Z> x y = x - y"
```
```   174 proof -
```
```   175   -- "Specification"
```
```   176   show "abelian_group \<Z>"
```
```   177   proof (rule abelian_groupI)
```
```   178     show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
```
```   179       by (simp add: int_ring_def) arith
```
```   180   qed (auto simp: int_ring_def)
```
```   181   then interpret int: abelian_group ["\<Z>"] .
```
```   182
```
```   183   -- "Operations"
```
```   184   { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
```
```   185   note add = this
```
```   186   have zero: "zero \<Z> = 0" by (simp add: int_ring_def)
```
```   187   { fix x
```
```   188     have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero)
```
```   189     then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) }
```
```   190   note a_inv = this
```
```   191   show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
```
```   192 qed
```
```   193
```
```   194 interpretation int: "domain" ["\<Z>"]
```
```   195   by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
```
```   196
```
```   197
```
```   198 interpretation int: partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
```
```   199   where "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
```
```   200 proof -
```
```   201   show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
```
```   202     by unfold_locales simp_all
```
```   203   show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
```
```   204     by (simp add: lless_def) auto
```
```   205 qed
```
```   206
```
```   207 interpretation int: lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
```
```   208   where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
```
```   209     and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
```
```   210 proof -
```
```   211   let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)"
```
```   212   show "lattice ?Z"
```
```   213     apply unfold_locales
```
```   214     apply (simp add: least_def Upper_def)
```
```   215     apply arith
```
```   216     apply (simp add: greatest_def Lower_def)
```
```   217     apply arith
```
```   218     done
```
```   219   then interpret int: lattice ["?Z"] .
```
```   220   show "join ?Z x y = max x y"
```
```   221     apply (rule int.joinI)
```
```   222     apply (simp_all add: least_def Upper_def)
```
```   223     apply arith
```
```   224     done
```
```   225   show "meet ?Z x y = min x y"
```
```   226     apply (rule int.meetI)
```
```   227     apply (simp_all add: greatest_def Lower_def)
```
```   228     apply arith
```
```   229     done
```
```   230 qed
```
```   231
```
```   232 interpretation int: total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
```
```   233   by unfold_locales clarsimp
```
```   234
```
```   235 (*
```
```   236 lemma int_le_total_order:
```
```   237   "total_order (| carrier = UNIV::int set, le = op \<le> |)"
```
```   238   apply (rule partial_order.total_orderI)
```
```   239    apply (rule partial_order.intro, simp+)
```
```   240   apply clarsimp
```
```   241   done
```
```   242
```
```   243 lemma less_int:
```
```   244   "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
```
```   245   by (auto simp add: expand_fun_eq lless_def)
```
```   246
```
```   247 lemma join_int:
```
```   248   "join (| carrier = UNIV::int set, le = op \<le> |) = max"
```
```   249   apply (simp add: expand_fun_eq max_def)
```
```   250   apply (rule+)
```
```   251   apply (rule lattice.joinI)
```
```   252   apply (simp add: int_le_total_order total_order.axioms)
```
```   253   apply (simp add: least_def Upper_def)
```
```   254   apply arith
```
```   255   apply simp apply simp
```
```   256   apply (rule lattice.joinI)
```
```   257   apply (simp add: int_le_total_order total_order.axioms)
```
```   258   apply (simp add: least_def Upper_def)
```
```   259   apply arith
```
```   260   apply simp apply simp
```
```   261   done
```
```   262
```
```   263 lemma meet_int:
```
```   264   "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
```
```   265   apply (simp add: expand_fun_eq min_def)
```
```   266   apply (rule+)
```
```   267   apply (rule lattice.meetI)
```
```   268   apply (simp add: int_le_total_order total_order.axioms)
```
```   269   apply (simp add: greatest_def Lower_def)
```
```   270   apply arith
```
```   271   apply simp apply simp
```
```   272   apply (rule lattice.meetI)
```
```   273   apply (simp add: int_le_total_order total_order.axioms)
```
```   274   apply (simp add: greatest_def Lower_def)
```
```   275   apply arith
```
```   276   apply simp apply simp
```
```   277   done
```
```   278
```
```   279 lemma carrier_int:
```
```   280   "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
```
```   281   apply simp
```
```   282   done
```
```   283
```
```   284 text {* Interpretation unfolding @{text lless}, @{text join} and @{text
```
```   285   meet} since they have natural representations in @{typ int}. *}
```
```   286
```
```   287 interpretation
```
```   288   int [unfolded less_int join_int meet_int carrier_int]:
```
```   289   total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
```
```   290   by (rule int_le_total_order)
```
```   291 *)
```
```   292
```
```   293
```
```   294 subsubsection {* Generated Ideals of @{text "\<Z>"} *}
```
```   295
```
```   296 lemma int_Idl:
```
```   297   "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
```
```   298   apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)
```
```   299   apply (simp add: cgenideal_def int_ring_def)
```
```   300   done
```
```   301
```
```   302 lemma multiples_principalideal:
```
```   303   "principalideal {x * a | x. True } \<Z>"
```
```   304 apply (subst int_Idl[symmetric], rule principalidealI)
```
```   305  apply (rule int.genideal_ideal, simp)
```
```   306 apply fast
```
```   307 done
```
```   308
```
```   309 lemma prime_primeideal:
```
```   310   assumes prime: "prime (nat p)"
```
```   311   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
```
```   312 apply (rule primeidealI)
```
```   313    apply (rule int.genideal_ideal, simp)
```
```   314   apply (rule int_is_cring)
```
```   315  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
```
```   316  apply (simp add: int_ring_def)
```
```   317  apply clarsimp defer 1
```
```   318  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
```
```   319  apply (simp add: int_ring_def)
```
```   320  apply (elim exE)
```
```   321 proof -
```
```   322   fix a b x
```
```   323
```
```   324   from prime
```
```   325       have ppos: "0 <= p" by (simp add: prime_def)
```
```   326   have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
```
```   327   proof -
```
```   328     fix x
```
```   329     assume "nat p dvd nat (abs x)"
```
```   330     hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
```
```   331     thus "p dvd x" by (simp add: ppos)
```
```   332   qed
```
```   333
```
```   334
```
```   335   assume "a * b = x * p"
```
```   336   hence "p dvd a * b" by simp
```
```   337   hence "nat p dvd nat (abs (a * b))"
```
```   338   apply (subst nat_dvd_iff, clarsimp)
```
```   339   apply (rule conjI, clarsimp, simp add: zabs_def)
```
```   340   proof (clarsimp)
```
```   341     assume a: " ~ 0 <= p"
```
```   342     from prime
```
```   343         have "0 < p" by (simp add: prime_def)
```
```   344     from a and this
```
```   345         have "False" by simp
```
```   346     thus "nat (abs (a * b)) = 0" ..
```
```   347   qed
```
```   348   hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
```
```   349   hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
```
```   350   hence "p dvd a | p dvd b" by (fast intro: unnat)
```
```   351   thus "(EX x. a = x * p) | (EX x. b = x * p)"
```
```   352   proof
```
```   353     assume "p dvd a"
```
```   354     hence "EX x. a = p * x" by (simp add: dvd_def)
```
```   355     from this obtain x
```
```   356         where "a = p * x" by fast
```
```   357     hence "a = x * p" by simp
```
```   358     hence "EX x. a = x * p" by simp
```
```   359     thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
```
```   360   next
```
```   361     assume "p dvd b"
```
```   362     hence "EX x. b = p * x" by (simp add: dvd_def)
```
```   363     from this obtain x
```
```   364         where "b = p * x" by fast
```
```   365     hence "b = x * p" by simp
```
```   366     hence "EX x. b = x * p" by simp
```
```   367     thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
```
```   368   qed
```
```   369 next
```
```   370   assume "UNIV = {uu. EX x. uu = x * p}"
```
```   371   from this obtain x
```
```   372       where "1 = x * p" by fast
```
```   373   from this [symmetric]
```
```   374       have "p * x = 1" by (subst zmult_commute)
```
```   375   hence "\<bar>p * x\<bar> = 1" by simp
```
```   376   hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
```
```   377   from this and prime
```
```   378       show "False" by (simp add: prime_def)
```
```   379 qed
```
```   380
```
```   381
```
```   382 subsubsection {* Ideals and Divisibility *}
```
```   383
```
```   384 lemma int_Idl_subset_ideal:
```
```   385   "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
```
```   386 by (rule int.Idl_subset_ideal', simp+)
```
```   387
```
```   388 lemma Idl_subset_eq_dvd:
```
```   389   "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
```
```   390 apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
```
```   391 apply (rule, clarify)
```
```   392 apply (simp add: dvd_def, clarify)
```
```   393 apply (simp add: int.m_comm)
```
```   394 done
```
```   395
```
```   396 lemma dvds_eq_Idl:
```
```   397   "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
```
```   398 proof -
```
```   399   have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric])
```
```   400   have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric])
```
```   401
```
```   402   have "(l dvd k \<and> k dvd l) = ((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k}))"
```
```   403   by (subst a, subst b, simp)
```
```   404   also have "((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})" by (rule, fast+)
```
```   405   finally
```
```   406     show ?thesis .
```
```   407 qed
```
```   408
```
```   409 lemma Idl_eq_abs:
```
```   410   "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)"
```
```   411 apply (subst dvds_eq_abseq[symmetric])
```
```   412 apply (rule dvds_eq_Idl[symmetric])
```
```   413 done
```
```   414
```
```   415
```
```   416 subsubsection {* Ideals and the Modulus *}
```
```   417
```
```   418 constdefs
```
```   419    ZMod :: "int => int => int set"
```
```   420   "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
```
```   421
```
```   422 lemmas ZMod_defs =
```
```   423   ZMod_def genideal_def
```
```   424
```
```   425 lemma rcos_zfact:
```
```   426   assumes kIl: "k \<in> ZMod l r"
```
```   427   shows "EX x. k = x * l + r"
```
```   428 proof -
```
```   429   from kIl[unfolded ZMod_def]
```
```   430       have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def)
```
```   431   from this obtain xl
```
```   432       where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
```
```   433       and k: "k = xl + r"
```
```   434       by auto
```
```   435   from xl obtain x
```
```   436       where "xl = x * l"
```
```   437       by (simp add: int_Idl, fast)
```
```   438   from k and this
```
```   439       have "k = x * l + r" by simp
```
```   440   thus "\<exists>x. k = x * l + r" ..
```
```   441 qed
```
```   442
```
```   443 lemma ZMod_imp_zmod:
```
```   444   assumes zmods: "ZMod m a = ZMod m b"
```
```   445   shows "a mod m = b mod m"
```
```   446 proof -
```
```   447   interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
```
```   448   from zmods
```
```   449       have "b \<in> ZMod m a"
```
```   450       unfolding ZMod_def
```
```   451       by (simp add: a_repr_independenceD)
```
```   452   from this
```
```   453       have "EX x. b = x * m + a" by (rule rcos_zfact)
```
```   454   from this obtain x
```
```   455       where "b = x * m + a"
```
```   456       by fast
```
```   457
```
```   458   hence "b mod m = (x * m + a) mod m" by simp
```
```   459   also
```
```   460       have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
```
```   461   also
```
```   462       have "\<dots> = a mod m" by simp
```
```   463   finally
```
```   464       have "b mod m = a mod m" .
```
```   465   thus "a mod m = b mod m" ..
```
```   466 qed
```
```   467
```
```   468 lemma ZMod_mod:
```
```   469   shows "ZMod m a = ZMod m (a mod m)"
```
```   470 proof -
```
```   471   interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
```
```   472   show ?thesis
```
```   473       unfolding ZMod_def
```
```   474   apply (rule a_repr_independence'[symmetric])
```
```   475   apply (simp add: int_Idl a_r_coset_defs)
```
```   476   apply (simp add: int_ring_def)
```
```   477   proof -
```
```   478     have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
```
```   479     hence "a = (a div m) * m + (a mod m)" by simp
```
```   480     thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast
```
```   481   qed simp
```
```   482 qed
```
```   483
```
```   484 lemma zmod_imp_ZMod:
```
```   485   assumes modeq: "a mod m = b mod m"
```
```   486   shows "ZMod m a = ZMod m b"
```
```   487 proof -
```
```   488   have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod)
```
```   489   also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
```
```   490   also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
```
```   491   finally show ?thesis .
```
```   492 qed
```
```   493
```
```   494 corollary ZMod_eq_mod:
```
```   495   shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
```
```   496 by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
```
```   497
```
```   498
```
```   499 subsubsection {* Factorization *}
```
```   500
```
```   501 constdefs
```
```   502   ZFact :: "int \<Rightarrow> int set ring"
```
```   503   "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
```
```   504
```
```   505 lemmas ZFact_defs = ZFact_def FactRing_def
```
```   506
```
```   507 lemma ZFact_is_cring:
```
```   508   shows "cring (ZFact k)"
```
```   509 apply (unfold ZFact_def)
```
```   510 apply (rule ideal.quotient_is_cring)
```
```   511  apply (intro ring.genideal_ideal)
```
```   512   apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
```
```   513  apply simp
```
```   514 apply (rule int_is_cring)
```
```   515 done
```
```   516
```
```   517 lemma ZFact_zero:
```
```   518   "carrier (ZFact 0) = (\<Union>a. {{a}})"
```
```   519 apply (insert int.genideal_zero)
```
```   520 apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
```
```   521 done
```
```   522
```
```   523 lemma ZFact_one:
```
```   524   "carrier (ZFact 1) = {UNIV}"
```
```   525 apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
```
```   526 apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps])
```
```   527 apply (rule, rule, clarsimp)
```
```   528  apply (rule, rule, clarsimp)
```
```   529  apply (rule, clarsimp, arith)
```
```   530 apply (rule, clarsimp)
```
```   531 apply (rule exI[of _ "0"], clarsimp)
```
```   532 done
```
```   533
```
```   534 lemma ZFact_prime_is_domain:
```
```   535   assumes pprime: "prime (nat p)"
```
```   536   shows "domain (ZFact p)"
```
```   537 apply (unfold ZFact_def)
```
```   538 apply (rule primeideal.quotient_is_domain)
```
```   539 apply (rule prime_primeideal[OF pprime])
```
```   540 done
```
```   541
```
```   542 end
```