src/HOL/Algebra/IntRing.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 22063 717425609192
child 23957 54fab60ddc97
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
ballarin@20318
     1
(*
ballarin@20318
     2
  Title:     HOL/Algebra/IntRing.thy
ballarin@20318
     3
  Id:        $Id$
ballarin@20318
     4
  Author:    Stephan Hohe, TU Muenchen
ballarin@20318
     5
*)
ballarin@20318
     6
ballarin@20318
     7
theory IntRing
ballarin@20318
     8
imports QuotRing IntDef
ballarin@20318
     9
begin
ballarin@20318
    10
ballarin@20318
    11
ballarin@20318
    12
section {* The Ring of Integers *}
ballarin@20318
    13
ballarin@20318
    14
subsection {* Some properties of @{typ int} *}
ballarin@20318
    15
ballarin@20318
    16
lemma dvds_imp_abseq:
ballarin@20318
    17
  "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)"
ballarin@20318
    18
apply (subst abs_split, rule conjI)
ballarin@20318
    19
 apply (clarsimp, subst abs_split, rule conjI)
ballarin@20318
    20
  apply (clarsimp)
ballarin@20318
    21
  apply (cases "k=0", simp)
ballarin@20318
    22
  apply (cases "l=0", simp)
ballarin@20318
    23
  apply (simp add: zdvd_anti_sym)
ballarin@20318
    24
 apply clarsimp
ballarin@20318
    25
 apply (cases "k=0", simp)
ballarin@20318
    26
 apply (simp add: zdvd_anti_sym)
ballarin@20318
    27
apply (clarsimp, subst abs_split, rule conjI)
ballarin@20318
    28
 apply (clarsimp)
ballarin@20318
    29
 apply (cases "l=0", simp)
ballarin@20318
    30
 apply (simp add: zdvd_anti_sym)
ballarin@20318
    31
apply (clarsimp)
ballarin@20318
    32
apply (subgoal_tac "-l = -k", simp)
ballarin@20318
    33
apply (intro zdvd_anti_sym, simp+)
ballarin@20318
    34
done
ballarin@20318
    35
ballarin@20318
    36
lemma abseq_imp_dvd:
ballarin@20318
    37
  assumes a_lk: "abs l = abs (k::int)"
ballarin@20318
    38
  shows "l dvd k"
ballarin@20318
    39
proof -
ballarin@20318
    40
  from a_lk
ballarin@20318
    41
      have "nat (abs l) = nat (abs k)" by simp
ballarin@20318
    42
  hence "nat (abs l) dvd nat (abs k)" by simp
ballarin@20318
    43
  hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff)
ballarin@20318
    44
  hence "abs l dvd k" by simp
ballarin@20318
    45
  thus "l dvd k" 
ballarin@20318
    46
  apply (unfold dvd_def, cases "l<0")
ballarin@20318
    47
   defer 1 apply clarsimp
ballarin@20318
    48
  proof (clarsimp)
ballarin@20318
    49
    fix k
ballarin@20318
    50
    assume l0: "l < 0"
ballarin@20318
    51
    have "- (l * k) = l * (-k)" by simp
ballarin@20318
    52
    thus "\<exists>ka. - (l * k) = l * ka" by fast
ballarin@20318
    53
  qed
ballarin@20318
    54
qed
ballarin@20318
    55
ballarin@20318
    56
lemma dvds_eq_abseq:
ballarin@20318
    57
  "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
ballarin@20318
    58
apply rule
ballarin@20318
    59
 apply (simp add: dvds_imp_abseq)
ballarin@20318
    60
apply (rule conjI)
ballarin@20318
    61
 apply (simp add: abseq_imp_dvd)+
ballarin@20318
    62
done
ballarin@20318
    63
ballarin@20318
    64
ballarin@20318
    65
ballarin@20318
    66
subsection {* The Set of Integers as Algebraic Structure *}
ballarin@20318
    67
ballarin@20318
    68
subsubsection {* Definition of @{text "\<Z>"} *}
ballarin@20318
    69
ballarin@20318
    70
constdefs
ballarin@20318
    71
  int_ring :: "int ring" ("\<Z>")
ballarin@20318
    72
  "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
ballarin@20318
    73
ballarin@20318
    74
lemma int_Zcarr[simp,intro!]:
ballarin@20318
    75
  "k \<in> carrier \<Z>"
ballarin@20318
    76
by (simp add: int_ring_def)
ballarin@20318
    77
ballarin@20318
    78
