src/HOL/Algebra/IntRing.thy

Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;

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

theory IntRing
imports QuotRing IntDef
begin


section {* The Ring of Integers *}

subsection {* Some properties of @{typ int} *}

lemma dvds_imp_abseq:
  "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)"
apply (subst abs_split, rule conjI)
 apply (clarsimp, subst abs_split, rule conjI)
  apply (clarsimp)
  apply (cases "k=0", simp)
  apply (cases "l=0", simp)
  apply (simp add: zdvd_anti_sym)
 apply clarsimp
 apply (cases "k=0", simp)
 apply (simp add: zdvd_anti_sym)
apply (clarsimp, subst abs_split, rule conjI)
 apply (clarsimp)
 apply (cases "l=0", simp)
 apply (simp add: zdvd_anti_sym)
apply (clarsimp)
apply (subgoal_tac "-l = -k", simp)
apply (intro zdvd_anti_sym, simp+)
done

lemma abseq_imp_dvd:
  assumes a_lk: "abs l = abs (k::int)"
  shows "l dvd k"
proof -
  from a_lk
      have "nat (abs l) = nat (abs k)" by simp
  hence "nat (abs l) dvd nat (abs k)" by simp
  hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff)
  hence "abs l dvd k" by simp
  thus "l dvd k" 
  apply (unfold dvd_def, cases "l<0")
   defer 1 apply clarsimp
  proof (clarsimp)
    fix k
    assume l0: "l < 0"
    have "- (l * k) = l * (-k)" by simp
    thus "\<exists>ka. - (l * k) = l * ka" by fast
  qed
qed

lemma dvds_eq_abseq:
  "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
apply rule
 apply (simp add: dvds_imp_abseq)
apply (rule conjI)
 apply (simp add: abseq_imp_dvd)+
done



subsection {* The Set of Integers as Algebraic Structure *}

subsubsection {* Definition of @{text "\<Z>"} *}

constdefs
  int_ring :: "int ring" ("\<Z>")
  "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"

lemma int_Zcarr[simp,intro!]:
  "k \<in> carrier \<Z>"
by (simp add: int_ring_def)

lemma int_is_cring:
  "cring \<Z>"
unfolding int_ring_def
apply (rule cringI)
  apply (rule abelian_groupI, simp_all)
  defer 1
  apply (rule comm_monoidI, simp_all)
 apply (rule zadd_zmult_distrib)
apply (fast intro: zadd_zminus_inverse2)
done

lemma int_is_domain:
  "domain \<Z>"
apply (intro domain.intro domain_axioms.intro)
  apply (rule int_is_cring)
 apply (unfold int_ring_def, simp+)
done

interpretation "domain" ["\<Z>"] by (rule int_is_domain)

lemma int_le_total_order:
  "total_order (| carrier = UNIV::int set, le = op \<le> |)"
  apply (rule partial_order.total_orderI)
   apply (rule partial_order.intro, simp+)
  apply clarsimp
  done

lemma less_int:
  "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
  by (auto simp add: expand_fun_eq lless_def)

lemma join_int:
  "join (| carrier = UNIV::int set, le = op \<le> |) = max"
  apply (simp add: expand_fun_eq max_def)
  apply (rule+)
  apply (rule lattice.joinI)
  apply (simp add: int_le_total_order total_order.axioms)
  apply (simp add: least_def Upper_def)
  apply arith
  apply simp apply simp
  apply (rule lattice.joinI)
  apply (simp add: int_le_total_order total_order.axioms)
  apply (simp add: least_def Upper_def)
  apply arith
  apply simp apply simp
  done

lemma meet_int:
  "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
  apply (simp add: expand_fun_eq min_def)
  apply (rule+)
  apply (rule lattice.meetI)
  apply (simp add: int_le_total_order total_order.axioms)
  apply (simp add: greatest_def Lower_def)
  apply arith
  apply simp apply simp
  apply (rule lattice.meetI)
  apply (simp add: int_le_total_order total_order.axioms)
  apply (simp add: greatest_def Lower_def)
  apply arith
  apply simp apply simp
  done

lemma carrier_int:
  "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
  apply simp
  done

text {* Interpretation unfolding @{text lless}, @{text join} and @{text
  meet} since they have natural representations in @{typ int}. *}

interpretation 
  int [unfolded less_int join_int meet_int carrier_int]:
  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
  by (rule int_le_total_order)


subsubsection {* Generated Ideals of @{text "\<Z>"} *}

lemma int_Idl:
  "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
apply (subst cgenideal_eq_genideal[symmetric], simp add: int_ring_def)
apply (simp add: cgenideal_def int_ring_def)
done

lemma multiples_principalideal:
  "principalideal {x * a | x. True } \<Z>"
apply (subst int_Idl[symmetric], rule principalidealI)
 apply (rule genideal_ideal, simp)
apply fast
done

lemma prime_primeideal:
  assumes prime: "prime (nat p)"
  shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
apply (rule primeidealI)
   apply (rule genideal_ideal, simp)
  apply (rule int_is_cring)
 apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def)
 apply (simp add: int_ring_def)
 apply clarsimp defer 1
 apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def)
 apply (simp add: int_ring_def)
 apply (elim exE)
