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
```