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