src/HOL/Algebra/IntRing.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 22063 717425609192
child 23957 54fab60ddc97
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     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 (| carrier = UNIV::int set, le = op \<le> |)"
   100   apply (rule partial_order.total_orderI)
   101    apply (rule partial_order.intro, simp+)
   102   apply clarsimp
   103   done
   104 
   105 lemma less_int:
   106   "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
   107   by (auto simp add: expand_fun_eq lless_def)
   108 
   109 lemma join_int:
   110   "join (| carrier = UNIV::int set, le = op \<le> |) = max"
   111   apply (simp add: expand_fun_eq max_def)
   112   apply (rule+)
   113   apply (rule lattice.joinI)
   114   apply (simp add: int_le_total_order total_order.axioms)
   115   apply (simp add: least_def Upper_def)
   116   apply arith
   117   apply simp apply simp
   118   apply (rule lattice.joinI)
   119   apply (simp add: int_le_total_order total_order.axioms)
   120   apply (simp add: least_def Upper_def)
   121   apply arith
   122   apply simp apply simp
   123   done
   124 
   125 lemma meet_int:
   126   "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
   127   apply (simp add: expand_fun_eq min_def)
   128   apply (rule+)
   129   apply (rule lattice.meetI)
   130   apply (simp add: int_le_total_order total_order.axioms)
   131   apply (simp add: greatest_def Lower_def)
   132   apply arith
   133   apply simp apply simp
   134   apply (rule lattice.meetI)
   135   apply (simp add: int_le_total_order total_order.axioms)
   136   apply (simp add: greatest_def Lower_def)
   137   apply arith
   138   apply simp apply simp
   139   done
   140 
   141 lemma carrier_int:
   142   "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
   143   apply simp
   144   done
   145 
   146 text {* Interpretation unfolding @{text lless}, @{text join} and @{text
   147   meet} since they have natural representations in @{typ int}. *}
   148 
   149 interpretation 
   150   int [unfolded less_int join_int meet_int carrier_int]:
   151   total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
   152   by (rule int_le_total_order)
   153 
   154 
   155 subsubsection {* Generated Ideals of @{text "\<Z>"} *}
   156 
   157 lemma int_Idl:
   158   "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
   159 apply (subst cgenideal_eq_genideal[symmetric], simp add: int_ring_def)
   160 apply (simp add: cgenideal_def int_ring_def)
   161 done
   162 
   163 lemma multiples_principalideal:
   164   "principalideal {x * a | x. True } \<Z>"
   165 apply (subst int_Idl[symmetric], rule principalidealI)
   166  apply (rule genideal_ideal, simp)
   167 apply fast
   168 done
   169 
   170 lemma prime_primeideal:
   171   assumes prime: "prime (nat p)"
   172   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
   173 apply (rule primeidealI)
   174    apply (rule genideal_ideal, simp)
   175   apply (rule int_is_cring)
   176  apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def)
   177  apply (simp add: int_ring_def)
   178  apply clarsimp defer 1
   179  apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def)
   180  apply (simp add: int_ring_def)
   181  apply (elim exE)
   182 proof -
   183   fix a b x
   184 
   185   from prime
   186       have ppos: "0 <= p" by (simp add: prime_def)
   187   have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
   188   proof -
   189     fix x
   190     assume "nat p dvd nat (abs x)"
   191     hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
   192     thus "p dvd x" by (simp add: ppos)
   193   qed
   194 
   195 
   196   assume "a * b = x * p"
   197   hence "p dvd a * b" by simp
   198   hence "nat p dvd nat (abs (a * b))"
   199   apply (subst nat_dvd_iff, clarsimp)
   200   apply (rule conjI, clarsimp, simp add: zabs_def)
   201   proof (clarsimp)
   202     assume a: " ~ 0 <= p"
   203     from prime
   204         have "0 < p" by (simp add: prime_def)
   205     from a and this
   206         have "False" by simp
   207     thus "nat (abs (a * b)) = 0" ..
   208   qed
   209   hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
   210   hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
   211   hence "p dvd a | p dvd b" by (fast intro: unnat)
   212   thus "(EX x. a = x * p) | (EX x. b = x * p)"
   213   proof
   214     assume "p dvd a"
   215     hence "EX x. a = p * x" by (simp add: dvd_def)
   216     from this obtain x
   217         where "a = p * x" by fast
   218     hence "a = x * p" by simp
   219     hence "EX x. a = x * p" by simp
   220     thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
   221   next
   222     assume "p dvd b"
   223     hence "EX x. b = p * x" by (simp add: dvd_def)
   224     from this obtain x
   225         where "b = p * x" by fast
   226     hence "b = x * p" by simp
   227     hence "EX x. b = x * p" by simp
   228     thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
   229   qed
   230 next
   231   assume "UNIV = {uu. EX x. uu = x * p}"
   232   from this obtain x 
   233       where "1 = x * p" by fast
   234   from this [symmetric]
   235       have "p * x = 1" by (subst zmult_commute)
   236   hence "\<bar>p * x\<bar> = 1" by simp
   237   hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
   238   from this and prime
   239       show "False" by (simp add: prime_def)
   240 qed
   241 
   242 
   243 subsubsection {* Ideals and Divisibility *}
   244 
   245 lemma int_Idl_subset_ideal:
   246   "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
   247 by (rule Idl_subset_ideal', simp+)
   248 
   249 lemma Idl_subset_eq_dvd:
   250   "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
   251 apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
   252 apply (rule, clarify)
   253 apply (simp add: dvd_def, clarify)
   254 apply (simp add: m_comm)
   255 done
   256 
   257 lemma dvds_eq_Idl:
   258   "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
   259 proof -
   260   have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric])
   261   have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric])
   262 
   263   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}))"
   264   by (subst a, subst b, simp)
   265   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+)
   266   finally
   267     show ?thesis .
   268 qed
   269 
   270 lemma Idl_eq_abs:
   271   "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)"
   272 apply (subst dvds_eq_abseq[symmetric])
   273 apply (rule dvds_eq_Idl[symmetric])
   274 done
   275 
   276 
   277 subsubsection {* Ideals and the Modulus *}
   278 
   279 constdefs
   280    ZMod :: "int => int => int set"
   281   "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
   282 
   283 lemmas ZMod_defs =
   284   ZMod_def genideal_def
   285 
   286 lemma rcos_zfact:
   287   assumes kIl: "k \<in> ZMod l r"
   288   shows "EX x. k = x * l + r"
   289 proof -
   290   from kIl[unfolded ZMod_def]
   291       have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def)
   292   from this obtain xl
   293       where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
   294       and k: "k = xl + r"
   295       by auto
   296   from xl obtain x
   297       where "xl = x * l"
   298       by (simp add: int_Idl, fast)
   299   from k and this
   300       have "k = x * l + r" by simp
   301   thus "\<exists>x. k = x * l + r" ..
   302 qed
   303 
   304 lemma ZMod_imp_zmod:
   305   assumes zmods: "ZMod m a = ZMod m b"
   306   shows "a mod m = b mod m"
   307 proof -
   308   interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast)
   309   from zmods
   310       have "b \<in> ZMod m a"
   311       unfolding ZMod_def
   312       by (simp add: a_repr_independenceD)
   313   from this
   314       have "EX x. b = x * m + a" by (rule rcos_zfact)
   315   from this obtain x
   316       where "b = x * m + a"
   317       by fast
   318 
   319   hence "b mod m = (x * m + a) mod m" by simp
   320   also
   321       have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
   322   also
   323       have "\<dots> = a mod m" by simp
   324   finally
   325       have "b mod m = a mod m" .
   326   thus "a mod m = b mod m" ..
   327 qed
   328 
   329 lemma ZMod_mod:
   330   shows "ZMod m a = ZMod m (a mod m)"
   331 proof -
   332   interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast)
   333   show ?thesis
   334       unfolding ZMod_def
   335   apply (rule a_repr_independence'[symmetric])
   336   apply (simp add: int_Idl a_r_coset_defs)
   337   apply (simp add: int_ring_def)
   338   proof -
   339     have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
   340     hence "a = (a div m) * m + (a mod m)" by simp
   341     thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast
   342   qed simp
   343 qed
   344 
   345 lemma zmod_imp_ZMod:
   346   assumes modeq: "a mod m = b mod m"
   347   shows "ZMod m a = ZMod m b"
   348 proof -
   349   have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod)
   350   also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
   351   also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
   352   finally show ?thesis .
   353 qed
   354 
   355 corollary ZMod_eq_mod:
   356   shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
   357 by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
   358 
   359 
   360 subsubsection {* Factorization *}
   361 
   362 constdefs
   363   ZFact :: "int \<Rightarrow> int set ring"
   364   "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
   365 
   366 lemmas ZFact_defs = ZFact_def FactRing_def
   367 
   368 lemma ZFact_is_cring:
   369   shows "cring (ZFact k)"
   370 apply (unfold ZFact_def)
   371 apply (rule ideal.quotient_is_cring)
   372  apply (intro ring.genideal_ideal)
   373   apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
   374  apply simp
   375 apply (rule int_is_cring)
   376 done
   377 
   378 lemma ZFact_zero:
   379   "carrier (ZFact 0) = (\<Union>a. {{a}})"
   380 apply (insert genideal_zero)
   381 apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
   382 done
   383 
   384 lemma ZFact_one:
   385   "carrier (ZFact 1) = {UNIV}"
   386 apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
   387 apply (subst genideal_one[unfolded int_ring_def, simplified ring_record_simps])
   388 apply (rule, rule, clarsimp)
   389  apply (rule, rule, clarsimp)
   390  apply (rule, clarsimp, arith)
   391 apply (rule, clarsimp)
   392 apply (rule exI[of _ "0"], clarsimp)
   393 done
   394 
   395 lemma ZFact_prime_is_domain:
   396   assumes pprime: "prime (nat p)"
   397   shows "domain (ZFact p)"
   398 apply (unfold ZFact_def)
   399 apply (rule primeideal.quotient_is_domain)
   400 apply (rule prime_primeideal[OF pprime])
   401 done
   402 
   403 end