src/HOL/Algebra/IntRing.thy
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (21 months ago)
changeset 67091 1393c2340eec
parent 67006 b1278ed3cd46
child 67118 ccab07d1196c
permissions -rw-r--r--
more symbols;
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
wenzelm@67006
     7
imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
ballarin@20318
     8
begin
ballarin@20318
     9
wenzelm@61382
    10
section \<open>The Ring of Integers\<close>
ballarin@20318
    11
wenzelm@61382
    12
subsection \<open>Some properties of @{typ int}\<close>
ballarin@20318
    13
ballarin@20318
    14
lemma dvds_eq_abseq:
wenzelm@55991
    15
  fixes k :: int
wenzelm@61945
    16
  shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
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
wenzelm@63167
    23
subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
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
wenzelm@61382
    50
subsection \<open>Interpretations\<close>
ballarin@20318
    51
wenzelm@61382
    52
text \<open>Since definitions of derived operations are global, their
ballarin@23957
    53
  interpretation needs to be done as early as possible --- that is,
wenzelm@61382
    54
  with as few assumptions as possible.\<close>
ballarin@23957
    55
wenzelm@30729
    56
interpretation int: monoid \<Z>
ballarin@61566
    57
  rewrites "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 -
wenzelm@63167
    62
  \<comment> "Specification"
wenzelm@61169
    63
  show "monoid \<Z>" by standard auto
wenzelm@30729
    64
  then interpret int: monoid \<Z> .
ballarin@23957
    65
wenzelm@63167
    66
  \<comment> "Carrier"
ballarin@41433
    67
  show "carrier \<Z> = UNIV" by simp
ballarin@23957
    68
wenzelm@63167
    69
  \<comment> "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>
nipkow@64272
    76
  rewrites "finprod \<Z> f A = prod f A"
ballarin@23957
    77
proof -
wenzelm@63167
    78
  \<comment> "Specification"
wenzelm@61169
    79
  show "comm_monoid \<Z>" by standard auto
wenzelm@30729
    80
  then interpret int: comm_monoid \<Z> .
ballarin@23957
    81
wenzelm@63167
    82
  \<comment> "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
nipkow@64272
    86
  show "finprod \<Z> f A = prod f A"
rene@60112
    87
    by (induct A rule: infinite_finite_induct, auto)
ballarin@23957
    88
qed
ballarin@23957
    89
wenzelm@30729
    90
interpretation int: abelian_monoid \<Z>
ballarin@61566
    91
  rewrites int_carrier_eq: "carrier \<Z> = UNIV"
ballarin@41433
    92
    and int_zero_eq: "zero \<Z> = 0"
ballarin@41433
    93
    and int_add_eq: "add \<Z> x y = x + y"
nipkow@64267
    94
    and int_finsum_eq: "finsum \<Z> f A = sum f A"
ballarin@23957
    95
proof -
wenzelm@63167
    96
  \<comment> "Specification"
wenzelm@61169
    97
  show "abelian_monoid \<Z>" by standard auto
wenzelm@30729
    98
  then interpret int: abelian_monoid \<Z> .
ballarin@20318
    99
wenzelm@63167
   100
  \<comment> "Carrier"
ballarin@41433
   101
  show "carrier \<Z> = UNIV" by simp
ballarin@41433
   102
wenzelm@63167
   103
  \<comment> "Operations"
ballarin@41433
   104
  { fix x y show "add \<Z> x y = x + y" by simp }
ballarin@23957
   105
  note add = this
wenzelm@55991
   106
  show zero: "zero \<Z> = 0"
wenzelm@55991
   107
    by simp
nipkow@64267
   108
  show "finsum \<Z> f A = sum f A"
rene@60112
   109
    by (induct A rule: infinite_finite_induct, auto)
ballarin@23957
   110
qed
ballarin@23957
   111
wenzelm@30729
   112
interpretation int: abelian_group \<Z>
ballarin@41433
   113
  (* The equations from the interpretation of abelian_monoid need to be repeated.
ballarin@41433
   114
     Since the morphisms through which the abelian structures are interpreted are
ballarin@41433
   115
     not the identity, the equations of these interpretations are not inherited. *)
ballarin@41433
   116
  (* FIXME *)
ballarin@61566
   117
  rewrites "carrier \<Z> = UNIV"
