src/HOL/Algebra/IntRing.thy
author ballarin
Tue Jul 24 15:29:57 2007 +0200 (2007-07-24)
changeset 23957 54fab60ddc97
parent 22063 717425609192
child 24131 1099f6c73649
permissions -rw-r--r--
Interpretation of rings (as integers) maps defined operations to defined
operations..
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@23957
    74
lemma int_Zcarr [intro!, simp]:
ballarin@20318
    75
  "k \<in> carrier \<Z>"
ballarin@23957
    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@23957
    89
(*
ballarin@20318
    90
lemma int_is_domain:
ballarin@20318
    91
  "domain \<Z>"
ballarin@20318
    92
apply (intro domain.intro domain_axioms.intro)
ballarin@20318
    93
  apply (rule int_is_cring)
ballarin@20318
    94
 apply (unfold int_ring_def, simp+)
ballarin@20318
    95
done
ballarin@23957
    96
*)
ballarin@23957
    97
subsubsection {* Interpretations *}
ballarin@20318
    98
ballarin@23957
    99
text {* Since definitions of derived operations are global, their
ballarin@23957
   100
  interpretation needs to be done as early as possible --- that is,
ballarin@23957
   101
  with as few assumptions as possible. *}
ballarin@23957
   102
ballarin@23957
   103
interpretation int: monoid ["\<Z>"]
ballarin@23957
   104
  where "carrier \<Z> = UNIV"
ballarin@23957
   105
    and "mult \<Z> x y = x * y"
ballarin@23957
   106
    and "one \<Z> = 1"
ballarin@23957
   107
    and "pow \<Z> x n = x^n"
ballarin@23957
   108
proof -
ballarin@23957
   109
  -- "Specification"
ballarin@23957
   110
  show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
ballarin@23957
   111
  then interpret int: monoid ["\<Z>"] .
ballarin@23957
   112
ballarin@23957
   113
  -- "Carrier"
ballarin@23957
   114
  show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
ballarin@23957
   115
ballarin@23957
   116
  -- "Operations"
