src/HOL/Algebra/IntRing.thy
author haftmann
Thu Apr 06 21:37:13 2017 +0200 (2017-04-06)
changeset 65417 fc41a5650fb1
parent 64272 f76b6dda2e56
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
session containing computational algebra
     1 (*  Title:      HOL/Algebra/IntRing.thy
     2     Author:     Stephan Hohe, TU Muenchen
     3     Author:     Clemens Ballarin
     4 *)
     5 
     6 theory IntRing
     7 imports "~~/src/HOL/Computational_Algebra/Primes" QuotRing Lattice Int
     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 = op *, one = 1, zero = 0, add = op +\<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> "Specification"
    63   show "monoid \<Z>" by standard auto
    64   then interpret int: monoid \<Z> .
    65 
    66   \<comment> "Carrier"
    67   show "carrier \<Z> = UNIV" by simp
    68 
    69   \<comment> "Operations"
    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> "Specification"
    79   show "comm_monoid \<Z>" by standard auto
    80   then interpret int: comm_monoid \<Z> .
    81 
    82   \<comment> "Operations"
    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> "Specification"
    97   show "abelian_monoid \<Z>" by standard auto
    98   then interpret int: abelian_monoid \<Z> .
    99 
   100   \<comment> "Carrier"
   101   show "carrier \<Z> = UNIV" by simp
   102 
   103   \<comment> "Operations"
   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> "Specification"
   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> "Operations"
   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   "(EX x : UNIV. P x) \<longleftrightarrow> (EX 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 = op =, le = op \<le>\<rparr>"
   176   rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
   177     and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
   178     and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
   179 proof -
   180   show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
   181     by standard simp_all
   182   show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
   183     by simp
   184   show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
   185     by simp
   186   show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<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 = op =, le = op \<le>\<rparr>"
   192   rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
   193     and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
   194 proof -
   195   let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<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 = op =, le = op \<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: "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. EX x. uu = x * p}"
   251   then obtain x where "1 = x * p" by best
   252   then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
   253   then show False using prime
   254     by (auto dest!: abs_zmult_eq_1 simp: prime_def)
   255 qed
   256 
   257 
   258 subsection \<open>Ideals and Divisibility\<close>
   259 
   260 lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
   261   by (rule int.Idl_subset_ideal') simp_all
   262 
   263 lemma Idl_subset_eq_dvd: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> l dvd k"
   264   apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
   265   apply (rule, clarify)
   266   apply (simp add: dvd_def)
   267   apply (simp add: dvd_def ac_simps)
   268   done
   269 
   270 lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
   271 proof -
   272   have a: "l dvd k \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})"
   273     by (rule Idl_subset_eq_dvd[symmetric])
   274   have b: "k dvd l \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})"
   275     by (rule Idl_subset_eq_dvd[symmetric])
   276 
   277   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}"
   278     by (subst a, subst b, simp)
   279   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}"
   280     by blast
   281   finally show ?thesis .
   282 qed
   283 
   284 lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
   285   apply (subst dvds_eq_abseq[symmetric])
   286   apply (rule dvds_eq_Idl[symmetric])
   287   done
   288 
   289 
   290 subsection \<open>Ideals and the Modulus\<close>
   291 
   292 definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set"
   293   where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
   294 
   295 lemmas ZMod_defs =
   296   ZMod_def genideal_def
   297 
   298 lemma rcos_zfact:
   299   assumes kIl: "k \<in> ZMod l r"
   300   shows "\<exists>x. k = x * l + r"
   301 proof -
   302   from kIl[unfolded ZMod_def] have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r"
   303     by (simp add: a_r_coset_defs)
   304   then obtain xl where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" and k: "k = xl + r"
   305     by auto
   306   from xl obtain x where "xl = x * l"
   307     by (auto simp: int_Idl)
   308   with k have "k = x * l + r"
   309     by simp
   310   then show "\<exists>x. k = x * l + r" ..
   311 qed
   312 
   313 lemma ZMod_imp_zmod:
   314   assumes zmods: "ZMod m a = ZMod m b"
   315   shows "a mod m = b mod m"
   316 proof -
   317   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
   318     by (rule int.genideal_ideal) fast
   319   from zmods have "b \<in> ZMod m a"
   320     unfolding ZMod_def by (simp add: a_repr_independenceD)
   321   then have "\<exists>x. b = x * m + a"
   322     by (rule rcos_zfact)
   323   then obtain x where "b = x * m + a"
   324     by fast
   325   then have "b mod m = (x * m + a) mod m"
   326     by simp
   327   also have "\<dots> = ((x * m) mod m) + (a mod m)"
   328     by (simp add: mod_add_eq)
   329   also have "\<dots> = a mod m"
   330     by simp
   331   finally have "b mod m = a mod m" .
   332   then show "a mod m = b mod m" ..
   333 qed
   334 
   335 lemma ZMod_mod: "ZMod m a = ZMod m (a mod m)"
   336 proof -
   337   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
   338     by (rule int.genideal_ideal) fast
   339   show ?thesis
   340     unfolding ZMod_def
   341     apply (rule a_repr_independence'[symmetric])
   342     apply (simp add: int_Idl a_r_coset_defs)
   343   proof -
   344     have "a = m * (a div m) + (a mod m)"
   345       by (simp add: mult_div_mod_eq [symmetric])
   346     then have "a = (a div m) * m + (a mod m)"
   347       by simp
   348     then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m"
   349       by fast
   350   qed simp
   351 qed
   352 
   353 lemma zmod_imp_ZMod:
   354   assumes modeq: "a mod m = b mod m"
   355   shows "ZMod m a = ZMod m b"
   356 proof -
   357   have "ZMod m a = ZMod m (a mod m)"
   358     by (rule ZMod_mod)
   359   also have "\<dots> = ZMod m (b mod m)"
   360     by (simp add: modeq[symmetric])
   361   also have "\<dots> = ZMod m b"
   362     by (rule ZMod_mod[symmetric])
   363   finally show ?thesis .
   364 qed
   365 
   366 corollary ZMod_eq_mod: "ZMod m a = ZMod m b \<longleftrightarrow> a mod m = b mod m"
   367   apply (rule iffI)
   368   apply (erule ZMod_imp_zmod)
   369   apply (erule zmod_imp_ZMod)
   370   done
   371 
   372 
   373 subsection \<open>Factorization\<close>
   374 
   375 definition ZFact :: "int \<Rightarrow> int set ring"
   376   where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
   377 
   378 lemmas ZFact_defs = ZFact_def FactRing_def
   379 
   380 lemma ZFact_is_cring: "cring (ZFact k)"
   381   apply (unfold ZFact_def)
   382   apply (rule ideal.quotient_is_cring)
   383    apply (intro ring.genideal_ideal)
   384     apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
   385    apply simp
   386   apply (rule int_is_cring)
   387   done
   388 
   389 lemma ZFact_zero: "carrier (ZFact 0) = (\<Union>a. {{a}})"
   390   apply (insert int.genideal_zero)
   391   apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def)
   392   done
   393 
   394 lemma ZFact_one: "carrier (ZFact 1) = {UNIV}"
   395   apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
   396   apply (subst int.genideal_one)
   397   apply (rule, rule, clarsimp)
   398    apply (rule, rule, clarsimp)
   399    apply (rule, clarsimp, arith)
   400   apply (rule, clarsimp)
   401   apply (rule exI[of _ "0"], clarsimp)
   402   done
   403 
   404 lemma ZFact_prime_is_domain:
   405   assumes pprime: "prime p"
   406   shows "domain (ZFact p)"
   407   apply (unfold ZFact_def)
   408   apply (rule primeideal.quotient_is_domain)
   409   apply (rule prime_primeideal[OF pprime])
   410   done
   411 
   412 end