ballarin@41433
   118
    and "zero \<Z> = 0"
ballarin@41433
   119
    and "add \<Z> x y = x + y"
nipkow@64267
   120
    and "finsum \<Z> f A = sum f A"
ballarin@41433
   121
    and int_a_inv_eq: "a_inv \<Z> x = - x"
ballarin@41433
   122
    and int_a_minus_eq: "a_minus \<Z> x y = x - y"
ballarin@23957
   123
proof -
wenzelm@63167
   124
  \<comment> "Specification"
ballarin@23957
   125
  show "abelian_group \<Z>"
ballarin@23957
   126
  proof (rule abelian_groupI)
wenzelm@55991
   127
    fix x
wenzelm@55991
   128
    assume "x \<in> carrier \<Z>"
wenzelm@55991
   129
    then show "\<exists>y \<in> carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
ballarin@41433
   130
      by simp arith
ballarin@41433
   131
  qed auto
wenzelm@30729
   132
  then interpret int: abelian_group \<Z> .
wenzelm@63167
   133
  \<comment> "Operations"
ballarin@41433
   134
  { fix x y have "add \<Z> x y = x + y" by simp }
ballarin@23957
   135
  note add = this
ballarin@41433
   136
  have zero: "zero \<Z> = 0" by simp
wenzelm@55991
   137
  {
wenzelm@55991
   138
    fix x
wenzelm@55991
   139
    have "add \<Z> (- x) x = zero \<Z>"
wenzelm@55991
   140
      by (simp add: add zero)
wenzelm@55991
   141
    then show "a_inv \<Z> x = - x"
wenzelm@55991
   142
      by (simp add: int.minus_equality)
wenzelm@55991
   143
  }
ballarin@23957
   144
  note a_inv = this
wenzelm@55991
   145
  show "a_minus \<Z> x y = x - y"
wenzelm@55991
   146
    by (simp add: int.minus_eq add a_inv)
ballarin@41433
   147
qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
ballarin@23957
   148
wenzelm@30729
   149
interpretation int: "domain" \<Z>
ballarin@61566
   150
  rewrites "carrier \<Z> = UNIV"
ballarin@41433
   151
    and "zero \<Z> = 0"
ballarin@41433
   152
    and "add \<Z> x y = x + y"
nipkow@64267
   153
    and "finsum \<Z> f A = sum f A"
ballarin@41433
   154
    and "a_inv \<Z> x = - x"
ballarin@41433
   155
    and "a_minus \<Z> x y = x - y"
ballarin@41433
   156
proof -
wenzelm@55991
   157
  show "domain \<Z>"
wenzelm@55991
   158
    by unfold_locales (auto simp: distrib_right distrib_left)
wenzelm@55991
   159
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
   160
ballarin@23957
   161
wenzelm@61382
   162
text \<open>Removal of occurrences of @{term UNIV} in interpretation result
wenzelm@61382
   163
  --- experimental.\<close>
ballarin@24131
   164
ballarin@24131
   165
lemma UNIV:
wenzelm@55991
   166
  "x \<in> UNIV \<longleftrightarrow> True"
wenzelm@55991
   167
  "A \<subseteq> UNIV \<longleftrightarrow> True"
wenzelm@55991
   168
  "(\<forall>x \<in> UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
wenzelm@67091
   169
  "(\<exists>x \<in> UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
wenzelm@55991
   170
  "(True \<longrightarrow> Q) \<longleftrightarrow> Q"
wenzelm@55991
   171
  "(True \<Longrightarrow> PROP R) \<equiv> PROP R"
ballarin@24131
   172
  by simp_all
ballarin@24131
   173
wenzelm@30729
   174
interpretation int (* FIXME [unfolded UNIV] *) :
wenzelm@55926
   175
  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
ballarin@61566
   176
  rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
wenzelm@55926
   177
    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
wenzelm@55926
   178
    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
ballarin@23957
   179
proof -
wenzelm@55926
   180
  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
wenzelm@61169
   181
    by standard simp_all
wenzelm@55926
   182
  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
ballarin@24131
   183
    by simp
wenzelm@55926
   184
  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
ballarin@24131
   185
    by simp
wenzelm@55926
   186
  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
ballarin@23957
   187
    by (simp add: lless_def) auto
ballarin@23957
   188
qed
ballarin@23957
   189