lemma int_is_cring:
ballarin@20318
    79
  "cring \<Z>"
ballarin@20318
    80
unfolding int_ring_def
ballarin@20318
    81
apply (rule cringI)
ballarin@20318
    82
  apply (rule abelian_groupI, simp_all)
ballarin@20318
    83
  defer 1
ballarin@20318
    84
  apply (rule comm_monoidI, simp_all)
ballarin@20318
    85
 apply (rule zadd_zmult_distrib)
ballarin@20318
    86
apply (fast intro: zadd_zminus_inverse2)
ballarin@20318
    87
done
ballarin@20318
    88
ballarin@20318
    89
lemma int_is_domain:
ballarin@20318
    90
  "domain \<Z>"
ballarin@20318
    91
apply (intro domain.intro domain_axioms.intro)
ballarin@20318
    92
  apply (rule int_is_cring)
ballarin@20318
    93
 apply (unfold int_ring_def, simp+)
ballarin@20318
    94
done
ballarin@20318
    95
ballarin@20318
    96
interpretation "domain" ["\<Z>"] by (rule int_is_domain)
ballarin@20318
    97
ballarin@20318
    98
lemma int_le_total_order:
ballarin@22063
    99
  "total_order (| carrier = UNIV::int set, le = op \<le> |)"
ballarin@22063
   100
  apply (rule partial_order.total_orderI)
ballarin@22063
   101
   apply (rule partial_order.intro, simp+)
ballarin@22063
   102
  apply clarsimp
ballarin@22063
   103
  done
ballarin@20318
   104
ballarin@21896
   105
lemma less_int:
ballarin@22063
   106
  "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
ballarin@22063
   107
  by (auto simp add: expand_fun_eq lless_def)
ballarin@21896
   108
ballarin@21896
   109
lemma join_int:
ballarin@22063
   110
  "join (| carrier = UNIV::int set, le = op \<le> |) = max"
ballarin@21896
   111
  apply (simp add: expand_fun_eq max_def)
ballarin@21896
   112
  apply (rule+)
ballarin@21896
   113
  apply (rule lattice.joinI)
ballarin@21896
   114
  apply (simp add: int_le_total_order total_order.axioms)
ballarin@22063
   115
  apply (simp add: least_def Upper_def)
ballarin@21896
   116
  apply arith
ballarin@21896
   117
  apply simp apply simp
ballarin@21896
   118
  apply (rule lattice.joinI)
ballarin@21896
   119
  apply (simp add: int_le_total_order total_order.axioms)
ballarin@22063
   120
  apply (simp add: least_def Upper_def)
ballarin@21896
   121
  apply arith
ballarin@21896
   122
  apply simp apply simp
ballarin@21896
   123
  done
ballarin@21896
   124
ballarin@21896
   125
lemma meet_int:
ballarin@22063
   126
  "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
ballarin@21896
   127
  apply (simp add: expand_fun_eq min_def)
ballarin@21896
   128
  apply (rule+)
ballarin@21896
   129
  apply (rule lattice.meetI)
ballarin@21896
   130
  apply (simp add: int_le_total_order total_order.axioms)
ballarin@22063
   131
  apply (simp add: greatest_def Lower_def)
ballarin@21896
   132
  apply arith
ballarin@21896
   133
  apply simp apply simp
ballarin@21896
   134
  apply (rule lattice.meetI)
ballarin@21896
   135
  apply (simp add: int_le_total_order total_order.axioms)
ballarin@22063
   136
  apply (simp add: greatest_def Lower_def)
ballarin@21896
   137
  apply arith
ballarin@21896
   138
  apply simp apply simp
ballarin@21896
   139
  done
ballarin@21896
   140
ballarin@22063
   141
lemma carrier_int:
ballarin@22063
   142
  "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
ballarin@22063
   143
  apply simp
ballarin@22063
   144
  done
ballarin@22063
   145
ballarin@22063
   146
text {* Interpretation unfolding @{text lless}, @{text join} and @{text
ballarin@21896
   147
  meet} since they have natural representations in @{typ int}. *}
ballarin@21896
   148
ballarin@21896
   149
interpretation 
ballarin@22063
   150
  int [unfolded less_int join_int meet_int carrier_int]:
ballarin@22063
   151
  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
ballarin@22063
   152
  by (rule int_le_total_order)
ballarin@20318
   153
ballarin@20318
   154
ballarin@20318
   155
subsubsection {* Generated Ideals of @{text "\<Z>"} *}
ballarin@20318
   156
