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