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