wenzelm@30729
   190
interpretation int (* FIXME [unfolded UNIV] *) :
wenzelm@55926
   191
  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
ballarin@61566
   192
  rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
wenzelm@55926
   193
    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
ballarin@23957
   194
proof -
wenzelm@55926
   195
  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
ballarin@23957
   196
  show "lattice ?Z"
ballarin@23957
   197
    apply unfold_locales
ballarin@23957
   198
    apply (simp add: least_def Upper_def)
ballarin@23957
   199
    apply arith
ballarin@23957
   200
    apply (simp add: greatest_def Lower_def)
ballarin@23957
   201
    apply arith
ballarin@23957
   202
    done
wenzelm@30729
   203
  then interpret int: lattice "?Z" .
ballarin@23957
   204
  show "join ?Z x y = max x y"
ballarin@23957
   205
    apply (rule int.joinI)
ballarin@23957
   206
    apply (simp_all add: least_def Upper_def)
ballarin@23957
   207
    apply arith
ballarin@23957
   208
    done
ballarin@23957
   209
  show "meet ?Z x y = min x y"
ballarin@23957
   210
    apply (rule int.meetI)
ballarin@23957
   211
    apply (simp_all add: greatest_def Lower_def)
ballarin@23957
   212
    apply arith
ballarin@23957
   213
    done
ballarin@23957
   214
qed
ballarin@23957
   215
wenzelm@30729
   216
interpretation int (* [unfolded UNIV] *) :
wenzelm@55926
   217
  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
wenzelm@61169
   218
  by standard clarsimp
ballarin@23957
   219
ballarin@20318
   220
wenzelm@63167
   221
subsection \<open>Generated Ideals of \<open>\<Z>\<close>\<close>
ballarin@20318
   222
wenzelm@55991
   223
lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
ballarin@41433
   224
  apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
ballarin@41433
   225
  apply (simp add: cgenideal_def)
ballarin@23957
   226
  done
ballarin@20318
   227
wenzelm@55991
   228
lemma multiples_principalideal: "principalideal {x * a | x. True } \<Z>"
wenzelm@55991
   229
  by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
nipkow@29700
   230
ballarin@20318
   231
lemma prime_primeideal:
lp15@55242
   232
  assumes prime: "prime p"
ballarin@20318
   233
  shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
ballarin@20318
   234
apply (rule primeidealI)
ballarin@23957
   235
   apply (rule int.genideal_ideal, simp)
ballarin@20318
   236
  apply (rule int_is_cring)
ballarin@23957
   237
 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
ballarin@20318
   238
 apply clarsimp defer 1
ballarin@23957
   239
 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
ballarin@20318
   240
 apply (elim exE)
ballarin@20318
   241
proof -
ballarin@20318
   242
  fix a b x
eberlm@63534
   243
  assume "a * b = x * p"
wenzelm@55991
   244
  then have "p dvd a * b" by simp
wenzelm@55991
   245
  then have "p dvd a \<or> p dvd b"
lp15@55242
   246
    by (metis prime prime_dvd_mult_eq_int)
eberlm@63534
   247
  then show "(\<exists>x. a = x * p) \<or> (\<exists>x. b = x * p)"
haftmann@57512
   248
    by (metis dvd_def mult.commute)
ballarin@20318
   249
next
wenzelm@67091
   250
  assume "UNIV = {uu. \<exists>x. uu = x * p}"
eberlm@63534
   251
  then obtain x where "1 = x * p" by best
eberlm@63534
   252
  then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
eberlm@63534
   253
  then show False using prime
eberlm@63633
   254
    by (auto dest!: abs_zmult_eq_1 simp: prime_def)
ballarin@20318
   255
qed
ballarin@20318
   256
ballarin@20318
   257
wenzelm@61382
   258
subsection \<open>Ideals and Divisibility\<close>
ballarin@20318
   259
