src/HOL/Algebra/IntRing.thy
 author haftmann Tue Sep 01 16:00:57 2009 +0200 (2009-09-01) changeset 32480 6c19da8e661a parent 30729 461ee3e49ad3 child 33657 a4179bf442d1 permissions -rw-r--r--
some reorganization of number theory
 ballarin@20318 ` 1` ```(* ``` ballarin@20318 ` 2` ``` Title: HOL/Algebra/IntRing.thy ``` ballarin@20318 ` 3` ``` Author: Stephan Hohe, TU Muenchen ``` ballarin@20318 ` 4` ```*) ``` ballarin@20318 ` 5` ballarin@20318 ` 6` ```theory IntRing ``` haftmann@32480 ` 7` ```imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes" ``` ballarin@20318 ` 8` ```begin ``` ballarin@20318 ` 9` ballarin@20318 ` 10` ballarin@20318 ` 11` ```section {* The Ring of Integers *} ``` ballarin@20318 ` 12` ballarin@20318 ` 13` ```subsection {* Some properties of @{typ int} *} ``` ballarin@20318 ` 14` ballarin@20318 ` 15` ```lemma dvds_imp_abseq: ``` ballarin@20318 ` 16` ``` "\l dvd k; k dvd l\ \ abs l = abs (k::int)" ``` ballarin@20318 ` 17` ```apply (subst abs_split, rule conjI) ``` ballarin@20318 ` 18` ``` apply (clarsimp, subst abs_split, rule conjI) ``` ballarin@20318 ` 19` ``` apply (clarsimp) ``` ballarin@20318 ` 20` ``` apply (cases "k=0", simp) ``` ballarin@20318 ` 21` ``` apply (cases "l=0", simp) ``` ballarin@20318 ` 22` ``` apply (simp add: zdvd_anti_sym) ``` ballarin@20318 ` 23` ``` apply clarsimp ``` ballarin@20318 ` 24` ``` apply (cases "k=0", simp) ``` ballarin@20318 ` 25` ``` apply (simp add: zdvd_anti_sym) ``` ballarin@20318 ` 26` ```apply (clarsimp, subst abs_split, rule conjI) ``` ballarin@20318 ` 27` ``` apply (clarsimp) ``` ballarin@20318 ` 28` ``` apply (cases "l=0", simp) ``` ballarin@20318 ` 29` ``` apply (simp add: zdvd_anti_sym) ``` ballarin@20318 ` 30` ```apply (clarsimp) ``` ballarin@20318 ` 31` ```apply (subgoal_tac "-l = -k", simp) ``` ballarin@20318 ` 32` ```apply (intro zdvd_anti_sym, simp+) ``` ballarin@20318 ` 33` ```done ``` ballarin@20318 ` 34` ballarin@20318 ` 35` ```lemma abseq_imp_dvd: ``` ballarin@20318 ` 36` ``` assumes a_lk: "abs l = abs (k::int)" ``` ballarin@20318 ` 37` ``` shows "l dvd k" ``` ballarin@20318 ` 38` ```proof - ``` ballarin@20318 ` 39` ``` from a_lk ``` ballarin@20318 ` 40` ``` have "nat (abs l) = nat (abs k)" by simp ``` ballarin@20318 ` 41` ``` hence "nat (abs l) dvd nat (abs k)" by simp ``` ballarin@20318 ` 42` ``` hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff) ``` ballarin@20318 ` 43` ``` hence "abs l dvd k" by simp ``` ballarin@20318 ` 44` ``` thus "l dvd k" ``` ballarin@20318 ` 45` ``` apply (unfold dvd_def, cases "l<0") ``` ballarin@20318 ` 46` ``` defer 1 apply clarsimp ``` ballarin@20318 ` 47` ``` proof (clarsimp) ``` ballarin@20318 ` 48` ``` fix k ``` ballarin@20318 ` 49` ``` assume l0: "l < 0" ``` ballarin@20318 ` 50` ``` have "- (l * k) = l * (-k)" by simp ``` ballarin@20318 ` 51` ``` thus "\ka. - (l * k) = l * ka" by fast ``` ballarin@20318 ` 52` ``` qed ``` ballarin@20318 ` 53` ```qed ``` ballarin@20318 ` 54` ballarin@20318 ` 55` ```lemma dvds_eq_abseq: ``` ballarin@20318 ` 56` ``` "(l dvd k \ k dvd l) = (abs l = abs (k::int))" ``` ballarin@20318 ` 57` ```apply rule ``` ballarin@20318 ` 58` ``` apply (simp add: dvds_imp_abseq) ``` ballarin@20318 ` 59` ```apply (rule conjI) ``` ballarin@20318 ` 60` ``` apply (simp add: abseq_imp_dvd)+ ``` ballarin@20318 ` 61` ```done ``` ballarin@20318 ` 62` ballarin@20318 ` 63` ballarin@27717 ` 64` ```subsection {* @{text "\"}: The Set of Integers as Algebraic Structure *} ``` ballarin@20318 ` 65` ballarin@20318 ` 66` ```constdefs ``` ballarin@20318 ` 67` ``` int_ring :: "int ring" ("\") ``` ballarin@20318 ` 68` ``` "int_ring \ \carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\" ``` ballarin@20318 ` 69` ballarin@23957 ` 70` ```lemma int_Zcarr [intro!, simp]: ``` ballarin@20318 ` 71` ``` "k \ carrier \" ``` ballarin@23957 ` 72` ``` by (simp add: int_ring_def) ``` ballarin@20318 ` 73` ballarin@20318 ` 74` ```lemma int_is_cring: ``` ballarin@20318 ` 75` ``` "cring \" ``` ballarin@20318 ` 76` ```unfolding int_ring_def ``` ballarin@20318 ` 77` ```apply (rule cringI) ``` ballarin@20318 ` 78` ``` apply (rule abelian_groupI, simp_all) ``` ballarin@20318 ` 79` ``` defer 1 ``` ballarin@20318 ` 80` ``` apply (rule comm_monoidI, simp_all) ``` ballarin@20318 ` 81` ``` apply (rule zadd_zmult_distrib) ``` ballarin@20318 ` 82` ```apply (fast intro: zadd_zminus_inverse2) ``` ballarin@20318 ` 83` ```done ``` ballarin@20318 ` 84` ballarin@23957 ` 85` ```(* ``` ballarin@20318 ` 86` ```lemma int_is_domain: ``` ballarin@20318 ` 87` ``` "domain \" ``` ballarin@20318 ` 88` ```apply (intro domain.intro domain_axioms.intro) ``` ballarin@20318 ` 89` ``` apply (rule int_is_cring) ``` ballarin@20318 ` 90` ``` apply (unfold int_ring_def, simp+) ``` ballarin@20318 ` 91` ```done ``` ballarin@23957 ` 92` ```*) ``` ballarin@27717 ` 93` ```subsection {* Interpretations *} ``` ballarin@20318 ` 94` ballarin@23957 ` 95` ```text {* Since definitions of derived operations are global, their ``` ballarin@23957 ` 96` ``` interpretation needs to be done as early as possible --- that is, ``` ballarin@23957 ` 97` ``` with as few assumptions as possible. *} ``` ballarin@23957 ` 98` wenzelm@30729 ` 99` ```interpretation int: monoid \ ``` ballarin@23957 ` 100` ``` where "carrier \ = UNIV" ``` ballarin@23957 ` 101` ``` and "mult \ x y = x * y" ``` ballarin@23957 ` 102` ``` and "one \ = 1" ``` ballarin@23957 ` 103` ``` and "pow \ x n = x^n" ``` ballarin@23957 ` 104` ```proof - ``` ballarin@23957 ` 105` ``` -- "Specification" ``` haftmann@28823 ` 106` ``` show "monoid \" proof qed (auto simp: int_ring_def) ``` wenzelm@30729 ` 107` ``` then interpret int: monoid \ . ``` ballarin@23957 ` 108` ballarin@23957 ` 109` ``` -- "Carrier" ``` ballarin@23957 ` 110` ``` show "carrier \ = UNIV" by (simp add: int_ring_def) ``` ballarin@23957 ` 111` ballarin@23957 ` 112` ``` -- "Operations" ``` ballarin@23957 ` 113` ``` { fix x y show "mult \ x y = x * y" by (simp add: int_ring_def) } ``` ballarin@23957 ` 114` ``` note mult = this ``` ballarin@23957 ` 115` ``` show one: "one \ = 1" by (simp add: int_ring_def) ``` ballarin@23957 ` 116` ``` show "pow \ x n = x^n" by (induct n) (simp, simp add: int_ring_def)+ ``` ballarin@23957 ` 117` ```qed ``` ballarin@23957 ` 118` wenzelm@30729 ` 119` ```interpretation int: comm_monoid \ ``` haftmann@28524 ` 120` ``` where "finprod \ f A = (if finite A then setprod f A else undefined)" ``` ballarin@23957 ` 121` ```proof - ``` ballarin@23957 ` 122` ``` -- "Specification" ``` haftmann@28823 ` 123` ``` show "comm_monoid \" proof qed (auto simp: int_ring_def) ``` wenzelm@30729 ` 124` ``` then interpret int: comm_monoid \ . ``` ballarin@23957 ` 125` ballarin@23957 ` 126` ``` -- "Operations" ``` ballarin@23957 ` 127` ``` { fix x y have "mult \ x y = x * y" by (simp add: int_ring_def) } ``` ballarin@23957 ` 128` ``` note mult = this ``` ballarin@23957 ` 129` ``` have one: "one \ = 1" by (simp add: int_ring_def) ``` haftmann@28524 ` 130` ``` show "finprod \ f A = (if finite A then setprod f A else undefined)" ``` ballarin@23957 ` 131` ``` proof (cases "finite A") ``` ballarin@23957 ` 132` ``` case True then show ?thesis proof induct ``` ballarin@23957 ` 133` ``` case empty show ?case by (simp add: one) ``` ballarin@23957 ` 134` ``` next ``` ballarin@23957 ` 135` ``` case insert then show ?case by (simp add: Pi_def mult) ``` ballarin@23957 ` 136` ``` qed ``` ballarin@23957 ` 137` ``` next ``` ballarin@23957 ` 138` ``` case False then show ?thesis by (simp add: finprod_def) ``` ballarin@23957 ` 139` ``` qed ``` ballarin@23957 ` 140` ```qed ``` ballarin@23957 ` 141` wenzelm@30729 ` 142` ```interpretation int: abelian_monoid \ ``` ballarin@23957 ` 143` ``` where "zero \ = 0" ``` ballarin@23957 ` 144` ``` and "add \ x y = x + y" ``` haftmann@28524 ` 145` ``` and "finsum \ f A = (if finite A then setsum f A else undefined)" ``` ballarin@23957 ` 146` ```proof - ``` ballarin@23957 ` 147` ``` -- "Specification" ``` haftmann@28823 ` 148` ``` show "abelian_monoid \" proof qed (auto simp: int_ring_def) ``` wenzelm@30729 ` 149` ``` then interpret int: abelian_monoid \ . ``` ballarin@20318 ` 150` ballarin@23957 ` 151` ``` -- "Operations" ``` ballarin@23957 ` 152` ``` { fix x y show "add \ x y = x + y" by (simp add: int_ring_def) } ``` ballarin@23957 ` 153` ``` note add = this ``` ballarin@23957 ` 154` ``` show zero: "zero \ = 0" by (simp add: int_ring_def) ``` haftmann@28524 ` 155` ``` show "finsum \ f A = (if finite A then setsum f A else undefined)" ``` ballarin@23957 ` 156` ``` proof (cases "finite A") ``` ballarin@23957 ` 157` ``` case True then show ?thesis proof induct ``` ballarin@23957 ` 158` ``` case empty show ?case by (simp add: zero) ``` ballarin@23957 ` 159` ``` next ``` ballarin@23957 ` 160` ``` case insert then show ?case by (simp add: Pi_def add) ``` ballarin@23957 ` 161` ``` qed ``` ballarin@23957 ` 162` ``` next ``` ballarin@23957 ` 163` ``` case False then show ?thesis by (simp add: finsum_def finprod_def) ``` ballarin@23957 ` 164` ``` qed ``` ballarin@23957 ` 165` ```qed ``` ballarin@23957 ` 166` wenzelm@30729 ` 167` ```interpretation int: abelian_group \ ``` ballarin@23957 ` 168` ``` where "a_inv \ x = - x" ``` ballarin@23957 ` 169` ``` and "a_minus \ x y = x - y" ``` ballarin@23957 ` 170` ```proof - ``` ballarin@23957 ` 171` ``` -- "Specification" ``` ballarin@23957 ` 172` ``` show "abelian_group \" ``` ballarin@23957 ` 173` ``` proof (rule abelian_groupI) ``` ballarin@23957 ` 174` ``` show "!!x. x \ carrier \ ==> EX y : carrier \. y \\<^bsub>\\<^esub> x = \\<^bsub>\\<^esub>" ``` ballarin@23957 ` 175` ``` by (simp add: int_ring_def) arith ``` ballarin@23957 ` 176` ``` qed (auto simp: int_ring_def) ``` wenzelm@30729 ` 177` ``` then interpret int: abelian_group \ . ``` ballarin@23957 ` 178` ballarin@23957 ` 179` ``` -- "Operations" ``` ballarin@23957 ` 180` ``` { fix x y have "add \ x y = x + y" by (simp add: int_ring_def) } ``` ballarin@23957 ` 181` ``` note add = this ``` ballarin@23957 ` 182` ``` have zero: "zero \ = 0" by (simp add: int_ring_def) ``` ballarin@23957 ` 183` ``` { fix x ``` ballarin@23957 ` 184` ``` have "add \ (-x) x = zero \" by (simp add: add zero) ``` ballarin@23957 ` 185` ``` then show "a_inv \ x = - x" by (simp add: int.minus_equality) } ``` ballarin@23957 ` 186` ``` note a_inv = this ``` ballarin@23957 ` 187` ``` show "a_minus \ x y = x - y" by (simp add: int.minus_eq add a_inv) ``` ballarin@23957 ` 188` ```qed ``` ballarin@23957 ` 189` wenzelm@30729 ` 190` ```interpretation int: "domain" \ ``` haftmann@28823 ` 191` ``` proof qed (auto simp: int_ring_def left_distrib right_distrib) ``` ballarin@23957 ` 192` ballarin@23957 ` 193` ballarin@24131 ` 194` ```text {* Removal of occurrences of @{term UNIV} in interpretation result ``` ballarin@24131 ` 195` ``` --- experimental. *} ``` ballarin@24131 ` 196` ballarin@24131 ` 197` ```lemma UNIV: ``` ballarin@24131 ` 198` ``` "x \ UNIV = True" ``` ballarin@24131 ` 199` ``` "A \ UNIV = True" ``` ballarin@24131 ` 200` ``` "(ALL x : UNIV. P x) = (ALL x. P x)" ``` ballarin@24131 ` 201` ``` "(EX x : UNIV. P x) = (EX x. P x)" ``` ballarin@24131 ` 202` ``` "(True --> Q) = Q" ``` ballarin@24131 ` 203` ``` "(True ==> PROP R) == PROP R" ``` ballarin@24131 ` 204` ``` by simp_all ``` ballarin@24131 ` 205` wenzelm@30729 ` 206` ```interpretation int (* FIXME [unfolded UNIV] *) : ``` ballarin@29237 ` 207` ``` partial_order "(| carrier = UNIV::int set, eq = op =, le = op \ |)" ``` ballarin@27713 ` 208` ``` where "carrier (| carrier = UNIV::int set, eq = op =, le = op \ |) = UNIV" ``` ballarin@27713 ` 209` ``` and "le (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x \ y)" ``` ballarin@27713 ` 210` ``` and "lless (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x < y)" ``` ballarin@23957 ` 211` ```proof - ``` ballarin@27713 ` 212` ``` show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \ |)" ``` haftmann@28823 ` 213` ``` proof qed simp_all ``` ballarin@27713 ` 214` ``` show "carrier (| carrier = UNIV::int set, eq = op =, le = op \ |) = UNIV" ``` ballarin@24131 ` 215` ``` by simp ``` ballarin@27713 ` 216` ``` show "le (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x \ y)" ``` ballarin@24131 ` 217` ``` by simp ``` ballarin@27713 ` 218` ``` show "lless (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x < y)" ``` ballarin@23957 ` 219` ``` by (simp add: lless_def) auto ``` ballarin@23957 ` 220` ```qed ``` ballarin@23957 ` 221` wenzelm@30729 ` 222` ```interpretation int (* FIXME [unfolded UNIV] *) : ``` ballarin@29237 ` 223` ``` lattice "(| carrier = UNIV::int set, eq = op =, le = op \ |)" ``` ballarin@27713 ` 224` ``` where "join (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = max x y" ``` ballarin@27713 ` 225` ``` and "meet (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = min x y" ``` ballarin@23957 ` 226` ```proof - ``` ballarin@27713 ` 227` ``` let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \ |)" ``` ballarin@23957 ` 228` ``` show "lattice ?Z" ``` ballarin@23957 ` 229` ``` apply unfold_locales ``` ballarin@23957 ` 230` ``` apply (simp add: least_def Upper_def) ``` ballarin@23957 ` 231` ``` apply arith ``` ballarin@23957 ` 232` ``` apply (simp add: greatest_def Lower_def) ``` ballarin@23957 ` 233` ``` apply arith ``` ballarin@23957 ` 234` ``` done ``` wenzelm@30729 ` 235` ``` then interpret int: lattice "?Z" . ``` ballarin@23957 ` 236` ``` show "join ?Z x y = max x y" ``` ballarin@23957 ` 237` ``` apply (rule int.joinI) ``` ballarin@23957 ` 238` ``` apply (simp_all add: least_def Upper_def) ``` ballarin@23957 ` 239` ``` apply arith ``` ballarin@23957 ` 240` ``` done ``` ballarin@23957 ` 241` ``` show "meet ?Z x y = min x y" ``` ballarin@23957 ` 242` ``` apply (rule int.meetI) ``` ballarin@23957 ` 243` ``` apply (simp_all add: greatest_def Lower_def) ``` ballarin@23957 ` 244` ``` apply arith ``` ballarin@23957 ` 245` ``` done ``` ballarin@23957 ` 246` ```qed ``` ballarin@23957 ` 247` wenzelm@30729 ` 248` ```interpretation int (* [unfolded UNIV] *) : ``` ballarin@29237 ` 249` ``` total_order "(| carrier = UNIV::int set, eq = op =, le = op \ |)" ``` haftmann@28823 ` 250` ``` proof qed clarsimp ``` ballarin@23957 ` 251` ballarin@20318 ` 252` ballarin@27717 ` 253` ```subsection {* Generated Ideals of @{text "\"} *} ``` ballarin@20318 ` 254` ballarin@20318 ` 255` ```lemma int_Idl: ``` ballarin@20318 ` 256` ``` "Idl\<^bsub>\\<^esub> {a} = {x * a | x. True}" ``` ballarin@23957 ` 257` ``` apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def) ``` ballarin@23957 ` 258` ``` apply (simp add: cgenideal_def int_ring_def) ``` ballarin@23957 ` 259` ``` done ``` ballarin@20318 ` 260` ballarin@20318 ` 261` ```lemma multiples_principalideal: ``` ballarin@20318 ` 262` ``` "principalideal {x * a | x. True } \" ``` ballarin@20318 ` 263` ```apply (subst int_Idl[symmetric], rule principalidealI) ``` ballarin@23957 ` 264` ``` apply (rule int.genideal_ideal, simp) ``` ballarin@20318 ` 265` ```apply fast ``` ballarin@20318 ` 266` ```done ``` ballarin@20318 ` 267` nipkow@29700 ` 268` ballarin@20318 ` 269` ```lemma prime_primeideal: ``` ballarin@20318 ` 270` ``` assumes prime: "prime (nat p)" ``` ballarin@20318 ` 271` ``` shows "primeideal (Idl\<^bsub>\\<^esub> {p}) \" ``` ballarin@20318 ` 272` ```apply (rule primeidealI) ``` ballarin@23957 ` 273` ``` apply (rule int.genideal_ideal, simp) ``` ballarin@20318 ` 274` ``` apply (rule int_is_cring) ``` ballarin@23957 ` 275` ``` apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) ``` ballarin@20318 ` 276` ``` apply (simp add: int_ring_def) ``` ballarin@20318 ` 277` ``` apply clarsimp defer 1 ``` ballarin@23957 ` 278` ``` apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) ``` ballarin@20318 ` 279` ``` apply (simp add: int_ring_def) ``` ballarin@20318 ` 280` ``` apply (elim exE) ``` ballarin@20318 ` 281` ```proof - ``` ballarin@20318 ` 282` ``` fix a b x ``` ballarin@20318 ` 283` ballarin@20318 ` 284` ``` from prime ``` ballarin@20318 ` 285` ``` have ppos: "0 <= p" by (simp add: prime_def) ``` ballarin@20318 ` 286` ``` have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x" ``` ballarin@20318 ` 287` ``` proof - ``` ballarin@20318 ` 288` ``` fix x ``` ballarin@20318 ` 289` ``` assume "nat p dvd nat (abs x)" ``` ballarin@20318 ` 290` ``` hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric]) ``` ballarin@20318 ` 291` ``` thus "p dvd x" by (simp add: ppos) ``` ballarin@20318 ` 292` ``` qed ``` ballarin@20318 ` 293` ballarin@20318 ` 294` ballarin@20318 ` 295` ``` assume "a * b = x * p" ``` ballarin@20318 ` 296` ``` hence "p dvd a * b" by simp ``` nipkow@29700 ` 297` ``` hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff) ``` ballarin@20318 ` 298` ``` hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib) ``` ballarin@20318 ` 299` ``` hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime]) ``` ballarin@20318 ` 300` ``` hence "p dvd a | p dvd b" by (fast intro: unnat) ``` ballarin@20318 ` 301` ``` thus "(EX x. a = x * p) | (EX x. b = x * p)" ``` ballarin@20318 ` 302` ``` proof ``` ballarin@20318 ` 303` ``` assume "p dvd a" ``` ballarin@20318 ` 304` ``` hence "EX x. a = p * x" by (simp add: dvd_def) ``` ballarin@20318 ` 305` ``` from this obtain x ``` ballarin@20318 ` 306` ``` where "a = p * x" by fast ``` ballarin@20318 ` 307` ``` hence "a = x * p" by simp ``` ballarin@20318 ` 308` ``` hence "EX x. a = x * p" by simp ``` ballarin@20318 ` 309` ``` thus "(EX x. a = x * p) | (EX x. b = x * p)" .. ``` ballarin@20318 ` 310` ``` next ``` ballarin@20318 ` 311` ``` assume "p dvd b" ``` ballarin@20318 ` 312` ``` hence "EX x. b = p * x" by (simp add: dvd_def) ``` ballarin@20318 ` 313` ``` from this obtain x ``` ballarin@20318 ` 314` ``` where "b = p * x" by fast ``` ballarin@20318 ` 315` ``` hence "b = x * p" by simp ``` ballarin@20318 ` 316` ``` hence "EX x. b = x * p" by simp ``` ballarin@20318 ` 317` ``` thus "(EX x. a = x * p) | (EX x. b = x * p)" .. ``` ballarin@20318 ` 318` ``` qed ``` ballarin@20318 ` 319` ```next ``` ballarin@20318 ` 320` ``` assume "UNIV = {uu. EX x. uu = x * p}" ``` ballarin@20318 ` 321` ``` from this obtain x ``` ballarin@29242 ` 322` ``` where "1 = x * p" by best ``` ballarin@20318 ` 323` ``` from this [symmetric] ``` ballarin@20318 ` 324` ``` have "p * x = 1" by (subst zmult_commute) ``` ballarin@20318 ` 325` ``` hence "\p * x\ = 1" by simp ``` ballarin@20318 ` 326` ``` hence "\p\ = 1" by (rule abs_zmult_eq_1) ``` ballarin@20318 ` 327` ``` from this and prime ``` ballarin@20318 ` 328` ``` show "False" by (simp add: prime_def) ``` ballarin@20318 ` 329` ```qed ``` ballarin@20318 ` 330` ballarin@20318 ` 331` ballarin@27717 ` 332` ```subsection {* Ideals and Divisibility *} ``` ballarin@20318 ` 333` ballarin@20318 ` 334` ```lemma int_Idl_subset_ideal: ``` ballarin@20318 ` 335` ``` "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} = (k \ Idl\<^bsub>\\<^esub> {l})" ``` ballarin@23957 ` 336` ```by (rule int.Idl_subset_ideal', simp+) ``` ballarin@20318 ` 337` ballarin@20318 ` 338` ```lemma Idl_subset_eq_dvd: ``` ballarin@20318 ` 339` ``` "(Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l}) = (l dvd k)" ``` ballarin@20318 ` 340` ```apply (subst int_Idl_subset_ideal, subst int_Idl, simp) ``` ballarin@20318 ` 341` ```apply (rule, clarify) ``` wenzelm@29424 ` 342` ```apply (simp add: dvd_def) ``` wenzelm@29424 ` 343` ```apply (simp add: dvd_def mult_ac) ``` ballarin@20318 ` 344` ```done ``` ballarin@20318 ` 345` ballarin@20318 ` 346` ```lemma dvds_eq_Idl: ``` ballarin@20318 ` 347` ``` "(l dvd k \ k dvd l) = (Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l})" ``` ballarin@20318 ` 348` ```proof - ``` ballarin@20318 ` 349` ``` have a: "l dvd k = (Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric]) ``` ballarin@20318 ` 350` ``` have b: "k dvd l = (Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric]) ``` ballarin@20318 ` 351` ballarin@20318 ` 352` ``` have "(l dvd k \ k dvd l) = ((Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l}) \ (Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k}))" ``` ballarin@20318 ` 353` ``` by (subst a, subst b, simp) ``` ballarin@20318 ` 354` ``` 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 (rule, fast+) ``` ballarin@20318 ` 355` ``` finally ``` ballarin@20318 ` 356` ``` show ?thesis . ``` ballarin@20318 ` 357` ```qed ``` ballarin@20318 ` 358` ballarin@20318 ` 359` ```lemma Idl_eq_abs: ``` ballarin@20318 ` 360` ``` "(Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l}) = (abs l = abs k)" ``` ballarin@20318 ` 361` ```apply (subst dvds_eq_abseq[symmetric]) ``` ballarin@20318 ` 362` ```apply (rule dvds_eq_Idl[symmetric]) ``` ballarin@20318 ` 363` ```done ``` ballarin@20318 ` 364` ballarin@20318 ` 365` ballarin@27717 ` 366` ```subsection {* Ideals and the Modulus *} ``` ballarin@20318 ` 367` ballarin@20318 ` 368` ```constdefs ``` ballarin@20318 ` 369` ``` ZMod :: "int => int => int set" ``` ballarin@20318 ` 370` ``` "ZMod k r == (Idl\<^bsub>\\<^esub> {k}) +>\<^bsub>\\<^esub> r" ``` ballarin@20318 ` 371` ballarin@20318 ` 372` ```lemmas ZMod_defs = ``` ballarin@20318 ` 373` ``` ZMod_def genideal_def ``` ballarin@20318 ` 374` ballarin@20318 ` 375` ```lemma rcos_zfact: ``` ballarin@20318 ` 376` ``` assumes kIl: "k \ ZMod l r" ``` ballarin@20318 ` 377` ``` shows "EX x. k = x * l + r" ``` ballarin@20318 ` 378` ```proof - ``` ballarin@20318 ` 379` ``` from kIl[unfolded ZMod_def] ``` ballarin@20318 ` 380` ``` have "\xl\Idl\<^bsub>\\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def) ``` ballarin@20318 ` 381` ``` from this obtain xl ``` ballarin@20318 ` 382` ``` where xl: "xl \ Idl\<^bsub>\\<^esub> {l}" ``` ballarin@20318 ` 383` ``` and k: "k = xl + r" ``` ballarin@20318 ` 384` ``` by auto ``` ballarin@20318 ` 385` ``` from xl obtain x ``` ballarin@20318 ` 386` ``` where "xl = x * l" ``` ballarin@20318 ` 387` ``` by (simp add: int_Idl, fast) ``` ballarin@20318 ` 388` ``` from k and this ``` ballarin@20318 ` 389` ``` have "k = x * l + r" by simp ``` ballarin@20318 ` 390` ``` thus "\x. k = x * l + r" .. ``` ballarin@20318 ` 391` ```qed ``` ballarin@20318 ` 392` ballarin@20318 ` 393` ```lemma ZMod_imp_zmod: ``` ballarin@20318 ` 394` ``` assumes zmods: "ZMod m a = ZMod m b" ``` ballarin@20318 ` 395` ``` shows "a mod m = b mod m" ``` ballarin@20318 ` 396` ```proof - ``` ballarin@29237 ` 397` ``` interpret ideal "Idl\<^bsub>\\<^esub> {m}" \ by (rule int.genideal_ideal, fast) ``` ballarin@20318 ` 398` ``` from zmods ``` ballarin@20318 ` 399` ``` have "b \ ZMod m a" ``` ballarin@20318 ` 400` ``` unfolding ZMod_def ``` ballarin@20318 ` 401` ``` by (simp add: a_repr_independenceD) ``` ballarin@20318 ` 402` ``` from this ``` ballarin@20318 ` 403` ``` have "EX x. b = x * m + a" by (rule rcos_zfact) ``` ballarin@20318 ` 404` ``` from this obtain x ``` ballarin@20318 ` 405` ``` where "b = x * m + a" ``` ballarin@20318 ` 406` ``` by fast ``` ballarin@20318 ` 407` ballarin@20318 ` 408` ``` hence "b mod m = (x * m + a) mod m" by simp ``` ballarin@20318 ` 409` ``` also ``` nipkow@29948 ` 410` ``` have "\ = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq) ``` ballarin@20318 ` 411` ``` also ``` ballarin@20318 ` 412` ``` have "\ = a mod m" by simp ``` ballarin@20318 ` 413` ``` finally ``` ballarin@20318 ` 414` ``` have "b mod m = a mod m" . ``` ballarin@20318 ` 415` ``` thus "a mod m = b mod m" .. ``` ballarin@20318 ` 416` ```qed ``` ballarin@20318 ` 417` ballarin@20318 ` 418` ```lemma ZMod_mod: ``` ballarin@20318 ` 419` ``` shows "ZMod m a = ZMod m (a mod m)" ``` ballarin@20318 ` 420` ```proof - ``` ballarin@29237 ` 421` ``` interpret ideal "Idl\<^bsub>\\<^esub> {m}" \ by (rule int.genideal_ideal, fast) ``` ballarin@20318 ` 422` ``` show ?thesis ``` ballarin@20318 ` 423` ``` unfolding ZMod_def ``` ballarin@20318 ` 424` ``` apply (rule a_repr_independence'[symmetric]) ``` ballarin@20318 ` 425` ``` apply (simp add: int_Idl a_r_coset_defs) ``` ballarin@20318 ` 426` ``` apply (simp add: int_ring_def) ``` ballarin@20318 ` 427` ``` proof - ``` ballarin@20318 ` 428` ``` have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality) ``` ballarin@20318 ` 429` ``` hence "a = (a div m) * m + (a mod m)" by simp ``` ballarin@20318 ` 430` ``` thus "\h. (\x. h = x * m) \ a = h + a mod m" by fast ``` ballarin@20318 ` 431` ``` qed simp ``` ballarin@20318 ` 432` ```qed ``` ballarin@20318 ` 433` ballarin@20318 ` 434` ```lemma zmod_imp_ZMod: ``` ballarin@20318 ` 435` ``` assumes modeq: "a mod m = b mod m" ``` ballarin@20318 ` 436` ``` shows "ZMod m a = ZMod m b" ``` ballarin@20318 ` 437` ```proof - ``` ballarin@20318 ` 438` ``` have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod) ``` ballarin@20318 ` 439` ``` also have "\ = ZMod m (b mod m)" by (simp add: modeq[symmetric]) ``` ballarin@20318 ` 440` ``` also have "\ = ZMod m b" by (rule ZMod_mod[symmetric]) ``` ballarin@20318 ` 441` ``` finally show ?thesis . ``` ballarin@20318 ` 442` ```qed ``` ballarin@20318 ` 443` ballarin@20318 ` 444` ```corollary ZMod_eq_mod: ``` ballarin@20318 ` 445` ``` shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)" ``` ballarin@20318 ` 446` ```by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod) ``` ballarin@20318 ` 447` ballarin@20318 ` 448` ballarin@27717 ` 449` ```subsection {* Factorization *} ``` ballarin@20318 ` 450` ballarin@20318 ` 451` ```constdefs ``` ballarin@20318 ` 452` ``` ZFact :: "int \ int set ring" ``` ballarin@20318 ` 453` ``` "ZFact k == \ Quot (Idl\<^bsub>\\<^esub> {k})" ``` ballarin@20318 ` 454` ballarin@20318 ` 455` ```lemmas ZFact_defs = ZFact_def FactRing_def ``` ballarin@20318 ` 456` ballarin@20318 ` 457` ```lemma ZFact_is_cring: ``` ballarin@20318 ` 458` ``` shows "cring (ZFact k)" ``` ballarin@20318 ` 459` ```apply (unfold ZFact_def) ``` ballarin@20318 ` 460` ```apply (rule ideal.quotient_is_cring) ``` ballarin@20318 ` 461` ``` apply (intro ring.genideal_ideal) ``` ballarin@20318 ` 462` ``` apply (simp add: cring.axioms[OF int_is_cring] ring.intro) ``` ballarin@20318 ` 463` ``` apply simp ``` ballarin@20318 ` 464` ```apply (rule int_is_cring) ``` ballarin@20318 ` 465` ```done ``` ballarin@20318 ` 466` ballarin@20318 ` 467` ```lemma ZFact_zero: ``` ballarin@20318 ` 468` ``` "carrier (ZFact 0) = (\a. {{a}})" ``` ballarin@23957 ` 469` ```apply (insert int.genideal_zero) ``` ballarin@20318 ` 470` ```apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) ``` ballarin@20318 ` 471` ```done ``` ballarin@20318 ` 472` ballarin@20318 ` 473` ```lemma ZFact_one: ``` ballarin@20318 ` 474` ``` "carrier (ZFact 1) = {UNIV}" ``` ballarin@20318 ` 475` ```apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) ``` ballarin@23957 ` 476` ```apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps]) ``` ballarin@20318 ` 477` ```apply (rule, rule, clarsimp) ``` ballarin@20318 ` 478` ``` apply (rule, rule, clarsimp) ``` ballarin@20318 ` 479` ``` apply (rule, clarsimp, arith) ``` ballarin@20318 ` 480` ```apply (rule, clarsimp) ``` ballarin@20318 ` 481` ```apply (rule exI[of _ "0"], clarsimp) ``` ballarin@20318 ` 482` ```done ``` ballarin@20318 ` 483` ballarin@20318 ` 484` ```lemma ZFact_prime_is_domain: ``` ballarin@20318 ` 485` ``` assumes pprime: "prime (nat p)" ``` ballarin@20318 ` 486` ``` shows "domain (ZFact p)" ``` ballarin@20318 ` 487` ```apply (unfold ZFact_def) ``` ballarin@20318 ` 488` ```apply (rule primeideal.quotient_is_domain) ``` ballarin@20318 ` 489` ```apply (rule prime_primeideal[OF pprime]) ``` ballarin@20318 ` 490` ```done ``` ballarin@20318 ` 491` ballarin@20318 ` 492` ```end ```