ballarin@20318
   157
lemma int_Idl:
ballarin@20318
   158
  "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
ballarin@20318
   159
apply (subst cgenideal_eq_genideal[symmetric], simp add: int_ring_def)
ballarin@20318
   160
apply (simp add: cgenideal_def int_ring_def)
ballarin@20318
   161
done
ballarin@20318
   162
ballarin@20318
   163
lemma multiples_principalideal:
ballarin@20318
   164
  "principalideal {x * a | x. True } \<Z>"
ballarin@20318
   165
apply (subst int_Idl[symmetric], rule principalidealI)
ballarin@20318
   166
 apply (rule genideal_ideal, simp)
ballarin@20318
   167
apply fast
ballarin@20318
   168
done
ballarin@20318
   169
ballarin@20318
   170
lemma prime_primeideal:
ballarin@20318
   171
  assumes prime: "prime (nat p)"
ballarin@20318
   172
  shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
ballarin@20318
   173
apply (rule primeidealI)
ballarin@20318
   174
   apply (rule genideal_ideal, simp)
ballarin@20318
   175
  apply (rule int_is_cring)
ballarin@20318
   176
 apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def)
ballarin@20318
   177
 apply (simp add: int_ring_def)
ballarin@20318
   178
 apply clarsimp defer 1
ballarin@20318
   179
 apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def)
ballarin@20318
   180
 apply (simp add: int_ring_def)
ballarin@20318
   181
 apply (elim exE)
ballarin@20318
   182
proof -
ballarin@20318
   183
  fix a b x
ballarin@20318
   184
ballarin@20318
   185
  from prime
ballarin@20318
   186
      have ppos: "0 <= p" by (simp add: prime_def)
ballarin@20318
   187
  have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
ballarin@20318
   188
  proof -
ballarin@20318
   189
    fix x
ballarin@20318
   190
    assume "nat p dvd nat (abs x)"
ballarin@20318
   191
    hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
ballarin@20318
   192
    thus "p dvd x" by (simp add: ppos)
ballarin@20318
   193
  qed
ballarin@20318
   194
ballarin@20318
   195
ballarin@20318
   196
  assume "a * b = x * p"
ballarin@20318
   197
  hence "p dvd a * b" by simp
ballarin@20318
   198
  hence "nat p dvd nat (abs (a * b))"
ballarin@20318
   199
  apply (subst nat_dvd_iff, clarsimp)
ballarin@20318
   200
  apply (rule conjI, clarsimp, simp add: zabs_def)
ballarin@20318
   201
  proof (clarsimp)
ballarin@20318
   202
    assume a: " ~ 0 <= p"
ballarin@20318
   203
    from prime
ballarin@20318
   204
        have "0 < p" by (simp add: prime_def)
ballarin@20318
   205
    from a and this
ballarin@20318
   206
        have "False" by simp
ballarin@20318
   207
    thus "nat (abs (a * b)) = 0" ..
ballarin@20318
   208
  qed
ballarin@20318
   209
  hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
ballarin@20318
   210
  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
ballarin@20318
   211
  hence "p dvd a | p dvd b" by (fast intro: unnat)
ballarin@20318
   212
  thus "(EX x. a = x * p) | (EX x. b = x * p)"
ballarin@20318
   213
  proof
ballarin@20318
   214
    assume "p dvd a"
ballarin@20318
   215
    hence "EX x. a = p * x" by (simp add: dvd_def)
ballarin@20318
   216
    from this obtain x
ballarin@20318
   217
        where "a = p * x" by fast
ballarin@20318
   218
    hence "a = x * p" by simp
ballarin@20318
   219
    hence "EX x. a = x * p" by simp
ballarin@20318
   220
    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
ballarin@20318
   221
  next
ballarin@20318
   222
    assume "p dvd b"
ballarin@20318
   223
    hence "EX x. b = p * x" by (simp add: dvd_def)
ballarin@20318
   224
    from this obtain x
ballarin@20318
   225
        where "b = p * x" by fast
ballarin@20318
   226
    hence "b = x * p" by simp
ballarin@20318
   227
    hence "EX x. b = x * p" by simp
ballarin@20318
   228
    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
ballarin@20318
   229
  qed
ballarin@20318
   230
next
ballarin@20318
   231
  assume "UNIV = {uu. EX x. uu = x * p}"
ballarin@20318
   232
  from this obtain x 
ballarin@20318
   233
      where "1 = x * p" by fast
