src/HOL/Algebra/IntRing.thy
 changeset 27717 21bbd410ba04 parent 27713 95b36bfe7fc4 child 28085 914183e229e9
equal inserted replaced
27716:96699d8eb49e 27717:21bbd410ba04
`     3   Id:        \$Id\$`
`     3   Id:        \$Id\$`
`     4   Author:    Stephan Hohe, TU Muenchen`
`     4   Author:    Stephan Hohe, TU Muenchen`
`     5 *)`
`     5 *)`
`     6 `
`     6 `
`     7 theory IntRing`
`     7 theory IntRing`
`     8 imports QuotRing Int`
`     8 imports QuotRing Int Primes`
`     9 begin`
`     9 begin`
`    10 `
`    10 `
`    11 `
`    11 `
`    12 section {* The Ring of Integers *}`
`    12 section {* The Ring of Integers *}`
`    13 `
`    13 `
`    60 apply (rule conjI)`
`    60 apply (rule conjI)`
`    61  apply (simp add: abseq_imp_dvd)+`
`    61  apply (simp add: abseq_imp_dvd)+`
`    62 done`
`    62 done`
`    63 `
`    63 `
`    64 `
`    64 `
`    65 `
`    65 subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}`
`    66 subsection {* The Set of Integers as Algebraic Structure *}`
`       `
`    67 `
`       `
`    68 subsubsection {* Definition of @{text "\<Z>"} *}`
`       `
`    69 `
`    66 `
`    70 constdefs`
`    67 constdefs`
`    71   int_ring :: "int ring" ("\<Z>")`
`    68   int_ring :: "int ring" ("\<Z>")`
`    72   "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"`
`    69   "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"`
`    73 `
`    70 `
`    92 apply (intro domain.intro domain_axioms.intro)`
`    89 apply (intro domain.intro domain_axioms.intro)`
`    93   apply (rule int_is_cring)`
`    90   apply (rule int_is_cring)`
`    94  apply (unfold int_ring_def, simp+)`
`    91  apply (unfold int_ring_def, simp+)`
`    95 done`
`    92 done`
`    96 *)`
`    93 *)`
`    97 subsubsection {* Interpretations *}`
`    94 subsection {* Interpretations *}`
`    98 `
`    95 `
`    99 text {* Since definitions of derived operations are global, their`
`    96 text {* Since definitions of derived operations are global, their`
`   100   interpretation needs to be done as early as possible --- that is,`
`    97   interpretation needs to be done as early as possible --- that is,`
`   101   with as few assumptions as possible. *}`
`    98   with as few assumptions as possible. *}`
`   102 `
`    99 `
`   252 interpretation int [unfolded UNIV]:`
`   249 interpretation int [unfolded UNIV]:`
`   253   total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]`
`   250   total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]`
`   254   by unfold_locales clarsimp`
`   251   by unfold_locales clarsimp`
`   255 `
`   252 `
`   256 `
`   253 `
`   257 subsubsection {* Generated Ideals of @{text "\<Z>"} *}`
`   254 subsection {* Generated Ideals of @{text "\<Z>"} *}`
`   258 `
`   255 `
`   259 lemma int_Idl:`
`   256 lemma int_Idl:`
`   260   "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"`
`   257   "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"`
`   261   apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)`
`   258   apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)`
`   262   apply (simp add: cgenideal_def int_ring_def)`
`   259   apply (simp add: cgenideal_def int_ring_def)`
`   340   from this and prime`
`   337   from this and prime`
`   341       show "False" by (simp add: prime_def)`
`   338       show "False" by (simp add: prime_def)`
`   342 qed`
`   339 qed`
`   343 `
`   340 `
`   344 `
`   341 `
`   345 subsubsection {* Ideals and Divisibility *}`
`   342 subsection {* Ideals and Divisibility *}`
`   346 `
`   343 `
`   347 lemma int_Idl_subset_ideal:`
`   344 lemma int_Idl_subset_ideal:`
`   348   "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"`
`   345   "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"`
`   349 by (rule int.Idl_subset_ideal', simp+)`
`   346 by (rule int.Idl_subset_ideal', simp+)`
`   350 `
`   347 `
`   374 apply (subst dvds_eq_abseq[symmetric])`
`   371 apply (subst dvds_eq_abseq[symmetric])`
`   375 apply (rule dvds_eq_Idl[symmetric])`
`   372 apply (rule dvds_eq_Idl[symmetric])`
`   376 done`
`   373 done`
`   377 `
`   374 `
`   378 `
`   375 `
`   379 subsubsection {* Ideals and the Modulus *}`
`   376 subsection {* Ideals and the Modulus *}`
`   380 `
`   377 `
`   381 constdefs`
`   378 constdefs`
`   382    ZMod :: "int => int => int set"`
`   379    ZMod :: "int => int => int set"`
`   383   "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"`
`   380   "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"`
`   384 `
`   381 `
`   457 corollary ZMod_eq_mod:`
`   454 corollary ZMod_eq_mod:`
`   458   shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"`
`   455   shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"`
`   459 by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)`
`   456 by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)`
`   460 `
`   457 `
`   461 `
`   458 `
`   462 subsubsection {* Factorization *}`
`   459 subsection {* Factorization *}`
`   463 `
`   460 `
`   464 constdefs`
`   461 constdefs`
`   465   ZFact :: "int \<Rightarrow> int set ring"`
`   462   ZFact :: "int \<Rightarrow> int set ring"`
`   466   "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"`
`   463   "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"`
`   467 `
`   464 `