ballarin@23957
   117
  { fix x y show "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
ballarin@23957
   118
  note mult = this
ballarin@23957
   119
  show one: "one \<Z> = 1" by (simp add: int_ring_def)
ballarin@23957
   120
  show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
ballarin@23957
   121
qed
ballarin@23957
   122
ballarin@23957
   123
interpretation int: comm_monoid ["\<Z>"]
ballarin@23957
   124
  where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
ballarin@23957
   125
proof -
ballarin@23957
   126
  -- "Specification"
ballarin@23957
   127
  show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
ballarin@23957
   128
  then interpret int: comm_monoid ["\<Z>"] .
ballarin@23957
   129
ballarin@23957
   130
  -- "Operations"
ballarin@23957
   131
  { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
ballarin@23957
   132
  note mult = this
ballarin@23957
   133
  have one: "one \<Z> = 1" by (simp add: int_ring_def)
ballarin@23957
   134
  show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
ballarin@23957
   135
  proof (cases "finite A")
ballarin@23957
   136
    case True then show ?thesis proof induct
ballarin@23957
   137
      case empty show ?case by (simp add: one)
ballarin@23957
   138
    next
ballarin@23957
   139
      case insert then show ?case by (simp add: Pi_def mult)
ballarin@23957
   140
    qed
ballarin@23957
   141
  next
ballarin@23957
   142
    case False then show ?thesis by (simp add: finprod_def)
ballarin@23957
   143
  qed
ballarin@23957
   144
qed
ballarin@23957
   145
ballarin@23957
   146
interpretation int: abelian_monoid ["\<Z>"]
ballarin@23957
   147
  where "zero \<Z> = 0"
ballarin@23957
   148
    and "add \<Z> x y = x + y"
ballarin@23957
   149
    and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
ballarin@23957
   150
proof -
ballarin@23957
   151
  -- "Specification"
ballarin@23957
   152
  show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
ballarin@23957
   153
  then interpret int: abelian_monoid ["\<Z>"] .
ballarin@20318
   154
ballarin@23957
   155
  -- "Operations"
ballarin@23957
   156
  { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
ballarin@23957
   157
  note add = this
ballarin@23957
   158
  show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
ballarin@23957
   159
  show "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
ballarin@23957
   160
  proof (cases "finite A")
ballarin@23957
   161
    case True then show ?thesis proof induct
ballarin@23957
   162
      case empty show ?case by (simp add: zero)
ballarin@23957
   163
    next
ballarin@23957
   164
      case insert then show ?case by (simp add: Pi_def add)
ballarin@23957
   165
    qed
ballarin@23957
   166
  next
ballarin@23957
   167
    case False then show ?thesis by (simp add: finsum_def finprod_def)
ballarin@23957
   168
  qed
ballarin@23957
   169
qed
ballarin@23957
   170
ballarin@23957
   171
interpretation int: abelian_group ["\<Z>"]
ballarin@23957
   172
  where "a_inv \<Z> x = - x"
ballarin@23957
   173
    and "a_minus \<Z> x y = x - y"
ballarin@23957
   174
proof -
ballarin@23957
   175
  -- "Specification"
ballarin@23957
   176
  show "abelian_group \<Z>"
ballarin@23957
   177
  proof (rule abelian_groupI)
ballarin@23957
   178
    show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
ballarin@23957
   179
      by (simp add: int_ring_def) arith
ballarin@23957
   180
  qed (auto simp: int_ring_def)
ballarin@23957
   181
  then interpret int: abelian_group ["\<Z>"] .
ballarin@23957
   182
ballarin@23957
   183
  -- "Operations"
ballarin@23957
   184
  { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
ballarin@23957
   185
  note add = this
ballarin@23957
   186
  have zero: "zero \<Z> = 0" by (simp add: int_ring_def)
ballarin@23957
   187
  { fix x
ballarin@23957
   188
    have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero)
ballarin@23957
   189
    then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) }
ballarin@23957
   190
  note a_inv = this
ballarin@23957
   191
  show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
ballarin@23957
   192
qed
ballarin@23957
   193
ballarin@23957
   194
interpretation int: "domain" ["\<Z>"]
ballarin@23957
   195
  by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
ballarin@23957
   196
ballarin@23957
   197
ballarin@23957
   198
interpretation int: partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
ballarin@23957
   199
  where "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
ballarin@23957
   200
proof -
ballarin@23957
   201
  show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
ballarin@23957
   202
    by unfold_locales simp_all
ballarin@23957
   203
  show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
ballarin@23957
   204
    by (simp add: lless_def) auto
ballarin@23957
   205
qed
ballarin@23957
   206
ballarin@23957
   207
interpretation int: lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
ballarin@23957
   208
  where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
ballarin@23957
   209
    and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
ballarin@23957
   210
proof -
ballarin@23957
   211
  let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)"
ballarin@23957
   212
  show "lattice ?Z"
ballarin@23957
   213
    apply unfold_locales
ballarin@23957
   214
    apply (simp add: least_def Upper_def)
ballarin@23957
   215
    apply arith
ballarin@23957
   216
    apply (simp add: greatest_def Lower_def)
ballarin@23957
   217
    apply arith
ballarin@23957
   218
    done
ballarin@23957
   219
  then interpret int: lattice ["?Z"] .
ballarin@23957
   220
  show "join ?Z x y = max x y"
ballarin@23957
   221
    apply (rule int.joinI)
ballarin@23957
   222
    apply (simp_all add: least_def Upper_def)
ballarin@23957
   223
    apply arith
ballarin@23957
   224
    done
ballarin@23957
   225
  show "meet ?Z x y = min x y"
ballarin@23957
   226
    apply (rule int.meetI)
ballarin@23957
   227
    apply (simp_all add: greatest_def Lower_def)
ballarin@23957
   228
    apply arith
ballarin@23957
   229
    done
ballarin@23957
   230
qed
ballarin@23957
   231
ballarin@23957
   232
interpretation int: total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
ballarin@23957
   233
  by unfold_locales clarsimp
ballarin@23957
   234
ballarin@23957
   235
(*
ballarin@20318
   236
lemma int_le_total_order:
ballarin@22063
   237
  "total_order (| carrier = UNIV::int set, le = op \<le> |)"
ballarin@22063
   238
  apply (rule partial_order.total_orderI)
ballarin@22063
   239
   apply (rule partial_order.intro, simp+)
ballarin@22063
   240
  apply clarsimp
ballarin@22063
   241
  done
ballarin@20318
   242
ballarin@21896
   243
lemma less_int:
ballarin@22063
   244
  "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
ballarin@22063
   245
  by (auto simp add: expand_fun_eq lless_def)
ballarin@21896
   246
ballarin@21896
   247
lemma join_int:
ballarin@22063
   248
  "join (| carrier = UNIV::int set, le = op \<le> |) = max"
ballarin@21896
   249
  apply (simp add: expand_fun_eq max_def)
ballarin@21896
   250
  apply (rule+)
ballarin@21896
   251
  apply (rule lattice.joinI)
ballarin@21896
   252
  apply (simp add: int_le_total_order total_order.axioms)
ballarin@22063
   253
  apply (simp add: least_def Upper_def)
ballarin@21896
   254
  apply arith
ballarin@21896
   255
  apply simp apply simp
ballarin@21896
   256
  apply (rule lattice.joinI)
ballarin@21896
   257
  apply (simp add: int_le_total_order total_order.axioms)
ballarin@22063
   258
  apply (simp add: least_def Upper_def)
ballarin@21896
   259
  apply arith
ballarin@21896
   260
  apply simp apply simp
ballarin@21896
   261
  done
ballarin@21896
   262
ballarin@21896
   263
lemma meet_int:
ballarin@22063
   264
  "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
ballarin@21896
   265
  apply (simp add: expand_fun_eq min_def)
ballarin@21896
   266
  apply (rule+)
ballarin@21896
   267
  apply (rule lattice.meetI)
ballarin@21896
   268
  apply (simp add: int_le_total_order total_order.axioms)
ballarin@22063
   269
  apply (simp add: greatest_def Lower_def)
ballarin@21896
   270
  apply arith
ballarin@21896
   271
  apply simp apply simp
ballarin@21896
   272
  apply (rule lattice.meetI)
ballarin@21896
   273
  apply (simp add: int_le_total_order total_order.axioms)
ballarin@22063
   274
  apply (simp add: greatest_def Lower_def)
ballarin@21896
   275
  apply arith
ballarin@21896
   276
  apply simp apply simp
ballarin@21896
   277
  done
ballarin@21896
   278
ballarin@22063
   279
lemma carrier_int:
ballarin@22063
   280
  "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
ballarin@22063
   281
  apply simp
ballarin@22063
   282
  done
ballarin@22063
   283
ballarin@22063
   284
text {* Interpretation unfolding @{text lless}, @{text join} and @{text
ballarin@21896
   285
  meet} since they have natural representations in @{typ int}. *}
ballarin@21896
   286
ballarin@21896
   287
interpretation 
ballarin@22063
   288
  int [unfolded less_int join_int meet_int carrier_int]:
ballarin@22063
   289
  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
ballarin@22063
   290
  by (rule int_le_total_order)
ballarin@23957
   291
*)
ballarin@20318
   292
ballarin@20318
   293
ballarin@20318
   294
subsubsection {* Generated Ideals of @{text "\<Z>"} *}
ballarin@20318
   295
ballarin@20318
   296
lemma int_Idl:
ballarin@20318
   297
  "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
ballarin@23957
   298
  apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)
