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