(* Title: HOL/Algebra/IntRing.thy Author: Stephan Hohe, TU Muenchen Author: Clemens Ballarin *) theory IntRing imports "HOL-Computational_Algebra.Primes" QuotRing Lattice begin section ‹The Ring of Integers› subsection ‹Some properties of @{typ int}› 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 ‹‹𝒵›: The Set of Integers as Algebraic Structure› 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 ‹Interpretations› text ‹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.› interpretation int: monoid 𝒵 rewrites "carrier 𝒵 = UNIV" and "mult 𝒵 x y = x * y" and "one 𝒵 = 1" and "pow 𝒵 x n = x^n" proof - ― ‹Specification› show "monoid 𝒵" by standard auto then interpret int: monoid 𝒵 . ― ‹Carrier› show "carrier 𝒵 = UNIV" by simp ― ‹Operations› { 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 𝒵 rewrites "finprod 𝒵 f A = prod f A" proof - ― ‹Specification› show "comm_monoid 𝒵" by standard auto then interpret int: comm_monoid 𝒵 . ― ‹Operations› { 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 𝒵 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 - ― ‹Specification› show "abelian_monoid 𝒵" by standard auto then interpret int: abelian_monoid 𝒵 . ― ‹Carrier› show "carrier 𝒵 = UNIV" by simp ― ‹Operations› { 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 𝒵 (* 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 - ― ‹Specification› show "abelian_group 𝒵" proof (rule abelian_groupI) fix x assume "x ∈ carrier 𝒵" then show "∃y ∈ carrier 𝒵. y ⊕⇘_{𝒵⇙}x = 𝟬⇘_{𝒵⇙}" by simp arith qed auto then interpret int: abelian_group 𝒵 . ― ‹Operations› { 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" 𝒵 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 ‹Removal of occurrences of @{term UNIV} in interpretation result --- experimental.› 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 ‹Generated Ideals of ‹𝒵›› lemma int_Idl: "Idl⇘_{𝒵⇙}{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⇘_{𝒵⇙}{p}) 𝒵" proof (rule primeidealI) show "ideal (Idl⇘_{𝒵⇙}{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⇘_{𝒵⇙}{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 ⊗⇘_{𝒵⇙}b ∈ Idl⇘_{𝒵⇙}{p}⟧ ⟹ a ∈ Idl⇘_{𝒵⇙}{p} ∨ b ∈ Idl⇘_{𝒵⇙}{p}" by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def dvd_def mult.commute) qed subsection ‹Ideals and Divisibility› lemma int_Idl_subset_ideal: "Idl⇘_{𝒵⇙}{k} ⊆ Idl⇘_{𝒵⇙}{l} = (k ∈ Idl⇘_{𝒵⇙}{l})" by (rule int.Idl_subset_ideal') simp_all lemma Idl_subset_eq_dvd: "Idl⇘_{𝒵⇙}{k} ⊆ Idl⇘_{𝒵⇙}{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⇘_{𝒵⇙}{k} = Idl⇘_{𝒵⇙}{l}" proof - have a: "l dvd k ⟷ (Idl⇘_{𝒵⇙}{k} ⊆ Idl⇘_{𝒵⇙}{l})" by (rule Idl_subset_eq_dvd[symmetric]) have b: "k dvd l ⟷ (Idl⇘_{𝒵⇙}{l} ⊆ Idl⇘_{𝒵⇙}{k})" by (rule Idl_subset_eq_dvd[symmetric]) have "l dvd k ∧ k dvd l ⟷ Idl⇘_{𝒵⇙}{k} ⊆ Idl⇘_{𝒵⇙}{l} ∧ Idl⇘_{𝒵⇙}{l} ⊆ Idl⇘_{𝒵⇙}{k}" by (subst a, subst b, simp) also have "Idl⇘_{𝒵⇙}{k} ⊆ Idl⇘_{𝒵⇙}{l} ∧ Idl⇘_{𝒵⇙}{l} ⊆ Idl⇘_{𝒵⇙}{k} ⟷ Idl⇘_{𝒵⇙}{k} = Idl⇘_{𝒵⇙}{l}" by blast finally show ?thesis . qed lemma Idl_eq_abs: "Idl⇘_{𝒵⇙}{k} = Idl⇘_{𝒵⇙}{l} ⟷ ¦l¦ = ¦k¦" apply (subst dvds_eq_abseq[symmetric]) apply (rule dvds_eq_Idl[symmetric]) done subsection ‹Ideals and the Modulus› definition ZMod :: "int ⇒ int ⇒ int set" where "ZMod k r = (Idl⇘_{𝒵⇙}{k}) +>⇘_{𝒵⇙}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⇘_{𝒵⇙}{l}. k = xl + r" by (simp add: a_r_coset_defs) then obtain xl where xl: "xl ∈ Idl⇘_{𝒵⇙}{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⇘_{𝒵⇙}{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⇘_{𝒵⇙}{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 ‹Factorization› definition ZFact :: "int ⇒ int set ring" where "ZFact k = 𝒵 Quot (Idl⇘_{𝒵⇙}{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