ballarin@23957
   299
  apply (simp add: cgenideal_def int_ring_def)
ballarin@23957
   300
  done
ballarin@20318
   301
ballarin@20318
   302
lemma multiples_principalideal:
ballarin@20318
   303
  "principalideal {x * a | x. True } \<Z>"
ballarin@20318
   304
apply (subst int_Idl[symmetric], rule principalidealI)
ballarin@23957
   305
 apply (rule int.genideal_ideal, simp)
ballarin@20318
   306
apply fast
ballarin@20318
   307
done
ballarin@20318
   308
ballarin@20318
   309
lemma prime_primeideal:
ballarin@20318
   310
  assumes prime: "prime (nat p)"
ballarin@20318
   311
  shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
ballarin@20318
   312
apply (rule primeidealI)
ballarin@23957
   313
   apply (rule int.genideal_ideal, simp)
ballarin@20318
   314
  apply (rule int_is_cring)
ballarin@23957
   315
 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
ballarin@20318
   316
 apply (simp add: int_ring_def)
ballarin@20318
   317
 apply clarsimp defer 1
ballarin@23957
   318
 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
ballarin@20318
   319
 apply (simp add: int_ring_def)
ballarin@20318
   320
 apply (elim exE)
ballarin@20318
   321
proof -
ballarin@20318
   322
  fix a b x
