Quellcode-Bibliothek IntRing.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/IntRing.thy
    Author:     Stephan Hohe, TU Muenchen
    Author:     Clemens Ballarin
*)

theory IntRing
imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
begin

section \<open>The Ring of Integers\<close>

subsection \<open>Some properties of \<^typ>\<open>int\<close>\<close>

lemma dvds_eq_abseq:
  fixes k :: int
  shows "l dvd k \ k dvd l \ \l\ = \k\"
  by (metis dvd_if_abs_eq lcm.commute lcm_proj1_iff_int)

subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>

abbreviation int_ring :: "int ring" (\<open>\<Z>\<close>)
  where "int_ring \ \carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\"

lemma int_Zcarr [intro!, simp]: "k \ carrier \"
  by simp

lemma int_is_cring: "cring \"
proof (rule cringI)
  show "abelian_group \"
    by (rule abelian_groupI) (auto intro: left_minus)
  show "Group.comm_monoid \"
    by (simp add: Group.monoid.intro monoid.monoid_comm_monoidI)
qed (auto simp: distrib_right)

subsection \<open>Interpretations\<close>

text \<open>Since definitions of derived operations are global, their
  interpretation needs to be done as early as possible --- that is,
  with as few assumptions as possible.\<close>

interpretation int: monoid \<Z>
  rewrites "carrier \ = UNIV"
    and "mult \ x y = x * y"
    and "one \ = 1"
    and "pow \ x n = x^n"
proof -
  \<comment> \<open>Specification\<close>
  show "monoid \" by standard auto
  then interpret int: monoid \<Z> .

  \<comment> \<open>Carrier\<close>
  show "carrier \ = UNIV" by simp

  \<comment> \<open>Operations\<close>
  show "mult \ x y = x * y" for x y by simp
  show "one \ = 1" by simp
  show "pow \ x n = x^n" by (induct n) simp_all
qed

interpretation int: comm_monoid \<Z>
  rewrites "finprod \ f A = prod f A"
proof -
  \<comment> \<open>Specification\<close>
  show "comm_monoid \" by standard auto
  then interpret int: comm_monoid \<Z> .

  \<comment> \<open>Operations\<close>
  show "finprod \ f A = prod f A"
    by (induct A rule: infinite_finite_induct) auto
qed

interpretation int: abelian_monoid \<Z>
  rewrites int_carrier_eq: "carrier \ = UNIV"
    and int_zero_eq: "zero \ = 0"
    and int_add_eq: "add \ x y = x + y"
    and int_finsum_eq: "finsum \ f A = sum f A"
proof -
  \<comment> \<open>Specification\<close>
  show "abelian_monoid \" by standard auto
  then interpret int: abelian_monoid \<Z> .

  \<comment> \<open>Carrier\<close>
  show "carrier \ = UNIV" by simp

  \<comment> \<open>Operations\<close>
  show "add \ x y = x + y" for x y by simp
  show zero: "zero \ = 0" by simp
  show "finsum \ f A = sum f A"
    by (induct A rule: infinite_finite_induct) auto
qed

interpretation int: abelian_group \<Z>
  (* The equations from the interpretation of abelian_monoid need to be repeated.
     Since the morphisms through which the abelian structures are interpreted are
     not the identity, the equations of these interpretations are not inherited. *)
  (* FIXME *)
  rewrites "carrier \ = UNIV"
    and "zero \ = 0"
    and "add \ x y = x + y"
    and "finsum \ f A = sum f A"
    and int_a_inv_eq: "a_inv \ x = - x"
    and int_a_minus_eq: "a_minus \ x y = x - y"
proof -
  \<comment> \<open>Specification\<close>
  show "abelian_group \"
  proof (rule abelian_groupI)
    fix x
    assume "x \ carrier \"
    then show "\y \ carrier \. y \\<^bsub>\\<^esub> x = \\<^bsub>\\<^esub>"
      by simp arith
  qed auto
  then interpret int: abelian_group \<Z> .
  \<comment> \<open>Operations\<close>
  have add: "add \ x y = x + y" for x y by simp
  have zero: "zero \ = 0" by simp
  show a_inv: "a_inv \ x = - x" for x
  proof -
    have "add \ (- x) x = zero \"
      by (simp add: add zero)
    then show ?thesis
      by (simp add: int.minus_equality)
  qed
  show "a_minus \ x y = x - y"
    by (simp add: int.minus_eq add a_inv)
qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+

interpretation int: "domain" \<Z>
  rewrites "carrier \ = UNIV"
    and "zero \ = 0"
    and "add \ x y = x + y"
    and "finsum \ f A = sum f A"
    and "a_inv \ x = - x"
    and "a_minus \ x y = x - y"
proof -
  show "domain \"
    by unfold_locales (auto simp: distrib_right distrib_left)
qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+

text \<open>Removal of occurrences of \<^term>\<open>UNIV\<close> in interpretation result
  --- experimental.\<close>

lemma UNIV:
  "x \ UNIV \ True"
  "A \ UNIV \ True"
  "(\x \ UNIV. P x) \ (\x. P x)"
  "(\x \ UNIV. P x) \ (\x. P x)"
  "(True \ Q) \ Q"
  "(True \ PROP R) \ PROP R"
  by simp_all

interpretation int (* FIXME [unfolded UNIV] *) :
  partial_order "\carrier = UNIV::int set, eq = (=), le = (\)\"
  rewrites "carrier \carrier = UNIV::int set, eq = (=), le = (\)\ = UNIV"
    and "le \carrier = UNIV::int set, eq = (=), le = (\)\ x y = (x \ y)"
    and "lless \carrier = UNIV::int set, eq = (=), le = (\)\ x y = (x < y)"
proof -
  show "partial_order \carrier = UNIV::int set, eq = (=), le = (\)\"
    by standard simp_all
  show "carrier \carrier = UNIV::int set, eq = (=), le = (\)\ = UNIV"
    by simp
  show "le \carrier = UNIV::int set, eq = (=), le = (\)\ x y = (x \ y)"
    by simp
  show "lless \carrier = UNIV::int set, eq = (=), le = (\)\ x y = (x < y)"
    by (simp add: lless_def) auto
qed

interpretation int (* FIXME [unfolded UNIV] *) :
  lattice "\carrier = UNIV::int set, eq = (=), le = (\)\"
  rewrites "join \carrier = UNIV::int set, eq = (=), le = (\)\ x y = max x y"
    and "meet \carrier = UNIV::int set, eq = (=), le = (\)\ x y = min x y"
proof -
  let ?Z = "\carrier = UNIV::int set, eq = (=), le = (\)\"
  show "lattice ?Z"
    apply unfold_locales
    apply (simp_all add: least_def Upper_def greatest_def Lower_def)
    apply arith+
    done
  then interpret int: lattice "?Z" .
  show "join ?Z x y = max x y"
    by (metis int.le_iff_meet iso_tuple_UNIV_I join_comm linear max.absorb_iff2 max_def)
  show "meet ?Z x y = min x y"
    using int.meet_le int.meet_left int.meet_right by auto
qed

interpretation int (* [unfolded UNIV] *) :
  total_order "\carrier = UNIV::int set, eq = (=), le = (\)\"
  by standard clarsimp

subsection \<open>Generated Ideals of \<open>\<Z>\<close>\<close>

lemma int_Idl: "Idl\<^bsub>\\<^esub> {a} = {x * a | x. True}"
  by (simp_all add: cgenideal_def int.cgenideal_eq_genideal[symmetric])

lemma multiples_principalideal: "principalideal {x * a | x. True } \"
  by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)

lemma prime_primeideal:
  assumes prime: "Factorial_Ring.prime p"
  shows "primeideal (Idl\<^bsub>\\<^esub> {p}) \"
proof (rule primeidealI)
  show "ideal (Idl\<^bsub>\\<^esub> {p}) \"
    by (rule int.genideal_ideal, simp)
  show "cring \"
    by (rule int_is_cring)
  have False if "UNIV = {v::int. \x. v = x * p}"
  proof -
    from that
    obtain i where "1 = i * p"
      by (blast intro:  elim: )
    then show False
      using prime by (auto simp add: abs_mult zmult_eq_1_iff)
  qed
  then show "carrier \ \ Idl\<^bsub>\\<^esub> {p}"
    by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
  have "p dvd a \ p dvd b" if "a * b = x * p" for a b x
    by (simp add: prime prime_dvd_multD that)
  then show "\a b. \a \ carrier \; b \ carrier \; a \\<^bsub>\\<^esub> b \ Idl\<^bsub>\\<^esub> {p}\
           \<Longrightarrow> a \<in> Idl\<^bsub>\<Z>\<^esub> {p} \<or> b \<in> Idl\<^bsub>\<Z>\<^esub> {p}"
    by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def dvd_def mult.commute)
qed

subsection \<open>Ideals and Divisibility\<close>