ballarin@20318
   234
  from this [symmetric]
ballarin@20318
   235
      have "p * x = 1" by (subst zmult_commute)
ballarin@20318
   236
  hence "\<bar>p * x\<bar> = 1" by simp
ballarin@20318
   237
  hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
ballarin@20318
   238
  from this and prime
ballarin@20318
   239
      show "False" by (simp add: prime_def)
ballarin@20318
   240
qed
ballarin@20318
   241
ballarin@20318
   242
ballarin@20318
   243
subsubsection {* Ideals and Divisibility *}
ballarin@20318
   244
ballarin@20318
   245
lemma int_Idl_subset_ideal:
ballarin@20318
   246
  "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
ballarin@20318
   247
by (rule Idl_subset_ideal', simp+)
ballarin@20318
   248
ballarin@20318
   249
lemma Idl_subset_eq_dvd:
ballarin@20318
   250
  "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
ballarin@20318
   251
apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
ballarin@20318
   252
apply (rule, clarify)
ballarin@20318
   253
apply (simp add: dvd_def, clarify)
ballarin@20318
   254
apply (simp add: m_comm)
ballarin@20318
   255
done
ballarin@20318
   256
ballarin@20318
   257
lemma dvds_eq_Idl:
ballarin@20318
   258
  "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
ballarin@20318
   259
proof -
ballarin@20318
   260
  have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric])
ballarin@20318
   261
  have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric])
ballarin@20318
   262
ballarin@20318
   263
  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}))"
ballarin@20318
   264
  by (subst a, subst b, simp)
ballarin@20318
   265
  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+)
ballarin@20318
   266
  finally
ballarin@20318
   267
    show ?thesis .
ballarin@20318
   268
qed
ballarin@20318
   269
ballarin@20318
   270
lemma Idl_eq_abs:
ballarin@20318
   271
  "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)"
ballarin@20318
   272
apply (subst dvds_eq_abseq[symmetric])
ballarin@20318
   273
apply (rule dvds_eq_Idl[symmetric])
ballarin@20318
   274
done
ballarin@20318
   275
ballarin@20318
   276
ballarin@20318
   277
subsubsection {* Ideals and the Modulus *}
ballarin@20318
   278
ballarin@20318
   279
constdefs
ballarin@20318
   280
   ZMod :: "int => int => int set"
ballarin@20318
   281
  "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
ballarin@20318
   282
ballarin@20318
   283
lemmas ZMod_defs =
ballarin@20318
   284
  ZMod_def genideal_def
ballarin@20318
   285
ballarin@20318
   286
lemma rcos_zfact:
ballarin@20318
   287
  assumes kIl: "k \<in> ZMod l r"
ballarin@20318
   288
  shows "EX x. k = x * l + r"
ballarin@20318
   289
proof -
ballarin@20318
   290
  from kIl[unfolded ZMod_def]
ballarin@20318
   291
      have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def)
ballarin@20318
   292
  from this obtain xl
ballarin@20318
   293
      where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
ballarin@20318
   294
      and k: "k = xl + r"
ballarin@20318
   295
      by auto
ballarin@20318
   296
  from xl obtain x
ballarin@20318
   297
      where "xl = x * l"
ballarin@20318
   298
      by (simp add: int_Idl, fast)
ballarin@20318
   299
  from k and this
ballarin@20318
   300
      have "k = x * l + r" by simp
ballarin@20318
   301
  thus "\<exists>x. k = x * l + r" ..
ballarin@20318
   302
qed
ballarin@20318
   303
ballarin@20318
   304
lemma ZMod_imp_zmod:
ballarin@20318
   305
  assumes zmods: "ZMod m a = ZMod m b"
ballarin@20318
   306
  shows "a mod m = b mod m"
ballarin@20318
   307
proof -
ballarin@20318
   308
  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast)
ballarin@20318
   309
  from zmods
ballarin@20318
   310
      have "b \<in> ZMod m a"
ballarin@20318
   311
      unfolding ZMod_def
ballarin@20318
   312
      by (simp add: a_repr_independenceD)
ballarin@20318
   313
  from this
ballarin@20318
   314
      have "EX x. b = x * m + a" by (rule rcos_zfact)
ballarin@20318
   315
  from this obtain x
ballarin@20318
   316
      where "b = x * m + a"
ballarin@20318
   317
      by fast
ballarin@20318
   318
ballarin@20318
   319
  hence "b mod m = (x * m + a) mod m" by simp
