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