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