src/HOL/Algebra/IntRing.thy

   Id:        $Id$
   Author:    Stephan Hohe, TU Muenchen
 *)
 
 theory IntRing
-imports QuotRing Int
+imports QuotRing Int Primes
 begin
 
 
 section {* The Ring of Integers *}
 

 apply (rule conjI)
  apply (simp add: abseq_imp_dvd)+
 done
 
 
-
-subsection {* The Set of Integers as Algebraic Structure *}
-
-subsubsection {* Definition of @{text "\<Z>"} *}
+subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
 
 constdefs
   int_ring :: "int ring" ("\<Z>")
   "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
 

 apply (intro domain.intro domain_axioms.intro)
   apply (rule int_is_cring)
  apply (unfold int_ring_def, simp+)
 done
 *)
-subsubsection {* Interpretations *}
+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 [unfolded UNIV]:
   total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   by unfold_locales clarsimp
 
 
-subsubsection {* Generated Ideals of @{text "\<Z>"} *}
+subsection {* Generated Ideals of @{text "\<Z>"} *}
 
 lemma int_Idl:
   "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
   apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)
   apply (simp add: cgenideal_def int_ring_def)

   from this and prime
       show "False" by (simp add: prime_def)
 qed
 
 
-subsubsection {* Ideals and Divisibility *}
+subsection {* 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 int.Idl_subset_ideal', simp+)
 

 apply (subst dvds_eq_abseq[symmetric])
 apply (rule dvds_eq_Idl[symmetric])
 done
 
 
-subsubsection {* Ideals and the Modulus *}
+subsection {* Ideals and the Modulus *}
 
 constdefs
    ZMod :: "int => int => int set"
   "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
 

 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 *}
+subsection {* Factorization *}
 
 constdefs
   ZFact :: "int \<Rightarrow> int set ring"
   "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"