ballarin@20318
   323
ballarin@20318
   324
  from prime
ballarin@20318
   325
      have ppos: "0 <= p" by (simp add: prime_def)
ballarin@20318
   326
  have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
ballarin@20318
   327
  proof -
ballarin@20318
   328
    fix x
ballarin@20318
   329
    assume "nat p dvd nat (abs x)"
ballarin@20318
   330
    hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
ballarin@20318
   331
    thus "p dvd x" by (simp add: ppos)
ballarin@20318
   332
  qed
ballarin@20318
   333
ballarin@20318
   334
ballarin@20318
   335
  assume "a * b = x * p"
ballarin@20318
   336
  hence "p dvd a * b" by simp
ballarin@20318
   337
  hence "nat p dvd nat (abs (a * b))"
ballarin@20318
   338
  apply (subst nat_dvd_iff, clarsimp)
ballarin@20318
   339
  apply (rule conjI, clarsimp, simp add: zabs_def)
ballarin@20318
   340
  proof (clarsimp)
ballarin@20318
   341
    assume a: " ~ 0 <= p"
ballarin@20318
   342
    from prime
ballarin@20318
   343
        have "0 < p" by (simp add: prime_def)
ballarin@20318
   344
    from a and this
ballarin@20318
   345
        have "False" by simp
ballarin@20318
   346
    thus "nat (abs (a * b)) = 0" ..
ballarin@20318
   347
  qed
ballarin@20318
   348
  hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
ballarin@20318
   349
  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
ballarin@20318
   350
  hence "p dvd a | p dvd b" by (fast intro: unnat)
ballarin@20318
   351
  thus "(EX x. a = x * p) | (EX x. b = x * p)"
ballarin@20318
   352
  proof
ballarin@20318
   353
    assume "p dvd a"
ballarin@20318
   354
    hence "EX x. a = p * x" by (simp add: dvd_def)
ballarin@20318
   355
    from this obtain x
ballarin@20318
   356
        where "a = p * x" by fast
ballarin@20318
   357
    hence "a = x * p" by simp
ballarin@20318
   358
    hence "EX x. a = x * p" by simp
ballarin@20318
   359
    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
ballarin@20318
   360
  next
ballarin@20318
   361
    assume "p dvd b"
ballarin@20318
   362
    hence "EX x. b = p * x" by (simp add: dvd_def)
ballarin@20318
   363
    from this obtain x
ballarin@20318
   364
        where "b = p * x" by fast
ballarin@20318
   365
    hence "b = x * p" by simp
ballarin@20318
   366
    hence "EX x. b = x * p" by simp
ballarin@20318
   367
    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
ballarin@20318
   368
  qed
ballarin@20318
   369
next
ballarin@20318
   370
  assume "UNIV = {uu. EX x. uu = x * p}"
ballarin@20318
   371
  from this obtain x 
ballarin@20318
   372
      where "1 = x * p" by fast
ballarin@20318
   373
  from this [symmetric]
ballarin@20318
   374
      have "p * x = 1" by (subst zmult_commute)
ballarin@20318
   375
  hence "\<bar>p * x\<bar> = 1" by simp
ballarin@20318
   376
  hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
ballarin@20318
   377
  from this and prime
ballarin@20318
   378
      show "False" by (simp add: prime_def)
ballarin@20318
   379
qed
ballarin@20318
   380
ballarin@20318
   381
ballarin@20318
   382