wenzelm@55991
   260
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
   261
  by (rule int.Idl_subset_ideal') simp_all
ballarin@20318
   262
wenzelm@55991
   263
lemma Idl_subset_eq_dvd: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> l dvd k"
wenzelm@55991
   264
  apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
wenzelm@55991
   265
  apply (rule, clarify)
wenzelm@55991
   266
  apply (simp add: dvd_def)
haftmann@57514
   267
  apply (simp add: dvd_def ac_simps)
wenzelm@55991
   268
  done
ballarin@20318
   269
wenzelm@55991
   270
lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
ballarin@20318
   271
proof -
wenzelm@55991
   272
  have a: "l dvd k \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})"
wenzelm@55991
   273
    by (rule Idl_subset_eq_dvd[symmetric])
wenzelm@55991
   274
  have b: "k dvd l \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})"
wenzelm@55991
   275
    by (rule Idl_subset_eq_dvd[symmetric])
ballarin@20318
   276
wenzelm@55991
   277
  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
   278
    by (subst a, subst b, simp)
wenzelm@55991
   279
  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
   280
    by blast
wenzelm@55991
   281
  finally show ?thesis .
ballarin@20318
   282
qed
ballarin@20318
   283
wenzelm@61945
   284
lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
wenzelm@55991
   285
  apply (subst dvds_eq_abseq[symmetric])
wenzelm@55991
   286
  apply (rule dvds_eq_Idl[symmetric])
wenzelm@55991
   287
  done
ballarin@20318
   288
ballarin@20318
   289
wenzelm@61382
   290
subsection \<open>Ideals and the Modulus\<close>
ballarin@20318
   291
wenzelm@55991
   292
definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set"
wenzelm@35848
   293
  where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
ballarin@20318
   294
ballarin@20318
   295
lemmas ZMod_defs =
ballarin@20318
   296
  ZMod_def genideal_def
ballarin@20318
   297
ballarin@20318
   298
lemma rcos_zfact:
ballarin@20318
   299
  assumes kIl: "k \<in> ZMod l r"
wenzelm@55991
   300
  shows "\<exists>x. k = x * l + r"
ballarin@20318
   301
proof -
wenzelm@55991
   302
  from kIl[unfolded ZMod_def] have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r"
wenzelm@55991
   303
    by (simp add: a_r_coset_defs)
wenzelm@55991
   304
  then obtain xl where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" and k: "k = xl + r"
wenzelm@55991
   305
    by auto
wenzelm@55991
   306
  from xl obtain x where "xl = x * l"
wenzelm@55991
   307
    by (auto simp: int_Idl)
wenzelm@55991
   308
  with k have "k = x * l + r"
wenzelm@55991
   309
    by simp
wenzelm@55991
   310
  then show "\<exists>x. k = x * l + r" ..
ballarin@20318
   311
qed
ballarin@20318
   312
ballarin@20318
   313
lemma ZMod_imp_zmod:
ballarin@20318
   314
  assumes zmods: "ZMod m a = ZMod m b"
ballarin@20318
   315
  shows "a mod m = b mod m"
ballarin@20318
   316
proof -
wenzelm@55991
   317
  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
wenzelm@55991
   318
    by (rule int.genideal_ideal) fast
wenzelm@55991
   319
  from zmods have "b \<in> ZMod m a"
wenzelm@55991
   320
    unfolding ZMod_def by (simp add: a_repr_independenceD)
wenzelm@55991
   321
  then have "\<exists>x. b = x * m + a"
wenzelm@55991
   322
    by (rule rcos_zfact)
wenzelm@55991
   323
  then obtain x where "b = x * m + a"
wenzelm@55991
   324
    by fast
wenzelm@55991
   325
  then have "b mod m = (x * m + a) mod m"
wenzelm@55991
   326
    by simp
wenzelm@55991
   327
  also have "\<dots> = ((x * m) mod m) + (a mod m)"
wenzelm@55991
   328
    by (simp add: mod_add_eq)
wenzelm@55991
   329
  also have "\<dots> = a mod m"
wenzelm@55991
   330
    by simp
wenzelm@55991
   331
  finally have "b mod m = a mod m" .
wenzelm@55991
   332
  then show "a mod m = b mod m" ..
ballarin@20318
   333
qed
ballarin@20318
   334
wenzelm@55991
   335
lemma ZMod_mod: "ZMod m a = ZMod m (a mod m)"
ballarin@20318
   336
proof -
wenzelm@55991
   337
  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
wenzelm@55991
   338
    by (rule int.genideal_ideal) fast
ballarin@20318
   339
  show ?thesis
wenzelm@55991
   340
    unfolding ZMod_def
wenzelm@55991
   341
    apply (rule a_repr_independence'[symmetric])
wenzelm@55991
   342
    apply (simp add: int_Idl a_r_coset_defs)
ballarin@20318
   343
  proof -
wenzelm@55991
   344
    have "a = m * (a div m) + (a mod m)"
haftmann@64246
   345
      by (simp add: mult_div_mod_eq [symmetric])
wenzelm@55991
   346
    then have "a = (a div m) * m + (a mod m)"
wenzelm@55991
   347
      by simp
wenzelm@55991
   348
    then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m"
wenzelm@55991
   349
      by fast
ballarin@20318
   350
  qed simp
ballarin@20318
   351
qed
ballarin@20318
   352
ballarin@20318
   353
lemma zmod_imp_ZMod:
ballarin@20318
   354
  assumes modeq: "a mod m = b mod m"
ballarin@20318
   355
  shows "ZMod m a = ZMod m b"
ballarin@20318
   356
proof -
wenzelm@55991
   357
  have "ZMod m a = ZMod m (a mod m)"
wenzelm@55991
   358
    by (rule ZMod_mod)
wenzelm@55991
   359
  also have "\<dots> = ZMod m (b mod m)"
wenzelm@55991
   360
    by (simp add: modeq[symmetric])
wenzelm@55991
   361
  also have "\<dots> = ZMod m b"
wenzelm@55991
   362
    by (rule ZMod_mod[symmetric])
ballarin@20318
   363
  finally show ?thesis .
ballarin@20318
   364
qed
ballarin@20318
   365
wenzelm@55991
   366
corollary ZMod_eq_mod: "ZMod m a = ZMod m b \<longleftrightarrow> a mod m = b mod m"
wenzelm@55991
   367
  apply (rule iffI)
wenzelm@55991
   368
  apply (erule ZMod_imp_zmod)
wenzelm@55991
   369
  apply (erule zmod_imp_ZMod)
wenzelm@55991
   370
  done
ballarin@20318
   371
ballarin@20318
   372
wenzelm@61382
   373
subsection \<open>Factorization\<close>
ballarin@20318
   374
wenzelm@55991
   375
definition ZFact :: "int \<Rightarrow> int set ring"
wenzelm@35848
   376
  where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
ballarin@20318
   377
ballarin@20318
   378
lemmas ZFact_defs = ZFact_def FactRing_def
ballarin@20318
   379
wenzelm@55991
   380
lemma ZFact_is_cring: "cring (ZFact k)"
wenzelm@55991
   381
  apply (unfold ZFact_def)
wenzelm@55991
   382
  apply (rule ideal.quotient_is_cring)
wenzelm@55991
   383
   apply (intro ring.genideal_ideal)
wenzelm@55991
   384
    apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
wenzelm@55991
   385
   apply simp
wenzelm@55991
   386
  apply (rule int_is_cring)
wenzelm@55991
   387
  done
ballarin@20318
   388
wenzelm@55991
   389
lemma ZFact_zero: "carrier (ZFact 0) = (\<Union>a. {{a}})"
wenzelm@55991
   390
  apply (insert int.genideal_zero)
wenzelm@55991
   391
  apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def)
wenzelm@55991
   392
  done
ballarin@20318
   393
wenzelm@55991
   394
lemma ZFact_one: "carrier (ZFact 1) = {UNIV}"
wenzelm@55991
   395
  apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
wenzelm@55991
   396
  apply (subst int.genideal_one)
wenzelm@55991
   397
  apply (rule, rule, clarsimp)
wenzelm@55991
   398
   apply (rule, rule, clarsimp)
wenzelm@55991
   399
   apply (rule, clarsimp, arith)
wenzelm@55991
   400
  apply (rule, clarsimp)
wenzelm@55991
   401
  apply (rule exI[of _ "0"], clarsimp)
wenzelm@55991
   402
  done
ballarin@20318
   403
ballarin@20318
   404
lemma ZFact_prime_is_domain:
lp15@55242
   405
  assumes pprime: "prime p"
ballarin@20318
   406
  shows "domain (ZFact p)"
wenzelm@55991
   407
  apply (unfold ZFact_def)
wenzelm@55991
   408
  apply (rule primeideal.quotient_is_domain)
wenzelm@55991
   409
  apply (rule prime_primeideal[OF pprime])
wenzelm@55991
   410
  done
ballarin@20318
   411
ballarin@20318
   412
end