ballarin@20318: (*
ballarin@20318:   Title:     HOL/Algebra/IntRing.thy
ballarin@20318:   Author:    Stephan Hohe, TU Muenchen
ballarin@20318: *)
ballarin@20318: 
ballarin@20318: theory IntRing
haftmann@28823: imports QuotRing Lattice Int Primes
ballarin@20318: begin
ballarin@20318: 
ballarin@20318: 
ballarin@20318: section {* The Ring of Integers *}
ballarin@20318: 
ballarin@20318: subsection {* Some properties of @{typ int} *}
ballarin@20318: 
ballarin@20318: lemma dvds_imp_abseq:
ballarin@20318:   "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)"
ballarin@20318: apply (subst abs_split, rule conjI)
ballarin@20318:  apply (clarsimp, subst abs_split, rule conjI)
ballarin@20318:   apply (clarsimp)
ballarin@20318:   apply (cases "k=0", simp)
ballarin@20318:   apply (cases "l=0", simp)
ballarin@20318:   apply (simp add: zdvd_anti_sym)
ballarin@20318:  apply clarsimp
ballarin@20318:  apply (cases "k=0", simp)
ballarin@20318:  apply (simp add: zdvd_anti_sym)
ballarin@20318: apply (clarsimp, subst abs_split, rule conjI)
ballarin@20318:  apply (clarsimp)
ballarin@20318:  apply (cases "l=0", simp)
ballarin@20318:  apply (simp add: zdvd_anti_sym)
ballarin@20318: apply (clarsimp)
ballarin@20318: apply (subgoal_tac "-l = -k", simp)
ballarin@20318: apply (intro zdvd_anti_sym, simp+)
ballarin@20318: done
ballarin@20318: 
ballarin@20318: lemma abseq_imp_dvd:
ballarin@20318:   assumes a_lk: "abs l = abs (k::int)"
ballarin@20318:   shows "l dvd k"
ballarin@20318: proof -
ballarin@20318:   from a_lk
ballarin@20318:       have "nat (abs l) = nat (abs k)" by simp
ballarin@20318:   hence "nat (abs l) dvd nat (abs k)" by simp
ballarin@20318:   hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff)
ballarin@20318:   hence "abs l dvd k" by simp
ballarin@20318:   thus "l dvd k" 
ballarin@20318:   apply (unfold dvd_def, cases "l<0")
ballarin@20318:    defer 1 apply clarsimp
ballarin@20318:   proof (clarsimp)
ballarin@20318:     fix k
ballarin@20318:     assume l0: "l < 0"
ballarin@20318:     have "- (l * k) = l * (-k)" by simp
ballarin@20318:     thus "\<exists>ka. - (l * k) = l * ka" by fast
ballarin@20318:   qed
ballarin@20318: qed
ballarin@20318: 
ballarin@20318: lemma dvds_eq_abseq:
ballarin@20318:   "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
ballarin@20318: apply rule
ballarin@20318:  apply (simp add: dvds_imp_abseq)
ballarin@20318: apply (rule conjI)
ballarin@20318:  apply (simp add: abseq_imp_dvd)+
ballarin@20318: done
ballarin@20318: 
ballarin@20318: 
ballarin@27717: subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
ballarin@20318: 
ballarin@20318: constdefs
ballarin@20318:   int_ring :: "int ring" ("\<Z>")
ballarin@20318:   "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
ballarin@20318: 
ballarin@23957: lemma int_Zcarr [intro!, simp]:
ballarin@20318:   "k \<in> carrier \<Z>"
ballarin@23957:   by (simp add: int_ring_def)
ballarin@20318: 
ballarin@20318: lemma int_is_cring:
ballarin@20318:   "cring \<Z>"
ballarin@20318: unfolding int_ring_def
ballarin@20318: apply (rule cringI)
ballarin@20318:   apply (rule abelian_groupI, simp_all)
ballarin@20318:   defer 1
ballarin@20318:   apply (rule comm_monoidI, simp_all)
ballarin@20318:  apply (rule zadd_zmult_distrib)
ballarin@20318: apply (fast intro: zadd_zminus_inverse2)
ballarin@20318: done
ballarin@20318: 
ballarin@23957: (*
ballarin@20318: lemma int_is_domain:
ballarin@20318:   "domain \<Z>"
ballarin@20318: apply (intro domain.intro domain_axioms.intro)
ballarin@20318:   apply (rule int_is_cring)
ballarin@20318:  apply (unfold int_ring_def, simp+)
ballarin@20318: done
ballarin@23957: *)
ballarin@27717: subsection {* Interpretations *}
ballarin@20318: 
ballarin@23957: text {* Since definitions of derived operations are global, their
ballarin@23957:   interpretation needs to be done as early as possible --- that is,
ballarin@23957:   with as few assumptions as possible. *}
ballarin@23957: 
ballarin@29237: interpretation int!: monoid \<Z>
ballarin@23957:   where "carrier \<Z> = UNIV"
ballarin@23957:     and "mult \<Z> x y = x * y"
ballarin@23957:     and "one \<Z> = 1"
ballarin@23957:     and "pow \<Z> x n = x^n"
ballarin@23957: proof -
ballarin@23957:   -- "Specification"
haftmann@28823:   show "monoid \<Z>" proof qed (auto simp: int_ring_def)
ballarin@29237:   then interpret int!: monoid \<Z> .
ballarin@23957: 
ballarin@23957:   -- "Carrier"
ballarin@23957:   show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
ballarin@23957: 
ballarin@23957:   -- "Operations"
ballarin@23957:   { fix x y show "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
ballarin@23957:   note mult = this
ballarin@23957:   show one: "one \<Z> = 1" by (simp add: int_ring_def)
ballarin@23957:   show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
ballarin@23957: qed
ballarin@23957: 
ballarin@29237: interpretation int!: comm_monoid \<Z>
haftmann@28524:   where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
ballarin@23957: proof -
ballarin@23957:   -- "Specification"
haftmann@28823:   show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
ballarin@29237:   then interpret int!: comm_monoid \<Z> .
ballarin@23957: 
ballarin@23957:   -- "Operations"
ballarin@23957:   { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
ballarin@23957:   note mult = this
ballarin@23957:   have one: "one \<Z> = 1" by (simp add: int_ring_def)
haftmann@28524:   show "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
ballarin@23957:   proof (cases "finite A")
ballarin@23957:     case True then show ?thesis proof induct
ballarin@23957:       case empty show ?case by (simp add: one)
ballarin@23957:     next
ballarin@23957:       case insert then show ?case by (simp add: Pi_def mult)
ballarin@23957:     qed
ballarin@23957:   next
ballarin@23957:     case False then show ?thesis by (simp add: finprod_def)
ballarin@23957:   qed
ballarin@23957: qed
ballarin@23957: 
ballarin@29237: interpretation int!: abelian_monoid \<Z>
ballarin@23957:   where "zero \<Z> = 0"
ballarin@23957:     and "add \<Z> x y = x + y"
haftmann@28524:     and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
ballarin@23957: proof -
ballarin@23957:   -- "Specification"
haftmann@28823:   show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
ballarin@29237:   then interpret int!: abelian_monoid \<Z> .
ballarin@20318: 
ballarin@23957:   -- "Operations"
ballarin@23957:   { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
ballarin@23957:   note add = this
ballarin@23957:   show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
haftmann@28524:   show "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
ballarin@23957:   proof (cases "finite A")
ballarin@23957:     case True then show ?thesis proof induct
ballarin@23957:       case empty show ?case by (simp add: zero)
ballarin@23957:     next
ballarin@23957:       case insert then show ?case by (simp add: Pi_def add)
ballarin@23957:     qed
ballarin@23957:   next
ballarin@23957:     case False then show ?thesis by (simp add: finsum_def finprod_def)
ballarin@23957:   qed
ballarin@23957: qed
ballarin@23957: 
ballarin@29237: interpretation int!: abelian_group \<Z>
ballarin@23957:   where "a_inv \<Z> x = - x"
ballarin@23957:     and "a_minus \<Z> x y = x - y"
ballarin@23957: proof -
ballarin@23957:   -- "Specification"
ballarin@23957:   show "abelian_group \<Z>"
ballarin@23957:   proof (rule abelian_groupI)
ballarin@23957:     show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
ballarin@23957:       by (simp add: int_ring_def) arith
ballarin@23957:   qed (auto simp: int_ring_def)
ballarin@29237:   then interpret int!: abelian_group \<Z> .
ballarin@23957: 
ballarin@23957:   -- "Operations"
ballarin@23957:   { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
ballarin@23957:   note add = this
ballarin@23957:   have zero: "zero \<Z> = 0" by (simp add: int_ring_def)
ballarin@23957:   { fix x
ballarin@23957:     have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero)
ballarin@23957:     then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) }
ballarin@23957:   note a_inv = this
ballarin@23957:   show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
ballarin@23957: qed
ballarin@23957: 
ballarin@29237: interpretation int!: "domain" \<Z>
haftmann@28823:   proof qed (auto simp: int_ring_def left_distrib right_distrib)
ballarin@23957: 
ballarin@23957: 
ballarin@24131: text {* Removal of occurrences of @{term UNIV} in interpretation result
ballarin@24131:   --- experimental. *}
ballarin@24131: 
ballarin@24131: lemma UNIV:
ballarin@24131:   "x \<in> UNIV = True"
ballarin@24131:   "A \<subseteq> UNIV = True"
ballarin@24131:   "(ALL x : UNIV. P x) = (ALL x. P x)"
ballarin@24131:   "(EX x : UNIV. P x) = (EX x. P x)"
ballarin@24131:   "(True --> Q) = Q"
ballarin@24131:   "(True ==> PROP R) == PROP R"
ballarin@24131:   by simp_all
ballarin@24131: 
ballarin@29237: interpretation int! (* FIXME [unfolded UNIV] *) :
ballarin@29237:   partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
ballarin@27713:   where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
ballarin@27713:     and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
ballarin@27713:     and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
ballarin@23957: proof -
ballarin@27713:   show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
haftmann@28823:     proof qed simp_all
ballarin@27713:   show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
ballarin@24131:     by simp
ballarin@27713:   show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
ballarin@24131:     by simp
ballarin@27713:   show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
ballarin@23957:     by (simp add: lless_def) auto
ballarin@23957: qed
ballarin@23957: 
ballarin@29237: interpretation int! (* FIXME [unfolded UNIV] *) :
ballarin@29237:   lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
ballarin@27713:   where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
ballarin@27713:     and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
ballarin@23957: proof -
ballarin@27713:   let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
ballarin@23957:   show "lattice ?Z"
ballarin@23957:     apply unfold_locales
ballarin@23957:     apply (simp add: least_def Upper_def)
ballarin@23957:     apply arith
ballarin@23957:     apply (simp add: greatest_def Lower_def)
ballarin@23957:     apply arith
ballarin@23957:     done
ballarin@29237:   then interpret int!: lattice "?Z" .
ballarin@23957:   show "join ?Z x y = max x y"
ballarin@23957:     apply (rule int.joinI)
ballarin@23957:     apply (simp_all add: least_def Upper_def)
ballarin@23957:     apply arith
ballarin@23957:     done
ballarin@23957:   show "meet ?Z x y = min x y"
ballarin@23957:     apply (rule int.meetI)
ballarin@23957:     apply (simp_all add: greatest_def Lower_def)
ballarin@23957:     apply arith
ballarin@23957:     done
ballarin@23957: qed
ballarin@23957: 
ballarin@29237: interpretation int! (* [unfolded UNIV] *) :
ballarin@29237:   total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
haftmann@28823:   proof qed clarsimp
ballarin@23957: 
ballarin@20318: 
ballarin@27717: subsection {* Generated Ideals of @{text "\<Z>"} *}
ballarin@20318: 
ballarin@20318: lemma int_Idl:
ballarin@20318:   "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
ballarin@23957:   apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)
ballarin@23957:   apply (simp add: cgenideal_def int_ring_def)
ballarin@23957:   done
ballarin@20318: 
ballarin@20318: lemma multiples_principalideal:
ballarin@20318:   "principalideal {x * a | x. True } \<Z>"
ballarin@20318: apply (subst int_Idl[symmetric], rule principalidealI)
ballarin@23957:  apply (rule int.genideal_ideal, simp)
ballarin@20318: apply fast
ballarin@20318: done
ballarin@20318: 
nipkow@29700: 
ballarin@20318: lemma prime_primeideal:
ballarin@20318:   assumes prime: "prime (nat p)"
ballarin@20318:   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
ballarin@20318: apply (rule primeidealI)
ballarin@23957:    apply (rule int.genideal_ideal, simp)
ballarin@20318:   apply (rule int_is_cring)
ballarin@23957:  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
ballarin@20318:  apply (simp add: int_ring_def)
ballarin@20318:  apply clarsimp defer 1
ballarin@23957:  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
ballarin@20318:  apply (simp add: int_ring_def)
ballarin@20318:  apply (elim exE)
ballarin@20318: proof -
ballarin@20318:   fix a b x
ballarin@20318: 
ballarin@20318:   from prime
ballarin@20318:       have ppos: "0 <= p" by (simp add: prime_def)
ballarin@20318:   have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
ballarin@20318:   proof -
ballarin@20318:     fix x
ballarin@20318:     assume "nat p dvd nat (abs x)"
ballarin@20318:     hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
ballarin@20318:     thus "p dvd x" by (simp add: ppos)
ballarin@20318:   qed
ballarin@20318: 
ballarin@20318: 
ballarin@20318:   assume "a * b = x * p"
ballarin@20318:   hence "p dvd a * b" by simp
nipkow@29700:   hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
ballarin@20318:   hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
ballarin@20318:   hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
ballarin@20318:   hence "p dvd a | p dvd b" by (fast intro: unnat)
ballarin@20318:   thus "(EX x. a = x * p) | (EX x. b = x * p)"
ballarin@20318:   proof
ballarin@20318:     assume "p dvd a"
ballarin@20318:     hence "EX x. a = p * x" by (simp add: dvd_def)
ballarin@20318:     from this obtain x
ballarin@20318:         where "a = p * x" by fast
ballarin@20318:     hence "a = x * p" by simp
ballarin@20318:     hence "EX x. a = x * p" by simp
ballarin@20318:     thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
ballarin@20318:   next
ballarin@20318:     assume "p dvd b"
ballarin@20318:     hence "EX x. b = p * x" by (simp add: dvd_def)
ballarin@20318:     from this obtain x
ballarin@20318:         where "b = p * x" by fast
ballarin@20318:     hence "b = x * p" by simp
ballarin@20318:     hence "EX x. b = x * p" by simp
ballarin@20318:     thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
ballarin@20318:   qed
ballarin@20318: next
ballarin@20318:   assume "UNIV = {uu. EX x. uu = x * p}"
ballarin@20318:   from this obtain x 
ballarin@29242:       where "1 = x * p" by best
ballarin@20318:   from this [symmetric]
ballarin@20318:       have "p * x = 1" by (subst zmult_commute)
ballarin@20318:   hence "\<bar>p * x\<bar> = 1" by simp
ballarin@20318:   hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
ballarin@20318:   from this and prime
ballarin@20318:       show "False" by (simp add: prime_def)
ballarin@20318: qed
ballarin@20318: 
ballarin@20318: 
ballarin@27717: subsection {* Ideals and Divisibility *}
ballarin@20318: 
ballarin@20318: lemma int_Idl_subset_ideal:
ballarin@20318:   "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
ballarin@23957: by (rule int.Idl_subset_ideal', simp+)
ballarin@20318: 
ballarin@20318: lemma Idl_subset_eq_dvd:
ballarin@20318:   "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
ballarin@20318: apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
ballarin@20318: apply (rule, clarify)
wenzelm@29424: apply (simp add: dvd_def)
wenzelm@29424: apply (simp add: dvd_def mult_ac)
ballarin@20318: done
ballarin@20318: 
ballarin@20318: lemma dvds_eq_Idl:
ballarin@20318:   "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
ballarin@20318: proof -
ballarin@20318:   have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric])
ballarin@20318:   have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric])
ballarin@20318: 
ballarin@20318:   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}))"
ballarin@20318:   by (subst a, subst b, simp)
ballarin@20318:   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+)
ballarin@20318:   finally
ballarin@20318:     show ?thesis .
ballarin@20318: qed
ballarin@20318: 
ballarin@20318: lemma Idl_eq_abs:
ballarin@20318:   "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)"
ballarin@20318: apply (subst dvds_eq_abseq[symmetric])
ballarin@20318: apply (rule dvds_eq_Idl[symmetric])
ballarin@20318: done
ballarin@20318: 
ballarin@20318: 
ballarin@27717: subsection {* Ideals and the Modulus *}
ballarin@20318: 
ballarin@20318: constdefs
ballarin@20318:    ZMod :: "int => int => int set"
ballarin@20318:   "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
ballarin@20318: 
ballarin@20318: lemmas ZMod_defs =
ballarin@20318:   ZMod_def genideal_def
ballarin@20318: 
ballarin@20318: lemma rcos_zfact:
ballarin@20318:   assumes kIl: "k \<in> ZMod l r"
ballarin@20318:   shows "EX x. k = x * l + r"
ballarin@20318: proof -
ballarin@20318:   from kIl[unfolded ZMod_def]
ballarin@20318:       have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def)
ballarin@20318:   from this obtain xl
ballarin@20318:       where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
ballarin@20318:       and k: "k = xl + r"
ballarin@20318:       by auto
ballarin@20318:   from xl obtain x
ballarin@20318:       where "xl = x * l"
ballarin@20318:       by (simp add: int_Idl, fast)
ballarin@20318:   from k and this
ballarin@20318:       have "k = x * l + r" by simp
ballarin@20318:   thus "\<exists>x. k = x * l + r" ..
ballarin@20318: qed
ballarin@20318: 
ballarin@20318: lemma ZMod_imp_zmod:
ballarin@20318:   assumes zmods: "ZMod m a = ZMod m b"
ballarin@20318:   shows "a mod m = b mod m"
ballarin@20318: proof -
ballarin@29237:   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
ballarin@20318:   from zmods
ballarin@20318:       have "b \<in> ZMod m a"
ballarin@20318:       unfolding ZMod_def
ballarin@20318:       by (simp add: a_repr_independenceD)
ballarin@20318:   from this
ballarin@20318:       have "EX x. b = x * m + a" by (rule rcos_zfact)
ballarin@20318:   from this obtain x
ballarin@20318:       where "b = x * m + a"
ballarin@20318:       by fast
ballarin@20318: 
ballarin@20318:   hence "b mod m = (x * m + a) mod m" by simp
ballarin@20318:   also
ballarin@20318:       have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
ballarin@20318:   also
ballarin@20318:       have "\<dots> = a mod m" by simp
ballarin@20318:   finally
ballarin@20318:       have "b mod m = a mod m" .
ballarin@20318:   thus "a mod m = b mod m" ..
ballarin@20318: qed
ballarin@20318: 
ballarin@20318: lemma ZMod_mod:
ballarin@20318:   shows "ZMod m a = ZMod m (a mod m)"
ballarin@20318: proof -
ballarin@29237:   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
ballarin@20318:   show ?thesis
ballarin@20318:       unfolding ZMod_def
ballarin@20318:   apply (rule a_repr_independence'[symmetric])
ballarin@20318:   apply (simp add: int_Idl a_r_coset_defs)
ballarin@20318:   apply (simp add: int_ring_def)
ballarin@20318:   proof -
ballarin@20318:     have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
ballarin@20318:     hence "a = (a div m) * m + (a mod m)" by simp
ballarin@20318:     thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast
ballarin@20318:   qed simp
ballarin@20318: qed
ballarin@20318: 
ballarin@20318: lemma zmod_imp_ZMod:
ballarin@20318:   assumes modeq: "a mod m = b mod m"
ballarin@20318:   shows "ZMod m a = ZMod m b"
ballarin@20318: proof -
ballarin@20318:   have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod)
ballarin@20318:   also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
ballarin@20318:   also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
ballarin@20318:   finally show ?thesis .
ballarin@20318: qed
ballarin@20318: 
ballarin@20318: corollary ZMod_eq_mod:
ballarin@20318:   shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
ballarin@20318: by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
ballarin@20318: 
ballarin@20318: 
ballarin@27717: subsection {* Factorization *}
ballarin@20318: 
ballarin@20318: constdefs
ballarin@20318:   ZFact :: "int \<Rightarrow> int set ring"
ballarin@20318:   "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
ballarin@20318: 
ballarin@20318: lemmas ZFact_defs = ZFact_def FactRing_def
ballarin@20318: 
ballarin@20318: lemma ZFact_is_cring:
ballarin@20318:   shows "cring (ZFact k)"
ballarin@20318: apply (unfold ZFact_def)
ballarin@20318: apply (rule ideal.quotient_is_cring)
ballarin@20318:  apply (intro ring.genideal_ideal)
ballarin@20318:   apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
ballarin@20318:  apply simp
ballarin@20318: apply (rule int_is_cring)
ballarin@20318: done
ballarin@20318: 
ballarin@20318: lemma ZFact_zero:
ballarin@20318:   "carrier (ZFact 0) = (\<Union>a. {{a}})"
ballarin@23957: apply (insert int.genideal_zero)
ballarin@20318: apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
ballarin@20318: done
ballarin@20318: 
ballarin@20318: lemma ZFact_one:
ballarin@20318:   "carrier (ZFact 1) = {UNIV}"
ballarin@20318: apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
ballarin@23957: apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps])
ballarin@20318: apply (rule, rule, clarsimp)
ballarin@20318:  apply (rule, rule, clarsimp)
ballarin@20318:  apply (rule, clarsimp, arith)
ballarin@20318: apply (rule, clarsimp)
ballarin@20318: apply (rule exI[of _ "0"], clarsimp)
ballarin@20318: done
ballarin@20318: 
ballarin@20318: lemma ZFact_prime_is_domain:
ballarin@20318:   assumes pprime: "prime (nat p)"
ballarin@20318:   shows "domain (ZFact p)"
ballarin@20318: apply (unfold ZFact_def)
ballarin@20318: apply (rule primeideal.quotient_is_domain)
ballarin@20318: apply (rule prime_primeideal[OF pprime])
ballarin@20318: done
ballarin@20318: 
ballarin@20318: end