subsubsection {* Ideals and Divisibility *}
ballarin@20318
   383
ballarin@20318
   384
lemma int_Idl_subset_ideal:
ballarin@20318
   385
  "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
ballarin@23957
   386
by (rule int.Idl_subset_ideal', simp+)
ballarin@20318
   387
ballarin@20318
   388
lemma Idl_subset_eq_dvd:
ballarin@20318
   389
  "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
ballarin@20318
   390
apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
ballarin@20318
   391
apply (rule, clarify)
ballarin@20318
   392
apply (simp add: dvd_def, clarify)
ballarin@23957
   393
apply (simp add: int.m_comm)
ballarin@20318
   394
done
ballarin@20318
   395
ballarin@20318
   396
lemma dvds_eq_Idl:
ballarin@20318
   397
  "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
ballarin@20318
   398
proof -
ballarin@20318
   399
  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
   400
  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
   401
ballarin@20318
   402
  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
   403
  by (subst a, subst b, simp)
ballarin@20318
   404
  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
   405
  finally
ballarin@20318
   406
    show ?thesis .
ballarin@20318
   407
qed
ballarin@20318
   408
ballarin@20318
   409
lemma Idl_eq_abs:
ballarin@20318
   410
  "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)"
ballarin@20318
   411
apply (subst dvds_eq_abseq[symmetric])
ballarin@20318
   412
apply (rule dvds_eq_Idl[symmetric])
ballarin@20318
   413
done
ballarin@20318
   414
ballarin@20318
   415
ballarin@20318
   416
subsubsection {* Ideals and the Modulus *}
ballarin@20318
   417
ballarin@20318
   418
constdefs
ballarin@20318
   419
   ZMod :: "int => int => int set"
ballarin@20318
   420
  "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
ballarin@20318
   421
ballarin@20318
   422
lemmas ZMod_defs =
ballarin@20318
   423
  ZMod_def genideal_def
ballarin@20318
   424
ballarin@20318
   425
lemma rcos_zfact:
ballarin@20318
   426
  assumes kIl: "k \<in> ZMod l r"
ballarin@20318
   427
  shows "EX x. k = x * l + r"
ballarin@20318
   428
proof -
ballarin@20318
   429
  from kIl[unfolded ZMod_def]
ballarin@20318
   430
      have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def)
ballarin@20318
   431
  from this obtain xl
ballarin@20318
   432
      where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
ballarin@20318
   433
      and k: "k = xl + r"
ballarin@20318
   434
      by auto
ballarin@20318
   435
  from xl obtain x
ballarin@20318
   436
      where "xl = x * l"
ballarin@20318
   437
      by (simp add: int_Idl, fast)
ballarin@20318
   438
  from k and this
ballarin@20318
   439
      have "k = x * l + r" by simp
ballarin@20318
   440
  thus "\<exists>x. k = x * l + r" ..
ballarin@20318
   441
qed
ballarin@20318
   442
ballarin@20318
   443
lemma ZMod_imp_zmod:
ballarin@20318
   444
  assumes zmods: "ZMod m a = ZMod m b"
ballarin@20318
   445
  shows "a mod m = b mod m"
ballarin@20318
   446
proof -
ballarin@23957
   447
  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
ballarin@20318
   448
  from zmods
ballarin@20318
   449
      have "b \<in> ZMod m a"
ballarin@20318
   450
      unfolding ZMod_def
ballarin@20318
   451
      by (simp add: a_repr_independenceD)
ballarin@20318
   452
  from this
ballarin@20318
   453
      have "EX x. b = x * m + a" by (rule rcos_zfact)
ballarin@20318
   454
  from this obtain x
ballarin@20318
   455
      where "b = x * m + a"
ballarin@20318
   456
      by fast
ballarin@20318
   457
ballarin@20318
   458
  hence "b mod m = (x * m + a) mod m" by simp
ballarin@20318
   459
  also
ballarin@20318
   460
      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
ballarin@20318
   461
  also
ballarin@20318
   462
      have "\<dots> = a mod m" by simp
ballarin@20318
   463
  finally
ballarin@20318
   464
      have "b mod m = a mod m" .