ballarin@20318
   320
  also
ballarin@20318
   321
      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
ballarin@20318
   322
  also
ballarin@20318
   323
      have "\<dots> = a mod m" by simp
ballarin@20318
   324
  finally
ballarin@20318
   325
      have "b mod m = a mod m" .
ballarin@20318
   326
  thus "a mod m = b mod m" ..
ballarin@20318
   327
qed
ballarin@20318
   328
ballarin@20318
   329
lemma ZMod_mod:
ballarin@20318
   330
  shows "ZMod m a = ZMod m (a mod m)"
ballarin@20318
   331
proof -
ballarin@20318
   332
  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast)
ballarin@20318
   333
  show ?thesis
ballarin@20318
   334
      unfolding ZMod_def
ballarin@20318
   335
  apply (rule a_repr_independence'[symmetric])
ballarin@20318
   336
  apply (simp add: int_Idl a_r_coset_defs)
ballarin@20318
   337
  apply (simp add: int_ring_def)
ballarin@20318
   338
  proof -
ballarin@20318
   339
    have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
ballarin@20318
   340
    hence "a = (a div m) * m + (a mod m)" by simp
ballarin@20318
   341
    thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast
ballarin@20318
   342
  qed simp
ballarin@20318
   343
qed
ballarin@20318
   344
ballarin@20318
   345
lemma zmod_imp_ZMod:
ballarin@20318
   346
  assumes modeq: "a mod m = b mod m"
ballarin@20318
   347
  shows "ZMod m a = ZMod m b"
ballarin@20318
   348
proof -
ballarin@20318
   349
  have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod)
ballarin@20318
   350
  also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
ballarin@20318
   351
  also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
ballarin@20318
   352
  finally show ?thesis .
ballarin@20318
   353
qed
ballarin@20318
   354
ballarin@20318
   355
corollary ZMod_eq_mod:
ballarin@20318
   356
  shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
ballarin@20318
   357
by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
ballarin@20318
   358
ballarin@20318
   359
ballarin@20318
   360
subsubsection {* Factorization *}
ballarin@20318
   361
ballarin@20318
   362
constdefs
ballarin@20318
   363
  ZFact :: "int \<Rightarrow> int set ring"
ballarin@20318
   364
  "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
ballarin@20318
   365
ballarin@20318
   366
lemmas ZFact_defs = ZFact_def FactRing_def
ballarin@20318
   367
ballarin@20318
   368
lemma ZFact_is_cring:
ballarin@20318
   369
  shows "cring (ZFact k)"
ballarin@20318
   370
apply (unfold ZFact_def)
ballarin@20318
   371
apply (rule ideal.quotient_is_cring)
ballarin@20318
   372
 apply (intro ring.genideal_ideal)
ballarin@20318
   373
  apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
ballarin@20318
   374
 apply simp
ballarin@20318
   375
apply (rule int_is_cring)
ballarin@20318
   376
done
ballarin@20318
   377
ballarin@20318
   378
lemma ZFact_zero:
ballarin@20318
   379
  "carrier (ZFact 0) = (\<Union>a. {{a}})"
ballarin@20318
   380
apply (insert genideal_zero)
ballarin@20318
   381
apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
ballarin@20318
   382
done
ballarin@20318
   383
ballarin@20318
   384
lemma ZFact_one:
ballarin@20318
   385
  "carrier (ZFact 1) = {UNIV}"
ballarin@20318
   386
apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
ballarin@20318
   387
apply (subst genideal_one[unfolded int_ring_def, simplified ring_record_simps])
ballarin@20318
   388
apply (rule, rule, clarsimp)
ballarin@20318
   389
 apply (rule, rule, clarsimp)
ballarin@20318
   390
 apply (rule, clarsimp, arith)
ballarin@20318
   391
apply (rule, clarsimp)
ballarin@20318
   392
apply (rule exI[of _ "0"], clarsimp)
ballarin@20318
   393
done
ballarin@20318
   394
ballarin@20318
   395
lemma ZFact_prime_is_domain:
ballarin@20318
   396
  assumes pprime: "prime (nat p)"
ballarin@20318
   397
  shows "domain (ZFact p)"
ballarin@20318
   398
apply (unfold ZFact_def)
ballarin@20318
   399
apply (rule primeideal.quotient_is_domain)
ballarin@20318
   400
apply (rule prime_primeideal[OF pprime])
ballarin@20318
   401
done
ballarin@20318
   402
ballarin@20318
   403
end