src/HOL/Algebra/IntRing.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 68399 0b71d08528f0 child 68561 5e85cda58af6 permissions -rw-r--r--
More on Algebra by Paulo and Martin
```     1 (*  Title:      HOL/Algebra/IntRing.thy
```
```     2     Author:     Stephan Hohe, TU Muenchen
```
```     3     Author:     Clemens Ballarin
```
```     4 *)
```
```     5
```
```     6 theory IntRing
```
```     7 imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
```
```     8 begin
```
```     9
```
```    10 section \<open>The Ring of Integers\<close>
```
```    11
```
```    12 subsection \<open>Some properties of @{typ int}\<close>
```
```    13
```
```    14 lemma dvds_eq_abseq:
```
```    15   fixes k :: int
```
```    16   shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
```
```    17 apply rule
```
```    18  apply (simp add: zdvd_antisym_abs)
```
```    19 apply (simp add: dvd_if_abs_eq)
```
```    20 done
```
```    21
```
```    22
```
```    23 subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
```
```    24
```
```    25 abbreviation int_ring :: "int ring" ("\<Z>")
```
```    26   where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
```
```    27
```
```    28 lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
```
```    29   by simp
```
```    30
```
```    31 lemma int_is_cring: "cring \<Z>"
```
```    32 apply (rule cringI)
```
```    33   apply (rule abelian_groupI, simp_all)
```
```    34   defer 1
```
```    35   apply (rule comm_monoidI, simp_all)
```
```    36  apply (rule distrib_right)
```
```    37 apply (fast intro: left_minus)
```
```    38 done
```
```    39
```
```    40 (*
```
```    41 lemma int_is_domain:
```
```    42   "domain \<Z>"
```
```    43 apply (intro domain.intro domain_axioms.intro)
```
```    44   apply (rule int_is_cring)
```
```    45  apply (unfold int_ring_def, simp+)
```
```    46 done
```
```    47 *)
```
```    48
```
```    49
```
```    50 subsection \<open>Interpretations\<close>
```
```    51
```
```    52 text \<open>Since definitions of derived operations are global, their
```
```    53   interpretation needs to be done as early as possible --- that is,
```
```    54   with as few assumptions as possible.\<close>
```
```    55
```
```    56 interpretation int: monoid \<Z>
```
```    57   rewrites "carrier \<Z> = UNIV"
```
```    58     and "mult \<Z> x y = x * y"
```
```    59     and "one \<Z> = 1"
```
```    60     and "pow \<Z> x n = x^n"
```
```    61 proof -
```
```    62   \<comment> \<open>Specification\<close>
```
```    63   show "monoid \<Z>" by standard auto
```
```    64   then interpret int: monoid \<Z> .
```
```    65
```
```    66   \<comment> \<open>Carrier\<close>
```
```    67   show "carrier \<Z> = UNIV" by simp
```
```    68
```
```    69   \<comment> \<open>Operations\<close>
```
```    70   { fix x y show "mult \<Z> x y = x * y" by simp }
```
```    71   show "one \<Z> = 1" by simp
```
```    72   show "pow \<Z> x n = x^n" by (induct n) simp_all
```
```    73 qed
```
```    74
```
```    75 interpretation int: comm_monoid \<Z>
```
```    76   rewrites "finprod \<Z> f A = prod f A"
```
```    77 proof -
```
```    78   \<comment> \<open>Specification\<close>
```
```    79   show "comm_monoid \<Z>" by standard auto
```
```    80   then interpret int: comm_monoid \<Z> .
```
```    81
```
```    82   \<comment> \<open>Operations\<close>
```
```    83   { fix x y have "mult \<Z> x y = x * y" by simp }
```
```    84   note mult = this
```
```    85   have one: "one \<Z> = 1" by simp
```
```    86   show "finprod \<Z> f A = prod f A"
```
```    87     by (induct A rule: infinite_finite_induct, auto)
```
```    88 qed
```
```    89
```
```    90 interpretation int: abelian_monoid \<Z>
```
```    91   rewrites int_carrier_eq: "carrier \<Z> = UNIV"
```
```    92     and int_zero_eq: "zero \<Z> = 0"
```
```    93     and int_add_eq: "add \<Z> x y = x + y"
```
```    94     and int_finsum_eq: "finsum \<Z> f A = sum f A"
```
```    95 proof -
```
```    96   \<comment> \<open>Specification\<close>
```
```    97   show "abelian_monoid \<Z>" by standard auto
```
```    98   then interpret int: abelian_monoid \<Z> .
```
```    99
```
```   100   \<comment> \<open>Carrier\<close>
```
```   101   show "carrier \<Z> = UNIV" by simp
```
```   102
```
```   103   \<comment> \<open>Operations\<close>
```
```   104   { fix x y show "add \<Z> x y = x + y" by simp }
```
```   105   note add = this
```
```   106   show zero: "zero \<Z> = 0"
```
```   107     by simp
```
```   108   show "finsum \<Z> f A = sum f A"
```
```   109     by (induct A rule: infinite_finite_induct, auto)
```
```   110 qed
```
```   111
```
```   112 interpretation int: abelian_group \<Z>
```
```   113   (* The equations from the interpretation of abelian_monoid need to be repeated.
```
```   114      Since the morphisms through which the abelian structures are interpreted are
```
```   115      not the identity, the equations of these interpretations are not inherited. *)
```
```   116   (* FIXME *)
```
```   117   rewrites "carrier \<Z> = UNIV"
```
```   118     and "zero \<Z> = 0"
```
```   119     and "add \<Z> x y = x + y"
```
```   120     and "finsum \<Z> f A = sum f A"
```
```   121     and int_a_inv_eq: "a_inv \<Z> x = - x"
```
```   122     and int_a_minus_eq: "a_minus \<Z> x y = x - y"
```
```   123 proof -
```
```   124   \<comment> \<open>Specification\<close>
```
```   125   show "abelian_group \<Z>"
```
```   126   proof (rule abelian_groupI)
```
```   127     fix x
```
```   128     assume "x \<in> carrier \<Z>"
```
```   129     then show "\<exists>y \<in> carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
```
```   130       by simp arith
```
```   131   qed auto
```
```   132   then interpret int: abelian_group \<Z> .
```
```   133   \<comment> \<open>Operations\<close>
```
```   134   { fix x y have "add \<Z> x y = x + y" by simp }
```
```   135   note add = this
```
```   136   have zero: "zero \<Z> = 0" by simp
```
```   137   {
```
```   138     fix x
```
```   139     have "add \<Z> (- x) x = zero \<Z>"
```
```   140       by (simp add: add zero)
```
```   141     then show "a_inv \<Z> x = - x"
```
```   142       by (simp add: int.minus_equality)
```
```   143   }
```
```   144   note a_inv = this
```
```   145   show "a_minus \<Z> x y = x - y"
```
```   146     by (simp add: int.minus_eq add a_inv)
```
```   147 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
```
```   148
```
```   149 interpretation int: "domain" \<Z>
```
```   150   rewrites "carrier \<Z> = UNIV"
```
```   151     and "zero \<Z> = 0"
```
```   152     and "add \<Z> x y = x + y"
```
```   153     and "finsum \<Z> f A = sum f A"
```
```   154     and "a_inv \<Z> x = - x"
```
```   155     and "a_minus \<Z> x y = x - y"
```
```   156 proof -
```
```   157   show "domain \<Z>"
```
```   158     by unfold_locales (auto simp: distrib_right distrib_left)
```
```   159 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
```
```   160
```
```   161
```
```   162 text \<open>Removal of occurrences of @{term UNIV} in interpretation result
```
```   163   --- experimental.\<close>
```
```   164
```
```   165 lemma UNIV:
```
```   166   "x \<in> UNIV \<longleftrightarrow> True"
```
```   167   "A \<subseteq> UNIV \<longleftrightarrow> True"
```
```   168   "(\<forall>x \<in> UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
```
```   169   "(\<exists>x \<in> UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
```
```   170   "(True \<longrightarrow> Q) \<longleftrightarrow> Q"
```
```   171   "(True \<Longrightarrow> PROP R) \<equiv> PROP R"
```
```   172   by simp_all
```
```   173
```
```   174 interpretation int (* FIXME [unfolded UNIV] *) :
```
```   175   partial_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
```
```   176   rewrites "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV"
```
```   177     and "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x \<le> y)"
```
```   178     and "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)"
```
```   179 proof -
```
```   180   show "partial_order \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
```
```   181     by standard simp_all
```
```   182   show "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV"
```
```   183     by simp
```
```   184   show "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x \<le> y)"
```
```   185     by simp
```
```   186   show "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)"
```
```   187     by (simp add: lless_def) auto
```
```   188 qed
```
```   189
```
```   190 interpretation int (* FIXME [unfolded UNIV] *) :
```
```   191   lattice "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
```
```   192   rewrites "join \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = max x y"
```
```   193     and "meet \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = min x y"
```
```   194 proof -
```
```   195   let ?Z = "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
```
```   196   show "lattice ?Z"
```
```   197     apply unfold_locales
```
```   198     apply (simp add: least_def Upper_def)
```
```   199     apply arith
```
```   200     apply (simp add: greatest_def Lower_def)
```
```   201     apply arith
```
```   202     done
```
```   203   then interpret int: lattice "?Z" .
```
```   204   show "join ?Z x y = max x y"
```
```   205     apply (rule int.joinI)
```
```   206     apply (simp_all add: least_def Upper_def)
```
```   207     apply arith
```
```   208     done
```
```   209   show "meet ?Z x y = min x y"
```
```   210     apply (rule int.meetI)
```
```   211     apply (simp_all add: greatest_def Lower_def)
```
```   212     apply arith
```
```   213     done
```
```   214 qed
```
```   215
```
```   216 interpretation int (* [unfolded UNIV] *) :
```
```   217   total_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
```
```   218   by standard clarsimp
```
```   219
```
```   220
```
```   221 subsection \<open>Generated Ideals of \<open>\<Z>\<close>\<close>
```
```   222
```
```   223 lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
```
```   224   apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
```
```   225   apply (simp add: cgenideal_def)
```
```   226   done
```
```   227
```
```   228 lemma multiples_principalideal: "principalideal {x * a | x. True } \<Z>"
```
```   229   by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
```
```   230
```
```   231 lemma prime_primeideal:
```
```   232   assumes prime: "Factorial_Ring.prime p"
```
```   233   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
```
```   234 apply (rule primeidealI)
```
```   235    apply (rule int.genideal_ideal, simp)
```
```   236   apply (rule int_is_cring)
```
```   237  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
```
```   238  apply clarsimp defer 1
```
```   239  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
```
```   240  apply (elim exE)
```
```   241 proof -
```
```   242   fix a b x
```
```   243   assume "a * b = x * p"
```
```   244   then have "p dvd a * b" by simp
```
```   245   then have "p dvd a \<or> p dvd b"
```
```   246     by (metis prime prime_dvd_mult_eq_int)
```
```   247   then show "(\<exists>x. a = x * p) \<or> (\<exists>x. b = x * p)"
```
```   248     by (metis dvd_def mult.commute)
```
```   249 next
```
```   250   assume "UNIV = {uu. \<exists>x. uu = x * p}"
```
```   251   then obtain x where "1 = x * p"
```
```   252     by best
```
```   253   then have "\<bar>p * x\<bar> = 1"
```
```   254     by (simp add: ac_simps)
```
```   255   then show False using prime
```
```   256     by (auto simp add: abs_mult zmult_eq_1_iff)
```
```   257 qed
```
```   258
```
```   259
```
```   260 subsection \<open>Ideals and Divisibility\<close>
```
```   261
```
```   262 lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
```
```   263   by (rule int.Idl_subset_ideal') simp_all
```
```   264
```
```   265 lemma Idl_subset_eq_dvd: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> l dvd k"
```
```   266   apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
```
```   267   apply (rule, clarify)
```
```   268   apply (simp add: dvd_def)
```
```   269   apply (simp add: dvd_def ac_simps)
```
```   270   done
```
```   271
```
```   272 lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
```
```   273 proof -
```
```   274   have a: "l dvd k \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})"
```
```   275     by (rule Idl_subset_eq_dvd[symmetric])
```
```   276   have b: "k dvd l \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})"
```
```   277     by (rule Idl_subset_eq_dvd[symmetric])
```
```   278
```
```   279   have "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<and> Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k}"
```
```   280     by (subst a, subst b, simp)
```
```   281   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} \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
```
```   282     by blast
```
```   283   finally show ?thesis .
```
```   284 qed
```
```   285
```
```   286 lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
```
```   287   apply (subst dvds_eq_abseq[symmetric])
```
```   288   apply (rule dvds_eq_Idl[symmetric])
```
```   289   done
```
```   290
```
```   291
```
```   292 subsection \<open>Ideals and the Modulus\<close>
```
```   293
```
```   294 definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set"
```
```   295   where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
```
```   296
```
```   297 lemmas ZMod_defs =
```
```   298   ZMod_def genideal_def
```
```   299
```
```   300 lemma rcos_zfact:
```
```   301   assumes kIl: "k \<in> ZMod l r"
```
```   302   shows "\<exists>x. k = x * l + r"
```
```   303 proof -
```
```   304   from kIl[unfolded ZMod_def] have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r"
```
```   305     by (simp add: a_r_coset_defs)
```
```   306   then obtain xl where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" and k: "k = xl + r"
```
```   307     by auto
```
```   308   from xl obtain x where "xl = x * l"
```
```   309     by (auto simp: int_Idl)
```
```   310   with k have "k = x * l + r"
```
```   311     by simp
```
```   312   then show "\<exists>x. k = x * l + r" ..
```
```   313 qed
```
```   314
```
```   315 lemma ZMod_imp_zmod:
```
```   316   assumes zmods: "ZMod m a = ZMod m b"
```
```   317   shows "a mod m = b mod m"
```
```   318 proof -
```
```   319   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
```
```   320     by (rule int.genideal_ideal) fast
```
```   321   from zmods have "b \<in> ZMod m a"
```
```   322     unfolding ZMod_def by (simp add: a_repr_independenceD)
```
```   323   then have "\<exists>x. b = x * m + a"
```
```   324     by (rule rcos_zfact)
```
```   325   then obtain x where "b = x * m + a"
```
```   326     by fast
```
```   327   then have "b mod m = (x * m + a) mod m"
```
```   328     by simp
```
```   329   also have "\<dots> = ((x * m) mod m) + (a mod m)"
```
```   330     by (simp add: mod_add_eq)
```
```   331   also have "\<dots> = a mod m"
```
```   332     by simp
```
```   333   finally have "b mod m = a mod m" .
```
```   334   then show "a mod m = b mod m" ..
```
```   335 qed
```
```   336
```
```   337 lemma ZMod_mod: "ZMod m a = ZMod m (a mod m)"
```
```   338 proof -
```
```   339   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
```
```   340     by (rule int.genideal_ideal) fast
```
```   341   show ?thesis
```
```   342     unfolding ZMod_def
```
```   343     apply (rule a_repr_independence'[symmetric])
```
```   344     apply (simp add: int_Idl a_r_coset_defs)
```
```   345   proof -
```
```   346     have "a = m * (a div m) + (a mod m)"
```
```   347       by (simp add: mult_div_mod_eq [symmetric])
```
```   348     then have "a = (a div m) * m + (a mod m)"
```
```   349       by simp
```
```   350     then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m"
```
```   351       by fast
```
```   352   qed simp
```
```   353 qed
```
```   354
```
```   355 lemma zmod_imp_ZMod:
```
```   356   assumes modeq: "a mod m = b mod m"
```
```   357   shows "ZMod m a = ZMod m b"
```
```   358 proof -
```
```   359   have "ZMod m a = ZMod m (a mod m)"
```
```   360     by (rule ZMod_mod)
```
```   361   also have "\<dots> = ZMod m (b mod m)"
```
```   362     by (simp add: modeq[symmetric])
```
```   363   also have "\<dots> = ZMod m b"
```
```   364     by (rule ZMod_mod[symmetric])
```
```   365   finally show ?thesis .
```
```   366 qed
```
```   367
```
```   368 corollary ZMod_eq_mod: "ZMod m a = ZMod m b \<longleftrightarrow> a mod m = b mod m"
```
```   369   apply (rule iffI)
```
```   370   apply (erule ZMod_imp_zmod)
```
```   371   apply (erule zmod_imp_ZMod)
```
```   372   done
```
```   373
```
```   374
```
```   375 subsection \<open>Factorization\<close>
```
```   376
```
```   377 definition ZFact :: "int \<Rightarrow> int set ring"
```
```   378   where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
```
```   379
```
```   380 lemmas ZFact_defs = ZFact_def FactRing_def
```
```   381
```
```   382 lemma ZFact_is_cring: "cring (ZFact k)"
```
```   383   apply (unfold ZFact_def)
```
```   384   apply (rule ideal.quotient_is_cring)
```
```   385    apply (intro ring.genideal_ideal)
```
```   386     apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
```
```   387    apply simp
```
```   388   apply (rule int_is_cring)
```
```   389   done
```
```   390
```
```   391 lemma ZFact_zero: "carrier (ZFact 0) = (\<Union>a. {{a}})"
```
```   392   apply (insert int.genideal_zero)
```
```   393   apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def)
```
```   394   done
```
```   395
```
```   396 lemma ZFact_one: "carrier (ZFact 1) = {UNIV}"
```
```   397   apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
```
```   398   apply (subst int.genideal_one)
```
```   399   apply (rule, rule, clarsimp)
```
```   400    apply (rule, rule, clarsimp)
```
```   401    apply (rule, clarsimp, arith)
```
```   402   apply (rule, clarsimp)
```
```   403   apply (rule exI[of _ "0"], clarsimp)
```
```   404   done
```
```   405
```
```   406 lemma ZFact_prime_is_domain:
```
```   407   assumes pprime: "Factorial_Ring.prime p"
```
```   408   shows "domain (ZFact p)"
```
```   409   apply (unfold ZFact_def)
```
```   410   apply (rule primeideal.quotient_is_domain)
```
```   411   apply (rule prime_primeideal[OF pprime])
```
```   412   done
```
```   413
```
```   414 end
```