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