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