lemma int_Idl_subset_ideal: "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} = (k \ Idl\<^bsub>\\<^esub> {l})"
  by (rule int.Idl_subset_ideal') simp_all

lemma Idl_subset_eq_dvd: "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} \ l dvd k"
  by (subst int_Idl_subset_ideal) (auto simp: dvd_def int_Idl)

lemma dvds_eq_Idl: "l dvd k \ k dvd l \ Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l}"
proof -
  have a: "l dvd k \ (Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l})"
    by (rule Idl_subset_eq_dvd[symmetric])
  have b: "k dvd l \ (Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k})"
    by (rule Idl_subset_eq_dvd[symmetric])

  have "l dvd k \ k dvd l \ Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k}"
    by (subst a, subst b, simp)
  also have "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l}"
    by blast
  finally show ?thesis .
qed

lemma Idl_eq_abs: "Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l} \ \l\ = \k\"
  apply (subst dvds_eq_abseq[symmetric])
  apply (rule dvds_eq_Idl[symmetric])
  done

subsection \<open>Ideals and the Modulus\<close>

definition ZMod :: "int \ int \ int set"
  where "ZMod k r = (Idl\<^bsub>\\<^esub> {k}) +>\<^bsub>\\<^esub> r"

lemmas ZMod_defs =
  ZMod_def genideal_def

lemma rcos_zfact:
  assumes kIl: "k \ ZMod l r"
  shows "\x. k = x * l + r"
proof -
  from kIl[unfolded ZMod_def] have "\xl\Idl\<^bsub>\\<^esub> {l}. k = xl + r"
    by (simp add: a_r_coset_defs)
  then obtain xl where xl: "xl \ Idl\<^bsub>\\<^esub> {l}" and k: "k = xl + r"
    by auto
  from xl obtain x where "xl = x * l"
    by (auto simp: int_Idl)
  with k have "k = x * l + r"
    by simp
  then show "\x. k = x * l + r" ..
qed

lemma ZMod_imp_zmod:
  assumes zmods: "ZMod m a = ZMod m b"
  shows "a mod m = b mod m"
proof -
  interpret ideal "Idl\<^bsub>\\<^esub> {m}" \
    by (rule int.genideal_ideal) fast
  from zmods have "b \ ZMod m a"
    unfolding ZMod_def by (simp add: a_repr_independenceD)
  then have "\x. b = x * m + a"
    by (rule rcos_zfact)
  then obtain x where "b = x * m + a"
    by fast
  then have "b mod m = (x * m + a) mod m"
    by simp
  also have "\ = ((x * m) mod m) + (a mod m)"
    by (simp add: mod_add_eq)
  also have "\ = a mod m"
    by simp
  finally have "b mod m = a mod m" .
  then show "a mod m = b mod m" ..
qed

lemma ZMod_mod: "ZMod m a = ZMod m (a mod m)"
proof -
  interpret ideal "Idl\<^bsub>\\<^esub> {m}" \
    by (rule int.genideal_ideal) fast
  show ?thesis
    unfolding ZMod_def
    apply (rule a_repr_independence'[symmetric])
    apply (simp add: int_Idl a_r_coset_defs)
  proof -
    have "a = m * (a div m) + (a mod m)"
      by (simp add: mult_div_mod_eq [symmetric])
    then have "a = (a div m) * m + (a mod m)"
      by simp
    then show "\h. (\x. h = x * m) \ a = h + a mod m"
      by fast
  qed simp
qed

lemma zmod_imp_ZMod:
  assumes modeq: "a mod m = b mod m"
  shows "ZMod m a = ZMod m b"
proof -
  have "ZMod m a = ZMod m (a mod m)"
    by (rule ZMod_mod)
  also have "\ = ZMod m (b mod m)"
    by (simp add: modeq[symmetric])
  also have "\ = ZMod m b"
    by (rule ZMod_mod[symmetric])
  finally show ?thesis .
qed

corollary ZMod_eq_mod: "ZMod m a = ZMod m b \ a mod m = b mod m"
  apply (rule iffI)
  apply (erule ZMod_imp_zmod)
  apply (erule zmod_imp_ZMod)
  done

subsection \<open>Factorization\<close>

definition ZFact :: "int \ int set ring"
  where "ZFact k = \ Quot (Idl\<^bsub>\\<^esub> {k})"

lemmas ZFact_defs = ZFact_def FactRing_def

lemma ZFact_is_cring: "cring (ZFact k)"
  by (simp add: ZFact_def ideal.quotient_is_cring int.cring_axioms int.genideal_ideal)

lemma ZFact_zero: "carrier (ZFact 0) = (\a. {{a}})"
  by (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int.genideal_zero)

lemma ZFact_one: "carrier (ZFact 1) = {UNIV}"
  unfolding ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps int.genideal_one
proof
  have "\a b::int. \x. b = x + a"
    by presburger
  then show "(\a::int. {\h. {h + a}}) \ {UNIV}"
    by force
  then show "{UNIV} \ (\a::int. {\h. {h + a}})"
    by (metis (no_types, lifting) UNIV_I UN_I singletonD singletonI subset_iff)
qed

lemma ZFact_prime_is_domain:
  assumes pprime: "Factorial_Ring.prime p"
  shows "domain (ZFact p)"
  by (simp add: ZFact_def pprime prime_primeideal primeideal.quotient_is_domain)

end

quality98%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.14Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.