proof -
  fix a b x

  from prime
      have ppos: "0 <= p" by (simp add: prime_def)
  have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
  proof -
    fix x
    assume "nat p dvd nat (abs x)"
    hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
    thus "p dvd x" by (simp add: ppos)
  qed


  assume "a * b = x * p"
  hence "p dvd a * b" by simp
  hence "nat p dvd nat (abs (a * b))"
  apply (subst nat_dvd_iff, clarsimp)
  apply (rule conjI, clarsimp, simp add: zabs_def)
  proof (clarsimp)
    assume a: " ~ 0 <= p"
    from prime
        have "0 < p" by (simp add: prime_def)
    from a and this
        have "False" by simp
    thus "nat (abs (a * b)) = 0" ..
  qed
  hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
  hence "p dvd a | p dvd b" by (fast intro: unnat)
  thus "(EX x. a = x * p) | (EX x. b = x * p)"
  proof
    assume "p dvd a"
    hence "EX x. a = p * x" by (simp add: dvd_def)
    from this obtain x
        where "a = p * x" by fast
    hence "a = x * p" by simp
    hence "EX x. a = x * p" by simp
    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
  next
    assume "p dvd b"
    hence "EX x. b = p * x" by (simp add: dvd_def)
    from this obtain x
        where "b = p * x" by fast
    hence "b = x * p" by simp
    hence "EX x. b = x * p" by simp
    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
  qed
next
  assume "UNIV = {uu. EX x. uu = x * p}"
  from this obtain x 
      where "1 = x * p" by fast
  from this [symmetric]
      have "p * x = 1" by (subst zmult_commute)
  hence "\<bar>p * x\<bar> = 1" by simp
  hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
  from this and prime
      show "False" by (simp add: prime_def)
qed


subsubsection {* Ideals and Divisibility *}

lemma int_Idl_subset_ideal:
  "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
by (rule Idl_subset_ideal', simp+)

lemma Idl_subset_eq_dvd:
  "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
apply (rule, clarify)
apply (simp add: dvd_def, clarify)
apply (simp add: m_comm)
done

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

  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}))"
  by (subst a, subst b, simp)
  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+)
  finally
    show ?thesis .
qed

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


subsubsection {* Ideals and the Modulus *}

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

lemmas ZMod_defs =
  ZMod_def genideal_def

lemma rcos_zfact:
  assumes kIl: "k \<in> ZMod l r"
  shows "EX x. k = x * l + r"
proof -
  from kIl[unfolded ZMod_def]
      have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def)
  from this obtain xl
      where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
      and k: "k = xl + r"
      by auto
  from xl obtain x
      where "xl = x * l"
      by (simp add: int_Idl, fast)
  from k and this
      have "k = x * l + r" by simp
  thus "\<exists>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>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast)
  from zmods
      have "b \<in> ZMod m a"
      unfolding ZMod_def
      by (simp add: a_repr_independenceD)
  from this
      have "EX x. b = x * m + a" by (rule rcos_zfact)
  from this obtain x
      where "b = x * m + a"
      by fast

  hence "b mod m = (x * m + a) mod m" by simp
  also
      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
  also
      have "\<dots> = a mod m" by simp
  finally
      have "b mod m = a mod m" .
  thus "a mod m = b mod m" ..
qed

lemma ZMod_mod:
  shows "ZMod m a = ZMod m (a mod m)"
proof -
  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast)
  show ?thesis
      unfolding ZMod_def
  apply (rule a_repr_independence'[symmetric])
  apply (simp add: int_Idl a_r_coset_defs)
  apply (simp add: int_ring_def)
  proof -
    have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
    hence "a = (a div m) * m + (a mod m)" by simp
    thus "\<exists>h. (\<exists>x. h = x * m) \<and> 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 "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
  also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
  finally show ?thesis .
qed

corollary ZMod_eq_mod:
  shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)


subsubsection {* Factorization *}

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

lemmas ZFact_defs = ZFact_def FactRing_def

lemma ZFact_is_cring:
  shows "cring (ZFact k)"
apply (unfold ZFact_def)
apply (rule ideal.quotient_is_cring)
 apply (intro ring.genideal_ideal)
  apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
 apply simp
apply (rule int_is_cring)
done

lemma ZFact_zero:
  "carrier (ZFact 0) = (\<Union>a. {{a}})"
apply (insert genideal_zero)
apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
done

lemma ZFact_one:
  "carrier (ZFact 1) = {UNIV}"
apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
apply (subst genideal_one[unfolded int_ring_def, simplified ring_record_simps])
apply (rule, rule, clarsimp)
 apply (rule, rule, clarsimp)
 apply (rule, clarsimp, arith)
apply (rule, clarsimp)
apply (rule exI[of _ "0"], clarsimp)
done

lemma ZFact_prime_is_domain:
  assumes pprime: "prime (nat p)"
  shows "domain (ZFact p)"
apply (unfold ZFact_def)
apply (rule primeideal.quotient_is_domain)
apply (rule prime_primeideal[OF pprime])
done

end