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