products/Sources/formale Sprachen/Isabelle/HOL/Algebra/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: IntRing.thy   Sprache: Isabelle

Original von: 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" ("\")
  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>
  { fix x y show "mult \ x y = 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>
  { fix x y have "mult \ x y = x * y" by simp }
  note mult = this
  have one: "one \ = 1" by simp
  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>
  { fix x y show "add \ x y = x + y" by simp }
  note add = this
  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>
  { fix x y have "add \ x y = x + y" by simp }
  note add = this
  have zero: "zero \ = 0" by simp
  {
    fix x
    have "add \ (- x) x = zero \"
      by (simp add: add zero)
    then show "a_inv \ x = - x"
      by (simp add: int.minus_equality)
  }
  note a_inv = this
  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

¤ Dauer der Verarbeitung: 0.22 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff