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