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