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