ballarin@20318
   465
  thus "a mod m = b mod m" ..
ballarin@20318
   466
qed
ballarin@20318
   467
ballarin@20318
   468
lemma ZMod_mod:
ballarin@20318
   469
  shows "ZMod m a = ZMod m (a mod m)"
ballarin@20318
   470
proof -
ballarin@23957
   471
  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
ballarin@20318
   472
  show ?thesis
ballarin@20318
   473
      unfolding ZMod_def
ballarin@20318
   474
  apply (rule a_repr_independence'[symmetric])
ballarin@20318
   475
  apply (simp add: int_Idl a_r_coset_defs)
ballarin@20318
   476
  apply (simp add: int_ring_def)
ballarin@20318
   477
  proof -
ballarin@20318
   478
    have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
ballarin@20318
   479
    hence "a = (a div m) * m + (a mod m)" by simp
ballarin@20318
   480
    thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast
ballarin@20318
   481
  qed simp
ballarin@20318
   482
qed
ballarin@20318
   483
ballarin@20318
   484
lemma zmod_imp_ZMod:
ballarin@20318
   485
  assumes modeq: "a mod m = b mod m"
ballarin@20318
   486
  shows "ZMod m a = ZMod m b"
ballarin@20318
   487
proof -
ballarin@20318
   488
  have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod)
ballarin@20318
   489
  also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
ballarin@20318
   490
  also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
ballarin@20318
   491
  finally show ?thesis .
ballarin@20318
   492
qed
ballarin@20318
   493
ballarin@20318
   494
corollary ZMod_eq_mod:
ballarin@20318
   495
  shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
ballarin@20318
   496
by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
ballarin@20318
   497
ballarin@20318
   498
ballarin@20318
   499
subsubsection {* Factorization *}
ballarin@20318
   500
ballarin@20318
   501
constdefs
ballarin@20318
   502
  ZFact :: "int \<Rightarrow> int set ring"
ballarin@20318
   503
  "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
ballarin@20318
   504
ballarin@20318
   505
lemmas ZFact_defs = ZFact_def FactRing_def
ballarin@20318
   506
ballarin@20318
   507
lemma ZFact_is_cring:
ballarin@20318
   508
  shows "cring (ZFact k)"
ballarin@20318
   509
apply (unfold ZFact_def)
ballarin@20318
   510
apply (rule ideal.quotient_is_cring)
ballarin@20318
   511
 apply (intro ring.genideal_ideal)
ballarin@20318
   512
  apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
ballarin@20318
   513
 apply simp
ballarin@20318
   514
apply (rule int_is_cring)
ballarin@20318
   515
done
ballarin@20318
   516
ballarin@20318
   517
lemma ZFact_zero:
ballarin@20318
   518
  "carrier (ZFact 0) = (\<Union>a. {{a}})"
ballarin@23957
   519
apply (insert int.genideal_zero)
ballarin@20318
   520
apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
ballarin@20318
   521
done
ballarin@20318
   522
ballarin@20318
   523
lemma ZFact_one:
ballarin@20318
   524
  "carrier (ZFact 1) = {UNIV}"
ballarin@20318
   525
apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
ballarin@23957
   526
apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps])
ballarin@20318
   527
apply (rule, rule, clarsimp)
ballarin@20318
   528
 apply (rule, rule, clarsimp)
ballarin@20318
   529
 apply (rule, clarsimp, arith)
ballarin@20318
   530
apply (rule, clarsimp)
ballarin@20318
   531
apply (rule exI[of _ "0"], clarsimp)
ballarin@20318
   532
done
ballarin@20318
   533
ballarin@20318
   534
lemma ZFact_prime_is_domain:
ballarin@20318
   535
  assumes pprime: "prime (nat p)"
ballarin@20318
   536
  shows "domain (ZFact p)"
ballarin@20318
   537
apply (unfold ZFact_def)
ballarin@20318
   538
apply (rule primeideal.quotient_is_domain)
ballarin@20318
   539
apply (rule prime_primeideal[OF pprime])
ballarin@20318
   540
done
ballarin@20318
   541
ballarin@20318
   542
end